基于过程间动态符号执行的C语言测试框架

邵巳航，苏 亭，顾 斌，王 政，杨孟飞

（1.华东师范大学 软件学院，上海200062；2.北京控制工程研究所，北京100080）

0 引 言

目前，工业界仍旧主要采用人工手动编写测试用例的方法。但由于软件规模的不断扩大，测试的人力和成本也随之上升。在此背景下，一系列自动化生成测试用例的工具得到了研究和发展，以辅助测试人员。

动态符号执行是自动化生成测试用例的方法之一，能通过程序实际运行时的实际值信息提高符号执行的可行性。根据测试的需求粒度不同，可以划分为过程内和过程间。现有的工具包括DART［1］，KLEE［2］，PEX［3］等。

本文贡献如下：基于一套过程间数据流分析方法（SMART 算法），在相关项目工具实现的基础上，针对C语言进行研究，建立了一套详细可行的过程间动态符号执行模型；解决了过程间调用时实参和形参变量的符号统一问题；对SMART 算法进行改进，使其在实际应用中能更准确地计算函数摘要。

1 动态符号执行

在自动化生成测试用例的研究中，符号执行是一种可行性较高的方法。主要思想是通过程序初始的随机输入，由负责监控的插桩代码收集路径上的符号约束，然后根据不同的路径选择策略生成新的路径约束，通过约束求解器进行求解，从而在下次迭代中使程序转入新的分支，最后根据相应的覆盖标准或特定条件终止测试［4］。

然而，由于实际程序的符号约束有时并不能被约束求解器求解，例如当遇到源代码不可得的函数调用，动态符号执行正是为了有效解决这类问题而被提出。它在传统的符号执行中利用符号的实例化提高了可行性，即动态地运行被测程序，当动态符号执行遇到某些不可求解的输入时，就使用它的运行时实际值来化简约束，再进行求解，从而使测试能尽可能覆盖更多的分支和路径［5］。

1.1 过程间动态符号执行

在白盒测试中，传统的过程间动态符号执行算法在遇到函数调用时每次都会跟进被调函数体内，进而收集分支上的约束。虽然这样可以保证尽可能覆盖被测程序分支，但由于实际被测的程序规模较大，加上频繁的函数调用，很容易造成路径爆炸的现象，使得过程间的动态符号执行可行性不高，效率下降。为解决路径爆炸的问题，T.Reps等人［6］曾提出在静态的过程间数据流分析中缩减问题规模的方法，后来P.Godefroid等人［7］在此基础上，引入SMART 算法，利用静态分析中类似的思想，对被调函数隔离地进行测试，收集函数的输入 （前置条件）和输出（后置条件）作为函数的摘要 （summary），以后调用时即可复用这些信息来收集约束，无需再重新搜索函数内部的路径，从而大大减少了问题规模和迭代次数，提高了测试效率。本文正是基于SMART 算法，针对C 语言论述了一套详细的过程间符号执行框架，并对其进行建模和实现。

1.2 CAUT

CAUT （C analysis and unit testing toolkit）是本文依托项目所实现的动态符号执行测试工具。它针对C 语言，以白盒测试覆盖目标为驱动，虽然主要面向以过程内单元测试为需求的客户，但设计时仍然考虑了过程间测试的功能。CAUT 作为面向自动化测试而开发的工具，可以分为前端和后端2部分，其中前端负责对C 语言被测代码做变形、化简和自动插桩等前期预处理，与动态符号执行有关的设计和算法集中在后端［8，9］。

CAUT 后端可以分为3个模块：①测试执行模块：负责收集程序运行期间变量的符号值赋值变化，分支上的约束等运行时信息。②约束求解模块：针对选择出来的路径收集分支上的约束，并对C 语言特有的约束进行化简，最后将符合约束范式的约束传递给约束求解器进行求解，CAUT 采用微软的Z3［10］可满足性求解器作为求解工具。③路径选择模块：负责在每次测试执行完毕之后，结合被测程序覆盖标准需求和相应的路径选择策略，生成一条新的路径并传递给约束求解模块进行求解。

2 SMART算法

SMART （systematic modular automated random testing），是由Patrice Godefroid等人提出的过程间动态符号执行算法。其核心的思想是隔离地对待程序中每一个函数，根据每次函数调用时参数的实际值来计算或者使用函数摘要，从而减少符号执行的迭代次数，提高执行效率和实际应用的可行性［7］。

2.1 函数摘要

若给定函数f，w 是其任意一条执行路径，cwi为路径上跟函数输入有关的约束，cwo为路径上跟函数输出有关的约束，令

则函数f 在路径w 上的摘要 （summary）为

若W ＝ ｛w1，w2，…，wn｝是函数f 所有执行路径的集合，则函数f 的摘要为

以表1所示程序代码中的函数f 为例，由于f 只有2条执行路径，所以f 的摘要为 （x＞0∧ret＝1）∨ （x＜＝0∧ret＝0），其中ret为函数f 的返回值符号。

表1 示例代码1

