近日，上海交通大学人工智能学院曹钦翔副教授与其博士生程章、硕士生吴基洋的研究工作《Denotation-based Compositional Compiler Verification》被程序语言领域顶级期刊ACM Transactions onProgramming Languages and Systems（TOPLAS）接收。TOPLAS是程序设计语言领域历史最为悠久的顶级权威期刊，每年接收的论文仅15-25篇，2021-2025年的5年内，以中国大陆科研院所作为第一单位发表的TOPLAS论文只有3篇。曹钦翔副教授的这一研究聚焦编译器正确性验证问题，提出了一种基于指称语义的全新验证框架。

研究背景

当你写下几行C++语言代码，轻轻按下编译按钮，你可曾想过：这个将高级语言转化为机器指令的编译器，真的值得无条件信任吗？在软件定义一切的时代，编译器作为基础软件的核心一环，其正确性关乎整个数字世界的根基。事实上，GCC、LLVM等现代编译器都是实施复杂变换、运用极致优化的复杂软件，其本身的错误难以避免。对编译器的正确性进行形式化验证，是解决这一问题的根本途径。所谓编译器的形式化验证，就是要用严格的经过机器检验的数学证明论证，对于任意一个合法的源程序（例如C/C++程序），只要经过该编译器编译，该程序与编译器生成的底层程序代码具有对应的整体行为。

长期以来，主流的编译器验证研究大多建立在小步操作语义（operational semantics）和模拟关系（simulation relation）之上。由于这一语义理论体系的基础在于定义程序的每一个单步行为而非整体行为，所以当人们基于这一理论论证两个程序（源代码与底层代码）整体行为的对应性时，就需要引入繁琐证明步骤和复杂的证明技巧。

指称语义（denotational semantics）则是侧重于定义程序整体行为的程序语义理论，其理应是用于完成编译器验证的有力工具，然而，先前的学者都未能成功将此理论应用于编译器验证等更具实践性的程序语言问题中去。本项研究克服了其中的理论挑战和形式化问题，基于指称语义理论提出了把“局部正确”自然、系统地推广为“整体正确”的新方法。

研究成果

全新的指称语义形式化方法：研究团队为编译器中的各种实用程序语言提出了一套系统且易于形式化语义刻画方案。他们将程序的语法成分映射到由若干简单集合构成的语义域之中，使其直接描述程序的整体行为，进而自然地刻画程序不同层次结构之间的组合关系。基于该方案，该研究团队引入了一种新型的语义链接算子来实现开放模块的语义链接，并从代数层面揭示了开放模块的语法链接和语义链接的等价性。例如，程序多模块编译正确性的关键结论就可以归结为以下的简单代数定理：

先前的研究中，人们只知道该结论在极简的作为理论研究prototype的命令式语言中成立，本项研究第一次将该结论拓展到C语言这样的实际编程语言中。

精化代数的可组合验证方法：该研究提出全新的精化代数概念抽象程序行为集合之间的精化关系。简单来说，该精化代数通过引入一个伽马函数以统一的方式来连接源程序与目标程序之间的行为集合，并且要求该伽马函数相对于语义组合算子满足一系列公理。该研究证实了各种实用的行为精化关系以及相应的语义组合算子是精化代数的实例。同时该研究设计了两个自动化证明策略：一个证明策略（ gamma_simpl）利用精化代数的公理将源程序与目标程序之间的行为精化规约为同一类行为集合之间的等价性；另一个证明策略（solvefix）利用KAT代数的公理自动验证行为集合算式之间的等价性。

实际应用

研究团队将该框架用于 CompCert 编译器前端以及若干典型优化的验证，并在若干命令式语言原型上完成了系统性形式化。结果表明，这一方法能够有效实现从子语句到语句、从函数到模块、再从模块到整个程序的逐层组合式验证。

该方法应用到CompCert的可组合验证示例

上图展示了该研究提出的验证方法在CompCert的Cshmgen编译阶段的一个应用示例。左侧定理展示了顺序语句的可组合证明，右侧定理展示了循环语句的可组合证明。该示例通过两个关键自动化证明策略gamma_simpl和solvefix完成证明，说明该研究提出的新方法可以轻量化地实现编译器的可组合验证。

该成果体现了人工智能学院在程序语言、形式化方法与可信软件方向上的持续积累，也为高可信编译器、关键基础软件验证以及自动化证明技术的发展提供了新的研究基础。面向未来，如何让复杂软件系统“可证明地正确”，是数字基础设施建设中的关键科学问题之一。

该论文的第一作者是上海交通大学博士生程章，通讯作者是曹钦翔副教授，文章的其他合作者有：上海交通大学硕士生吴基洋和北京大学助理教授王迪。

论文链接：https://dl.acm.org/doi/epdf/10.1145/3797874