基于变量符号关联分析的程序状态优化方法

郭曦; 王盼

doi:10.11959/j.issn.1000-436x.2018094

您当前的位置：

首页 >

文章列表页 >

基于变量符号关联分析的程序状态优化方法

学术论文 | 更新时间：2024-06-05

- 基于变量符号关联分析的程序状态优化方法
- Program state optimal method based on variable symbolic relation analysis
- 通信学报 2018年39卷第6期页码：81-88
- 作者机构：
  
  1. 华中农业大学信息学院，湖北武汉 430070
  2. 武汉电力职业技术学院电力工程系，湖北武汉 430079
- 作者简介：
  
  [ "郭曦（1983-），男，湖北鄂州人，博士，华中农业大学副教授、硕士生导师，主要研究方向为软件分析与测试、信息安全等。" ]
  [ "王盼（1987-），女，河南济源人，博士，武汉电力职业技术学院讲师，主要研究方向为电力电子变换等。" ]
- 基金信息：
  
  国家自然科学基金资助项目(61502194);中央高校基本科研业务费专项基金资助项目(2662018JC028)
- DOI：10.11959/j.issn.1000-436x.2018094
  中图分类号： TP311
- 网络出版日期：2018-06，
  
  纸质出版日期：2018-06-25
- 稿件说明：
移动端阅览
郭曦, 王盼. 基于变量符号关联分析的程序状态优化方法[J]. 通信学报, 2018,39(6):81-88.

Xi GUO, Pan WANG. Program state optimal method based on variable symbolic relation analysis[J]. Journal on communications, 2018, 39(6): 81-88.
郭曦, 王盼. 基于变量符号关联分析的程序状态优化方法[J]. 通信学报, 2018,39(6):81-88. DOI： 10.11959/j.issn.1000-436x.2018094.

Xi GUO, Pan WANG. Program state optimal method based on variable symbolic relation analysis[J]. Journal on communications, 2018, 39(6): 81-88. DOI： 10.11959/j.issn.1000-436x.2018094.

摘要

程序分析是主要的程序属性分析方法，在变量依赖关系、路径覆盖率、测试用例约简等方面有广泛的应用，并取得了大量研究成果。目前，程序分析主要以符号执行工具为核心，但是普遍存在路径条件逻辑表达式难以准确生成和约束求解器性能不够高的问题，从而影响程序分析的效果。以提高路径分析精度为目标，首先分析不同执行路径对应的路径条件，并提取公共的符号表达式以提高符号关联分析的精度，然后逆向生成依赖条件逻辑表达式集合，使用依赖关联分析算法以提高路径分析的精度。实验结果表明，所提方法相对于传统的路径分析方法，有更准确的时间复杂度和更高的路径分析精度。

Abstract

Program analysis is the prime method to program property analysis

which is widely used in the domain of parameter dependent relation

path coverage and test case generation

and a lot of progress has been made.Current program analysis is based on the method of symbolic execution

but symbolic execution is usually tackled with the problems of logic expression generation of path condition and low efficiency of constrain solver

which will affect the results of program analysis.Aiming at enhancing the path analysis efficiency

the path conditions of different paths were collected

the common symbolic expression was extracted and the efficiency of symbolic analysis was enhanced

then the logic expression set was generated

the dependent relation algorithm was used to enhance the efficiency of symbolic analysis.Experimental results demonstrate that the proposed method has the advantages of accurate time complexity and better analysis efficiency compare to traditional program analysis method.

关键词

Keywords

references

KUZNETSOV V , KINDER J , BUCUR S , et al . Efficient state merging in symbolic execution [J ] . ACM Sigplan Notices , 2012 , 47 ( 6 ): 193 - 204 .

GODEFROID P , . Compositional dynamic test generation [C ] // ACMSigplan-Sigact Symposium on Principles of Programming Languages . 2007 : 47 - 54 .

AVGERINOS T , REBERT A , SANG K C , et al . Enhancing symbolic execution with veritesting [C ] // International Conference on Software Engineering . 2014 : 1083 - 1094 .

GODEFROID P , NORI A V , RAJAMANI S K , et al . Compositional maymust program analysis:unleashing the power of alternation [C ] // ACM Sigplan-Sigact Symposium on Principles of Programming Languages . 2010 : 43 - 56 .

王翀 , 吕荫润 , 陈力 , 等 . SMT 求解技术的发展及最新应用研究综述 [J ] . 计算机研究与发展 , 2017 , 54 ( 7 ): 1405 - 1425 .

WANG C , LYU Y R , CHEN L , et al . Survey on development of solving methods and state of theart application of satisfiability modulo theories [J ] . Journal of Computer Research and Development , 2017 , 54 ( 7 ): 1405 - 1425 .

TORLAK E , BODIK R . A lightweight symbolic virtual machine for solver-aided host languages [J ] . ACM SIGPLAN Notices , 2014 , 49 ( 6 ): 530 - 541 .

VISSER W , REANU C S , NEK R . Test input generation for Java containers using state matching [C ] // International Symposium on Software Testing and Analysis . 2006 : 37 - 48 .

CHAKRABARTI A , GODEFROID P . Software partitioning for effective automated unit testing [C ] // ACM ＆ IEEE International Conference on Embedded Software . 2006 : 262 - 271 .

SHARIR M , PNUELI A . Two approaches to interprocedural dataflow analysis [M ] . Englewood : Prentice-HallPress , 1981 : 189 - 234 .

REPS T , HORWITZ S , SAGIV M . Precise interprocedural dataflow analysis via graph reachability [C ] // ACM Sigplan-Sigact Symposium on Principles of Programming Languages . 1995 : 49 - 61 .

PENG T , PADUA D . Gated SSA-based demand driven symbolic analysis for parallelizing compilers [C ] // International Conference on Supercomputing . 1995 : 414 - 423 .

SEN K , NECULA G , GONG L , et al . MultiSE:multi-path symbolic execution using value summaries [C ] // The 10th Joint Meeting on Foundations of Software Engineering . 2015 : 842 - 853 .

QI D W , NGUYEN H , ROYCHOUDHURY A . Path exploration based on symbolic output [J ] // ACM Transactions on Software Engineering and Methodology , 2011 , 22 ( 4 ): 278 - 288 .

王伟光 , 曾庆凯 , 孙浩 . 面向危险操作的动态符号执行方法 [J ] . 软件学报 , 2016 , 27 ( 5 ): 1230 - 1245 .

WANG W G , ZENG Q K , SUN H . Dynamic symbolic execution method oriented to critical operation [J ] . Journal of Software , 2016 , 27 ( 5 ): 1230 - 1245 .

BANG L , AYDIN A , BULTAN T . Automatically computing path complexity of programs [C ] // Joint Meeting on Foundations of Software Engineering . 2015 : 61 - 72 .

浏览量

997

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

面向代码重用检测的程序语义分析模型

基于输入约束的符号执行优化