updated: 2026-04-05

静态分析基础知识

概念

SSA

静态单赋值形式（static single assignment form），即每个变量仅被赋值一次，对于下面的情形：

x <- 1
x <- x + 2

可以看到x被赋值了两次，将其转换为SSA时，只需要将第二行中被赋值的x视为x的另一个版本，将其加上版本号即可，即

x_1 <- 1
x_2 <- x_1 + 2

但这又引起了一个问题：当两个版本的同一变量的其中一个可能在后续代码中被使用时，如何决定使用哪个，如：

    x_1 <- 1
    x_2 <- x_1 + 2
    if y < 3 goto L1
    x_3 <- x_1 - 2
L1:
    z <- x_?

在这里，z有可能取x_3，也有可能取x_2，这时为了加以说明，我们使用一个称为Φ函数的函数，它起到这样的作用：

    x_1 <- 1
    x_2 <- x_1 + 2
    if y < 3 goto L1
    x_3 <- x_1 - 2
L1:
    x_4 <- Φ(x_2, x_3)
    z <- x_4

在这里，Φ函数产生了一个新版本的x，这个版本的x的值由程序运行的路径动态决定。

Rice's Theorem

递归可枚举语言的所有非平凡性质都是不可判定的。

递归可枚举：乔姆斯基层级中的0-型语言，基本包含了目前现行的所有计算机语言
非平凡性质：仅被部分递归可枚举语言所具有的性质
不可判定：一般意义上，可以指不存在相应的算法来对问题给出真或假的结论

program point

program point可以视为一个抽象点，比如我们认为每一个basic block的前后有一个program point，这个点仅仅具有形式的意义，可以为这个点附加状态（如在basic block $B$ 前的一个program point $s$ 处，某变量 $a$ 有定义，“ $a$ 有定义”就是我们对这个program point附加的状态）

Must Analysis VS May Analysis

从分析的目的来看待这两个概念比较容易理解

当我们想要分析所有情况（如考虑到所有的控制流路径对一个program point带来的影响）时，我们常常在算法中进行过近似（over approximation），这时我们在做的分析称作may analysis，可以理解为求并。

当我们认为只要有一种情况无效，那么整体结论就无效（如下面提到的available expression analysis）时，我们在算法中进行欠近似（under approximation），这时我们做的分析称为must analysis，可以理解为求交。

Data Flow Analysis

这里我们先给出三个经典的data-flow analysis及其datalog实现，然后再来分析这些算法背后的数学基础。

Reaching Definition Analysis

本节中我们使用下面的例子来进行分析：

问题分析

目的：对每一个变量，确定它的哪些赋值有可能通过某一个控制流路径到达过程内的任意一个特定点。

例如上面的例子，首先对问题进行建模：

对每一个赋值语句，我们给它一个编号 $Di$
将每个基本块的第一条语句前和最后一条语句后视为一个program point
每个基本块 $B$ 对应一组状态 $out[B]$ 以及 $in[B]$ ，用于表示 $B$ 之前的program point和 $B$ 之后的program point的状态
对每一个基本块 $B$ ，有事实（facts） $gen_B$ 以及 $kill_B$ 。对于 $B$ 中的每一条赋值语句，将其放入 $gen_B$ ，并将所有被赋值变量与该语句相同的语句放入 $kill_B$ ，

最终我们得到下面的式子：

out[B] = gen_B \cup (in[B] - kill_B)

同时我们也指出块之间的状态传递方式，对于一个块 $B$ ，假设它有一个或者多个前驱块，我们有：

in[B] = \Cup_{S\ is\ precursor\ of\ B}\ out[S]

使用Datalog解决问题

datalog现在我们可以使用datalog来对问题进行求解，对于本问题，我们得到三个要素：

facts：
- Kill(m, n): m is basic block, n is definition. n is killed after block m
- Gen(m, n): m is basic block, n is definition. n is defined in block m
- Next(m, n): m, n are both basic blocks. m is the precursor of n
outputs:
- Out(m, n): n is in $out[m]$
- In(m, n): n is in $in[m]$
rules:
- Out(m, n) <- Gen(m, n) // Gen中的所有定义将会进入Out
- Out(m, n) <- In(m, n), !Kill(m, n) // 在In中且不在Kill中的定义进入Out
- In(m, n) <- Out(p, n), Next(p, m) // p为m的前驱块，则p的Out进入m的In

