鄭華利 劉釗遠(yuǎn) 田 野

（西安郵電大學(xué)計(jì)算機(jī)學(xué)院 西安 710061）

1 引言

軟件測(cè)試是保證軟件正確性、完整性、安全性和質(zhì)量的主要程序分析方法。相比于覆蓋率低的模糊測(cè)試［1］，符號(hào)執(zhí)行［2］覆蓋率高且應(yīng)用廣泛，然而其本身存在一定的瓶頸，即路徑爆炸、約束求解、符號(hào)執(zhí)行精確性三大問題，使得符號(hào)執(zhí)行很難應(yīng)用到實(shí)際的測(cè)試環(huán)境當(dāng)中。所謂的路徑爆炸問題指的是假如一個(gè)實(shí)際程序有X個(gè)分支語(yǔ)句，那么該程序的路徑數(shù)是2x個(gè)，即程序的路徑數(shù)量隨程序的分支語(yǔ)句數(shù)呈指數(shù)增長(zhǎng)。

目前為止，對(duì)于符號(hào)執(zhí)行中的路徑爆炸［3～4］問題解決方案有很多，主要包括智能搜索策略［5～6］、摘要、路徑合并［7］、修剪冗余路徑等。這些解決方案的共同點(diǎn)是只訪問或者先訪問能夠達(dá)到測(cè)試標(biāo)準(zhǔn)的路徑。Chen［8］等提出了幾種針對(duì)符號(hào)執(zhí)行中的路徑爆炸問題進(jìn)行分析的智能搜索策略，不同的搜索策略存在不同程度的缺陷，例如深度優(yōu)先搜索算法存在覆蓋率低，必須指定最大深度的問題。羅榮森［9］等提出基于符號(hào)摘要的動(dòng)態(tài)執(zhí)行方法，借助函數(shù)摘要［10］和符號(hào)摘要的思想，對(duì)動(dòng)態(tài)符號(hào)執(zhí)行過程中的符號(hào)和約束信息進(jìn)行保存，避免后續(xù)對(duì)相同的路徑進(jìn)行重復(fù)地符號(hào)執(zhí)行，此方法存在存儲(chǔ)空間的消耗問題。Kuznetsov［11］等提出的狀態(tài)合并技術(shù)是將不同路徑上的路徑前綴進(jìn)行合并，使得搜索路徑的數(shù)量由指數(shù)級(jí)增長(zhǎng)降低為多項(xiàng)式的增長(zhǎng)。RW-set［12］等提出的路徑修剪技術(shù)通過跟蹤程序的讀取和寫入的內(nèi)存位置，判斷路徑是否能夠探索到新的程序行為，修剪那些已經(jīng)探索過能夠產(chǎn)生同樣效果的執(zhí)行狀態(tài)的路徑，此方法針對(duì)大型應(yīng)用程序面臨著巨大的可擴(kuò)展性挑戰(zhàn)。

因此，為了克服現(xiàn)有的路徑爆炸解決方案中存儲(chǔ)空間消耗大、只適用于小型程序的缺陷，本文提出一種利用Hoare邏輯中的后置條件引導(dǎo)符號(hào)執(zhí)行的冗余路徑刪除方法。利用前置條件計(jì)算已探索路徑的路徑條件，在測(cè)試用例生成時(shí)針對(duì)程序共享的路徑后綴使用后置條件進(jìn)行識(shí)別，若當(dāng)前的路徑條件合并到后置條件，則此執(zhí)行路徑的其余部分將跳過，在保證覆蓋有效的測(cè)試用例的情況下，通過冗余路徑的刪除，減少程序的執(zhí)行時(shí)間，從而達(dá)到減輕符號(hào)執(zhí)行的路徑爆炸問題的目的。

2 相關(guān)理論依據(jù)

2.1 符號(hào)執(zhí)行

