基于符號執行與混合約束求解的測試用例生成研究
2016-07-19 02:07:18周海將吳軍華
計算機應用與軟件 2016年6期
周海將 吳軍華
(南京工業大學計算機科學與技術系 江蘇 南京 210009)
?
基于符號執行與混合約束求解的測試用例生成研究
周海將吳軍華
(南京工業大學計算機科學與技術系江蘇 南京 210009)
摘要由于現有基于符號執行的測試用例生成方法無法對關于字符串的測試用例生成提供有效支持，因此提出并實現了基于符號執行與混合約束求解測試用例自動化生成方法。該方法利用模型檢測軟件對被測軟件源代碼進行符號執行，生成關于字符串與數值的混合約束集,利用字符串-數值約束求解器對約束集進行求解，最終根據求解結果生成軟件測試用例與不可達路徑。實驗結果表明，該方法較好地支持了關于字符串測試用例生成，且具有良好的效率與準確性。
關鍵詞測試用例生成符號執行技術混合約束求解字符串
0引言
隨著軟件業的不斷發展，主流軟件中字符串操作的占比越來越大[1]。例如Web軟件中后臺邏輯處理部分通常需要與數據庫進行交互，其中SQL語句的動態生成主要通過字符串操作完成。此外，前端界面用于顯示的字符串變量與常量基本通過字符串操作動態地生成。而軟件測試是保證軟件質量的重要手段，由于早期的傳統軟件測試方法主要針對數值與邏輯計算，對于字符串變量和字符串操作不能有效的支持，因此關于字符串的測試用例生成技術逐漸成為國內外的研究熱點之一[2]。
1研究現狀
近年來軟件測試領域基于符號執行的測試研究成為熱點。它是一種靜態程序分析技術[3]，主要原理是使用符號變量代替實際值模擬程序的執行，獲取相應路徑的約束，最終通過約束求解獲得測試數據。如今該技術的瓶頸在于約束求解器的效率，尤其缺乏優秀的字符串求解器。關于約束求解技術，根據表示字符串的形式，字符串約束求解器主要分為基于位向量與基于有限狀態自動機兩種類型。
HAMPI[4]是基于位向量的字符串約束求解器，主要原理是將輸入的字符串約束轉換為是否為正則語言接受的形式，利用位向量表示，最后利用STP位向量求解器求解約束條件。但僅支持固定長度的字符串約束且不支持數值約束。Kudzu[5]基于位向量，改進了HAMPI，提供了較多字符串操作的支持，并且有限支持數值約束。
文獻[2]詳細論述了基于有限狀態自動機的字符串約束求解器技術。其中Rex[7]基于有限狀態機與SMT約束求解器，使用邏輯謂語表示自動機的轉換。Rex支持字符串約束與數值約束，但效率很低，遠遠慢于HAMPI。文獻[8]提出一種基于怠惰算法的約束求解技術，利用圖表示字符串之間的約束，通過回溯搜索圖尋求結果。該技術若有解時，效率很高；若無解則求解時間往往超出可接受范圍。此外，該技術只能對字符串操作與正則語言提供有限的支持。
綜上所述，要實現基于符號執行軟件測試自動化，就應改進約束求解技術的效率與增強適用性。
2符號執行與約束求解
符號執行[3]是一種可靠的程序分析技術，基本原理是：在源代碼中，將程序中變量值替換為表示為未知但固定的符號標記，模擬程序執行的過程。符號標記在靜態數學意義上用來表示一些未知的但固定的值，一個程序在特定的執行過程中會有與其相關的多個不同的符號標記。主要思想是從控制流圖的入口處用符號標記代替具體的輸入值來模擬程序符號化的執行過程。一般的軟件測試用具體值作為測試用例輸入來執行程序，所進行的計算是具體邏輯運算，符號執行使用符號標記來執行程序，所進行的是代數運算，符號執行即一般測試的擴充。符號執行是程序驗證和程序測試的折中，一方面它具有普通測試所具有的測試方法，通過運行被測程序驗證程序的可靠性；另一方面，符號執行沿著一條路徑的一次執行積累的約束條件代表了一大類普通測試的集合，驗證程序接受此類輸入后是否正確，同時可以發現程序中不可行的路徑。
約束問題由三個基本元素組成：變量、變量域與約束。約束求解即在變量域中找到特定變量值使之與各變量之間均滿足約束?；旌霞s束問題是傳統約束問題的擴展，即變量域為多個，本文分為數值變量域與字符串變量域。約束求解技術主要包括數值法、符號計算法、區間分析法、啟發式算法等。
3基于符號執行與混合約束求解的測試用例生成技術
3.1符號執行框架
本文提出了一個基于符號執行技術與混合約束求解的測試用例自動化生成方法框架，總體來說包括兩個部分：符號執行生成約束部分；對約束集求解得到測試輸入與不可達路徑部分。主要步驟為：
(1) 將源程序進行擴展，利用符號執行工具對已擴展的源代碼進行符號執行，遍歷源程序的每個路徑，生成每個與程序終點相對應的路徑條件。路徑條件定義為與該程序終點對應的約束。這樣的過程最后得到的就是路徑條件集合，即約束條件集合。
(2) 利用約束求解方法對約束條件集合進行約束求解，得到關于每個程序終點的約束的具體值，即程序測試輸入。若約束求解無解，即程序終點不可達，說明該路徑是錯誤的，返回該錯誤路徑。符號執行框架的結構如圖1所示。
圖1 基于符號執行與混合約束求解測試用例生成框架
本文對基于符號執行與混合約束求解測試用例生成框架給出以下定義:
定義 1定義執行該路徑得到的路徑條件為PC(Path Condition)，PC積累了該路徑每一條語句執行必須滿足的約束。不可達路徑的執行路徑定義為PU。
定義2約束集C：定義由對源程序進行符號執行得到的路徑集合為C{c1,….,ci,….,cn},稱C為約束條件集合，其中ci表示某個具體的路徑條件表達式，n為約束條件的總數。
定義3若是關于數值的路徑條件，定義為數值約束PCN；若是關于字符串的約束，定義為字符串約束PCS；若PC中既包含數值約束又包含字符串約束，稱該PC為混合約束條件PCH，對于混合約束條件集合為CH。
定義4由PCN求解得到的值為關于數值約束條件的測試輸入，定義為TN;由PCS求解得到的值為關于字符串約束條件的測試輸入，定義為TS;相應的TN與TS的集合即關于該執行路徑的測試輸入T。
定義5由對約束條件集合進行求解的過程定義為S，其中S的輸入是約束條件集合，輸出為測試輸入集合與不可達路徑條件。表達式為：
S(C)=TANDPU
其中C={c1,…,ci,…,cN};T={T1,…，Ti,…，TN}，Ti=TNiANDTSi。
3.2路徑條件生成
本文將通過圖2的例子詳細論述符號執行的過程。圖2表示的是根據字符串取值的不同采取不同處理，目的是對字符串進行辨識以確定S的含義，并決定采取哪些方法處理S。
圖2 路徑條件的分支樹
如圖2所示，PC0表示的是符號執行的起點，Path1-Path6表示的是符號路徑的終點。符號L(q)代表字符串q的長度。符號執行過程中，首先檢測輸入字符串是否以負號為開頭，即檢測字符串s代表的是否為負數；接著檢測字符串是否符合正則表示式的格式；然后檢測字符串s中是否含有逗號，若無逗號，字符串s將被轉換為長精度類型，否則將s中逗號后面的數字賦值整型變量x;最后檢測x是否小于100。這個代碼在一般的Web程序中比較常見，首先對輸入字符串進行格式檢測，接著將字符串轉換為數字，最終在分支中對字符串進行處理。在每個路徑終點都生成了約束條件的交集，即通過符號執行得到的約束條件集合C，其中C中元素為：
c1={s.charAt(0)==’-’}
c2={ s.charAt(0)==’-’,s.matches(“-d+,d{3}”)}
c3={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.notCtains(“,”),i==-1,f==VOF(s),f1==(f/102),round(f1/3)=dl}
c4={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.notCtains(“,”),i==-1,f==VOF(s),f1==(f/102),round(f1/3)≠dl}
c5={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.subString(i,i+1)==”,”sl=s.substring(i+1),VOF(sl)>=100 }
c6={s.charAt(0)==’-’,s.notmatches(“-d+,d{3}”,s.subString(i,i+1)==”,”sl=s.substring(i+1),VOF(sl)<100 }
在下一步中通過對C進行約束求解，則可以生成測試數據與不可達路徑。由于C中的元素ci既包含PCN又包含PCS，因此，約束求解器就需要具有對PCN和PCS兩種約束條件的求解能力。當前的約束求解算法對字符串約束不能提供有效支持，對此本文提出并實現了數值—字符串混合約束求解器[9]。
3.3混合約束求解算法
混合約束集合包含數值約束與字符串約束。本文對此的解決方法為：通過將兩種約束集進行分離，運用不同的約束求解器進行處理。數值約束條件選用已有的Coral[10]方法和Yices[11]方法處理，其中線性數值約束使用Yices方法處理，簡單非線性數值約束使用Coral方法處理。對于字符串約束條件使用本文設計的基于有限狀態機(FSM)約束求解器。具體算法為：
步驟1初始化約束求解器。加載由符號執行步驟得到的約束條件集合CH。對CH中的所有元素ci遍歷執行以下步驟。
步驟2利用Coral與Yices數值約束求解器對ci中的PN部分進行求解，若無解則輸出該執行路徑，并退出；若有解，保存Ts并執行下一步。
步驟3將CH中的Cs部分加載到求解器中，并對其進行字符串求解。若有解則輸出Ts與Tn。即該執行路徑的測試輸入；若無解，執行以下步驟。
步驟4首先判斷求解時間是否超出限制，若超出則放棄，返回求解時間并退出；反之，根據RULE庫替換可以替換的字符串約束條件為相應的數值約束條件，轉到步驟1循環。
在算法中提到的RULE庫是為了提高混合約束條件求解效率而增加的。主要實現的原理:字符串約束部分可以轉換為數值約束，數值約束求解效率一般優于字符串約束期間效率，實現部分數值約束與字符串約束互相的轉換將提高求解效率。
3.4字符串約束求解改進
本文使用有限狀態機(FSM)表示一個符號字符串變量，即所有變量可能的取值組成了可以被這個FSM識別的語言。實現是基于文獻[12]提出的自動機。FSM的轉換(邊)擁有一個范圍取值。當一個自動機求精時，不僅需要改變結點和邊，邊上的額外取值范圍也會變化。例如圖3表示的是接受正則表達式“-d+,d{3}”的自動機。
圖3 接受-d+,d{3}的自動機
本文通過使用有限狀態自動機來實現字符串的操作。例如，字符串s1和字符串s2的連接操作轉換為s2的自動機附加到s1自動機的操作。該自動機支持了很多的字符串操作，但是因為其設計是用于靜態分析，本文擴展該自動機不支持的字符串操作。例如，substring(2,4)方法的操作返回的是從索引位置2到索引位置4的子字符串，如圖4所示。基本方法是：首先從開始狀態轉移兩個步驟；然后將訪問到的節點作為開始節點；接著將從開始節點兩步轉換中所有的狀態作為接受狀態；最后，我們交互該自動機并接受所有長度為2的自動機用來得到最終的自動機版本。除此之外還有其他需要擴展，比如替換字符與替換子字符串等。
圖4 在自動機上操作substring(2,4)操作
字符串約束描述的是字符串之間的關系。FSM并不直接對字符串約束求解，因此需要根據字符串約束加強對字符串的求精。這個過程包括：(1)自動機求精；(2)不動點計算；(3)優化收斂速度。例如，對于s.charAt(0)=’-’約束，將字符串s與接收首字符為負號的自動機交互。后來，因為字符串s的部分通過parseInt方法轉換為整型變量，將字符串s的該部分與建模所有有效整數交互；同樣需要對字符串s的根據更新部分對字符串s進行求精。例如，將字符串s的自動機與以某種形式結尾部分的自動機交互。這部分工作將一直進行，直到沒有什么求精是可能的，并且得到不動點，即得到一個可能的字符串值。
本文通過RULE庫來實現字符串約束與數值約束之間的互相轉換，因此字符串約束和數值約束對于共享的符號變量取值必須一致，即共享的符號變量在數值約束與字符串約束中的值相同。在符號變量同步的過程中，數值約束求解器N會給出一些候選值，提交給字符約束求解器S判斷該符號變量值是否沖突。若無沖突，則符號變量取值被S和N都接受；否則S會返回N引起沖突的約束變量值，請求N提交其他候選符號變量取值。接著N取消沖突的符號變量值，使用啟發式算法重新搜索另一個有效賦值，繼續以上步驟。在交互的過程中只有共享變量的具體值可以從N提交到S，N也可以理解一些字符串沖突，并傳遞給S。例如，數值約束s.length()>5使相應的自動機應該與接受長度大于5的自動機交互。
在迭代過程中，我們將字符串約束求解器[14，15]和數值約束求解器得到的約束交換，這樣就可以提高收斂速度。例如，對于字符串約束s1=s2.trim()，數值約束求解器會給出一個數值約束給出L(s1)<=L(s2)，其中L()方法返回的是字符串對象的長度。
在方法中，類似上例的交互約束由RULE庫建模，RULE庫包含一般Java程序常見的交互規則，表1展示了該庫的部分規則。
表1 RULE庫中部分RULE規則
續表1
為了解釋數值與字符串約束迭代求解的過程，對于圖2中的path 4,下面給出了path 4的路徑條件，包含了已經增加的額外的約束。為了對該約束求解，數值約束求解器將得到一組有效的數值變量賦值，L(s)=2,L(s1)=1,i=0,x=100。然后將這組賦值提交給字符串約束求解器。但是因為x=parseInt(s1)條件不滿足，所以字符串求解器沒有找到有效賦值。這就要求N進行重新計算直到s1的長度大于等于3，或者求解器利用RULE庫從“x=parseInt(s1) ^ 》100”得到一個額外的L(s1)>=3約束。此外從“s1 = s.substring(i+1)”得到L(s)>=L(s1)。有了額外的約束，求解器可以很快得到新的一組有效變量賦值，例如s=“-,100”, s1=“100”, i=1,x=100。
NumericString
(1 : L(s) > 0)s:charAt[0] = `-’
(3 : i + 1 + L(s1) = L(s))s1 = s.substring(i + 1)
(4 : L(s1) > 0)x = parseInt(s1)
i=≠-1 ^ x》 100┐(s.matches(- d+,d{3}))
當字符串約束求解器S不能得到一個有效賦值時，額外的約束被傳遞給數值約束求解器并始新的迭代計算。最終，混合約束迭代求解器可以得到一個有效的解決。
在符號執行得到的混合約束可能包含非線性數值約束條件，對非線性約束求解，正常的處理不僅效率不高，而且容易導致約束求解失敗。對此本文通過將非線性約束條件轉換為多個線性約束組合來避免直接求解效果不佳。例如round()方法，該方法的作用是對于給定的浮點數變量返回最接近的整型值。對于round()方法，本文將其轉換為“((e-0.5
4實驗部分
本文使用的是兩個富含字符串操作的Java源程序進行對比試驗，使用JPF的符號執行版本[13]對實驗樣本進行符號執行兩個程序的詳細情況見表2。由于程序代碼量過大，因此僅關注邏輯處理部分，因為這部分代表了程序中最復雜的字符串與數值計算與處理。測試環境為HPPC機-IntelCore2DuoCPUE7500,2.93GHz,2GB;WindowsXPsp3。
表2 實驗程序數據
測試中記錄生成的是輸入符號變量的個數，在程序有效結束狀態下生成的測試用例個數，在符號執行中因異常拋出而未執行的路徑個數。完成實驗的時間、完成實驗中迭代的次數見表3所示。最后在符號輸入個數為四個時，得到了的測試用例覆蓋率達到80%。
表3 程序A的實驗結果
由表3可以看出在符號輸入個數為4時，得到了的測試用例覆蓋率達到80%。綜上所述，該技術在合理的時間內能有效自動化地生成測試用例與不可達路徑。
為了說明非線性約束求解的有效性，本文使用金融應用程序B進行單元測試。程序B包含很多對Java語言長精度類型的舍入操作。實驗對非線性模式開啟與否做了多次實驗(如表4所示)。當開啟非線性模式時，所有生成的路徑條件由Yices求解，反之則由Coral求解?？梢詮谋碇忻黠@看到，非線性模式下的具有明顯優勢。
表4 程序B的實驗結果
從表3、表4可以看出，本文提出的基于符號執行與混合約束求解技術的測試自動化技術明顯優于傳統基于符號執行的測試自動化技術。不僅對字符串約束與數值約束提供支持，求解效率也有明顯提升。
5結語
本文對符號執行技術、數值—字符串混合約束求解進行了研究，設計并實現了基于符號執行和混合約束求解的自動化測試技術。它能有效提高約束求解效率，并支持字符串約束與數值約束。實驗表明，該方法能在可接受的時間范圍內生成測試
用例與錯誤路徑。文中的混合約束求解框架還有一些不足與需要改進的算法?；旌霞s束求解算法的效率還存在提高的可能，優化可以采用各個擊破的“on-the-fly”技術。此外該方法只能對Java源程序提供支持，以后可以擴展到其他主流編程語言例如C++、C等。
參考文獻
[1] 梅宏,王嘯吟,張路.字符串分析研究進展[J].軟件學報,2012,24(13):37-49.
[2]HooimeijerP,VeanesM.Anevaluationofautomataalgorithmsforstringanalysis[C]//Verification,ModelChecking,andAbstractInterpretation.SpringerBerlinHeidelberg, 2011: 248-262.
[3]KingJC.Symbolicexecutionandprogramtesting[J].CommunicationsoftheACM, 1976, 19(7): 385-394.
[5]SaxenaP,AkhaweD,HannaS,etal.Asymbolicexecutionframeworkforjavascript[C]//SecurityandPrivacy(SP), 2010IEEESymposiumon.IEEE, 2010: 513-528.
[6]VeanesM,DeHalleuxP,TillmannN.Rex:Symbolicregularexpressionexplorer[C]//SoftwareTesting,VerificationandValidation(ICST), 2010ThirdInternationalConferenceon.IEEE, 2010: 498-507.
[7]HooimeijerP,WeimerW.Solvingstringconstraintslazily[C]//ProceedingsoftheIEEE/ACMinternationalconferenceonAutomatedsoftwareengineering.ACM, 2010: 377-386.
[8]ShannonD,GhoshI,RajanS,etal.Efficientsymbolicexecutionofstringsforvalidatingwebapplications[C]//Proceedingsofthe2ndInternationalWorkshoponDefectsinLargeSoftwareSystems:HeldinconjunctionwiththeACMSIGSOFTInternationalSymposiumonSoftwareTestingandAnalysis(ISSTA2009).ACM, 2009: 22-26.
[9]SouzaM,BorgesM,d’AmorimM,etal.CORAL:solvingcomplexconstraintsforsymbolicpathfinder[M]//NASAFormalMethods.SpringerBerlinHeidelberg, 2011: 359-374.
[10]DutertreB,DeMouraL.Theyicessmtsolver[OL]. 2006.Toolpaperathttp://yices.csl.sri.com/tool-paper.pdf.
[11]ChristensenAS,M?llerA,SchwartzbachMI.Preciseanalysisofstringexpressions[M].SpringerBerlinHeidelberg, 2003.
[12]P?s?reanuCS,RungtaN.SymbolicPathFinder:symbolicexecutionofJavabytecode[C]//ProceedingsoftheIEEE/ACMinternationalconferenceonAutomatedsoftwareengineering.ACM, 2010: 179-180.
ON TEST CASE GENERATION BASED ON SYMBOLIC EXECUTION AND HYBRID CONSTRAINT SOLVING
Zhou HaijiangWu Junhua
(Department of Computer Science and Technology, Nanjing Tech University, Nanjing 210009, Jiangsu, China)
AbstractSince current test case generation method based on symbolic execution is unable to provide effective support to the test case generation with regard to character string, therefore we present an automatic test case generation method, which is based on symbolic execution and hybrid constraint solving, and implement it as well. The method uses the model checking software to make symbolic execution on the source code of the software to be tested and generates a mixed constraint set correlated to string and numeral. Then it uses the string-numerical constraints solver to calculate the constraint set. Finally, according to the calculation result it generates the software test case and the infeasible path. Experimental result shows that this method well support the generation of test case in regard to string and has good efficiency and accuracy.
KeywordsTest cases generationSymbolic execution technologyHybrid constraint solvingString
收稿日期：2015-01-30。周海將，碩士，主研領域：軟件測試。吳軍華，副教授。
中圖分類號TP301
文獻標識碼A
DOI:10.3969/j.issn.1000-386x.2016.06.006
