This paper provides a novel approach to reconciling complex low-level memory model features, such as pointer--integer casts, with desired refinements that are needed to justify the correctness of program transformations. The idea is to use a "two-phased" memory model, one with and unbounded memory and corresponding unbounded integer type, and one with a finite memory; the connection between the two levels is made explicit by our notion of refinement that handles out-of-memory behaviors. This approach allows for more optimizations to be performed and establishes a clear boundary between the idealized semantics of a program and the implementation of that program on finite hardware. To demonstrate the utility of this idea in practice, we instantiate the two-phase memory model in the context of Zakowski et al.'s VIR semantics, yielding infinite and finite memory models of LLVM IR, including low-level features like undef and bitcast. Both the infinite and finite models, which act as specifications, can provably be refined to executable reference interpreters. The semantics justify optimizations, such as dead-alloca-elimination, that were previously impossible or difficult to prove correct.

翻译：本文提出了一种新方法，用于协调复杂低级内存模型特性（例如指针-整数强制转换）与证明程序变换正确性所需的设计细化。其核心思想是采用“两阶段”内存模型：一个阶段具有无限内存及对应的无限整数类型，另一个阶段具有有限内存；通过显式定义的处理内存不足行为的细化概念，将两个层级联系起来。该方法能够支持更多优化操作，并在程序的理想化语义与有限硬件上的程序实现之间建立清晰边界。为验证该思想在实际中的应用价值，我们在Zakowski等人的VIR语义框架内实例化了这一两阶段内存模型，生成了LLVM IR的无限与有限内存模型，涵盖undef、bitcast等低级特性。这两个作为规范说明的模型均可被证明能够细化为可执行参考解释器。该语义支持诸如死分配消除等此前无法证明或难以证明正确性的优化。