賈尚坤,賀 飛

(清華大學(xué) 軟件學(xué)院, 北京 100084)(*通信作者電子郵箱 hefei@tsinghua.edu.cn)

0 引言

為了保障軟件的正確性與魯棒性,傳統(tǒng)的方法是通過(guò)一系列功能與性能相關(guān)的測(cè)試發(fā)現(xiàn)軟件的問(wèn)題與缺陷。然而,測(cè)試方法只能在整個(gè)系統(tǒng)或相關(guān)功能實(shí)現(xiàn)后進(jìn)行,無(wú)法在軟件的需求或設(shè)計(jì)階段預(yù)見(jiàn)系統(tǒng)潛在的問(wèn)題。另外,測(cè)試方法不可能包含所有情況的測(cè)試用例,因此無(wú)法證明系統(tǒng)不存在缺陷,也無(wú)法證明它滿足特定的屬性。而驗(yàn)證方法則恰好可以解決上述問(wèn)題。軟件的形式化驗(yàn)證[1]指的是在軟件系統(tǒng)的抽象數(shù)學(xué)模型上應(yīng)用形式化的證明,驗(yàn)證系統(tǒng)滿足或違反相應(yīng)的規(guī)約和屬性,以確保軟件的正確性。用于建模系統(tǒng)的數(shù)學(xué)對(duì)象包括有限狀態(tài)機(jī)、Petri網(wǎng)、時(shí)間自動(dòng)機(jī)等,而形式化的證明方法則在數(shù)理邏輯、自動(dòng)機(jī)、圖論等數(shù)學(xué)理論基礎(chǔ)之上對(duì)系統(tǒng)進(jìn)行分析與驗(yàn)證。形式化驗(yàn)證主要包含定理證明和模型檢測(cè)兩種途徑,其中后者由于輕量級(jí)和完全自動(dòng)化在工業(yè)界得到了廣泛應(yīng)用。

多版本迭代是當(dāng)前軟件開(kāi)發(fā)的普遍狀況。為了節(jié)約軟件開(kāi)發(fā)的資金、人力、時(shí)間等投入,軟件公司需要用盡可能少的版本迭代為軟件增加更多的新特性。然而,軟件在對(duì)自身功能進(jìn)行擴(kuò)展的同時(shí),可能會(huì)與已有功能產(chǎn)生沖突而引發(fā)錯(cuò)誤,這一現(xiàn)象被稱為“回歸”[2]。為了避免回歸,文獻(xiàn)[3]中首先提出了回歸測(cè)試的概念,即用一組覆蓋面盡可能大的回歸測(cè)試用例對(duì)軟件的新版本進(jìn)行檢測(cè),報(bào)告任何可能出現(xiàn)的新漏洞。但由于回歸測(cè)試不可能包含所有的測(cè)試用例,因此無(wú)法保證所有的新漏洞在軟件發(fā)布前都能被提前發(fā)現(xiàn)而得到解決。因此,為了確保軟件的安全性與可靠性,需要在軟件的研發(fā)進(jìn)程中引入程序驗(yàn)證方法?？紤]到鄰近版本之間往往有較多的相似性,如果將這些版本視為不同軟件分別進(jìn)行驗(yàn)證,將會(huì)浪費(fèi)掉大量的共享信息,從而影響驗(yàn)證效率。為了利用鄰近版本之間的共享信息,學(xué)者又提出了回歸模型檢測(cè)[4]與回歸驗(yàn)證[5]的概念。最初回歸驗(yàn)證指的是證明相關(guān)聯(lián)程序的等價(jià)性,即:程序P1與P2的任意可終止的執(zhí)行若具有相同的輸入,則運(yùn)行結(jié)束后將得到相同的返回值。后來(lái)人們用回歸驗(yàn)證表示將形式化驗(yàn)證技術(shù)應(yīng)用到連續(xù)檢測(cè)的開(kāi)發(fā)版本中,利用鄰近版本之間的共享信息驗(yàn)證程序?qū)傩浴?/p>

