基于JDart的測(cè)試用例自動(dòng)生成與優(yōu)化

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

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

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

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

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

1 基于符號(hào)執(zhí)行的測(cè)試用例生成

符號(hào)執(zhí)行是一種可靠、經(jīng)典的白盒測(cè)試用例生成方法。其基本原理是將程序中變量值用符號(hào)標(biāo)記替換,并以符號(hào)值模擬程序執(zhí)行的過(guò)程。基于符號(hào)執(zhí)行的測(cè)試用例生成方法,主要通過(guò)計(jì)算每條符號(hào)執(zhí)行路徑所需要滿足的約束條件,來(lái)得到測(cè)試輸入。

1.1 相關(guān)定義

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

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

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

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

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

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

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

1.2 測(cè)試生成過(guò)程

符號(hào)執(zhí)行的核心思想,是用抽象化的符號(hào)表示程序中的具體輸入變量;通過(guò)解析程序的語(yǔ)句,為每條路徑生成路徑表達(dá)式,來(lái)生成符號(hào)執(zhí)行樹(shù),并通過(guò)對(duì)路徑表達(dá)式進(jìn)行求解獲得符號(hào)變量解的集合[7]。例如對(duì)于圖1所示的待測(cè)示例代碼,通過(guò)符號(hào)執(zhí)行分析,可以得到符號(hào)執(zhí)行語(yǔ)法樹(shù)如圖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 示例代碼

通過(guò)該語(yǔ)法分析樹(shù),可以得到程序執(zhí)行路徑、路徑約束條件以及對(duì)應(yīng)的輸入,如表1所示。這就是一個(gè)簡(jiǎn)單的基于符號(hào)執(zhí)行的測(cè)試用例生成過(guò)程。

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

圖2 符號(hào)執(zhí)行樹(shù)

2 基于JDart的測(cè)試用例生成

2.1 JDart工具簡(jiǎn)介

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

2.2 JDart測(cè)試用例生成機(jī)制

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

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

Step2 在類ConcolicMethodExplorer的initialize

Method()函數(shù)中,調(diào)用函數(shù)initializeSymbolicParams(),對(duì)測(cè)試方法輸入值符號(hào)化。

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

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

2.3 存在問(wèn)題

JDart實(shí)現(xiàn)了基本的測(cè)試用例生成思路和框架。但是,對(duì)于許多具體的數(shù)據(jù)類型(如對(duì)象、數(shù)組、字符串等)還無(wú)法支持。圖3是一個(gè)簡(jiǎn)單的包含數(shù)組的程序,圖4展示該程序預(yù)期的執(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 測(cè)試程序代碼

圖4 預(yù)期路徑

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

3 分析及優(yōu)化

3.1 問(wèn)題分析

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

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

3.2 改進(jìn)策略

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

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

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

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

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

4 結(jié)果驗(yàn)證

下面采用經(jīng)典的三角形程序,對(duì)本文上述對(duì)數(shù)組符號(hào)化改進(jìn)的效果進(jìn)行驗(yàn)證。三角形代碼如圖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ù)組是否構(gòu)成三角形代碼

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

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

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

5 結(jié) 論

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

但是,對(duì)于字符串、指針、對(duì)象等復(fù)雜對(duì)象的符號(hào)化仍存在問(wèn)題,而且動(dòng)態(tài)符號(hào)執(zhí)行技術(shù)對(duì)比其他軟件測(cè)試技術(shù)雖然有顯著的優(yōu)點(diǎn),但是它仍舊面臨著諸多的挑戰(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] 周海將, 吳軍華. 基于符號(hào)執(zhí)行與混合約束求解的測(cè)試用例生成研究[J]. 計(jì)算機(jī)應(yīng)用與軟件, 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] 白曉穎, 黃軍. 基于約束組合的測(cè)試用例生成[J]. 清華大學(xué)學(xué)報(bào):自然科學(xué)版, 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)