Computer Science ›› 2017, Vol. 44 ›› Issue (2): 209-215.doi: 10.11896/j.issn.1002-137X.2017.02.034

Previous Articles     Next Articles

State Merging for Symbolic Execution Engine with Shape Analysis

DENG Wei and LI Zhao-peng   

  • Online:2018-11-13 Published:2018-11-13

Abstract: Symbolic execution is widely used in static code analysis and automatic test generation for its well controlled precision and code coverage.When applied to analyze a program,symbolic execution traversals all possible states by simulating the execution of the program to analyze the data-flow and control-flow information and get results.High precision and coverage request detailed and complete description of program states,which will lead to the path-explosion problem in almost all implementations of symbolic execution.State merging is an effective way to solve the path-explosion problem.We firstly proposed an algorithm for the merging of states from different paths,then abstracted the states in a proper way to expand the application scope of the algorithm.Finally,we discussed the actual effect of state merging and put forward an optimization scheme.The whole algorithm is deployed in ShapeChecker,which is our symbolic execution tool,and experiments show good results in performance.

Key words: Symbolic execution,State merging,Query cost,Memory model,State abstraction

[3] ZHU L ,LI Z P,LIANG J B,et al.A Specification Language for Precise Shape Analysis of C Program[J].Journal of Chinese Mini-Micro Computer Systems,2016,7(4):653-658.(in Chinese) 朱玲,李兆鹏,梁家彪,等.C程序精确形状分析中的规范语言设计[J].小型微型计算机系统,2016,7(4):653-658.
[4] SOOS M.SMT Competition’14 and STP.http://www.msoos.org/2014/06/smt-competition14-and-stp.
[5] LLVM I R.LLVM Language Reference Manual.http://llvm.org/docs/LangRef.html.
[6] BAUDIN P,CUOQ P,FILLARTE J C,et al.ACSL:ACSL/ISO C Specification Language(Version 1.7)[Z].2009-2013 .
[7] ShapeChecker.http://kyhcs.ustcsz.edu.cn/~shapechecker.
[10] CADAR C,DUNBAR D,ENGLER D.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[C]∥Usenix Symposium on Operating Systems Design & Implementation.2008:208-224 .
[11] HOARE C A R.An Axiomatic Basis for Computer Programming[J].Communications of the ACM,1969,12(10):576-580.
[12] Clang Static Analyzer.http://clang-analyzer.llvm.org.
[13] XU Z X,KREMENEK T,ZHANG J.A Memory Model forStatic Analysis of C Programs[C]∥Proceeding of the 4th International Conference on Leveraging Applications of Formal Methods,Verification and Validation.2010.
[14] Coverity.https://coverity.com.
[15] PALIKAREVA H,CADAR C.Multi-solver Support in Symbo-lic Execution[M]∥Computer Aided Verification:Lecture Notes in Computer Science,2013:53-68
[16] CIFUENTES C,SCHOLZ B.Parfait:Designing a Scalable Bug Checker[C]∥IEEE International Working Conference on Source Code Analysis & Manipulation.2008:4-11.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!