基于抽象符号表的内存模型

A Memory Model Based on Abstract Symbol Tables

符号执行技术在软件测试和程序验证中发挥着重要作用。如何抽象和处理程序中各种数据类型和语法成分是符号执行必须解决的问题。本文提出抽象符号表的概念,以及基于抽象符号表建模内存的方法。抽象符号表记录可寻址对象的名称、类型、抽象地址和符号值,是一种简单、精确的内存抽象机制。内存模型是所有使用符号执行的技术的前提,本文系统给出了一个面向符号执行的内存模型。基于抽象符号表的内存模型能够统一处理各种数据类型和语法成分,包括函数和类,能够直接处理指针别名问题,不需要额外的别名分析算法。经过一些性能优化处理,基于抽象符号表的内存模型具有较好的性能。

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.