👍

A Memory Model for Static Analysis of C Programs

作者

常见的内存模型

Name Binding Model

内存被看做是"Name-Value"的键值对的形式，在求值和赋值表达式的时候将左侧变量名称绑定到右侧表达式的值上，此内存模型较为常见。但是因为C语言中包含指针，所以不能模拟C语言的语义。

c
int x, y;
int *p = &x;
x = 3;
*p = 4;
y = x;

考虑上例，其中变量 $p$ 是一个指向变量 $x$ 的指针，指针的存在带来了别名问题(Aliasing Problem)。别名问题是指两个或者多个名称可以表示相同的存储位置。我们在修改一个名称的值的时候也应该修改与之关联的所有名称的值，但是在名称绑定模型中并没有探测到所有名称的别名的能力，所以不能模糊C语言的语义。

Array Simulation Model

Name Binding Model最大的问题是没有内存位置的概念，但是C语言中的指针是通过操作内存位置的值来实现的，所以由此提出了Array Simulation Model。简单来说该模型将所有的内存视为一个数组，如果在一个数组中分配所有的变量，那么所有针对变量的操作都可以转化成为对于一个数组元素的操作，同时该模型通过将数组元素的索引和变量内存位置的对应引入了内存位置的概念。

上述例子可以使用Array Simulation Model进行转化

c
Assume mem[] is the memory simulation array.
Memory allocation:
x: mem[1], y: mem[2], p: mem[3]
mem[3] = 1; // p = &x; mem[3] is ’p’,
            // 1 is x’s simulation location.
mem[1] = 3; // x = 3;
mem[mem[3]] = 4; // dereference ’*’ means
                 // we have to nest mem[]’s
mem[2] = mem[1]; // y = x;

Array Simulation Model解决了内存位置的问题，但是要求每个变量都有固定的位置。在现实中我们并不一定能够确定所有的内存对象的具体大小，例如一个变长数组或者一个位置大小的堆块，该模型就无法使用。所以针对这个弊端提出了针对Array Simulation Model的改进，其将一个单独的大数组更换为多个小数组，每个内存对象都有一个对应的数组，但是在这种形式下很难表示复合对象，例如

c
struct s
{
  int d;
} sa[2];

如果我们使用单个数组来表示该结构则存在和未改进版本同样的问题，如果使用多个数组则会丢失内存对象之间的层次关系。

作者的内存模型

Region Based Ternary Model

使用两个映射对于内存状态进行建模: 一个变量环境将位置与每个变量关联，一个存储将值和每个位置关联。形式上，作者将变量环境 $Env$ 的映射定义成为

$Env = Var \rightarrow Loc$ , 其中 $Loc$ 是一组位置的集合。

将映射 $store$ 形式化定义为:

$Store = Loc \rightarrow Value$

在此基础上作者定义了一种新的内存位置表示方法 $Region$ , $Region$ 是一个抽象的内存块，对应C语言中的左值表达式。根据C语言的标准， $lvalue$ 表示一个对象类型的表达式。也就是说，一个左值表达式有一个关联的内存对象，所以我们使用一个抽象区域来表示这个内存对象。此外，表示相同内存对象的左值表达式应该具有与之对应的相同区域。

作者定义了几种 $Region$ ，

对于显式声明的变量，作者提供了变量声明标识 $VarRegion$ 。每一个变量都一个唯一对应的 $VarRegion$ 。
- 如果变量是数组或者结构类型，则其有一个称为 $element$ 或者 $field$ 的子对象，为了表示内存之间的层次结构，引入了子区域的概念，一个区域可以指向另一个区域的子区域。一个Super Region的指针可以指向另外一个Super Region的子区域
对于数组元素有 $ElementRegion$ 及其Super Region指针指向其他数组区域。
- $ElementRegion$ 由他们的数组区域和索引来标识
对于Struct元素有 $FieldRegion$ 及其Super Region指针指向其他Struct区域。
- $FieldRegion$ 由他们的结构区域和字段声明来标识
针对C语言中的三种存储类: local(stack)、global(static)、dynamically allocated(heap)，也有三种类型的 $MemSpaceRegion$ 与之对应
- 所有的局部变量都将 $stack MemSpaceRegion$ 作为他们的Super Region
- 所有的全局变量都将 $static MemSpaceRegion$ 作为他们的Super Region
- 所有动态分配的对象都将 $heap MemSpaceRegion$ 作为他们的Super Region
在静态分析中，有时候会使用符号值。假设函数参数和全局变量在函数的入口处保存符号值，如果符号变量是一个指针则可能指向一个未知的内存块，所以使用 $SymbolicRegion$ 表示符号指针指向的内存块。
- $SymbolicRegion$ 由指向他们的符号指针的值来标识。

