基于JDart的测试用例自动生成与优化

吴潇雪, 郑炜, 王培源, 王培甲, 樊宋宇

(1.西北工业大学 自动化学院, 陕西 西安 710072; 2.西北工业大学 软件与微电子学院, 陕西 西安 710072)

作为软件测试工作重要内容的测试用例生成,是影响软件测试效果的重要环节,测试用例的自动产生,对保证测试质量、提高测试效率至关重要[1-2]。其中,符号执行引起了广泛关注[3-5],并产生许多开源的符号执行工具[6],诸如CUTE/jCUTE、CREST、JPathFinder[7]、KLEE[8]、SPF以及JDart[9-10]等。面向C的符号执行工具,大多依赖于较为成熟的LLVM平台和KLEE,发展较为迅速,在工业界也得到广泛应用。而面向Java语言的符号执行技术则发展相对较慢,尚处于探索阶段。可靠且高效的面向Java程序的测试用例生成技术和工具亟待开发。

JDart[10]是一款较为成功的面向JAVA的符号执行工具,它提供了良好的模型和框架。然而,目前JDart只能支持基本简单的数据类型,如Int、Char的符号化,而对于复杂数据类型如Array、String、Object等还无法进行符号化,因而影响了其推广和应用。

本文根据对JDart工具及动态符号技术的研究和应用,通过对JDart测试用例生成能力和所存在问题进行了深入剖析,针对数组符号化和约束求解,给出改进和优化策略,以提高生成测试用例的覆盖率,保证测试工作的质量。

1 基于符号执行的测试用例生成

符号执行是一种可靠、经典的白盒测试用例生成方法。其基本原理是将程序中变量值用符号标记替换,并以符号值模拟程序执行的过程。基于符号执行的测试用例生成方法,主要通过计算每条符号执行路径所需要满足的约束条件,来得到测试输入。

1.1 相关定义

为了便于讨论,我首先列出与符号执行测试用例生成相关的定义[11-12]。

定义1待测系统SUT(system under test)。给定n个称之为待测软件的参数pi(i=1,2,…,n)。这些参数可能代表系统的配置参数、内部实践或者用户输入。

定义2路径条件PC(path condition)。汇积了执行某条路径中每一条语句必须满足的约束,不可达路径的执行路径定义为PU。

定义3(约束集C)设由对源程序进行符号执行所得到的路径集合为C={c1,…ci,…,cn},则称C为约束条件集合,其中cn表示某个具体的路径条件表达式,n为约束条件的总数。

定义4(约束PC)对关于数值的路径条件,定义为数值约束NPC;对关于字符串的约束,定义为字符串约束SPC;对PC中既包含数值约束又包含字符串约束,则称该PC为混合约束条件HPC。

定义5(测试输入T)由NPC求解所得到的值称为关于数值约束条件的测试输入,定义为TN;由SPC求解所得到的值称为关于字符串约束条件的测试输入,定义为TS;相应的TN和TS的集合即为关于该执行路径的测试输入T。

定义6(求解过程S)将对约束条件结合进行求解的过程记为S,其中S的输入是约束条件集合,输出为测试输入集合与不可达路径条件,可写成S(C)=TANDPU,式中C={c1,…ci,…,cn};T={T1,…Ti,…,TN}。

1.2 测试生成过程

符号执行的核心思想,是用抽象化的符号表示程序中的具体输入变量;通过解析程序的语句,为每条路径生成路径表达式,来生成符号执行树,并通过对路径表达式进行求解获得符号变量解的集合[7]。例如对于图1所示的待测示例代码,通过符号执行分析,可以得到符号执行语法树如图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 示例代码

通过该语法分析树,可以得到程序执行路径、路径约束条件以及对应的输入,如表1所示。这就是一个简单的基于符号执行的测试用例生成过程。

表1 路径条件、路径、以及生成输入

图2 符号执行树

2 基于JDart的测试用例生成

2.1 JDart工具简介

JDart[7]是一个面向Java的动态符号分析框架,采用模块化架构。其中,执行动态探索的主要组件与有效构建约束的组件进行通信,并与约束求解器进行接口通信。这些组件可以轻松扩展或修改,以支持多个约束求解器或不同的探索策略。此外,连同其最近的开源,使JDart成为研究和实验的理想平台。在当前版本中,JDart支持CORAL,SMTInterpol和Z3求解器,并能处理包含位操作、浮点算术和复杂算术运算(例如,三角和非线性计算)的约束求解器。

2.2 JDart测试用例生成机制

用动态符号执行工具JDart测试程序时,还需要2个辅助工具:JConstraints和JConstraints-Z3。符号执行工具在执行过程中需要使用约束求解器对收集到的约束条件求解,JDart中常用的约束求解器是Z3,而Z3求解器为了提高求解的效率,对常用的数据类型定义了独特的数据结构变量。因此,想要使用Z3求解器,需要使用Z3求解器提供的API接口,将收集到的约束条件中的变量和常量转化为Z3求解器中的数据形式。动态符号执行工具Jdart的工作流程如下:

Step1 初始化被测程序代码模块,创建一个新的任务。

Step2 在类ConcolicMethodExplorer的initialize

Method()函数中,调用函数initializeSymbolicParams(),对测试方法输入值符号化。

Step3 创建符号值。对于基本数据类型,直接创建符号值。对于对象或数组等复杂数据类型时,调用processObject()方法进行处理,在processObject()方法中,进行符号值创建。

