5.5　符号执行

符号执行（Symbolic Execution）是指使用符号值而非具体值或特定值，代替真实值作为输入，将运算过程逐语句或逐指令转换为数学表达式，生成基于控制流图的符号执行树，为每条路径建立以输入数据为变量的符号表达式，执行过程中产生关于输入符号的代数表达式。每一步的状态包括路径条件、程序计数器、程序变量的符号值。路径条件是基于程序变量的布尔型表达式，由输入变量符号值和程序中间变量符号组成的不等式集合，记录程序每一步输入必须满足的约束。当程序满足约束条件时，沿着路径条件规定的路径运行，程序计数器定义下一个需要执行的语句，将符号执行的每一步状态结合起来，产生一个符号执行树，即路径条件树，刻画程序运行的所有路径。符号执行在静态执行代码的同时，将所有中间变量替换成由初始输入变量组成的表达式，当程序执行后得到对应于路径的不同不等式组，不等式组中的变量全部为初始输入变量，其解空间就是满足当前路径的测试用例集，如果不等式组的解空间不存在，即当前路径不可达，将测试用例生成问题转变成约束求解问题，可以精确地找出满足约束条件的测试用例即不可达路径。

对于给定程序，符号执行旨在探索尽可能多的不同程序路径，对于每条路径，生成一个输入集合，检查程序是否存在错误。符号执行适用于程序路径检查、程序证明、程序简约、符号调试等不同场合。符号执行包括变量替换、表达式简化、约束条件求解3个过程。

5.5.1　符号执行原理

符号执行分为前向扩展与后向回溯执行。虽然执行方式不同，但其原理相同，都是用来找出覆盖不同路径的测试用例及不可达路径。符号执行的原理及基本过程如图5-24所示。

5.5.1.1　前向扩展

前向扩展符号执行是从程序初始状态入手，由前向后，对程序进行顺序分析。例如，对于如下代码，在执行过程中，对变量x、y输入实际值，如3和2，x−y>0。在符号执行过程中，如果变量x、y分别赋以符号值X、Y，且X>Y成立，x最后得到的值为X，y最后得到的值为Y。

图5-25是上述代码符号执行后所产生的路径条件树，方框表示程序状态，箭头表示状态间的转换。

初始状态下，当路径条件（Path Condition，PC）为“真”时，对x、y分别赋以符号值X和Y，在每一个分支上，路径条件不断扩展。例如，在语句S1中，根据输入的符号值X和Y，路径条件扩展为2条不同的执行路径。

如果X>Y，执行左边的路径，如果X≤Y ，执行右边的路径。在语句S2，将A的符号值替换为X≤Y 。对于语句S3，x=(X+Y)−Y ，经简化后，x = Y。同理，对于语句S4，y的符号值替换为X。该程序共有3条不同路径，对应于3个不同路径条件，即3个表达式组，分别为

其中，第一个不等式组无解，即其对应路径不可达。

每一个不等式组对应路径条件树中的一条路径，即一个等价类。3个等价类如下：

（1）等价类1：执行路径S1、S2、S3、S4、S5、S6，路径条件为 。

（2）等价类2：执行路径S1、S2、S3、S4、S5、S6，路径条件为 。

（3）等价类3：执行路径S1，路径条件为 。

5.5.1.2　后向回溯

后向回溯符号执行是当程序状态已知时，自后向前，从程序的某一条语句出发，找出到达特定状态的程序路径以及路径的约束条件，聚焦于一条路径上，从路径的最后一个目标状态开始，沿着路径的每一节点（状态）自后向前进行搜索，直至回溯到程序的初始状态。在此过程中，不断地对变量进行替换和简化，得到该路径的路径条件，通过求解由路径条件组成的不等式组，进而得到覆盖该路径的输入。对于本章5.5.1.1节给出的代码，图5-26描述了其对应的后向回溯符号执行过程。

回溯算法是一种类似于枚举的选优搜索方法。针对所给出的问题，定义至少包含一个最优解的问题解空间，确定易于搜索的解空间结构，以深度优先方式等系统地搜索整个解空间，在搜索过程中使用剪枝函数可避免无效搜索。

