路 紅 王承毅 黃 皓

1(南京理工大學(xué)紫金學(xué)院 江蘇 南京 210003) 2(南京大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系 江蘇 南京 210023)

0 引 言

軟件作為當(dāng)今信息化社會(huì)的重要基礎(chǔ)設(shè)施，已廣泛應(yīng)用于能源、交通、通信、金融和國(guó)防等安全攸關(guān)領(lǐng)域中[1]。然而，隨著軟件集成程度的提高和軟件系統(tǒng)結(jié)構(gòu)的日益復(fù)雜，各類軟件的高可信性越來(lái)越不能保證。軟件驗(yàn)證以邏輯和數(shù)學(xué)為基礎(chǔ)，支持軟件進(jìn)行嚴(yán)格的形式化規(guī)約和驗(yàn)證，是確保軟件可信性的一種有效措施[2-3]。軟件驗(yàn)證的目標(biāo)是證明程序在任何執(zhí)行路徑下均滿足一定的形式化規(guī)約，即程序在確定的條件下執(zhí)行結(jié)束后便可滿足一定的要求。軟件驗(yàn)證的一般步驟是針對(duì)待驗(yàn)證的程序撰寫形式化規(guī)約(如前置條件、后置條件和循環(huán)不變式)，然后利用自動(dòng)驗(yàn)證工具或交互式定理證明器驗(yàn)證給定程序是否滿足所撰寫的形式化規(guī)約[4-5]。為了提高驗(yàn)證效率、簡(jiǎn)化驗(yàn)證難度，出現(xiàn)了Z3[6]、Danfy[7]和Why3[8]等自動(dòng)化驗(yàn)證工具。運(yùn)用這類自動(dòng)化驗(yàn)證工具對(duì)代碼量較少的程序進(jìn)行驗(yàn)證，無(wú)須驗(yàn)證者撰寫大量證明腳本，僅須按照自動(dòng)化驗(yàn)證工具的規(guī)范撰寫待驗(yàn)證程序的形式化規(guī)約，即可快速得到程序是否正確的驗(yàn)證結(jié)果。然而，為程序提供合適的形式化規(guī)約，尤其是循環(huán)不變式，需要驗(yàn)證者依據(jù)對(duì)程序的正確理解進(jìn)行手工撰寫，這對(duì)于程序驗(yàn)證者來(lái)說(shuō)是一項(xiàng)任務(wù)繁重的工作且容易出現(xiàn)錯(cuò)誤。因此，研究循環(huán)不變式的自動(dòng)生成方法，減少人工撰寫程序形式化規(guī)約的工作量以及因人工撰寫形式化規(guī)約導(dǎo)致的驗(yàn)證錯(cuò)誤問題，已成為軟件驗(yàn)證研究領(lǐng)域關(guān)注的一個(gè)重要問題[9]。

1 相關(guān)工作及貢獻(xiàn)

近年來(lái)，已有一些研究致力于循環(huán)不變式的自動(dòng)生成方法研究。文獻(xiàn)[10-12]運(yùn)用參數(shù)模板將循環(huán)不變式設(shè)置為一個(gè)參數(shù)模板，然后利用前置條件和后置條件進(jìn)行約束求解。文獻(xiàn)[13-17]利用抽象解釋方法構(gòu)造多項(xiàng)式循環(huán)不變式，在語(yǔ)義等式基礎(chǔ)上進(jìn)行多次不動(dòng)點(diǎn)迭代計(jì)算，從而生成循環(huán)不變式。這些構(gòu)造循環(huán)不變式的方法均受限于所設(shè)定的模板。文獻(xiàn)[18]使用了“GUSESS AND CHECK”方法，將生成循環(huán)不變式的過(guò)程分為GUSESS和CHECK兩個(gè)階段。其中，GUSESS階段主要生成候選不變式，CHECK階段主要驗(yàn)證GUSESS階段所生成的候選不變式是否正確。若不正確則繼續(xù)迭代執(zhí)行GUSESS和CHECK兩個(gè)階段的步驟，直到生成一個(gè)正確的循環(huán)不變式為止。文獻(xiàn)[19]運(yùn)用游戲和眾包策略將生成候選不變式的過(guò)程交給網(wǎng)絡(luò)游戲玩家來(lái)完成。文獻(xiàn)[20]提出了一種基于數(shù)據(jù)分類生成候選不變式的方法，但不支持具有分支條件的循環(huán)語(yǔ)句生成循環(huán)不變式。文獻(xiàn)[21]提出的不變式生成方法雖然解決了具有分支條件的循環(huán)語(yǔ)句的循環(huán)不變式生成問題，但研究的是針對(duì)抽象程序進(jìn)行不變式的生成方法。

