2017, Vol. 28
同步数据流语言, 如Lustre[1, 2]和Signal[3], 近年来在实时嵌入式安全攸关系统开发中得到了广泛应用, 此类语言相关开发工具本身的安全性在这些领域中的准入标准也越来越严格.例如, 以Lustre为基础定义建模语言的Scade[4]工具的代码生成器KCG或许是获得民用航空软件生产许可的第1个商用编译器 (在我国航空、高铁及核电等领域也有广泛使用), 其设计开发过程 (严格的V & V过程) 符合民航电子系统的国际标准DO-178B, 并成功应用于空客 (Airbus) A340和A380的设计中.尽管如此, 这并不足以说明Scade的编译器不存在“误编译”.虽然Scade的KCG开发经受了很严格的测试和过程管理, 然而, 和其他软件一样, 通过测试只能发现错误, 严格的过程管理会改进产品质量, 这些努力并不足以保证编译器是正确的.为了进一步提高编译器的安全和可信程度, 仅通过传统的方法显然是不够的, 人们很自然地会想到形式化验证的途径.
人们在几十年前就开展了编译器形式化验证的工作, McCarthy等人在1967年手工证明了一个简单编译器 (从算术表达式翻译到栈式机目标代码) 的正确性[5], 随后, Milner等人在1972年给出了相应的机器证明[6].Dave于2003年的综述列举了1967年~2003年的大部分相关工作[7], 包含从简单语言的单遍编译器到较成熟的代码优化遍历等形形色色的工作.近年来, 随着技术的不断进步, 已经可以验证较为复杂的编译器.CompCert编译器[8]是经过形式化验证的可信编译器的杰出代表.该编译器将C的一个重要子集Clight翻译为PowerPC汇编代码 (后来也支持IA32和ARM后端), 使其可直接应用于范围广泛的嵌入式应用开发.该编译器将编译过程划分为多个阶段, 每个阶段的翻译正确性 (语义保持性) 都借助证明辅助工具Coq[9, 10]进行了证明, 且这些证明可由独立的证明检查器检查, 达到了人们所能期望的最高可信程度[11].Yang等人关于Csmith的研究工作[12]表明: CompCert在正确性方面的表现明显优于常用的开源或商用C编译器.因为CompCert编译器的杰出成就, 其代表性论文[13]的作者Leroy获得了2016年度的10年内最有影响POPL论文奖 (Most Influential POPL Paper Award).
CompCert编译器实现了对翻译过程本身的验证.编译器验证的另外一种可选方案是翻译确认 (translation validation), 由Pnueli等人首先提出[14, 15], 所给出的示范例子的源语言是同步数据流语言Signal[3], 目标语言是C.翻译确认的方法只对编译器的输入和输出做检查, 而不关心编译器的具体实现, 因而具有较好的可重用性.不是直接验证翻译程序, 而是用统一的语义框架为某一翻译过程的源和目标代码建模, 两个模型之间定义一种求精 (refining) 等价关系, 设计一种可证明二者等价性的自动确认程序.确认程序本身是编译器的一部分, 因此必须是一个自动化的过程, 从理论上决定了它往往只能关注部分或抽象性质的保持性, 这是翻译确认方法的不足之处.相对来说, 对编译器的翻译过程本身进行形式化验证是一种比较完美的解决方案, 原理上可以保证源程序的一般性质都可以保持到目标程序, 但这一方法的缺点是扩展性较差.实践中, 较好的选择是针对较为稳定的主体翻译过程本身进行形式化验证, 而对于容易变化的步骤 (比如编译优化) 进行翻译确认.比如, 一些针对优化算法的翻译确认工作[16, 17]可以很好地融合到CompCert编译器中.
L2C是采用类似于CompCert编译器的方法开发的可信编译器.它以扩展的Lustre语言作为源语言, 以CompCert的Clight作为目标语言, 并且从验证方面也与CompCert完全对接.L2C是采用对翻译过程本身进行验证的可信编译器中, 面向实际工业应用的同步数据流语言编译器.
本文第1节概述L2C编译器的基本信息.第2节简介源语言的特性.第3节叙述L2C编译器的主体翻译框架.第4节结合具体例子介绍L2C编译器的几个有特色的核心翻译步骤.第5节以核心翻译步骤为重点, 介绍翻译过程的验证中所考虑的主要问题以及相关的经验.第6节是相关工作的分析.第7节给出本文工作总结以及对未来工作的展望.
1 L2C编译器简介为了满足国内某安全攸关领域的需求, L2C编译器的开发始于2010年9月, 其目标是设计实现一个经过形式化验证的可信编译器, 其源语言是面向领域的同步数据流语言Lustre*(Lustre语言的一个变种, 参考下一节), 目标语言是C, 最终可用作相关领域数字化仪控系统的安全级代码生成器.
L2C编译器的发展进程可归为3个里程碑.一个是面向Lustre*的一个核心子集, 设计实现了L2C编译器的一个原型系统[18], 于2013年6月完成验收.另一个里程碑是已实现除嵌套时钟外Lustre*全部特性的一个单时钟L2C编译器版本, 完全能够满足国内该安全攸关领域目前的实际应用需求, 并于2015年4月完成严格的企业级验收, 这些工作的相关技术和代码已在实际应用中发挥作用.
在上述第2个里程碑之后, 项目组对L2C编译器的设计框架进行了较大程度的优化调整, 目标是拓展应用领域以及开源系统的建设.目前, L2C编译器进入了第3个里程碑的发展阶段, 其目标是在目前面向企业的版本 (不开源) 基础上裁减并适当改造, 形成了覆盖Lustre V6[19]全部特性的可开源版本.目前, 这一L2C编译器的单时钟版本 (L2C-MC) 已经开放源码 (https://github.com/l2ctsinghua/l2c/releases/tag/version-0.8), 支持嵌套时钟的版本处于测试与完善的周期, 其源码不久也将开放.
2 源语言的特性L2C编译器的不同版本, 其源语言 (Lustre*) 可能有所不同, 本文以目前支持的最多特性为准.Lustre*覆盖了Lustre V6[19]的全部特性, 并且根据实际应用的需求在此基础上有许多扩展, 特别是在高阶运算方面比Lustre V6更加丰富.
图 1展示一个简单的Lustre*程序, 可见, 一个Lustre*程序 (program) 由多个节点 (node) 组成, 节点中包含输入参数 (parameters)、输出参数 (returns) 和函数体 (body), 其中函数体又由局部变量 (local variables) 和等式 (或语句) 序列组成, 结构清晰.
|
Fig. 1 A simple Lustre* program 图 1 一个简单的Lustre*程序 |
下面以图 1所示的Lustre*程序为例来阐述Lustre*的某些重要语言特性, 并且在图 2中给出图 1中主节点Main的一组合理输入与输出来直观展示Lustre*语言的这些特性.
(1) 流数据对象.图 2展示的输入输出很直观地体现了Lustre*程序区别于C语言程序的一个很重要的特性, 即在Lustre*中每一个变量都是一个无穷长的流 (stream) 数据对象, 而不仅仅是一个单个的值.每一个周期 (cycle), 变量都可能会有不同的值或者没有值, 其中图 2截取了输入输出前10个周期的值, 后面还有无穷个周期.虽然每个周期的值可能会变化, 但处理逻辑每个周期都一样, 如图 1所示的主节点Main的代码逻辑, 每个周期都一样.Lustre*是同步语言的一种, 所有同步语言均满足同步假设:当前周期的输入时间出现时, 系统能够在下个周期的输入时间出现之间计算出当前周期的输出.这一重要的同步假设使得同步语言在嵌入式实时控制系统中得到大规模应用.
(2) 数据流并发性.不同于C程序, Lustre*程序具有数据流并发性, Lustre*节点中的等式 (相当于语句) 虽然在书写时有先后顺序, 但都是并发执行的.更复杂的情况是, Lustre*程序中的等式 (或语句) 之间存在因果关系, 所以在并发执行时还需要考虑等式 (或语句) 间的拓扑关系.如图 1中第7行~第8行所示, 这两行就存在因果关系.第7行k的赋值依赖于第8行执行的结果, 所以第7行应该在第8行之后执行.这里拓扑关系的具体含义可参见第4节.
(3) 高阶算子.Lustre*支持如map, re等10多个高阶算子, 这些高阶算子可以很方便地操作数组对象, 在编写程序时会更加便利.如图 1中第10行所示的map算子, 以节点 (或称函数) Max以及两个数组x1和x2作为参数, 返回另一个数组p.语义上, 相当于并行执行“p[i]=Max (x1[i], x2[i])”(i从0变到1).
(4) 时态与时钟算子.由于Lustre*的流数据对象特性, 语言提供了时态算子, 比如pre, fby, arrow (→) 等, 可以对流数据进行操作.另外, Lustre*还支持嵌套的时钟, 提供了可改变时钟快慢的算子, 如when使时钟变慢形成下一层嵌套的时钟, 而current与merge使时钟变快, 回到上一层嵌套时钟.如图 2所示, 使用when算子后, 主节点中y1的时钟相对于x3的时钟变慢了 (根据布尔量b取值为true时进行采样); 使用了fby算子之后, 主节点中s相对于y1时钟周期不变, 但每个周期的值向后shift了1个周期 (注意, 这里指相对于y1时钟的shift, 即对应于b取值为true时的时钟周期).
由于源语言Lustre*这些Clight语言中没有的特性, 导致了设计翻译算法的难度较大, 正确性证明工作也显得相当复杂.正是这些原因, 我们对整个可信翻译任务进行了合理的拆分, 形成主体翻译框架, 参见下一节.
3 L2C编译器的主体翻译框架随着源语言 (Lustre*) 特性的增加以及不同开发阶段的不同理念, L2C可信编译器的翻译框架也在不断变化, 先后出现过接近10个稳定的框架图, 图 3是其中最近的一个.
|
Fig. 3 Translation framework of L2C 图 3 L2C翻译过程框架 |
如图 3所示, Lustre*源程序经过词法、语法以及静态语义分析 (类型检查), 翻译到类型良好的抽象语法树 (abstract syntax tree, 简称AST) 形式的高级中间语言Well-typed Lustre* AST代码. Well-typed Lustre* AST代码经过一些简单的预处理变换 (LustreSGen) 生成一种具有规范形式的中间语言LustreS代码.预处理变换主要包括全局常量和类型的合并、拆分表达式列表、通过引入新变量提升某些特殊表达式 (如call和fby表达式) 至等式 (或语句) 级别等.
对于这部分的翻译过程, 目前我们没有去进行形式化验证, 故在图 3中用虚线箭头来表示.词法和语法分析算法或者相关的工具是比较成熟的, 比较可信, 但若要验证它们的正确性却是很困难的, 因此目前的可信编译器 (包括CompCert) 基本上不验证这一部分工作.此外, 其余的翻译工作 (包括类型检查) 相对比较简单, 也比较容易验证, 同时也因为它们是受Lustre*变化影响较大的部分, 所以我们在整个L2C可信编译器的实现中将这部分验证工作放在了最低的优先级.另外, 这些翻译过程的翻译确认程序是比较容易实现的, 这也是我们不急于完成这部分验证工作的重要原因之一.
图 3中后续的翻译过程均表示为实线, 其中所有的变换均经过了形式化验证 (最后一步从Clight到汇编的变换对应于CompCert编译器的一系列翻译过程).这些翻译过程 (CompCert编译器除外) 的主要工作分别是:
(1) Toposort:对LustreS代码的拓扑排序;
(2) LustreRGen:将高阶运算翻译为for循环, 同时完成嵌套时钟的消去;
(3) TransMainArgs:将主节点的输入参数翻译为结构体;
(4) TransTypecmp:将复杂类型比较运算翻译为比较函数;
(5) LustreFGen:消去所有时态算子;
(6) OutstructGen:翻译生成输出结构体;
(7) ClassifyRetsVar:将输出变量从普通变量中分离出来;
(8) ResetfuncGen:生成reset函数;
(9) SimplEnv:将节点输入参数翻译为结构体以简化存储模型;
(10) ClassifyArgsVar:将输入变量从普通变量中分离出来;
(11) CtempGen:生成Clight代码的第1步, 主要是完成到C的语法翻译;
(12) ClightGen:生成Clight代码的第2步, 主要是将Ctemp中的memcpy语义翻译为内存拷贝函数.
对完整翻译过程进一步的细化以及相关的对各翻译过程本身的正确性验证超出了本文的范围.下面我们分两节分别讨论核心的翻译步骤, 以及有关翻译正确性验证的重点疑难问题及其设计实现方案.
4 核心翻译步骤示例本节我们以第2节提到的Lustre*语言的主要特性为线索来解释L2C在翻译过程中的关键节点是如何处理的, 并以图 1的实例来解释Lustre*程序是如何被一步步地翻译到Clight语言的.
4.1 数据流并发性Lustre*程序具有数据流并发性, 而Clight程序却是串行执行的.因此, 翻译过程中的一大难题就是要将Lustre*语句串行化.现在一般采用的因果分析和排序大多采用测试或翻译确认的方法, 未进行形式化验证.对于L2C构建经过形式化证明的可信编译器的目标, 对排序做严格证明是必要的.我们首先定义Lustre*中的因果关系.
(1) 如果一个等式A的左值出现在等式B的右值中, 则说等式B依赖于等式A.
(2) 如果一个节点A的左值出现在等式B的时钟中, 则说等式B依赖于等式B.
然后, 我们定义拓扑排序的性质, 并且定义拓扑排序等价性定理, 即任意两个满足拓扑排序性质的程序在串行执行语义中是等价的, 以此来保证串行化方案的正确性.最后利用Coq实现拓扑排序算法, 将并行的LustreS串行化, 并以此算法完成之前定义的拓扑排序性质和语义等价性证明.
实际翻译效果以图 1中的第7行~第8行为例, 按照第1条因果关系的定义, 图 1中第8行的左值出现在了第7行的右值中, 所以第7行语句依赖于第8行.图 4显示了拓扑排序后LustreS程序中与图 1第7行~第8行对应的代码片段, 在排序后, 图 1的第7行被翻译为图 4中的第4行, 图 1中的第8行被对应到图 4中的第2行, 可见排序后的语句满足因果关系的定义.
|
Fig. 4 Topsorted LustreS intermediate representation of the statement of line 7~8 in Fig. 1 图 4 图 1中第7行~第8行翻译到排序后的LustreS的中间表示 |
4.2 高阶算子
Lustre*提供了10多个高阶算子 (涵盖了LustreV6支持的所有高阶算子), 包括map, red等.图 1第10行使用了map算子, 本节以map为例来介绍高阶算子消去.Lustre*中map算子的形式为map《op; size》(a1, a2, …, an), 其中, a1~an是n个输入数组, size为数组的大小; 而op为一个操作, 可以是运算符或一个节点, 拥有n个输入参数.map算子运算的结果为一个数组, 记为res, 其中, res[i]=op (a1[i], a2[i], …, an[i]).图 1中的p值展示了图 1第10行map算子运算的结果, 可见高阶算子简化了对数组的循环操作.
由于目标语言Clight不支持高阶运算, 所以在翻译过程中, 需要消去Lustre*中的高阶算子.基于高阶算子对数组处理的特点, 我们最终在LustreS到LustreR1阶段将所支持的各个高阶算子按其语义特性展开为Clight支持的语法结构, 主体为for循环结构.
图 5展示了图 1中第10行的map运算在LustreS这一层的中间表示, 可见, 在LustreS这一层L2C不会对map高阶算子做翻译.
|
Fig. 5 LustreS intermediate representation of the statement of line 10 in Fig. 1 图 5 图 1中第10行翻译到LustreS的中间表示 |
经过LustreRGen过程, L2C会将map高阶表达式转换成for循环, 如图 6所示.
|
Fig. 6 LustreR1 intermediate representation of the statement of line 10 in Fig. 1 图 6 图 1中第10行翻译到LustreR1的中间表示 |
通过设计翻译算法将LustreS中的高阶复杂运算分解成LustreR1中多个基础运算的循环, 我们消除了Lustre*程序中的所有高阶算子.
4.3 时态和时钟算子Lustre*支持如LustreV6的一些可以操作流数据的时态算子, 如fby, 以及操作变量时钟的时钟算子, 如when算子.在Lustre*程序中, 每个变量均有自己的时钟, 默认情况下为一个全局基本时钟, 该时钟在每个时钟周期都为True.如图 2中拥有全局基本时钟的x3, 在每个时钟周期都有值.而Lustre*提供的when算子则可以用来改变某个变量的时钟, 如图 2中的y1, b为True的周期有值且与x3当前周期值相同, 但b为False的周期的值则是未定义.再如Lustre*提供的fby算子, 可以用来访问流数据的历史值, 它不改变时钟, 返回值相当于向右shift流数据的值, 如图 2中的s, 它的值在y1上整体向右shift了一位, 并且在shift产生的空缺值中补上了fby函数指定的默认值5.
L2C在LustreS到LustreR1阶段会处理所有时钟算子, 在LustreR3到LustreF1阶段会处理所有的时态算子.以fby算子为例, 在LustreF1中, 图 1中Stay节点内的第27行和第28行, fby算子会被最终翻译成如图 7所示的LustreF1代码, 其中a为Stay节点的输入参数.
|
Fig. 7 LustreF1 intermediate representation of the statement of line 27~28 in Fig. 1 图 7 图 1中第27行~第28行翻译到LustreF1的中间表示 |
L2C引入acg_init变量来标识当前周期是否为第1个周期, 如果是第1个周期, 那么将对变量m和n赋初值, 赋初值时会根据fby指定的周期数来初始化存储m和n的数组大小, 并在数组中对每个值赋予fby指定的默认值, 然后在之后的周期依次循环遍历数组的值, 并在每次读取值之后在数组当前位置记录变量在fby之前当前周期的值.以图 2的输入值为例, 我们将图 7中n对应的fby相关参数acg_fby2前4个周期的变化过程展示出来, 如图 8所示, 便于更好地理解图 7的翻译结果.
4.4 翻译至Clight
经过前面几个核心步骤后, 已经消除了Lustre*中最显著的同步数据流特征, 程序已经十分接近常规的串行命令式语言.又经过后续若干个关键步骤 (包含初始化函数生成ResetfunGen) 到LustreC, 已经十分接近Clight, 经由最后两个步骤实现与CompCert完全对接 (如图 3所示).从LustreC到Clight的翻译过程中, 在语法上几乎没有太大的变化, 但在语义环境上差异较大, 证明工作繁重.图 9展示了L2C翻译图 1所示Lustre*程序中Main节点的最终结果, 具体翻译验证的难点我们将在下一节详细描述.
|
Fig. 9 Clight program translated from the Main node in the Lustre* program in Fig. 1 图 9 由图 1所示Lustre*程序的Main节点翻译而来的Clight程序 |
4.5 流数据对象
如图 1所示, 主节点Main的输入和输出都是无穷长的流数据, 简单来说, 每个时钟周期, Lustre*程序以输入流数据当前时钟周期的值传入Main节点作为输入, 执行得到输出流中当前时钟周期的值.
由于程序获取输入和处理输出的方式不尽相同, 所以L2C只会翻译Lustre*程序中的节点, 并不会给最终的Clight程序中加入C语言的入口函数Main函数.在实际使用中, 如图 10所示, 我们会编写C语言的main函数循环调用调用生成Main函数, 以此来处理流数据.
|
Fig. 10 A solution for Infinite input and output stream 图 10 一种针对Lustre*无限长输入输出流的解决方案 |
5 有关翻译正确性验证的重点疑难问题及其设计实现方案
在L2C可信编译器的设计与实现中, 对于图 3中实线所对应的翻译过程 (CompCert编译器除外) 均借助于Coq证明了正确性 (语义保持性), 然后得出LustreSGen所产生的LustreS代码到Clight代码整个翻译过程的正确性.从LustreS到Clight的任意两个中间语言S和T(设S在前) 之间的语义保持性可描述为
| $\forall P.sound\left( P \right) \Rightarrow sound\left( {\tau \left( P \right)} \right) \wedge {S_S}\left( P \right) \approx {S_T}\left( {\tau \left( P \right)} \right),$ |
其中, τ是翻译函数, 可将S中间语言的程序P翻译至T中间语言的程序τ(P); SS是S中间语言的语义函数, ST是T中间语言的语义函数; sound(P) 和sound(τ(P)) 分别刻画翻译前后的程序应满足的一些Well-formedness性质 (比如第5.4节所述的左右值不相交的性质.另外, 各层中间表示的性质会有所不同), 用以将各阶段翻译过程的证明串连起来得到整个翻译过程的语义保持性, 同时保证在每一阶段可以正常得到SS(P) 和ST(τ(P)); ≈是单向模拟等价关系:SS(P)≈ST(τ(P)) 意味着:P的所有环境变量在τ(P) 都有匹配对象, 且SS(P) 对环境的改变可以由ST(τ(P)) 对相匹配环境的改变进行模拟.对于合法的LustreS程序, 求值结果总是确定的, 这意味着语义计算的确定性 (在非串行语义的情形, 不同求值过程的结果也是确定的).因此, 证明上述单向模拟关系就足够了.
这一验证目标看似比较明确, 然而在具体设计和实现时, LustreS到Clight的验证过程很复杂, 会遇到许许多多的疑难问题.一方面是因为这两种语言差异非常大, LustreS自身有很多独特的特点; 另一方面是因为形式化验证的特点决定证明的过程可能会经过多次反复.限于篇幅, 本文有选择地与读者分享在实际的设计和实现过程中遇到的一些重点疑难问题以及采取的具体方案, 首先讨论若干共性的问题, 然后再针对前一节提到过的核心翻译步骤详细加以说明.
5.1 整体证明框架的定义形式化验证的特点决定了工作最难点在于整体证明框架的定义.形式化证明虽然能够为验证的正确性提供可靠保证, 但验证过程的可复用性、可移植性差.如果在整体框架的定义上出现问题, 即使是微小的问题, 也可能造成整个证明过程需要推倒重来.所以, 如何定义证明框架是能否完成证明的基础, 这直接决定了整体证明的工作量.
为了解决证明框架的定义问题, 我们在总结经验后采取了逆序分层验证的方式.一是由正常的LustreS到Clight的顺序验证, 改为由Clight到LustreS的逆序验证过程.二是尽量将翻译过程拆分为小的步骤, 每步只完成1个功能, 使每一步的的验证尽量简单, 以减少出错的可能性.
逆序验证能够保证每一步验证完成后, 都能形成一个Lustre*子集到Clight的已验证翻译过程.而这部分已验证的工作不会因为前端的翻译和证明的修改而变化.如果按顺序方式来验证, 即使前面的证明已完成, 也可能由于考虑不周而无法完成后续到Clight的证明, 这样, 前面已经完成的证明还是不得不反复修改.而小步分层的验证过程能够使每一层的证明过程简单化, 而越简单的验证越不容易出现错误.而且由于是逆序验证, 已完成的验证和前端待验证的层是独立的, 以减少证明工作的耦合性, 从而减少验证工作移植性差、可复用性差带来的工作量.
5.2 语义值和语义环境的定义Lustre*的操作语义定义是实现L2C编译器中主体翻译阶段正确性验证的基础, 而语义值和语义环境又是操作语义定义的基础.
在实现L2C编译器的证明过程中语义值的定义反复经过多次改动.每次改动都给证明过程带来很大的影响.最初Lustre*语义值的定义与Clight相差非常大, 这一方面导致Lustre*在自身的简化证明过程中难度很大, 另一方面又导致很难和Clight进行对接.最开始的定义尤其在Lustre*语义值的写入和读取时, 不支持读写范围的限制, 这导致最后和Clight对接时, 无法提供相应的条件.经过多次证明的反复修改, 最终决定让Lustre*语义值的定义尽量接近Clight, 这样一方面可以吸收Compcert的成功经验, 另一方面减少语义值的差异能够简化证明的过程.
Lustre*环境的定义是整个工作的难点之一.Lustre*程序的特点决定了Lustre*不能简单使用Clight类似的环境定义.Lustre*的时态运算需要保留历史环境; Lustre*拓扑排序的证明需要环境在等式交换顺序时便于证明; Lustre*翻译过程中会对多种变量进行分类, 要求不同类型变量的环境要有一定的隔离性; call过程的证明是每层证明的重点, 要求环境在一定程度上反映call的调用关系; Lustre*程序执行过程中对类型和时钟的限制很严格, 这要求环境在存储值的同时也要保存变量类型和时钟.环境定义的难点就在于在工作的初期很难预见到Lustre*对环境有如此多的要求, 所以初期所定义的环境自然是很难满足证明需要的, 在证明过程中不断地被修改, 导致证明的过程也反复地被修改.比如, 在第5版也是最终版的环境定义中, 我们修改了第4版将普通变量和需要存储到输出结构体的特殊变量混合存放的做法 (会使证明的难度增加), 分开存放为普通变量和时态运算自定义变量等特殊变量提供了很好的隔离性, 既简化了各层的证明, 又解决了时态运算证明的问题.
5.3 ID管理翻译过程中可能产生大量的中间变量, 而且翻译的层数比较多.如何定义程序中已有的id集合不重复, 如何保证翻译新生成的id集合不重复, 以及如何保证新生成的id集合与已有id集合不相交, 是贯穿整个验证过程的问题.为了解决这个问题, 我们对整个翻译过程中的id进行了分类:程序自带的id、翻译新增中间变量的id、预定义id以及特殊预定义的id.
5.4 左右值不相交的保持性证明这一难点是在CtempGen的证明中处理结构体和数组类型的赋值运算时发现的.结构体和数组类型赋值运算要翻译为Ctemp中memcpy运算, 这需要有一个对地址范围的限制:要么源地址和目的地址的指针不同, 要么源地址和目的地址的偏移量不同, 要么源地址范围和目的地址范围不相交.而Lustre*中不存在指针, 在这一步的证明之前也没有对Lustre*赋值运算左右值的地址进行限制, 所以需要定义Lustre*中赋值的左右值地址不相交.后来发现在call运算中也存在类似的问题.由于地址不相交性质贯穿Lustre*的所有层, 还涉及call运算, 所以带来的工作量非常大.尤其是在部分类型节点的输入和输出参数需要被翻译成结构体的情况下, 这时结构体变量的地址相同, 要证明其偏移范围不相交, 证明过程很复杂.又因为这个定义涉及对表达式的地址求值, 这也增加了证明的工作量.
5.5 程序初始化及reset函数的证明Lustre*程序的主节点和节点列表都有对应的reset函数, 主要用于初始化时态运算中所需的第1周期标识变量acg_init.Reset函数的生成和证明本身难度不大, 难点在于在哪些层生成reset函数.Reset函数的生成位置选择不对, 会使证明难度加大, 还可能因为提供的条件不够造成无法证明.经过多次试证, 才发现节点类reset函数的生成ResetfuncGen放在返回值分类ClassifyRetsVar之后最合适.因为返回值分类后, 将需要翻译为输出结构体的变量都归为一类, 这为reset函数的翻译证明提供了合适的条件.而且reset函数翻译后, 和普通节点类型统一起来, 后续不必单独证明reset函数.reset函数和程序初始化紧密相连, 都是贯穿整个证明的过程, 整体证明的工作量也较大.
5.6 拓扑排序Toposort的证明经过预处理的LustreS程序是未经排序的.需要对节点列表和每个节点内的等式列表进行排序.使排序后的程序的执行按顺序语义执行, 为后续证明提供条件.其中, 节点的排序能够为后续只翻译单个节点时的证明提供条件.这一部分的证明分3个方面:(1) 排序后的程序和排序前的程序是同一个程序的排列; (2) 排序后的程序满足拓扑排序的性质; (3) 对同一程序经排序后, 任意两个满足拓扑排序性质的程序按照LustreS顺序语义执行的结果是等价的.当前版本中定义了LustreS的并发语义, 从并发语义到顺序语义的语义保持性证明本质上与这3个方面的证明是等效的.
5.7 高阶算子与嵌套时钟消去过程LustreRGen的证明为了描述Lustre*复杂的高阶运算, 以及mix等各种特殊运算, LustreS的语法定义比较复杂.LustreS中的高阶运算以及各种特殊运算实际上是由多种简单运算组合而成.比如, 普通的高阶运算可以化简为for循环运算; mapw等特殊高阶运算可以化简为for循环和if运算的组合; flatten运算可以拆分为多个赋值运算的序列; aryprj运算可以拆分为if语句和赋值运算的组合.高阶算子消去的作用就是将LustreS中各种复杂运算拆分为多步简单运算.另外, 嵌套时钟的消除仅需要在等式/语句之前添加相应的条件语句.LustreRGen翻译的过程不产生中间变量, 其证明不涉及环境匹配的问题, 因为翻译前后执行环境都完全相同.但因为需要拆分的复杂运算比较多, 部分复杂运算的拆分过程比较复杂, 使得证明的过程虽然不是很难, 但证明的量比较大.
5.8 时态算子消去过程LustreFGen的证明这一层的翻译主要是消去节点列表中的时态运算, 这也是整体翻译和证明的难点.但通过前面一系列的分类和简化, 使得这一部分的证明得以完成, 需要处理3个时态算子fby, fbyn和arrow, 而且以语句的形式独立呈现.
Fby语句的来源分为两部分, 一是由arrow (→) 和pre算子转换过来的, 二是fbyn中n为1的语句.Fby和fbyn的翻译需要生成后置赋值等式 (参见第5.7节的示例), 负责延续历史值的生成.Fby的翻译比较简单, 通过第1周期标志变量FLAGID, 生成主体的if分类赋值语句, 再生成预定义的中间变量和后置赋值等式.Fbyn语句的翻译较为复杂, 因为其历史值是存放在对应的数组当中的.在第1周期是需要利用for循环对其进行初始化; 在后续周期循环取数组对应位置的值; 后置等式要对fbyn下标进行模加运算, 还需循环更新对应下标的值.Arrow的翻译比较简单, 通过第1周期标志变量FLAGID, 生成if分类赋值语句即可.
Fbyn的翻译还会生成循环变量acg_j, 这需要根据是否有fbyn运算动态生成.后置等式的生成也是一样, 需要根据是否有时态运算动态生成.
LustreFGen的证明比较难, 尤其是fbyn运算的证明.这种复杂的运算证明, 必须在定义语义时与翻译过程相匹配, 从而将复杂的运算拆分成小步的证明.而且之前的各层已经对Lustre*语法和语义进行了大幅度简化, 这使得本层的证明也得到了简化.
Fbyn运算的复杂性使得证明语义保持性时环境的匹配过程相当复杂, 它需要利用for循环对数组进行初始化操作, 这样翻译后的程序环境中就可能增加循环变量LOOPJ, 而且LOOPJ变量需要根据是否有fbyn运算动态生成, 为了适应这种情况的环境匹配, 需要定义以下5条性质:(1) LOOPJ不在全局常量中; (2) 翻译前后局部环境匹配; (3) 翻译后的环境已动态分配LOOPJ变量; (4) 全局常量中的值不在翻译前后的环境当中; (5) LOOPJ不在翻译前的局部环境当中.
进一步地, 还需要处理好Fbyn循环初始化执行的等价证明, 以及后置等式列表的执行等价证明.
5.9 LustreC到Ctemp的证明LustreC到Ctemp翻译过程CtempGen的证明是整个证明过程中工作量最大的, 也是最难的证明.由于证明的量过大, 不得不分成两部分, 第1部分主要是完成一些基本定义和底层证明, 第2部分完成主体的证明.这里我们抛开翻译细节, 主要分析一下证明量大的原因并描述解决方案.
首先是语义环境的差异较大.LsemC的语义环境主要包括全局常量环境gc、存储节点本地变量的环境te、存储节点输入参数变量的ta和存储输出参数的se.Ctemp的环境主要包括全局环境ge、存储节点本地变量地址的环境eC、存储输入参数的环境leC、存储输出参数的环境teC和存储数据的内存mem.一是两者的环境的种类多, 二是环境之间差异大.种类多造成工作量大, 执行每步语义都需要证明所有环境都匹配.环境差异大造成环境匹配的定义较为复杂, 从而证明的难度增加.语义环境中变量种类多所造成的证明工作量的问题是小问题, 通过这种分类和环境隔离的方式, 可以起到通过增加工作量来降低证明难度的目的.这正是前面各层拆分化简想要达到的目的.如果之前不对不同种类变量进行分类隔离, 证明的难度将会更高.通过变量的分类隔离相对缩小了两者环境的差异.
其次, 输出C代码的规范要求造成证明分支多.C代码的规范化是企业版L2C编译器用户方的需求.仅举一个例子, 比如主节点的输入输出结构体的生成.当输入参数为空时, 不生成输入结构体; 当输入参数不为空时, 生成输入结构体.当输出参数为空时, 不生成输出结构体; 当输出参数不为空时, 生成输入参数结构体.输入参数的两种情况和输出参数两种情况组合起来就是4种情况.这意味着Ctemp程序初始化的语义定义要分4种情况, Ctemp程序的执行过程也要分4种情况.程序初始化和执行过程的证明就要分4种情况.诸如此类的情况是证明过程中不得不面对的问题, 只能尽量将各种性质和语义定义得更加抽象, 以适应更普遍的情况.在不考虑C代码输出时 (如只关心通过CompCert将Clight翻译为会编码), 情况会简化一些.
第三, Ctemp语义环境内的隔离性定义.虽然Ctemp语义环境的几种变量都是隔离的, 但在Ctemp中的值主要还是存储在mem中.Ctemp输入参数环境只存储普通值, 结构体和数组类型的值只存储其指针, 而指针对应的存储数据还是在mem中.Ctemp中的输出参数也是一样.还有, Ctemp的全局常量也是存储在mem中.这就使得在Ctemp的mem中写入任意一类变量, 都要证明其不影响其他类型变量的值.即将mem中的多种变量隔离起来.为了解决这个问题, 我们将mem划分几个范围, 并通过多个性质的约束来实现不同类型变量地址范围的隔离性, 包括:(1) 全局常量的存储范围; (2) 输入参数的地址范围; (3) 输出参数的地址范围不相交的性质; (4) 子函数的输出参数和父函数的输出参数的地址范围的关系定义; (5) 函数内局部变量的地址范围.
最后, 函数和语句的互归纳证明.所有各层的节点和语句的证明都要通过互归纳的方式来实现.但由于LustreC到Ctemp的证明比较复杂, 其函数和语句的互归纳的证明也就成为难点.最难之处在于没法一次完成该部分证明目标的定义和互归纳证明分支的定义.因为只有完成该部分的整体证明才能最终说明定义的目标是可证的.事实上, 我们在实现这部分证明时, 证明目标的定义和互归纳证明分支定义通过数十遍的反复证明才最终确定可证.这也是形式化验证证明复杂问题的一个困境, 不到最后完成证明, 很难确定之前的证明是否有用, 甚至可能需要推倒重来.解决的方法只能通过不断拆分化简, 将复杂的问题尽量分解为简单问题, 以避免直接证明复杂的问题.好在之前已经经过了十几层的化简, 否则很难想象证明的过程会有多复杂.
6 相关工作学术界在关于编译器验证的工作中, 面向C、Java之类的常规语言较多[8, 20, 21], 而高级建模语言则并不多见.对于同步数据流语言, 目前尚未见到有开源的或者在实际应用中发挥作用的经过形式化 (机器) 验证的编译器.
与本文工作密切相关的是以Lustre和Signal为代表的同步数据流语言的可信编译器研究.根据安全攸关领域的实际应用需求, 目前这些编译器的目标语言均为C语言.就已知的项目情况而言, Lustre到C可信编译器的代表性研究主要集中于对翻译过程本身进行验证; 而Signal到C可信编译器的代表性研究则是以翻译确认的方法为主.
除了Pnueli等人首次提出翻译确认方法时的示范例子以外[14, 15], 近年来, Van Ngo等人基于翻译确认的思想进一步开展了Signal到C的编译器验证工作[22, 23], 其主要工作是对源代码和目标代码使用统一的语义框架建模, 给出源和目标之间的各种抽象等价关系, 通过对等价关系进行验证来保证某些语义特征的一致性 (比如时钟一致性), 采用求解器自动验证等价关系的成立.
关于Lustre到C可信编译器, 据我们所知, 具有一定规模的研究小组, 除作者课题组与国内面向安全关键领域的某技术企业建立的L2C项目组之外, 国外主要是法国INRIA的M.Pouzet项目组.Pouzet等人于2006年启动了一个有关同步数据流语言Lustre编译器验证的长线项目.该项目的工作[24-26]是将一种具有Lustre语言关键特性的小语言MiniLS翻译至一种基于对象的中间语言 (这一中间语言容易翻译至Java和C), 采用Coq构造其核心翻译步骤并进行证明性证明.
CompCert编译器已被学术界广泛用于构建可信软件的基础平台, 如翻译确认程序的验证[16, 17]、OS内核的验证[27]、静态分析程序的验证[28], 等等.以CompCert编译器为基础构建同步数据流语言可信编译器已成为国际上相关研究团队的兴趣点, 包括M.Pouzet项目组[25].这样做, 其直接优势是可以重用已被广泛认可的CompCert C形式规范 (如语法、语义、存储模型以及相关性质[29, 30]), 并继承其从C到汇编的可信翻译过程.L2C项目组从启动伊始就规划了以Clight为目标语言, 因而在复用CompCert编译器方面占有一定的先机.
在国内, 有一些关于同步语言建模、调度以及代码生成等方面的工作[31, 32], 但与编译器的验证关系不大.也有研究人员开展了关于编译器的验证、验证式编译器等相关领域的工作, 另有一些研究组借助编译器进行程序的静态分析与验证, 但均未涉及到同步语言的编译问题.
7 结论与展望L2C是从同步数据流语言Lustre*(扩展的Lustre语言) 到Clight (CompCert编译器中经过形式化验证部分的源语言) 的可信编译器, 其主体翻译过程本身经过了严格的形式化验证 (借助证明辅助器Coq), 是同类工作中首个面向实际工业应用的同步数据流语言编译器.本文以L2C编译器的核心翻译步骤为出发点, 结合实际开发经验, 列举了L2C编译器的设计与实现过程中的若干重要或难点问题以及所采取的解决方案.本文不是对L2C可信编译器完整和形式的论述, 有许多重要方面未能涉及.同时, 它也不是一份技术文档, 不可能对所讨论到的问题进行详尽描述.本文旨在实践经验的分享, 有利同行读者之间相互学习交流.有意进一步了解L2C编译器细节的读者, 可关注L2C主页 (http://soft.cs.tsinghua.edu.cn:8000/).目前可下载单时钟L2C编译器的开源版本L2C-MC, 很快也会有支持嵌套时钟的开源版本上线.
| [1] | Caspi P, Pilaud D, Halbwachs N, Plaice J. Lustre: A declarative language for programming synchronous systems. In: Proc. of the 14th ACM Symp. on Principles of Programming Languages (POPL'87). Munchen, 1987. 178-188. |
| [2] | Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language LUSTRE. Proc. of the IEEE, 1991, 79(9): 1305–1320 . [doi:10.1109/5.97300] |
| [3] | Guernic M, Gautier T, Maire C. Programming real time applications with signal. Proc. of the IEEE, 1991, 79(9): 1321–1336 . [doi:10.1109/5.97301] |
| [4] | http://www.esterel-technologies.com/products/scade-suite/ |
| [5] | McCarthy J, Painter J. Correctness of a compiler for arithmetical expressions. In: Proc. of the Symp. in Applied Mathematics Aspects of Computer Science, Vol. 19. AMS, 1967. 33-41. |
| [6] | Milner R, Weyhrauch R. Proving compiler correctness in a mechanized logic. In: Proc. of the 7th Annual Machine Intelligence Workshop, Vol.7. Edinburgh University Press, 1972. 51-72. |
| [7] | Dave MA. Compiler verification: A bibliography. ACM SIGSOFT Software Engineering Notes, 2003, 28(6): 2 . [doi:10.1145/966221.966235] |
| [8] | Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115 . [doi:10.1145/1538788.1538814] |
| [9] | Coq Development Team. The Coq Reference Manual. 2016. http://coq.inria.fr/ |
| [10] | Bertot Y, Castéran P. Interactive theorem proving and program development—Coq'Art: The calculus of inductive constructions. In: Proc. of the EATCS on Texts in Theoretical Computer Science. Springer-Verlag, 2004. [doi: 10.1007/978-3-662-07964-5] |
| [11] | Morrisett G. Technical perspective: A compiler's story. Communications of the ACM, 2009, 52(7): 106 . [doi:10.1145/1538788.1538813] |
| [12] | Yang XJ, Chen Y, Eide E, Regehr J. Finding and understanding bugs in C compilers. In: Proc. of the 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2011). 2011. 283-294. [doi: 10.1145/1993498.1993532] |
| [13] | Leroy X. Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. ACM SIGPLAN Notices, 2006, 41(1): 42–54 . [doi:10.1145/1111320.1111042] |
| [14] | Pnueli A, Siegel M, Singerman E. Translation validation. In: Proc. of the TACAS'98. LNCS 1384, 1998. 151-166. [doi:10.1007/BFb0054170] |
| [15] | Pnueli A, Shtrichman O, Siegel M. Translation validation for synchronous languages. In: Proc. of the ICALP'98. LNCS 1443, 1998. 235-246. [doi:10.1007/BFb0055057] |
| [16] | Tristan J-B, Leroy X. Verified validation of lazy code motion. In: Proc. of the PLDI. 2009. 316-326. [doi:10.1145/1542476.1542512] |
| [17] | Tristan J-B, Leroy X. A simple, verified validator for software pipelining. In: Proc. of the POPL. 2010. 83-92. [doi:10.1145/1706299.1706311] |
| [18] | Shi G, Wang SY, Dong Y, Ji ZY, Gan YK, Zhang LB, Zhang YC, Wang L, Yang F. Construction for the trustworthy compiler of a synchronous data-flow language. Ruan Jian Xue Bao/Journal of Software, 2014, 25(2): 341–356 (in Chinese with English abstract). http://www.jos.org.cn/ch/reader/view_abstract.aspx?flag=1&file_no=4542&journal_id=jos [doi:10.13328/j.cnki.jos.004542] |
| [19] | http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6 |
| [20] | Chlipala A. A certified type-preserving compiler from lambda calculus to assembly language. In: Proc. of the 2007 ACM SIGPLAN Conf. on Programming Language Design and Implementation. 2007. 54-65. [doi:10.1145/1273442.1250742] |
| [21] | Klein G, Nipkow T. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. on Programming Languages and Systems, 2006, 28(4): 619–695 . [doi:10.1145/1146809.1146811] |
| [22] | Van Ngo C, Talpin JP, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychronous equations. In: Latella D, Treharne H, eds. Proc. of the IFM 2012. LNCS 7321, 2012. 113-127. [doi:10.1007/978-3-642-30729-4_9] |
| [23] | Van Ngo C, Talpin JP, Gautier T, Le Guernic P. Translation validation for clock transformations in a synchronous compiler. In: Proc. of the 18th Int'l Conf. on Fundamental Approaches to Software Engineering (FASE-ETAPS 2015). LNCS 9039, 2015. 171-185. [doi:10.1007/978-3-662-46675-9_12] |
| [24] | Biernacki D, Colaco JL, Hamon G, Pouzet M. Clock-Directed modular code generation of synchronous data-flow languages. In: Proc. of the ACM Int'l Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES). Tucson, 2008. [doi:10.1145/1375657.1375674] |
| [25] | Auger C, Pouzet M. A formalization and proof of a modular lustre compiler. Technical Report, LRI, 2012. http://www.di.ens.fr/~pouzet/cours/mpri/cours4/scp12 |
| [26] | Auger C. Compilation certifiee de SCADE/LUSTRE [Ph.D. Thesis]. Universite de ParisSud, 2013. |
| [27] | Gu RH, Koenig J, Ramanamandro T, Shao Z, Wu XN, Weng SC, Zhang HZ, Guo Y. Deep specifications and certified abstraction layers. In: Proc. of the POPL 2015. Mumbai: ACM Press, 2015. 593-608. [doi:10.1145/2676726.2676975] |
| [28] | Jourdan J-H, Laporte V, Blazy S, Leroy X, Pichardie D. A formally-verified c static analyzer. In: Proc. of the POPL2015. Mumbai: ACM Press, 2015. 247-259. [doi:10.1145/2676726.2676966] |
| [29] | Blazy S, Leroy X. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009, 43(3): 263–288 . [doi:10.1007/s10817-009-9148-3] |
| [30] | Leroy X, Blazy S. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of. Automated Reasoning, 2008, 41(1): 1–31 . [doi:10.1007/s10817-008-9099-0] |
| [31] | Zhu XY, Yan RJ, Gu YL, Zhang J, Zhang WH, Zhang GQ. Static optimal scheduling for synchronous data flow graphs with model checking. In: Proc. of the 20th Int'l Symp. on Formal Methods (FM 2015). LNCS 9109, At Oslo, 2015. 551-569. [doi:10.1007/978-3-319-19249-9_34] |
| [32] | Yang ZB, Zhao YW, Huang ZQ, Hu K, Ma DF, Bodeveix JP, Filali M. Time-Predicatable multi-threaded code generation with synchronous languages. Ruan Jian Xue Bao/Journal of Software, 2016, 27(3): 611–632 (in Chinese with English abstract). http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4984&flag=1 [doi:10.13328/j.cnki.jos.004984] |
| [18] | 石刚, 王生原, 董渊, 嵇智源, 甘元科, 张玲波, 张煜承, 王蕾, 杨斐. 同步数据流语言可信编译器的构造. 软件学报, 2014, 25(2): 341–356. http://www.jos.org.cn/ch/reader/view_abstract.aspx?flag=1&file_no=4542&journal_id=jos [doi:10.13328/j.cnki.jos.004542] |
| [32] | 杨志斌, 赵永望, 黄志球, 胡凯, 马殿富, BodeveixJP, FilaliM. 基于同步语言的时间可预测多线程代码生成方法. 软件学报, 2016, 27(3): 611–632. http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4984&flag=1 [doi:10.13328/j.cnki.jos.004984] |