A desired but challenging property of compiler verification is compositionality, in the sense that the compilation correctness of a program can be deduced incrementally from that of its substructures ranging from statements, functions, and modules. This article proposes a novel compiler verification framework based on denotational semantics for better compositionality, compared to previous approaches based on small-step operational semantics and simulation theories. Our denotational semantics is defined by semantic functions that map a syntactic component to a semantic domain composed of multiple behavioral \emph{sets}, with compiler correctness established through behavior refinement between the semantic domains of the source and target programs. The main contributions of this article include proposing a denotational semantics for open modules, a novel semantic linking operator, and a refinement algebra that unifies various behavior refinements, making compiler verification structured and compositional. Furthermore, our formalization captures the full meaning of a program and bridges the gap between traditional power-domain-based denotational semantics and the practical needs of compiler verification. We apply our denotation-based framework to verify the front-end of CompCert and typical optimizations on simple prototypes of imperative languages. Our results demonstrate that the compositionality from sub-statements to statements, from functions to modules, and from modules to the whole program can be effectively achieved.

翻译：编译器验证中一项理想但富有挑战性的性质是组合性，即程序的编译正确性能够从它的子结构（包括语句、函数和模块）逐步推导得到。本文提出一种基于指称语义的编译器验证框架，与先前基于小步操作语义和模拟理论的方法相比，该框架能实现更好的组合性。我们的指称语义通过语义函数定义，该函数将语法组件映射到由多个行为集合构成的语义域，编译器正确性则通过源程序和目标程序语义域之间的行为精炼建立。本文的主要贡献包括：提出开放模块的指称语义、一种新型语义连接算子，以及统一多种行为精炼的拓扑代数，使编译器验证更加结构化和组合化。此外，我们的形式化工作捕捉了程序的完整语义，弥合了传统基于幂域的指称语义与编译器验证实际需求之间的鸿沟。我们应用基于指称的框架验证了CompCert前端及命令式语言简单原型上的典型优化。实验结果表明，从子语句到语句、从函数到模块、从模块到整个程序的组合性能够得到有效实现。