一种符号执行制导的循环内界分析方法

循环是计算机中重要的复杂程序结构.很多应用场景要求静态分析循环可能达到的最大迭代次数,即循环边界（Loop Bound）.对应技术在文献中被称为循环边界分析（Loop Bound Analysis）.现有的循环边界分析均使用保守方式进行外界分析,即产生略高于循环边界的近似值.基于这一现状,本文提出了一种自动地循环内界分析方法,产生略低于循环边界的近似值.当用户综合利用外界与内界分析,能将循环边界值约束到一个统计区间,从而能对分析结果获得更为完整的认识.本文基于循环条件制导的符号执行（Symbolic Execution）技术实现了循环内界分析,该技术的本质在于它能够利用符号执行符号化推导程序执行约束的特点,准确求解循环在程序所有合法输入条件下的边界值,并由生成的测试用例来保证该边界值一定可达（即保证是循环内界）.本文对符号执行制导技术进行了优化,并在多组已有研究采用的基准用例集上进行了实例评估,实验结果表明,本文的循环内界分析方法具备准确性和高效性,可以满足应用需求.