使用约束函数在扩展节点处剪去不满足约束条件的子树，使用分支限界函数剪去得不到最优解的子树，避免无效搜索。这两类函数称为剪枝函数。剪枝函数给出每个可行节点相应的子树，获得最大价值的上界，如果上界不大于当前最优值，则说明相应子树中不含问题的最优解，可以剪去。

另外，将上界函数确定的每个节点的上界值作为优先级，以该优先级的非增序抽取当前扩展节点，该策略可以更加迅速地找到最优解。 剪枝用以减少极小化极大算法搜索树的节点数，是分支界限类算法，也是一种对抗性搜索算法，能够减少搜索树分枝，将搜索时间用在“更有希望”的子树上，提高搜索深度。

使用后向回溯查找语句S6的路径及路径条件，说明后向回溯符号执行的工作方式。初始状态下，语句为S6，路径条件为“真”，向后回溯到语句S5，路径条件变为 。在语句S4遇到赋值语句 ，用符号值替换当前路径条件中的Y，PC变为 ；同理，回溯到语句S2后，变量x的符号值为Y，变量y的符号值为X，PC为 。该路径条件所组成的不等式组无解，说明语句S6的路径S1、S2、S3、S4、S5、S6不可达。

5.5.2　符号执行技术

5.5.2.1　经典符号执行

符号执行的主要思想是将输入用符号而非具体值进行表征，同时将程序变量表征为符号表达式，程序输出则被表征为一个输入的函数。在时间和计算等资源足够的情况下，遍历目标程序的所有路径，判断其可达性。

对于符号执行，首当其冲的是将一个程序的所有执行路径表征为一棵执行树。关于程序执行路径的执行树表示，限于篇幅，在此不介绍。感兴趣的读者可以参考相关文献。这里仅根据图5-27给出的示例，讨论通过符号执行遍历程序执行树的过程。

在图5-27（a）所示代码中，函数testme()有3条执行路径，可以将其转化为如图5-27（b）所示的执行树，即将该程序的所有执行路径表征为一棵执行树。从直观上看，只要能够给出3个输入，就可以遍历此3条路径，即图5-27（b）中灰色填充方框中x和y的取值。符号执行的目标就是生成这样的输入集合，在给定的时间内，探索所有路径。

确定解空间结构后，从根节点出发，以深度优先方式搜索整个解空间。开始节点称为一个活节点，同时也是当前的扩展节点。在当前扩展节点处，搜索向纵深方向移至一个新节点，这个新节点成为一个新的活节点，同时成为当前扩展节点。如果在当前扩展节点处不能继续向纵深方向移动，则当前扩展节点成为死节点。此时，向回移动即回溯至最近的一个活节点处，使该活节点成为当前的扩展节点。后向回溯法就是以这种方式在解空间中进行递归搜索，直至找到所要求的解或解空间中不再有活节点为止。

为了形式化地完成此任务，符号执行在全局维护两个变量。其一是符号状态$\sigma$，它是一个从变量到符号表达式的映射；其二是符号化路径约束PC，是一个无量词的一阶公式，用来表示路径条件。

在符号执行开始时，符号状态$\sigma$初始化为一个空的映射，而符号路径约束PC初始化为true。$\sigma$和PC在符号执行过程中会不断更新。在符号执行结束时，PC用约束求解器进行求解，以生成实际的初始值。这个实际的输入值如果用程序执行，就会走符号执行过程探索的那条路径，即此时PC的公式所表示的路径。

对于函数testme()，当符号执行开始时，符号状态$\sigma$为空，符号路径约束为true。当遇到第一条读语句，其形式为var=sym_input()，即接收程序输入，符号执行会在符号状态$\sigma$中加入一个映射$var\rightarrow s$。其中，s是一个新的未约束的符号值。main()函数的前两行得到结果$\sigma=\left {x\rightarrow x_{0},y\rightarrow y_{0}\right}$。其中，$x_{0}$和$y_{0}$是两个初始的未约束的符号值。

