一種自適應的循環不變式生成方法

劉自恒，曾慶凱,b

(南京大學 a.計算機科學與技術系；b.計算機軟件新技術國家重點實驗室，南京 210093)

1 概述

軟件的任何漏洞都可能導致非常嚴重的后果。無論是軟件設計人員還是軟件的用戶，均希望在軟件系統投入在正式使用之前，能得到軟件正確性的保證。通過測試可以在一定程度上保證軟件的正確性，但成本較高，不能完全保證軟件的可靠，而且測試只能發現程序中的錯誤，不能證明程序無錯。從另一個角度考慮，如果可以從理論上證明程序符合預期的行為或者沒有某種錯誤，同樣可以認為軟件是可靠的。20世紀50年代出現的形式化方法思想，以嚴格的數學和邏輯理論為基礎，適合于軟件和硬件系統的描述、開發和驗證。

1967年，Floyd提出采用形式化方法證明程序的正確性，經過多年的研究，取得了一系列理論和實踐的重大進展。在形式化分析驗證程序時，以Floyd-Hoare邏輯為基礎，將程序轉換為抽象模型，進行邏輯歸納演繹，驗證程序是否滿足程序規范。使用形式化的思想對程序進行分析驗證并不排斥測試，但可以認為它是一種更好的測試框架。在分析驗證時開發者給出要驗證函數的規范，但是在低層次結構上(如基本指令、分支、循環結構等)需要驗證程序自動地推導這些結構的規范，表達出它們實現的語義。對于基本的結構，如賦值和分支，Hoare邏輯已經給出了直接的轉換規則；但是循環結構中需要循環不變式來證明循環初始時和執行過程中均保持的性質，而 Hoare邏輯沒有給出直接的生成循環不變式的規則，這是因為并不存在通用的不變式生成規則。因此，形式化程序分析的一個關鍵性難點在于程序中循環結構的存在，而且實際的循環結構中常常又有嵌套循環和分支結構，操作的數據類型除矢量型變量外，還包含數組等向量型變量，使得循環不變式的生成工作變得困難。

本文分析、總結了當前常見的循環不變式生成方法，并提出一種改進的循環不變式生成方法，并通過實驗評價其分析性能。

2 現有方法

通常對于給定的函數前置條件和后置條件，不變式并不是唯一的，開發人員往往增量地得到不變式：首先預測不變式，然后通過觀察程序行為來逐步細化預測的不變式[1]，最終得到驗證所需要的不變式信息。計算循環不變式的方法主要有下面的幾種。

2.1 基于迭代不動點的計算

使用該方法的技術有數據流分析、模型檢測和抽象解釋等。在計算程序的狀態轉換過程中，連續地計算直到得到數據流方程的最小不動點，當發現程序狀態不再變化時，認為發現不動點。計算的過程是一個不斷迭代直到收斂的過程。但計算過程的收斂性是不可判定的，因此需要一些技術來保證和加速收斂的過程，如使用放大算子、提高抽象粒度等。

使用放大算子會導致一定程序的精度損失，因此，要盡可能地延遲使用放大算子的時機，如使用前向放大[2]，同時在合適的位置再使用縮小算子。其他的加速措施也存在同樣的問題，需要在效率和精度之間取一個合理的平衡點。

2.2 基于參數化模板

該方法主要針對線性數值計算程序進行。計算時通過程序或開發者指定目標不變式的模板形式，其中變量的系數未知，稱為模板參數；程序經過抽象解釋映射為抽象域上的轉換系統；使用不同的技術求解模板中的系數，得到不變式。根據與結合求解的技術不同，又可細分如下：

(1)與約束求解結合。首先由開發者或程序默認為循環指定一個帶參數的不變式模板，其中變量的系數未知；隨后采用歸納斷言方法，建立不變式之間以及不變式與循環的前置條件之間的約束，再利用 Farkas定理[3]，消除約束中出現的程序變量，并表達出循環相關的條件，得到關于模板參數的非線性約束，從而將線性循環不變式構造問題轉化為約束求解問題。最后，使用因式分解、線性規劃或非線性求解器等方法求參數的數值解。基于約束的方法相對于基于不動點計算的方法有如下優點：目標指向性明確，效率更高。不需要使用難以控制的放大方法，精確損失小[4]。

(2)與可滿足性(Satisfiability,SAT)求解結合。先將約束化為合取范式，然后利用Farkas定理消除約束中的程序變量，再將約束中的參數建模為比特向量(bit-vector)，進而將該約束轉化為布爾公式，使用SAT求解器搜索滿足約束的參數值。該方法受益于SAT求解技術的進步。