有了这些内容，我们便可以针对上面的问题给出对应的datalog代码，参见https://xxx/StaticAnalysis/blob/master/src/reaching_definition.rs

使用迭代算法

reaching-definition问题的本质是求取状态（program point处的definition状态）在转移函数（我们定义的 $in[B]$ 与 $out[B]$ 间的关系）下的不动点（fixpoint），因此可以使用通用的迭代算法来对问题进行求解，基本思路是将所有 $out[..]$ 设置为空，然后对每一个基本块进行遍历，每次遍历都对当前块 $B$ 根据我们的 $kill_B$ ， $gen_B$ 以及 $in[B]$ 之间的关系计算出新的 $out[B]$ ，最终每个基本块的 $out$ 在遍历一遍之后不发生变化时，算法结束。

该算法必然停机的依据在于，每次遍历如果更新 $out$ ，则它的大小必然增大（个人理解：每一个 $out$ 的单调性与对应的 $in$ 相同，而最初的 $in$ 来自entry block，它是不减的，因此所有的 $in$ 与 $out$ 都是不减的，因此 $out$ 发生变化时一定是增大的），加之整个程序中的definition的数目是有限的，因此通过上述方法来确定算法的终止是可以实现的。

进一步的，当上述“每个基本块的 $out$ 在遍历一遍之后不发生变化”的情况发生时，即使再运行算法，所有program points的状态也不会发生改变，因此这个算法是安全的（老师说的，存疑）。

Live Variables Analysis

本节中使用下面的程序作为例子：

问题分析

目的：对于一个变量 $a$ ，和一个program point $p$ ，假设 $a$ 在 $p$ 处有定义，本算法要求给出是否存在一条以 $p$ 为起始的控制流路径，使得 $a$ 在该路径上的某一点被使用。

现在对问题进行建模：

首先我们需要的信息可以使用一个布尔值给出，真代表变量将会被使用，即live，假代表不再使用，即dead
我们分析的对象是一个程序中的所有变量，因此每个progrom point处的状态是一个位向量，每一位对应相应变量在此处的liveness
对于一个基本块 $B$ 有fact $kill_B$ ，假设变量 $a$ 在B中被重定义，即被kill掉，那么 $a \in kill_B$
对于一个基本块 $B$ 有fact $use_B$ ，若变量 $a$ 在B中被使用（如果有kill，则要求在kill之前使用），那么 $a \in use_B$
对于每个基本块 $B$ 有 $in[B]$ 和 $out[B]$ ，分别表示该块之前和之后的program point的状态

最终我们显然有：

in[B] = use_B \cup (out[B] - kill_B)

从这个式子我们可以看出，本问题更适合演着控制流的逆向分析，根据 $out$ 来计算对应的 $in$ .

同时我们也指出块之间的状态传递方式，对于一个块B，假设它有一个或者多个后继（注意我们是backward的分析）块，我们有：

out[B] = \Cup_{S\ is\ successor\ of\ B}\ in[S]

使用Datalog解决问题

对于本问题，我们同样可以得到三个要素：

facts:
- Use(m, n) variable n is used in block m
- Kill(m, n) variable n is killed in block m
- Next(m, n) block n is the successor of m
outputs:
- In(m, n) variable n is live at program point $in[m]$
- Out(m, n) variable n is live at program point $out[m]$
rules:
- In(m, n) <- Use(m, n)
- In(m, n) <- Out(m, n), !Kill(m, n)
- Out(m, n) <- In(d, n), Next(m, d)

代码地址：https://xxx/StaticAnalysis/blob/master/src/live_variables.rs

Available Expression Analysis

以下面的程序为例

问题分析

我们称一个expression $e$ 在一个program point $p$ 处是available的当且仅当

从CFG的entry block到 $p$ 之间在每一条控制流路径上 $e$ 都被计算
在每一条控制流路径上，从 $e$ 被计算的点到 $p$ 之间 $e$ 中使用的变量都没有被重新赋值

从定义中我们可以看到，这是个must analysis，通过计算 $e$ 在 $p$ 处是否是available的，我们可以进行如子表达式替换等操作。

接下来对问题进行建模：

对于每一个表达式，有编号 $E_i$
对于每一个基本块 $B$ 有 $gen_B$ ，若计算了 $E_i$ 且后续没有重新定义 $E_i$ 中的变量，则 $E_i \in gen_B$
对于每一个基本块有 $kill_B$ ，某语句重新定义了 $E_i$ 中的一个变量，则 $E_i \in kill_B$
对于一个基本块有 $in_B$ ，代表在 $B$ 前的program point处available的 $E$ 的集合
对于一个基本块有 $out_B$ ，代表在 $B$ 后的program point处available的 $E$ 的集合

