基于抽象符号表的内存模型
收稿日期: 2009-09-01
修回日期: 2009-12-03
网络出版日期: 2011-06-25
基金资助
国家863计划资助项目(2007AA010301)
A Memory Model Based on Abstract Symbol Tables
Received date: 2009-09-01
Revised date: 2009-12-03
Online published: 2011-06-25
代子营,毛晓光,马晓东,王瑞 . 基于抽象符号表的内存模型[J]. 计算机工程与科学, 2011 , 33(6) : 84 -90 . DOI: 10.3969/j.issn.1007130X.2011.
Symbolic execution plays an important role in the area of software testing and program verification. However, there are several difficulties facing symbolic execution, one of which is how to abstract various data types and syntax in the source codes. This paper addresses this problem by proposing a new concept of abstract symbol table and a method to model memory using abstract symbol tables. The abstract symbol table records names, types, abstract addresses and symbolic values of addressable objects, which is a simple and accurate memory abstracting mechanism. The memory model is prerequisite for any techniques involving symbolic execution, but this paper systematically presents a memory model for symbolic execution in detail. The abstract symbol tablebased memory model can handle various data types and syntax uniformly including function and class, handle the aliasing problem directly, and possess good scalability because of several performanceimproving techniques.
［1］King J C. Symbolic Execution and Program Testing［J］. Communications of the ACM, 1976, 19(7):385394.
［2］Shannon D, Hajra S, Lee A, et al. Abstracting Symbolic Execution with String Analysis［C］∥Proc of the Testing: Academic and Industrial Conference Practice and Research Techniques, 2007:1322.
［3］Xie T, Marinov D, Schulte W, et al. Symstra: A Framework for Generating ObjectOriented Unit Tests Using Symbolic Execution［C］∥Proc of the TACAS’05, 2005:365381.
［4］张健. 精确的程序静态分析［J］. 计算机学报, 2008, 31(9):15491553.
［5］Saswat A, Patrice G, Nikolai T. DemandDriven Compositional Symbolic Execution［C］∥Proc of the 14th Int’l Conf on Tools and Algorithms for the Construction and Analysis of Systems, 2008:367381.
［6］Zhang J. Symbolic Execution of Program Paths Involving Pointer and Structure Variables［C］∥Proc of the Fourth Int’l Conf on Quality Software, 2004:8792.
［7］Hampapuram H, Yang Y, Das M. Symbolic Path Simulation in PathSensitive Dataflow Analysis［C］∥Proc of the 6th ACM SIGPLANSIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2005:5258.
［8］Xie Yichen, Chou Andy, Engler Dawson. ARCHER: Using Symbolic, PathSensitive Analysis to Detect Memory Access Errors［C］∥Proc of the ESEC/FSE’03, 2003:327336.
［9］Coward P D. Symbolic Execution SystemsA Review［J］. Software Engineering Journal, 1988, 3(6):229239.
［10］Boyer R S, Elspas B, Levitt K N. SELECT A Formal System for Testing and Debugging Programs by Symbolic Execution［C］∥Proc of the Int’l Conf on Reliable Software, 1975:234245.
［11］Gunter Elsa L, Peled Doron. Path Exploration Tool［C］∥Proc of the 5th Int’l Conf on Tools and Algorithms for Construction and Analysis of Systems, 1999:405419.
［12］Zhang J, Wang X. A Constraint Solver and Its Application to Path Feasibility Analysis［J］. International Journal of Software Engineering and Knowledge Engineering, 2001,11(2):139156.
［13］Khurshid S, Suen Y L. Generalizing Symbolic Execution to Library Classes［J］. ACM SIGSOFT Software Engineering Notes, 2006,31(1):103110.
［14］Ghiya R, Hendren L J. Is It a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for HeapDirected Pointers in C［C］∥Proc of the 23rd ACM SIGPLANSIGACT Symp on Principles of Programming Languages, 1996:115.
［15］LevAmi T, Reps T, Sagiv M, et al. Putting Static Analysis to Work for Verification: A Case Study［C］∥Proc of the 2000 ACM SIGSOFT Int’l Symp on Software Testing and Analysis, 2000:2638.
［16］Pratt Terrence W, Zelkowitz Marvin V.程序设计语言:设计与实现［M］. 第四版.傅育熙, 张冬茉, 黄林鹏, 译. 北京: 电子工业出版社, 2001.
［17］Lattner C, Adve V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation［C］∥Proc of Int’l Symp on Code Generation and Optimization, 2004:7586.
［18］Harbison III Samuel P, Steele Jr. Guy L. C语言参考手册［M］. 第五版. 英文版. 北京:人民邮电出版社, 2007.
［19］Khurshid S, Pasareanu C S, Visser W. Generalized Symbolic Execution for Model Checking and Testing［C］∥Proc of TACAS2003, 2003:553568.
［20］Choi JD, Burke M, Carini P. Efficient FlowSensitive Interprocedural Computation of PointerInduced Aliases and Side Effects［C］∥Proc of the Twentieth Annual ACM SIGPLANSIGACT Symp on Principles of Programming Languages, 1993:232245.
/
| 〈 |
|
〉 |