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

发布时间：2018-03-20 18:54

本文选题：循环边界分析　切入点：符号执行　出处：《电子学报》2017年11期 　论文类型：期刊论文

【摘要】：循环是计算机中重要的复杂程序结构.很多应用场景要求静态分析循环可能达到的最大迭代次数,即循环边界(Loop Bound).对应技术在文献中被称为循环边界分析(Loop Bound Analysis).现有的循环边界分析均使用保守方式进行外界分析,即产生略高于循环边界的近似值.基于这一现状,本文提出了一种自动地循环内界分析方法,产生略低于循环边界的近似值.当用户综合利用外界与内界分析,能将循环边界值约束到一个统计区间,从而能对分析结果获得更为完整的认识.本文基于循环条件制导的符号执行(Symbolic Execution)技术实现了循环内界分析,该技术的本质在于它能够利用符号执行符号化推导程序执行约束的特点,准确求解循环在程序所有合法输入条件下的边界值,并由生成的测试用例来保证该边界值一定可达(即保证是循环内界).本文对符号执行制导技术进行了优化,并在多组已有研究采用的基准用例集上进行了实例评估,实验结果表明,本文的循环内界分析方法具备准确性和高效性,可以满足应用需求.
[Abstract]:Loop is an important complex program structure in a computer. Many application scenarios require the maximum number of iterations that can be achieved by a static analysis loop. The corresponding technique is called Loop Bound Analysis in the literature. The existing circular boundary analysis uses conservative methods to carry out external analysis, that is, an approximate value slightly higher than the cyclic boundary. In this paper, a method of automatic circular inner bound analysis is proposed, which produces approximate values slightly lower than the cyclic boundary. When the user synthetically utilizes the external and inner boundary analysis, the cyclic boundary value can be restricted to a statistical interval. Therefore, a more complete understanding of the analysis results can be obtained. In this paper, the cyclic internal bound analysis is realized based on the symbolic execution execution technique based on cyclic conditional guidance. The essence of this technique is that it can accurately solve the boundary value of the loop under all the legitimate input conditions of the program by taking advantage of the characteristic of symbolic execution symbolic derivation program execution constraints. The generated test cases are used to ensure that the boundary value can be reached (that is, cyclic inner bound). In this paper, the symbolic execution guidance technology is optimized, and an example is evaluated on the set of reference cases that have been studied. The experimental results show that the proposed method is accurate and efficient, and can meet the needs of application.
【作者单位】：南京大学软件新技术国家重点实验室;南京大学软件学院;南瑞集团公司(国网电力科学研究院);国电南瑞科技股份有限公司;
【基金】：国家自然科学基金(No.61402222,No.61632015) 国家重点研发计划(No.2016YFB1000802) 教育部高等学校博士学科点专项科研基金(No.20110091120058) 江苏省产学研项目(No.BY2014126-03)
【分类号】：TP311.53

【相似文献】