而對(duì)于證據(jù)(witness),最開(kāi)始更多被用來(lái)描述驗(yàn)證工具在系統(tǒng)違反驗(yàn)證屬性時(shí)生成的錯(cuò)誤路徑,它們?cè)趶?fù)現(xiàn)系統(tǒng)的錯(cuò)誤中扮演了“見(jiàn)證人”的角色。后來(lái)證據(jù)的含義得到擴(kuò)展,指的是軟件驗(yàn)證工具在驗(yàn)證完成后生成的一個(gè)驗(yàn)證結(jié)果輔助文件,用來(lái)對(duì)驗(yàn)證程序進(jìn)行再檢驗(yàn),進(jìn)而確定程序是否如驗(yàn)證結(jié)果所說(shuō)滿足或違反其驗(yàn)證屬性[6],如圖1所示。證據(jù)需要有統(tǒng)一的格式,這樣不僅方便不同驗(yàn)證工具的交互,也有助于證據(jù)文件的可讀性與可視化。目前在國(guó)際軟件驗(yàn)證大賽(Competition on Software Verification, SV-COMP)上采用的證據(jù)文件格式為GraphML(一種可擴(kuò)展標(biāo)記語(yǔ)言),其中定義了一個(gè)非確定有限自動(dòng)機(jī),即證據(jù)自動(dòng)機(jī)。自動(dòng)機(jī)的節(jié)點(diǎn)表示一個(gè)程序位置(對(duì)應(yīng)程序計(jì)數(shù)器的一個(gè)值),自動(dòng)機(jī)的邊表示控制流從邊的起點(diǎn)到終點(diǎn)時(shí)程序執(zhí)行的操作(對(duì)應(yīng)一條程序語(yǔ)句),整個(gè)證據(jù)自動(dòng)機(jī)刻畫(huà)了程序的大致結(jié)構(gòu)。圖2給出了一個(gè)證據(jù)自動(dòng)機(jī)的示例,自動(dòng)機(jī)每個(gè)節(jié)點(diǎn)上的編號(hào)對(duì)應(yīng)一個(gè)程序位置,而每條邊除了對(duì)應(yīng)的程序語(yǔ)句之外,還包含起始行號(hào)、偏移量等相關(guān)的定位信息。

圖1 證據(jù)文件的生成與檢驗(yàn)Fig. 1 Generation and validation of witness files

圖2 證據(jù)自動(dòng)機(jī)示例Fig. 2 Example of witness automata

根據(jù)驗(yàn)證結(jié)果的不同(不考慮超時(shí)等未知驗(yàn)證結(jié)果),證據(jù)分為正確證據(jù)(correctness witness)[7]與違反證據(jù)(violation witnesss)[8]兩類,分別表示程序滿足或違反其驗(yàn)證屬性。二者的內(nèi)涵也有所不同,正確證據(jù)包含了程序驗(yàn)證得到的循環(huán)不變式,而違反證據(jù)記錄了程序驗(yàn)證過(guò)程中到達(dá)錯(cuò)誤狀態(tài)的反例路徑信息。由于回歸驗(yàn)證的關(guān)鍵在于鄰近版本之間的共享信息,因此基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證的主要目標(biāo)是提取并重用證據(jù)文件中的共享信息。對(duì)于鄰近版本的程序而言,若均滿足驗(yàn)證屬性,則相同或相近程序位置處成立的不變式很可能相差不大;而若均違反驗(yàn)證屬性,前一版本的反例路徑在后一版本中未必有效,即使有效也未必導(dǎo)向錯(cuò)誤狀態(tài)。因此,基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證主要指的是提取并重用之前版本正確證據(jù)中的循環(huán)不變式,對(duì)多版本程序進(jìn)行回歸驗(yàn)證。

歷屆國(guó)際軟件驗(yàn)證大賽都要求所有參賽工具提供能夠復(fù)現(xiàn)驗(yàn)證結(jié)果的證據(jù)文件,從SV-COMP 2015開(kāi)始規(guī)定了反例文件的格式并要求為屬性違反提供違反證據(jù)[9],從SV-COMP 2017開(kāi)始規(guī)定了正確文件的格式并要求為屬性滿足提供正確證據(jù)[10]。但大多數(shù)能生成證據(jù)文件的驗(yàn)證工具并不能利用證據(jù)文件中的信息,截至SV-COMP 2017只有可配置程序分析檢測(cè)工具(Configurable Program Analysis checker, CPAchecker)和終極自動(dòng)機(jī)驗(yàn)證工具(Ultimate Automizer, UAutomizer)被選為證據(jù)文件的檢驗(yàn)工具[10]。由于UAutomizer對(duì)證據(jù)文件中循環(huán)不變式的利用效率偏低[7],因此本文在CPAchecker源代碼的基礎(chǔ)上實(shí)現(xiàn)回歸驗(yàn)證功能。CPAchecker是一個(gè)應(yīng)用可配置程序分析(configurable program analysis)框架[11]整合各種軟件分析與驗(yàn)證技術(shù)的開(kāi)源工具[12],可以通過(guò)命令行或Eclipse插件運(yùn)行。