2.2 SMART算法

SMART 算法的重点在于计算函数摘要，设集合I 为函数f 的输入，concrete（I）为输入的实际值，summary（f）为函数f 的摘要，C 为程序的约束集合，backtracking为判断是否追溯的标志。则其算法框架见表2。

由算法描述可知，当程序遇到函数f 调用时，会首先检验实参传入的实际值是否满足f 的摘要，如果f 当前有摘要可用，直接将摘要添加到当前约束中，并将追溯标志设为0，这样程序就不再收集f 函数体内的约束；如果f当前无摘要可用，说明本次迭代需要计算新的摘要，设追溯标志为1，对f 函数体内的每个分支上的约束进行收集，当f 返回后，将收集到的约束和返回值添加到f 的摘要中，然后继续搜索f 的下一条路径。当f 搜索完毕之后，函数摘要也就计算完成。

表2 SMART 算法

3 基于SMART算法的CAUT模型

3.1 Def－Use链

定义－使用链［11］（definition－use chain，Def－Use链），是一种经典的数据流分析结构，实际上由2个链表组成，分别按顺序存放所有的变量使用和定义情况。CAUT 正是基于此类方法分析运行时变量的符号值变化，其算法见表3。

表3 CAUT 的Def－Use算法

以表1所示C 语言代码为例，CAUT 模型将分别对每个函数维护一个Def－Use链，如果一次动态实际执行中top函数的形参取w＝1，y＝1，那么其Def－Use链将会见表4。

表4 top 函数形参取w＝1，y＝1时的Def－Use链情况

即取得函数f 当前摘要的符号表达式： （x＞0）∧（return＿symbol＿f＝1）。以后使用该摘要时，只需要根据实参和形参的对应关系，如y 对应x，即可替换成调用点所在函数的符号，即 （y＞0）∧ （return＿symbol＿f＝1）。算法以函数为单位正确收集了分支上的约束条件，由于调用函数时保存了实参和形参的对应关系，从而解决了在过程间符号执行期间，约束求解变量的符号统一问题。

3.2 扩展的执行树

由于SMART 算法需要隔离对待每个被测函数，所以本文对传统的执行树定义进行扩展。

扩展的执行树定义：

（1）执行树是二叉树，根节点代表每个函数的入口。

（2）叶子节点表示函数的一条路径。

（3）非叶子节点包括2种节点类型：分支条件和函数调用。

（4）分支条件节点的假分支节点表示该路径下条件取假，真分支节点表示该路径下条件取真。

（5）函数调用节点的假分支节点为调用点之后的分支条件节点，真分支节点为被调函数的根节点。

以表1所示程序代码为例，如果一次动态实际执行中top 函数的形参取w＝1，y＝1，那么其经过扩展后的执行树如图1所示。函数top 的执行树由实线节点组成，函数f的执行树由虚线节点组成。由此可见，本文提出的执行树不但能隔离地表示各个函数的执行情况，而且同时保存了函数调用的信息，从而为SMART 算法提供了模型基础。

3.3 改进后的SMART算法

图1 top 函数的形参取w＝1，y＝1时程序的执行树

观察表5所示代码，按照SMART 算法，由于第3 行有y＞0的约束条件，第4行的函数调用只会产生 （x＞0）∧ （return＿symbol＿f＝1）一条摘要，如果下一次迭代中函数的输入w 随机取到1，由于SMART算法只检验w 的实际值是否满足当前函数摘要，结果导致第5行的函数调用并没有如预期产生相应的函数摘要 （x＜＝0）∧ （return＿symbol＿f＝0）（实际上w 此时是可以取小于等于0的值）。

表5 示例代码2

所以，在实际执行中，为了获得更精确的函数摘要，在遇到函数调用时，还需要结合实参当前的取值范围来判断是否可以生成新的函数摘要。基于CAUT 的扩展执行树模型，对SMART 改进后的算法描述见表6，其中calling＿context（f）为调用函数f 前的约束集合，current＿node为当前执行树路径上的节点，choice为分支的选择。

算法的本质实际上是一个构造程序执行树的过程，当程序遇到函数f 调用时，首先在当前执行树路径上添加一个函数f 的调用节点calling＿node，然后检验参数的实际值是否满足函数f 摘要，如果不满足，设置追溯标记backtracking＝1；如果参数实际值能满足，此时仍不能保证当前摘要可用，需要对f 执行树上每条不可达的路径结合此次调用实参的取值范围calling＿context（f）进行求解，如果有解，说明此次调用仍可以产生新的摘要，将此解I’作为程序输入，进入下一次迭代。如果无解，表示此次调用确实不能生成新的摘要，将f 的函数摘要作为约束保存到calling＿node，设置追溯标记backtracking＝0。如此便可确保每次函数摘要都能被充分计算。

表6 补充后的SMART 算法

