基于抽象解釋理論的循環邊界計算方法

崔少軒，喻 慎

（南京航空航天大學計算機科學與技術學院，江蘇南京 211100）

在安全關鍵領域有許多硬實時的系統需求。例如航空發動機的控制系統，汽車的防抱死系統，一旦程序未能在有限的時間范圍內完成既定的功能，就可能帶來嚴重的后果。因此，對于諸如此的安全關鍵軟件進行執行時間尤其是最壞執行時間的分析是十分有必要的[1]。為此在一些特定領域出現了許多對程序進行執行時間分析的工具。例如空客公司使用的程序分析工具OTAWA等[2]。但是在程序的執行時間分析過程中需要用戶標注程序的循環邊界。

對程序循環邊界的分析是對程序的循環迭代次數的近似（approximate）。程序的循環邊界用一個二元組（l，u）表示（l表示下界 lower bounds，u 表示上界upper bounds）。為了獲取程序的循環的迭代次數目前主流的方法有兩種。一種是程序編譯階段動態記錄程序循環的迭代次數[3]。雖然使用這種動態方法得到的是程序的實際循環次數，但是顯然這種方法不能考慮程序在所有情況下的循環迭代次數，并且無法實現跨平臺的分析。另一種方法是對程序進行靜態分析，估算程序在運行過程中循環的迭代次數[4]。本文提出的基于抽象解釋的程序循環邊界分析方法屬于靜態分析的方法。相比之前的循環邊界分析方法，結合程序中的控制依賴關系和數據依賴關系對程序進行切片，通過這種方法可以獲取循環變量取值的約束關系因此能夠對依據變量取值范圍進行循環邊界計算的過程進行了改進。

1 相關工作

1.1 程序切片

程序切片技術[5]是一種通過對程序進行分解，只保留與待分析特性相關的程序片段來對程序進行分析的技術。由Mark Weiser在80年代提出，最初程序切片技術主要被用于程序的調試工作[6]。Susan Horwitz等人在文章[7]對程序切片技術的定義為：“對程序的切片得到的程序，一般是由程序中的部分語句和部分判定表達式組成的”。其中的部分語句和表達式是指那些對程序上的某個點p所使用的變量v產生影響的語句和表達式。其中將（p，v）定義為程序的切片準則。

1.2 抽象解釋

在對程序進行靜態分析時為了構造和逼近程序的不動點理論，Patrick Cousot和Radhia Cousot在1977年提出了基于格的抽象解釋理論[8]用于對程序的語義進行可靠近似。程序具體的對象域上的計算稱為程序的操作語義或者指稱語義，描述了對象域上的計算過程[9]。對程序的抽象解釋過程可以描述為通過對待分析程序在抽象域上的計算，使得抽象域上的計算結果盡可能地逼近程序在具體域上的計算結果過程。通過程序在抽象域上的計算結果來獲取真實程序計算結果的某些信息。抽象解釋實際上是通過損失一部分的計算結果的精確程度來取得較高的計算速度。是在計算結果的精度損失和計算時間效率之間的一種平衡。

1.2.1 抽象域

抽象域[10]是指通過一組由計算機可以表示的元素命名為域元素以及基于該元素定義的一系列的操作，稱為域操作，來對具體的程序所進行的抽象刻畫。在抽象解釋的理論基礎上的分析驗證過程都是在程序的抽象域中展開的。作為抽象解釋的理論中的一個核心概念，抽象域的描述要從抽象域的表示（即域元素的描述）和抽象域中的操作，兩方面來考慮。

（1）抽象域的表示：程序的抽象域是一種指對程序的具體域的抽象刻畫。常見的抽象域的表示形式的不同進行分類。例如有使用多項式約束的八邊形抽象域以及使用區間表示的區間抽象域等。

（2）抽象域上的操作：抽象域上的操作是對程序中的具體操作的抽象刻畫。用來描述程序在具體域中的例如賦值操作、條件判斷操作和程序循環執行等操作。

1.2.2 抽象執行

抽象執行（Abstract Executiom，AE）是擴展的抽象解釋的程序分析方法，它基于抽象解釋理論的符號執行方法。在文章[11]中James R.Larus將抽象執行描述為一種在程序執行過程中通用的事件追蹤技術。抽象執行的對象是程序變量的在抽象域中的表達形式。并且與一般的抽象解釋過程不同的是，抽象執行作為一種擴展的抽象執行理論，抽象執行的對象可以是一個單獨的程序片段，而并不強調對整個程序進行。

