同步数据流语言代码生成工具的研究进展

摘要

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用，因此与这类语言相关的开发工具本身的安全性问题受到高度关注.同步数据流语言到串行命令式语言的代码生成工具是此类工具的典型代表(如Scade)。构造代码生成工具的途径可分为两大类：一类是传统的方法，例如通过大量测试和严格的过程管理等手段来实现；另一类是通过形式化方法，例如直接对编译器本身进行形式化证明，采用翻译确认的方法等。近年来，形式化方法作为构造和验证代码生成工具的关键途径而得到广泛的重视，有望最大限度地解决“误编译”问题，因而成为新的研究热点。文章在介绍代码生成工具的形式化构造和验证方法的基础上，特别聚焦于同步数据流语言代码生成工具的相关研究工作，对其现状进行综述和分析。

1引言

计算机技术日益广泛地应用于航空航天、高速铁路、核电能源和医疗卫生等领域的安全关键系统（Safety-CriticalSys-tem,SCS）中。SCS一旦失效，将给人类的生命财产、社会生产和生活环境带来巨大的破坏。在现代计算机技术的发展中，相比软件来说，硬件方面的安全性保障技术更加成熟，人为因素导致硬件故障的概率相对较小。虽然人们一直关注于软件安全性问题，并积累了大量研究成果和实践经验，但软件方面的安全保障目前仍旧是计算机系统安全性中的薄弱环节。如何为安全关键系统构造一个基础的安全软件环境是需要解决的首要问题，尤其是对操作系统、编译器等基础软件。本文将针对安全可信的编译器进行介绍。所谓安全可信的编译器，就是要保证编译器做正确的事情，保证它能将符合源语言规范的程序正确翻译到目标语言程序。这里，“正确翻译”主要指功能方面，通常情况下是指源语言到目标语言的语义保持关系（通常被刻画为一种反向的行为模拟等价关系）不能实现“正确翻译”的编译器，则一定存在某种程度的“误编译”错误。作为用于产生代码的工具，编译器的实现和维护自然经过了“精雕玉琢”，同时又“随时随地”经受着无数应用程序的“考验”，因此编译器的正确性问题容易被人们忽视。但了解实际情况的人都知道，编译器的“误编译”问题是司空见惯、习以为常之事。在许多领域中，由于“误编译”一般不会引发本质的问题，又是小概率事件，因此人们往往也忽视了“误编译”所带来的影响。然而，对于安全攸关系统而言，则必须考虑编译器引入的错误，否则在源程序级的高成本验证工作可能在目标程序级失效。实际上，在航空领域的RTCADO-178B/C类标准中，编译器属于需要鉴定的工具类软件,需要按照机载软件的要求同等对待。图1（摘自X。Leroy在POPL^2011的特邀报告⑵）描述了安全关键的嵌入式控制领域中典型的应用程序开发流程：从高级算法描述语言或建模语言所描述的安全级应用程序生成行为等价的C代码，后者接着被翻译成可执行的目标代码。图1中，Simulink是面向建模语言MatLab的著名工具；Scade是基于同步数据流语言Lustre的建模与开发工具。如图1所示，在对安全关键系统进行验证和确认（V&V）时，不能不考虑编译器可能引入的错误。另外，更值得关注的是：若代码生成器或编译器不可信，针对（高级算法描述语言或建模语言）源程序（模型）进行的有关安全性方面的各种努力（模型检查、正确性证明、静态分析及模拟仿真等）则会付之东流。因此，除了要保障应用程序本身的安全性之外，还需要有安全可信的编译器（或代码生成器）。

图1编译器（代码生成器）带来安全隐患的流程