除了存储类之外，内存对象还有 $extents$ 或者 $size$ 属性。一些对象的 $extents$ 是显式定义的，例如一个字符变量的 $extents$ 是一个字节。但是动态分配对象的 $extents$ 是不确定的。所以我们使用从一个对象关联的 $Region$ 到他的 $extent$ 的映射，即 $Region - extent$ 映射对来记录该信息。

$extent$ 可以有多种形式

具体整数值(concreate interger value)
符号未知值(symbolic unknown value)

内存的状态由 $Region$ 的绑定来进行建模。绑定通常有两种形式

直接绑定(direct binding): 在赋值表达式中，一般都为直接绑定。例如x = 3;，我们通过直接绑定将x的 $Region$ 与3进行绑定。
默认绑定(default binding): 默认绑定通常是在 $Super Region$ 上使用，例如bzero(buf);，我们可以使用默认绑定将buf的 $Region$ 与0进行绑定，否则我们需要将buf中的每个元素的 $Region$ 与0进行绑定，显然开支非常大。

Region View

C语言允许指针类型之间进行转换给静态分析工具带来了很大的困难。

c
void *p = malloc(10);
char *buf1 = (char *) p;
buf1[0] = ’a’;
int *buf2 = (int *) p;
buf2[0] = 0;
char c = buf1[0];

这种代码模式在系统程序中相当常见，程序员通常分配一个通用类型的内存块，然后根据需要将其转换成为不同类型。这种使用(滥用)方法，本质是在C语言中可以存在无类型的泛型内存块。在上述的代码中，由 $p$ 指向的内存块就是这样的存在，后面将其转换成为char *和int *可以理解成为在其上安装了一个 $view$ ，当他被buf1指针操作的时候即被视作是char类型，当他被buf2操作的时候就被视作是int类型。

我们使用从 $Region$ 到 $view$ 的映射来表示一些匿名类型的区域。将一个泛型的内存块强制转换为某种类型相当于向这块内存块添加一个 $view$ 。我们创建一个匿名类型的区域来表示 $view$ ，然后在将泛型内存块强制转换到另一个类型的时候，将创建一个新的匿名类型区域来表示这个新的 $view$ 。

一个 $Region$ 可以同时拥有多个 $view$ 但是同时只能有一个 $view$ 生效。

在上述例子中，模型的行为表示为，当表达式buf1[0]='a'之后buf[0]的值为a。但是当表达式buf[2]=0之后，我们不仅将buf2[0]的值设置为0，同时还删除了buf1[0]的绑定，当c被赋值成为buf1[0]的时候，我们可以发现buf1[0]是一个未定义的值。

Simulation of C Semantics

在上述模型的基础上，作者对对其进行了扩充。作者将程序状态(program state)由两个映射进行建模: $Enviroment$ (环境)、 $Store$ (存储)。

作者将 $Enviroment$ 定义成由表达式到值的映射

$Env: Expr\rightarrow SVal$ 其中 $Expr$ 是C表达式的一个元素， $SVal$ 是一种抽象值。

作者将 $Store$ 定义为从Region到Value的映射

$Store: Region \rightarrow SVal$ 其中 $Region$ 是内存对象的抽象表示。

Abstract Value

我们将符号模拟中出现的值分为两类

位置相关的 $loc$ ， $loc$ 表示抽象内存位置，简单来说指针都是 $loc$
非位置相关的 $non-loc$ ，具体整数、符号整数等都是 $non-loc$

l-value and r-value

根据C语言中的定义，表达式分为lvalue和rvalue，引用对象的 $Expr$ 是lvalue表达式，其他都是rvalue表达式。我们将表达式的左值定义为预期关联的内存对象的内存位置。如果表达式是左值表达式，则表达式的右值为与内存对象相关联的值；如果表达式不是左值表达式，则表达式的右值表示为语义值。

目录