Page 132 - 《软件学报》2025年第8期

于涛 等: 基于下推自动机的同步数据流语言可信编译 3555

SCADE 语言是一种以 Lustre 为主, 融合了 Esterel、Signal 语言特性的建模语言; SCADE suite 工具可以图形
化的开发模块, 并将 SCADE 语言编译为 C 语言, 进而编译为可执行代码, 常用于在安全关键系统的建模和开发.
但是, SCADE suite 作为一个商用软件, 其编译过程对于用户不可见, 源码和目标码之间不可追溯, 因此无法对其
进行深入的验证, 保证编译过程的正确性. 虽然对编译器的测试技术的研究已经发展出相当多的成果, 但测试的方
法仍然无法从根本上证明正确性: 对于任意一种语言, 满足其文法规则的程序都是无限多的. 因此, 对于安全关键
系统, 仍然需要引入更加可靠的方法——形式化方法进行验证.
编译器的形式化验证工作始于 1967 年, McCarthy 等人 [9] 证明了一个将算数表达式编译为机器语言的简单编
译器的正确性, 表达式仅允许常量、变量和二进制加法. 尽管该证明面向的目标语言是一个十分简单的语言, 但其
将源语言、目标语言和编译器进行形式化描述的方法对编译器的形式化验证领域有深远的影响.
可信编译器的一个重要实现是 Leroy [10] 于 2009 年发布的 CompCert 编译器. 该编译器将一个 Clight (一个
C 语言的重要子集) 编译到机器码, 使用 Coq [11] 对编译器进行编程并证明其正确性, CompCert 目前已经支持生
成 ARM, PowerPC, RISC-V 和 x86 处理器的机器码. 如图 1 所示, 除了词法分析、语法分析和静态检查外, 整个
编译过程经过 7 种中间表示, 而中间的每种变换都经过了形式化验证. 经过 Csmith 工具检查, CompCert 编译器
在正确性上优于常见的 C 编译器: 它是唯一一个 Csmith 无法找到“错误代码”错误的编译器 [12] .

前端解析
CompCert C Clight … CminorSel
符合性检查
RTL
形式化验证 LTL

Mach Linear
汇编代码生成 (重定向)
目标机汇编代码 (PowerPC, ARM, x86, RISC-V)
图 1 CompCert 编译器前后端架构

在同步数据流语言领域, Paulin 等人 [13] 于 2006 年开启了一个针对 Lustre 语言的可信编译器项目. 其团队的
Bourke 等人 [14] 最终于 2017 年完成了从 Lustre 语言的子集到上文提到的 CompCert 编译器的源语言 Clight 的可信
编译器 Vélus. 该编译器首先将 Lustre 源程序进行规范化和调度, 形成中间表示 SN-Lustre, 并通过常规的编译程序
将其翻译为 Obc 语言, 而该语言可以作为 CompCert 编译器的输入, 进而生成可靠的机器码.
L2C 编译器是清华大学 L2C 项目组于 2010 年开始的一项针对 Lustre 语言的可信编译器项目, 截至 2017 年,
该项目组已经实现了支持多时钟语言特性的 Lustre 编译器, 项目组同时维护了一个开源的 L2C 项目 [15] . L2C 编译
器的编译过程经历了拓扑排序、嵌套时钟消去、时态算子消去、比较运算符翻译等多个步骤, 从源代码到目标码
的编译总共经历 11 种中间状态, 图 2 中用实线指代的每种变换过程都经过了 Coq 的形式化验证.
编译器验证的另外一种可选方案是翻译确认, 该方法由 Pnueli 等人 [16] 首先提出, 在验证同步数据流语言的翻
译过程中使用了翻译确认的方法 [17] . 翻译确认的方法, 不直接证明编译器的正确性, 而是证明翻译过程中的每一
步转换或者优化都正确, 否则停止编译过程.
van Ngo 等人 [18,19] 采用翻译确认的思想实现了 Signal 到 C 语言的可信编译器. 具体来讲, 通过证明翻译前后
代码的语义等价性来证明转换的正确性, 其中的证明采用定理求解器自动验证等价关系的成立.
由于安全关键系统的建模语言商用代码生成器存在不可追溯、不可验证、不可扩展的问题, 本文的研究目标
是在符合 DO-178C 开发规范的环境中, 将同步数据流语言 Lustre 编译为 C 语言目标码, 并保证编译过程中的源
码可追溯性. 为实现这一目标, 本文提出了一种基于下推自动机的编译方法, 该方法基于上下文无关文法, 与所编
译的语言无关, 具有良好的可扩展性.
为保证编译过程的正确性和可靠性, 本文进一步提出了一种基于语义确认的形式化验证方法. 该方法能对编