本文将在介绍代码生成工具的形式化构造和验证方法的基础上，特别聚焦于同步数据流语言代码生成工具的相关研究工作及其发展现状。同步数据流语言（如Lustre,Signal）近年来在安全关键领域得到了广泛应用，比如Scade工具将一种扩展的Lustre语言翻译成C语言。在实际应用中，通常会将诸如同步数据流语言之类的高级算法描述语言翻译成常规的串行命令式语言（通常为C语言），如图1的上半部分。同步数据流语言与串行命令式语言之间有很大的语义差距，正如X。Leroy所言，构造这样的代码生成工具（或可信代码生成器）是一项很有价值且富有挑战性的工作。本文第2节先对同步数据流语言进行简要介绍；第3节分析并讨论当前实现代码生成工具的主要途径；第4节侧重对同步数据流语言到串行命令式语言（通常为C语言）代码生成工具的典型工作和发展情况进行综述；最后有针对性地进行小结。

2同步数据流语言

传统的常规语言，如C语言，一直以来都是安全关键领域中使用最为普遍的开发语言。人们为安全有效地使用C语言下了很大功夫，积累了非常丰富的经验。尽管人们通过各种办法来使得基于C语言的系统开发更加安全高效，但毕竟C语言程序层次较低，不易使人们聚焦于问题本身，开发效率受到很大影响，并且也难于验证。因此，基于模型/模型驱动的开发逐步兴起并成为业界主流，由模型自动生成的代码（C代码为主）已占据主导地位，比较著名的建模语言/工具有Simulink和Scade等。有一类建模语言被称为同步语言，特别适合于实时控制系统的开发。所有同步语言均遵循同步假设（synchronyhypothesis），即每个周期内的计算（从输入值得到输出值）都是瞬间完成的；同步语言的语义被要求具有确定性。同步假设以及确定性可以极大地简化实时系统的验证。另外，同步语言通常有严格且可靠的数学定义，对于同步范型有友好的工程设计方法，因此它在实时嵌入式应用的建模、规范描述、验证以及实现等各个层面都已成为重要的技术选项。20世纪80年代，人们就开始了同步范型的理论研究工作随即又出现了许多基于同步假设的语言，并且这些语言都得到了广泛的应用。Esteel,Lustre和Signal是最著名的几种有代表性的同步语言。其中，Esterel是命令式语言；Lustre和Signal是陈述式语言，具有数据流特征，常被称为同步数据流语言。Lustre是函数风格的语言，而Sig-nal是关系型的语言。除Esterel,Lustre和Signal外，学术界和工业界还有其他具有同步特征的语言：LucidSynchrone是对早期数据流语言Lucid的同步化，并采纳了Lustre的许多语言特征；Quartz是一种基于Esterel的面向响应式系统的规范、验证以及实现的同步语言；Argos是State-chats（一种著名的响应式系统的形式化图形语言）的同步化；Synccharts是一种具有Statecharts风格和Esterel语义的图形语言；Grafcet是一种基于有同步特征的Petri网的建模/仿真工具。这些同步语言各自的特点有利于进行一些实质性的静态检查，甚至形式化分析和验证，从而有益于产生安全的代码。在基于同步语言的开发工具中，最著名的是Scade,其代码生成器KCG将一种基于Lustre的建模语言翻译成C语言。KCG应该是获得民用航空软件生产许可（DO-178B/C）的第一个商用代码生成器。目前，Scade工具已渗透到我国航空航天、轨道交通及核电等安全关键领域。虽然同步语言的发展已经相当成熟，并在安全关键的嵌入式实时系统中极具影响力，但一直以来，人们对安全关键系统的可信性要求日益提高，期待在各个环节上都达到最高程度的安全可信。同步语言实现工具（各阶段的编译器、代码生成器）本身的安全性，近年来已引起了学术界和工业界的极大关注和兴趣。本文主要关注同步数据流语言的代码生成工具，Lustre,Signal以及LucidSynchrone是此类语言的典型代表。上面提到的其余同步语言与本文话题关系不大，仅简单提及。此外，LucidSynchrone项目所积累的有关编译器验证的基础研究，均由同一课题组人员转化为对Lustre编译器的验证工作。事实上，关于同步数据流语言编译器的验证工作，从目前学术界和工业界的进展来看，仅需关注与Lustre和Signal相关的工作即可。同步数据流语言具有时钟同步、并发、流数据对象等特征。例如,Lustre语言中，所有的数据都是流（stream），对应于无穷多个逻辑时钟周期，每个周期有一个取值。所有的运算都作用于流。每个逻辑时钟周期都执行同样的计算（即相同的代码），并假设在逻辑时钟周期内计算一定可以完成，即满足所谓的同步假设。各个周期内的计算由多个计算节点（node）组成，每个计算节点内部是一个等式的集合，每个等式都定义流上的运算，等式之间并发执行，是数据驱动的计算过程。时态运算和时钟运算是Lustre语言（以及其他同步数据流语言）中具有特色的流运算。基本的时态运算包括pre,fby和arow（f）等，其中pre和fby可用于访问历史信息；基本的时钟运算包括when,current和merge等算子，可用于改变时钟的快慢。

