Configurable Pointer-Alias Analysis for CPAchecker 原文

背景
描述指针-值关系的方法
不同分析方法
出色的算法代表
- Andersen’s Pointer Analysis
  - 定义
  - 解释
  - 例子
  - 复杂度分析
- Steensgaard’s Pointer Analysis
  - 定义
  - 例子
验证技术
- 软件验证（Program Analysis）
- 模型验证（Model Checking）
自动机

背景

在C代码环境下仅考虑值分析是不够全面的，故需要考虑对指针的分析。

描述指针-值关系的方法

Points-to

描述指针$\rightarrow$值的集合，例如
$$
[p\rightarrow{i}]
$$
或者
$$
pts(p)={i}
$$

Alias pairs

描述具有相同地址的指针-值对，例如
$$
(\ast p,i)
$$

Equivalence sets

描述具有相同地址的指针、值集合，例如
$$
{\ast p,i}
$$

对于样例：

int i, j, *p, *q, (*fn_ptr)(int); 
int id(int i) {return(i);} 
fn_ptr = &id; 
p = &i; 
q = &j;

可得到：

Points-to sets: $[p\rightarrow{i}],[fn_ptr\rightarrow{id}],[q\rightarrow{j}]$
Alias pairs: $(\ast p \rightarrow i),(\ast r \rightarrow i),(\ast p,\ast r),(\ast q,j)$
Equivalence sets: $ {\ast p,\ast r,i},{\ast q,j} $

对于后两者，会出现爆炸情况，且并没有区分函数指针

不同分析方法

函数内部vs函数之间- 3.3.2

前者假定函数调用影响了所有的变量，而后者则不是。

前者更慢

流敏感vs流不敏感 - 3.3.3

前者假定所有代码按照顺序逐行执行，而后者不假定之。例如

1
2
3

int i, j, *p;
p = &i;
p = &j;

对于流不敏感，经过计算生成$[p\to{i,j}]$
对于流敏感：
- 对于line1，生成空
- 对于line2，生成$[p\to{i}]$
- 对于line3，生成$[q\to{j}]$

流敏感非常慢，并且降低了扩展性。

上下文敏感vs上下文不敏感 - 3.3.4

考虑下述代码：

1
2
3

int i, j;   //1 
p = id(&i); //2 
q = id(&j); //3

1	int* id(int* r) { return (r); }

对于上下文敏感：
- 对于line2，生成$[p\to{i}]$
- 对于line3，生成$[q\to{j}]$
对于上下文不敏感，会认为函数$id$的返回值是${i,j}$，因为每次结果都会与先前的结果融合

Every time $id$ is being called, the result will be merged with the previous one, possibly creating ambiguous values for the return variable $r$ in $id$.

对上下文不敏感者，可能导致非真实路径产生。

关于结构体、共用体 - 3.3.5

对于不敏感（流、上下文）者，不能很好的处理结构体、共用体，例如

struct Person
{
    int age;
}p1, p2;
Person *ptr1 = p1;
Person *ptr2 = p2;

只能生成
$$
[ptr1\to{Person}]
$$
和
$$
[ptr2\to{Person}]
$$

对于字段（不）敏感者，考虑下述代码：

int i, j;                       //1 
struct S {int *p; int *q;} st;  //2 
S *ptr = &st;                   //3 
ptr->p = &i;                    //4 
ptr->q = &j;                    //5

敏感者可生成$[S,st.p\to{i}]$和$[S,st.q\to{j}]$
不敏感者仅能生成$[S,st.p\to{i,j}]$

总结

流、上下文敏感是被推荐的，但是单独每个效率极低，更不必说配合使用；
为了提高效率、实用性，必要的容忍不精确是必须的；

出色的算法代表

Andersen’s Pointer Analysis

流不敏感
上下文不敏感
函数间
may-pointer-alias
定义

引用
$$
p=\And i;\Rightarrow i\in pts(p)
$$
解引用-读
$$
p=\ast q;\Rightarrow \forall x \in pts(q):pts(x)\subseteq pts(p)
$$
解引用-写
$$
\ast p=q;\Rightarrow \forall x \in pts(p):pts(q)\subseteq pts(x)
$$
复制（Aliasing）
$$
p=q;\Rightarrow pts(q)\subseteq pts(p)
$$
解释
在解引用时，一条基础约束便产生，便可知道集合$p$至少含有元素变量$i$
在解引用指针$q$时，变量$p$就变成了$q$的超集（父集），也就是说$p$涵盖了全体$q$可能的取值
类比2
在将$q$复制进$p$时，后者则变成了前者的超集，涵盖了其所有可能的取值
例子

