一種基于符號執行的測試用例生成方法

鄭華利 劉釗遠 田 野

（西安郵電大學計算機學院 西安 710061）

1 引言

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

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

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

2 相關理論依據

2.1 符號執行

符號執行的核心思想是將程序輸入符號化，利用符號值來代替具體值，對程序進行靜態分析，獲取代碼中的控制流圖，在控制流圖的基礎上生成符號執行樹，為程序所有路徑建立一系列的以輸入數據為變量的表達式，在符號執行樹的基礎上，將測試數據的生成問題轉化為可滿足性問題，并使用約束求解器來求解新的測試輸入。

2.2 基于Hoare邏輯的符號執行技術

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

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

對于語句S，前置條件和后置條件分別為P和Q，語句S的最弱前置條件的計算可以通過轉換函數wp［S，Q］［16］來獲得，在最弱前置條件所遵循的語法規則中，前置條件的計算為

對于分支語句，前置條件的計算為wp（S1 or S2，Q）=wp（S1，Q）∧wp（S2，Q）。在實際的分析過程中，最弱前置條件通過當前語句及其后置條件經過轉換函數所計算獲得。

3 冗余路徑刪除方法

3.1 冗余路徑刪除模型

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

圖1 冗余路徑刪除模型

3.2 冗余路徑刪除實現步驟

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

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

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

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

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

圖2 冗余路徑刪除實現流程

詳細的實現步驟描述如下:

步驟一:設置全局變量post［l］記錄每條路徑的后置條件，并置為false，初始化路徑條件pcon、控制位置l、存儲映射mem等信息，利用數據結構中的堆棧來存儲符號執行中的程序狀態，將初始化的數據進行入棧操作。

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

3.3 實例分析

下面以圖3為例的程序對本文所提出的方法進行具體說明。

圖3 程序實例

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

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

對圖3中的實例進行符號計算來說明本文所提出方法的主要思想，如表1所示。1～4列展示了標準的符號執行是如何工作的，5～7列展示了在同一個例子上本文提出的方法是如何工作的，以此達到緩解路徑爆炸問題的目的。

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

表1 圖3中實例的符號計算

4 實驗與分析

4.1 實驗環境設置

為了驗證本文所提出的后置條件引導符號執行的冗余路徑刪除方法，設置實驗環境如表2所示。

表2 實驗環境和工具

4.2 實驗結果

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

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

由圖5可以看出，針對GNU Coreutils軟件包分別使用klee和本文方法對每個基準程序的性能進行測試，使用本文方法使得程序的執行時間有所減少，并且符號執行效率得到了顯著的提高。當基準程序路徑數較小時，KLEE的符號執行的效率和本文方法相比而言，性能變化不是非常明顯，但當選取的基準程序路徑數較為龐大時，本文所提出的方法符號執行效率明顯優于klee的符號執行效率。同樣也解決了現有路徑爆炸問題方案只適用于程序規模較小的缺陷。

圖4 路徑數對比

圖5 性能對比

5 結語

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