基于分段執行和摘要的動態程序分析

摘 要:傳統的動態程序分析需探索程序運行的所有可能路徑。然而，實際的程序通常有大量甚至無限多的路徑。由于不能完全探索所有路徑，對程序的準確分析只限于一些簡單的情形。具體符號測試方法結合符號分析和通過運行程序獲得變量的具體數值。它提高了傳統方法的適用性，但同樣受到路徑數目的限制。為解決這一問題，提出基于分段執行程序和對程序段落自動生成摘要的手段。該手段擴展了具體符號測試，提高其效率，并使之可應用于一些具有無限路徑的程序。

關鍵詞:程序設計; 動態程序分析; 路徑探索; 具體符號測試

中圖分類號:TP311文獻標志碼:A

文章編號:1001-3695(2010)06-2130-04

doi:10.3969/j.issn.1001-3695.2010.06.039

Dynamic program analysis based on partitioning and summarization

FENG Huining

(Oracle Corporation， Redwood Shores， CA， USA)

Abstract:Traditional dynamic program analysis relies on exploring all possible paths of program execution. In reality， however， programs have a large number of， or even infinitely many， paths. Since it is not feasible to explore all paths， precise analysis is limited to simple cases. Concolic testing method combines symbolic analysis and concrete values of variables obtained by executing programs. Though it improves applicability of traditional approaches， concolic testing is still limited by the number of explorable paths. To address this problem， this paper proposed a method here based on executing partitions of a program and automatically generating summaries for those partitions. This method extends concolic testing， improving its performance and making it applicable to certain programs with unbounded paths.

Key words:programming; dynamic program analysis; path exploration; concolic testing

動態程序分析是指通過運行程序來分析它的行為，從而總結屬性或發現存在的錯誤。動態程序分析通常依靠探索程序運行的所有路徑。一個簡單的做法是隨機產生輸入數據并觀察程序對這些輸入返回的結果[1]。若程序對特定的輸入表現出與需求相悖的行為，可認為該輸入暴露了程序的錯誤。若程序對大量隨機輸入產生的結果滿足一定的性質，如輸出值總在有效范圍內，則認為程序對所有輸入都具備此屬性[2]。

簡單分析方法存在不足之處。對于稍為復雜的程序，輸入數據的選取十分困難。一方面，冗余的輸入無助于探索更多的路徑;另一方面，某些路徑的選取取決于特定的輸入，而這些輸入被隨機產生的幾率極小。而且在最壞情況下，路徑數目隨程序中的條件判斷個數呈指數增長，這更使盲目的路徑探索變得不切實際。

有界徹底測試(bounded exhaustive testing， BET)改進了隨機產生輸入數據的方法[3，4]。它通過用戶提供的說明來產生不同的輸入數據。這一方法在實際應用中的不足在于需要額外的說明因而增加用戶的負擔，并可能因為說明不夠準確而導致路徑的遺漏。

具體符號測試(concolic testing)[5]運用可滿足性問題解決器(SAT solver)來探索程序的路徑。使用此方法可保證每次選取的輸入數據必使程序運行經過一條未被探索的路徑，由此冗余輸入數據和低概率輸入數據的問題都得到了解決。此外，具體符號測試無須任何用戶輸入即可自動完成對程序的分析。

然而具體符號測試并不能有效減少路徑的數目，這使它的實際應用受到了限制。本文提出分段執行和自動生成摘要的方法。作為對具體符號測試的擴展，這一方法可大大減小需要探索的路徑數目，在最好情況下使路徑數目隨條件判斷個數呈線性增長。另外，這一方法也可用于分析某些路徑數目無限的程序，而傳統動態程序分析方法和單純的具體符號測試則不能做到。

1 動態程序分析背景

早在1969年，Hoare[6]提出了霍爾邏輯，用于推導程序的屬性。他用{P}S{Q}表示一項關于程序S的屬性，即若條件P成立，則經過運行S以后條件Q成立。若已知S和Q，P可由一系列規則推導出。