本文提出了一種基于數(shù)據(jù)分類的方法實(shí)現(xiàn)面向可運(yùn)行的C程序自動(dòng)生成循環(huán)不變式。本文的主要貢獻(xiàn)在于：

(1) 設(shè)計(jì)了一種自動(dòng)生成可執(zhí)行C程序后置條件的算法，并構(gòu)造相應(yīng)的Hoare三元組，作為自動(dòng)生成候選循環(huán)不變式的輸入。

(2) 所提出的基于KSVM的自動(dòng)循環(huán)不變式生成方法，支持生成包含析取和合取這兩種謂詞邏輯關(guān)系的、多項(xiàng)式不等式形式的循環(huán)不變式。

(3) 對(duì)于分支循環(huán)程序，首先通過(guò)路徑敏感分析將其劃分成多條執(zhí)行路徑，然后針對(duì)每條執(zhí)行路徑分別使用KSVM分別生成候選不變式，最后使用SMT求解器檢查其正確性，從而得到具有分支條件的循環(huán)程序的循環(huán)不變式。

(4) 所提出的方法在31個(gè)基準(zhǔn)測(cè)試程序上進(jìn)行評(píng)估和比較。實(shí)驗(yàn)結(jié)果表明，本文所提出的方法能夠?yàn)樽疃嗟难h(huán)程序生成有效的循環(huán)不變式。

2 問題定義與方法概覽

2.1 問題定義

為了清晰闡述本文所需解決的問題，我們對(duì)本文中所使用的符號(hào)進(jìn)行界定。符號(hào)C表示循環(huán)條件，符號(hào)B表示循環(huán)體，符號(hào)V={v1,v2,…,vn}表示與循環(huán)語(yǔ)句相關(guān)的變量集合。符號(hào)Bodyi(v)={v1→xi,v2→yi,…,vn→mi}表示循環(huán)程序執(zhí)行第i次循環(huán)后V中各個(gè)變量的值。符號(hào)P表示循環(huán)語(yǔ)句的前置條件，即在執(zhí)行某條程序語(yǔ)句前所需要滿足的公式集合。符號(hào)Q表示循環(huán)語(yǔ)句的后置條件，即在執(zhí)行某條語(yǔ)句后應(yīng)該要滿足的公式集合。

Loop_A和Loop_B是兩個(gè)可運(yùn)行的C循環(huán)程序。其中，Loop_A的變量集合V={i,j,n}，第2行的assume語(yǔ)句表示前置條件P，第7行的assert語(yǔ)句表示后置條件Q。Loop_B的變量集合V={x,y}，第2行的assume語(yǔ)句表示前置條件P，第8行的assert語(yǔ)句表示后置條件Q。

算法1循環(huán)程序Loop_A

1: int loop_function (int i, int n){

2: assume(i==0&&j==0);

3: while (i

4: i=i+1;

5: j=j+1;

6: }

7: assert(i==n-1&&j==i);

8: return j;

9: }

算法2循環(huán)程序Loop_B

1: int loop_function (int x, int y) {

2: assume(x>0||y>0);

3: while (x+y<-2) {

4: if (x>0)

5: x=x+1;

6: else

7: y=y+1;

8: }

9: assert(x>=0||y>=0);

10: return x+y;

11: }

Hoare邏輯為程序驗(yàn)證提供了一套公理和規(guī)則[22]。在文獻(xiàn)[23]中，基于Hoare邏輯的循環(huán)語(yǔ)句驗(yàn)證使用一種斷言來(lái)驗(yàn)證程序所滿足的性質(zhì)，該斷言即為循環(huán)不變式。

定義1斷言I是循環(huán)語(yǔ)句的循環(huán)不變式，當(dāng)且僅當(dāng)其滿足以下3個(gè)條件：

(1)P→I。

(2)I∧C→Bodyi(v)∧I。

(3)I∧C→Q。

條件(1)表示循環(huán)語(yǔ)句的前置條件P可推導(dǎo)出斷言I，即斷言I在循環(huán)的入口點(diǎn)是成立的。條件(2)表示斷言I在循環(huán)體執(zhí)行前后均成立，即在循環(huán)體執(zhí)行之前的程序點(diǎn)、循環(huán)體執(zhí)行之后的程序點(diǎn)及循環(huán)語(yǔ)句的退出點(diǎn)均成立。條件(3)表示斷言I和循環(huán)語(yǔ)句的退出條件可推導(dǎo)出后置條件Q，即斷言I可用于后置條件的正確性驗(yàn)證。條件(1)和條件(2)成立可保證斷言I是循環(huán)語(yǔ)句的循環(huán)不變式，條件(3)說(shuō)明循環(huán)不變式I可證明循環(huán)語(yǔ)句執(zhí)行結(jié)束之后應(yīng)滿足的性質(zhì)。

