『论文笔记』A Memory Model for Static Analysis of C Programs

前置知识：

• C 语言中的左值 / 右值表达式；
• C 语言的内存组织
• 符号执行与路径敏感分析的理论基础

---

Clang 编译器使用的内存模型是一种 基于区域（Region）的三元组模型 ，其设计的出发点是服务于程序分析中对程序进行自动错误检查和测试数据生成的这一需求。

传统数据流分析服务的是编译优化，在数据流分析场景中，程序点状态的布尔信息已经足够使用（因此我们建立一个表示布尔信息的位向量的格，用这种简化的形式进行数据流信息的传播与分析），而想要进行错误检查，则需要采用 路径敏感 的方法，对程序的运行时状态进行分析，此时简单的布尔信息就完全不够用了。

为了保存程序点中最精确的程序状态信息，目前采用的是符号分析技术。本文介绍的三元组内存模型则是一种对程序状态的建模方法，基于它就可以得到一个较为完善的、能够进行精确符号分析的模型。

模型基本框架

此前曾经提出过比较基本的几个模型，它们都具有局限性：

• 名字 - 值映射模型
  • 缺少地址概念，无法表示指针变量的值
• 大数组模型
  • 使用一个大数组来表示计算机内存，将对变量的操作转化为对数组单元的操作，因此需要在符号表中登记变量在大数组中的下标信息
  • 对每个内存对象都需要知道其具体长度，处理形如 int *p = malloc(n) 的语句时，在符号执行场景下无法得知具体长度，进而无法对其建模
• 独立数组模型
  • 为每个内存对象单独分配一个数组
  • 对指针变量使用一个 <变量，位移> 对来表征其指向值（不仅要知道变量的相对地址，还要知道其指向变量）
  • 无法表示没有显式变量名的内存对象，指针嵌套着指几层就寄了

上面三个模型的局限性归根到底都在于试图建立变量名到值的直接映射。此时重新考虑程序分析的本质问题：用数学对计算机程序进行正确性分析，或者说要从程序代码中提取出一组关于程序中值的静态关系。而数学与程序的本质区别在于 存储 ，也即，程序操作的对象其实是内存状态。因此，本三元组模型的基本思路就是要建立从程序中的表达式到内存位置的映射，再通过内存位置到值的映射得到程序语句实际操作的值，最终得到关于值的数学关系。

此前有过关于 C 内存组织和左值 / 右值表达式的理论基础之后，这里的建模思路实际上就很清晰了，就是一个对内存指向关系计算的模拟。

最终，作者给出了 区域（Region） 这一建模概念（它的具体含义是对内存对象的抽象表示），把 存储 建模成了一个从区域到值的映射。

---

对一个表达式，使用如下的一个三元组来解释它：

其中需要注意的是区域概念之间的 层次关系 ：区域之间存在着明确的父子层级。对于程序的栈、堆、静态存储，也用三个区域 stack region、heap region 和 static region 表示。区域的层次关系允许我们通过查询区域之间的层次关系来解决内存指向关系的计算问题。这样，就使得前面谈到的区域区分问题（比如不同 struct 的同一个域）、指针嵌套问题等等得到解决。

例如，数组元素的父区域是数组区域，局部数组的的父区域是 stack region。

区域有起始位置、范围和类型三个特征概念（非常类似 C 语言内存组织模型）。这使得我们可以解决诸如区分数组指针和指针数组这样的问题。

关于 Value 的两个分类，其目的是为了解决指针的表示，结合 region 的概念为内存指向关系计算提供方便。我们知道表达式的左值是指针，右值是指针或者非指针，在这个模型里，指针值（也即分类中的位置值）用一个区域来表示，而非指针值则用其本身数字来常规地描述。

基于该模型的 C 语言语义模拟

本节讲述如何使用上述的三元组模型来模拟 C 语言语义。

存储

• Region(Var) : 变量 Var 对应的区域
• Store(R) : 区域 R 对应的值（内存区域中的比特值）
• lvalue(expr) : 表达式 expr 的左值，是一个指针值，在本文的分析系统中使用一个 Region 来表示
  • 获取 lvalue(expr) 的值: Store(lvaule(expr))
• rvalue(expr) : 表达式 expr 的右值，可能是一个常规值也可能是一个指针值，可以通过程序语义求到
• Region(expr) (if expr is an variable): 变量对应的区域
  • 可见 lvalue(expr) 在 expr 为变量时返回的就是这个值

声明

• 简单变量
  • 为其分配一个区域表示它对应的内存对象
• 数组或结构变量
  • 给变量本身分配区域；
  • 对每个数组元素或结构域都分配区域，并将其父区域设置为变量的区域
  • 在声明的修饰符中，为 extern 分配存储区域，特殊处理 static 的赋值，忽略 auto 和 register（因为它们与静态分析无关）

为变量声明分配内存区域后，在 Store 中建立从该声明到分配的内存区域的映射。

表达式求值

数组变量表达式只有左值没有右值，具体原因可以复习 C 系统级编程相关内容。

其中 ElementRegion(base, index) 根据 base 表示的数组区域和 index 表示的位移得到一个数组元素区域，其父区域是 base 表示的数组区域。FieldRegion(base, field) 类似，base 是父级结构区域，field 是域的声明。

上表中没有谈到的是二元运算。二元运算在符号执行中的求值规则是：

• 若所有操作数都是具体数则按具体运算进行
• 若至少一个操作数是符号值则按符号运算进行
• 若至少一个操作数是 undefined 的，则结果是 undefined 的
• 若所有操作数已定义且至少有一个是 unnamed 的，则结果是 unnamed 的
• 条件表达式的值是一个约束，需要结合其他约束求解得到真假值
  • 注意复合条件表达式的最短路求值和 lazy evaluation 问题（只先构造形如 3 == 5 这样的符号表示，等到不得不计算的时候再计算布尔值）

---

区域内存模型可以在不做指针分析的情况下，只通过上述的求值算法就得到内存对象的正确对应，这样就不用做别名分析了。一方面是因为模型的先进性，另一方面是因为做的是路径敏感分析，每条特定执行路径上的信息是确定的。