3代码生成工具的构造途径

如何才能保证编译器的安全和可信？对于编译器来说，安全和可信的具体指标就是其正确性，要保证从源程序到目标程序的翻译过程正确，即保证源语言的行为特征能够在目标语言中被正确地体现，杜绝“误编译”。目前保证可信性的方法主要有两类：1）非形式化的方法（或传统的方法），如采用测试和过程管理;2）采用形式化的方法，主要包括直接对编译器本身进行验证和翻译确认，以及混合使用这些方法。

3.1 通过测试和过程管理实现编译器的可信性

为了保证编译器实现的正确性，普遍的做法是采用大量的测试用例对编译器进行测试。例如，GCC的torture测试集包含几千个C源程序用例，商用的PlumHallStandardValidationSuiteforC有几万个用例,LustreV6的开源软件包中含几百个源程序用例，等等。还有一些Bug-hunting工具，例如Csmith，它可以产生更多或更独特的源程序用例，从而扩大覆盖范围，发现更多的编译器缺陷。尽管如此，采用测试的手段仍是不完善的，如果测试用例的覆盖范围不够广泛，则可能会遗漏编译器中的错误。即便是通过测试发现了错误并且做了修改，也无法保证编译器自身的正确性。实际上，仅编译器自动测试工具Csmith（截至2011年2月）以及EMI/SPE（截至2017年10月）就发现了GCC和LLVM的近1700个编译错误。 Scade工具的代码生成器KCG经过了严格的V&V过程，符合民航电子系统的国际标准DO-178B/C，并且在空客公司的多款客机如A340和A380中成功应用。然而，DO-178B/C主要是以过程质量控制为主的标准，不足以说明Scade的编译器不存在“误编译”。KCG并没有通过形式化的方法加以严格验证，虽然DO-178C中包含了一些非强制的形式化相关条款，但经调研，业界的用户仍会不时发现ScadeKCG的某些翻译漏洞。

3.2 通过对翻译过程本身进行形式化验证实现代码生成工具

为增加编译器的安全和可信程度，仅通过测试和严格的过程管理都是不够的。对编译器进行正确性验证，是解决问题的根本途径。最严格的验证手段莫过于采用形式化方法。工业界也早已意识到形式化软件开发的潜力，在一些安全攸关领域的安全级软件开发标准中也逐步新增了与形式化方法相关的目标或者相应的补充说明。CC（CommonCriteria）安全评估标准［6］中将可信性分为7个级别（EAL1到EAL7），可信性级别越高，其采用形式化规范和验证的程度就越高。航空无线电委员会（RTCA）近期也已推出民航电子系统的国际标准DO-178C,其在DO-178B的基础上增加了对形式化规范和验证的要求，如DO-178C和DO-333等补充说明。近年来，有关编译器形式化验证的研究工作取得了长足的进步，达到了实用化水平，为未来制定新的工业标准奠定了强有力的基础。CompCert28］编译器是经过形式化验证的代码生成工具的杰出代表。该编译器将C的一个重要子集Clight翻译为PowerPC汇编代码（后来也支持IA32和ARM后端，目前已扩展至可支持64位处理器以及开源的RISCV体系结构），其编译过程划分为多个阶段，前端解析过程之后每个阶段的翻译正确性都借助辅助工具Coq进行了证明，且这些证明可由独立的证明检查器检查。这是迄今最强的形式化验证手段，达到了人们所能期望的最高可信程度客］。由于其目标是对主体翻译过程本身进行验证（如图2所示），因此称此类代码生成工具为经过验证的编译器。Yang等关于Csmith的研究工作表明：CompCert在正确性方面的表现明显优于常用的开源或商用C编译器。因CompCert编译器具有的杰出成就,其代表性论文的作者Leroy获得了2016年度的“十年前最有影响POPL论文奖”（MostInfluentialPOPLPaperAward）。

