一种基于符号执行的测试用例生成方法

郑华利 刘钊远 田 野

（西安邮电大学计算机学院 西安 710061）

1 引言

软件测试是保证软件正确性、完整性、安全性和质量的主要程序分析方法。相比于覆盖率低的模糊测试［1］，符号执行［2］覆盖率高且应用广泛，然而其本身存在一定的瓶颈，即路径爆炸、约束求解、符号执行精确性三大问题，使得符号执行很难应用到实际的测试环境当中。所谓的路径爆炸问题指的是假如一个实际程序有X个分支语句，那么该程序的路径数是2x个，即程序的路径数量随程序的分支语句数呈指数增长。

目前为止，对于符号执行中的路径爆炸［3～4］问题解决方案有很多，主要包括智能搜索策略［5～6］、摘要、路径合并［7］、修剪冗余路径等。这些解决方案的共同点是只访问或者先访问能够达到测试标准的路径。Chen［8］等提出了几种针对符号执行中的路径爆炸问题进行分析的智能搜索策略，不同的搜索策略存在不同程度的缺陷，例如深度优先搜索算法存在覆盖率低，必须指定最大深度的问题。罗荣森［9］等提出基于符号摘要的动态执行方法，借助函数摘要［10］和符号摘要的思想，对动态符号执行过程中的符号和约束信息进行保存，避免后续对相同的路径进行重复地符号执行，此方法存在存储空间的消耗问题。Kuznetsov［11］等提出的状态合并技术是将不同路径上的路径前缀进行合并，使得搜索路径的数量由指数级增长降低为多项式的增长。RW-set［12］等提出的路径修剪技术通过跟踪程序的读取和写入的内存位置，判断路径是否能够探索到新的程序行为，修剪那些已经探索过能够产生同样效果的执行状态的路径，此方法针对大型应用程序面临着巨大的可扩展性挑战。

因此，为了克服现有的路径爆炸解决方案中存储空间消耗大、只适用于小型程序的缺陷，本文提出一种利用Hoare逻辑中的后置条件引导符号执行的冗余路径删除方法。利用前置条件计算已探索路径的路径条件，在测试用例生成时针对程序共享的路径后缀使用后置条件进行识别，若当前的路径条件合并到后置条件，则此执行路径的其余部分将跳过，在保证覆盖有效的测试用例的情况下，通过冗余路径的删除，减少程序的执行时间，从而达到减轻符号执行的路径爆炸问题的目的。

2 相关理论依据

2.1 符号执行

符号执行的核心思想是将程序输入符号化，利用符号值来代替具体值，对程序进行静态分析，获取代码中的控制流图，在控制流图的基础上生成符号执行树，为程序所有路径建立一系列的以输入数据为变量的表达式，在符号执行树的基础上，将测试数据的生成问题转化为可满足性问题，并使用约束求解器来求解新的测试输入。

2.2 基于Hoare逻辑的符号执行技术

Hoare逻辑［13］的核心特征是Hoare三元组，表示为｛P｝S｛Q｝，其中P、Q均为逻辑公式，前置条件P和后置条件Q是程序S的规约。Hoare三元组表示当S执行前P成立，那么S执行并终止后有Q成立。

在证明程序正确性的过程中，程序中的每一条语句的前后都会有一个变量的逻辑表达式所组成的约束条件，语句中的变量根据程序执行的语义必须满足对应的约束条件。公理语义中使用的逻辑表达式称为谓词或断言，在程序语句前面的谓词是当前语句中变量的约束条件。相反地，在程序语句后面的谓词是语句执行后变量所满足的新约束条件，这些谓词分别称为语句的前置条件和后置条件。在符号分析的过程中，利用已知的后置条件来计算当前语句的前置条件。其中，最弱前置条件是保证后置条件有效的最小前置条件［14］。在实际的分析中，以程序的执行结果作为最后一条语句的后置条件，通过该后置条件和程序最后一条执行语句来计算其最弱前置条件，该前置条件又作为上一条语句的后置条件，以此类推到程序的开始［15］。

对于语句S，前置条件和后置条件分别为P和Q，语句S的最弱前置条件的计算可以通过转换函数wp［S，Q］［16］来获得，在最弱前置条件所遵循的语法规则中，前置条件的计算为

对于分支语句，前置条件的计算为wp（S1 or S2，Q）=wp（S1，Q）∧wp（S2，Q）。在实际的分析过程中，最弱前置条件通过当前语句及其后置条件经过转换函数所计算获得。

3 冗余路径删除方法

3.1 冗余路径删除模型

本文利用Hoare逻辑中的后置条件引导符号执行将程序中的冗余路径进行删除，以生成有效的测试用例。首先将源程序进行LLVM中间语言转换成LLVM字节码，获取初始路径集合。然后使用最弱前置条件计算路径后缀，使用后置条件识别程序运行过程中的共享路径后缀。最后通过约束求解器检查路径条件的可满足性来计算测试输入。具体的冗余路径删除实现模型如图1所示。

图1 冗余路径删除模型

3.2 冗余路径删除实现步骤

本文方法将程序中可能出现的故障利用特殊的中止指令进行表示，考虑到中止可能出现在路径的任何地方，因此检测故障需要覆盖所有有效的执行路径，指令可能是以下类型之一。

skip:（跳过）代表虚拟语句，通常用于省略其他分支；

halt:（停止）代表正常的程序终止；