從定義1可以看出，如果一個(gè)循環(huán)不變式I成立，則循環(huán)程序執(zhí)行前變量集合的取值V0和任意一次循環(huán)執(zhí)行后變量集合的取值Vi均使得I成立。否則，循環(huán)不變式I不成立。從另一個(gè)角度來(lái)看，假如已知數(shù)據(jù)集SV+使條件(1)、(2)、(3)均成立，而數(shù)據(jù)集SV-使條件(1)、(2)、(3)中的任意一個(gè)均不成立，那么循環(huán)不變式I將是SV+和SV-的分類器?；谏鲜霭l(fā)現(xiàn)，本文使用核支持向量機(jī)(Kernel Support Vector Machines，KSVM)[24]求解該分類器，進(jìn)而得到相應(yīng)的循環(huán)不變式。

2.2 方法概覽

使用KSVM作為一種分類器來(lái)自動(dòng)生成循環(huán)不變式的過(guò)程如圖1所示，整個(gè)過(guò)程共分為三個(gè)階段。第一個(gè)階段是預(yù)處理，目標(biāo)是實(shí)現(xiàn)對(duì)程序中循環(huán)語(yǔ)句后置條件的自動(dòng)生成，并將前置條件、循環(huán)語(yǔ)句和后置條件組成Hoare三元組(文件命名為*.cfg)。第二個(gè)階段是迭代生成候選不變式。首先，依據(jù)循環(huán)語(yǔ)句的前置條件隨機(jī)生成測(cè)試數(shù)據(jù)，以這些測(cè)試數(shù)據(jù)作為循環(huán)變量的初始值運(yùn)行循環(huán)語(yǔ)句，并收集循環(huán)語(yǔ)句執(zhí)行過(guò)程中循環(huán)變量的值，組成樣本數(shù)據(jù)集SV。對(duì)數(shù)據(jù)集SV，依據(jù)所生成的Hoare三元組判定SV中的每一個(gè)樣本數(shù)據(jù)s是否屬于循環(huán)不變式的范圍進(jìn)行標(biāo)注，然后使用KSVM對(duì)標(biāo)注后的數(shù)據(jù)集SV進(jìn)行分類，從而自動(dòng)生成候選不變式。為了減少迭代次數(shù)，在候選不變式的邊界線上選擇有限個(gè)樣本數(shù)據(jù)加入到SV中，訓(xùn)練用于生成候選不變式的KSVM分類器，直到其不再發(fā)生變化為止。最后，運(yùn)用SMT求解器驗(yàn)證候選不變式是否存在不滿足Hoare邏輯的反例數(shù)據(jù)。若存在反例數(shù)據(jù)，則將其加入到SV繼續(xù)進(jìn)行下一次迭代，直到產(chǎn)生一個(gè)循環(huán)不變式為止。其中，數(shù)據(jù)集SV的收集有兩種方法：一種是依據(jù)每個(gè)變量的定義域隨機(jī)生成有限組變量的值。另一種是利用SMT求解器分別生成滿足前置條件P和不滿足前置條件P的變量值。第三個(gè)階段是驗(yàn)證自動(dòng)生成的候選循環(huán)不變式是否符合條件(1)、(2)和(3)中，輸出結(jié)果為有效循環(huán)不變式或無(wú)效循環(huán)不變式。

圖1 基于數(shù)據(jù)分類的循環(huán)不變式自動(dòng)生成過(guò)程

3 后置條件的自動(dòng)生成

根據(jù)定義1，循環(huán)不變式與前置條件P、循環(huán)條件C、循環(huán)體B和循環(huán)語(yǔ)句的后置條件Q相關(guān)。后置條件Q是生成循環(huán)不變式的關(guān)鍵，本節(jié)將重點(diǎn)闡述后置條件Q的自動(dòng)生成算法。文獻(xiàn)[25]依據(jù)循環(huán)條件C的特點(diǎn)，將循環(huán)語(yǔ)句的類型分成IVCondition和NIVCondition兩種。如果循環(huán)條件C所包含的每個(gè)循環(huán)控制變量都是可歸納的，則該條件屬于IVCondition類循環(huán)條件。否則，該條件屬于NIVCondition。本文所提出的自動(dòng)后置條件生成算法是面向具有IVCondition類循環(huán)條件的循環(huán)程序。

