吳瀟雪, 鄭煒, 王培源, 王培甲, 樊宋宇

(1.西北工業(yè)大學 自動化學院, 陜西 西安 710072; 2.西北工業(yè)大學 軟件與微電子學院, 陜西 西安 710072)

作為軟件測試工作重要內容的測試用例生成,是影響軟件測試效果的重要環(huán)節(jié),測試用例的自動產生,對保證測試質量、提高測試效率至關重要[1-2]。其中,符號執(zhí)行引起了廣泛關注[3-5],并產生許多開源的符號執(zhí)行工具[6],諸如CUTE/jCUTE、CREST、JPathFinder[7]、KLEE[8]、SPF以及JDart[9-10]等。面向C的符號執(zhí)行工具,大多依賴于較為成熟的LLVM平臺和KLEE,發(fā)展較為迅速,在工業(yè)界也得到廣泛應用。而面向Java語言的符號執(zhí)行技術則發(fā)展相對較慢,尚處于探索階段?？煽壳腋咝У拿嫦騄ava程序的測試用例生成技術和工具亟待開發(fā)。

JDart[10]是一款較為成功的面向JAVA的符號執(zhí)行工具,它提供了良好的模型和框架。然而,目前JDart只能支持基本簡單的數(shù)據類型,如Int、Char的符號化,而對于復雜數(shù)據類型如Array、String、Object等還無法進行符號化,因而影響了其推廣和應用。

本文根據對JDart工具及動態(tài)符號技術的研究和應用,通過對JDart測試用例生成能力和所存在問題進行了深入剖析,針對數(shù)組符號化和約束求解,給出改進和優(yōu)化策略,以提高生成測試用例的覆蓋率,保證測試工作的質量。

1 基于符號執(zhí)行的測試用例生成

符號執(zhí)行是一種可靠、經典的白盒測試用例生成方法。其基本原理是將程序中變量值用符號標記替換,并以符號值模擬程序執(zhí)行的過程?；诜枅?zhí)行的測試用例生成方法,主要通過計算每條符號執(zhí)行路徑所需要滿足的約束條件,來得到測試輸入。

1.1 相關定義

為了便于討論,我首先列出與符號執(zhí)行測試用例生成相關的定義[11-12]。

定義1待測系統(tǒng)SUT(system under test)。給定n個稱之為待測軟件的參數(shù)pi(i=1,2,…,n)。這些參數(shù)可能代表系統(tǒng)的配置參數(shù)、內部實踐或者用戶輸入。

定義2路徑條件PC(path condition)。匯積了執(zhí)行某條路徑中每一條語句必須滿足的約束,不可達路徑的執(zhí)行路徑定義為PU。

定義3(約束集C)設由對源程序進行符號執(zhí)行所得到的路徑集合為C={c1,…ci,…,cn},則稱C為約束條件集合,其中cn表示某個具體的路徑條件表達式,n為約束條件的總數(shù)。

定義4(約束PC)對關于數(shù)值的路徑條件,定義為數(shù)值約束NPC;對關于字符串的約束,定義為字符串約束SPC;對PC中既包含數(shù)值約束又包含字符串約束,則稱該PC為混合約束條件HPC。

定義5(測試輸入T)由NPC求解所得到的值稱為關于數(shù)值約束條件的測試輸入,定義為TN;由SPC求解所得到的值稱為關于字符串約束條件的測試輸入,定義為TS;相應的TN和TS的集合即為關于該執(zhí)行路徑的測試輸入T。

定義6(求解過程S)將對約束條件結合進行求解的過程記為S,其中S的輸入是約束條件集合,輸出為測試輸入集合與不可達路徑條件,可寫成S(C)=TANDPU,式中C={c1,…ci,…,cn};T={T1,…Ti,…,TN}。

1.2 測試生成過程

符號執(zhí)行的核心思想,是用抽象化的符號表示程序中的具體輸入變量;通過解析程序的語句,為每條路徑生成路徑表達式,來生成符號執(zhí)行樹,并通過對路徑表達式進行求解獲得符號變量解的集合[7]。例如對于圖1所示的待測示例代碼,通過符號執(zhí)行分析,可以得到符號執(zhí)行語法樹如圖2所示。

