符号执行中的循环依赖分析方法

符号执行方法处理循环时存在路径爆炸的问题。为此，提出一种基于归纳变量的循环依赖分析方法。通过识别循环归纳变量及符号表达式，结合边界约束条件生成可达归纳变量分支的路径约束，并采用符号化映射方法分析嵌套循环归纳变量依赖问题，从而在不展开循环的情况下生成覆盖归纳变量分支的测试用例。对开源工具Libxml2进行实验，该方法能发现其中2个while循环所引发的数组访问越界错误。

Loop Dependence Analysis Method in Symbolic Execution

Input-dependent loops can cause the problem of path explosion in symbolic execution, a method based on induction variable for analysis of loop dependence is proposed in this paper. By recognizing the loop induction variables and symbolic expressions, it is combined with the bound conditions to generate feasible path constraint for induction variable branches. Induction variable dependence of nested-loop is solved by symbolic affine analysis. It can generate test cases which can cover the branches of induction variables without loop unrolling. Test results show that by this method, two array access violations of the open source tools Libxml2 are found in while loops.