算法3描述的是循環(huán)語(yǔ)句后置條件的生成方法。第1步，依據(jù)循環(huán)的前置條件P、循環(huán)條件C和循環(huán)體B中所出現(xiàn)的變量構(gòu)造變量集合V。第2步，計(jì)算循環(huán)體B執(zhí)行一次循環(huán)后，變量集合V中各個(gè)變量的增量Δ(V)。假設(shè)程序執(zhí)行第i次循環(huán)后V的值為Vi,程序執(zhí)行第i+1次循環(huán)后V的值為Vi+1,則Δ(V)=Vi+1-Vi。第3步，使用邊界值分析法計(jì)算循環(huán)執(zhí)行次數(shù)k。假定給定的循環(huán)語(yǔ)句在開始執(zhí)行前循環(huán)變量的值滿足前置條件P和循環(huán)條件C，當(dāng)執(zhí)行k次后程序終止，則表示該循環(huán)體B在執(zhí)行k次之后循環(huán)變量的值不滿足循環(huán)條件C。因此，在循環(huán)語(yǔ)句執(zhí)行k-1次后，V的值Vk-1滿足循環(huán)條件C，在執(zhí)行k次循環(huán)后，V的值Vk不滿足的循環(huán)條件，根據(jù)這兩個(gè)條件可計(jì)算出循環(huán)體B的執(zhí)行次數(shù)k。第4步，依據(jù)第2步和第3步計(jì)算的結(jié)果生成關(guān)于集合V中每個(gè)變量在循環(huán)體B執(zhí)行結(jié)束時(shí)的不等式表示形式。最后，對(duì)第4步得到的各個(gè)變量的值的表示形式進(jìn)行簡(jiǎn)化，即可得到后置條件Q。

算法3循環(huán)語(yǔ)句后置條件的自動(dòng)生成算法

輸入 前置條件P,循環(huán)體B。

輸出 后置條件Q。

1.依據(jù)前置條件P，循環(huán)條件C和循環(huán)體B構(gòu)造變量集合V；

2.根據(jù)循環(huán)體B執(zhí)行第i次循環(huán)和第i+1次循環(huán)后的V值的變化，計(jì)算循環(huán)增量Δ(V)；

3.使用邊界值分析法計(jì)算循環(huán)的迭代次數(shù)k;

4.依據(jù)Δ(V)和k，對(duì)變量集合V中的每個(gè)變量計(jì)算循環(huán)執(zhí)行結(jié)束時(shí)的值(不等式形式的表示);

5.依據(jù)前置條件P對(duì)第4步的不等式進(jìn)行簡(jiǎn)化并輸出后置條件Q。

就循環(huán)程序Loop_A來(lái)說(shuō)，其后置條件的自動(dòng)生成步驟如下：首先，依據(jù)其前置條件P、循環(huán)條件C和循環(huán)體B所影響的變量，構(gòu)造變量集合V={i,j}。循環(huán)體B執(zhí)行1次后，變量i和j的增量分別為Δ(i)=1和Δ(j)=1；循環(huán)體B執(zhí)行k-1次后，變量的值分別為ik-1=i+k-1和jk-1=j+k-1；循環(huán)語(yǔ)句執(zhí)行k次后，變量的值分別為ik=i+k和jk=j+k。循環(huán)體B執(zhí)行k-1次后變量ik-1滿足循環(huán)條件i

在現(xiàn)階段的初中語(yǔ)文課外閱讀教學(xué)中，為使教師的教學(xué)方法真正被學(xué)生接受和理解，教師可以采用階梯式閱讀教學(xué)方法，根據(jù)學(xué)生的學(xué)習(xí)情況和理解能力選取合適的讀本，逐步實(shí)現(xiàn)課外閱讀教學(xué)目標(biāo)。學(xué)生在階梯式課外閱讀教學(xué)中，閱讀難度逐漸增強(qiáng)，給學(xué)生閱讀水平提供循序漸進(jìn)的過(guò)程，有利于學(xué)生閱讀能力的發(fā)展和提高，是教師課外閱讀教學(xué)的有效方法。

循環(huán)程序Loop_B后置條件的自動(dòng)生成步驟如下：首先，依據(jù)前置條件P、循環(huán)條件C和循環(huán)體Q的變量，得到其變量集合V={x,y}。該程序的循環(huán)體有兩種執(zhí)行路徑，分別標(biāo)記為pathi和pathj，pathi的循環(huán)條件為x+y<-2∧x>0，在該執(zhí)行路徑下執(zhí)行1次循環(huán)后變量x的增量為Δ(x)=1，執(zhí)行k次和k-1次后變量x的值分別為xk-1=x+k-1和xk=x+k。依據(jù)該執(zhí)行路徑的循環(huán)條件，簡(jiǎn)化后可得k=-2-x-y。那么，xk=-y-2。最后，再利用前置條件P和Z3簡(jiǎn)化，可得到該執(zhí)行路徑的后置條件Qi=(x>0)。同理，得到另外一種執(zhí)行路徑的后置條件Qj=y>0。整個(gè)循環(huán)程序Loop_B的后置條件Q為x>0‖y>0。