1 intx,y;

2 if(x>y){

3x=x+y

4y=x-y;

5x=x-y;

6 if(x-y>0)

7 Assert false;

8 }

9 print(x,y)

圖1 示例代碼

通過該語法分析樹,可以得到程序執(zhí)行路徑、路徑約束條件以及對應的輸入,如表1所示。這就是一個簡單的基于符號執(zhí)行的測試用例生成過程。

表1 路徑條件、路徑、以及生成輸入

圖2 符號執(zhí)行樹

2 基于JDart的測試用例生成

2.1 JDart工具簡介

JDart[7]是一個面向Java的動態(tài)符號分析框架,采用模塊化架構。其中,執(zhí)行動態(tài)探索的主要組件與有效構建約束的組件進行通信,并與約束求解器進行接口通信。這些組件可以輕松擴展或修改,以支持多個約束求解器或不同的探索策略。此外,連同其最近的開源,使JDart成為研究和實驗的理想平臺。在當前版本中,JDart支持CORAL,SMTInterpol和Z3求解器,并能處理包含位操作、浮點算術和復雜算術運算(例如,三角和非線性計算)的約束求解器。

2.2 JDart測試用例生成機制

用動態(tài)符號執(zhí)行工具JDart測試程序時,還需要2個輔助工具:JConstraints和JConstraints-Z3。符號執(zhí)行工具在執(zhí)行過程中需要使用約束求解器對收集到的約束條件求解,JDart中常用的約束求解器是Z3,而Z3求解器為了提高求解的效率,對常用的數(shù)據類型定義了獨特的數(shù)據結構變量。因此,想要使用Z3求解器,需要使用Z3求解器提供的API接口,將收集到的約束條件中的變量和常量轉化為Z3求解器中的數(shù)據形式。動態(tài)符號執(zhí)行工具Jdart的工作流程如下:

Step1 初始化被測程序代碼模塊,創(chuàng)建一個新的任務。

Step2 在類ConcolicMethodExplorer的initialize

Method()函數(shù)中,調用函數(shù)initializeSymbolicParams(),對測試方法輸入值符號化。

Step3 創(chuàng)建符號值。對于基本數(shù)據類型,直接創(chuàng)建符號值。對于對象或數(shù)組等復雜數(shù)據類型時,調用processObject()方法進行處理,在processObject()方法中,進行符號值創(chuàng)建。

Step4 收集約束條件并進行約束求解。收集被測程序中的分支條件作為路徑約束,將路徑約束添加到約束集合中,按深度優(yōu)先路徑調度策略對約束集合中的某一項或幾項取反,得到路徑樹上下一條路徑的約束集合,然后調用JConstraints-Z3中的add()方法,將路徑約束轉化為Z3求解器可以識別的約束條件,并將其添加到約束求解器中,最后調用solve()函數(shù)對約束集合求解,得到下一條路徑的輸入值。并依次執(zhí)行,直到遍歷被測程序所有路徑的執(zhí)行。

2.3 存在問題

JDart實現(xiàn)了基本的測試用例生成思路和框架。但是,對于許多具體的數(shù)據類型(如對象、數(shù)組、字符串等)還無法支持。圖3是一個簡單的包含數(shù)組的程序,圖4展示該程序預期的執(zhí)行路徑。

1 int ArrayTest(int[]a)

2 {

3 if(a==null) {

4 return 0;

5 }else if(a.length>0) {

6 if(a[0]==123) {

7 throw new Exception("bug");

8 }

9 returna[0];

10 } else {

11 return 0;

12 }

13 }

圖3 測試程序代碼

圖4 預期路徑

理論上,動態(tài)符號執(zhí)行測試時會遍歷程序所有4條路徑,如圖4所示。但是, JDart根據初始輸入數(shù)組值的不同,卻只能探索到1到2條路徑,例如:初始輸入數(shù)組為null,只能探索到路徑:3->4;如果數(shù)組為{1,2,3},則可以探索到2條路徑:3->5->6->9和3->5->6->7。造成這種情況的原因在于:JDart在數(shù)組符號化后,具體執(zhí)行程序一次,收集該條路徑的約束條件時,會檢測到數(shù)組a不是符號值,不能對路徑條件a==null和a.length> 0取反,從而導致JDart執(zhí)行時對這種路徑分支只執(zhí)行了一條路徑。因此,應當對JDart處理數(shù)組的符號化時所存在的問題進行分析和改進,使Jdart測試程序時可以實現(xiàn)如圖4所示的數(shù)組類型程序代碼,遍歷被測程序的所有路徑。

