电子学报2017，Vol.45Issue(11)：2582-2592,11.DOI:10.3969/j.issn.0372-2112.2017.11.003
一种符号执行制导的循环内界分析方法
A Symbolic Execution Guided Inner Loop Bound Analysis
摘要
Abstract
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.关键词
循环边界分析/符号执行/软件测试Key words
loop bound analysis/symbolic execution/software testing分类
信息技术与安全科学引用本文复制引用
赵祖威,冯世宁,汤恩义,陈鑫,李宣东,潘敏学,赵晨..一种符号执行制导的循环内界分析方法[J].电子学报,2017,45(11):2582-2592,11.基金项目
国家自然科学基金(No.61402222,No.61632015) （No.61402222,No.61632015）
国家重点研发计划(No.2016YFB1000802) （No.2016YFB1000802）
教育部高等学校博士学科点专项科研基金(No.20110091120058) （No.20110091120058）
江苏省产学研项目(No.BY2014126-03) （No.BY2014126-03）
