蘭 林，馬 權(quán)，侯榮彬，蔣 維，楊 斐

（中國(guó)核動(dòng)力研究設(shè)計(jì)院 核反應(yīng)堆系統(tǒng)設(shè)計(jì)技術(shù)重點(diǎn)實(shí)驗(yàn)室，成都 610213）

0 引言

安全攸關(guān)的嵌入式控制領(lǐng)域（如核儀控、軌道交通等領(lǐng)域）常使用基于Lustre語(yǔ)言描述的圖形化邏輯建模工具（如SCADE等）來(lái)開(kāi)發(fā)控制邏輯，然后使用代碼生成器將控制邏輯翻譯為C代碼。這些領(lǐng)域?qū)浖陌踩砸蠓浅?yán)格（如在核儀控領(lǐng)域中必須滿(mǎn)足核電標(biāo)準(zhǔn)IEC60880）。因此，為保證嵌入式軟件的可靠運(yùn)行，必須考慮代碼生成器（編譯器）的可靠性。如果代碼生成器存在潛在的錯(cuò)誤，將會(huì)有產(chǎn)生不安全代碼的風(fēng)險(xiǎn)，由此可能帶來(lái)巨大的災(zāi)難和損失。目前，主要是通過(guò)反復(fù)的測(cè)試和嚴(yán)格的過(guò)程管理等傳統(tǒng)方法來(lái)保證代碼生成器的可靠性。但代碼生成器在開(kāi)發(fā)過(guò)程中引入的錯(cuò)誤通常是很難發(fā)現(xiàn)的，采用傳統(tǒng)的方法無(wú)法杜絕代碼生成器的誤編譯。經(jīng)過(guò)傳統(tǒng)方法開(kāi)發(fā)的編譯器如GCC、LLVM，通過(guò)Csmith工具發(fā)現(xiàn)了多個(gè)錯(cuò)誤，即使工控領(lǐng)域廣泛使用的SCADE Suite也不能證明它不會(huì)出現(xiàn)誤編譯。而通過(guò)形式化方法開(kāi)發(fā)的代碼生成器，能夠在開(kāi)發(fā)的同時(shí)，對(duì)其翻譯前后語(yǔ)言語(yǔ)義一致性進(jìn)行邏輯推理證明，能夠最大限度地消除誤編譯。本文將在闡述可信代碼生成器形式化開(kāi)發(fā)方法的基礎(chǔ)上，介紹同步數(shù)據(jù)流語(yǔ)言Lustre的特征及相關(guān)可信代碼生成器的形式化研究進(jìn)展。

1 Lustre語(yǔ)言

Lustre作為一種同步數(shù)據(jù)流語(yǔ)言，最早出現(xiàn)在P.Caspi的論文中[1]，多用于嵌入式控制系統(tǒng)和信號(hào)處理系統(tǒng)。它在工控領(lǐng)域主要用于描述實(shí)時(shí)控制邏輯，核儀控、航天航空、軌道交通等安全攸關(guān)領(lǐng)域廣泛使用的SCADE Suite就是基于Lustre語(yǔ)言描述實(shí)現(xiàn)的。Lustre語(yǔ)言具有數(shù)據(jù)流特征和確定性語(yǔ)義[1]，適用于反應(yīng)式控制系統(tǒng)編程、模塊化的代碼生成[2]以及程序的形式化驗(yàn)證[3-5]。Lustre程序是由一系列的node或 function聲明、常量聲明和數(shù)據(jù)類(lèi)型聲明組成，node或function是用于處理輸入流并輸出的函數(shù)，node體是由一系列等式組成。與串行命令式語(yǔ)言（如C語(yǔ)言）相比，具有許多獨(dú)有的特征[6]，如下所示：

1）數(shù)據(jù)流和時(shí)鐘

Lustre語(yǔ)言的變量、等式都是一個(gè)數(shù)據(jù)流（Stream）。一個(gè)數(shù)據(jù)流由相同類(lèi)型的數(shù)據(jù)值序列和邏輯時(shí)鐘兩部分組成，默認(rèn)情況下邏輯時(shí)鐘都為true，叫作基本時(shí)鐘。Lustre程序具有周期性循環(huán)執(zhí)行的特點(diǎn)，對(duì)應(yīng)著無(wú)窮多個(gè)周期，循環(huán)作用在數(shù)據(jù)流上。一個(gè)有基本時(shí)鐘的數(shù)據(jù)流，在程序執(zhí)行的第n個(gè)周期，取值為數(shù)據(jù)流的第n個(gè)值。另外，可以利用布爾值自定義一個(gè)時(shí)鐘，使用時(shí)態(tài)算子對(duì)數(shù)據(jù)流進(jìn)行過(guò)濾等處理。

2）時(shí)態(tài)算子

pre算子：用于訪問(wèn)前一周期的值。若表達(dá)式E的無(wú)窮多個(gè)周期對(duì)應(yīng)的值序列為（e1,e2,...,en,...）,則表達(dá)式pre(E)的邏輯時(shí)鐘與E相同，且當(dāng)周期n=1時(shí)，它的值為nil（nil表示一個(gè)未定義的值）；n>1時(shí)，它各周期的值為表達(dá)式E前一個(gè)周期的值。即最后結(jié)果為pre(E)=（nil,e1,e2,...,en-1,...）。

->算子：用于初始化，可以和pre算子結(jié)合使用，以消除pre算子使用過(guò)程中第一個(gè)周期可能出現(xiàn)的nil。若表達(dá)式E和F的值序列分別為（e1,e2,...,en,...）和（f1,f2,...,fn,...），且它們的邏輯時(shí)鐘相同，那么，E->F 的時(shí)鐘也和E、F的時(shí)鐘相同，且當(dāng)n=1時(shí)，其值為E第一個(gè)周期的值；當(dāng)n>1時(shí)，其各周期的值分別為F對(duì)應(yīng)的各周期的值。即最后結(jié)果為E->F =（e1, f2,f3,...,fn,...）。

二元fby算子：相當(dāng)于pre算子和->算子的結(jié)合體。若表達(dá)式E和F的值序列分別為（e1,e2,...,en,...）和（f1,f2,...,fn,...），且它們的邏輯時(shí)鐘都相同，那么E fby F的時(shí)鐘也和E、F的時(shí)鐘相同，對(duì)應(yīng)的值序列為（e1, f1,f2,...,fn,...）。

三元fby算子：若表達(dá)式E和F的值序列分別為（e1,e2,...,en,...）和（f1,f2,...,fn,...），且它們的邏輯時(shí)鐘都相同，那么fby(E,n,F)的時(shí)鐘也和E、F的時(shí)鐘相同，對(duì)應(yīng)的值序列（e1,e2,...,en,f1,f2,...,fn,...）

when算子：用于過(guò)濾某些周期的值。若E是一個(gè)算術(shù)表達(dá)式，B是一個(gè)布爾表達(dá)式，它們具有相同的時(shí)鐘。那么，表達(dá)式E when B 的邏輯時(shí)鐘就是B對(duì)應(yīng)的布爾值序列，它的值序列就是當(dāng)B為true時(shí)，E的取值。

2 可信代碼生成器形式化開(kāi)發(fā)方法

廣義的講，形式化方法是使用數(shù)方法來(lái)解決軟件工程領(lǐng)域中遇到的問(wèn)題，主要內(nèi)容是建立數(shù)學(xué)模型以及對(duì)其進(jìn)行充分、合理的分析；狹義的講，形式化方法是使用形式化語(yǔ)言對(duì)規(guī)則進(jìn)行描述，然后進(jìn)行邏輯推理和證明的方法。經(jīng)過(guò)形式化開(kāi)發(fā)的可信代碼生成器，其最大的特點(diǎn)是生成的目標(biāo)代碼的行為是嚴(yán)格符合源語(yǔ)言語(yǔ)義的，即源程序與目標(biāo)代碼之間語(yǔ)義具有一致性，不會(huì)產(chǎn)生有歧義的代碼，從而保證了代碼生成的可靠性。用于開(kāi)發(fā)可信代碼生成器的形式化方法主要有對(duì)代碼生成器本身的證明和翻譯驗(yàn)證，接下來(lái)分別對(duì)這兩種形式化開(kāi)發(fā)方法進(jìn)行介紹。

2.1 翻譯驗(yàn)證

