謝章偉，崔展齊，鄭麗偉，張志華

北京信息科技大學(xué) 計(jì)算機(jī)學(xué)院，北京 100101

1 引言

由于軟件缺陷的存在，程序在運(yùn)行過程中可能會(huì)出現(xiàn)一些不正常的行為，輕則造成程序功能異常，重則導(dǎo)致系統(tǒng)崩潰。軟件測(cè)試作為檢測(cè)軟件缺陷的一種重要方法，能夠有效檢測(cè)出程序存在的缺陷，提升軟件的可靠性[1]。符號(hào)執(zhí)行作為一種重要的軟件測(cè)試方法，能夠通過生成高覆蓋率的測(cè)試用例，檢測(cè)隱藏較深的程序錯(cuò)誤。

King 等人[2]于1975 年提出使用符號(hào)執(zhí)行進(jìn)行軟件分析，其基本思想是使用符號(hào)值表示輸入變量，在運(yùn)行程序的過程中逐語句轉(zhuǎn)換成符號(hào)表達(dá)式，收集相應(yīng)的路徑約束條件，并通過約束求解器求得滿足路徑約束條件的測(cè)試用例。當(dāng)時(shí)由于受制于約束求解器求解能力，導(dǎo)致符號(hào)執(zhí)行的路徑覆蓋率遠(yuǎn)小于程序分析方法，使得研究陷入了低谷。隨著現(xiàn)代計(jì)算機(jī)計(jì)算能力的增強(qiáng)，以及研究人員對(duì)于約束求解器的不斷優(yōu)化和改進(jìn)，例如Z3[3]、MathSAT4[4]等性能優(yōu)秀的約束求解器的出現(xiàn)，使得符號(hào)執(zhí)行技術(shù)重新引起研究人員的關(guān)注[5]。常見的符號(hào)執(zhí)行工具有 Symbolic Pathfinder[6]、KLEE[7]、JDart[8]、jCUTE和CUTE[9]等。盡管約束求解器的相關(guān)研究取得了突破性的發(fā)展，但隨著程序規(guī)模和復(fù)雜程度的劇增，約束求解器依舊面臨路徑爆炸、求解能力不足等問題[5，10]。

為此，常亮等人[11]提出采用并行化方法減少符號(hào)執(zhí)行中路徑探索和約束求解耗時(shí)問題，該方法基于Actor模型并行模式，將動(dòng)態(tài)符號(hào)執(zhí)行中的約束求解任務(wù)和路徑探索任務(wù)并行執(zhí)行，減少耗時(shí)代價(jià)；Bryant[12]使用積極算法，將SMT公式轉(zhuǎn)換成一個(gè)CNF型的命題公式，然后使用SAT求解器進(jìn)行求解，通過高效地利用SAT求解器提升SMT的求解效率；Nuzzo[13]則提出使用凸規(guī)劃求解非線性凸的約束條件的可滿足性。雖然上述工作能夠在一定程度上緩解約束求解器求解能力不足的問題，但動(dòng)態(tài)符號(hào)執(zhí)行的覆蓋率仍受限于約束求解器的求解能力。

針對(duì)上述問題，本文提出了一種遺傳算法輔助的動(dòng)態(tài)符號(hào)執(zhí)行測(cè)試方法。首先，通過動(dòng)態(tài)符號(hào)執(zhí)行工具收集約束條件，當(dāng)約束求解器無法求解當(dāng)前約束條件或者求解時(shí)間超時(shí)，使用遺傳算法生成測(cè)試輸入；然后，根據(jù)輸入變量的數(shù)據(jù)類型生成一定數(shù)量的初始種群，通過適應(yīng)度函數(shù)計(jì)算每個(gè)個(gè)體的適應(yīng)度，根據(jù)適應(yīng)度大小剔除適應(yīng)度低的個(gè)體，通過對(duì)篩選之后的個(gè)體進(jìn)行交叉變異和隨機(jī)變異生成新的種群；不斷迭代上述過程，直到生成滿足約束條件的測(cè)試輸入為止。本文基于所提出的方法開發(fā)了原型工具JDart-Ga，并在JDart 提供的測(cè)試用例集上進(jìn)行了實(shí)驗(yàn)。實(shí)驗(yàn)結(jié)果表明，對(duì)于存在JDart無法覆蓋路徑的3 個(gè)實(shí)驗(yàn)對(duì)象，JDart-Ga 的路徑覆蓋率均取得了提升，路徑覆蓋率最低提升了16%，最高提升了23%，同時(shí)測(cè)試時(shí)間增加不超過10%。