(3)與量詞消去結合[5-6]。如果通過循環完成對數組的操作，則不變式公式中將含有量詞，無法直接使用約束求解或SAT求解，需要先將其中的量詞消去得到與之等價的不包含量詞的公式，然后再使用約束求解或SAT求解的方法來解。

面向驗證性質的增量式歸納不變式構造方法[7]。該方法根據驗證不成立時，求解器返回的虛假反例增量式地生成歸納的不變式，這樣提高了生成不變式的效率，能夠得到剛好滿足驗證需求的不變式性質。

在基于參數化模板的不變式生成方法中，增加模板大小可以有更大機會使得前置條件適應模板，但會生成更大的 SAT式子要求解[4]，使得求解所需的時間和空間變大。對于模板形式的選擇，文獻[4,8-9]由用戶指定不變式模板(同時程序提供了默認的模板可以使用)，文獻[4]既可以由用戶指定模板(如指定未知關系式析取范式表示中合取和析取數量的最大值)，也提供了一種迭代增加模板大小的方案，直到發現某個解。適用范圍方面，文獻[10]只處理簡單while程序并針對線性算術運算，文獻[11-12]只能處理一個簡化了的程序語言，等同于一個C語言的子集，文獻[13]擴大了文獻[11]的適應范圍。

這種生成不變式方法并不是歸納的，求解之前需要開發者給出正確的模板形式；應用擴展性受限于約束求解器的求解能力；對于這種生成方式，用戶指定的模板形式固定，需要與用戶交互，對使用者來講比較繁瑣，適應性不強。

2.3 基于機器學習和實際執行的方法

文獻[1,14]提出可以通過機器學習的方法來推斷循環不變式。而Daikon[15]是動態不變式發現器，可以探測包括C、C++、Java、Perl語言編寫的程序和含有記錄型結構的數據類型。

3 改進方法

通過前面的介紹可以發現，現有的不變式生成方法存在以下不足：(1)處理程序能力往往有限，通常假定處理某個簡單的程序語言，應對復雜的C語言能力不足。(2)使用了參數化模板求解的方法，其靈活性不足，需要開發者在對程序深刻理解的基礎上指定模板形式，然后對模板系數求解，不能自動地考慮程序中的操作語義信息。(3)現有的方法有的只關注循環內容本身，有的除循環外只關注了循環外的某一點信息，沒有綜合考慮函數規范、循環本身、循環后操作等內容，使得生成的不變式不夠全面。(4)現有的工作沒有從執行不變式生成分析，其分析結果是否使得函數規范得以順利完成驗證方面進行檢驗，而這正是進行不變式生成分析的原始出發點，現有工作缺乏一定的實踐性評估。

本文提出以下改進思路，基于條件賦值轉換和自適應模板規則生成循環不變式，在生成過程中綜合考慮函數規范、循環本身、循環后操作等信息，這樣能更有針對性地、自動地發現潛在的循環不變式，但這種分析是一種保守的分析，會產生并不正確的不變式，需要進行驗證；對分析的結果，除了評價不變式本身的正確性外，還從程序驗證的角度，根據分析結果是否使得驗證順利完成，對其有效性進行分析。

3.1 條件賦值轉換

基于條件賦值轉換控制流的思想，這里提出一種條件賦值轉換的方法。對于循環中的每一條賦值語句，直接根據分支條件和賦值操作類型的不同，轉換得到不同的候選不變式，轉換的規則主要有下面的幾種，本文參考文獻[16]的一些做法，執行一些變量變換。這里假定循環開始時變量x的取值范圍為集合x0，它可以是離散的集合，也可能是連續的區間；P表示更新操作的內容，包含四則運算、指針引用等。標量變量指只包含一個值的變量，如C語言中的基本數據類型，矢量變量指包含一系列值的變量，如數組。這里不考慮包含用戶自定義數據類型的賦值操作。

(1)分支判斷條件和賦值操作都是標量型變量操作(非數組、指針變量)：

(2)分支判斷條件為標量型變量，賦值操作為數組訪問操作，若數組A長度為len：

(3)分支判斷條件是關于下標的判斷，賦值操作為數組訪問操作，若數組A長度為len：

(4)分支判斷條件是關于數組元素值的，賦值操作為數組訪問操作，若數組A長度為len：