当遇到一个赋值语句，形式为v=e时，符号执行将更新符号状态$\sigma$，加入一个v到$\sigma\left(e\right)$的映射。其中，$\sigma\left(e\right)$就是在当前符号化状态计算e得到的表达式。

对于图5-27（a）所示的testme()函数，当代码执行完第6行时，$\sigma=\left{x\rightarrow x_{0}, y\rightarrow y_{0},z\rightarrow 2y_{0}\right}$。这样，可得到如图5-28所示的testme()函数的符号执行结果。

符号执行的目标就是在给定的时间内，生成一个输入集合，使得所有或尽可能多的执行路径依赖于由符号表征的输入。当遇到条件语句if(e)S1 else S2时，PC会有两个不同的更新。首先是PC更新为PC$\wedge\sigma\left(e\right)$，这就表示then分支。然后，建立一个符号路径约束 ，初始化为PC$\wedge\ neg\ sigma\left(e\right)$，表示else分支。如果PC是可满足的，赋予一些实际值，程序就会执行then分支，此时的状态为：符号状态$\sigma$和符号路径PC。反之，如果 是可满足的，则会建立另一个符号实例，其符号状态为$\sigma$，符号路径约束为 ，执行else分支。如果PC和 都不能满足，那么执行就会在对应路径终止。

如果符号执行遇到exit语句或错误，如程序崩溃、违反断言等情况时，符号执行的当前实例会终止，利用约束求解器对当前符号路径约束赋一个可满足的值，构成测试输入。如果程序执行这些实际输入值，就会在同样的路径结束。

对于图5-27（a）所示函数testme()，3条不同执行路径构成了一棵执行树。经过符号执行计算，得到3组输入{x=0,y=1} 、{x=2,y=1} 、{x=30,y=15} ，覆盖了所有执行路径。当其中代码包含循环和递归时，如果终止条件是符号，符号执行就会产生无限数量的执行路径。循环及递归代码符号执行结果如下。

这时，符号路径要么是一串有限长度的“true”后跟着一个“false”（跳出循环），要么是无限长度的“true”。方程表示如下：

如果符号路径的约束不可解或者不能被高效求解，则不可能生成输出。对于图5-27（a）所示函数testme()，如果将函数“twice”更改为“(v*v)％50”，求解器将无法求解非线性约束问题，则符号执行失败，无法生成输出，该路径不可达。

5.5.2.2　现代符号执行

1.混合执行测试

混合执行测试能够同时维护精确状态和符号状态。精确状态将所有变量映射到具体值，符号状态仅映射具有非具体值的变量。由于混合执行测试需要维护程序执行时的精确状态，所以需要赋予以一个精确的初始值。当给定若干个具体输入时，混合执行测试动态进行符号执行。对于上述testme()函数，其混合符号执行测试过程及结果如图5-29所示。

2.执行生成测试

执行每个操作前，检查相关值是精确值还是已符号化的值，然后动态地进行精确和符号执行。若所有相关值都是实际值，则执行原始程序。若至少有一个值已符号化，则该操作将被符号执行。对于图5-27（a）所讨论的程序，如果将第17行改成“y=10”，调用“twice”时，传入精确参数，则其返回值是一个精确值。那么，第7行中的“z”及第8行中的“y+10”被转换成精确值，即可通过符号执行。基于精确值的符号执行测试结果如图5-30所示。

3.动态符号执行中的不精确性

不精确性是当调用第三方代码库时，由于某种原因而无法进行代码插装，从而假设传入参数都是精确值，全部当作精确执行，从而导致不精确性。即使传入参数中包含符号，动态符号执行依然可以将符号设定为一个具体值。

混合执行测试和执行生成测试具有不同的解决方法，除了调用外部代码，对于难以处理的操作数如浮点型或复杂函数，使用精确值可以有效地改进符号执行效果。动态符号执行通过精确值可以简化约束，从而防止符号执行受阻。但这种简化可能导致不完整性，即有时候无法对所有执行路径都生成输出。

5.5.2.3　存在的问题及解决方法

当代码中存在数组元素、复杂数据结构、循环、方法调用、指针等情况时，基于符号执行的分析还存在不少困难，尚有一些关键技术需要突破。

