前言

我们程序分析的学习进入了下一个阶段。在第一篇文章中提到程序分析可以大体分成抽象和搜索两部分，之前都是学习了抽象的部分。我们从数据流分析开始，讨论了抽象的基本思想，分支（包括循环）如何合并，节点如何更新等知识。从理论层面，探讨了数据流分析的的抽象和转换函数必须满足的条件以及数据流分析的性质，因此我们介绍了格理论。特别地，详细介绍了 widening 和 narrowing 的方法。在这一部分，我们建立了对于抽象的方法的基本认识。

然后，我们学习的 Datalog ，从基本数理逻辑出发介绍了逻辑式编程语言，接着介绍了典型的 Souffle 语言和它在程序分析上的应用。

在数据流分析中有几种很典型的方法Def-use 和 SSA，Def-use 主要简化了节点更新时关注的值，缩小了范围。进一步学习了静态单赋值(SSA)的方法，每个变量只赋值一次。但是分支会造成变量赋值不一致的情况，所以加入和交汇函数。为了优化交汇函数，确定什么时候需要在某个基本块引入交汇函数，我们又学习了「支配」「支配边界」的概念以解决这个问题。最后，讨论了无法完全转换成 SSA 时，可以采用部分 SSA 的方法。

具备了单个程序的过程内分析的基础后，我们开始学习过程间分析的基本原理，将过程间分析转换成过程内分析的衔接。特别的，我们以函数调用作为例子，考虑了全局变量和过程间分析导致的精度损失的问题。为了避免函数调用时错误的节点更新操作，我们学习了基于克隆的上下文敏感性分析，并且特别讨论了递归函数如何处理以及不同的上下文类型的处理方式。我们将程序分析转换成图的形式，引入了括号匹配的 CFL-reachability 的精确上下文敏感分析。最后，简要学习了加快过程间分析速度的两种方式函数摘要和动态规划，额外介绍了函数嵌套情况下的合并方式。

指针分析是非常重要的一块内容，我们首先学习了程序分析中的各种敏感性，包括流敏感（flow-sensitive）、路径敏感（path-sensitive）、上下文敏感（context-sensitive）、域敏感（field-sensitive），为后面的进一步学习打下基础。接着学习了流非敏感的指向分析和流敏感指向分析，他们对于指针操作的转换函数不同，但是思路是基本一致的。指针分析中有两个很重要的算法，Anderson 算法和 Steensgaard 算法，希望读者可以掌握它们的思路和规则。基于 get-put 的 CFL-reachability 的指向分析支持域敏感分析，只要了解到有这一回事就可以了。我们探讨了指针分析的难点，它很难处理的情况以及降低敏感度的方式。最后简单介绍了指针分析和控制流分析的关系和 Class Hierarchy Analysis, Rapid Type Analysis 这两种处理方式，意识到指针分析往往是复杂综合性分析的基础。

最后，抽象解释理论是我们以上学习的方法的理论基础，虽然只是简单的学习皮毛，但是我们应该意识到不同抽象域的综合是复杂问题，但是同样是有效的增加程序分析精度的方法。文中以关系抽象域如何增加精度做了说明，特别介绍了数值分析中的八边形抽象。

以上的内容都是笔者自己的学习笔记，不能说理解和认识有多么深刻，但是写出来的论述都是经过了本人的消化，整理和输出的。日后如果有时间将会在阅读完 CMU 的静态程序分析教材、南大的程序分析课程、软件理论基础之后，对内容进行进一步的补充和完善。读者如果感兴趣，可以继续关注本博客。欢迎指出错误和交流学习。让我们开始「搜索」的方式的学习吧，之后会以区块链智能合约代码分析为例，从理论到实践详细介绍符号执行的所有过程。

基础的思想其实都大概涉及到了，由于笔者有论文压力了，只能需要什么学习什么，所以后期学习比较大略，没有最开始小白的时候，记录的那么细致。

约束求解简介

搜索的策略是精确的，但是可能复杂度非常高，所以会放弃超时的路径的搜索。约束求解就是给出了一组约束，如果约束可以成立，那么久给出这么一组值；如果不可以满足，那么找到是哪一部分造成无法满足，这一部分叫做矛盾集（unsatisfiable core）。例如对于约束