受這一思想啟發，麻省理工學院的程序分析組開發了Daikon以及后來的Agitator，用于驗證關于程序屬性的不變式[7，8]。Daikon對程序的分析可產生誤確認結果(由于探索程序不可能選取的路徑而誤報程序錯誤)和誤否認結果(由于探索路徑不足而認為錯誤不會發生)。另一程序分析工具Korat利用程序員手工輸入的不變式來驗證程序[9]。基于程序員提供的不變式正確這一假設，該工具用定理證明的方法推導程序的屬性。然而在實際應用中，程序員提供的不變式常常存在錯誤或因條件太弱無法驗證所需結果。提供這些額外信息也使程序員的工作量大增。修改程序以后，不變式也必須及時地更新。

具體符號測試由Koushik Sen提出。CUTE和jCUTE[10]是分別為C和Java語言實現該測試的工具。這一研究發現使動態程序分析可以自動化地廣泛應用于大量的程序，而無須程序員的干預。

2 具體符號測試

具體符號測試的主要思想是盡量使用符號分析來計算程序經過不同路徑的條件，但遇到符號分析不能解決的問題時，代入具體數值簡化問題。

2.1 示例

考慮以下條件判斷例子中的f函數。例子使用Java語言的語法，但下文關于動態程序分析的討論適用于其他命令式編程語言。f函數中有4個獨立的條件判斷語句，因此路徑總數為24=16。進行具體符號測試時，首先為4個參數選取隨機數值，設分別為1~4。用這些值作為輸入運行程序，得到的結果是“Branch 4”和一個錯誤。自動加入到程序中的額外代碼記錄，這一次運行經過所有4個條件測試，并且只有條件4得到滿足。因此，這一次程序運行的路徑可以標志為[F，F，F，T]。

條件判斷例子如下:

