賈尚坤,賀 飛

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

0 引言

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

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

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

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

圖2 證據(jù)自動機(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)證過程中到達(dá)錯誤狀態(tài)的反例路徑信息。由于回歸驗(yàn)證的關(guān)鍵在于鄰近版本之間的共享信息,因此基于證據(jù)自動機(jī)的回歸驗(yàn)證的主要目標(biāo)是提取并重用證據(jù)文件中的共享信息。對于鄰近版本的程序而言,若均滿足驗(yàn)證屬性,則相同或相近程序位置處成立的不變式很可能相差不大;而若均違反驗(yàn)證屬性,前一版本的反例路徑在后一版本中未必有效,即使有效也未必導(dǎo)向錯誤狀態(tài)。因此,基于證據(jù)自動機(jī)的回歸驗(yàn)證主要指的是提取并重用之前版本正確證據(jù)中的循環(huán)不變式,對多版本程序進(jìn)行回歸驗(yàn)證。

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

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

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

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

1.1 影響域分析

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

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

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

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

a6 1

int c=a+b;

d12 2

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

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

/*@ impact pragma stmt; */

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

frama-c -impact-pragma -impact-print

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

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

1.2 證據(jù)文件生成

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

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

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

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

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

1)

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

2)

對于diff.txt中的每一行diffline:

3)

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

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

對新版程序進(jìn)行回歸驗(yàn)證的關(guān)鍵在于提取并重用原證據(jù)文件中的不變式信息。不受版本變動影響的不變式可以直接重用,而受影響的不變式則需要在新證據(jù)文件中檢驗(yàn)通過后才能重用。檢驗(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]。后來k-induction技術(shù)逐漸應(yīng)用到軟件分析與驗(yàn)證領(lǐng)域,如直接內(nèi)存訪問競爭分析[15]、同步程序分析[16]與嵌入式軟件驗(yàn)證[17]等。

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

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

(1)

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

(2)

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

k-induction驗(yàn)證是歸納方法在軟件驗(yàn)證中的應(yīng)用,連續(xù)k+1個狀態(tài)可以看作程序循環(huán)的k次展開。當(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值下無法驗(yàn)證程序。

為了將k-induction推廣到一般程序,Beyer等[18]提出了用輔助不變式增強(qiáng)的k-induction算法。具體來說,就是用與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)首先初始化一個較小的k值，以當(dāng)前的k值為界,調(diào)用有界模型檢測(bounded model checking)算法驗(yàn)證式(1)的可滿足性,若其可滿足,則發(fā)現(xiàn)了一條程序的錯誤路徑,結(jié)束驗(yàn)證；2)若式(1)不可滿足,則在當(dāng)前已知不變式的輔助下驗(yàn)證式(3)的可滿足性,若其不可滿足,則程序正確性得證；3)若式(3)可以滿足,且在前面的驗(yàn)證過程中并行算法生成了更強(qiáng)的不變式,則在新不變式的輔助下重新驗(yàn)證式(3)的可滿足性；4)若式(3)始終可以滿足,則說明在當(dāng)前k值與輔助不變式下無法驗(yàn)證程序的正確性，此時(shí)CPAchecker會增大k值進(jìn)行下一輪驗(yàn)證,直到得出驗(yàn)證結(jié)果或超時(shí)為止。

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

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

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

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

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

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

既然k-induction和CPAAlgorithm都能生成輔助不變式,可以通過并行主KI、從KI與CPAAlgorithm,在回歸驗(yàn)證中將證據(jù)自動機(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,用來同時(shí)接受從KI與數(shù)據(jù)流分析生成的不變式。

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

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

3.1 回歸測例

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

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

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

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

本文用獨(dú)立于驗(yàn)證工具的輕量級開源基準(zhǔn)測試(benchmarking)框架BenchExec[22]對所有回歸測例進(jìn)行批量驗(yàn)證,統(tǒng)計(jì)其驗(yàn)證結(jié)果、時(shí)間與內(nèi)存消耗。BenchExec接受一個XML文件作為輸入,XML文件定義了待執(zhí)行命令、資源使用限制與驗(yàn)證任務(wù)集合。在本實(shí)驗(yàn)中,BenchExec調(diào)用CPAchecker驗(yàn)證所有測例程序,時(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 對比實(shí)驗(yàn)結(jié)果Tab. 2 Contrast experiment results

BenchExec調(diào)用CPAchecker得到的驗(yàn)證結(jié)果可能為true、 false或unknown,分別表示屬性滿足、屬性違反或無法確定(原因可能是運(yùn)行錯誤、超時(shí)或內(nèi)存不足等)。由于本實(shí)驗(yàn)在原始測例選取和版本變異時(shí)均確保程序滿足其驗(yàn)證屬性,因此驗(yàn)證結(jié)果為true對應(yīng)表2的正確計(jì)數(shù),驗(yàn)證結(jié)果為false對應(yīng)錯誤計(jì)數(shù),而當(dāng)驗(yàn)證結(jié)果為unknown時(shí),驗(yàn)證時(shí)間不足200 s(即由超時(shí)以外的原因?qū)е买?yàn)證結(jié)果無法確定)對應(yīng)錯誤計(jì)數(shù),反之對應(yīng)超時(shí)計(jì)數(shù)。由表2可知,除了因驗(yàn)證時(shí)間限制引起的部分超時(shí)(國際軟件驗(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é)果相一致,說明了實(shí)驗(yàn)結(jié)果的正確性。

4 結(jié)語

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

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