那么我们有如下关系：

out[B] = gen_B \cup (in[B] - kill_B)

同时由于这个分析是一个must analysis，我们需要使用交来处理控制流的merge

in[B] = \Cap_{S\ is\ precursor\ of\ B}out[S]

使用Datalog解决问题

datalog现在我们可以使用datalog来对问题进行求解，对于本问题，我们得到三个要素：

facts：
- Kill(m, n): m is basic block, n is expression. n is killed after block m
- Gen(m, n): m is basic block, n is expression. n is defined in block m
- Next(m, n): m, n are both basic blocks. m is the precursor of n
outputs:
- Out(m, n): n is in $out[m]$
- In(m, n): n is in $in[m]$
rules（暂时能用，感觉还可以再优化）:
- Out(m, n) <- Gen(m, n) // Gen中的所有定义将会进入Out
- Out(m, n) <- In(m, n), !Kill(m, n) // 在In中且不在Kill中的定义进入Out
- MultiPre(n) <- Next(p, n), Next(q, n), (p != q); // 基本块 $n$ 有多个前驱块
- Intersection(n, m, b) <- Out(m, b), Out(n, b); // $b \in out[m] \cap out[n]$
- $in[B] = \cap_{S\ is\ precursor\ of\ B}out[S]$
```
In(n, d) <- Next(m, n), Next(p, n), Intersection(m, p, d), (m != p);
In(n, d) <- Next(m, n), !MultiPre(n), Out(m, d);    
```

代码在这里：https://xxx/StaticAnalysis/blob/master/src/available_expression.rs

迭代算法

对于本问题，迭代算法的伪代码如下：

Foundation

本节首先给出Data flow Analysis的数学基础以及求解的一般方法。

基本概念

定义1：定义在集合 $U$ 上的关系 $(U, \sqsubseteq)$ 是一个偏序关系当且仅当该关系满足自反性，反对称性与传递性*（注意这并不要求任意两个元素之间存在关系）*

定义2：对于定义在集合 $U$ 上的关系 $(U, \sqsubseteq)$ ，假设集合 $S \subseteq U$ ，有 $a \in U$ 使得 $\forall x \in S, x \sqsubseteq a$ ，那么称 $a$ 为集合 $S$ 的一个上界，记为；同样的，有 $a \in U$ 使得 $\forall x \in S, a \sqsubseteq x$ ，那么称 $a$ 为集合 $S$ 的一个下界。

定义3：对于定义在集合 $U$ 上的关系 $(U, \sqsubseteq)$ ，假设集合 $S \subseteq U$ ，有 $a \in U$ 使得

\forall x \in S: (\forall b \in U: ((x \sqsubseteq a, x \sqsubseteq b) \Rightarrow b \sqsubseteq a))

那么称 $a$ 为集合 $S$ 的一个上确界，记为 $\sqcup S$ ，特别的，当 $S$ 仅包含 $x$ ， $y$ 两个元素时，可以记为 $x \sqcup y$ ；

同样的，有 $a \in U$ 使得

\forall x \in S: (\forall a \in U: ((a \sqsubseteq x, b \sqsubseteq x) \Rightarrow a \sqsubseteq b))

那么称 $b$ 为集合 $S$ 的一个下确界，记为 $\sqcap S$ ，特别的，当 $S$ 仅包含 $x$ ， $y$ 两个元素时，可以记为 $x \sqcap y$ 。

定义4：对于定义在集合 $U$ 上的关系 $(U, \sqsubseteq)$ ，若

\forall a, b \in U: (\exists m, n: (m = a \sqcup b \wedge n = a \sqcap b))

则称 $(U, \sqsubseteq)$ 为一个格（lattice）

定义5：对于定义在集合 $U$ 上的关系 $(U, \sqsubseteq)$ ，若

\forall S \subseteq U: (\exists x, y: (x = \sqcap S \wedge y = \sqcap S))

则称 $(U, \sqsubseteq)$ 为一个全格（complete lattice）（这里可以理解为在半格的基础上添加了一个“一定具有全局的上/下确界”的限定，如正整数集上的 $\le$ 关系是一个格，但由于不存在上确界（ $\infty$ 未定义），因此它不是一个全格，但稍后我们可以看到，由于具有下确界0，它是一个半格）。但注意并非全格一定是有限的，如 $([0, 1], \le)$ 是一个全格，但定义在一个无限的集合上。

