符号执行在发展过程中出现了一种叫做动态符号执行的方法。动态符号执行是以具体数值作为输入来模拟执行程序代码，与传统静态符号执行相比，其输入值的表示形式不同。动态符号执行使用具体值作为输入，同时启动代码模拟执行器，并从当前路径的分支语句的谓词中搜集所有符号约束。然后修改该符号约束内容构造出一条新的可行的路径约束，并用约束求解器求解出一个可行的新的具体输入，接着符号执行引擎对新输入值进行一轮新的分析。通过使用这种输入迭代产生变种输入的方法，理论上所有可行的路径都可以被计算并分析一遍。
    动态符号执行相对于静态符号执行的优点是每次都是具体输入的执行，在模拟执行这个过程中，符号化的模拟执行比具体化的模拟执行的花销大很多；并且模拟执行过程中所有的变量都为具体值，而不必使用复杂的数据结构来表达符号值，使得模拟执行的花销进一步减少。但是动态符号执行的结果是对程序的所有路径的一个“下逼近”，即其最后产生路径集合应该比所有路径集合小，但这种情况在软件测试中是允许的。 
2. 符号执行示例
    本节将通过一个示例代码来具体说明符号执行的分析原理。如图3所示，先对一段简单的代码函数test 构建控制流图CFG，可以看出该CFG只包含了2条路径。接着，以符号值为输入，模拟执行代码，在遇到分支语句时，使用约束求解器判定这两条路径的可行性，本示例使用的是“深度优先”的路径调度策略，详细的分析过程见图3。在对两条路径模拟执行并收集路径约束后，使用约束求解器可以求解出分别触发这两条路径的两个测试例输入及对应的返回值。测试例输入为“i=11”时，返回值“10”；测试例输入为“i=10”时，返回值为“9”。
    通过这个简单的例子可以看出使用符号执行的方法进行分析可以达到很高的路径覆盖率，并且结合约束求解器还可以实现测试例的自动生成。但是这仅仅是符号执行技术和约束求解结合的具体应用的一个方面，符号执行技术还可以有其它的应用。
    图 3 符号执行原理示例

三、 符号执行的关键技术及发展现状 
    上节介绍了符号执行的基本原理，本节将重点介绍符号执行的关键技术及其解决方法，此外，还将介绍使用该技术开发的工具。
1. 符号执行的关键技术
    (1)路径状态空间爆炸
    符号执行技术在理论上面临着路径状态空间的爆炸问题，其主要形成原因是每一个分支条件语句都可能会使当前的路径再分支出一条新的路径，而这是“指数级”增长的。相对于静态符号执行在分支语句时都是符号值的约束，动态符号执行在分支语句时则都是具体值的约束。动态符号执行的当前路径执行过程中不会产生新路径，只在执行结束后再去产生新路径，且一次只产生一条。但是它们都没法从根本上避免路径状态空间爆炸所造成的影响。
    一方面，在具体的实现中有使用限定每个过程内的分析路径数目上限的方法来缓解该问题所产生的影响，如Coverity，也可以使用设置时间上限或者内存空间上限的方法来缓解路径爆炸问题所可能造成分析工具崩溃的恶劣影响，如Fortify。另一方面，符号执行工具的实现者总是希望能设计出好的路径遍历策略，以在有限的时间和空间范围内达到最大的代码检测覆盖率。人们通过改进路径调度算法来提高符号执行的分析性能，但是这些路径调度算法都只是局部改进，很难从根本上解决这一问题。
    (2)复杂结构语义和操作语义的建模
    符号执行实现时需要对被分析代码的结构语义进行建模，然后再对被分析代码的操作语义进行建模，最后构建一个虚拟机模型。由于符号执行是路径敏感的分析方法，因此一般为每条路径都会创建一个专属的虚拟机模型，以保证路径之间的相互独立性。该模型的准确程度将直接影响静态分析结果的精度。由于编程语言中使用的复杂数据结构和复杂操作语句具有较高的灵活性，使得它们的建模变得十分困难。
    人们提出了一种“惰性初始化”的方法，其思想是为每个数据结构（特别是复杂数据结构）建模时，在声明或者定义时只为其构建类型信息，直到被使用的时候，才根据使用的需要来初始化该变量的对象信息。
    (3)程序全局分析
    在程序全局分析过程中，当对一个规模较大、包含很多的过程间调用的程序进行上下文敏感的分析时，每当一个过程调用了另一个过程时都进入子过程进行分析，虽然会很精确，但这种方式可能会造成大量的时间空间花销，而使分析过程异常中止或在用户可接受的时间内无法完成。
    一种比较好的全局分析方法叫做“函数摘要”。函数摘要的方法是在过程内分析的基础上对已分析过的函数进行一个摘要记录的操作。在以后的分析中遇到调用其他函数时，如果已存在被调用函数的摘要，则直接调用该函数的摘要并对该摘要行为进行解释；如果不存在被调用函数的摘要信息，则进入被调用函数进行分析，并在分析之后进行摘要保存。函数摘要是一种相对折中的办法，所创建的函数摘要也可能很不准确。另一个问题是对无法获得源代码的第三方库函数的摘要只能通过人工的编写来完成，这也可能是不精确的，而这两点都会影响到最终的分析结果的精度。
    对于函数摘要的构建策略也是一个研究内容，参考文献[10]使用在函数调用图上的自顶向下的需求驱动策略来为所有子过程创建函数摘要。由于循环语句可能会使被摘要函数的路径空间爆炸，而使得无法对函数的所有路径都进行分析摘要，该文章介绍了使用循环不变量来进行函数摘要以解决循环语句所引入的问题。

(责任编辑：adminadmin2008)