Hoare三元組描述一段代碼在執(zhí)行后如何改變程序的狀態(tài)，其由前置條件P，后置條件Q和程序組成。在生成循環(huán)的后置條件Q之后，循環(huán)語(yǔ)句的Hoare三元組可快速構(gòu)造出。Loop_A和Loop_B的Hoare三元組如圖2所示。在圖2中，第1行表示循環(huán)語(yǔ)句的變量集合V，第2行表示循環(huán)執(zhí)行前變量的初值，第3行表示循環(huán)的前置條件P，第4行表示循環(huán)條件C，第5行表示循環(huán)體B，第6行表示后置條件Q。

圖2 循環(huán)語(yǔ)句的Hoare三元組

4 循環(huán)不變式的自動(dòng)生成與驗(yàn)證

算法4是提出的基于數(shù)據(jù)分類的循環(huán)不變式自動(dòng)生成方法。算法4以第3節(jié)所生成的Hoare三元組作為輸入，執(zhí)行后輸出所得到的循環(huán)不變式I。

算法4循環(huán)不變式的自動(dòng)生成算法

輸入 Hoare三元組，time_limit=600 s。

輸出 循環(huán)不變式I。

1. 依據(jù)前置條件P隨機(jī)生成測(cè)試數(shù)據(jù)，得到數(shù)據(jù)集SV；

//當(dāng)前時(shí)間

3.Whiletime_limit>=0do{

4. 以數(shù)據(jù)集SV作為測(cè)試數(shù)據(jù)，運(yùn)行循環(huán)語(yǔ)句并記錄循環(huán)變量值，將其加入到數(shù)據(jù)集SV；

5. 標(biāo)注數(shù)據(jù)集SV的變量值是否屬于循環(huán)不變式的范圍，將其分為CE(SV)、PE(SV)、NE(SV)和NP(SV)四類樣本；

6. 使用KSVM方法對(duì)SV中的樣本進(jìn)行分類，生成候選不變式CanInvr；

7. 驗(yàn)證CanInvr是否能夠存在反例使得條件(1)、(2)、(3)的取反成立，如果成立則將反例加入到數(shù)據(jù)集SV，繼續(xù)迭代下一次循環(huán)，如果不存在反例，則I=CanInvr；

8. time_limit=current_time-start_time;}

9. 驗(yàn)證循環(huán)不變式I是否有效。

4.1 循環(huán)不變式的自動(dòng)生成

構(gòu)造合理的數(shù)據(jù)集是運(yùn)用KSVM生成循環(huán)不變式的基礎(chǔ)。假設(shè)數(shù)據(jù)集為SV，且其應(yīng)包含滿足循環(huán)不變式的數(shù)據(jù)集SV+和不滿足循環(huán)不變式的數(shù)據(jù)集SV-。算法4中的第1行主要是構(gòu)造循環(huán)執(zhí)行之前變量的初始值。首先，通過(guò)隨機(jī)方式生成滿足前置條件的數(shù)據(jù)集SP和不滿足前置條件的數(shù)據(jù)集SN，這兩種方式構(gòu)造測(cè)試數(shù)據(jù)集SV=SP∪SN。其次，以測(cè)試數(shù)據(jù)集SV作為循環(huán)體執(zhí)行的初始值，依據(jù)循環(huán)條件執(zhí)行有限次循環(huán)語(yǔ)句，并記錄每一次循環(huán)結(jié)束后循環(huán)變量的值，組成數(shù)據(jù)集SC，并將數(shù)據(jù)集SC加入到數(shù)據(jù)集SV中，即SV=SP∪SN∪SC(見算法4的第4行)。第三，依據(jù)文獻(xiàn)[21]提出劃分?jǐn)?shù)據(jù)集SV中的一個(gè)數(shù)據(jù)s是否滿足循環(huán)不變式的方法，將SV劃分為CE(SV)、PE(SV)、NE(SV)和NP(SV)四種分類集(見算法4的第5行)。

CE(SV)={s∈SV}|?s0,s′,s0∈P∧s0→

s→s′∧s′∈C∧s′∈Q

(1)

CE(SV)包含數(shù)據(jù)集SV中不能通過(guò)Hoare邏輯驗(yàn)證程序的數(shù)據(jù)。式(1)表示數(shù)據(jù)集SV中一個(gè)數(shù)據(jù)樣本s屬于集合CE(SV)的條件為：存在數(shù)據(jù)s0和s′，s0滿足循環(huán)前置條件P，執(zhí)行一次或多次循環(huán)體B后經(jīng)過(guò)中間某個(gè)狀態(tài)s得到s′，但數(shù)據(jù)s′不滿足后置條件Q。如果集合CE(SV)非空，則表示Hoare三元組不能被驗(yàn)證。

