A Casual Introduction to Algebraic Program Analysis (In Chinese)

本文参考了 Zachary Kincaid 和 Thomas Reps 在 CAV 2021 上的关于代数程序分析（Algebraic Program Analysis）的教程^{1 2}。

代数程序分析简单来说就是一种基于代数结构来设计程序分析的方法论：某种代数结构中的元素代表了程序的含义，而其上的运算则代表组合程序含义的方式。 这其实跟我们在程序语法树上用结构递归定义指称语义（Denotational Semantics）的方式类似： $$\begin{array}{rl}\mathcal{A}[-]& :\mathit{Program}\to \mathit{Meaning}\\ \mathcal{A}[S_1;S_2]& =\mathcal{A}[S_1]\cdot \mathcal{A}[S_2]\\ \mathcal{A}[\mathbf{if}(\ast )\{S_1\}\mathbf{else}\{S_2\}]& =\mathcal{A}[S_1]+\mathcal{A}[S_2]\\ \mathcal{A}[\mathbf{while}(\ast )\{S_0\}]& =(\mathcal{A}[S_0]{)}^{\ast }\end{array}$$ 而上面式子中的 $\cdot$、$+$ 和 ${}^{\ast }$ 就可以视作某种代数结构所支持的运算。 这种方式具有良好的 Compositionality：一个程序的含义总是由该程序的组成部分的含义结合而来。 例如，如果上面的 $\mathcal{A}$ 代表了一个程序分析，那么我们需要指定如何实现连接（$\cdot$）、分支（$+$）和循环（${}^{\ast }$）这三种运算。 注意，这里出现了一个与传统基于迭代的程序分析的重要不同：一个循环语句的含义并不是由反复迭代循环体直到不动点来获得，而是通过一个显式的 ${}^{\ast }$ 运算来获得。 换句话说，代数程序分析允许我们使用别的（非迭代的）方式来分析循环，这就为我们设计新的程序分析技术提供了可能性。

在本文中，我们考虑通过状态转移公式代数（Transition Formula Alegebras）来分析程序变量间的数值关系。 一个状态转移公式$F(X,X^{\prime })$是一个逻辑公式，它描述了程序状态上的转移关系：$X$ 集合表示前状态（pre-state）的变量，$X^{\prime }$ 集合表示后状态（post-state）的变量。 比如我们考虑变量有 $x,y$，那么程序语句 x = x + 1; 的状态转移公式就是 $x^{\prime }=x+1\wedge y^{\prime }=y$。 对于一个固定的变量集合 $X$，我们考虑在所有可能的状态转移公式 $F(X,X^{\prime })$ 上建立一个适用于程序分析的代数结构。 在传统程序分析中，我们往往需要预先对可能的公式进行限制来使得迭代算法可以收敛：例如，只考虑变量间的线性不等式。 在代数程序分析中，我们不需要这种预先的限制，而是可以在实现循环运算（${}^{\ast }$）时以即插即用的方式使用不同的近似方法。 在状态转移公式代数中，我们定义常数 $0$ 为 $\mathit{false}$，常数 $1$ 为 $\underset{x\in X}{\bigwedge }(x^{\prime }=x)$，分支运算为 $F+G=F\vee G$，连接运算为 $F\cdot G=\mathrm{\exists }{X}^{″}.F(X,X^{″})\wedge G(X^{″},X^{\prime })$（即用 $X^{″}$ 来表示中间状态）。 而对于循环运算 $(-{)}^{\ast }:\mathit{TransitionFormula}\to \mathit{TransitionFormula}$，我们只需考虑在转移公式这一层面进行计算，并不用考虑循环语句本身可能有的嵌套循环结构！ 换句话说，我们可以借鉴已有的各种 Loop Summarization / Acceleration 技术。

在这里，我们只讨论一种基于区间分析的循环运算实现方法（本文开头提到的参考材料中有更多的例子）。 在区间分析中，我们一般考虑形如 $\underset{x\in X}{\bigwedge }(a_x\le x\le b_x)$ 的状态公式，其中 $a_x,b_x$ 为常数。 例如，对于下面这个程序中的循环而言，$0\le i\le 10\wedge 0\le j\le 20$ 是一个区间不变量，但是 $0\le i\le 10\wedge 0\le j\le 10$ 并不是：