图2 经过验证的编译器(以CompCert为例)

3.3 通过翻译确认技术实现代码生成工具

尽管对编译器的翻译过程本身进行形式化验证是一种比较完美的保证可信性的办法，但是其难度高，工作量大，并且无法扩展（一旦编译器需要修改，那么证明就需要重做）。于是，Pnueli等最早提出了翻译确认的方案［1］。翻译确认的方法不是直接验证翻译程序，而是用统一的语义框架为翻译过程的源和目标代码建模，两个模型之间定义一种特定的语义等价关系/模拟等价关系，设计一种可自动证明二者等价性的确认程序（返回成功与否，成功时或给出证明脚本，不成功时或给出反例）。根据不同的语义模型，确认程序可以通过自动求解或证明、符号计算、模型检查、静态分析等方式来实现模型间的等价性确认。如图3所示的翻译确认过程中，在发现前后中间表示的语义不等价时，会使编译器停下来。若非主体翻译阶段，比如某类中间代码的优化，则可以不必让编译器停下来，不做这一优化即可，如图4所示。

图4翻译确认（针对某个中间表示上的优化）

早期,Necula和Lee提出了PCC（proofcarryingcode）机制，并带动了关于确认式编译器（certifyingcompiler）的研究。可以认为Pnueli的翻译确认是比PCC更通用的机制。PCC机制主要被用来对编译结果进行安全性检查，而不是对编译器进行验证。对于翻译确认来说，如果翻译前后的语义保持性的确认过程比较容易构造，或者说源语言与目标语言的语义模拟等价性关系比较容易定义，则证明也会相对容易，那么验证该等价关系是一个不错的选择。因为该方法最大的优点就是可以不放弃现有的编译框架，其可扩展性较好。一些大型编译器也有类似的工作。但是当源语言与目标语言差异较大（类似于将同步数据流语言翻译成串行语言）时，两种语言的语义等价性关系是很难定义的，其证明过程也会更加困难。相比较而言，当源语言和目标语言的语义定义达到认可的程度时，对翻译过程进行验证是一种彻底的做法，原理上可以保证源程序的一般性质都可以保持到目标程序上。而翻译确认的做法往往只是关注部分性质的保持性（当然，也可以逐步逼近一般性质），因而有可能会存在“虚假预警”（falsealarms）。因此，直接验证翻译过程与翻译确认两种方案各有利弊。目前看来，针对一个完整的编译过程，根据各个翻译的特点，将这两种方案混合使用是一种十分有益的做法。比如，一些针对优化算法的翻译确认工作可以很好地融合到CompCert编译器中。

4 同步数据流语言的代码生成工具