抽象執行的本質是在抽象域將程序變量的抽象表示形式作為程序變量本身帶入程序進行計算。首先要對程序的變量和程序中的函數操作進行抽象表示，然后抽象域中執行程序的運行過程。

2 邊界分析框架

2.1 程序依賴指導切片

構建程序切片所依據的是程序的切片準則，基于程序中的依賴關系來對程序進行切片的。出于對程序執行時間的目的考慮，切片準則的設定要保留程序中影響程序執行路徑的依賴關系。程序的依賴關系的獲取要對程序的控制流和數據流分析來獲得。構建程序的依賴關系首先要構建程序的數據依賴關系以及程序的控制依賴關系。其中程序的數據依賴關系以及控制依賴關系分別使用程序的控制流程圖和數據依賴圖來描述。

2.1.1 控制依賴

程序的控制依賴關系在程序的控制流程圖（Control Flow Graph，CFG）中體現。程序的控制流程圖是對程序或者一個過程的抽象描述。CFG被描述為一個有向圖G（V，E）。在程序中的每條語句都可以與控制流程圖中的一個節點對應。CFG通過使用節點和邊之間的關系來描述程序執行過程中所有后可能的執行路徑以及每條執行路徑所對應的語句和判定表達式。因而，繪制程序的控制流程圖的依據是程序的邏輯行之間的控制關系。

如表1中依次給出了順序結構、分支結構和循環結構的控制流程圖和控制依賴圖的結構。為了方便表示，可以對程序的節點用0到n的自然數表示。其中程序的入口節點記作0節點，依次標號。

表1 控制依賴關系

由此可以對如下所示示例程序進行控制依賴關系分析，得到程序的控制流程圖和控制依賴圖如圖1和圖2所示：

圖1 控制流程圖

圖2 控制依賴圖

2.1.2 數據依賴

數據依賴是對程序的數據由于程序結構的關系引用已經被程序處理過的數據而產生的數據之間的關聯關系的抽象。程序變量之間的數據依賴[12]關系可以用程序的數據依賴圖（Data Dependence Graph，DDG）來體現。數據依賴圖也是由節點和有向邊描述的有向圖。數據依賴關系有三種：

（1）流依賴或真依賴：是指在某程序點中被賦值的變量在后面的程序點中被重新引用的情況。例如某一程序變量v1，在某一程序點p1被賦值，然后在p1后面的某一程序點p2被另一個變量v2引用。

（2）反依賴:是指某程序點出現過的變量，在該程序點之后的某點被取值發生變化的情況。例如某一程序變量v1，在某一程序點p1被使用，然后在p1后面的某一程序點p2被重新賦值。

（3）輸出依賴：是指某一程序變量在不同的程序點分別被賦值的情況。例如某一程序變量v1，在某一程序點p1被賦值或重新賦值，然后在p1后面的某一程序點p2被重新賦值。

如表2依次給出了三種數據依賴關系的依賴圖的結構：

表2 數據依賴關系

由此，對示例程序的數據依賴關系構造數據依賴圖如圖3所示：

圖3 數據依賴圖

2.1.3 構建程序依賴圖指導切片

根據本文的定義程序的控制依賴關系和數據依賴關系均使用G（V，E）表示。那么可以將程序的控制依賴關系和數據依賴關系在同一個有向圖中表示出來。其中，為了對控制依賴和數據依賴關系進行區分，仍然使用實線表示控制依賴關系，虛線表示數據依賴關系。得到程序的依賴關系圖如圖4所示：

圖4 程序依賴圖

由于對程序的循環邊界問題的分析過程中，只考慮會對循環迭代次數產生影響的程序語句。此類語句在程序依賴圖上體現為包含出度的節點。由此，我們提出刪除有向圖中不包含出度的節點無關節點，以達到程序依賴圖的約簡目的。逐步刪除無關節點后得到約簡后的程序依賴圖如圖5所示：

圖5 約簡程序依賴圖

根據圖5得到約簡后的程序依賴圖中的節點就是與循環迭代次數相關的程序語句。因此得到切片后的程序中保留了原示例程序的2、4、6、7、9、10行代碼。

2.2 抽象表示

