基于分段執(zhí)行和摘要的動態(tài)程序分析

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

關(guān)鍵詞:程序設(shè)計; 動態(tài)程序分析; 路徑探索; 具體符號測試

中圖分類號:TP311文獻(xiàn)標(biāo)志碼: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

動態(tài)程序分析是指通過運(yùn)行程序來分析它的行為，從而總結(jié)屬性或發(fā)現(xiàn)存在的錯誤。動態(tài)程序分析通常依靠探索程序運(yùn)行的所有路徑。一個簡單的做法是隨機(jī)產(chǎn)生輸入數(shù)據(jù)并觀察程序?qū)@些輸入返回的結(jié)果[1]。若程序?qū)μ囟ǖ妮斎氡憩F(xiàn)出與需求相悖的行為，可認(rèn)為該輸入暴露了程序的錯誤。若程序?qū)Υ罅侩S機(jī)輸入產(chǎn)生的結(jié)果滿足一定的性質(zhì)，如輸出值總在有效范圍內(nèi)，則認(rèn)為程序?qū)λ休斎攵季邆浯藢傩訹2]。

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

有界徹底測試(bounded exhaustive testing， BET)改進(jìn)了隨機(jī)產(chǎn)生輸入數(shù)據(jù)的方法[3，4]。它通過用戶提供的說明來產(chǎn)生不同的輸入數(shù)據(jù)。這一方法在實(shí)際應(yīng)用中的不足在于需要額外的說明因而增加用戶的負(fù)擔(dān)，并可能因?yàn)檎f明不夠準(zhǔn)確而導(dǎo)致路徑的遺漏。

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

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

1 動態(tài)程序分析背景

早在1969年，Hoare[6]提出了霍爾邏輯，用于推導(dǎo)程序的屬性。他用{P}S{Q}表示一項(xiàng)關(guān)于程序S的屬性，即若條件P成立，則經(jīng)過運(yùn)行S以后條件Q成立。若已知S和Q，P可由一系列規(guī)則推導(dǎo)出。

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

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

2 具體符號測試

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

2.1 示例

考慮以下條件判斷例子中的f函數(shù)。例子使用Java語言的語法，但下文關(guān)于動態(tài)程序分析的討論適用于其他命令式編程語言。f函數(shù)中有4個獨(dú)立的條件判斷語句，因此路徑總數(shù)為24=16。進(jìn)行具體符號測試時，首先為4個參數(shù)選取隨機(jī)數(shù)值，設(shè)分別為1~4。用這些值作為輸入運(yùn)行程序，得到的結(jié)果是“Branch 4”和一個錯誤。自動加入到程序中的額外代碼記錄，這一次運(yùn)行經(jīng)過所有4個條件測試，并且只有條件4得到滿足。因此，這一次程序運(yùn)行的路徑可以標(biāo)志為[F，F(xiàn)，F(xiàn)，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();//產(chǎn)生錯誤

}

}

}

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

op1 * op2 != 100 op2 != 10

op3 != 24 op4 == 100

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

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

在測試[F，F(xiàn)，F(xiàn)，F(xiàn)]路徑后可以選擇[F，F(xiàn)，T，F(xiàn)]，然后是[F，F(xiàn)，T，T]等。由于每次選取路徑后程序?qū)为?dú)運(yùn)行，也可以同時選取一定數(shù)量的路徑，讓程序的多個實(shí)例同步運(yùn)行以提高速度。

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

2.2 存在的問題

具體符號測試依賴可滿足性問題解決器獲取令邏輯表達(dá)式為真的參數(shù)值。對于用現(xiàn)有工具不能求解的表達(dá)式采取代入具體數(shù)值的辦法。代入具體數(shù)值會降低分析的準(zhǔn)確性，產(chǎn)生誤確認(rèn)或誤否認(rèn)的結(jié)果。然而通過優(yōu)化，合理選取代入的數(shù)值，這一不足在一定程度上可以彌補(bǔ)。

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

2.3 解決問題思路

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

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

3 分段執(zhí)行與自動生成摘要

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

作為對具體符號測試的擴(kuò)展，分段執(zhí)行和摘要的設(shè)計與實(shí)現(xiàn)必須保持原方法的優(yōu)點(diǎn)，因此必須滿足自動化的要求。

3.1 條件判斷的處理

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

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

表1 分段執(zhí)行條件判斷例子的過程

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