i = 0;
j = 0;
while (i < 10 && j != 20 && j < 100) {
  i = i + 1;
  j = j + 1;
}

传统的基于区间的程序分析会使用 widening / narrowing 等技术来确保迭代分析可以收敛，但这会影响分析的精度。 在代数程序分析的框架中，我们则拥有更好的自由度来设计对于循环的分析：考虑循环体的转移公式为 $F(X,X^{\prime })$，那么断言“$A=\{a_x\mid x\in X\}$ 和 $B=\{b_x\mid x\in X\}$构成一个区间不变量”可以表述为下面的公式： $$\mathrm{\forall }X,X^{\prime }.((\underset{x\in X}{\bigwedge }(a_x\le x\le b_x))\wedge F(X,X^{\prime }))⟹\underset{x\in X}{\bigwedge }(a_x\le x^{\prime }\le b_x)$$ 令 $Inv(A,B)$ 为上面这个式子。那么循环运算 $F^{\ast }$ 可以定义为： $$\mathrm{\forall }A,B.(Inv(A,B)\wedge \underset{x\in X}{\bigwedge }(a_x\le x\le b_x))⟹\underset{x\in X}{\bigwedge }(a_x\le x^{\prime }\le b_x)$$ 这种循环运算的实现蕴含了所有可以由循环体转移公式 $F$ 得出的区间不变量！

前面我们提到，代数程序分析要求在程序语法树上进行结构递归，那么在非结构的程序上（例如有 break 和 continue），我们是否还能进行代数程序分析呢？ 答案再次由 Robert Tarjan 给出：Yes！（至于为什么用“再”可以看我上次的分享。) Tarjan 的两篇文章 Fast Algorithms for Solving Path Problems 和 A Unified Approach to Path Problems 中提出了一种高效的基于代数的在图上解决路径问题的算法：这里的路径问题指的是图中的边上有权值，一条路径的权值为其中边权相乘，然后我们想要计算符合某种条件的所有路径的权值和（这里的乘和和都是抽象的，例如如果权值为非负数，乘为加，和为取最小值，那么路径问题描述的则是最短路问题）。 Tarjan 提出了一种可以计算图上两点间所有路径的集合的高效算法，其关键点在于这个（可能无穷的）路径集合可以表述为一个有限的正则表达式，其后解路径问题就可以转化为在一个描述问题的代数结构中解释正则表达式：这与我们上文描述的三种运算（连接 $\cdot$，分支 $+$，循环 ${}^{\ast }$）正好是符合的！ 所以，对于非结构的程序，我们可以把它表示成一个控制流图，然后通过 Tarjan 的算法计算出描述所有可能的程序执行路径的正则表达式，最后在描述程序分析的代数结构中解释该正则表达式。 例如，以下程序

while (true) {
  m = 0;
  while (m < 8) {
    if (n < 0) {
      return;
    } else {
      m = m + 1;
      n = n - 1;
    }
  }
}

中的所有可能路径的集合可以表述为下面的正则表达式： $${(\boxed{\text{m=0}}\cdot {(\boxed{\text{m<8}}\cdot \boxed{\text{n>=0}}\cdot \boxed{\text{m=m+1}}\cdot \boxed{\text{n=n-1}})}^{\ast }\cdot \boxed{\text{m>=8}})}^{\ast }\cdot \boxed{\text{m=0}}\cdot \boxed{\text{m<8}}\cdot \boxed{\text{n<0}}$$

在文章的最后，我们聊一聊代数程序分析的不足。 最明显的不足在于，尽管 Compositionality 是个好性质，它也意味着我们在程序分析中丢失了上下文信息。 一方面，由于在分析某个程序组成部分时不能依赖其上下文，我们在分析时需要追踪更多的信息（例如上文的状态转移公式代数需要同时记录 $X$ 和 $X^{\prime }$）；另一方面，我们可能会由于缺乏上下文信息而对某个程序组成部分进行过于保守的分析（这取决于程序分析状态空间设计得好不好）。