同时注意我们之后会比较关注全格中的两个特殊的元素，即 $\sqcap U$ 以及 $\sqcup U$ ，我们将其分别记为 $\bot$ 和 $\top$ 。

定义6：在理解了全格的概念之后，半格的概念也很容易理解，即对于定义在集合 $U$ 上的关系 $(U, \sqsubseteq)$ ：

\forall S \subseteq U: (\exists x: x = \sqcap S)

或者

\forall S \subseteq U: (\exists x: x = \sqcup S)

那么称 $(U, \sqsubseteq)$ 是一个半格。可以看到，半格要么只有 $\top$ ，要么只有 $\bot$

定义7：对一个格 $L$ ，有函数 $F: L \rightarrow L$ ，假如有 $X$ 使得 $X = F(X)$ ，那么称X是函数F的一个不动点。

例如定义格 $L$ 为 $(\{x|0 \le x \le 1\}, \le)$ ，有函数 $f(x) = 2x - \frac{1}{2}$ ，那么 $x = \frac{1}{2}$ 即为 $f$ 的一个不动点。

定义8：对于一个格 $L$ ，有函数 $F: L \rightarrow L$ ，若 $\forall x_1, x_2: (x_1 \sqsubseteq x_2 \Leftrightarrow F(x_1) \sqsubseteq F(x_2))$ ，则称 $F$ 为 $L$ 上的一个单调函数（monotonic function）。

定义9：假设有格 $L_1, L_2, L_3, ..., L_n$ ，我们定义

L = L_1 \times L_2 \times L_3 \times ... \times L_n

其中有：

$U = U_1 \times U_2 \times U_3 \times ... \times U_n$
$(x_1, x_2, x_3, ..., x_n) \sqsubseteq (y_1, y_2, y_3, ..., y_n) \Leftrightarrow (x_1 \sqsubseteq y_1) \land (x_2 \sqsubseteq y_2) \land (x_3 \sqsubseteq y_3) \land ... \land (x_n \sqsubseteq y_n)$
$(x_1, x_2, x_3, ..., x_n) \sqcap (y_1, y_2, y_3, ..., y_n) = (x_1 \sqcap y_1, x_2 \sqcap y_2, x_3 \sqcap y_3, ..., x_n \sqcap y_n)$
$(x_1, x_2, x_3, ..., x_n) \sqcup (y_1, y_2, y_3, ..., y_n) = (x_1 \sqcup y_1, x_2 \sqcup y_2, x_3 \sqcup y_3, ..., x_n \sqcup y_n)$

那么 $L$ 称为 $L_1, L_2, L_3, ..., L_n$ 的积，易知 $L$ 也是一个格。

关于不动点

我们的下面我们给出几个关于单调函数与不动点的定理：

定理1：对于一个定义在全格 $L: (U, \sqsubseteq)$ 上的单调函数 $F: L \rightarrow L$ ，若 $U$ 是有限的，则有 $\exists x: F(x) = x$

证明：由 $F$ 以及 $\bot$ 的定义，我们有：

\bot \sqsubseteq F(\bot)

可以得到：

\bot \sqsubseteq F(\bot) \sqsubseteq F(F(\bot)) = F^2(\bot)

重复应用该条结论，我们可以得到：

\bot \sqsubseteq F(\bot) \sqsubseteq F^2(\bot) ... \sqsubseteq F^n(\bot)

由于L是有限的，因此我们有

\exists k: F^{k-1}(\bot) = F^k(\bot) = F_{fix}

此时有 $F_{fix} = F(F_{fix})$ ，因此 $F_{fix}$ 是 $F$ 的一个不动点。

注：该证明不够严谨，更完整的证明参见Knaster–Tarski_theorem

现在我们证明了单调函数在全格上不动点的存在性，下面我们要给出一个算法来求解该不动点：

推论1：若 $F: L \rightarrow L$ 是 $L$ 上的一个单调函数，那么迭代的应用

F(\bot), F^2(\bot), F^3(\bot), ..., F^n(\bot)

直到有一点 $K$ 使得

F^{k-1}(\bot) = F^k(\bot) = F_{fix}

这时我们就得到了F的一个不动点。该算法也被称为迭代算法，到后面我们将会看到，它也是Datalog求解中的naive evaluation算法的基础。