符號(hào)執(zhí)行的核心思想是將程序輸入符號(hào)化，利用符號(hào)值來代替具體值，對(duì)程序進(jìn)行靜態(tài)分析，獲取代碼中的控制流圖，在控制流圖的基礎(chǔ)上生成符號(hào)執(zhí)行樹，為程序所有路徑建立一系列的以輸入數(shù)據(jù)為變量的表達(dá)式，在符號(hào)執(zhí)行樹的基礎(chǔ)上，將測(cè)試數(shù)據(jù)的生成問題轉(zhuǎn)化為可滿足性問題，并使用約束求解器來求解新的測(cè)試輸入。

2.2 基于Hoare邏輯的符號(hào)執(zhí)行技術(shù)

Hoare邏輯［13］的核心特征是Hoare三元組，表示為｛P｝S｛Q｝，其中P、Q均為邏輯公式，前置條件P和后置條件Q是程序S的規(guī)約。Hoare三元組表示當(dāng)S執(zhí)行前P成立，那么S執(zhí)行并終止后有Q成立。

在證明程序正確性的過程中，程序中的每一條語(yǔ)句的前后都會(huì)有一個(gè)變量的邏輯表達(dá)式所組成的約束條件，語(yǔ)句中的變量根據(jù)程序執(zhí)行的語(yǔ)義必須滿足對(duì)應(yīng)的約束條件。公理語(yǔ)義中使用的邏輯表達(dá)式稱為謂詞或斷言，在程序語(yǔ)句前面的謂詞是當(dāng)前語(yǔ)句中變量的約束條件。相反地，在程序語(yǔ)句后面的謂詞是語(yǔ)句執(zhí)行后變量所滿足的新約束條件，這些謂詞分別稱為語(yǔ)句的前置條件和后置條件。在符號(hào)分析的過程中，利用已知的后置條件來計(jì)算當(dāng)前語(yǔ)句的前置條件。其中，最弱前置條件是保證后置條件有效的最小前置條件［14］。在實(shí)際的分析中，以程序的執(zhí)行結(jié)果作為最后一條語(yǔ)句的后置條件，通過該后置條件和程序最后一條執(zhí)行語(yǔ)句來計(jì)算其最弱前置條件，該前置條件又作為上一條語(yǔ)句的后置條件，以此類推到程序的開始［15］。

對(duì)于語(yǔ)句S，前置條件和后置條件分別為P和Q，語(yǔ)句S的最弱前置條件的計(jì)算可以通過轉(zhuǎn)換函數(shù)wp［S，Q］［16］來獲得，在最弱前置條件所遵循的語(yǔ)法規(guī)則中，前置條件的計(jì)算為

對(duì)于分支語(yǔ)句，前置條件的計(jì)算為wp（S1 or S2，Q）=wp（S1，Q）∧wp（S2，Q）。在實(shí)際的分析過程中，最弱前置條件通過當(dāng)前語(yǔ)句及其后置條件經(jīng)過轉(zhuǎn)換函數(shù)所計(jì)算獲得。

3 冗余路徑刪除方法

3.1 冗余路徑刪除模型

本文利用Hoare邏輯中的后置條件引導(dǎo)符號(hào)執(zhí)行將程序中的冗余路徑進(jìn)行刪除，以生成有效的測(cè)試用例。首先將源程序進(jìn)行LLVM中間語(yǔ)言轉(zhuǎn)換成LLVM字節(jié)碼，獲取初始路徑集合。然后使用最弱前置條件計(jì)算路徑后綴，使用后置條件識(shí)別程序運(yùn)行過程中的共享路徑后綴。最后通過約束求解器檢查路徑條件的可滿足性來計(jì)算測(cè)試輸入。具體的冗余路徑刪除實(shí)現(xiàn)模型如圖1所示。

圖1 冗余路徑刪除模型

3.2 冗余路徑刪除實(shí)現(xiàn)步驟

本文方法將程序中可能出現(xiàn)的故障利用特殊的中止指令進(jìn)行表示，考慮到中止可能出現(xiàn)在路徑的任何地方，因此檢測(cè)故障需要覆蓋所有有效的執(zhí)行路徑，指令可能是以下類型之一。

skip:（跳過）代表虛擬語(yǔ)句，通常用于省略其他分支；

halt:（停止）代表正常的程序終止；

abort:（中止），代表程序終止失敗。

