计算机科学 ›› 2017, Vol. 44 ›› Issue (2): 209-215.doi: 10.11896/j.issn.1002-137X.2017.02.034
邓维,李兆鹏
DENG Wei and LI Zhao-peng
摘要: 符号执行技术以其良好的精确度控制和代码覆盖率被广泛应用于静态程序分析和高覆盖率测试用例自动生成。 符号执行 在分析程序时,以模拟真实的程序执行过程的方式分析程序的数据流和控制流信息,并检查程序可能出现的所有状态,得到程序的分析结果。高精确度和高覆盖率要求对程序状态描述具体而完备,这会导致符号执行过程中常见的状态爆炸问题。首先提出在不同的执行路径上对具体内存状态进行合并的算法,然后对内存模型进行适度的抽象,扩大状态合并算法的适用范围,最后讨论状态合并所带来的实际效果,并提出了状态合并的优化解决方案。所提出的算法在符号执行引擎ShapeChecker上实现,并取得了良好的实验结果。
[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! |
|