蘭 林，馬 權，侯榮彬，蔣 維，楊 斐

（中國核動力研究設計院 核反應堆系統(tǒng)設計技術重點實驗室，成都 610213）

0 引言

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

1 Lustre語言

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

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

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

2）時態(tài)算子

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

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

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

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

when算子：用于過濾某些周期的值。若E是一個算術表達式，B是一個布爾表達式，它們具有相同的時鐘。那么，表達式E when B 的邏輯時鐘就是B對應的布爾值序列，它的值序列就是當B為true時，E的取值。

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

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

2.1 翻譯驗證

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

圖1 帶有翻譯驗證的代碼生成過程Fig.1 Code generation process with translation validation

2.2 對代碼生成器本身進行證明

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

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

3 Lustre語言的可信代碼生成器

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

圖3 Velus架構圖Fig.3 The architecture of Velus compiler

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

4 結束語

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

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