本文的主要貢獻(xiàn)包括：

（1）提出了一種遺傳算法輔助的動(dòng)態(tài)符號(hào)執(zhí)行測(cè)試方法，為約束求解器不能有效求解的路徑生成測(cè)試輸入。

（2）基于所提出的方法實(shí)現(xiàn)了原型工具JDart-Ga，并在一組公開的示例程序上進(jìn)行實(shí)驗(yàn)，以驗(yàn)證該方法的有效性。

2 研究背景

2.1 動(dòng)態(tài)符號(hào)執(zhí)行

動(dòng)態(tài)符號(hào)執(zhí)行[14]結(jié)合使用了具體執(zhí)行和符號(hào)執(zhí)行，不再靜態(tài)模擬程序執(zhí)行，而是為程序提供具體的輸入，通過實(shí)際運(yùn)行程序，在程序運(yùn)行中對(duì)程序進(jìn)行動(dòng)態(tài)分析。在動(dòng)態(tài)符號(hào)執(zhí)行的過程中，對(duì)符號(hào)變量相關(guān)的代碼段進(jìn)行符號(hào)執(zhí)行，使用約束求解器求解路徑約束條件，為每條路徑生成一個(gè)測(cè)試用例，將測(cè)試用例輸入并執(zhí)行程序。通常情況下約束求解器有三種返回結(jié)果：如果約束求解器求解返回值為sat，則表示當(dāng)前約束條件有解并已經(jīng)找到某個(gè)合適的解；返回值為unsat，則表示當(dāng)前約束條件無解；但如果返回值為don’t know，則表示約束求解器無法判斷當(dāng)前約束條件是否有解。動(dòng)態(tài)符號(hào)執(zhí)行根據(jù)約束求解器的返回結(jié)果來選擇是否應(yīng)該沿著當(dāng)前路徑繼續(xù)往下探索。

2.2 遺傳算法

遺傳算法由Holland 提出[15]，是一種模擬達(dá)爾文生物進(jìn)化論的自然選擇和遺傳學(xué)機(jī)理的生物進(jìn)化過程的計(jì)算模型，是一種通過模擬自然進(jìn)化過程的全局最優(yōu)搜索方法，近些年來被廣泛運(yùn)用于信息安全[16]、軟件測(cè)試[17]等領(lǐng)域。在達(dá)爾文進(jìn)化論中提到，生物是通過不斷的基因變異來實(shí)現(xiàn)物種的進(jìn)化，而自然選擇主導(dǎo)著進(jìn)化的方向?；蛲蛔兊姆较蚴请S機(jī)性的，自然選擇通過不斷淘汰不適應(yīng)環(huán)境的類型，從而定向地改變種群中的基因向適應(yīng)環(huán)境的方向演化。遺傳算法正是以此為指導(dǎo)思想，通過對(duì)問題的解（稱為個(gè)體）進(jìn)行編碼，表現(xiàn)成染色體形式，通過模擬基因的隨機(jī)突變和交叉變異的方式實(shí)現(xiàn)個(gè)體的進(jìn)化，并使用適應(yīng)度函數(shù)評(píng)估當(dāng)前個(gè)體的適應(yīng)度，根據(jù)適應(yīng)度的高低衡量個(gè)體對(duì)目標(biāo)問題的適應(yīng)度，選擇使用具有高適應(yīng)度的個(gè)體進(jìn)行遺傳，從而增大產(chǎn)生滿足目標(biāo)問題解的概率。

3 遺傳算法輔助的動(dòng)態(tài)符號(hào)執(zhí)行測(cè)試方法