同样的，从 $\top$ 出发，我们也能得到一个不动点，下面我们将看到这两个不动点之间的区别。

定理2：利用推论2中算法找到的不动点一定是最小不动点

证明：若存在一个不动点 $F_{lt} \sqsubseteq F_{fix}$ ，那么有 $F(F_{lt}) = F_{lt}$

又由单调性可得：

\bot \sqsubseteq F_{lt} \Leftrightarrow F(\bot) \sqsubseteq F(F_{lt})

又有：

F^2(\bot) \sqsubseteq F^2(F_{lt})

根据单调性，我们有：

F^{n - 1}(\bot) \sqsubseteq F^{n-1}(F_{lt}) \Leftrightarrow F^n(\bot) \sqsubseteq F^n(F_{lt})

应用数学归纳法以及定理1，我们得到：

\exists k: F_{fix} = F^{k-1}(\bot) = F^k(\bot) \sqsubseteq F^k(F_{lt}) = F_{lt}

由反对称性，得：

(F_{fix} \sqsubseteq F_{lt} \land F_{lt} \sqsubseteq F_{fix}) \Leftrightarrow F_{fix} = F_{lt}

与条件相悖，故找到的不动点一定是最小不动点

同理，如果我们从 $\top$ 开始迭代，得到的不动点一定是最大不动点。

数据流分析与格

下面我们以live variables分析为例，解析如何将上面的数学知识应用到数据流分析的设计中，回忆之前使用的CFG。

显然，每个program point都是一个格，该格的定义为 $(\{x, y, z, p, q, m, k\}, \subseteq)$ ，且有 $\sqcap \Leftrightarrow \cap$ ， $\sqcup \Leftrightarrow \cup$ 。

方便起见，假设变量只有 $x, y, z$ 三个，每个program point处对应的格可以用下图表示：

假设对于每一个基本块 $B$ 的 $out[B]$ （不使用 $in[B]$ 是因为我们后面的证明中，把 $in[B]$ 当作是一个中间变量，而且实际上也只有 $out[B]$ 对于我们的分析是有意义的），我们有一个对应的格 $L_i$ ，那么一个程序中所有的program point的积 $L = L_1 \times L_2 \times ... \times L_n$ 也是一个格，同时我们有一个定义在这个格上的函数 $F: L \rightarrow L$ ，以reaching definition analysis为例，该函数的定义有以下两部分构成：

\displaylines{in[B] = \Cup_{S\ is\ precurser\ of\ B}out[S] \\ out[B]=gen_B \cup (in[B] - kill_B)}

该函数的第一部分可以看作一个格上的 $\sqcup$ 操作，它用来处理控制流引起的基本块的汇聚；第二部分是一个per block的转移函数 $f_i$ ，它将状态 $in[B]$ 转移到 $out[B]$ 。

当我们使用迭代算法进行求解时，我们的每一次遍历都相当于在格 $L$ 上应用了函数 $F$ 。这时为了证明在这个问题上，我们的迭代算法一定可以找到一个解，我们首先需要证明函数 $F$ 的单调性.

证明 $F$ 在 $L = (U, \sqsubseteq)$ 上单调，即证:

\forall x, y \in U: x \sqsubseteq y \Leftrightarrow F(x) \sqsubseteq F(y)

我们将 $x$ 与 $y$ 拆解为对应的分量 $(x_1, x_2, ..., x_n)$ 以及 $(y_1, y_2, ..., y_n)$ ，这些分量代表每一个基本块的 $out[B]$ ，根据格之积的定义，我们有：

\forall x, y \in U: (x_1 \sqsubseteq y_1) \land (x_2 \sqsubseteq y_2) \land ... \land (x_n \sqsubseteq y_n) \Leftrightarrow F(x) \sqsubseteq F(y)

因此我们只需证明每一个 $out[B]$ 单调，即可证明 $F$ 单调，

显然，转移函数 $f_i$ 是单调的，我们只需证明格上的 $\sqcup$ 运算单调，即证明：

\forall x, y, z\in U: x \sqsubseteq y \Leftrightarrow x \sqcup z \sqsubseteq y \sqcup z

由 $\sqcup$ 的定义可知：

y \sqsubseteq y \sqcup z, \ z \sqsubseteq y \sqcup z

由传递性，得：

x \sqsubseteq y \land y \sqcup z \Rightarrow x \sqsubseteq y \sqcup z