3 分析及優(yōu)化

3.1 問題分析

對JDart的程序代碼進行分析,發(fā)現(xiàn)當被測程序的初始輸入為數(shù)組時,JDart對數(shù)組的符號化是將數(shù)組視為一個字節(jié)數(shù)組,然后將數(shù)組中每個字節(jié)與一個不同的符號量相關聯(lián)實現(xiàn)數(shù)組的符號化的。在上一節(jié)介紹了JDart的執(zhí)行過程,在對測試方法的初始輸入符號化時,當輸入值為對象或數(shù)組,調用processObject()方法進行處理,processObject()中調用的doProcessObject方法會根據對象類型的不同,調用不同的處理器,來決定是否符號化和如何符號化。

JDart根據初始輸入數(shù)組值的長度對數(shù)組符號化,但數(shù)組符號化是定長的。例如:數(shù)組a的初始輸入長度為10,那么JDart就會創(chuàng)建10個符號變量a[0],a[1],…,a[9]。在此情況下,在測試程序執(zhí)行過程中,JDart所收集的約束條件中的數(shù)組元素是有符號值的,但是,數(shù)組本身和數(shù)組長度沒有符號值,對包含數(shù)組本身和數(shù)組長度的約束條件部分,JDart將只能執(zhí)行一條路徑。

3.2 改進策略

只創(chuàng)建一個數(shù)組本身的符號變量a,然后根據數(shù)組的數(shù)據結構性質,用函數(shù)表達式來表示長度和下標。這樣,當JDart在動態(tài)符號執(zhí)行被測程序時,若遇到涉及數(shù)組下標和長度的分支,就可以收集到這些路徑的約束條件,再通過對路徑約束取反,就能實現(xiàn)動態(tài)符號執(zhí)行工具JDart對這些分支條件中2條分支的遍歷,從而可以提高JDart對被測程序的覆蓋率,使錯誤檢測模塊盡量檢測到程序中所有可能的bug。

綜上所述,修改步驟可描述如下:

Step1 在JConstraints中,添加對數(shù)組的支持,將Z3求解器求解出的model中,涉及數(shù)組的模塊解析成數(shù)組形式輸出,使JDart中可以創(chuàng)建對應的數(shù)組類型符號值。

Step2 在JConstraints-Z3中,添加對數(shù)組的支持。JConstraints-Z3的功能主要有3點:①將傳入的約束表達式,轉化為Z3求解器可以識別的Z3斷言形式;②調用Z3求解器提供的API,對轉化后的Z3斷言求解;③對求解出的model進行遍歷,將求解的結果轉化為用戶常見的格式。因為Z3求解器能支持對數(shù)組的求解,因此,僅需針對第一點和第三點進行修改。

Step3 對JDart的數(shù)組符號化進行優(yōu)化。對數(shù)組符號化的優(yōu)化,主要為了使以下3個涉及數(shù)組的分支條件覆蓋到:a==null、a.length>0和a[i]==x。因此,僅從3個方面實現(xiàn)對數(shù)組符號化的優(yōu)化:①在類PrimitiveArrayHandler的annotateObject方法中,直接創(chuàng)建數(shù)組類型符號;②對數(shù)組長度的讀取,修改arraylength指令,在gov.nasa.jpf.jdart.bytecode下新建一個ARRAYLENGTH類,用以繼承jpf-core中重寫的ARRAYLENGTH類,如果數(shù)組是符號值,則生成length表達式;③對數(shù)組元素的讀取,可修改iaload指令,同樣新建一個IALOAD類,來生成item表達式。

4 結果驗證

下面采用經典的三角形程序,對本文上述對數(shù)組符號化改進的效果進行驗證。三角形代碼如圖5所示。