1.数组元素混淆

例如，如下含有数组的代码段，完成简单的乘法运算，返回数组元素值a[i]。

采用符号执行对该程序进行分析，当 、 、 时，令 、 、 的输入符号值分别为 、 和 ，可以得到该程序的返回值为 ，且只产生一条简单的路径条件。当 ， ， 中任意一条路径不满足时，程序将返回不同结果。如果 ， ， ，则程序先对 进行2倍运算， 的值变为 ，对 进行3倍运算，因 ，实际上是对 又进行了一次3倍运算。程序将 的值乘以6得到 。根据 i 、 j 、 k 之间的关系，得到如表5-20所示结果。

鉴于 i 、 j 、 k 之间的关系，符号执行路径由原来的1条变成5条，路径数大幅增加，测试用例数亦大幅增加到原来的5倍。当使用符号执行工具处理这类数组运算时，可能会造成测试用例遗漏。一个行之有效的办法是通过专门程序，对可能发生数组元素混淆的代码段定位，对混淆情况进行分类，并定义一个前置断言集。当前置断言满足时，产生一类混淆情况；反之不产生混淆。将每种混淆的分类看成一个执行内容（Execution Context，EC），当所有EC被定义之后，再次运行符号执行程序，根据前置断言集对程序进行数组元素混淆分析，并通过EC升级符号执行树。

假设参数 i 、 i 、 k 在数组界内，且 ， ， ，但这些条件并未在代码中体现，使用元素混淆处理程序即可以解决这类问题。元素混淆处理程序定义了如表5-21所示5个可能产生的EC及相应的输出， 、 、 的存储位置分别为 、 、 。当 i = j 时， 、 的存储位置为 ；而当 i = j = k 时， 、 、 的存储位置为 。

2.复杂数组结构处理

对于面向对象软件，使用符号执行处理链表、树、应用等复杂数据结构时，需要设计另外的算法。其中，“懒惰初始化”算法将类中具有复杂数据结构的属性视为不同对象，对这些属性进行调用，即对这些对象引用的调用。其主要特征是在类的属性值为空的状态下即开始运行类的方法，在这些属性第一次被方法调用时才“惰性”地初始化它的值。它允许类中的方法在不限制起始输入对象的数量与界限时就可以启动符号执行。“懒惰初始化”算法如图5-31所示。

首先建立一个未初始化属性值C的实例O，用一般符号执行方式运行实例。执行过程中遇到未初始化属性 f 时，根据 f 的类型采用不同处理方式。若 f 为复杂数据结构，算法对 f 进行不确定性操作，初始化为空，或新建一个实例，或已存在一个类型相同的实例，该对象在初始化属性过程中创建。初始化完成后，根据方法的前置断言对 f 进行检查，如果存在冲突，则重新初始化。如果 f 为基本数据类型或字符串，则将其初始化为一个新的数据类型的符号值。

3.循环语句处理

在进行循环语句处理时，如果循环结束条件依赖于一个或多个变量，符号执行过程中则无法明确判断循环的终止时间。当循环次数增加时，将导致符号执行过程中可能的路径急剧增加。White和Wiszniewski研究表明，当输出变量与输入变量呈线性关系时，为循环设置一个适当上限，虽然会遗漏一些错误，但这些错误仅在循环执行一定次数后才会产生，具有较好的测试效果。

4.方法调用

在符号执行过程中，遇到方法调用时，可以选择宏扩展、引理和可信3种处理方式。当可以获得被调用代码段时，宏扩展方式将被调用方法的代码内置化。在引理方式中，被调用方法已经过分析并被划分成等价类，不仅省去了进一步的分析，而且也无须获得被调用代码段，直接增加等价类数量。可信方式认为某些被调用方法 f (x)是可信的，对 f (x)的调用不会增加等价类数量，也不会产生新的路径。对一些操作符，如“+”的使用就是对可信 f (x)的调用，调用常规库函数时，常常使用这种方式。

5.5.3　符号表达式简化