本文提出的方法框架如圖1所示，該方法主要包括兩個(gè)階段，左邊的是動(dòng)態(tài)符號(hào)執(zhí)行階段，右邊是遺傳算法階段。給定一個(gè)程序，首先進(jìn)行動(dòng)態(tài)符號(hào)執(zhí)行測(cè)試，使用動(dòng)態(tài)符號(hào)執(zhí)行工具收集一條路徑上的約束條件，將其傳遞給約束求解器，根據(jù)約束求解器的求解結(jié)果result選擇下一步操作。若求解結(jié)果result為sat或unsat，則直接將結(jié)果返回給動(dòng)態(tài)符號(hào)執(zhí)行工具，若求解結(jié)果result=don’t know或者求解時(shí)間超時(shí)，則嘗試使用遺傳算法生成測(cè)試用例。通過不斷迭代上述過程，以覆蓋更多程序路徑。

圖1 遺傳算法輔助的動(dòng)態(tài)符號(hào)執(zhí)行測(cè)試框架

3.1 動(dòng)態(tài)符號(hào)執(zhí)行

圖2 展示了本文所使用的動(dòng)態(tài)符號(hào)執(zhí)行方法流程。與傳統(tǒng)動(dòng)態(tài)符號(hào)執(zhí)行方法相比，增加了一個(gè)調(diào)用遺傳算法生成測(cè)試輸入的步驟。首先，選擇一個(gè)目標(biāo)程序，收集目標(biāo)程序中的輸入變量并將其符號(hào)化，給定一個(gè)初始輸入并運(yùn)行程序，從而獲得一條路徑約束條件集合。然后按照深度優(yōu)先調(diào)度策略將路徑中的約束取反，獲得一條未覆蓋路徑的約束條件集合，使用約束求解器對(duì)約束條件集合進(jìn)行求解，若約束求解器求解的結(jié)果為don’t know或者求解時(shí)間超時(shí)，則使用遺傳算法嘗試生成下一條路徑的測(cè)試輸入，否則直接將約束求解器的求解結(jié)果傳遞給動(dòng)態(tài)符號(hào)執(zhí)行工具。不斷重復(fù)上述過程，直到所有路徑都遍歷完畢。

圖2 動(dòng)態(tài)符號(hào)執(zhí)行方法流程

3.2 遺傳算法

遺傳算法的優(yōu)點(diǎn)是在搜索過程中不需要關(guān)注問題的內(nèi)在性質(zhì)，對(duì)于目標(biāo)函數(shù)和約束條件，無論是線性的還是非線性的，離散的還是連續(xù)的都可處理。

本文使用遺傳算法對(duì)約束求解器無法求解的約束條件進(jìn)求解，具體的求解過程如算法1所示。算法1的輸入為一條為約束求解器無法求解的路徑約束條件集合constraintsExpr={expr1，expr2，…，expri}，其中，expri表示路徑上的約束條件。輸出為求解結(jié)果result，輸出的求解結(jié)果有兩種，若生成了滿足約束條件集合constraintsExpr的測(cè)試用例，則result=sat和滿足約束條件的測(cè)試輸入，否則返回result=don’t know。在算法1 中，population表示包含一定數(shù)量個(gè)體的初始種群，num表示種群進(jìn)化的最大次數(shù)，size表示每次變異后下一代生存的個(gè)體數(shù)量。

在算法1 中，首先根據(jù)傳入的約束條件集合con-straintsExpr獲取輸入變量的數(shù)據(jù)類型，然后根據(jù)輸入變量的數(shù)據(jù)類型生成一定數(shù)量的種群population，計(jì)算當(dāng)前種群中每個(gè)個(gè)體的適應(yīng)度Fitness，如果當(dāng)前個(gè)體的適應(yīng)度Fitness=0，則說明當(dāng)前個(gè)體為路徑約束條件constraintsExpr中所有約束條件的解，將解返回并結(jié)束。如果不滿足，則根據(jù)適應(yīng)度的大小從小到大進(jìn)行排列，保留排序靠前size的個(gè)體，通過對(duì)個(gè)體染色體進(jìn)行交叉變異和隨機(jī)變異操作，產(chǎn)生新的種群newPopulation，不斷重復(fù)上述過程，直到找到滿足路徑約束條件constraintsExpr的個(gè)體為止。但如果種群進(jìn)化的次數(shù)大于num時(shí)，仍然沒有生成滿足路徑約束條件constraintsExpr的測(cè)試用例時(shí)，出于對(duì)時(shí)間成本的考慮，結(jié)束循環(huán)并返回result=don’t know。

算法1使用遺傳算法生成測(cè)試用例

input：constraintsExpr：路徑約束條件