1 public class lnput {

2

3 public static void main(String[]args) {

4 lnput local Test=new lnput();

5 int[]a={2,3,3};

6 localTest.isConstructiveTriangles(a);

7 }

8

9 private void isConstructiveTriangles(int[]a) {

10 if (a[0]

[1]+a[0]) {

11 assert true;

12 } else {

13 assert false;

14 }

15 }

16 }

圖5 判定輸入數(shù)組是否構成三角形代碼

對上述代碼,采用改進前后的JDart程序分別執(zhí)行。表2和表3為2次執(zhí)行遍歷路徑所對應的測試用例,其中PC為每條路徑的約束,Program Input為該路徑所對應的測試輸入。結果表明,改進之前的JDart,對圖8所示的代碼可以探測到4條路徑。而改進之后,則可探測到10條路徑,即該函數(shù)的所有執(zhí)行路徑。因此,實現(xiàn)數(shù)組符號化后,JDart對包含數(shù)組的被測程序,路徑覆蓋率有顯著提高,不僅實現(xiàn)了對數(shù)組為空、長度和下標的判斷,并且對數(shù)組的長度添加了約束,以防止數(shù)組長度過大導致Z3求解出現(xiàn)異常。

表2 JDart優(yōu)化前生成的測試用例

表3 JDart優(yōu)化后生成的測試用例

5 結 論

本文分析了JDart在實際程序測試中所存在的問題,通過對JDart執(zhí)行過程的分析,提出了一種對數(shù)組類型符號化進行優(yōu)化的策略,并在JDart中實現(xiàn)。通過對比優(yōu)化前、后程序測試的結果的比較,驗證了其有效性。本文的優(yōu)化策略可以有效提高JDart對涉及復雜對象程序測試的覆蓋率。

但是,對于字符串、指針、對象等復雜對象的符號化仍存在問題,而且動態(tài)符號執(zhí)行技術對比其他軟件測試技術雖然有顯著的優(yōu)點,但是它仍舊面臨著諸多的挑戰(zhàn),尚有很大的研究空間。

[1] Shamsoddin-Motlagh E. A Review of Automatic Test Cases Generation[J]. International Journal of Computer Applications, 2012, 57(13): 25-29

[2] Zheng W, Hierons R M, Li M, et al. Multi-Objective Optimisation for Regression Testing[J]. Information Sciences, 2016, 334/335: 1-16

[3] Anand S, Burke E K, Chen T Y, et al. An Orchestrated Survey of Methodologies for Automated Software Test Case Generation[J]. Journal of Systems & Software, 2013, 86(8):1978-2001

[4] Cadar C, Sen K. Symbolic Execution for Software Testing: Three Decades Later[J]. Communications of the ACM, 2013, 56(2): 82-90

[5] Stephens N, Grosen J, Salls C, et al. Driller: Augmenting Fuzzing through Selective Symbolic Execution[C]∥NDSS, 2016, 16: 1-16

[6] Yi Q, Yang Z, Guo S, et al. Postconditioned Symbolic Execution[C]∥2015 IEEE 8th International Conference on Software Testing, Verification and Validation, 2015: 1-10

[7] Sobeih A, Marinov D. Optimized Execution of Deterministic Blocks in Java Pathfinder[C]∥International Conference on Formal Methods and Software Engineering, 2006: 549-567

[8] Cadar C, Dunbar D, Engler D R. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs[C]∥OSDI, 2008: 209-224

[11] 周海將, 吳軍華. 基于符號執(zhí)行與混合約束求解的測試用例生成研究[J]. 計算機應用與軟件, 2016, 33(6):23-26

Zhou Haijiang, Wu Junhua. On Test Case Generation Based on Symbolic Execution and Hybrid Constraint Solving. Computer Applications and Software,2016, 33(6):23-26 (in Chinese)

[12] 白曉穎, 黃軍. 基于約束組合的測試用例生成[J]. 清華大學學報:自然科學版, 2017(3):225-233

Bai Xiaoying, Huang Jun. Case Generation by Constraints Combinatorial Testing[J]. Journal of Tsinghua University: Science and Technology, 2017(3):225-233 (in Chinese)