A desired but challenging property of compiler verification is compositionality in the sense that the compilation correctness of a program can be deduced from that of its substructures ranging from statements, functions, and modules incrementally. Previously proposed approaches have devoted extensive effort to module-level compositionality based on small-step semantics and simulation theories. This paper proposes a novel compiler verification framework based on denotational semantics for better compositionality. Specifically, our denotational semantics is defined by semantic functions that map a syntactic component to a semantic domain composed of multiple behavioral \emph{sets}, and compiler correctness is defined by the behavioral refinement between semantic domains of the source and the target programs. Therefore, when proving compiler correctness, we can extensively leverage the algebraic properties of sets. Another important contribution is that our formalization of denotational semantics captures the full meaning of a program and bridges the gap between those based on conventional powerdomains and what realistic compiler verification actually needs. We demonstrate our denotation-based framework viable and practical by applying it to the verification of the front-end of CompCert and showing that the compositionality from the compilation correctness of sub-statements to statements, from functions to modules, and from modules to the whole program (i.e., module-level compositionality) can be achieved similarly.

翻译：编译器验证的一个理想但具有挑战性的属性是组合性——即程序的编译正确性可以从其子结构（从语句、函数到模块）逐步推导得出。以往提出的方法基于小步语义和模拟理论，对模块级组合性进行了广泛研究。本文提出了一种基于指称语义的新型编译器验证框架，以实现更优的组合性。具体而言，我们的指称语义由语义函数定义，这些函数将语法组件映射到由多个行为集合组成的语义域，而编译器正确性则通过源程序和目标程序语义域之间的行为精化来定义。因此，在证明编译器正确性时，我们可以充分利用集合的代数性质。另一重要贡献在于，我们对指称语义的形式化捕捉了程序的完整含义，并弥合了基于传统幂域的理论与真实编译器验证需求之间的鸿沟。我们通过将该框架应用于CompCert前端的验证，证明基于指称的框架是可行且实用的，并展示了从子语句到语句、从函数到模块、从模块到整个程序的编译正确性的组合性（即模块级组合性）均可类似实现。