public class A {

void f(int opi， int op2， int op3， int op4) {

if (opl*op2==100) { // 條件1

System.out.println(\"Branch 1\");

}

if (op2==10) {//條件2

System.out.println(\"Branch 2\");

}

if (op3==24) { //條件3

System.out.println(\"Branch 3\");

}

if (op4!=100) {//條件4

System.out.println(\"Branch 4\");

throw new Failure();//產生錯誤

}

}

}

下一步筆者試圖通過改變參數來逼使程序采用不同的路徑。運用深度搜索算法，首先改變的是最后一個條件判斷。為得到標志為[F，F，F，T]的路徑，須找到滿足如下邏輯表達式的參數:

op1 * op2 != 100 op2 != 10

op3 != 24 op4 == 100

一些邏輯表達式可以使用現有的工具求解，如可滿足性問題解決器和整數規劃工具。這些工具返回的結果包括表達式可否成立，以及在可成立的情況下至少一組使之成立的參數值。用這些值作為輸入即可使程序按預定的路徑執行。

對于不能輕易求解的表達式，具體符號測試使用的折中辦法是代入具體數據，使表達式變得簡單。假設現有的工具不能求解以上表達式，當將op1換成上次運行的具體數值1，該工具就可以求解。為了得到參數的具體數值，必須為程序增加額外的代碼，將運行過程中出現的數值記錄到外部文件。這些代碼可以通過自動修改程序的方法加入。

在測試[F，F，F，F]路徑后可以選擇[F，F，T，F]，然后是[F，F，T，T]等。由于每次選取路徑后程序將單獨運行，也可以同時選取一定數量的路徑，讓程序的多個實例同步運行以提高速度。

具體符號測試方法與現有的其他輸入數據選取方法相比，有保證路徑不被重復探索、無須程序員提供額外信息等優點。此外，對于需要特定輸入才能到達的路徑，如上例中條件2為真時的多條路徑，用隨機方法容易遺漏，而這些路徑往往是程序的錯誤所在，這些路徑用具體符號測試就可以探索到。

2.2 存在的問題

具體符號測試依賴可滿足性問題解決器獲取令邏輯表達式為真的參數值。對于用現有工具不能求解的表達式采取代入具體數值的辦法。代入具體數值會降低分析的準確性，產生誤確認或誤否認的結果。然而通過優化，合理選取代入的數值，這一不足在一定程度上可以彌補。

具體符號測試的另一個不足在于不能有效地降低路徑的數目。在圖條件判斷例子的程序中共有16條路徑，因此需要找出除第一條路徑以外的15條路徑，亦即要為15個邏輯表達式求解。在實際應用中，探索所有按指數級增長的路徑并不可行，因此必須為減少路徑找到一個可行的方法，以提高具體符號測試的實用性。

2.3 解決問題思路

具體符號測試中遇到路徑數目過多而不能逐一探索的問題，可以通過分解程序為較小的段落來解決。假設程序有n個分支，那么如上所述，路徑數目為2n。然而，試想將程序分割成m個段落，使每個段落有n/m個分支，再分別對每個段落進行分析，那么總共需要探索m×2n/m條路徑。在極端情形下，若令m=2，則路徑數目為2n。顯然，這一數目隨n線性遞增，而遠遠小于2n。

基于以上思想，對具體符號測試的改進著重在兩個方面:a)將程序分段并探索每個段落中的所有路徑;b)將段落分析的結果加以總結，生成概括段落屬性的摘要，再將這些摘要應用于對程序整體的分析。

3 分段執行與自動生成摘要

具體符號測試的一大優點是便于用戶分析普通程序而無須提供額外信息或人工干預。jCUTE工具可自動為用戶找出Java程序中的所有路徑并逐一加以探索。出現錯誤的路徑將被記錄下來。

作為對具體符號測試的擴展，分段執行和摘要的設計與實現必須保持原方法的優點，因此必須滿足自動化的要求。

3.1 條件判斷的處理

以條件判斷例子的程序為例說明分段執行和摘要的過程。設分析目的是確定不同的輸入參數是否會引起Failure錯誤，以及當答案為肯定時，什么參數會引起該錯誤。對其他屬性的分析可依此類推。可以看出，在這個簡化的例子中，Failure產生當且僅當op4不等于100。實際程序常常比這復雜，并可能包含程序員不能預見的分支(如將條件1改為op1 / op2 == 100時產生的一個除零分支)。

表1示范由下而上對程序分析的過程。

表1 分段執行條件判斷例子的過程

步驟程序段落步驟程序段落

(a)if(op4!=100) {//條件4

System.out.println(\"Branch 4\");

@Failure (\"true\") int_C1_;

}(c)if(op2==10) {//條件2

System.out.println(\"Branch 2\");

}

@Failure (\"op4!=100\") int_C1_;

(b)if(op3!==24) {//條件3

System.out.println(\"Branch 3\");

}

@Failure (\"op4!=100\") int_C1_;

(d)if(op1*op2==10) {//條件1

System.out.println(\"Branch 1\");

}

@Failure (\"op4!=100\") int_C1_;

選取表示錯誤產生條件的邏輯表達式作為段落的摘要。在分析初始時，原程序中的錯誤產生語句:

throw new Failure();

被自動替換成

@Failure(\"true\") int _C1_;

后者是一個帶有標注的作為占位符的變量。筆者僅關心標注附帶的參數。它記錄錯誤發生的條件，而該條件初始化為true，表明程序執行到此處錯誤必然發生。

將錯誤產生語句替換后，第一步是分析距離錯誤最近的程序段落。在此設定一個段落為單個條件判斷語句或函數本身。(在實際應用中，段落設定可采取更粗粒度，如多個嵌套的條件判斷。)表1中(a)是第一個段落，它對應標注外層的條件判斷，以及分支內的代碼。

用具體符號測試的方法分析表1中(a)的段落，可以探索到取決于op4是否等于100的兩條路徑。對路徑的分析得出該段落的錯誤條件為

op4 != 100 true

得到這一結果的原因是，當op4等于100時，程序的運行并沒有經過標注“@Failure”的語句，因此錯誤并不發生;當op4不等于100時，帶有該標注的語句被執行，而標注的參數為true。

將摘要簡化后，第一步中分析過的程序段落就可以被替換成新的標注，得到第二個段落，如表1中(b)所示。對該段落實施具體符號測試可得到如下的錯誤條件:

op3 == 24 op4 != 100 | |

op3 != 24 op4 != 100

簡化后得到

op4 != 100

同理，經過第三、第四步，得到的錯誤條件經簡化后仍為op4 != 100。在每一步中，上一次獲得的錯誤條件取代之前的段落，用來分析下一個段落的錯誤條件。此后，分析到達函數首部，而得到的錯誤條件就是整個函數的錯誤條件。

使用此方法，每步所需探索的路徑數目為2，因而總路徑數目為2×4=8。這一數目隨條件判斷個數呈線性增長。

3.2 循環分解

上例展示了分析一個簡單程序的過程。這一程序沒有循環，而在實際應用中，對循環的處理必不可少。

以下程序是一個結構上較為復雜的例子，它發生錯誤的條件是“x>0 y == z”。要使用動態程序分析的方法自動得出以上結論，必須對循環進行分解，使之變成易于處理的條件判斷。

public class A {

float g(int x， int y， int z) {

float f=1.0f;

for (int i=0; i

if (y==z) {

throw new Failure();

} else {

f+=f/(y-z);

}

}

return f;

}

}

分析過程表2所示。

表2 分斷執行上述一個結構上較為復雜的例子的過程

步驟程序段落步驟程序段落

(a)if(y==z) {

@Failure (\"true\")int_C1_;

} else {

f+=f/(y-z);

}(c)if(i

i++;

@Failure (\"i

}

(b)if(i

@Failure (\"y==z\")int_C1_;

i++;

}

(d)f=1.0f;

i=0;

@Failure (\"i

第一步仍然是將產生錯誤的語句替換為

@Failure(\"true\") int _C1_;

這一步所關注的段落為最內層的條件判斷，得到的錯誤條件為y == z。

第二步，將最內層的條件判斷替換為

@Failure(\"y == z\") int _C1_;

并將外層的循環改為條件判斷。對循環變量的遞增則在條件判斷為真時最后發生。如表2中(b)，修改后的段落對應循環最多只執行一次的情況。經過分析此段落可得出，當循環最多執行一次時的錯誤條件為

i < x y == z

第三步是再次展開循環，以獲得循環最多運行兩次的錯誤條件。表2中(c)的段落是將循環分解為兩層嵌套的條件判斷，并將已經得出的錯誤條件代入到相應位置的結果。第一個“@Failure”語句對應循環的第一次執行。所執行的運算是循環中的條件判斷，其錯誤條件已在第一步中取得。第二個“@Failure”語句對應循環再執行最多一次，其錯誤條件在第二步得出。以上兩個語句之間的“i++;”模仿循環對變量的更新。對表2中(c)分析可知錯誤條件為

i < x (y == z | | i + 1 < x y == z)

簡化后的結果仍為

i < x y == z

經過第三步，可以認定循環本身(不包括對i的初始賦值)的錯誤條件為“i < x y == z”。這是因為將循環展開兩次得到的錯誤條件等于將循環展開一次的錯誤條件。從后面的定理可知，即使將循環展開更多的次數，得到的段落與表2中(c)將會一樣，而錯誤條件也不再改變。

分析完成例子程序中惟一循環后，可以將錯誤條件代入余下的程序中，得到表2中(d)的段落。分析這一段落的結果為x > 0 y == z。由于已經到達函數首部，分段分析即告完成。

從上例可以看出，對循環的處理是基于將循環逐層分解為條件判斷與變量更新。每一次分解可使用前面步驟中得到的錯誤條件簡化分析。當某一步驟中得到的錯誤條件與前一步驟相同時，即就可認定它是整個循環的錯誤條件，從而用它替換循環本身。

3.3 對無限路徑的分析

上例中的分析還顯示出分段執行和摘要方法的另一個優點，即可用于處理一些具有無限路徑的程序。3.2節中一個結構上較為復雜的例子中的程序理論上有無限數目的路徑，因為參數x可以是任意整數，而循環的次數由x決定。即使考慮Java語言定義的整數上限，路徑數目也是十分巨大而不能逐一探索。對于這樣的程序，不能使用單純的具體符號方法。

在表2的分析過程中，循環被逐次分解為條件判斷，但當錯誤條件不再變化時對循環的分析即告終止。對某些程序，這一情況可在有限步數內發生。分段執行和摘要可以處理這類具有無限路徑的程序。

3.4 對循環分解的理論分析

以下的定理為循環的分析提供理論依據。為方便討論，令C(m)和C(n)分別為將循環分解m次和n次得到的錯誤條件。

定理1 若m

因為C(m)對應循環最多執行m次的錯誤條件，而C(n)對應循環最多執行n次的錯誤條件，顯然，當m

定理2 C是從自然數集合到邏輯表達式集合的連續函數。

取任意自然數子集M。M的最小上界sup(M)為其中最大的自然數或∞。若sup(M)=∞，因為

C(∞)=∑∞m=0C(m)

可得C(sup(M))=sup(C(M))。其中∑∞m=0C(m)表示將所有C(m)進行“或”操作以后的結果。若sup(M)<∞，則有

C(sup(M))=C(max(M))=

∑max(M)m=0C(m)=sup(C(M))

總結以上兩種情況可知C(sup(M))=sup(C(M))總得到滿足，因此C是連續函數。

定理3 對循環的分解分析過程存在最小不動點。到達該不動點后，繼續對循環分解得到的錯誤條件不變。

定理3由定理2和Kleene不動點定理可證[11]。

值得注意的是，定理3并未保證最小不動點可在有限步驟內取得。事實上，對于某些循環，不能在有限時間內完成分析并獲得最強的錯誤條件，對此須使用折中的辦法，例如限定在若干步數后強制消除對一個或多個變量的約束，減弱錯誤條件。由于變量個數有限，這一方法可以保證在有限步數內到達不動點，但該不動點不一定最小。對循環的分析可能因此產生誤確認的結果(如前所述，由于探索程序不可能選取的路徑而誤報程序錯誤)。實際應用中，誤確認對分析結果的影響通常比誤否認容易處理，可由程序員手工剔除。

4 實現

結合分段執行和摘要的具體符號測試在Eclipse集成環境中實現。同樣的技術也可應用于其他開發環境和工具。

在Eclipse上實現的一個優點是方便程序員在編寫程序時調用分析工具，再即時得到反饋到程序中的分析結果。另外，程序員還可以選擇對部分程序進行分析，從而加快速度。

軟件的設計主要包括Eclipse插件、jCUTE和可更換的可滿足性問題解決器三個模塊。其中，Eclipse插件提供與用戶交互的界面和總控其他模塊。當收到動態分析請求時，它自動將程序分段，并對每一段落調用jCUTE。

jCUTE對給定的程序段落進行具體符號測試。具體做法是，jCUTE自動插入額外代碼到段落中，然后對給定的一組參數(第一次的輸入數據為隨機產生)運行程序，并實時記錄變量值的改變。在運行結束時，jCUTE返回所選路徑的標志、錯誤條件和變量在程序不同位置的值。

Eclipse插件從jCUTE獲取返回信息后，用深度搜索的辦法尋找下一條不同的路徑。它首先產生一個邏輯表達式。當該表達式滿足時，程序將按預定的路徑運行;然后，Eclipse插件調用可滿足性問題解決器嘗試獲取使表達式滿足的參數組合。在當前實現中選用lpsolve，但理論上可使用任意的可滿足性問題解決器。如表達式可解，Eclipse插件獲取參數的值，將這些值作為下一次段落分析的輸入，再次調用jCUTE;否則，表達式中的一些變量會被它們上次運行時的具體數值代替，以簡化表達式。若因為代入具體數值令表達式不能滿足，那么Eclipse插件將拋棄當前路徑，另選其他路徑。(這可能引起誤否認的結果，但選用功能更強大的可滿足性問題解決器可減少這種情況的出現。)

每次對段落所有路徑探索完畢后，Eclipse插件總結這些路徑的錯誤條件并將它們簡化。簡化后的結果即為段落本身的錯誤條件。此后，Eclipse插件將錯誤條件代入原程序，產生下一個段落，并繼續以同樣的方法分析。這一過程持續至整個函數或用戶選擇的部分分析結束。

圖1顯示使用Eclipse插件時的界面。通過上下文菜單，程序員可以輕易地調用分析工具，而分析的結果則通過標注的形式插入到程序相應的位置。這樣用戶可以考察程序各處產生錯誤的條件，發現潛在的問題。

5 結束語

與傳統動態程序分析方法相比，具體符號測試可以自動而且準確地探索程序運行的不同路徑，包括隨機輸入數據不易觸發的路徑。然而與傳統方法相同的是，具體符號測試并不能有效減小需要探索的路徑數目，而這一數目隨程序中的條件判斷個數呈指數增長。

分段執行和摘要彌補了具體符號測試的不足。通過將程序分段并對每個段落分別進行測試，每次處理的條件判斷個數得到減小，而路徑數目也因此減小。對段落測試的結果經簡化后成為段落的摘要。段落摘要可用于簡化程序，降低以后分析的復雜度。在最好情況下，復雜度從原來的2n降低到2n(n為條件判斷個數)。這一情況在每個段落僅包含一個條件判斷和對摘要簡化的工作需時不多的時候出現。實際應用中，段落可包含多個條件判斷，從而避免頻繁調用外部程序(如jCUTE和lpsolve)。若每個段落包含n/m個條件判斷，則復雜度約為m×2n/m。

致謝 感謝加州大學伯克利分校的Koushik Sen教授在項目設計與實現過程中的寶貴意見。

參考文獻:

[1]ERNST M D. Dynamically discovering likely program invariants[D]. Seattle: University of Washington， 2000.

[2]劉磊. 程序分析技術[M]. 北京:機械工業出版社， 2005.

[3]KHURSHID S， MARINOV D. TestEra: a novel framework for automated testing of Java programs[C]//Proc of Automated Software Engineering. Washington DC: IEEE Computer Society， 2001.

[4]SULLIVAN K， YANG Jinlin， COPPIT D， et al. Software assurance by bounded exhaustive testing[C]//Proc of ACM SIGSOFT International Symposium on Software Testing and Analysis. New York: ACM Press， 2004:133-142.

[5]SEN K. Concolic testing[C]//Proc of the 21th IEEE/ACM International Conference on Automated Software Engineering. New York: ACM Press， 2007:571-572.

[6]HOARE C A R. An axiomatic basis for computer programming[J]. Communications of the ACM，1969，12(10): 576-585.

[7]ERNST M D， COCKRELL J， GRISWOLD W G， et al. Dynamically discovering likely program invariants to support program evolution[J]. IEEE Trans on Software Engineering， 2001，27(2):99-123.

[8]BOSHERNITSAN M， DOONG R， SAVOIA A. From Daikon to agitator: lessons and challenges in building a commercial tool for developer testing[C]//Proc of International Symposium on Software Testing and Analysis. New York: ACM Press， 2006:169-180.

[9]BOYAPATI C， KHURSHID S， MARINOV D. Korat: automated testing based on Java predicates[C]//Proc of ACM International Symposium on Software Testing and Analysis. New York: ACM Press，2002:123-133.

[10]SEN K， AGHA G. CUTE and jCUTE: concolic unit testing and explicit path modelchecking tools[C]//Proc of International Conference on Computer Aided Verification. Germany: SpringerVerlag， 2006:419-423.

[11]DAVEY B A， PRIESTLEY H A. Introduction to lattices and order[M]. 2nd ed. Cambridge: Cambridge University Press， 2002.