1 證據(jù)預(yù)處理

對(duì)于多版本程序而言,即便鄰近版本的程序結(jié)構(gòu)也會(huì)存在一定的差異,因此上一個(gè)版本的證據(jù)文件并不能直接應(yīng)用到下一個(gè)版本的驗(yàn)證中。為了利用之前版本證據(jù)自動(dòng)機(jī)中的不變式信息,需要對(duì)證據(jù)文件進(jìn)行相應(yīng)的預(yù)處理。預(yù)處理大致可以分為兩個(gè)部分:影響域分析與證據(jù)文件生成。整個(gè)預(yù)處理過(guò)程如圖3所示。證據(jù)預(yù)處理的相關(guān)實(shí)現(xiàn)已被整合到CPAchecker源碼中。

圖3 證據(jù)預(yù)處理Fig. 3 Witness preprocessing

1.1 影響域分析

影響域分析的目的在于確定版本變動(dòng)對(duì)原證據(jù)文件中不變式的影響。不受影響的不變式可以直接重用,而受影響的不變式在新版程序中可能仍然成立,需要進(jìn)一步檢驗(yàn)。影響域分析分為三步:比較新舊程序、生成混合程序、得到影響結(jié)果。

比較新舊程序主要用到了Linux系統(tǒng)中的diff命令:

diff -b -B -H -n old.c new.c

其中:-b用于忽視空格字符;-B用于忽視空白行;-H用于提高大文件比較的速度;-n用于修改輸出格式。通過(guò)調(diào)用diff命令比較新舊版本程序的文本差異,并將比較結(jié)果重定向到差異文件diff.txt中。diff.txt包含了新版程序相對(duì)于舊版程序增加和刪除的語(yǔ)句信息,例如對(duì)于diff.txt中的以下內(nèi)容:

a6 1

int c=a+b;

d12 2

其中:a和d分別表示增加和刪除。a和d后面的第一個(gè)數(shù)字表示舊版程序的行號(hào);第二個(gè)數(shù)字表示增加或刪除的代碼行數(shù),若為增加還會(huì)在后面附加具體的語(yǔ)句。

生成混合程序通過(guò)將原證據(jù)文件old-witness與差異文件diff.txt的信息綜合到舊版程序old.c中,得到用于影響域分析的混合程序mix.c。old-witness的信息主要指證據(jù)自動(dòng)機(jī)節(jié)點(diǎn)上的循環(huán)不變式。由圖2可知,自動(dòng)機(jī)節(jié)點(diǎn)可以通過(guò)其入邊與出邊在程序中定位,因而可以將節(jié)點(diǎn)上的不變式作為布爾表達(dá)式插入到相應(yīng)的程序位置。之后將diff.txt中的新增語(yǔ)句插入混合程序,并且在新增語(yǔ)句和刪除語(yǔ)句前加上影響標(biāo)注:

/*@ impact pragma stmt; */

由混合程序mix.c調(diào)用Frama-C的影響域分析插件即可得到版本變動(dòng)語(yǔ)句對(duì)原證據(jù)文件中不變式的影響結(jié)果。Frama-C是一個(gè)面向大規(guī)模C程序驗(yàn)證的源碼分析平臺(tái)[13],通過(guò)整合相關(guān)插件實(shí)現(xiàn)各種分析與驗(yàn)證功能。通過(guò)圖形界面或命令行調(diào)用Frama-C的影響域分析插件,可以分析帶有影響標(biāo)注的語(yǔ)句對(duì)其他語(yǔ)句的影響。調(diào)用該插件的具體命令如下:

frama-c -impact-pragma -impact-print

-impact-log r:impact.txt -val-initialized-locals mix.c