在計算程序的循環邊界過程中，變量在抽象域中的描述用區間抽象域表示。其中本文的程序循環邊界分析過程中，只考慮變量取值為整數情況下的程序的邊界值的計算。其中，為了分析方便的考慮，我們定義了一種只包含整數的區間，整數區間的描述形式使用諸如[C1..C2]（其中C1和C2均為整數，且滿足C1..C2）的形式表示從C1到C2的所有整數構成的區間。在 C1、C2為整數，N1、N2為正整數，且滿足 C1..C2，N1..N2的情況下，使用[C1..C2]，N1%N2的形式表示在整數區間[C1..C2]中模N2余N1的整數區間。對于該整數區間抽象域上的操作過程與一般的區間抽象域的四則運算過程類似，描述如下：整數區間的算術算術運算符號是指對取值范圍為整數的區間的表示的變量進行的加（＋*）、減（－*）、乘（×*）、除（/*）的基本操作。其中當空區間⊥參與運算時，運算結果一律為空區間。具體的算術運算定義如下：

例如對于程序中的變量值i，假定變量i的取值范圍為1到100的整數，那么i的取值范圍的抽象表示為[1..100]。當i在程序中進行四則運算時，映射在抽象域上計算過程即為對區間[1..100]上的四則運算。

2.3 邊界值計算

程序的循環邊界由程序的變量的取值范圍所確定。因而確定的程序的邊界值需要對與循環相關的程序變量的取值范圍進行分析。將程序的控制流程圖和循環變量的取值范圍作為輸入，抽象執行過程通過抽象的執行程序的操作，變量的抽象取值區間進行運算。抽象執行的過程中的運算法則與整數區間的四則運算法則一致。最后輸出程序的循環迭代次數。

在對程序的抽象執行過程中，不難得出程序中循環變量 i和 j的取值為：i=[1..10]，j=[1..10]。傳統的循環邊界計算方法是以及循環變量的取值范圍計算循環邊界[13]。按照這種方法計算得到較為粗糙的循環邊界結果為：10×10=100次。由此推測出該循環結構的循環邊界為（0，100）。顯然這種方法計算結果存在較大的誤差。又由于在本文的分析過程中，可以清晰地獲取程序中的依賴關系，對如下形式的循環代碼，根據程序切片模塊中得到的程序數據依賴信息對程序循環變量的取值進行約束，對循環結構中的外層循環變量i和內層循環變量j建立形如公式（1）所示的約束條件。根據約束條件，使用更加精確的變量取值，得到更加接近實際迭代次數的程序循環邊界。

例如，對示例程序點9所確定的對變量j重新賦值的多項式j=j+2。顯然內層的循環的迭代次數不大于（10-2）/2=5次，且不小于（10-4）/2=3次。對外層結構的循環中循環變量i的多項式為i=i+1，外層循環的迭代次數不大于（10-1）/1=9次，且不小于（10-4）/1=6次。所以該循環結構迭代次數為：[3..5]×*[6..9]=[min（3×6，3×9，5×6，5×9）..max（3×6，3×9，5×6，5×9）]=[18..45]次。相比與之前粗糙的邊界值（0，100），顯然依據本文中提出的方法可以得到的較為精確的程序循環邊界為（l，u）=（18，45）。

3 分析驗證

為了證明本文提出的分析方法的有效性，使用形式化的程序分析工具Frama-C的值分析插件[14]對上述的分析結果進行驗證。使用命令“frama-cvalue slevel 100 example.c”設置循環展開100次后計算得到循環結構中變量i，j的取值，當i和j的取值為“i∈{10}，j∈{11}”時，循環結束。分析可知該循環結構的循環上界必然是不大于100的。進一步，使用命令“frama-c-value slevel 45”，將循環展開的次數設置為45，得到的i和j的取值仍為“i∈{10}，j∈{11}”。由此可見示例函數的循環上界必然不大于45次，將45作為函數的循環上界，比100更加精確。并且在人為將循環變量i和j的值設定為“i=4”，“j=4”之后，使用命令“frama-c-value slevel 18 example.c”，將循環展開的次數設置為18之后，變量 i和 j的計算結果“i∈{10}，i∈{10}”并沒有達到循環結束時的取值。由此可見示例函數的循環下界必然不小于18。所以18可以作為該段循環片段的循環下界比0要更接近實際值。

結果表明使用本文的循環邊界分析方法得到的程序循環下界“l”不大于程序實際迭代的次數，計算得到的循環上界“u”不小于程序的實際迭代次數。證明使用本文所述的循環邊界分析方法得到的（l，u）可以作為有效的邊界。從而驗證了本文提出的方法的有效性。

3 結語

針對程序的循環邊界計算問題，通過對程序中的控制流和數據流分析的來獲取程序中與循環相關的程序語句，來指導程序的切片。并且根據約簡后的依賴關系，可以將縮小循環變量的取值范圍，通過更加精確到取值范圍計算得到更加接近實際循環次數的邊界值。