在可信代碼生成器形式化驗(yàn)證領(lǐng)域，John Mccarthy等人已經(jīng)做了大量工作[7-10]，但仍然無(wú)法自動(dòng)證明給定的優(yōu)化編譯器的目標(biāo)語(yǔ)言和源語(yǔ)言語(yǔ)義的一致性。如果不能證明代碼生成器本身的正確性，也許可以檢查每個(gè)編譯過(guò)程的正確性。這啟發(fā)了翻譯驗(yàn)證技術(shù)，翻譯驗(yàn)證的概念最早由Pnueli等人于90年代提出[11-13]，作為一種形式化驗(yàn)證代碼生成器正確性的技術(shù)，用于避免代碼在轉(zhuǎn)換過(guò)程中引入語(yǔ)義的歧義。翻譯驗(yàn)證屬于等價(jià)性驗(yàn)證的一種，它通過(guò)驗(yàn)證源程序和目標(biāo)代碼的語(yǔ)義等價(jià)性來(lái)證明代碼生成器的正確性[14,15]。從而避免了對(duì)代碼生成器本身的證明，只需要對(duì)驗(yàn)證器進(jìn)行定理證明，具有較好的可重用性。帶有翻譯驗(yàn)證的代碼生成過(guò)程如圖1所示，與普通代碼生成器的編譯過(guò)程是一樣的，只是從源程序到目標(biāo)代碼翻譯完成后，沒(méi)有立刻輸出目標(biāo)代碼，而是增加了一個(gè)形式化開(kāi)發(fā)的驗(yàn)證器，用于驗(yàn)證源程序和目標(biāo)代碼的語(yǔ)義是否具有一致性。把驗(yàn)證器看做一個(gè)函數(shù)Validate(S,C)，代碼生成過(guò)程看作函數(shù)Comp，驗(yàn)證語(yǔ)義等價(jià)性S≈C。如果由源程序S翻譯生成了目標(biāo)代碼C，即Comp(S)=OK(C)，并且通過(guò)了驗(yàn)證器的驗(yàn)證，即Validate(S,C)=true。那么，生成的目標(biāo)代碼C就被認(rèn)為是可信的。因此驗(yàn)證器是翻譯驗(yàn)證方法的核心，目標(biāo)代碼通過(guò)了驗(yàn)證器的驗(yàn)證后，才輸出目標(biāo)代碼，否則編譯報(bào)錯(cuò)。隨著翻譯驗(yàn)證技術(shù)的逐漸成熟，在商用代碼生成器中也得到了應(yīng)用，Michael等人[16]為商用RTW代碼生成器開(kāi)發(fā)了一個(gè)翻譯驗(yàn)證工具TVS(RTW[20]代碼生成器實(shí)現(xiàn)了從Simulink模型轉(zhuǎn)換到C代碼過(guò)程)。文獻(xiàn)[17]中，基于翻譯驗(yàn)證技術(shù)為GNU C優(yōu)化編譯器實(shí)現(xiàn)了一個(gè)驗(yàn)證器。

圖1 帶有翻譯驗(yàn)證的代碼生成過(guò)程Fig.1 Code generation process with translation validation

2.2 對(duì)代碼生成器本身進(jìn)行證明

