A Memory Model Based on Abstract Symbol Tables

doi:10.3969/j.issn.1007130X.2011.

Abstract

Abstract:

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 tablebased 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 performanceimproving techniques.

Key words: symbolic execution;memory model;abstract symbol table, program analysis

DAI Ziying,MAO Xiaoguang,MA Xiaodong,WANG Rui. A Memory Model Based on Abstract Symbol Tables[J]. J4, 2011, 33(6): 84-90.

References

［1］King J C. Symbolic Execution and Program Testing［J］. Communications of the ACM, 1976, 19(7):385394.
［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:1322.
［3］Xie T, Marinov D, Schulte W, et al. Symstra: A Framework for Generating ObjectOriented Unit Tests Using Symbolic Execution［C］∥Proc of the TACAS’05, 2005:365381.
［4］张健. 精确的程序静态分析［J］. 计算机学报, 2008, 31(9):15491553.
［5］Saswat A, Patrice G, Nikolai T. DemandDriven Compositional Symbolic Execution［C］∥Proc of the 14th Int’l Conf on Tools and Algorithms for the Construction and Analysis of Systems, 2008:367381.
［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:8792.
［7］Hampapuram H, Yang Y, Das M. Symbolic Path Simulation in PathSensitive Dataflow Analysis［C］∥Proc of the 6th ACM SIGPLANSIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2005:5258.
［8］Xie Yichen, Chou Andy, Engler Dawson. ARCHER: Using Symbolic, PathSensitive Analysis to Detect Memory Access Errors［C］∥Proc of the ESEC/FSE’03, 2003:327336.
［9］Coward P D. Symbolic Execution SystemsA Review［J］. Software Engineering Journal, 1988, 3(6):229239.
［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:234245.
［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:405419.
［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):139156.
［13］Khurshid S, Suen Y L. Generalizing Symbolic Execution to Library Classes［J］. ACM SIGSOFT Software Engineering Notes, 2006,31(1):103110.
［14］Ghiya R, Hendren L J. Is It a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for HeapDirected Pointers in C［C］∥Proc of the 23rd ACM SIGPLANSIGACT Symp on Principles of Programming Languages, 1996:115.
［15］LevAmi 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:2638.
［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:7586.
［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:553568.
［20］Choi JD, Burke M, Carini P. Efficient FlowSensitive Interprocedural Computation of PointerInduced Aliases and Side Effects［C］∥Proc of the Twentieth Annual ACM SIGPLANSIGACT Symp on Principles of Programming Languages, 1993:232245.