同步数据流语言是应用较为广泛的建模语言，比如著名工具Scade所使用的建模语言是在同步数据流语言Lustre基础上定义的。如图1所示，像Scade和Simulink这样的建模工具，往往是先将建模语言变换到领域语言（许多安全关键领域均采用传统C语言），然后从C这样的领域语言编译到目标语言。对于C语言的可信编译研究近年来已经取得了不错的进展，如前面所提到的Leroy等开发的C编译器Comp-Cert，其原理图参见图2。近年来，针对图1中所示的从高级建模语言到C语言之间的可信编译研究已成为人们的聚焦点⑵。比如，Michael和Strichman采用了翻译确认的方法对从Simulink到C的代码生成器Real-TimeWorkshop（RTW）的编译过程进行了形式化验证。Simulink是MATLAB中的一种基于块状图设计环境的可视化仿真工具，可实现动态系统建模、仿真和分析，被广泛应用于线性系统、非线性系统、数字控制及数字信号处理的建模和仿真中。模型在Simulink中被认为是可执行的描述,借助于RTW代码生成器，这些模型可以生成C代码。这一节主要介绍以Lustre和Signal为代表的同步数据流语言的代码生成工具的研究现状。就目前的进展情况而言，Lustre代码生成工具的代表性研究主要集中于对翻译过程进行验证，即采用图2所示的方法;而Signal代码生成工具的代表性研究则是以翻译确认的方法为主，即采用图3和图4所示的方法。4.1节介绍Lustre代码生成工具的代表性研究，4.2节介绍Signal代码生成工具的代表性研究，4.3节介绍一些相关的基础性研究。

4.1 对翻译过程进行形式化验证的方法

对翻译过程进行形式化验证，通常需要对翻译前后语言的语法和语义以及翻译过程进行严格的形式化描述，然后对翻译前后的语义保持关系进行机器证明。这其中涉及到许多相关的基础性研究，本文为了更好地聚焦，不对这些方面的研究工作展开讨论，仅列举某些关系比较密切的内容，参见4.3节。关于同步数据流语言编译器，这方面最早的工作或许是Gimenez等于1999年试图采用Coq针对ScadeV3进行翻译过程的形式化验证，但这项工作似乎没有坚持下来，因相关资料不详，这里不多述。关于对翻译过程进行验证的同步数据流语言代码生成工具的研究，在国际上较有代表性的长线项目主要是两个团队的工作：一个是法国INRIA的Pouzet团队，另一个是清华大学计算机系的L2C项目组。受CompCert项目的启发，Paulin和Pouzet于2006年启动了一个有关同步数据流语言编译器验证的长线项目，其源语言接近Scade的Lustre语言且具有LucidSynchro-ne的特征。据了解，该项目初期的工作集中于前端，完成了类型检查和时钟演算相关过程的验证；后续又开展了因果性分析程序的验证工作。后来，Biernacki等描述了该项目的一些相关工作细节，他们将Lustre语言的一个较早版本翻译至Java和C代码，采用了一种基于对象的中间语言。再后来，该团队的Auger在其博士论文和技术论文中对该项目进行了较完整的表述（特别是理论基础的论述方面）。从中可进一步了解到，Pouzet团队的工作是针对一种小的但具有全部Lustre语言关键特征的语言MiniLS，并在此基础上实现了同步数据流语言代码生成工具的原型系统句。最近，该团队的Bourke等又基于Biernacki和Auger等的工作，实现了从上述基于对象的中间语言Obc到CompCett的前端中间语言Clight的翻译与验证，从而得到一个核心Lustre子集的代码生成工具Velus。清华大学计算机系的L2C项目组于2010年开始了一项Lustre语言核心子集到C语言的可信翻译器的研究（简称L2C项目）该项工作的原理与CompCert项目一致，工作目标和上述Pouzet团队的项目相似。L2C项目组创立时主要是面向国内核电领域的实际需求，先是实现了单一时钟情形下的一个完整翻译过程的形式化验证，后来又升级到一个可以支持多个嵌套时钟的版本。L2C项目所定义的源语言Lustre综合参考了Scade工具的Lustre语言版本和LustreV6，能够体现同步数据流语言的主要特征。目前，该项目组正在开发和维护一个兼顾学术界和企业界的开源L2C版本。上述两个项目和CompCert项目一样，源语言、目标语言和各阶段中间语言的语法、语义、翻译过程的定义以及语义保持性证明都在交互式辅助定理证明工具Coq中实现。然而，二者在许多方面存在不同。首先是源语言的差异，L2C编译器立项时是出于国内某安全关键领域的实际需求，因此企业版的源语言最终定格为ScadeLustre语言的一个核心子集，而开源版的源语言则是将其中的高阶迭代算子（9个）替换为了LustreV6中的高阶迭代算子（5个）与L2C相比，Pouzet团队的工作目前主要是面向学术研究，其源语言（包括最新版编译器V§lus的源语言）不支持许多数组和结构体上的操作，尚未支持任何高阶运算，并且对时态和时钟算子的支持也略少于前者。其次，L2C项目代码生成工具的目标语言C从一开始就借用了CompCert编译器中Clight的语法和语义定义或］,语义定义中直接釆用了贯穿CompCert编译器几个阶段的底层存储模型；而Veins是从中间语言Obc翻译到Clight，语义定义中的存储模型有明显的跨度。另外一个明显的差异在于编译器结构丄2C编译器在Clight之前的核心中间层超过10层，而Veins编译器在Clight之前的核心中间层仅有2层翻译过程分散为多个阶段，有利于简化各翻译阶段的正确性证明，且具有更好的可扩展性。对于实现工业级的代码生成工具来说，可扩展性是非常重要的；但同时翻译过程也不应过多，否则会加重实现和维护的负担。

