2010-A Memory Model for Static Analysis of C Programs

[skyleaworlder]

https://lcs.ios.ac.cn/~xzx/memmodel.pdf

Zhongxing Xu1 , Ted Kremenek2, and Jian Zhang1
1 State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences xzx@ios.ac.cn zj@ios.ac.cn
2 Apple Inc. kremenek@apple.com

from FDU-PAG Wiki

ISOLA '10

[skyleaworlder]

文中提出的内存模型适用于 path-sensitive 分析，比如符号执行，abs 里面说本文的内存模型可以支持任意层的 pointer dereference，pointer arithmetic，复杂的复合类型，感觉 C 语言的特性大体满足了。

Sec 2 和 Sec 3 提出了两种如果他不说我都不知道算内存模型的内存模型，Sec 2 介绍的 name binding model 只是绑定了名字，无法有效处理别名，array simulation model 通过把内存想象成一个大数组，为确定大小的数据结构分配内存单元，但是无法处理不确定大小的数据结构。

[skyleaworlder]

就像中文互联网中对左右值的理解（左值就是在等号左边、可以取地址；右值就是在等号右边，没有地址）。在本文看来，C 语言中 “左值表达式” 可以看作 “refer to 一个对象” 的表达式，“右值表达式” 就是除 “refer to 一个对象” 之外的所有表达式（比如说字面量、未经优化的函数返回值等）。

而 “表达式的左值” 则看作 “该左值相关联的那个对象的地址”，“表达式的右值” 可以看作：

• 如果是 “左值表达式的右值”，那就是 “该左值表达式相关的那个对象” 的地址指向的值；
• 如果是 “右值表达式的右值”，那就是字面意思。

左右值表达式和左右值不是一个概念：

• 左值表达式有左值和右值（可以取地址，这个地址又对应了一个值，但这个值不是地址的数值，而是地址指向的那个值。不过这个值有的时候或许还真是另一个 region 的 r-value），右值表达式一定只有右值。
• 左值只能是 loc（），但右值可以是 loc 和 non-loc。

文中给出了一个语法对应 l-value / r-value 的计算规则。举例来说，alloca(n) 是要分配内存，返回的是一个 region；*expr 本身这个 expr 就是个指针，*expr 的左值就是 *expr 对应的那个对象的地址，恰好就等于 expr 这个指针的值，也就是 r-value(expr)；*expr 的右值自然就是在 Store 里面找。

[skyleaworlder]

• loc 可以是 region 或者 unknown。因为表示的是 memory model 中的 location，所以允许不知道确切的地址。
• non-loc 可以是一个具体的值，比如 3, "asd" 之类；也可以是一个符号值，比如一个还未确定的入参。

文中提出了一个 tenary model，总之就是两个 map，一个 map 从 “表达式” 到 SVal，也就是上面这两个无序列表说的。另一个 map (Store) 从 region 到 SVal，看起来更广泛用于 Store(l-value(x)) ==> r-value(x)。

[skyleaworlder]

本文疑点很多，if-else 合并处怎么处理？循环和递归怎么处理？展开的话展开几层？一个 region 只对应一个 value？

总之不看 LLVM 实际代码的话根本不知道这些问题的答案。我的评价是写了等于没写。