Program state optimal method based on variable symbolic relation analysis

Xi GUO; Pan WANG

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

您当前的位置：

首页 >

文章列表页 >

Program state optimal method based on variable symbolic relation analysis

Papers | 更新时间：2024-06-05

- Program state optimal method based on variable symbolic relation analysis
- Journal on Communications Vol. 39, Issue 6, Pages: 81-88(2018)
- 作者机构：
  
  1. 华中农业大学信息学院，湖北武汉 430070
  2. 武汉电力职业技术学院电力工程系，湖北武汉 430079
- 作者简介：
- 基金信息：
  
  The National Natural Science Foundation of China(61502194);The Central University Basic Business Expenses Special Funding for Scientific Research Projects(2662018JC028)
- DOI：10.11959/j.issn.1000-436x.2018094
  CLC： TP311
- Online First：2018-06，
  
  Published：25 June 2018
- 稿件说明：
移动端阅览
Xi GUO, Pan WANG. Program state optimal method based on variable symbolic relation analysis[J]. Journal on Communications, 2018, 39(6): 81-88.
DOI：

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 .

Views

1789

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Binary program tracing and analysis framework by integrating Intel PT and dynamic instrumentation

Program semantic analysis model for code reuse detection

Symbolic execution optimization method based on input constraint

Related Author

PAN Jiaye

Sha Letian

LU Jing

XIAO Fu

GUO Xi

WANG Pan

Sunlyu WANG

Yuqi LIN

Related Institution

School of Computer Science, Nanjing University of Posts and Telecommunications

College of Informatics, Huazhong Agricultural University

Hubei Collaborative Innovation Center for High-Efficiency Utilization of Solar Energy, Hubei University of Technology

National Engineering Research Center of Fundamental Software,Institute of Software Chinese Academy of Sciences

AI问答

⁰