4.2翻译确认的方法

1998年，Pnueli第一次提出了翻译确认的设计思想。Pnueii所给示范例子的源语言就是Signal特征的多时钟同步数据流语言，其目标语言是C随后，Pnueii在原有工作的基础上继续实现了对两种同步数据流语言到C的编译器的翻译确认（这两个编译器中包含了大约100个优化规则），证明了翻译确认方法也适用于优化编译器，同时实现了一个翻译确认器CVT（codevalidationtool），其可对编译器每一次执行所产生的代码进行检测，通过模型检验判定与源代码是否等价。这一技术用到编译器可追溯的信息，如状态变量是如何翻译的。近年来，Ngo和Talpin等基于翻译确认的思想，也开展了同步数据流语言Signal到C的编译器验证工作。其主要工作包括：对源代码和目标代码使用统一的语义框架PDS（polynomialdynamicalsystems）建模，给出一种源和目标之间的抽象时钟等价关系，通过对等价关系进行验证来保证编译器时钟语义的一致性，其证明釆用SMT求解器自动完成；同时，也基于一种由一阶逻辑公式定义的时钟模型，开展了保持时钟语义的翻译确认工作,利用同步依赖图（SDGs）对依赖关系的保持性进行确认；使用同步数据流求值图（SDVGs）,对翻译前后的求值语义保持性进行确认并基于这些技术，提出了一种大规模同步数据流语言编译器验证的扩展性良好的设计方案，该方案侧重于对时钟、数据依赖关系的保持性，以及变量的求值等价性等方面的翻译确认。如3.3节所述，翻译确认方法不依赖于翻译的具体过程，相比于对翻译过程进行验证的方法更具有可扩展性。然而,这种方法也有自身的缺陷，比如一般情况下难免存在某种程度的误报（mis-alarm）率。总体来看，上述工作要达到工业级应用的要求，尚有较长的路要走。

4.3 —些相关的基础性研究

