基于數(shù)據(jù)分類的循環(huán)不變式自動生成

路 紅 王承毅 黃 皓

1(南京理工大學紫金學院 江蘇 南京 210003) 2(南京大學計算機科學與技術系 江蘇 南京 210023)

0 引 言

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

1 相關工作及貢獻

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

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

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

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

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

(4) 所提出的方法在31個基準測試程序上進行評估和比較。實驗結(jié)果表明，本文所提出的方法能夠為最多的循環(huán)程序生成有效的循環(huán)不變式。

2 問題定義與方法概覽

2.1 問題定義

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

Loop_A和Loop_B是兩個可運行的C循環(huán)程序。其中，Loop_A的變量集合V={i,j,n}，第2行的assume語句表示前置條件P，第7行的assert語句表示后置條件Q。Loop_B的變量集合V={x,y}，第2行的assume語句表示前置條件P，第8行的assert語句表示后置條件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邏輯為程序驗證提供了一套公理和規(guī)則[22]。在文獻[23]中，基于Hoare邏輯的循環(huán)語句驗證使用一種斷言來驗證程序所滿足的性質(zhì)，該斷言即為循環(huán)不變式。

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

(1)P→I。

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

(3)I∧C→Q。

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

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

2.2 方法概覽

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

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

3 后置條件的自動生成

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

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

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

輸入 前置條件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值的變化，計算循環(huán)增量Δ(V)；

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

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

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

就循環(huán)程序Loop_A來說，其后置條件的自動生成步驟如下：首先，依據(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)語句執(zhí)行k次后，變量的值分別為ik=i+k和jk=j+k。循環(huán)體B執(zhí)行k-1次后變量ik-1滿足循環(huán)條件i

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

循環(huán)程序Loop_B后置條件的自動生成步驟如下：首先，依據(jù)前置條件P、循環(huán)條件C和循環(huán)體Q的變量，得到其變量集合V={x,y}。該程序的循環(huán)體有兩種執(zhí)行路徑，分別標記為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)條件，簡化后可得k=-2-x-y。那么，xk=-y-2。最后，再利用前置條件P和Z3簡化，可得到該執(zhí)行路徑的后置條件Qi=(x>0)。同理，得到另外一種執(zhí)行路徑的后置條件Qj=y>0。整個循環(huán)程序Loop_B的后置條件Q為x>0‖y>0。

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

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

4 循環(huán)不變式的自動生成與驗證

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

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

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

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

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

//當前時間

3.Whiletime_limit>=0do{

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

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

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

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

8. time_limit=current_time-start_time;}

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

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

構(gòu)造合理的數(shù)據(jù)集是運用KSVM生成循環(huán)不變式的基礎。假設數(shù)據(jù)集為SV，且其應包含滿足循環(huán)不變式的數(shù)據(jù)集SV+和不滿足循環(huán)不變式的數(shù)據(jù)集SV-。算法4中的第1行主要是構(gòu)造循環(huán)執(zhí)行之前變量的初始值。首先，通過隨機方式生成滿足前置條件的數(shù)據(jù)集SP和不滿足前置條件的數(shù)據(jù)集SN，這兩種方式構(gòu)造測試數(shù)據(jù)集SV=SP∪SN。其次，以測試數(shù)據(jù)集SV作為循環(huán)體執(zhí)行的初始值，依據(jù)循環(huán)條件執(zhí)行有限次循環(huán)語句，并記錄每一次循環(huán)結(jié)束后循環(huán)變量的值，組成數(shù)據(jù)集SC，并將數(shù)據(jù)集SC加入到數(shù)據(jù)集SV中，即SV=SP∪SN∪SC(見算法4的第4行)。第三，依據(jù)文獻[21]提出劃分數(shù)據(jù)集SV中的一個數(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中不能通過Hoare邏輯驗證程序的數(shù)據(jù)。式(1)表示數(shù)據(jù)集SV中一個數(shù)據(jù)樣本s屬于集合CE(SV)的條件為：存在數(shù)據(jù)s0和s′，s0滿足循環(huán)前置條件P，執(zhí)行一次或多次循環(huán)體B后經(jīng)過中間某個狀態(tài)s得到s′，但數(shù)據(jù)s′不滿足后置條件Q。如果集合CE(SV)非空，則表示Hoare三元組不能被驗證。

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)體語句B后得到s′，當循環(huán)結(jié)束時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中的一個數(shù)據(jù)樣本s屬于NE(SV)的條件為：存在數(shù)據(jù)點s0和s′，s0不滿足循環(huán)前置條件P時，執(zhí)行一次或多次循環(huán)體語句B后經(jīng)過中間數(shù)據(jù)s得到s′，循環(huán)終止時s′不滿足后置條件Q。

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

(4)

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

以循環(huán)程序Loop_A為例，假設為變量集合(i,j,n)隨機生成滿足前置條件和不滿足前置條件的數(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的定義，對這些對數(shù)據(jù)進行標注，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)>。

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

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

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

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

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

對于帶分支條件的循環(huán)，為其生成循環(huán)不變式的基本方法是：首先，按照路徑分析方法將循環(huán)分成多條執(zhí)行路徑；然后，對每條路徑按照上述步驟(1)和(2)中的方法，使用KSVM的方法生成候選不變式；最后，將針對不同執(zhí)行路徑求得的循環(huán)不變式進行綜合，從而得到各個循環(huán)不變式的析取式，即可分支循環(huán)程序的候選循環(huán)不變式。例如，Loop_B的循環(huán)體有兩個執(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)不變式的驗證

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

P∧CanInvr

(5)

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

(6)

CanInvr∧Q∧C

(7)

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

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

5 實驗分析

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

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

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

續(xù)表1

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

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

6 結(jié) 語

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