output：result：求解結(jié)果

1.SymbolicPar=constraintsExpr.containsAl（l）；

2.population=createInitialPopulation（SymbolicPar）；

3.//生成初始種群

4.foreach（evolve（num）） do

5.//進(jìn)化到第num代之后就結(jié)束

6.foreach（chromosome：population）do

7.Fitness=calculate（chromosome）；

8.//計(jì)算每個(gè)個(gè)體的適應(yīng)度

9.i（fFitness==0）then

10.return result；

11.end

12.newPopulation.sortByFitness（population）；

13.//根據(jù)適應(yīng)度大小排序

14.newPopulation.trim（size）；

15.//剔除第population個(gè)之后的所有個(gè)體

16.newPopulation.chromosome.crossove（r）；

17.//交叉變異

18.newPopulation.randomChromosome（）；

19.//隨機(jī)變異

20.population=newPopulation；

21.end

22.end

23.returnresult；

其中，適應(yīng)度函數(shù)是決定是否能成功生成測(cè)試輸入的關(guān)鍵，適應(yīng)度函數(shù)的合理性決定生成測(cè)試用例的效率[18]。由于本文使用遺傳算法求解滿足路徑約束條件的解，故使用公式（1）來評(píng)價(jià)當(dāng)前個(gè)體的適應(yīng)度：

其中，length表示當(dāng)前路徑約束條件集合constraintsExpr中約束條件的個(gè)數(shù)，N表示當(dāng)前個(gè)體滿足路徑約束條件中約束條件的個(gè)數(shù)，N越大，適應(yīng)度的值Fitness越低，說明當(dāng)前個(gè)體越接近滿足路徑約束條件的解。

3.3 示例

以圖3 所示的代碼片段為例，該段代碼來自JDart提供的示例程序double2long。若使用動(dòng)態(tài)符號(hào)執(zhí)行方法，假設(shè)當(dāng)前輸入為x=10.0，則覆蓋路徑的約束條件集合為constraintsExpr={x≥0.0,(sint64)(x/10.0)＜100} ，根據(jù)深度優(yōu)先遍歷策略，將當(dāng)前路徑約束條件集合中的第2個(gè)約束條件取反，則獲得了一條新的路徑約束集合{x≥0.0,(sint64)(x/10.0)≥100} 。此時(shí)約束求解器無法求解該條路徑的約束條件集合，返回的求解結(jié)果為result=don’t know，動(dòng)態(tài)符號(hào)執(zhí)行工具無法覆蓋該條路徑。若使用本文所提出的方法，當(dāng)約束求解器返回result=don’t know時(shí)，將使用遺傳算法生成滿足目標(biāo)路徑約束條件的測(cè)試輸入，將約束條件constraintsExpr={x≥0.0,(sint64)(x/10.0)≥100} 作為參數(shù)傳遞給遺傳算法模塊，求得當(dāng)x=1 000.1 時(shí)，該路徑約束條件有解，則返回result=sat和測(cè)試用例x=1 000.1，從而輔助動(dòng)態(tài)符號(hào)執(zhí)行工具覆蓋上述路徑。

圖3 代碼示例

4 實(shí)驗(yàn)分析

基于上述方法，本文在Java符號(hào)執(zhí)行工具JDart的基礎(chǔ)上，實(shí)現(xiàn)了符號(hào)執(zhí)行工具JDart-Ga。運(yùn)行實(shí)驗(yàn)的軟硬件環(huán)境為Intel?Core?i7-7700HQ處理器，主頻為2.80 GHz，內(nèi)存2 GB，操作系統(tǒng)為Ubuntu 14.04，Sun JRE 1.8（64 bit mode）。

JDart[19]是一個(gè)基于Java PathFinder 框架的符號(hào)執(zhí)行工具。在檢測(cè)Java 程序的過程中，JDart 能夠同時(shí)進(jìn)行具體執(zhí)行和符號(hào)執(zhí)行，并將路徑約束組合起來，形成約束樹。JDart 通過SMT 求解器生成測(cè)試用例，并且嘗試運(yùn)行從而收集未探索分支的路徑，不斷增強(qiáng)約束樹。