另一種形式化開(kāi)發(fā)可信代碼生成器的方法是對(duì)代碼生成器本身進(jìn)行證明。這是一種將源語(yǔ)言的語(yǔ)法、語(yǔ)義模型及其滿(mǎn)足規(guī)范的性質(zhì)抽象為邏輯公式，然后使用邏輯推理技術(shù)來(lái)證明其語(yǔ)義一致性的技術(shù)，是最嚴(yán)格的開(kāi)發(fā)方式。這種方法和數(shù)理邏輯相聯(lián)系，常使用高階邏輯系統(tǒng)進(jìn)行形式化描述，可通過(guò)Coq[18]、Isabel/HOL等輔助定理證明工具進(jìn)行證明。該形式化開(kāi)發(fā)方法貫穿整個(gè)可信代碼生成器的開(kāi)發(fā)過(guò)程，為了降低形式化驗(yàn)證的難度，整個(gè)開(kāi)發(fā)過(guò)程一般會(huì)劃分為包含不同中間語(yǔ)言的多個(gè)翻譯階段，逐步翻譯到目標(biāo)代碼。第一個(gè)形式化證明在1967年[8]手工完成的，用于將算術(shù)表達(dá)式的編譯成堆棧機(jī)器碼，并在1972年[19]對(duì)其進(jìn)行了機(jī)械證明。Xavier[20]等人使用定理輔助證明工具Coq，使用定理證明方式開(kāi)發(fā)的CompCert編譯器，實(shí)現(xiàn)了從結(jié)構(gòu)化的命令式語(yǔ)言到匯編代碼的生成。CompCert由兩部分組成，編譯器前端：把C語(yǔ)言子集Clight[21]轉(zhuǎn)換成一種低級(jí)的、結(jié)構(gòu)化的中間語(yǔ)言Cminor；編譯器后端[22,23]：把中間語(yǔ)言Cminor生成為匯編代碼。定理證明方法開(kāi)發(fā)可信代碼生成器的基本流程如圖2所示，Language1和Language 2分別代表可信代碼生成器翻譯過(guò)程中的兩個(gè)中間語(yǔ)言，首先分別定義好源語(yǔ)言和目標(biāo)語(yǔ)言的形式化語(yǔ)法、語(yǔ)義，然后證明翻譯前后對(duì)應(yīng)Language 1和Language 2的語(yǔ)義是否具有一致性，如果一致，則說(shuō)明這個(gè)過(guò)程是可信的，利用Coq的抽取功能（Extraction）把翻譯算法抽取成Ocaml代碼。否則，迭代修改其形式化語(yǔ)法、語(yǔ)義的形式化定義，直到證明得到翻譯前后語(yǔ)義具有一致性，再抽取翻譯算法。把各翻譯階段的可信翻譯算法抽取出來(lái)與代碼生成器前端結(jié)合起來(lái)，最后就得到了一個(gè)經(jīng)過(guò)證明的可信代碼生成器。

圖2 對(duì)代碼生成器本身進(jìn)行證明的開(kāi)發(fā)流程圖Fig.2 The process of theorem proving method to develop trusted code generator

3 Lustre語(yǔ)言的可信代碼生成器

學(xué)術(shù)界做了許多關(guān)于Lustre語(yǔ)言特性的形式化研究，Jakubiec L[24]等人在Coq中使用歸納類(lèi)型定義了Lustre語(yǔ)言的一個(gè)子集；G. Hamon[25]等人研究了同步數(shù)據(jù)流語(yǔ)言Lucid的高階特性，并完成了Lucid時(shí)鐘演算；E. Gimenez 等人在開(kāi)發(fā)Scade3代碼生成器過(guò)程中，完成了Lustre語(yǔ)言的語(yǔ)義和時(shí)鐘的定義[26]?；谇叭藢?duì)Lustre語(yǔ)法語(yǔ)義及性質(zhì)的研究基礎(chǔ)上，法國(guó)INRIA的Poute團(tuán)隊(duì)和清華大學(xué)計(jì)算機(jī)系的L2C團(tuán)隊(duì)利用對(duì)代碼生成器本身進(jìn)行證明的方式，各開(kāi)發(fā)了一款用于學(xué)術(shù)研究的Lustre到Clight的代碼生成器。Poute團(tuán)隊(duì)于2006年啟動(dòng)了Lustre語(yǔ)言代碼生成器的形式化驗(yàn)證的研究工作，使用定理證明技術(shù)，在Coq中開(kāi)發(fā)得到了Lustre到Clight的可信代碼生成器Velus。Velus的架構(gòu)如圖3所示，主要由兩部分內(nèi)容構(gòu)成，包括對(duì)源程序Lustre的預(yù)處理和代碼生成及優(yōu)化。該團(tuán)隊(duì)成員BERTAILS A等人[27]完成了Lustre程序的預(yù)處理過(guò)程，包括把源程序解析成沒(méi)有注入時(shí)鐘和類(lèi)型的抽象語(yǔ)法樹(shù)（parsing）；對(duì)程序注入時(shí)鐘和類(lèi)型（elaboration）以對(duì)程序進(jìn)行靜態(tài)檢查；簡(jiǎn)化程序中的復(fù)雜等式（normalization）；對(duì)程序進(jìn)行因果分析和拓?fù)渑判颍共⑿谐绦虼谢╯cheduling）等工作。該團(tuán)隊(duì)成員Bourke等人[28]，完成了中間代碼生成及優(yōu)化和目標(biāo)代碼生成，以及語(yǔ)義一致性的證明。包括從源程序到中間語(yǔ)言O(shè)bc的翻譯（translation），該階段消去了Lustre程序中的fby等時(shí)態(tài)算子；對(duì)Obc代碼的優(yōu)化（Fusion optimization）；從Obc到目標(biāo)程序Clight的代碼生成（generation）等工作。由圖3中虛線連接的部分表示，經(jīng)Velus生成的Clight代碼可直接在CompCert中編譯，生成能在嵌入式設(shè)備中運(yùn)行的可執(zhí)行代碼。為了簡(jiǎn)化證明過(guò)程，Vleus定義了一個(gè)中間語(yǔ)言O(shè)bc，這是在Lustre語(yǔ)言可信代碼生成器的開(kāi)發(fā)過(guò)程中常用的手段，一種中間語(yǔ)言對(duì)應(yīng)了一個(gè)翻譯階段，一個(gè)翻譯階段只完成部分Lustre算子的消去工作。