代码	数学符号
`int i, p, q, r, s, *t;`
`p = &i;`	$i\in pts(p)$
`r = &p;`	$p\in pts(r)$
`s = &q;`	$q\in pts(s)$
`*s = p;`	$\forall x \in pts(s):pts(p)\subseteq pts(x)$
`s = *r;`	$\forall x \in pts(r):pts(x)\subseteq pts(s)$
`t = r;`	$pts(r)\subseteq pts(t)$

从上面的例子可以推断出以下约束

$$\begin{matrix}
i\in pts(p) & \Rightarrow & [p\to {i}]\\
p\in pts(r) & \Rightarrow & [r\to{p}]\\
q\in pts(s) & \Rightarrow & [s\to{q}]\\
\forall x \in pts(s):pts(p)\subseteq pts(x) & \Rightarrow & pts(p)\subseteq pts(q) & \Rightarrow & [q\to{i}]\\
\forall x \in pts(r):pts(x)\subseteq pts(s) & \Rightarrow & pts(p)\subseteq pts(s) & \Rightarrow & [s\to{q,i}]\\
pts(r)\subseteq pts(t) & \Rightarrow & [t\to{p}]\\
\end{matrix}
$$

最终结果就是

$$
[p\to {i}],[r\to {p}],[q\to {i}],\require{color}\colorbox{red}{$[s\to {q,i}]$},[t\to {p}]
$$

而预期是

$$
[p\to {i}],[r\to {p}],[q\to {i}],\require{color}\colorbox{red}{$[s \to {i}]$},[t\to {p}]
$$
可以看出该方法精确度较高，仅有一处指针指向多余。

更多的复制与解引用会导致精度降低，因为在指针传播过程中，子集被逐步放大

However, the more aliasing or dereferencing there is in the input program, the less precise the results will get due to the corresponding constraints which continuously propagate the according subsets.

复杂度分析

对于$n$条约束，在最坏的情况下，即每个指针变量全部指向其他全部指针，复杂度为$O(n^2)$；进一步地，如果存在解引用-读，复杂度将会变为$O(n^3)$

Steensgaard’s Pointer Analysis

流不敏感
上下文不敏感
函数间
may-pointer-alias
指针信息双向流动，这加快了分析速度但是降低了精度
复杂度几乎是线性，实际上是
$$
O(n\alpha(n,n))
$$
其中
$$
\alpha(x,y) =
\begin{cases}
y+1 &, \text{if }x=0 \\
\alpha(x-1,1) &, \text{if }y=0\\
\alpha(x-1,\alpha(x,y-1)) &, \text{otherwise}
\end{cases}
$$

$$
\alpha(2^{132})<4
$$

可以证明

$$
\lim_{x\to+\infty}\alpha(x,x)=1
$$

定义

join(p1,p2)函数被定义为将p2指针指向的所有可能变量的集合加入到p1中；或者按照如下伪代码定义：

join(p1, p2) 
    if (p1 == p2) 
        return 
    p1next = *p1; 
    p2next = *p2; 
    unify(p1, p2) 
    join(p1next, p2next)

引用
$$
p=\And i;\Rightarrow join(\ast p,i)
$$
解引用-读
$$
p=\ast q;\Rightarrow join(\ast p,\ast \ast q)
$$
解引用-写
$$
\ast p=q;\Rightarrow join(\ast \ast p,\ast q)
$$
复制（Aliasing）
$$
p=q;\Rightarrow join(\ast p,\ast q)
$$

例子

参照例子

经过分析可得

$$
\begin{matrix}
1.&join(\ast p,i) & \Rightarrow & [p\to{i}]\\
2.&join(\ast r,p) & \Rightarrow & [r\to{p}]\\
3.&join(\ast s,q) & \Rightarrow & [s\to{q}]\\
4.&join(\ast \ast s,p) & \Rightarrow & [q\to{i}]\\
5.&join(\ast s,\ast \ast r) & \Rightarrow & [s\to{q,i}]\\
6.&join(\ast t,\ast r) & \Rightarrow & [t\to{p}]\\
\end{matrix}
$$
其中，对于4，s指针指向的变量变更为p，而p指向i，即得q指向i

综上，最终结果就是

$$
[p\to {q,i}],\require{color}\colorbox{green}{$[r\to {p}]$},[q\to {q,i}],[q,i\to {q,i}],\require{color}\colorbox{green}{$[t\to {p}]$}
$$

和预期

$$
[p\to {i}],\require{color}\colorbox{green}{$[r\to {p}]$},[q\to {i}],[s \to {i}],\require{color}\colorbox{green}{$[t\to {p}]$}
$$