PE(SV)={s∈SV}|?s0,s∧′,s_0∈P∧s_0→

s→s′∧s′∈C∧s′∈Q

(2)

PE(SV)包含數(shù)據(jù)集SV中屬于數(shù)據(jù)集SV+的樣本數(shù)據(jù)，其一定滿足循環(huán)不變式。式(2)表示數(shù)據(jù)集SV中的數(shù)據(jù)樣本s屬于集合PE(SV)的條件為：存在數(shù)據(jù)s0和s′，s0滿足循環(huán)前置條件P，執(zhí)行一次或多次循環(huán)體語(yǔ)句B后得到s′，當(dāng)循環(huán)結(jié)束時(shí)s′滿足后置條件Q。

NE(SV)={s∈SV}|s0,s′,s0∈P∧s0→

s→s′∧s′∈C∧s′∈Q

(3)

NE(SV)包含數(shù)據(jù)集SV中屬于數(shù)據(jù)集SV-的樣本數(shù)據(jù)，其一定不滿足循環(huán)不變式。式(3)表示表示數(shù)據(jù)集SV中的一個(gè)數(shù)據(jù)樣本s屬于NE(SV)的條件為：存在數(shù)據(jù)點(diǎn)s0和s′，s0不滿足循環(huán)前置條件P時(shí)，執(zhí)行一次或多次循環(huán)體語(yǔ)句B后經(jīng)過(guò)中間數(shù)據(jù)s得到s′，循環(huán)終止時(shí)s′不滿足后置條件Q。

NP(SV)=SV-CE(SV)-PE(SV)-NE(SV)

(4)

式中：NP(SV)表示SV中存在的、不能確定屬于上述三類樣本的數(shù)據(jù)集合。

以循環(huán)程序Loop_A為例，假設(shè)為變量集合(i,j,n)隨機(jī)生成滿足前置條件和不滿足前置條件的數(shù)據(jù)集為(0,0,29)、(1,7,7)和(0,0,-8)，以這3組數(shù)據(jù)作為初始變量值，執(zhí)行循環(huán)體后可得到變量的中間狀態(tài)值分別為<(0,0,29)，(1,1,29)，(2,2,29)，…，(30,30,29)>、<(1,7,7)>和<(0,0,-8)>。然后，依據(jù)CE、PE、NE和NP的定義，對(duì)這些對(duì)數(shù)據(jù)進(jìn)行標(biāo)注，CE(SV)為空，PE(SV)為<(0,0,29)，(1,1,29)，(2,2,29)，…，(30,30,29)>，NE(SV)為<(1,7,7)>和NP(SV)為<(0,0,-8)>。

通過(guò)上述方法生成數(shù)據(jù)集SV并對(duì)其所屬類別進(jìn)行標(biāo)注。根據(jù)算法4中第6行，采用KSVM方法對(duì)數(shù)據(jù)集SV進(jìn)行分類，可得到一個(gè)候選不變式CanInv，具體生成步驟如下：

(1) 利用KSVM對(duì)數(shù)據(jù)集SV進(jìn)行分類，生成一個(gè)分類器，將它作為初始候選不變式CanInv；

(2) 在分類器邊界上選取樣本添加到SV中，通過(guò)多次迭代得到優(yōu)化后的候選不變式CanInv。

通過(guò)步驟(1)，基于隨機(jī)生成的測(cè)試數(shù)據(jù)，采用KSVM生成一個(gè)線性不等式，即第一個(gè)候選不變式。該候選不變式是由有限個(gè)隨機(jī)樣本分類得到，其不能保證對(duì)所有可能的測(cè)試數(shù)據(jù)都能準(zhǔn)確分類。因此，得到一個(gè)初始候選不變式CanInv后，通過(guò)步驟(2)，在候選不變式的分類邊界上選擇兩個(gè)樣本數(shù)據(jù)，將這兩個(gè)樣本數(shù)據(jù)加入到SV中后，再次使用KSVM生成新的候選不變式CanInv。當(dāng)在候選不變式的分類邊界上選擇的數(shù)據(jù)樣本不能生成新的候選不變式CanInv時(shí)，生成候選不變式的過(guò)程便可結(jié)束，從而得到優(yōu)化后的候選不變式。選擇樣本的過(guò)程是先將得到的候選不變式轉(zhuǎn)換為等式，然后假定其中某一個(gè)變量為任意整數(shù)，求其他變量的值。例如，Loop_A的初始候選不變式為342-7×i+8×n≥0，其分邊界為等式342-7×i+8×n=0。假定n=1，從而求得i=60，得到變量集合(n,i)的一個(gè)選擇樣本數(shù)據(jù)為(1,60)。

