经验证的指令选择

形式陈述 ​

指令选择把较抽象 IR 的运算、条件与访存转换成目标机器或机器无关低层 IR 的指令序列。经验证的选择器不仅计算 $Q=\mathrm{select}(P)$，还证明这个编译阶段语义保持公理库语义保持的编译器阶段Semantics-preserving compiler pass · Correct compiler transformation · 编译阶段语义保持在固定观察、错误与未定义行为契约下，要求一次编译变换的目标程序不产生源程序未允许的行为。。典型证明定义源状态与目标状态的关系 $R$，其中对应的控制点、内存和已映射临时量取值一致，并为每种选择规则建立局部引理：

$${\mathrm{eval}}_S(op,\overrightarrow{v},\mu )=v⟹⟨\mathrm{code}(op),\rho ,\mu ⟩{⟶}_T^{\ast }⟨\mathrm{next},\rho [r\mapsto v],{\mu }^{\prime }⟩.$$

${\mu }^{\prime }=\mu$ 只对纯运算成立；load、store、调用和 trap 必须使用各自效果关系。证明还要覆盖条件码、整数宽度、浮点舍入、寻址范围、寄存器类别和合法指令编码。选择器引入的临时量必须新鲜，不能覆盖源仍活跃的值；固定用途寄存器与隐式 clobber 要进入状态关系。

许多机械化后端按源语义规则建立编译器前向模拟公理库编译器前向模拟Compiler forward simulation · Forward simulation proof for compilers · 编译正确性的前向模拟以源状态到目标状态的关系逐步匹配每个源执行步，并用正步进展或良基度量约束静默停顿。：一条源运算可由目标数步匹配，选择阶段制造的中间状态由关系的阶段索引描述。最终的整体行为结论仍依赖所采用模拟转换定理的假设。

分支模式需要单独的布尔对应引理。源比较可能直接产生布尔值，目标则先设置条件码、再由条件跳转读取；证明要表明所有操作数下选中的后继相同，并声明哪些中间指令会破坏 flags。若条件码在源模型中不可见，目标设置 flags 可以作为内部变化，但后续使用前绝不能被未建模指令覆盖。

合法编码也是每条选择规则的前提。把常量选成 add-immediate 之前，必须证明它落在目标指令的有符号或无符号立即数字段内；移位量、重定位类别也要满足各自编码谓词。base-index-scale-displacement 寻址还受可选 scale、位移范围、对齐和地址宽度限制。侧条件不成立时，选择器必须物化常量、分步计算地址或回退到通用序列，不能只凭数学等式输出无法编码的指令。

浮点规则还要固定舍入模式、次正规数与有符号零，并明确 NaN 契约。signaling NaN 是否置 invalid 标志或触发 trap、quiet NaN 的符号与 payload 是否可观察或由语义留作非确定选择，都会改变可接受结果集合；后一种口径要求目标结果属于源允许集合，而非强求任意两台机器给出相同 payload。把乘加收缩为 FMA 还会改变舍入次数和异常时点，只有源契约允许或侧条件排除差异时才可选择。

直觉

指令选择像把抽象算式翻译成一台具体机器会说的话。一条源操作可能恰好命中一条机器指令，也可能需要载入常量、计算地址和多步组合。验证的重点不是“生成汇编能启动”，而是每个模式在所有合法输入、标志位和内存状态上都实现源操作的语义。

模式越聪明，侧条件越重要。把乘以八选择为左移三位，在无符号模算术中直接成立；若源操作会对有符号溢出 trap，而目标移位只截断位串，就必须先证明输入范围不会溢出，或在目标插入检查。模式名字相同不会自动统一两层的异常契约。

例子与边界

源指令为 $r:=(x+4)\times 8$，目标 $w$ 位机器可选择

$$t:={\mathrm{addi}}_w(x,4);r:={\mathrm{slli}}_w(t,3).$$

在两层都解释为模 $2^w$ 运算时，手算有 $r=((x+4)mod{2}^w)\cdot 8mod{2}^w$，与源位向量表达式相等。新鲜 $t$ 只活在两条目标指令之间；关系在第一步后记录 $t=x+4$，第二步后回到主关系。若 $t$ 被错误分配到保存 $x$ 的位置，而源中的 $x$ 在这段代码之后仍活跃，局部证明的 frame 条件会失败。

寻址模式给出另一边界。把 “先算 $p+i\times 4$ 再 load” 合成带 base-index-scale 的 load，需证明地址宽度、对齐和越界检查顺序一致。某些机器在地址计算溢出时只截断，而源 IR 规定 trap；某些 load 还可能触发页故障或 volatile 事件。只比较成功读取的值会漏掉这些观察。

模式覆盖不完整通常只影响编译成功率：选择器可回退到较长的通用序列。若遇到未支持操作却生成近似指令，则是 soundness 问题。calling convention 也不是后续寄存器分配才出现；调用指令的参数位置、返回位置和被破坏寄存器必须在选择结果中正确标注。

例如源条件“若无符号 $x<16$ 则到 $L$”可选为 compare-immediate 后接 unsigned-branch。取 $x=15,16,2^w-1$ 手算，三者应分别走真、假、假边。若误选 signed-branch，最高位为一的 $2^w-1$ 会被解释为 $-1$ 并错误走真边；常见的小正数测试无法发现这一符号扩展边界。

推论与应用

逐模式引理可由选择器结构归纳组合成整函数模拟；基本块终结指令还需证明后继映射与分支条件一致。指令调度若随后重排所选序列，是另一阶段，必须维护数据依赖与 trap 顺序，不能借用选择证明自动覆盖。

经验证的选择器可以完全在证明助理内实现，也可让外部搜索器提出模式并由验证器检查。两种架构的可信基不同，但都需固定机器语义。最终二进制还依赖汇编器、链接器、调用约定实现和硬件符合该语义；单个选择阶段的证明不会越过这些接口自动扩张。

参考资料

• Xavier Leroy, “A Formally Verified Compiler Back-end,” Journal of Automated Reasoning 43(4), 2009, §§5–6.
• Steven S. Muchnick, Advanced Compiler Design and Implementation, Morgan Kaufmann, 1997, Chapter 6.
• Andrew W. Appel, Modern Compiler Implementation in ML, Cambridge University Press, 1998, Chapters 9 and 11.
• Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond, “Verified Compilation of Floating-Point Computations,” Journal of Automated Reasoning 54(2), 2015, pp. 135–163.