(5)分支判斷條件是關于同一數組元素之間值的，賦值操作為數組訪問操作，若數組A長度為len：

(6)分支判斷條件是關于2個數組元素之間值的，賦值操作為數組訪問操作，若數組A長度為len1，數組B長度為len2：

在上面的轉換規則中，如果數組的長度不能確定，則排除對于下標表達式上界的約束表達。

正確性說明。以第(1)條規則為例，其他的與之類似。結果由兩部分構成。當變量x∈x0時即變量在初始值范圍內時，由于未執行賦值操作，具有屬性y!=P；當變量值不在初始值范圍內時，認為是在循環中，當滿足路徑條件f(x) ＞0時，執行賦值操作，因而有 f(x) ＞0? y=P。這些轉換規則是對于程序語義的直觀的邏輯轉換，同時通過變量轉換等方式表達了有關數組下標變換的屬性；但由于忽略了變量間的別名關系、變量的值范圍分析并不總是準確等元素，導致轉換結果存在過近似的問題，因此需要驗證其正確性。

3.2 自適應模板生成

這里的模板生成不變式的方法和前面的有所不同，不是根據指定的模板形式求解未知的模板變量系數，而是以一種啟發式的方法生成模板形式表達的候選不變式。本文希望從程序的語義信息出發，結合程序變量的取值情況，使用模板形式表達出變量之間存在的約束關系。而模板變量的系數則從程序中提取得到。這樣可以自動地尋找程序中最有可能存在的不變式約束關系，適應具體程序的語義特點，不需要用戶來指定模板的形式。但這種表達可能不是精確的，也可能是錯誤的，因而需要驗證其真假，驗證的過程可以由定理證明器完成，也可以在計算不動點時根據程序的狀態在抽象域上求解模板約束關系是否可滿足。

這些啟發式生成的循環不變式是根據從程序中提取到的信息按照生成規則得到的，這些信息包括要驗證的程序規范、程序中的屬性斷言、程序變量操作的方式、程序變量可能的系數、程序變量的取值范圍等。因此，如果可以進行更加細節的操作分類，提出更多的模板生成規則，則可以發現更多的不變式。

目前定義的生成規則主要從以下方面考慮：

(1)根據預定義謂詞生成，判斷某組變量是否可以使得該謂詞屬性成立，判斷由定理證明器判斷，這些謂詞一般是比較簡單的屬性，如判斷某個變量取值是否單調變化、數組中的元素是否相等；這里判斷的變量類型必須是和謂詞中的變量類型相兼容的。

(2)被調用函數是否有函數規范，如果有將相應的參數變量應用于規范中的謂詞中，則得到被調用函數的操作結果。如果沒有函數規范，則忽略函數調用。被調用函數的函數規范是其后置條件，表達了調用它對變量產生的“影響”，是函數具體內容的一種摘要表示。因此，這里的分析是一種使用了函數摘要的半過程間的分析。

(3)收集程序中的常量信息，主要是函數規范中、循環后斷言和條件判斷中的常量。

(4)根據從循環體內、循環后的 assert語句和其他分支判斷條件收集到的變量和變量的系數信息，生成變量間可能的模板約束關系。如果分析關注的變量集Var，個數為N；對于長度T的模板，即從Var中選擇T個變量組成模板。但有的抽象域限制系數值和變量數量，如八邊形域中限制變量系數只能為1、0或者?1，限制模板變量數量為2。

當生成模板時，從Var中選擇指定數量的變量作為模板變量，枚舉選定的模板變量的所有系數組合，對于系數不為0的變量，累加其最大值(最小值)的和。生成的模板具有如下形式：

其中，op ∈{＞,≥,==,!=},ci∈ coefv,c∈Const∪{m in,m ax}，cofv是變量v的候選系數集合，Const是收集到的常數值集合，min、max分別是選定的系數不為0的模板變量的最小值、最大值。

3.3 優化措施

從分析處理的范圍和方法可知，分析驗證的復雜度不僅與程序規模有關，更與要分析的變量個數、模板中變量的個數、每個模板變量候選的系數個數有關。在模板大小一定時，當程序規模較大、要分析的變量增多時，需要驗證的情況急劇增加；而增大模板尺寸時，需要驗證的情況也會急劇增加。如果有N個變量，每個Vair變量有ni個候選的系數，提取到C個常數，由之前的模板生成規則，如果模板里面最多可以含有T個變量(即模板尺寸為T)，則最多需要枚舉驗證種情況，可以看出其具有較高的復雜度，因此為了使分析過程及時有效地終止，需要執行一些剪枝優化策略，以壓縮要分析驗證的不變式數量，本文采用的策略如下：