在實(shí)驗(yàn)分析中延用了JDart 的路徑分類方式，使用OK PATHS 統(tǒng)計(jì)測(cè)試用例能覆蓋并且不會(huì)觸發(fā)錯(cuò)誤的路徑數(shù)量；使用ERROR PATHS統(tǒng)計(jì)檢測(cè)出存在錯(cuò)誤的路徑數(shù)量，例如斷言或者未捕獲的異常，斷言違規(guī)或未捕獲的異常等；使用DON’T KNOW PATHS 統(tǒng)計(jì)未探索的路徑數(shù)量；使用TOTAL PATHS 統(tǒng)計(jì)總的路徑覆蓋情況，即 TOTAL PATHS 等于 OK PATHS、ERROR PATHS和DON’T KNOW PATHS之和。

4.1 實(shí)驗(yàn)設(shè)計(jì)

為了驗(yàn)證所提出方法的有效性，本文將JDart 所提供的17個(gè)測(cè)試示例全部作為實(shí)驗(yàn)對(duì)象，實(shí)驗(yàn)對(duì)象信息如表1所示。表1中測(cè)試對(duì)象的命名方法為“類名稱_類內(nèi)被測(cè)試方法名稱”。17個(gè)測(cè)試對(duì)象的輸入變量包括int、char、double、long和boolean等數(shù)據(jù)類型。

表1 實(shí)驗(yàn)對(duì)象基本情況

實(shí)驗(yàn)沿用文獻(xiàn)[7]所使用的評(píng)價(jià)方法，使用覆蓋路徑數(shù)量、路徑覆蓋率和測(cè)試的時(shí)間開銷進(jìn)行對(duì)比分析。其中，路徑覆蓋率Cov的計(jì)算公式如公式（2）所示：

在公式（2）中，okPaths和errorPaths分別表示OK PATHS和ERROR PATH 的值，兩者相加表示測(cè)試用例能夠覆蓋的路徑數(shù)量，max{totalPathsJDart,totalPathsJDart-Ga}表示JDart和JDart-Ga中TOTAL PATHS的最大值。

在統(tǒng)計(jì)時(shí)間開銷的過程中，本文規(guī)定測(cè)試單個(gè)程序的時(shí)間上限不超過30 min，超出30 min 則記為超時(shí)，時(shí)間開銷記為30 min，覆蓋的路徑數(shù)量記為30 min內(nèi)覆蓋的路徑。在實(shí)驗(yàn)過程中，本文將遺傳算法中的參數(shù)值分別設(shè)置為：初始種群中的個(gè)體數(shù)population=100，每次進(jìn)化之后下一代生存的個(gè)體數(shù)量size=100，進(jìn)化的次數(shù)num=1 000。

4.2 實(shí)驗(yàn)結(jié)果及分析

在實(shí)驗(yàn)過程中，使用JDart和JDart-Ga分別對(duì)表1中測(cè)試對(duì)象進(jìn)行測(cè)試，并收集了相關(guān)的路徑覆蓋信息，實(shí)驗(yàn)結(jié)果如表2和圖4所示。其中，表2為三種路徑的覆蓋情況，圖4為路徑覆蓋率。從表2中可以看出，當(dāng)DON’T KNOW PATHS為零時(shí)，即表示不存在SMT求解器無法求解的約束條件，所以JDart-Ga 和JDart 覆蓋的OKPATHS、ERROR PATHS 和 TOTALS PATHS 都相等。在17個(gè)測(cè)試對(duì)象中，有11個(gè)測(cè)試對(duì)象不存在SMT求解器無法求解的路徑約束條件，剩余6個(gè)測(cè)試對(duì)象中存在無法探索的路徑。其中，對(duì)于solvers_foo、nested_bar 和double2long_foo 3 個(gè)測(cè)試對(duì)象，JDart-Ga 的路徑覆蓋數(shù)量高于JDart，路徑覆蓋率分別提升了20%、23%和16%。具體來說，OK PATHS 分別增加了 0、2 和 1 條，ERROR PATHS分別增加了1、1和0條，TOTALS PATHS分別增加了0、6和0條。

表2 不同路徑覆蓋情況對(duì)比

圖4 路徑覆蓋率對(duì)比