此外，為了生成合取式的循環(huán)不變式，每次在集合NE(SV)中選擇一個(gè)數(shù)據(jù)樣本s，使用KSVM將數(shù)據(jù)s和集合PE(SV)中的數(shù)據(jù)進(jìn)行分類得到一個(gè)分類器，迭代有限次這個(gè)過(guò)程后，直到NE(SV)為空，最后將每個(gè)分類器按照合取式關(guān)系生成候選不變式CanInv[22]。例如，采用這種方法，可生成Loop_A的候選循環(huán)不變式(78-n≥0)∧(1-i+j≥0)∧(47-i≥0)∧(i-j≥0)。

對(duì)于帶分支條件的循環(huán)，為其生成循環(huán)不變式的基本方法是：首先，按照路徑分析方法將循環(huán)分成多條執(zhí)行路徑；然后，對(duì)每條路徑按照上述步驟(1)和(2)中的方法，使用KSVM的方法生成候選不變式；最后，將針對(duì)不同執(zhí)行路徑求得的循環(huán)不變式進(jìn)行綜合，從而得到各個(gè)循環(huán)不變式的析取式，即可分支循環(huán)程序的候選循環(huán)不變式。例如，Loop_B的循環(huán)體有兩個(gè)執(zhí)行路徑：pathi為(4,6,7)行，pathj為(4,8,9)行。pathi的候選循環(huán)不變式為x>0，pathj的候選循環(huán)不變式為y>0，則分支循環(huán)程序Loop_B的候選循環(huán)不變式為x>0‖y>0。

4.2 循環(huán)不變式的驗(yàn)證

有效的循環(huán)不變式必須是能夠依據(jù)Hoare邏輯規(guī)則驗(yàn)證循環(huán)。而4.1節(jié)得到的候選不變式是通過(guò)KSVM分類測(cè)試樣本數(shù)據(jù)得到的不變式，不能確定其是否為有效循環(huán)不變式，故本節(jié)目標(biāo)是驗(yàn)證候選不變式的有效性，進(jìn)而求得可驗(yàn)證的循環(huán)不變式。

P∧CanInvr

(5)

(SV(sv+)∧C,Body)∧CanInvr

(6)

CanInvr∧Q∧C

(7)

式(5)-式(7)分別是Hoare邏輯規(guī)則中循環(huán)不變式的取反，即CanInvr。如果一個(gè)候選循環(huán)不變式是有效的循環(huán)不變式的話，其必定不會(huì)使得式(5)-式(7)中任何一個(gè)條件成立。算法4中的第7行，則是通過(guò)SMT求解器(如Z3)驗(yàn)證候選不變式是否滿足式(5)-式(7)中的任意一個(gè)，如果滿足，將會(huì)產(chǎn)生一個(gè)反例數(shù)據(jù)，將該反例數(shù)據(jù)加入到數(shù)據(jù)集SV中，迭代調(diào)用KSVM算法訓(xùn)練分類器，直到?jīng)]有反例為止。如果不滿足式(5)-式(7)，則候選不變式為有效的循環(huán)不變式。

使用Z3驗(yàn)證Loop_A的候選不變式是否滿足式(5)-式(7)時(shí)，得到一組反例(0,0,-31)和(0,0,79)，依次將兩個(gè)數(shù)據(jù)加入到SV后訓(xùn)練分類器，得到優(yōu)化的循環(huán)不變式為i-j≥0。經(jīng)Z3驗(yàn)證，i-j≥0為L(zhǎng)oop_A的一個(gè)有效循環(huán)不變式。

5 實(shí)驗(yàn)分析

為評(píng)估本文所提出的循環(huán)不變式自動(dòng)生成方法，使用C++、KLEE[26]和Z3實(shí)現(xiàn)了一個(gè)原型系統(tǒng)。首先，使用C++實(shí)現(xiàn)了后置條件的自動(dòng)生成。然后，使用約束求解器Z3簡(jiǎn)化后置條件。其次，將自動(dòng)生成的后置條件、前置條件以及循環(huán)語(yǔ)句構(gòu)造成Hoare三元組作為輸入，隨機(jī)生成測(cè)試數(shù)據(jù)集并利用Z3生成滿足前置條件的測(cè)試數(shù)據(jù)，以這些測(cè)試數(shù)據(jù)作為程序變量的初始值，應(yīng)用KLEE執(zhí)行循環(huán)語(yǔ)句并記錄每次循環(huán)體執(zhí)行后變量的值。最后，使用KSVM方法對(duì)這些中間數(shù)據(jù)進(jìn)行分類得到候選不變式。最后，使用Z3驗(yàn)證所生成的候選循環(huán)不變式是否為可驗(yàn)證的循環(huán)不變式。