(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_;

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

throw new Failure();

被自動替換成

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

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

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

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

op4 != 100 true

得到這一結(jié)果的原因是，當(dāng)op4等于100時，程序的運(yùn)行并沒有經(jīng)過標(biāo)注“@Failure”的語句，因此錯誤并不發(fā)生;當(dāng)op4不等于100時，帶有該標(biāo)注的語句被執(zhí)行，而標(biāo)注的參數(shù)為true。

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

op3 == 24 op4 != 100 | |

op3 != 24 op4 != 100

簡化后得到

op4 != 100

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

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

3.2 循環(huán)分解

上例展示了分析一個簡單程序的過程。這一程序沒有循環(huán)，而在實(shí)際應(yīng)用中，對循環(huán)的處理必不可少。

以下程序是一個結(jié)構(gòu)上較為復(fù)雜的例子，它發(fā)生錯誤的條件是“x>0 y == z”。要使用動態(tài)程序分析的方法自動得出以上結(jié)論，必須對循環(huán)進(jìn)行分解，使之變成易于處理的條件判斷。

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 分?jǐn)鄨?zhí)行上述一個結(jié)構(gòu)上較為復(fù)雜的例子的過程

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

(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

第一步仍然是將產(chǎn)生錯誤的語句替換為

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

這一步所關(guān)注的段落為最內(nèi)層的條件判斷，得到的錯誤條件為y == z。

第二步，將最內(nèi)層的條件判斷替換為

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

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

i < x y == z

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

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

簡化后的結(jié)果仍為

i < x y == z

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

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

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

3.3 對無限路徑的分析

上例中的分析還顯示出分段執(zhí)行和摘要方法的另一個優(yōu)點(diǎn)，即可用于處理一些具有無限路徑的程序。3.2節(jié)中一個結(jié)構(gòu)上較為復(fù)雜的例子中的程序理論上有無限數(shù)目的路徑，因?yàn)閰?shù)x可以是任意整數(shù)，而循環(huán)的次數(shù)由x決定。即使考慮Java語言定義的整數(shù)上限，路徑數(shù)目也是十分巨大而不能逐一探索。對于這樣的程序，不能使用單純的具體符號方法。

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

3.4 對循環(huán)分解的理論分析

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

定理1 若m

因?yàn)镃(m)對應(yīng)循環(huán)最多執(zhí)行m次的錯誤條件，而C(n)對應(yīng)循環(huán)最多執(zhí)行n次的錯誤條件，顯然，當(dāng)m

定理2 C是從自然數(shù)集合到邏輯表達(dá)式集合的連續(xù)函數(shù)。

取任意自然數(shù)子集M。M的最小上界sup(M)為其中最大的自然數(shù)或∞。若sup(M)=∞，因?yàn)?/p>

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

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

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

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

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

定理3 對循環(huán)的分解分析過程存在最小不動點(diǎn)。到達(dá)該不動點(diǎn)后，繼續(xù)對循環(huán)分解得到的錯誤條件不變。

定理3由定理2和Kleene不動點(diǎn)定理可證[11]。

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

4 實(shí)現(xiàn)

結(jié)合分段執(zhí)行和摘要的具體符號測試在Eclipse集成環(huán)境中實(shí)現(xiàn)。同樣的技術(shù)也可應(yīng)用于其他開發(fā)環(huán)境和工具。

在Eclipse上實(shí)現(xiàn)的一個優(yōu)點(diǎn)是方便程序員在編寫程序時調(diào)用分析工具，再即時得到反饋到程序中的分析結(jié)果。另外，程序員還可以選擇對部分程序進(jìn)行分析，從而加快速度。

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

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

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

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

圖1顯示使用Eclipse插件時的界面。通過上下文菜單，程序員可以輕易地調(diào)用分析工具，而分析的結(jié)果則通過標(biāo)注的形式插入到程序相應(yīng)的位置。這樣用戶可以考察程序各處產(chǎn)生錯誤的條件，發(fā)現(xiàn)潛在的問題。

5 結(jié)束語

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

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

致謝 感謝加州大學(xué)伯克利分校的Koushik Sen教授在項(xiàng)目設(shè)計與實(shí)現(xiàn)過程中的寶貴意見。

參考文獻(xiàn):

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

[2]劉磊. 程序分析技術(shù)[M]. 北京:機(jī)械工業(yè)出版社， 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.