库结构

CSA库结构分为两层：

  1. 一个（低层）静态分析引擎（GRExprEngine.cpp 和 同类）
  2. 一些静态检查器（×Checker.cpp）

静态检查器是通过Checker和CheckerVisitor接口（Checker.h和CheckerVisitor.h）构建在静态分析引擎之上的。

检查器的接口被设计得尽可能小而简单，目的是为了将它们与内部的分析引擎尽可能地分离开来。

如何工作

CSA是由一些论文启发而产生的。链接附在文章最后。

简而言之，CSA是一个跟踪所有可执行路径的代码模拟器。程序的状态（变量和表达式的值）被封装成ProgramState（状态）。程序中的一个位置被成为ProgramPoint（程序点）。ProgramState和ProgramPoint的组合就是ExplodedGraph的节点。exploded这个词来源于explode控制流图（CFG）的边。

从概念上来说，CSA通过ExplodedGraph来做可达性分析。开始一个root节点，它代表着程序的进入点和初始状态。然后通过分析独立的表达式来模拟转换。一个表达式的分析可引起程序状态（ProgramState）的改变，随即在ExplodedGraph中产生一个包含更新后的程序状态与程序点的节点。通过查找满足“bug条件”（违反checker条件）的节点，就可以找到bug。

CSA通过推理分支然后将状态分叉：真-分支上的满足条件被假定为真，假-分支的满足条件被假定为假。这种假设创建了对程序值的约束，这些约束都被ProgramState对象记录了下来（并被ConstraintManager使用）。如果对分支条件的假设引起约束不满足的话，那么这个分支就被认为是不可行的，这条路径就不会被采用。CSA通过这种方法来实现路径敏感性的分析。CSA通过缓存节点来避免指数爆炸。如果一个即将被生成的新节点与已经存在的节点有相同的程序点和状态，那么这条路径会被“缓存”起来，以及直接重用已经存在的节点（并不会生成新节点）。所以ExplodedGraph并不是一个DAG，它
可能包含环（路径可能往回循环然后去到另外的路径或“缓存”路径）。

ProgramState和ExplodedNode在生成后是不可变的。一旦创建了一个ProgramState，你就需要创建一个新的ProgramState来标志一个新的程序状态。这种不变性是关键，因为ExplodedGraph表示的是被分析程序从程序进入点开始的行为。为了精确地表达这些行为，我们使用功能性的数据结构（如ImmutableMap）在实例之间共享数据。

最后，独立的那些Checker通过操作分析状态来工作。分析引擎通过一个访问接口来与它们交互。例如，GRExprEngine调用PreVisitCallExpr()方法，去通知Checker现在准备分析一个CallExpr，然后Checker就去检查是否有不满足的前提条件。Checker可以什么都不做，也可以生成一个新的ProgramState和包含更新后检查状态的ExplodedNode。如果Checker找到一个bug，它会向BugReporter对象报告bug，并提供给它这条路径上的最后触发bug的ExplodedNode。

关于C++

使用CSA

如果你对为C++表达式提供支持感兴趣的话，那么最适合你去看的部分是GRExprEngine的访问逻辑，这部分处理单个表达式的模拟。有很多关于表达式如何处理的例子。

如果你对写Checker有兴趣的话，那么去看Checker和CheckerVisitor接口（Checker.h和CheckerVisitor.h）。同时也看一看那些叫“×Checker.cpp”的文件，这样你就知道该如何实现这些接口了。

调试 CSA

有许多调试相关的有用的命令行命令，例如：

1
2
3
4
$ clang -cc1 -help | grep analyze
 -analyzer-function <value>
 -analyzer-display-progress
 -analyzer-viz-egraph-graphviz

第一个命令允许你只分析特定的函数。
第二个命令将被分析的函数打印到终端。
第三个命令生成一个ExplodedGraph的graphviz点图。
这对调试CSA和查看模拟结果非常有帮助。

当然，查看CFG（Control-Flow-Graph）同样也非常有帮助：

1
2
3
4
5
6
$ clang -cc1 -help | grep cfg
 -cfg-add-implicit-dtors	对于所有分析，添加C++的隐式析构函数到CFG
 -cfg-add-initializers		对于所有分析，添加C++的构造函数到CFG
 -cfg-dump					显示CFG
 -cfg-view					使用GraphViz查看CFG
 -unoptimized-cfg			对于所有分析，生成未优化的CFG

-cfg-dump在终端打印CFG的文本格式的表示；
-cfg-view生成一个GraphViz格式的表示。

引用

[1] Precise interprocedural dataflow analysis via graph reachability,
T Reps, S Horwitz, and M Sagiv, POPL '95,
http://portal.acm.org/citation.cfm?id=199462

[2] A memory model for static analysis of C programs, Z Xu, T
Kremenek, and J Zhang, http://lcs.ios.ac.cn/~xzx/memmodel.pdf