-impact-pragma后接函數(shù)名表示在相應(yīng)的函數(shù)中檢測(cè)影響標(biāo)注。由于影響標(biāo)注在所有函數(shù)中都可能出現(xiàn),因此需要調(diào)用CPAchecker的相關(guān)接口getAllFunctionNames獲取程序所有的函數(shù)名。又因?yàn)镃PAchecker在生成證據(jù)自動(dòng)機(jī)時(shí)會(huì)對(duì)程序進(jìn)行預(yù)處理,從混合程序看來(lái)自動(dòng)機(jī)節(jié)點(diǎn)上不變式中的變量在相應(yīng)的程序位置處可能尚未初始化,如果直接對(duì)這樣的程序進(jìn)行影響域分析將無(wú)法得到正確的影響結(jié)果,因此需要用-val-initialized-locals選項(xiàng)對(duì)所有的局部變量進(jìn)行初始化。影響域分析的結(jié)果保存在文件impact.txt中。

1.2 證據(jù)文件生成

得到影響域分析結(jié)果之后,未受影響的不變式可以直接重用。而由于受影響的不變式在新版程序中可能仍然成立,需要將其寫(xiě)入用于進(jìn)一步檢驗(yàn)的新證據(jù)文件new-witness。生成new-witness的目的是如果之后的版本迭代不改變程序結(jié)構(gòu),可以直接將new-witness作為驗(yàn)證后面版本的輸入,從而省去證據(jù)預(yù)處理過(guò)程。

生成new-witness之前,需要從原證據(jù)文件old-witness中提取受影響不變式的相關(guān)信息,包括不變式的內(nèi)容、所屬的節(jié)點(diǎn)編號(hào)、在程序中的作用域以及與所屬節(jié)點(diǎn)相關(guān)聯(lián)的邊。邊上的代碼行號(hào)關(guān)系到不變式在新證據(jù)自動(dòng)機(jī)中的定位,而由于版本變動(dòng),舊版程序的代碼行號(hào)在新版程序中也會(huì)相應(yīng)變化。因此,需要對(duì)行號(hào)進(jìn)行相應(yīng)的轉(zhuǎn)換,轉(zhuǎn)換方法如算法1所示。

算法1 新舊代碼行號(hào)轉(zhuǎn)換。

輸入 舊版程序代碼行數(shù)len,新舊版本差異文件diff.txt。

輸出 整型數(shù)組oldToNew[],數(shù)組下標(biāo)和相應(yīng)的元素值分別表示舊版程序及其在新版程序中對(duì)應(yīng)的代碼行號(hào)(均從0開(kāi)始)。

1)

新建一個(gè)大小為len的整型數(shù)組oldToNew[],并將其每一項(xiàng)初始化為0

2)

對(duì)于diff.txt中的每一行diffline:

3)

解析diffline,得到變動(dòng)類型type、行號(hào)number與行數(shù)count

4)

if (type==′d′)

5)

oldToNew[number-1] -=count

6)

else

7)

oldToNew[number]+=count

8)

diff.txt繼續(xù)向后讀取count行

9)

intlastIndex=0

10)

for (inti=1;i

11)

oldToNew[i]+=oldToNew[i-1]+1

12)

for (inti=len-1;i>=0; --i)

13)

if (oldToNew[i]>=0)

14)

lastIndex=oldToNew[i]

15)

else

16)

oldToNew[i]=lastIndex

預(yù)處理過(guò)程改寫(xiě)了CPAchecker的接口writeProofWitness,在得到不變式相關(guān)信息之后,可以由該接口將其寫(xiě)入新證據(jù)文件。對(duì)于原證據(jù)文件中一條與不變式所屬節(jié)點(diǎn)相關(guān)聯(lián)的邊,找出它經(jīng)過(guò)行號(hào)轉(zhuǎn)換后在新證據(jù)自動(dòng)機(jī)中對(duì)應(yīng)的邊,若二者的控制條件一致,則在新證據(jù)自動(dòng)機(jī)中的對(duì)應(yīng)節(jié)點(diǎn)上附加相應(yīng)的不變式信息。然后通過(guò)合并冗余節(jié)點(diǎn)及其不變式,得到最終的新證據(jù)自動(dòng)機(jī),再調(diào)用CPAchecker中GraphML構(gòu)造器GraphMlBuilder的appendTo方法生成新證據(jù)文件new-witness。new-witness刻畫(huà)了新版程序的大致結(jié)構(gòu),因而可以應(yīng)用到新版程序的驗(yàn)證中。

2 回歸驗(yàn)證過(guò)程