SV-Comp[27]是由慕尼黑大學(xué)構(gòu)建并維護(hù)的形式化驗(yàn)證方法的基準(zhǔn)測(cè)試數(shù)據(jù)集，為評(píng)估形式化驗(yàn)證技術(shù)提供了公平的基準(zhǔn)測(cè)量程序。為驗(yàn)證本文所提出的不變式自動(dòng)生成方法，我們?cè)赟V-Comp2019提供的C測(cè)試程序庫(kù)中選擇了被已有的文獻(xiàn)[21,28-30]使用的31個(gè)測(cè)試程序進(jìn)行實(shí)驗(yàn)分析。每個(gè)測(cè)試程序由前置條件和循環(huán)語(yǔ)句組成，所選擇的測(cè)試程序不包含數(shù)組和嵌套循環(huán)，且循環(huán)條件是可歸納的。為了評(píng)估本文所提出算法的有效性，將本文所提出的循環(huán)不變式自動(dòng)生成方法與ZILU[21]、CPAChecker[28]、BLAST[29]和InvGen[30]這四種方法進(jìn)行對(duì)比，實(shí)驗(yàn)結(jié)果如表1所示。ZILU是一個(gè)采用數(shù)據(jù)分類生成循環(huán)不變式的工具，其以循環(huán)程序的Hoare三元組開始，運(yùn)用SVM生成循環(huán)不變式。CPAChecker是一款基于抽象解釋的循環(huán)不變式的自動(dòng)生成工具。BLAST是一款驗(yàn)證C程序是否滿足指定安全屬性的自動(dòng)驗(yàn)證工具，其基于反例自動(dòng)構(gòu)造循環(huán)不變式。InvGen是一種結(jié)合靜態(tài)分析和動(dòng)態(tài)分析方法自動(dòng)生成線性算術(shù)循環(huán)不變式的工具。

表1 基于KSVM生成循環(huán)不變式的實(shí)驗(yàn)結(jié)果

續(xù)表1

在表1中，T表示可生成有效的循環(huán)不變式，F(xiàn)表示不能生成有效的循環(huán)不變式。第1列表示測(cè)試用的C程序標(biāo)識(shí)號(hào)，第2列是生成循環(huán)不變式所需要的樣本數(shù)據(jù)的個(gè)數(shù)，第3列表示生成循環(huán)不變式所需要的平均迭代次數(shù)，第4列表示使用本文所提出的方法是否能夠生成可驗(yàn)證的循環(huán)不變式，后面4列是利用其他4種循環(huán)不變式生成方法可否為相應(yīng)的測(cè)試程序生成可驗(yàn)證的循環(huán)不變式。

從表1可以看出，ZILU僅可成功為26個(gè)測(cè)試程序生成可驗(yàn)證的循環(huán)不變式。CAPchecker、BLAST和InvGen分別可為28個(gè)測(cè)試程序生成可驗(yàn)證的循環(huán)不變式。相比之下，本文提出的循環(huán)不變式自動(dòng)生成方法可為所有31個(gè)測(cè)試程序生成候選不變式，僅有兩個(gè)候選不變式不能驗(yàn)證通過(guò)，分別是lh8和lh23。同時(shí)，所生成的循環(huán)不變式中各個(gè)元素關(guān)系可以是線性的、析取的或合取的。由此可見，本文所提出的循環(huán)不變式生成方法可基于后置條件，采用KSVM分類方法自動(dòng)生成有效的循環(huán)不變式。值得注意的是，本文所提出的方法在生成循環(huán)不變式的成本較低，生成一個(gè)循環(huán)不變式需要的平均測(cè)試樣本數(shù)約為46.1，平均循環(huán)迭代次數(shù)約為3.5。

6 結(jié) 語(yǔ)

本文提出了一種基于數(shù)據(jù)分類的循環(huán)不變式自動(dòng)生成方法，通過(guò)隨機(jī)生成測(cè)試數(shù)據(jù)、在初始候選不變式的分類邊界選擇測(cè)試數(shù)據(jù)、KSVM分類等方法，可為可行C循環(huán)程序自動(dòng)生成可驗(yàn)證的循環(huán)不變式。實(shí)驗(yàn)驗(yàn)證與分析表明，本文所提出的循環(huán)不變式自動(dòng)生成方法不僅能夠?yàn)檩^少的循環(huán)程序生成有效的循環(huán)不變式，而且生成成本較低。