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

摘要

Loop is an important program structure in computer.Many applications need to estimate the maximum iteration number of loops in programs by loop bound analysis.Existing loop bound analysis uses conservative methods to derive outer loop bounds,which estimates the bounds higher than the real ones.In this paper,we propose an automatic inner bound analysis,which generates bounds slightly lower than the real ones.When users combine the inner bound analysis with traditional outer bound analysis,they can restrict every real loop bound in an interval and get more information about the loops.We implement the inner bound analysis by a scope-condition guided symbolic execution.The insight of our technique is that when symbolic execution substitutes program inputs by symbols in its derivation,it generates loop bounds for all valid inputs and generates corresponding test cases that make the inner bounds feasible.We optimize the technique and evaluate it on several benchmarks.The results show that the analysis is precise and efficient.%循环是计算机中重要的复杂程序结构.很多应用场景要求静态分析循环可能达到的最大迭代次数,即循环边界(Loop Bound).对应技术在文献中被称为循环边界分析(Loop Bound Analysis).现有的循环边界分析均使用保守方式进行外界分析,即产生略高于循环边界的近似值.基于这一现状,本文提出了一种自动地循环内界分析方法,产生略低于循环边界的近似值.当用户综合利用外界与内界分析,能将循环边界值约束到一个统计区间,从而能对分析结果获得更为完整的认识.本文基于循环条件制导的符号执行(Symbolic Execution)技术实现了循环内界分析,该技术的本质在于它能够利用符号执行符号化推导程序执行约束的特点,准确求解循环在程序所有合法输入条件下的边界值,并由生成的测试用例来保证该边界值一定可达(即保证是循环内界).本文对符号执行制导技术进行了优化,并在多组已有研究采用的基准用例集上进行了实例评估,实验结果表明,本文的循环内界分析方法具备准确性和高效性,可以满足应用需求.