当程序遇到函数f 体内的分支语句时，会根据追溯标志backtracking 来判断是否需要继续构造执行树。如果backtracking＝1，说明正在计算函数新的摘要，函数f 返回时，将此次f 执行树路径上的约束集合和返回值作为新的摘要保存，然后对f 的执行树深度优先搜索新的路径，把无解的节点标记为当前不可达路径，对有解的路径，则将其解作为程序的输入进入下一次迭代，直到f 的执行树搜索完毕。

4 应用和实验

4.1 应用实例

表7的被测函数test（）为例，本文将使用SMART 算法和基于CAUT 模型改进后的SMART 算法分别进行动态符号执行自动化测试。

表7 被测函数test（）

SMART 算法的测试结果见表8，根据生成的函数摘要来看，测试并没有覆盖程序第11行和第17行的分支路径。

表8 SMART 算法的测试结果

基于CAUT 模型改进后的SMART 测试结果见表9，由于在判断函数摘要的过程中结合了参数的当前约束，所以能更准确地计算摘要，最终覆盖了被测函数的全部路径。

4.2 实验分析

首先对本文出现的3段示例代码做实验分析。测试结果见表10。

表9 改进后的SMART 算法的测试结果

表10 示例代码实验结果

其中表1代码是简单的过程间调用例子，2种算法都能做到完全分支覆盖；表5代码是为了测试算法是否能精确计算函数摘要而设计的，SMART 由于只采用形参实际值来检验函数摘要是否可用，导致函数摘要计算受形参随机值影响，未能覆盖被调函数的所有分支。而改进的SMART 算法由于考虑了形参的当前约束，所以排除了随机情况的影响，覆盖了被调函数的所有分支；表7代码是为了测试上述随机情况对程序后续分支的影响，SMART由于没有精确计算函数摘要，影响了后续代码的分支覆盖情况。改进的SMART 算法则能正常覆盖调用点之后的分支。

本文实验的被测项目对象主要来自SIR［12］，从中选取了bash，flex和make这3个开源项目，实验结果见表11。实验目的是检测CAUT 在基于改进前后的SMART 算法上针对分支覆盖标准的支持度。从结果中可以看到，虽然SMART 算法已经能对程序提供较好的覆盖率，但改进后的算法仍然提高了原先的覆盖率，原因主要是在判断函数摘要是否可用的过程中结合了参数的当前约束，所以能更准确地计算摘要。

表11 被测项目指标及实验结果

5 结束语

本文介绍了自动化测试用例生成技术中动态符号执行的基本概念和原理，并基于SMART 的过程间数据流分析算法，在相关项目工具CAUT 的实现基础上，针对C 语言进行研究，建立了一套详细可行的过程间动态符号执行模型，解决了过程间调用时实参和形参变量的符号统一问题，同时对SMART 算法进行改进，使其在实际应用中能更准确地计算函数摘要。

动态符号执行将在未来一段时间内成为自动测试理论研究的主流框架，而如何在C 语言的过程间动态符号执行中处理指针和复杂内存操作的函数摘要模型将会是本文未来的工作方向。

［1］Godefroid P，Klarlund N，Sen K.Dart：Directed automated random testing ［C］／／Proceedings of the 5th International Haifa Verification Conference on Hardware and Software：Verification and Testing，2009.

［2］Cadar C，Dunbar D，Engler D.Klee：Unassisted and automatic generation of high－coverage tests for complex systems programs［C］／／Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation， 2008：209－224.

［3］Tillmann N，Halleux J De.Pex：White box test generation for net［C］／／Proceedings of the 2nd International Conference on Tests and Proofs，2008：134－153.

［4］Person S，Yang G，Rungta N，et al.Directed incremental symbolic execution ［C］／／Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation，2011：504－515.

［5］Cadar C，Godefroid P，Khurshid S，et al.Symbolic execution for software testing in practice：Preliminary assessment［C］／／New York：Proceedings of the 33rd International Conference on Software Engineering，2011：1066－1071.

［6］Xu Guoqing，Rountev A.AJANA：A general framework for source－code－level inter procedural dataflow analysis of aspect software［C］／／Proceedings of the 7th International Conference on Aspect－Oriented Software Development，2008：36－47.

［7］Godefroid P.Compositional dynamic test generation ［J］.ACM SIGPLAN Notices，2007，42 （1）：47－54.

［8］Yu Xiao，Sun Shuai，Pu Geguang，et al.A parallel approach to concolic testing with low－cost synchronization ［C］／／Proc the 4th International Wokshop on Harnessing Theories for Tool Support in Software，2010：83－96.

［9］Wang Zheng，Yu Xiao，Sun Tao，et al.Test data generation for derived types in C program ［C］／／Proc the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering，2009：155－162.

［10］ Moura L de，Bjrner N.Z3：An efficient SMT solver［C］／／Proceedings of Tools and Algorithms for the Construction and Analysis of Systems，2008：337－340.

［11］Stanier J，Watson D.Intermediate representations in imperative compilers：A survey ［J］.ACM Computing Surveys，2013，45 （3）：1－26.

［12］Bertolino A.Software testing research：achievements，challenges，dreams ［C］／／Future of Software Engineering，2007：85－103.