{a>10b>5a+b=25

那么约束求解可以找到一组值 (a,b)=(15,10) 满足约束。

历史上出现了很多的约束求解器，这些求解器本质上就是让代码自己做题，去证明。当时因为大规模约束求解计算速度太慢了，但是 2000 年依赖 SAT 算法得到了极大的改进，不过知道现在似乎都还没搞清楚为啥效率就那么高的原理。

SAT solver：解著名的 NP 完全问题
Linear solvers：求线性方程组
Array solvers: 求解包含数组的约束
String solver：求解字符串约束

最后出现了综合性的求解工具 SMT。

SAT

先看 wiki 的介绍：

In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when xis true, so the solver should return "satisfiable".

简单的说是布尔可满足性问题，也就是说对于一个逻辑公式，能否找到一组逻辑变量，使得公式为真。这里希望读者有基础的离散数学基础，将会有助于理解和学习。由于所有的命题公式可以转化成合取范式，所以我们可以给出如下的例子：

F=(a∨¬d)∧(¬b∨c)∧(b∨d)∧(¬b∨¬c∨d)∧(¬a∨¬d)

对于以上的命题公式 F 是否存在一组变量使得 F=1呢。最直接的方法就是遍历，复杂度为 2 的幂次。接下来做一些优化：

短路机制。比如对于 (a∨¬d) 有 1 个为 1，那么就不用算另外一个了，如果整体为 0，那么就剪枝，不再搜索下去。
赋值推导，对于每个变量，如果 a 为 1，那么 ¬a 必须为 0，为了保持 (ad) 为 1，那么 ¬d 必须为 1。这样根据条件推导下去。到那时复杂的公式中推导可能代价比较大，实际应用的规则还是比较复杂。
平凡属性。优先考虑恒真或者恒假的公式，用常数代替。

根据以上的规则，学术界提出了 DPLL 算法，可以知道原理还是相对简单的。另外还有优化的方法，比如

考查变量之间的关系，增加赋值的约束，缩小解空间。
考查子句的等价性，去除冗余性。
是否有些变量比其他变量影响大，先赋值成 0 还是 1。比如优先选择短的子句中的变量，优先选择出现次数多的变量，优先选择出现冲突次数较多的变量等。

在 2000 年初，出现了非常重大的进步，学术界提出了冲突导向的子句学习（CDCL, Conflict-Driven Clause Learning）。也就是一边搜索，一边学习公式的性质，改进搜索方法。这似乎和 AI 类似。笔者暂时跳过，进一步了解可以见：

https://www.cs.ox.ac.uk/people/james.worrell/lec7-2015.pdf
https://stackoverflow.com/questions/12547160/how-does-the-dpll-algorithm-work
https://en.wikipedia.org/wiki/DPLL_algorithm
Decision Procedures An Algorithmic Point of View (Daniel Kroening, Ofer Strichman (auth.))

SMT

SMT 是可满足性模理论（Satisfiability Modulo Theories）的简称。相比于 SAT 判断逻辑公式的可满足性，SMT 加入了一阶逻辑（也就是谓词逻辑）。比如 P(x) 中 x 是个体、P 是谓词，表示 x 具有性质 P。另外一阶逻辑还加入了量词，可以知道 SMT 是基于命题逻辑的 SAT 的拓展。

a+b<c∧f(b)>c∨c>0

例如上面的式子，除了命题逻辑中的运算，还有 < 和 > 符号，实际上小于、大于符号代表着更加一般的逻辑判断。f(b)也是表示逻辑判断。SMT 的任务就是在一组条件下，找到满足所有条件的解。

SMT 的求解有两种方法：

Eager 方法：将 SMT 转换成 SAT，但是现在不常用了。简单的说，就是换元然后增加约束。x2−y2=(x+y)(x−y)=AB 这里用 A,B 换元。换元之后需要保持原有的约束或者增加约束。比如 A+B∈interval(2x),A−B∈interval(2y)。
Lazy 方法：主流方法，SAT 方法和其他方法交叉使用，这样特定领域的问题可以使用现已研究过的高效算法。

定理证明理论的内容，就暂时跳过，有需要再回头学习。读者可以参考如下内容：

SMT 求解器标准：http://smtlib.cs.uiowa.edu/language.shtml

符号执行

符号执行其实和测试很类似，都是一次只跑一条路径，如果有 bug，那么就有 bug，如果找不到也不能说明没 bug。相比于静态分析是在抽象域进行属性抽象，符号执行可能相对精确一些。

通过例子看符号执行的做法。通过符号执行分析：如果 y>0 是否 main(x,y)>0。

int main(x,y) {
y+=10;
if (x>0) {
        x+=10;
        z=x/5;
    }
else {
        z=x/5+2;
        x+=10;
    }
    z+=y;
    return z;
}

无法确定的值，用符号代替。入口处 x=a,y=b,z=0;b>0;next=2，表示下一个语句是第二行。
根据语句改变符号表达式。x=a,y=b+10,z=0;b>0;next=3.
遇到条件分支就增加约束，按一定顺序遍历路径。例如选择 else 分支，x=a,y=b+10,z=0;b>0,a<=0;next=8；选择 if分支 x=a,y=b+10,z=0;b>0,a>0;next=4。
最终得到目标的约束，使用 SMT 求解。

恒成立z>0恒成立?s.t.{x=a+10y=b+10z=(a+10)5+(b+10)a>0b>0

或者

恒成立z>0恒成立?s.t.{x=a+10y=b+10z=a/5+2+(b+10)a⩽0b>0

优化方法

符号执行很容易遇到路径爆炸的问题，就是路径太多、太长，求解就会非常慢。

剪枝

剪枝，是指在分支处调用约束求解的语句，如果约束直接冲突，那么就代表不可达。比较经典的办法是 Eager evaluation，在分支的时候就判断路径的可达性，虽然求解次数更多，但是探索的路径更少。但是上面示例中 Lazy evaluation，只对完整路径判断，也有自己的好处。约束越多，就越容易发生冲突，所以判断无解的速度也很快。