相差较大

验证技术

分为动态验证技术和静态验证技术，其中：

动态验证技术通过详细地和引起失败地方式执行代码，即黑盒测试
静态验证技术不执行代码，只是测试是否可以满足给定条件；其中，静态验证技术可以分为
- 软件验证
- 模型验证

软件验证（Program Analysis）

为了兼顾有效性和效率，通常是路径不敏感的。也就是说，等效的路径结果会被合并。
典型应用：错误查找、编译器优化。

模型验证（Model Checking）

通过给定系统有限的模型和标准化的性质，系统性地检查相关性质是否符合模型。

因此，模型验证需要两个重要因素：

期望的模型
给定的约束规范

通常来说，系统模型指的是有限状态图和推断可达树（inferred reachability tree）

由于使用详尽的探索模型，每次检测都会详尽地检测是否符合模型；虽然正确性得到保障，但是效率低下，只适合小型程序。

为此可以将二者合并。

自动机

控制流自动机（Control Flow Automaton, or CFA）

定义

4.1 P25

CFA由以下部分组成：
1. 代表程序计数器($pc$)的节点$L$
2. 代表程序入口的初始节点$pc_0$
3. 边集合$G\subseteq L\times Ops \times L$
每个具体的状态的变量值是从$X\cup{pc}$取得的。
每个边$g\in G$同时定义了一个转移关系$\overset{g}{\to} \subseteq C \times {g} \times C$，其中：
1. $C$是所有具体状态的集合
2. $\to$被定义为$\to=\bigcup_{g\in G} \overset{g}{\to}$
  
  当存在状态序列$ \langle c_0,c_1,…,c_n \rangle $，且当$c_0\in r$时，$\forall i \in [1,n],c_{i-1}\to c_i$，称$c_n$从$r$可达，记作$c_n\in Reach(r)$

可配置程序自动机（Configurable Program Analysis, or CPA）

定义

$\mathbb D=(D,\rightsquigarrow,\text{merge},\text{stop})$由四部分组成。

抽象域$D=(C,\varepsilon,[[\centerdot]])$由三部分组成
1. 具体状态集合$C$
2. 半格$\varepsilon$，其中$\varepsilon=(E,\top,\bot,\sqsubseteq,\sqcup)$，由五部分组成
  1. 代表抽象状态的可达无穷的域元素集合$E$
  2. 顶端元素（top element）$\top \in E$
  3. 底端元素（bottom element）$\bot \in E$
  4. 先序关系（preorder）$\sqsubseteq \subseteq E \times E$
  5. 总函数（total function）$\sqcup:E\times E\to E$，代表加入半格的操作符
3. 实例化函数$[[\centerdot]]$，其中$[[\centerdot]]:E\to 2^C$，代表将每个抽象状态指派进具体状态集合中；考虑完备性，抽象域必须满足以下条件
  1. $[[\top]]=C \text{ and } [[\bot]]=\emptyset$
  2. $\forall e,e’ \in E:[[e]]\cup[[e’]]\subseteq[[e\sqcup e’]]$(加入操作符是精确的或者是上近似的)
转移关系$\rightsquigarrow\subseteq E\times G \times E$为给定的所有可能的抽象状态$e,e’\in E$分配一条CFA边$g\in G$，记作$e\overset{g}{\rightsquigarrow} e’$或者$(e,g,e’)\in \rightsquigarrow$
考虑完备性，转移关系必须满足以下条件
1. $\forall e\in E: \exists e’\in E: e \rightsquigarrow e’$(转移关系总体)
2. $\forall e\in E,g\in G: \bigcup_{c\in [[e]]}{ c’\vert c\overset{g}{\to}c’ } \subseteq \bigcup_{e\overset{g}{\rightsquigarrow} e’}[[e’]]$(操作的上近似)
合并操作$\text{merge}:E\times E \to E$用于合并两个抽象状态及其信息；考虑完备性，必须满足以下条件：
1. $\forall e,e’:e’ \sqsubseteq \text{merge}(e,e’)$，可以保证结果必然比第二个参数更抽象或同等抽象；从两方面考虑：
  1. 结果仅能介于$e’,\top$之间
  2. 操作不具有交换性（commutative）
终止操作$\text{stop}:E\times 2^E \to \mathbb B$用于检查抽象状态（第一个参数）是否被抽象状态集合（第二个参数）覆盖；考虑完备性，需要满足：
1. $\forall e\in E,R\subseteq E:\text{stop}(e,R)=true\Rightarrow[[e]]\subseteq \bigcup_{e’\in R}[[e’]]$

CPAchecker