在符号执行过程中，路径条件树中的每个节点都记录路径执行的约束条件及变量符号值。路径条件与变量符号值均由符号表达式组成，路径条件由逻辑表达式表征，变量符号值由代数表达式描述。在变量的不断替换过程中，逻辑及代数表达式均不断地被引入新成分，从而产生大量冗余，最终变得非常复杂，难以计算，必须对其进行简化处理，形成统一的标准形式。

5.5.3.1　逻辑表达式简化

逻辑表达式简化应用于路径条件简化，旨在为约束条件求解提供最简形式，限制路径条件的复杂度。在符号执行过程中，路径条件中的约束条件不断增加。这里，考虑如下例子：

PC 1 是符号执行过程中所产生的某一条路径所对应的执行条件，包含not 与and 两个逻辑操作符。此时，无法直接将PC 1 作为约束求解，得到覆盖该路径的测试用例。必须首先将PC 1 进行逻辑简化。我们将 作为表达式 E 1 ， y >0作为表达式 E 2 。则PC 1 可以表示为

根据逻辑简化规则， 可以转化成 ， 再次转化为 。因为 恒为空，所以，最后 可以简化为 ，将 还原成

逻辑表达式简化形式包括简化前及简化后符号表达式必须满足的形式两个部分。表5-22列出了部分逻辑表达式的简化规则。其中， E 1 、 E 2 代表符号表达式，1代表全集。

5.5.3.2　代数表达式简化

代数表达式简化应用于路径条件及变量符号值简化，去除代数表达式冗余，将其转换成一种标准形式。大部分静态分析工具简化系统的核心是简化规则数据库，每一规则均包括简化前后符号表达式必须满足的形式两部分。例如，规则 ，其中 与 为数字， 为任何形式的代数表达式。对于 形式的代数表达式，可以将其简化为 。表5-23列出了部分代数表达式的简化规则。

假设考虑代数表达式3( Z +5)+5( Z +5) ，简化系统通过扫描发现，该代数表达式满足规则( N 1 E )+( N 2 E )→( N 1 + N 2 ) E 的形式，将其简化成(3+5)( Z +5) ，再进行一次扫描，发现(3+5)( Z +5) 满足规则 N 1 + N 2 → N 3 ，则该表达式再次被简化成8( Z +5) ，经过进一步分析，发现它不满足简化规则库中的任一条规则，显然8( Z +5) 就是最简化的标准形式。

5.5.4　约束条件求解

路径条件树可能存在多个终止节点，终止节点的路径条件是从程序入口节点到达终止节点的约束条件。如果存在满足约束条件的输入，则路径可达，否则不可达。例如，一条路径的PC为{ R i <10, R i =0} ，可得到该路径的测试用例为{ R i =0} 。又如，一条路径的执行条件为{ R i <10, R i >100} ，路径条件矛盾，无法得到其解空间，该路径不可达，无法得到测试用例。

对于大多数实际问题，一些约束求解工具能够对不等式组进行求解或断定其解不存在。其中，Clark和Richardson提出的公理与代数技术，较好地解决了路径的可达性问题。公理使用定理证明系统，以判断路径的可达性，代数技术将PC中的不等式组视为求解最优问题的条件约束集合，若最优解存在，则路径可达，最优解就是满足路径条件的测试用例；若最优解不存在，则路径不可达。路径条件限制下，如果将路径条件当成线性规划问题中的不等式约束条件，即可将解空间问题转化为线性规划问题。与线性规划问题唯一不同的是，在求解空间时没有目标函数以及用来求解最大值或最小值的变量表达式。目标函数的形式并不重要，可以将源程序中所有变量简单相加后形成的表达式作为目标函数。添加目标函数后，约束求解就是求最优解的过程。

如果目标函数存在最优解，则满足最优解的所有变量取值的组合，肯定也能满足路径条件的限制，这些变量的取值就可以当成覆盖当前路径的测试用例。如果不存在最优解，则说明在PC中存在矛盾，当前路径不可达。 ITQRXCLylYcpwbcZXcqcKvnuSMfjVL3vLMXO7X6O/hcriyqFsDpvNznkCG8h8AOp