(1)控制關注的變量數量。分析時不分析過程中所有的變量，只分析當前循環中使用的變量、循環后條件中的變量，除此之外的變量與當前循環的關聯性較弱。忽略不能處理的數據類型(如結構體)變量。當有循環嵌套時，該策略避免了大量的重復分析。從其復雜度公式可以看出，減小分析的變量數量可以縮減模板數量。

(2)限制模板尺寸T。當T增大時(T＜N /2)，C隨之增大。驗證者可以指定模板的尺寸，例如這里默認設定為3，即模板中最多含有 3個變量。從其復雜度公式可以看出，減小模板尺寸可以縮減模板數量。

(3)屏蔽指針本身的分析，只關注指針指向變量的值即指針引用。忽略非標準數據類型，如結構體、枚舉等類型變量。將數組元素和一般標量變量的操作區分開來，不放在同一個模板中。這樣可以減少候選的不變式模板個數。

(4)使用改進的搜索策略。基本的思想是：如果I＞0成立，則I ≥0一定成立，不需要再驗證，而且它是冗余的，只需要返回I＞0即可；如果I＞0成立，則I≤0一定不成立，它們是互斥的。判斷過程如下。

(5)在生成模板時，首先執行依賴分析，判斷變量之間是否有依賴關系(包括數據依賴和控制依賴)，不存在依賴關系時認為它們之間聯系較弱，不應該一同構成循環不變式。

4 實現與實驗結果

4.1 loopInv設計與實現

本文基于Frama-C平臺和APRON庫對上述方法做了實現，作為一個插件 loopInv集成在 Frama-C中。其在Frama-C的位置和處理流程如圖1所示，其內部結構如圖2所示。

圖1 loopInv分析框架

圖2 loopInv框架設計

預處理階段完成的工作有：收集要驗證的函數規范、數組變量信息、循環中的分支條件和其后的斷言條件集合、程序中的常量信息、模板變量的候選系數集合、循環中賦值語句的路徑約束條件等信息。在生成轉換系統時，循環中加入模板約束表達式。驗證時使用 WP插件和 APRON庫可滿足性求解。

4.2 實驗結果

實驗中選取了2組程序進行分析，評估loopInv的有效性。一組是簡單的示例程序，對于這類程序同時用其他不變式生成工具進行分析，或分析符合工具特定要求的與之等價的程序，和loopInv對比實驗結果，這里使用的對比工具是invGen[8]和gin-pink[16]；這些程序來自其他文獻，或出自 WP的測試程序，先將手工書寫的循環不變式去除；另一部分是規模較大的實際的開源C程序，由于對比工具或者還不能處理這樣規模的程序，或者進行等價轉換工作量較大，不再進行對比分析，這里側重關注發現的不變式數量，不再驗證函數規范。

選用的測試對象如表1、表2所示。這里變量個數是指作為模板變量的變量數量。

表1 測試程序1

表2 測試程序2

分別設定模板尺寸為 2和 3，得到的實驗結果分別如表3和表4所示。其中，列C1～C8分別表示程序編號、輸出不變式個數、實際正確不變式個數、錯誤不變式個數、經分析后程序是否得到證明、分析執行時間(s)、總的執行時間(即包含驗證不變式時間，時:分:秒)、峰值內存(MB)。

表3 loopInv實驗結果統計1

表4 loopInv實驗結果統計2

同時，選擇工具invGen和gin-pink對程序1～程序6進行不變式分析，得到的結果如表 5所示。其中，列Ca～Ce分別表示程序編號、輸出不變式個數、程序是否得證、總的執行時間(分:秒)、峰值內存(MB)；各個統計項的第 1列是 invGen的分析結果，第 2列是 gin-pink的分析結果，gin-pink輸出不變式個數一列中，括號外表示候選的不變式個數，括號內表示正確的不變式個數。

表5 其他工具分析結果統計

從實驗結果可以看出，通過分析，多數函數規范得到了驗證，說明分析過程是有效的；模板尺寸的變大時生成的不變式數量急劇增多，這能夠發現更多的循環不變式，但同時求解所需要的時間和空間都發生了增長，特別是求解時間增長很快；而實驗結果也表明，設定較小的模板尺寸時，得到的不變式分析結果也可以滿足多數驗證的需求；求解需要的時間和空間不僅與程序規模陒關，更加與程序本身的操作方式陒關。當程序變量數量較多、操作變化靈活、程序結構變化復雜、變量中含有數組等類型時，需要分析的情況增多，分析的難度也隨之上升；陒比invGen和gin-pink，loopInv具有更好的適應性和有效性。