复合CPA由$C=(\mathbb D_1,\mathbb D_2,…,\mathbb D_n,\rightsquigarrow_\times,\text{merge}_ \times,\text{stop}_ \times)$定义，$n$是非无穷正整数，$\rightsquigarrow_\times,\text{merge}_ \times,\text{stop}_ \times$是相关符号的复合定义。进一步地，定义两种新符号$\downarrow,\preccurlyeq$

增强符号$\downarrow:E_1\times E_2\to E_1$强调了从格集合$E_1$到格集合$E2$的带信息的抽象状态，但必须满足$\downarrow(e,e’)\sqsubseteq e$
比较符号$\preccurlyeq \subseteq E_1\times E_2$用于比较不同格的元素

$\rightsquigarrow_\times,\text{merge}_ \times,\text{stop}_ \times,\downarrow,\preccurlyeq$是$\mathbb D_1,\mathbb D_2(\rightsquigarrow_\times,\text{merge}_ \times,\text{stop}_ \times,[[\centerdot]]_i,E_i,\top_i,\bot_i,\sqsubseteq_i,\sqcup_i)$的表达式

考虑完备性，复合CPA（简化起见，仅考虑2个域的情况） $C=(\mathbb D_1,\mathbb D_2,\mathbb D_n,\rightsquigarrow_\times,\text{merge}_ \times,\text{stop}_ \times)$通过以下约束被可配置程序分析$\mathbb D_\times=(D_\times,\rightsquigarrow_\times,\text{merge}_\times,\text{stop}_\times)$构造：

乘积域$D_\times$被定义为与CPA们的域的直接乘积，$D_\times=D_1 \times D_2=(C,\varepsilon,[[\centerdot]])$。乘积格依据$\varepsilon_\times=\varepsilon_1\times\varepsilon_2=(E_1 \times E_2,(\top_1,\top_2),(\bot_1,\bot_2),\sqsubseteq_\times,\sqcup_\times)$当$(e_1,e_2)\sqsubseteq_\times(e_1’,e_2’)$构建，当且仅当$e_1\sqsubseteq_1e_1’$且$e_2\sqsubseteq_2e_2’$且$(e_1,e_2)\sqcup_\times(e_1’,e_2’)=(e_1\sqcup_1e_1’,e_2\sqcup_2e_2’)$
乘积实例化函数$[[\centerdot]]_\times$被构建当$[[(d_1,d_2)]]_\times=[[d_1]]_\times \cap[[d_2]]_\times$

CPA算法 - 4.3.2

为了执行分析流程，算法将会计算给定CPA和上近似的代表可达具体状态的初始抽象状态；接着C代码将会被抽象出符号树，然后进一步转换为控制流自动机（CFA）。CFA集合和CPA即可构造出该算法的主要构件——复合CPA。在此，全部四个CPA组件均与算法准确度和性能相关。之后，基于其CPA和附加的初始抽象状态$e_0$，计算了一组可达的抽象状态。为此，两抽象状态集合被计算，代表所有已达抽象状态、和包含尚未处理的等待集合。而转移关系则计算当前抽象状态$E$及其后继。该算法考虑了$E$的每个后继$E’$，并使用$\text{merge}$操作将其与现有的抽象状态梳理。如果合并为抽象状态添加了新信息，则将更换旧的抽象状态。如果未达到的新抽象状态未涵盖新的抽象状态，则将添加到访问列表和等待集合中。

样例

显式值分析（Explicit-Value Analysis）

CPAchecker有许多不同的分析。其中之一是显式值分析，旨在跟踪给定输入程序的指定集变量的整数值。此任务需要一个由负责跟踪程序位置的CPA，和另一个用于显式值分析的CPA组成的复合CPA。但是，显式值分析不支持指针分析，这是一个主要的缺陷，因为指针能够完全改变变量的值。因此，在下文中通过加强操作符$\downarrow$获得新的可配置的指针分析来加强显式值分析。

论文5.1 P32

通过上文的CPA规范构建新的指针CPA $\mathbb D_p=(D_p,\rightsquigarrow_p,\text{merge}_p,\text{stop}^{SEP})$，类同，不再赘述。详见论文。

在CPAchecker中Steensgaard 和 Andersen 算法的表现

考虑下述代码

int main() { 
int i, j, *p, *q, **r, **s; //1
p = &i;                     //2
q = &j;                     //3
r = &p;                     //4
s = &q;                     //5
*r = q;                     //6
*s = *r;                    //7
r = s;                      //8
return (0);                 //9 
}

Andersen 和 Steensgaard的表现如下

Configurable Pointer-Alias Analysis for CPAchecker 大创笔记

背景