對(duì)于程序中的if分支用i（fc）表示，else分支用else表示，也可以用i（f?c）表示。后置條件引導(dǎo)符號(hào)執(zhí)行的冗余路徑刪除方法的流程如圖2所示。

圖2 冗余路徑刪除實(shí)現(xiàn)流程

詳細(xì)的實(shí)現(xiàn)步驟描述如下:

步驟一:設(shè)置全局變量post［l］記錄每條路徑的后置條件，并置為false，初始化路徑條件pcon、控制位置l、存儲(chǔ)映射mem等信息，利用數(shù)據(jù)結(jié)構(gòu)中的堆棧來存儲(chǔ)符號(hào)執(zhí)行中的程序狀態(tài)，將初始化的數(shù)據(jù)進(jìn)行入棧操作。

步驟二:利用while循環(huán)來判斷stack是否為空，若不為空，將程序狀態(tài)中的＜pcon，l，mem＞信息進(jìn)行出棧操作，并判斷路徑條件是否滿足mem。若滿足，則利用for循環(huán)遍歷控制位置l，去執(zhí)行指令事件。若stack為空，則直接跳出循環(huán)，并結(jié)束。

3.3 實(shí)例分析

下面以圖3為例的程序?qū)Ρ疚乃岢龅姆椒ㄟM(jìn)行具體說明。

圖3 程序?qū)嵗?/p>

針對(duì)上述的例子，它有兩個(gè)輸入變量x，y和兩個(gè)連續(xù)的if-else語(yǔ)句。動(dòng)態(tài)符號(hào)執(zhí)行能夠計(jì)算一組測(cè)試輸入，每個(gè)測(cè)試輸入都具有所有輸入變量的具體值，目的是覆蓋程序所有的有效路徑。要執(zhí)行22=4個(gè)不同的執(zhí)行路徑，經(jīng)典的符號(hào)執(zhí)行工具KLEE將產(chǎn)生四個(gè)測(cè)試輸入。編號(hào)1到4是本例的覆蓋路徑如圖3所示，P1是通過第一行，第三行的if分支語(yǔ)句。根據(jù)觀察，許多的路徑后綴在不同的測(cè)試運(yùn)行之間共享，反復(fù)探索這些路徑后綴是路徑爆炸的主要原因。

雖然圖3中的四條路徑不同，但是根據(jù)觀察發(fā)現(xiàn)路徑后綴3是由P1和P3共享，路徑后綴4是由P2和P4共享，為了避免冗余路徑的探索，本文提出了一種利用Hoare邏輯中的后置條件引導(dǎo)符號(hào)執(zhí)行的冗余路徑刪除方法以生成有效的測(cè)試用例。該方法通過檢查分支是否被以前的探索所合并，利用最弱前置條件計(jì)算總結(jié)先前探索的路徑，將程序控制位置與后置條件進(jìn)行關(guān)聯(lián)，在隨后新的測(cè)試輸入過程中，檢查當(dāng)前的路徑是否被歸入到后置條件中，結(jié)果為true，則其余執(zhí)行路徑被跳過，以此來達(dá)到消除冗余路徑的目的。

對(duì)圖3中的實(shí)例進(jìn)行符號(hào)計(jì)算來說明本文所提出方法的主要思想，如表1所示。1～4列展示了標(biāo)準(zhǔn)的符號(hào)執(zhí)行是如何工作的，5～7列展示了在同一個(gè)例子上本文提出的方法是如何工作的，以此達(dá)到緩解路徑爆炸問題的目的。