与同步数据流语言编译器验证相关的研究有很多，它们都釆用了形式化的方法对同步数据流语言的语义进行定义，这对翻译过程中的形式化验证是很有帮助的。 Kahn将一类异步确定并行程序（现称为Kahn网络）描述为基于流变换（streamtransformation）的递归方程系统，并给出一种完全偏序集（CPO）语义。若将Kahn网络限制到同步程序，则可以认为其是Lustre或其他同步语言的基础。以Kahn网络为出发点，人们也便于对同步数据流范型进行扩展叫。无疑，对于同步数据流语言语义的形式化定义，Kahn网络的CPO语义（指称语义）是重要的参考之一。Paulin-Mo-hring基于Coq开发的KahnNetworksinCoq库是这方面的一项重要工作，同时他们也开发了通用CPO库，其比Kahn为Coq开发的CPO库更加完善。由于是一脉相承，针对Lucid或LucidSynchrone语义的一些研究。包括具体的操作或指称语义定义以及这些工作在Coq环境中的实现，在Lustre语言代码生成工具的研发中都可以借鉴。借鉴上述工作，可以给出同步数据流语言的指称语义，甚至使用Coq的描述语言给出精确的定义。然而，利用此类指称语义来指导编译器的实现以及完成翻译过程的验证有一定难度。在Lustre语言的原始论文中，作者给出了Lustre语言的基本操作语义规则，涵盖了时态算子的语义规则，也包含了时钟演算的规则。在Caspi和Pouzet的研究其中也釆用类似方法来定义同步数据流语言的同步操作语义。这种操作语义的语义规则非常直观且容易理解，然而若是要对应到编译器的实现，还需要在面向实现方面进一步细化和改进。还有许多与同步数据流语言相关的工作也值得关注。Cohen等于2005-2008年间提出了针对同步数据流系统更加宽松的同步和时钟演算模型，如"。Delaval等提出了空间类型系统，以支持分布式系统上同步数据流语言的设计。 Schneider等开展了类Esterel的命令式同步语言的翻译验证工作，解决了Schizophrenia问题。辅助证明工具釆用HOL。Schizophrenia问题必须在因果分析（causalityanal-ysis）之前解决，因同步数据流语言不存在此类问题，故此处不赘述。 L2C课题组基于一个小的Lustre语言子集实现了一个时钟归一化过程的原型，可以将多时钟流转化为单一的时钟流，并形式化验证了变换过程的语义保持性然而，这一方法仅适用于传统的fby算子（2个参数），在当前L2C项目，財中未釆用。

结束语

现阶段，与常规语言一样，同步数据流语言编译器（或代码生成器）形式化验证的方法可以大致分为两大类：一类是针对编译器本身的验证（整体或部分），另一类是翻译确认的方法（验证目标代码和源代码之间的符合性，不验证编译器本身）前者是一种较完美的做法，但工作量大，不容易扩展；后者的扩展性较好，但只适合于解决局部问题。目前已有一些基于辅助定理证明器针对编译器本身进行验证的工作，比如本文提到的Pouzet项目组以及L2C项目组，二者的源语言均基于Lustre语言。关于翻译确认，Pnueli等首先提出这一方案时，所釆用的示例就是基于同步数据流语言Signal;目前进展较好的工作有Ngo和Talpin等所开展的同步数据流语言Signal到C的编译器验证工作。同步数据流语言与串行命令式语言的语义之间有很大差距，因而对同步数据流语言编译器进行验证（特别是针对编译器本身进行验证）的难度和工作量较大，但实际中存在此类需求，比如，花大力气开发出的安全级产品一旦经过认证而投入使用后，允许再度更新的周期相当长。另外，也无需对编译器的所有环节进行验证，比如，目前很少有人特别重视lexer和parser部分的验证工作。还有，为降低难度，在某些扩展和维护工作量过大的翻译阶段，我们可以选择不对编译器本身进行验证，而选择釆用翻译确认的方法作为补充，比如Comp-Cert项目也有个别阶段釆用了翻译确认方案。用这种混合的方法能更好地平衡编译器实现过程中的可信性、难度以及工作量之间的关系。虽然经过形式化验证的编译器离商用尚有很长的路要走，但未来某些标准强制性地要求严格证明是极有可能的，工业界需要有一个逐渐适应的过程。对于代码生成工具的开发，形式化验证的方法无疑代表了一种未来新技术变革的趋势。现实中，可信编译还有另外一层含义，即尽可能保障被编译对象的可信。本文仅关注编译过程的可信，不涉及这方面内容。

致谢

清华大学L2C项目组的师生为本研究提供了许多有价值的素材，在此表示感谢。原文链接：

---

转载于：http://www.digiproto.com/archives/2711