摘要
符号执行技术以其良好的精确度控制被广泛应用于程序分析领域,它将程序中变量的值用抽象的符号表示,模拟真实的程序执行.由于其路径敏感,在分析过程中会带来严重的状态爆炸问题.提出针对缺陷的程序切片方法来缓解这一问题,首先根据用户关心的缺陷生成源程序的切片准则,然后分析源代码生成数据依赖图和控制依赖图,由两者构成程序依赖图,再根据切片准则做程序切片,将源程序规模缩小,最后将切片后的程序交给程序分析工具分析.在符号执行分析工具ShapeChecker上的实验结果表明,提出的方法具有良好的效果.
Symbolic execution is widely used in program analysis for its well-controlled precision. It denotes the value of variables as abstract symbols and simulates the execution of programs. Because our tool is path-sensitive, we suffer the path-explosion problem when analyzing source code. We present a program slicing method for defects to alleviate the problem. Firstly, we generate the slicing criterion of source programs according to defects that users concern about. Then we analyze the source code to generate Data Depend- ence Graph and Control Dependence Graph, which constitute Program Dependence Graph. Next, the program is sliced according to the slicing criterion so that the source code could be reduced. Finally, we use the program analyzer to analyze the sliced program. The ex- perimental results on ShapeChecker, our symbolic execution tool, show that the method is effective.
出处
《小型微型计算机系统》
CSCD
北大核心
2018年第3期401-405,共5页
Journal of Chinese Computer Systems
基金
国家自然科学基金项目(61379039,61632005)资助.
关键词
缺陷检测
程序切片
静态分析
符号执行
defect detection
program slicing
static analysis
symbolic execution