圖3 Velus架構(gòu)圖Fig.3 The architecture of Velus compiler

清華大學(xué)L2C項(xiàng)目組于2010年開(kāi)始著手研究Lustre到Clight的可信代碼生成器(簡(jiǎn)稱(chēng)L2C)，經(jīng)過(guò)形式化驗(yàn)證的L2C單時(shí)鐘版本[29]已經(jīng)實(shí)現(xiàn)了開(kāi)源，在此基礎(chǔ)上又為國(guó)內(nèi)某核電企業(yè)開(kāi)發(fā)了多時(shí)鐘版本[30]。Velus和L2C都是參考了CompCert成功的技術(shù)路線，在Coq中利用定理證明技術(shù)來(lái)進(jìn)行形式化的開(kāi)發(fā)。它們的目標(biāo)語(yǔ)言Clight的形式化定義也都是借鑒CompCert的定義。因此，L2C（開(kāi)源版本）的架構(gòu)跟Velus非常相似，這里不再贅述。但它們還是存在許多的不同，主要體現(xiàn)在支持的Lustre語(yǔ)言特性上。為了結(jié)合實(shí)際工業(yè)控制領(lǐng)域的需要， L2C、SCADE等工具在前述的Lustre語(yǔ)言特性的基礎(chǔ)上，為了滿(mǎn)足工業(yè)控制的需要，又增加了一些如用于處理數(shù)組的高階算子等特性。如表1所示，為Velus、L2C（開(kāi)源版本）和SCADE特性上的比較。

4 結(jié)束語(yǔ)

Lustre的可信代碼生成器的形式化開(kāi)發(fā)方法包括翻譯驗(yàn)證和對(duì)代碼生成器本身進(jìn)行證明，翻譯驗(yàn)證開(kāi)發(fā)的核心在驗(yàn)證器，開(kāi)發(fā)方式較簡(jiǎn)單、重用性好，多用于代碼生成器的優(yōu)化；定理證明是對(duì)代碼生成器本身進(jìn)行證明，是最嚴(yán)格的形式化開(kāi)發(fā)方式，經(jīng)過(guò)此方式開(kāi)發(fā)的代碼生成器能夠達(dá)到人們所期望的最高的可信程度。未來(lái)在Lustre可信代碼生成器的形式化開(kāi)發(fā)中，可考慮把兩種開(kāi)發(fā)方式結(jié)合起來(lái)，把翻譯驗(yàn)證作為對(duì)代碼生成器本身進(jìn)行證明的一種補(bǔ)充，如在CompCert編譯器開(kāi)發(fā)中，就混合使用了這兩種方法，可以很好地平衡可靠性和工作量的問(wèn)題。通過(guò)形式化方法開(kāi)發(fā)的Velus和L2C代碼生成器還未真正實(shí)現(xiàn)商用，主要用于學(xué)術(shù)研究。結(jié)合現(xiàn)有的學(xué)術(shù)成果和工業(yè)控制的需求，完善適用于工業(yè)控制的算子，優(yōu)化Lustre到C的可信代碼生成器，成為L(zhǎng)ustre可信代碼生成器真正用于安全攸關(guān)領(lǐng)域的關(guān)鍵一步。

表1 Velus、L2C和SCADE的特性比較Table 1 The comparison of Velus, L2C and SCADE