對(duì)新版程序進(jìn)行回歸驗(yàn)證的關(guān)鍵在于提取并重用原證據(jù)文件中的不變式信息。不受版本變動(dòng)影響的不變式可以直接重用,而受影響的不變式則需要在新證據(jù)文件中檢驗(yàn)通過(guò)后才能重用。檢驗(yàn)新證據(jù)文件及驗(yàn)證新版程序的回歸驗(yàn)證算法基于CPAchecker中用輔助不變式增強(qiáng)的k-歸納(k-induction)算法。

2.1 k-induction及其增強(qiáng)

k-induction最初作為有限狀態(tài)遷移系統(tǒng)基于可滿足性判定的一種驗(yàn)證技術(shù),被用于硬件設(shè)計(jì)與轉(zhuǎn)移關(guān)系的驗(yàn)證[14]。后來(lái)k-induction技術(shù)逐漸應(yīng)用到軟件分析與驗(yàn)證領(lǐng)域,如直接內(nèi)存訪問(wèn)競(jìng)爭(zhēng)分析[15]、同步程序分析[16]與嵌入式軟件驗(yàn)證[17]等。

對(duì)于一個(gè)表示程序的狀態(tài)遷移系統(tǒng),s和s′為其中的兩個(gè)狀態(tài)變量,I(s)表示s為初始狀態(tài),T(s,s′)表示存在s到s′的狀態(tài)轉(zhuǎn)移,P(s)表示程序的安全屬性P在s上成立。給定一個(gè)任意的正整數(shù)k,分兩步說(shuō)明k-induction的驗(yàn)證過(guò)程。

為了用k-induction證明程序,首先需要驗(yàn)證P在從初始狀態(tài)s1出發(fā)k步內(nèi)可達(dá)的所有狀態(tài)s1,s2, …,sk上均成立,也就是式(1)不可滿足:

(1)

接下來(lái),還需要驗(yàn)證只要P在任意k個(gè)連續(xù)狀態(tài)sn,sn+1, …,sn+k-1上成立,P在第k+1個(gè)狀態(tài)sn+k上就一定成立,也就是式(2)不可滿足:

(2)

由上述兩步即可驗(yàn)證程序的正確性。若式(1)可以滿足,則程序違反其驗(yàn)證屬性;若式(2)可以滿足,則在當(dāng)前k值下無(wú)法驗(yàn)證程序(程序可能滿足或違反其驗(yàn)證屬性)。

k-induction驗(yàn)證是歸納方法在軟件驗(yàn)證中的應(yīng)用,連續(xù)k+1個(gè)狀態(tài)可以看作程序循環(huán)的k次展開(kāi)。當(dāng)k=1時(shí),k-induction退化為標(biāo)準(zhǔn)歸納方法,且隨著k的增大,式(2)的歸納假設(shè)隨之不斷增強(qiáng),從而使證明變得更容易。但若要使用k-induction,程序的安全屬性P必須滿足相應(yīng)的可歸約性(即式(2)不可滿足),否則在當(dāng)前k值下無(wú)法驗(yàn)證程序。

為了將k-induction推廣到一般程序,Beyer等[18]提出了用輔助不變式增強(qiáng)的k-induction算法。具體來(lái)說(shuō),就是用與k-induction算法并行的不變式生成算法為程序生成不斷強(qiáng)化的循環(huán)不變式,在k-induction的每輪驗(yàn)證中用當(dāng)前已知的不變式Inv增強(qiáng)式(2)的歸納假設(shè),也就是改為證明式(3)不可滿足:

(3)

CPAchecker總的k-induction驗(yàn)證流程如下:1)首先初始化一個(gè)較小的k值，以當(dāng)前的k值為界,調(diào)用有界模型檢測(cè)(bounded model checking)算法驗(yàn)證式(1)的可滿足性,若其可滿足,則發(fā)現(xiàn)了一條程序的錯(cuò)誤路徑,結(jié)束驗(yàn)證；2)若式(1)不可滿足,則在當(dāng)前已知不變式的輔助下驗(yàn)證式(3)的可滿足性,若其不可滿足,則程序正確性得證；3)若式(3)可以滿足,且在前面的驗(yàn)證過(guò)程中并行算法生成了更強(qiáng)的不變式,則在新不變式的輔助下重新驗(yàn)證式(3)的可滿足性；4)若式(3)始終可以滿足,則說(shuō)明在當(dāng)前k值與輔助不變式下無(wú)法驗(yàn)證程序的正確性，此時(shí)CPAchecker會(huì)增大k值進(jìn)行下一輪驗(yàn)證,直到得出驗(yàn)證結(jié)果或超時(shí)為止。