因此 $y \sqcup z$ 是 $\{x, z\}$ 的一个上界。由上确界的定义得：

x \sqcup z \sqsubseteq y \sqcup z

因此格上的 $\sqcup$ 运算单调。

综上所述， $F$ 单调。

经过上述证明，只要我们为data flow analysis设计了良好的transfer function（满足单调性），我们可以得到如下结论：

通过迭代算法进行的求解一定能得到一个解（算法必然停机）
对于may analysis而言，初始状态是格的 $\bot$ ，算法必然找到一个最小不动点；对于must analysis而言，初始状态是格的 $\top$ ，算法必然找到一个最大不动点。

接下来，为了衡量迭代算法求出的解，我们考虑从格的角度再对may analysis以及must analysis进行分析：

再探Must Analysis与May Analysis

首先我们需要明确data flow analysis的目的，确定我们的分析结果是否是safe的，其中safe与unsafe的定义如下：

当我们根据data flow analysis的结果进行相应的操作，操作会带来错误的结果时，我们称分析结果是unsafe的，比如available expression分析中错误的指出某一个expression是available的，这可能会导致后续的优化出现错误，进而导致程序运行时出现非预期的结果。
当出现多余的操作，或者是需要进行优化的位置没有得到优化，但不会造成程序的非预期行为时，我们称结果是safe的。比如在live variables分析中指出所有的variabe都将被使用，这当然是正确的，但是会导致后续的操作变得困难（如寄存器分配难以进行）

需要注意的是，我们通过data flow analysis想要达到的目的是找到一个safe与unsafe的分界点，即truth的位置，这时我们尽可能为后续的优化提供丰富的信息，同时也避免提供错误的结果，因此我们可以通过衡量算法给出的结果与这个值的接近程度来确定算法的准确性。

下图给出了may analysis与must analysis的关系：

首先需要明确，算法中的转移函数 $F$ 是认为构造的，因此它到达一个不动点时，我们认为一个正确的算法一定是safe的，我们需要衡量的便是在safe的范围内，找到的不动点是否接近unsafe。我们之所以认为迭代算法给出的是最优解，是因为格的性质决定了它一定取得的是最大/最小不动点，这个不动点是 $F$ 的所有不动点中最接近truth的那一个。

另一种方法：MOP

MOP是Meet-Over-All-Paths solution，与上面提到的分为两部分的转移函数的设计不同的是，MOP的方法是将每个block的转移函数应用到每个前驱块的结果上，然后再进行 $\sqcup$ 操作，简要来说，我们之前使用的方法是 $f_i(x \sqcup y)$ ，而MOP使用的方法是 $f_i(x) \sqcup f_i(y)$ 。这种方法考虑到了CFG中的所有path，因此它的准确性高于我们的方法，但是该方法的时间和空间代价过于高昂，而且由于考虑了比实际更多的路径，该算法仍然不是一个完全准确的方法。

特别的，当我们选择的转移函数可分配时，我们的方案与MOP的转确性相同。

// TODO 添加形式化的证明

Constant Propagation Analysis

常量传播是一项非常重要的优化，首先根据上面提到的格的知识来为该问题进行建模：

该问题是一个forward analysis
定义一个包含变量所有可能取值的集合 $A = \{\top, \bot, false, true, 0, -1, 1, 2, .....\}$
每一个变量对应一个格 $V_i = (A, \sqcup)$ ，该变量可以被表示为 $(varname, x), x \in A_i$ ，这个格称为ICP，具有以下性质：
- $\forall n \in ICP: n \sqcup \top = \top$
- $\forall n \in ICP: n \sqcap \bot = \bot$
- $\forall m, n \in ICP: m \ne n \Rightarrow m \sqcup n = \top \land m \sqcap n = \cup$
- $\forall n \in ICP: n = n \sqcup n = n \sqcap n$
每一条语句前后都有一个program point，此处的状态 $P_i$ 由所有变量对应格的积组成
每一个block $B$ 的状态 $out[B], in[B]$ 作为特定语句前后状态的别名
程序的状态由每一个program point的状态的积组成

特别的，对于block $B$ 的状态 $out[B], in[B]$ 有：

in[B] = \sqcup_{S\ is\ precurser\ of\ B}out[S]

对于一条赋值语句，我们首先求出右侧的表达式的值（注意这个过程可能会用到之前已经经过求值的变量），然后找到语句前的program point处被赋值变量的值，然后将该值更新为新旧两值的 $\sqcup$ 。

∧