abort:（中止），代表程序终止失败。

对于程序中的if分支用i（fc）表示，else分支用else表示，也可以用i（f¬c）表示。后置条件引导符号执行的冗余路径删除方法的流程如图2所示。

图2 冗余路径删除实现流程

详细的实现步骤描述如下:

步骤一:设置全局变量post［l］记录每条路径的后置条件，并置为false，初始化路径条件pcon、控制位置l、存储映射mem等信息，利用数据结构中的堆栈来存储符号执行中的程序状态，将初始化的数据进行入栈操作。

步骤二:利用while循环来判断stack是否为空，若不为空，将程序状态中的＜pcon，l，mem＞信息进行出栈操作，并判断路径条件是否满足mem。若满足，则利用for循环遍历控制位置l，去执行指令事件。若stack为空，则直接跳出循环，并结束。

3.3 实例分析

下面以图3为例的程序对本文所提出的方法进行具体说明。

图3 程序实例

针对上述的例子，它有两个输入变量x，y和两个连续的if-else语句。动态符号执行能够计算一组测试输入，每个测试输入都具有所有输入变量的具体值，目的是覆盖程序所有的有效路径。要执行22=4个不同的执行路径，经典的符号执行工具KLEE将产生四个测试输入。编号1到4是本例的覆盖路径如图3所示，P1是通过第一行，第三行的if分支语句。根据观察，许多的路径后缀在不同的测试运行之间共享，反复探索这些路径后缀是路径爆炸的主要原因。

虽然图3中的四条路径不同，但是根据观察发现路径后缀3是由P1和P3共享，路径后缀4是由P2和P4共享，为了避免冗余路径的探索，本文提出了一种利用Hoare逻辑中的后置条件引导符号执行的冗余路径删除方法以生成有效的测试用例。该方法通过检查分支是否被以前的探索所合并，利用最弱前置条件计算总结先前探索的路径，将程序控制位置与后置条件进行关联，在随后新的测试输入过程中，检查当前的路径是否被归入到后置条件中，结果为true，则其余执行路径被跳过，以此来达到消除冗余路径的目的。

对图3中的实例进行符号计算来说明本文所提出方法的主要思想，如表1所示。1～4列展示了标准的符号执行是如何工作的，5～7列展示了在同一个例子上本文提出的方法是如何工作的，以此达到缓解路径爆炸问题的目的。

对于路径1，由于全局变量post［l］还不存在，在计算修剪之后的路径条件时，先假设对于每个位置 post［l］=false。因此，第 1、3行的新路径条件不变，如表1中所示。从该路径的最后一条分支向前扫描，通过最弱前置条件计算其路径后缀，结果如列7所示。对于路径2，第4行修剪之后的路径约束条件和路径1的否定后置条件相关，为m'=m∧¬（x+5＞y），其后置条件变为（x＞y）∨（x≤ y）=true，第1行的修剪后路径条件和后置条件不变仍为x≤0。对于路径3，修剪之后的路径条件为m'=m∧¬true（¬true为第2条路径末尾计算的后置条件的否定）。路径4在我们的方法中被跳过，沿着第3条路径的第3行的else分支就可以到达第4行，第3条路径在执行第3行之前终止，因此路径4将在本文提出的方法中完全跳过，就相当于是一条冗余路径。

表1 图3中实例的符号计算

4 实验与分析

4.1 实验环境设置

为了验证本文所提出的后置条件引导符号执行的冗余路径删除方法，设置实验环境如表2所示。

表2 实验环境和工具

4.2 实验结果

为验证本文所提出的后置条件引导符号执行的冗余路径删除方法的有效性，选择GNU Coreutils软件包中的 expr、uniq、id、nice、touch、tr、unlink、sort、du、ln等十种程序进行实验。

通过最弱前置条件计算先前已探索的路径，利用后置条件引导符号执行在测试生成时进行冗余路径的识别和消除。图4是使用开源工具klee和本文方法针对GUN Coreutils软件包进行符号执行程序的路径数的一个对比。由实验结果图可知，采用本文的方法进行冗余路径的识别和删除，程序的路径数目明显减少了，使得程序覆盖有效的测试用例，减少了冗余路径的覆盖，在一定程度上，削弱了符号执行中的路径爆炸问题，使得程序的“指数级”路径数有所降低，更进一步地证明本文方法的有效性。

由图5可以看出，针对GNU Coreutils软件包分别使用klee和本文方法对每个基准程序的性能进行测试，使用本文方法使得程序的执行时间有所减少，并且符号执行效率得到了显著的提高。当基准程序路径数较小时，KLEE的符号执行的效率和本文方法相比而言，性能变化不是非常明显，但当选取的基准程序路径数较为庞大时，本文所提出的方法符号执行效率明显优于klee的符号执行效率。同样也解决了现有路径爆炸问题方案只适用于程序规模较小的缺陷。

图4 路径数对比

图5 性能对比

5 结语

本文提出了一种利用Hoare逻辑中的后置条件引导符号执行的冗余路径删除方法。该方法使用最弱前置条件对符号执行中已探索过的路径进行计算，在测试用例生成时使用后置条件，对共享的路径后缀进行识别和消除。经实验验证，本文方法在一定程度上减少了程序的路径探索数目和执行时间，缓解了符号执行中的路径爆炸问题。但对于在冗余路径删除方法中存在的计算开销大的问题仍然无法解决，将是下一步工作的研究重点。