2.2 基于不同不變式生成策略的回歸驗(yàn)證

CPAchecker通過(guò)用不斷強(qiáng)化的不變式增強(qiáng)k-induction的歸納假設(shè)以驗(yàn)證程序的正確性。但如果k-induction驗(yàn)證的不是程序的安全屬性,而是一些不變式的候選(如證據(jù)自動(dòng)機(jī)中待檢驗(yàn)的不變式),將驗(yàn)證成立的候選作為輔助不變式提供出去,則k-induction本身也可以作為不變式生成算法。

用CPAchecker的原有配置即可并行兩個(gè)k-induction算法,其中一個(gè)k-induction(下稱“從KI”)為另一個(gè)k-induction(下稱“主KI”)提供輔助不變式,而后者負(fù)責(zé)驗(yàn)證程序的正確性。該配置取程序所有到達(dá)錯(cuò)誤狀態(tài)的控制流路徑的否定作為從KI的候選不變式[18]。每當(dāng)從KI成功證明一條候選不變式λ,從KI就將λ加入輔助不變式提供給主KI以增強(qiáng)主KI的歸納假設(shè);同時(shí)λ作為從KI的已知不變式,在從KI驗(yàn)證其他候選不變式時(shí)也會(huì)增強(qiáng)從KI的歸納假設(shè)。隨著k不斷增大,從KI證明的候選不變式不斷增多,提供給主KI的輔助不變式也不斷增強(qiáng)。

在上述配置的基礎(chǔ)上,提取新證據(jù)文件中受版本變動(dòng)影響的不變式加入從KI的候選不變式,用證據(jù)預(yù)處理得到的不受影響的不變式增強(qiáng)主KI的歸納假設(shè),即可實(shí)現(xiàn)基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證,如圖4所示。除了原有配置的候選不變式,此過(guò)程主要用證據(jù)自動(dòng)機(jī)中的不變式信息增強(qiáng)主KI的歸納假設(shè),但證據(jù)文件包含的不變式可能不足以輔助程序驗(yàn)證[7]。因此,只用從KI生成輔助不變式的回歸驗(yàn)證可能得不到足夠強(qiáng)的歸納假設(shè)。

圖4 基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證Fig. 4 Regression verification based on witness automata

除了k-induction之外,CPAchecker還可用可配置程序分析算法(Configurable Program Analysis Algorithm, CPAAlgorithm)[19]執(zhí)行數(shù)據(jù)流分析生成輔助不變式。CPAAlgorithm通過(guò)廣度優(yōu)先搜索維護(hù)可達(dá)抽象狀態(tài)的集合,動(dòng)態(tài)更新每個(gè)狀態(tài)上的不變式,在每次迭代結(jié)束后將所有狀態(tài)上不變式的析取與當(dāng)前不變式的合取作為輔助不變式提供給主KI。由于CPAAlgorithm應(yīng)用了動(dòng)態(tài)精度調(diào)整,在迭代過(guò)程中會(huì)不斷增加重要程序變量的數(shù)目和表達(dá)式的嵌套深度,因此產(chǎn)生的輔助不變式也是經(jīng)過(guò)連續(xù)精化的[20]。

既然k-induction和CPAAlgorithm都能生成輔助不變式,可以通過(guò)并行主KI、從KI與CPAAlgorithm,在回歸驗(yàn)證中將證據(jù)自動(dòng)機(jī)中的不變式信息與數(shù)據(jù)流分析生成的輔助不變式相結(jié)合。如圖5所示,既可用數(shù)據(jù)流分析生成的輔助不變式增強(qiáng)從KI的歸納假設(shè),再由從KI將其提供給主KI間接增強(qiáng)主KI的歸納假設(shè)(用虛線表示),又可以將數(shù)據(jù)流分析與從KI生成的兩部分輔助不變式合并后直接增強(qiáng)主KI的歸納假設(shè)(用點(diǎn)劃線表示)。

圖5 結(jié)合數(shù)據(jù)流分析的回歸驗(yàn)證Fig. 5 Regression verification combined with data flow analysis

