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   
[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .