语义保持的编译器阶段

语义保持不是要求源、目标逐条指令相同，而是要求外部观察者无法看到契约禁止的新结果。优化可以删除临时量、合并基本块或把一条指令扩成数步；状态形状和步数因此不同。证明需要一座桥，把两边状态及若干步对应起来，最终比较完整行为。

“保持”也不总是双向相等。源语言可能允许表达式求值顺序的多种结果，编译器固定其中一种，这是减少非确定性，仍满足目标行为包含于源行为。反过来，若目标新增一个崩溃结果，即使它还保留所有正常结果，也破坏上述精化方向。

固定字宽 $w\ge 3$，常量 $2,3,5$ 均可编码，以下值和算术均在模 $2^w$ 下解释。设源 IR 的常量计算分两步：

这里假定 $t,x,y$ 是不同的变量；$\rho (x)$ 是初态中 $x$ 的值，第二次更新必须保留第一次写入的 $t$。常量折叠、传播并删除死临时量后，目标直接含 $y:=5\times x;\mathrm{return}y$。若整数运算均为同一宽度的模运算且赋值无可见事件，源的第一步可由目标零步匹配，第二步由一次目标步匹配，随后返回相同位串。

两边最终环境并不完全相同：源更新了 $t$，目标可能没有。因此状态关系应要求可观察变量相等，并允许死临时量 $t$ 不同；若后续又读取 $t$，这个忽略就不合法。减少内部步能够保持观察，依赖的是“该临时量此后确实不用”的条件，而不只是算术恒等式。

边界例取 $0\times \mathrm{load}(p)\mapsto 0$。在纯数学中等式成立；若读取 $p$ 可能越界 trap、触发 volatile 设备或参与原子顺序，目标删除了源的可见事件或错误，便不是同一契约下的语义保持。类似地，把有符号除法替换为右移可能对负数采用不同舍入方向，几个正数测试全部通过也无法覆盖反例。

回归测试只检查有限输入和有限运行。即使一百万次测试都相等，也不能推出所有状态、路径、发散执行与环境交互上的集合包含。测试适合发现实现错误，语义定理则量化全部合法程序和执行；两者作用互补，不能互相改名。

带余数尾段的计数循环展开理路带余数尾段的计数循环展开Counted-loop unrolling · Quotient-remainder loop unrolling · 计数循环展开将一次捕获的N轮分解为整组与余数尾段，实际复制连续完整循环体，证明每个状态转换和事件恰一次且保序，精确核算控制测试与输出体积。将观察契约落实到一个有事件的闭合片段：进入时捕获非负次数，按商与余数生成连续完整体和尾段，逐个原体证明源变量与事件前缀相同。它不重排体内操作，也不接受提前退出；不变分支外提理路循环不变分支外提Loop unswitching · 循环选择外提对入口已定义且体内不写的条件生成两份完整计数循环，以一次运行时选择代替逐轮选择，并证明事件次序、零轮状态与次数捕获不变。可先产生两个运行时选择的版本，两阶段在同一事件语义下组合。

未定义行为还必须说明采用哪种放宽。若采用本文的“已产生事件前缀之后任意延续”模型，源在第十步越界，并不允许目标抹去前九步已经规定的可见事件。若某语言规范直接对任何会触发 UB 的整个执行不作要求，则不能从规范推出这种前缀保证。精化定理必须固定其中一种解释；不能把一个模型中的前缀结论自动推广到所有 C 编译器契约。

若目标是让源语言中可互换的开放部件，在任意目标客户端中也可互换，则还须讨论翻译的完全抽象理路完全抽象Full abstraction · 全抽象用三个布尔探针证明充分模型并不完全抽象，再构造L到L+por的保守翻译，区分完整程序行为保持与部件等价保持。：$e{\simeq }_S{e}^{\prime }$ 当且仅当 $C(e){\simeq }_{T}C(e^{\prime })$。这里的等价各自量化全部良类型闭合上下文。保持完整程序的行为与保持这个上下文等价是不同契约；前者不能自动替代对目标上下文表达能力的论证。

L到L+por的完整双语言例子理路完全抽象Full abstraction · 全抽象用三个布尔探针证明充分模型并不完全抽象，再构造L到L+por的保守翻译，区分完整程序行为保持与部件等价保持。把这一区别变成可证明任务：保持语法的翻译对所有闭合源布尔程序保留观察，却被新增的目标客户端区分一对源端上下文等价部件。该页给出目标三条并行或求值规则、源程序保守性的双向推导归纳及具体区分上下文，并明确有限求值观察与不公平调度的区别。

若每个阶段 $C_i$ 都在相容观察下满足行为精化，则集合包含的传递性给出整条编译流水线

组合要求相邻 IR 对事件、返回和错误的编码一致；一层把 trap 当事件、下一层把它当 UB，会让形式上可复合的符号失去实际含义。

常用证明方法包括编译器前向模拟理路编译器前向模拟Compiler forward simulation · Forward simulation proof for compilers · 编译正确性的前向模拟以源状态到目标状态的关系逐步匹配每个源执行步，并用正步进展或良基度量约束静默停顿。、编译器后向模拟理路编译器后向模拟Compiler backward simulation · Backward simulation proof for compilers · 编译正确性的后向模拟从目标执行步反向要求源语义给出同迹匹配，以直接排除编译结果新增源程序不允许的行为。、逻辑关系和翻译验证理路翻译验证Translation validation · Per-run translation validation · 编译翻译验证给无环有限位算术IR建立良构检查、总解释器与全输入验证器，证明接受可靠性，并用四位溢出反例拒绝错误优化。。它们是建立语义保持的不同证据接口，并不等于性质本身。选择方法应由确定性、非确定性、内部停顿与阶段实现的可信边界决定。

无环位算术的完整检查器理路翻译验证Translation validation · Per-run translation validation · 编译翻译验证给无环有限位算术IR建立良构检查、总解释器与全输入验证器，证明接受可靠性，并用四位溢出反例拒绝错误优化。把这项契约实例化为有限语言：先查类型、所有分支目标和确定赋值，再证明解释器总返回，最后枚举全部输入。四位加法的溢出分支给出输入15时的7与0反例；只有覆盖已声明的整个有限输入域，枚举才成为该片段的完整判定。

改变循环次序时，完整数组冲突边理路循环数组依赖分析Loop dependence analysis · Array dependence analysis · 循环携带依赖把有限循环展开为带坐标的赋值实例，按真实存储位置建立三类冲突边，并证明保持这些边足以保持任意初始整数内存。与实例双射可以给出另一份语义保持证明。交换理路循环交换Loop interchange · Loop permutation · 循环置换置换矩形循环的嵌套顺序，生成实际For代码，再以实例一一覆盖与依赖边方向验证每次变换。改变原维度的嵌套顺序，分块理路循环分块Loop tiling · Loop blocking · 循环铺块以块循环和裁边循环覆盖每个迭代点，再检查跨块依赖；生成可运行的非整除分块代码，分开证明覆盖、语义与性能条件。另外引入块坐标及尾界；二者都交付实际目标循环，再核验任意整数初始内存的最终内容。这里的结论依赖纯总运算、固定地址和无外部事件，不能直接推广到带异常或可见访问的程序。