CPAchecker為用輔助不變式增強(qiáng)的k-induction算法實(shí)現(xiàn)了三種不變式生成策略,其中除了不生成不變式的策略DO_NOTHING之外,INDUCTION接受從KI生成的不變式,REACHED_SET接受數(shù)據(jù)流分析生成的不變式。本文另外實(shí)現(xiàn)了新策略KIDF,用來(lái)同時(shí)接受從KI與數(shù)據(jù)流分析生成的不變式。

3 實(shí)驗(yàn)

本章主要介紹不使用證據(jù)自動(dòng)機(jī)中不變式信息的直接驗(yàn)證與2.2節(jié)介紹的三種回歸驗(yàn)證之間的對(duì)比實(shí)驗(yàn)。為了方便表述,下面引入相應(yīng)的符號(hào)記法。

3.1 回歸測(cè)例

實(shí)驗(yàn)的原始測(cè)例來(lái)自于國(guó)際軟件驗(yàn)證大賽的驗(yàn)證任務(wù)集(https://github.com/sosy-lab/sv-benchmarks)。整個(gè)驗(yàn)證任務(wù)集包含了使用C語(yǔ)言(遵循GNU C標(biāo)準(zhǔn))、Java語(yǔ)言、霍恩(Horn)子句的待驗(yàn)證程序,涵蓋了可達(dá)性、內(nèi)存安全、并發(fā)安全、可終止性、溢出檢測(cè)等各個(gè)方面的驗(yàn)證。驗(yàn)證任務(wù)集主要為歷屆國(guó)際軟件驗(yàn)證大賽提供統(tǒng)一的、覆蓋面盡可能廣的測(cè)例程序,同時(shí)也被許多研究項(xiàng)目用于評(píng)估軟件驗(yàn)證算法的驗(yàn)證性能。

由于測(cè)例程序被用于回歸驗(yàn)證實(shí)驗(yàn),選取原始測(cè)例時(shí)需要考慮與回歸驗(yàn)證方法的契合度。由于屬性違反時(shí)的證據(jù)文件不包含不變式信息,而回歸驗(yàn)證的核心思想是提取并重用證據(jù)文件中的循環(huán)不變式,因此選取原始測(cè)例時(shí)要排除驗(yàn)證任務(wù)集中違反驗(yàn)證屬性的程序。另外,由于原始測(cè)例程序互不相關(guān),為了由原始測(cè)例生成體現(xiàn)版本迭代過(guò)程的回歸測(cè)例,還需要考慮原始測(cè)例的變異效果。綜上,為了在對(duì)比實(shí)驗(yàn)中更好地體現(xiàn)回歸驗(yàn)證的作用,本文從驗(yàn)證任務(wù)集C語(yǔ)言分支下與Linux內(nèi)核相關(guān)更適合變異的ldv-linux-3.4-simple文件夾中隨機(jī)選取了56個(gè)滿足驗(yàn)證屬性的程序作為版本迭代前的原始測(cè)例程序。

而為了由原始測(cè)例得到回歸測(cè)例,需要將原始測(cè)例中的每個(gè)程序看作獨(dú)立分支下的初始版本,在初始版本的基礎(chǔ)上依次進(jìn)行程序變異得到該分支下的其他版本。進(jìn)行回歸驗(yàn)證時(shí),上一個(gè)版本的證據(jù)文件作為下一個(gè)版本程序驗(yàn)證的輸入。由于要驗(yàn)證不變式重用的效果,與選取原始測(cè)例時(shí)類似,變異程序時(shí)同樣需要舍棄違反驗(yàn)證屬性的版本。

對(duì)于每一個(gè)原始測(cè)例程序P0,用開(kāi)源C程序變異工具M(jìn)ilu[21]對(duì)其進(jìn)行變異得到P1,若P1滿足其驗(yàn)證屬性(用CPAchecker和UAutomizer參與國(guó)際軟件驗(yàn)證大賽的標(biāo)準(zhǔn)配置對(duì)P1的驗(yàn)證結(jié)果均為true),再在P1的基礎(chǔ)上變異得到P2；否則重新由P0變異P1。類似可得P3、P4、P5,從P0到P5代表了一系列版本迭代的完整流程。這樣就得到了56組用于回歸驗(yàn)證的測(cè)例程序,每組回歸測(cè)例包含6個(gè)版本。

本文用獨(dú)立于驗(yàn)證工具的輕量級(jí)開(kāi)源基準(zhǔn)測(cè)試(benchmarking)框架BenchExec[22]對(duì)所有回歸測(cè)例進(jìn)行批量驗(yàn)證,統(tǒng)計(jì)其驗(yàn)證結(jié)果、時(shí)間與內(nèi)存消耗。BenchExec接受一個(gè)XML文件作為輸入,XML文件定義了待執(zhí)行命令、資源使用限制與驗(yàn)證任務(wù)集合。在本實(shí)驗(yàn)中,BenchExec調(diào)用CPAchecker驗(yàn)證所有測(cè)例程序,時(shí)間限制為200 s,內(nèi)存限制為4 GB,CPU核心數(shù)限制為4。

3.2 運(yùn)行環(huán)境

實(shí)驗(yàn)機(jī)器的CPU為i5-4590 (3.30 GHz×4),內(nèi)存為8 GB,操作系統(tǒng)為Ubuntu 16.04 (64位)。實(shí)驗(yàn)所用的CPAchecker版本為1.6.1-svn,Frama-C版本為16.0-Sulfur-beta,Milu版本為3.0,BenchExec版本為1.14。

3.3 實(shí)驗(yàn)結(jié)果與分析

表1 base.properties新增配置項(xiàng)Tab. 1 Additional configuration options in base.properties

表2 對(duì)比實(shí)驗(yàn)結(jié)果Tab. 2 Contrast experiment results

BenchExec調(diào)用CPAchecker得到的驗(yàn)證結(jié)果可能為true、 false或unknown,分別表示屬性滿足、屬性違反或無(wú)法確定(原因可能是運(yùn)行錯(cuò)誤、超時(shí)或內(nèi)存不足等)。由于本實(shí)驗(yàn)在原始測(cè)例選取和版本變異時(shí)均確保程序滿足其驗(yàn)證屬性,因此驗(yàn)證結(jié)果為true對(duì)應(yīng)表2的正確計(jì)數(shù),驗(yàn)證結(jié)果為false對(duì)應(yīng)錯(cuò)誤計(jì)數(shù),而當(dāng)驗(yàn)證結(jié)果為unknown時(shí),驗(yàn)證時(shí)間不足200 s(即由超時(shí)以外的原因?qū)е买?yàn)證結(jié)果無(wú)法確定)對(duì)應(yīng)錯(cuò)誤計(jì)數(shù),反之對(duì)應(yīng)超時(shí)計(jì)數(shù)。由表2可知,除了因驗(yàn)證時(shí)間限制引起的部分超時(shí)(國(guó)際軟件驗(yàn)證大賽的超時(shí)時(shí)間一般設(shè)置為900 s,而本實(shí)驗(yàn)為200 s),所有驗(yàn)證方式得到的驗(yàn)證結(jié)果均為true,與CPAchecker和UAutomizer標(biāo)準(zhǔn)參賽配置的驗(yàn)證結(jié)果相一致,說(shuō)明了實(shí)驗(yàn)結(jié)果的正確性。

