Verified compilers aim to guarantee that compilation preserves the observable behavior of source programs. While small-step semantics are widely used in such compilers, they are not always the most convenient framework for structural transformations such as loop optimizations. This paper proposes an approach that leverages both small-step and big-step semantics: small-step semantics are used for local transformations, while big-step semantics are employed for structural transformations. An abstract behavioral semantics is introduced as a common interface between the two styles. Coinductive big-step semantics is extended to correctly handle divergence with both finite and infinite traces, bringing it on par with the expressiveness of small-step semantics. This enables the insertion of big-step transformations into the middle of an existing small-step pipeline, thereby fully preserving all top-level semantic preservation theorems. This approach is practically demonstrated in CompCert by implementing and verifying a few new loop optimizations in big-step Cminor, including loop unswitching and, notably, full loop unrolling.

翻译：验证编译器旨在保证编译过程保持源程序的可观测行为。虽然此类编译器广泛采用小步语义，但其并非总是结构变换（如循环优化）最便捷的框架。本文提出一种同时利用小步与大步语义的方法：小步语义用于局部变换，而大步语义则应用于结构变换。通过引入抽象行为语义作为两种语义风格的统一接口，将余归纳大步语义扩展至正确处理含有限与无限轨迹的发散行为，使其表达能力与小步语义相当。这使得大步语义变换能够嵌入现有小步语义编译流程中，从而完整保留所有顶层语义保持定理。该方法在CompCert中通过实现并验证大步步Cminor数项新型循环优化得到实践验证，包括循环切换及完整的循环展开优化。