Step4 收集约束条件并进行约束求解。收集被测程序中的分支条件作为路径约束,将路径约束添加到约束集合中,按深度优先路径调度策略对约束集合中的某一项或几项取反,得到路径树上下一条路径的约束集合,然后调用JConstraints-Z3中的add()方法,将路径约束转化为Z3求解器可以识别的约束条件,并将其添加到约束求解器中,最后调用solve()函数对约束集合求解,得到下一条路径的输入值。并依次执行,直到遍历被测程序所有路径的执行。

2.3 存在问题

JDart实现了基本的测试用例生成思路和框架。但是,对于许多具体的数据类型(如对象、数组、字符串等)还无法支持。图3是一个简单的包含数组的程序,图4展示该程序预期的执行路径。

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 预期路径

理论上,动态符号执行测试时会遍历程序所有4条路径,如图4所示。但是, JDart根据初始输入数组值的不同,却只能探索到1到2条路径,例如:初始输入数组为null,只能探索到路径:3->4;如果数组为{1,2,3},则可以探索到2条路径:3->5->6->9和3->5->6->7。造成这种情况的原因在于:JDart在数组符号化后,具体执行程序一次,收集该条路径的约束条件时,会检测到数组a不是符号值,不能对路径条件a==null和a.length> 0取反,从而导致JDart执行时对这种路径分支只执行了一条路径。因此,应当对JDart处理数组的符号化时所存在的问题进行分析和改进,使Jdart测试程序时可以实现如图4所示的数组类型程序代码,遍历被测程序的所有路径。

3 分析及优化

3.1 问题分析

对JDart的程序代码进行分析,发现当被测程序的初始输入为数组时,JDart对数组的符号化是将数组视为一个字节数组,然后将数组中每个字节与一个不同的符号量相关联实现数组的符号化的。在上一节介绍了JDart的执行过程,在对测试方法的初始输入符号化时,当输入值为对象或数组,调用processObject()方法进行处理,processObject()中调用的doProcessObject方法会根据对象类型的不同,调用不同的处理器,来决定是否符号化和如何符号化。

JDart根据初始输入数组值的长度对数组符号化,但数组符号化是定长的。例如:数组a的初始输入长度为10,那么JDart就会创建10个符号变量a[0],a[1],…,a[9]。在此情况下,在测试程序执行过程中,JDart所收集的约束条件中的数组元素是有符号值的,但是,数组本身和数组长度没有符号值,对包含数组本身和数组长度的约束条件部分,JDart将只能执行一条路径。

3.2 改进策略

只创建一个数组本身的符号变量a,然后根据数组的数据结构性质,用函数表达式来表示长度和下标。这样,当JDart在动态符号执行被测程序时,若遇到涉及数组下标和长度的分支,就可以收集到这些路径的约束条件,再通过对路径约束取反,就能实现动态符号执行工具JDart对这些分支条件中2条分支的遍历,从而可以提高JDart对被测程序的覆盖率,使错误检测模块尽量检测到程序中所有可能的bug。

综上所述,修改步骤可描述如下:

Step1 在JConstraints中,添加对数组的支持,将Z3求解器求解出的model中,涉及数组的模块解析成数组形式输出,使JDart中可以创建对应的数组类型符号值。

Step2 在JConstraints-Z3中,添加对数组的支持。JConstraints-Z3的功能主要有3点:①将传入的约束表达式,转化为Z3求解器可以识别的Z3断言形式;②调用Z3求解器提供的API,对转化后的Z3断言求解;③对求解出的model进行遍历,将求解的结果转化为用户常见的格式。因为Z3求解器能支持对数组的求解,因此,仅需针对第一点和第三点进行修改。

Step3 对JDart的数组符号化进行优化。对数组符号化的优化,主要为了使以下3个涉及数组的分支条件覆盖到:a==null、a.length>0和a[i]==x。因此,仅从3个方面实现对数组符号化的优化:①在类PrimitiveArrayHandler的annotateObject方法中,直接创建数组类型符号;②对数组长度的读取,修改arraylength指令,在gov.nasa.jpf.jdart.bytecode下新建一个ARRAYLENGTH类,用以继承jpf-core中重写的ARRAYLENGTH类,如果数组是符号值,则生成length表达式;③对数组元素的读取,可修改iaload指令,同样新建一个IALOAD类,来生成item表达式。

4 结果验证

下面采用经典的三角形程序,对本文上述对数组符号化改进的效果进行验证。三角形代码如图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 判定输入数组是否构成三角形代码

对上述代码,采用改进前后的JDart程序分别执行。表2和表3为2次执行遍历路径所对应的测试用例,其中PC为每条路径的约束,Program Input为该路径所对应的测试输入。结果表明,改进之前的JDart,对图8所示的代码可以探测到4条路径。而改进之后,则可探测到10条路径,即该函数的所有执行路径。因此,实现数组符号化后,JDart对包含数组的被测程序,路径覆盖率有显著提高,不仅实现了对数组为空、长度和下标的判断,并且对数组的长度添加了约束,以防止数组长度过大导致Z3求解出现异常。

表2 JDart优化前生成的测试用例

表3 JDart优化后生成的测试用例

5 结 论

本文分析了JDart在实际程序测试中所存在的问题,通过对JDart执行过程的分析,提出了一种对数组类型符号化进行优化的策略,并在JDart中实现。通过对比优化前、后程序测试的结果的比较,验证了其有效性。本文的优化策略可以有效提高JDart对涉及复杂对象程序测试的覆盖率。

但是,对于字符串、指针、对象等复杂对象的符号化仍存在问题,而且动态符号执行技术对比其他软件测试技术虽然有显著的优点,但是它仍旧面临着诸多的挑战,尚有很大的研究空间。

[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] 周海将, 吴军华. 基于符号执行与混合约束求解的测试用例生成研究[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)