對(duì)于路徑1，由于全局變量post［l］還不存在，在計(jì)算修剪之后的路徑條件時(shí)，先假設(shè)對(duì)于每個(gè)位置 post［l］=false。因此，第 1、3行的新路徑條件不變，如表1中所示。從該路徑的最后一條分支向前掃描，通過最弱前置條件計(jì)算其路徑后綴，結(jié)果如列7所示。對(duì)于路徑2，第4行修剪之后的路徑約束條件和路徑1的否定后置條件相關(guān)，為m'=m∧?（x+5＞y），其后置條件變?yōu)椋▁＞y）∨（x≤ y）=true，第1行的修剪后路徑條件和后置條件不變?nèi)詾閤≤0。對(duì)于路徑3，修剪之后的路徑條件為m'=m∧?true（?true為第2條路徑末尾計(jì)算的后置條件的否定）。路徑4在我們的方法中被跳過，沿著第3條路徑的第3行的else分支就可以到達(dá)第4行，第3條路徑在執(zhí)行第3行之前終止，因此路徑4將在本文提出的方法中完全跳過，就相當(dāng)于是一條冗余路徑。

表1 圖3中實(shí)例的符號(hào)計(jì)算

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

4.1 實(shí)驗(yàn)環(huán)境設(shè)置

為了驗(yàn)證本文所提出的后置條件引導(dǎo)符號(hào)執(zhí)行的冗余路徑刪除方法，設(shè)置實(shí)驗(yàn)環(huán)境如表2所示。

表2 實(shí)驗(yàn)環(huán)境和工具

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

為驗(yàn)證本文所提出的后置條件引導(dǎo)符號(hào)執(zhí)行的冗余路徑刪除方法的有效性，選擇GNU Coreutils軟件包中的 expr、uniq、id、nice、touch、tr、unlink、sort、du、ln等十種程序進(jìn)行實(shí)驗(yàn)。

通過最弱前置條件計(jì)算先前已探索的路徑，利用后置條件引導(dǎo)符號(hào)執(zhí)行在測(cè)試生成時(shí)進(jìn)行冗余路徑的識(shí)別和消除。圖4是使用開源工具klee和本文方法針對(duì)GUN Coreutils軟件包進(jìn)行符號(hào)執(zhí)行程序的路徑數(shù)的一個(gè)對(duì)比。由實(shí)驗(yàn)結(jié)果圖可知，采用本文的方法進(jìn)行冗余路徑的識(shí)別和刪除，程序的路徑數(shù)目明顯減少了，使得程序覆蓋有效的測(cè)試用例，減少了冗余路徑的覆蓋，在一定程度上，削弱了符號(hào)執(zhí)行中的路徑爆炸問題，使得程序的“指數(shù)級(jí)”路徑數(shù)有所降低，更進(jìn)一步地證明本文方法的有效性。

由圖5可以看出，針對(duì)GNU Coreutils軟件包分別使用klee和本文方法對(duì)每個(gè)基準(zhǔn)程序的性能進(jìn)行測(cè)試，使用本文方法使得程序的執(zhí)行時(shí)間有所減少，并且符號(hào)執(zhí)行效率得到了顯著的提高。當(dāng)基準(zhǔn)程序路徑數(shù)較小時(shí)，KLEE的符號(hào)執(zhí)行的效率和本文方法相比而言，性能變化不是非常明顯，但當(dāng)選取的基準(zhǔn)程序路徑數(shù)較為龐大時(shí)，本文所提出的方法符號(hào)執(zhí)行效率明顯優(yōu)于klee的符號(hào)執(zhí)行效率。同樣也解決了現(xiàn)有路徑爆炸問題方案只適用于程序規(guī)模較小的缺陷。

圖4 路徑數(shù)對(duì)比

圖5 性能對(duì)比

5 結(jié)語(yǔ)

本文提出了一種利用Hoare邏輯中的后置條件引導(dǎo)符號(hào)執(zhí)行的冗余路徑刪除方法。該方法使用最弱前置條件對(duì)符號(hào)執(zhí)行中已探索過的路徑進(jìn)行計(jì)算，在測(cè)試用例生成時(shí)使用后置條件，對(duì)共享的路徑后綴進(jìn)行識(shí)別和消除。經(jīng)實(shí)驗(yàn)驗(yàn)證，本文方法在一定程度上減少了程序的路徑探索數(shù)目和執(zhí)行時(shí)間，緩解了符號(hào)執(zhí)行中的路徑爆炸問題。但對(duì)于在冗余路徑刪除方法中存在的計(jì)算開銷大的問題仍然無法解決，將是下一步工作的研究重點(diǎn)。