5 結束語

針對當前自動生成循環不變式方法存在的一些局限性，本文綜合考慮函數規范、循環本身、循環后操作等信息，提出一種基于條件賦值轉換和自適應模板生成技術的生成方法，并設計實現了一個Frama-C的插件loopInv。實驗結果表明，該方法具有良好的適應性，能夠使得實驗中的大部分程序驗證過程順利完成。今后需要在細化分析程序操作的基礎上，進一步完善不變式生成規則，同時優化分析過程，以適應更大規模的程序。

[1]Jung Y,Kong S,Wang B,et al.Deriving Invariants by Algorithmic Learning,Decision Procedures,and Predicate Abstraction[C]//Proc.of the 11th International Conference on Verification,Model Checking,and Abstract Interpretation.Madrid,Spain: Springer,2010.

[2]Gopan D,Reps T W.Lookahead Widening[C]//Proc.of the 18th International Conference on Computer Aided Verification.Seattle,USA: Springer,2006.

[3]Bradley A R,Manna Z,Sipma H B.Linear Ranking with Reachability[C]//Proc.of the 17th International Conference on Computer Aided Verification.Edinburgh,UK: Springer,2005.

[4]Gulwani S,Srivastava S,Venkatesan R.Program Analysis as Constraint Solving[C]//Proc.of ACM SIGPLAN Conference on Programming Language Design and Implementation.Tucson,USA: ACM Press,2008.

[5]Kapur D.Automatically Generating Loop Invariants Using Quantifier Elimination[J].Deduction and Applications,2006,64(1): 54-75.

[6]Monniaux D.A Quantifier Elimination Algorithm for Linear Real Arithmetic[C]//Proc.of the 15th International Conference on Logic for Programming,Artificial Intelligence,and Reasoning.Doha,Qatar: Springer,2008.

[7]Bradley A R,Manna Z.Property-directed Incremental Invariant Generation[J].Formal Aspects of Computing,2008,20(4):379-405.

[8]Gupta A,Rybalchenko A.InvGen: An Efficient Invariant Generator[C]//Proc.of the 21th International Conference on Computer Aided Verification.Grenoble,France: Springer,2009.

[9]Hart T E,Ku K,Gurfinkel A,et al.Ptyasm: Software Model Checking with Proof Templates[C]//Proc.of the 23th IEEE/ACM International Conference on Automated Software Engineering.L'Aquila,Italy: IEEE Press,2008.

[10]Podelski A,Rybalchenko A.A Complete Method for the Synthesis of Linear Ranking Functions[C]//Proc.of the 5th International Conference on Verification,Model Checking,and Abstract Interpretation.Venice,Italy: Springer,2004.

[11]Lalire G,Argoud M,Jeannet B.Interproc[EB/OL].(2008-10-21).http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html.

[12]Moy Y,Marché C.Modular Inference of Subprogram Contracts for Safety Checking[J].Journal of Symbolic Computation,2010,45(11): 1184-1211.

[13]邢建英,李夢君,李舟軍.CILinear: 一個陑性不變式自動構造工具[J].計算機科學,2010,37(12): 91-95.

[14]Jung Y,Kong S,David C,et al.Automatically Inferring Loop Invariants via Algorithmic Learning[C]//Proc.of MSCS’12.[S.1.]: IEEE Press,2012.

[15]Ernst M D,Perkins J H,Guo P J,et al.The Daikon System for Dynamic Detection of Likely Invariants[J].Science of Computer Programming,2007,69(1-3): 35-45.

[16]Furia C A,Meyer B.Inferring Loop Invariants Using Postconditions[M].Berlin,Germany: Springer [s.n.],2010.

[17]Sharma R,Dillig I,Dillig T,et al.Simplifying Loop Invariant Generation Using Splitter Predicates[C]//Proc.of the 23th International Conference on Computer Aided Verification.Cliff Lodge,USA: Springer,2011.

[18]Kovács L,Voronkov A.Finding Loop Invariants for Programs over Arrays Using a Theorem Prover[C]//Proc.of the 12th International Conference on Fundamental Approaches to Software Engineering.York,UK: Springer,2009.