4 結(jié)語(yǔ)

在多版本程序的驗(yàn)證中,為了利用鄰近版本之間的共享信息,本文提出了基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證?；贑PAchecker中用輔助不變式增強(qiáng)的k-induction算法,本文設(shè)計(jì)并實(shí)現(xiàn)了三種使用不同不變式生成策略的回歸驗(yàn)證方法,并與不使用不變式信息的直接驗(yàn)證進(jìn)行了對(duì)比實(shí)驗(yàn)。實(shí)驗(yàn)結(jié)果表明，當(dāng)程序滿足其驗(yàn)證屬性時(shí),基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證能極大地提高驗(yàn)證效率,而將證據(jù)自動(dòng)機(jī)與數(shù)據(jù)流分析相結(jié)合的驗(yàn)證方式能得到更好的驗(yàn)證效果。

由于證據(jù)文件包含的不變式可能不足以輔助程序驗(yàn)證或不一定必需,基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證仍然存在一定的局限性,三種回歸驗(yàn)證方法之間的對(duì)比結(jié)果也反映了這一點(diǎn)。在已有回歸驗(yàn)證實(shí)現(xiàn)的基礎(chǔ)上,未來(lái)的工作方向主要在于改進(jìn)不變式生成方法,提高證據(jù)文件中的不變式質(zhì)量,使得只基于證據(jù)自動(dòng)機(jī)的回歸驗(yàn)證就能得到足夠好的驗(yàn)證效果。