對(duì)JDart-Ga 提升上述3 個(gè)實(shí)驗(yàn)對(duì)象路徑覆蓋率的原因進(jìn)行分析發(fā)現(xiàn)：（1）如果路徑約束條件中涉及強(qiáng)制類型轉(zhuǎn)換，有可能會(huì)出現(xiàn)同一輸入變量在路徑約束條件中存在兩種不同的數(shù)據(jù)類型的情況，約束求解器求解此類約束條件時(shí)間開銷過大，導(dǎo)致超出規(guī)定的時(shí)間，nested_bar 和double2long_foo 中存在這種類型的約束條件，例如：nested_bar 中的路徑約束條件{d<3.141，（sint32）d+65>64，5×（（sint32）d+65）>325，（sint32）d+65!=66}；（2）當(dāng)存在約束求解器不能求解的復(fù)雜約束條件時(shí)，可以利用遺傳算法優(yōu)勢(shì)，根據(jù)測(cè)試用例的適應(yīng)度不斷變異生成趨近于滿足路徑約束條件的解，例如：對(duì)于solvers_foo中的路徑約束條件{d≥ 0.0，d≤ 6.283 185 307 179 586，sin（d）<0.0，cos（d）>0.0}，JDart無法求解，而JDart-Ga可以成功生成測(cè)試輸入d=4.715 407 046 706 579。

表3對(duì)JDart和JDart-Ga測(cè)試17個(gè)實(shí)驗(yàn)對(duì)象的時(shí)間開銷進(jìn)行了統(tǒng)計(jì)。由于JDart-Ga相比于JDart增加了一個(gè)求解判斷模塊，所以測(cè)試實(shí)驗(yàn)對(duì)象所需的時(shí)間花銷要比JDart略長(zhǎng)。如表3所示，與JDart相比，JDart-Ga測(cè)試solvers_foo、nhandler_foo、functions_foo、fields_foo 和double2long_foo 5 個(gè)實(shí)驗(yàn)對(duì)象的時(shí)間開銷增幅超過10%；測(cè)試nested_bar 的時(shí)間開銷減少了99.8%；測(cè)試剩余11 個(gè)實(shí)驗(yàn)對(duì)象的時(shí)間開銷增幅低于10%，與預(yù)期相符。對(duì)5 個(gè)時(shí)間開銷增幅超過10%的實(shí)驗(yàn)對(duì)象進(jìn)行代碼分析發(fā)現(xiàn)：（1）solvers_foo 和 double2long_foo 中均存在JDart 無法覆蓋的路徑，JDart-Ga 覆蓋了更多的程序路徑，從而導(dǎo)致時(shí)間開銷分別增加了15.2%和14.8%；（2）fields_foo、functions_foo和nhandler_foo中的DON’T KNOW PATHS 為約束求解器報(bào)告錯(cuò)誤，實(shí)際上應(yīng)該為unsat，而遺傳算法并不能從邏輯上去判斷約束條件是否有解，這導(dǎo)致JDart-Ga仍嘗試使用遺傳算法生成覆蓋上述路徑的測(cè)試輸入，消耗了大量無效時(shí)間，時(shí)間開銷分別增加了596.6%、400.9%和372.7%。對(duì)測(cè)試時(shí)間開銷大幅降低的nested_bar 進(jìn)行分析，發(fā)現(xiàn)在該程序中有8條路徑約束條件都含有強(qiáng)制類型轉(zhuǎn)換操作，故約束求解器在無法判斷該類型的路徑約束條件是否有解的過程中消耗了大量的時(shí)間，而JDart-Ga 可以快速求解，從而節(jié)省了大量時(shí)間開銷。

表3 測(cè)試時(shí)間對(duì)比 ms

5 總結(jié)

本文深入研究了現(xiàn)有符號(hào)執(zhí)行測(cè)試方法面臨的問題和挑戰(zhàn)，提出了一種遺傳算法輔助的動(dòng)態(tài)符號(hào)執(zhí)行測(cè)試方法。該方法能夠彌補(bǔ)動(dòng)態(tài)符號(hào)執(zhí)行中約束求解器所存在的求解能力不足的問題，從而達(dá)到提升路徑覆蓋的目的。實(shí)驗(yàn)結(jié)果表明，本文提出的方法能夠有效地提升路徑覆蓋率。在下一步工作中，將嘗試將優(yōu)化本方法應(yīng)用于更加復(fù)雜的輸入數(shù)據(jù)類型和更大規(guī)模程序。