1. 南京大学软件新技术国家重点实验室,江苏,南京,210023
2. 南京大学软件学院,江苏,南京,210093
3. 南瑞集团公司(国网电力科学研究院),江苏,南京,211106
4. 国电南瑞科技股份有限公司,江苏,南京,211106
5. 南京大学软件新技术国家重点实验室,江苏,南京,210023
6. 南京大学软件学院,江苏,南京,210093
7. 南瑞集团公司(国网电力科学研究院),江苏,南京,211106
8. 国电南瑞科技股份有限公司,江苏,南京,211106
网络出版:2017-11-25,
纸质出版:2017
移动端阅览
赵祖威, 冯世宁, 汤恩义, 等. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017,45(11):2582-2592.
ZHAO Zu-wei, FENG Shi-ning, TANG En-yi, et al. A Symbolic Execution Guided Inner Loop Bound Analysis[J]. Acta Electronica Sinica, 2017, 45(11): 2582-2592.
赵祖威, 冯世宁, 汤恩义, 等. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017,45(11):2582-2592. DOI: 10.3969/j.issn.0372-2112.2017.11.003.
ZHAO Zu-wei, FENG Shi-ning, TANG En-yi, et al. A Symbolic Execution Guided Inner Loop Bound Analysis[J]. Acta Electronica Sinica, 2017, 45(11): 2582-2592. DOI: 10.3969/j.issn.0372-2112.2017.11.003.
循环是计算机中重要的复杂程序结构.很多应用场景要求静态分析循环可能达到的最大迭代次数,即循环边界(Loop Bound).对应技术在文献中被称为循环边界分析(Loop Bound Analysis).现有的循环边界分析均使用保守方式进行外界分析,即产生略高于循环边界的近似值.基于这一现状,本文提出了一种自动地循环内界分析方法,产生略低于循环边界的近似值.当用户综合利用外界与内界分析,能将循环边界值约束到一个统计区间,从而能对分析结果获得更为完整的认识.本文基于循环条件制导的符号执行(Symbolic Execution)技术实现了循环内界分析,该技术的本质在于它能够利用符号执行符号化推导程序执行约束的特点,准确求解循环在程序所有合法输入条件下的边界值,并由生成的测试用例来保证该边界值一定可达(即保证是循环内界).本文对符号执行制导技术进行了优化,并在多组已有研究采用的基准用例集上进行了实例评估,实验结果表明,本文的循环内界分析方法具备准确性和高效性,可以满足应用需求.
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.
0
浏览量
293
下载量
0
CSCD
关联资源
相关文章
相关作者
相关机构
京公网安备11010802024621