想象一名分析器沿着控制流图巡查程序。走过赋值语句，它更新变量信息；来到分支，它复制状态分别前进；遇到汇合点，它把两条路径的发现合在一起。最麻烦的是循环：新的信息会沿回边送回旧节点，迫使分析器重新检查已经看过的代码。
如果这种巡查没有明确规则，分析器要么漏掉路径，要么永远绕着循环打转。真正让它运转起来的，是三个彼此衔接的部件：transfer function 负责处理一条指令，join 负责合并多条路径，fixed point 则说明整张图何时已经稳定。
上一篇介绍了抽象状态与 lattice。本文继续回答一个更接近实现的问题：怎样把局部的抽象规则变成一个能够在 CFG 上运行并停止的算法。推导会先从单个节点的输入、输出状态开始，再把 transfer function 与 join 连接成全图方程，随后通过循环解释不动点，最后落到一个可执行的 worklist algorithm。
一、Transfer Function：一条指令改变了什么？
具体执行中，一条指令把状态 $\sigma$ 变成新状态 $\sigma’$。抽象分析不保存全部具体值，而是在抽象状态空间 $\hat{\Sigma}$ 上做类似的转换。对于 CFG 节点 $\ell$，通常写成：
\[F_\ell:\hat{\Sigma}\rightarrow\hat{\Sigma}.\]$F_\ell$ 就是节点 $\ell$ 的 transfer function（传递函数）。它接收节点执行前的抽象状态，返回执行后的抽象状态：
\[\hat{\sigma}_{out} = F_\ell(\hat{\sigma}_{in}).\]例如，常量传播只关心变量是否拥有一个确定常量。可以使用下面的抽象值域：
\[\hat{V}=\{\bot\}\cup\mathbb{Z}\cup\{\top\}.\]这里，$\bot$ 表示节点当前不可达，整数 $c$ 表示“确定等于 $c$”，$\top$ 表示“可能取不同的值”。执行 x = 1 后，无论 x 原来是什么，传递函数都会把它更新为常量 1：
这与第一篇介绍的状态更新形式相同，只是其中保存的已经是抽象值。
赋值、条件判断和函数调用对状态的影响并不相同。常量传播中的几条典型规则可以直观地写成：
1
2
3
4
x = 1 将 x 更新为 1
x = y 将 y 的抽象值复制给 x
x = y + z 根据 y、z 的抽象值计算 x；无法确定时得到 ⊤
assume(c) 保留满足条件 c 的状态，并丢弃不可能的状态
论文的创新经常就藏在这些规则里。阅读 transfer function 时，先找它的输入和输出，再看它保留、丢弃或新引入了哪些信息，通常比从公式内部逐字符阅读更有效。
Transfer function 回答的是局部问题：执行当前节点后，抽象状态怎样变化？
二、从局部规则到 CFG 方程
设控制流图为 $G=(N,E)$。对于每个节点 $n\in N$，分析器通常维护两份状态：
- $IN[n]$：进入节点前的抽象状态；
- $OUT[n]$：执行节点后的抽象状态。
它们由节点的 transfer function 连接：
\[OUT[n]=F_n(IN[n]).\]如果节点只有一个前驱，输入状态可以直接来自该前驱的输出。若节点有多个前驱，就必须先合并所有到达这里的状态。记 $pred(n)$ 为 $n$ 的前驱集合，则：
\[IN[n] = \bigsqcup_{p\in pred(n)}OUT[p].\]这两条方程放在一起，就是许多前向数据流分析的骨架：
\[\boxed{ IN[n]=\bigsqcup_{p\in pred(n)}OUT[p], \qquad OUT[n]=F_n(IN[n]) }\]入口节点需要单独给定初始状态；其他尚不可达的节点通常从 $\bot$ 开始。
这组方程中，join 合并的是不同前驱带来的可能性。考虑下面的程序：
1
2
3
4
5
6
7
if (flag) {
x = 1;
} else {
x = 2;
}
use(x);
两条分支分别产生 $x\mapsto1$ 和 $x\mapsto2$。到达 use(x) 之前，分析器计算：
因此，汇合后的状态是 $x\mapsto\top$。它不再能说出 x 的确切值，却仍然覆盖了两条真实路径。如果两个分支都得到 1，则有：
Join 不是随意“取一个较大的结果”，而是寻找能够同时代表各条路径、同时又尽量精确的最小上界。
在本系列采用的顺序中，状态越靠上覆盖的具体行为越多，也越不精确。Join 扩大可能性，但不能遗漏任何输入路径。
三、循环为什么变成不动点问题？
顺序代码只需向前传播一次；循环却会让后面的输出重新成为前面的输入：
1
2
3
4
5
x = 0;
while (unknown()) {
x = x + 1;
}
第一次到达循环头时，常量传播得到 $x=0$。执行一次循环体后，回边带来 $x=1$；两者合并后得到 $\top$。再执行一次，输入与输出都不再变化。传播过程可以写成：
\[\bot \sqsubseteq 0 \sqsubseteq \top.\]这是一条不断上升的抽象状态序列。只要某次重新计算后所有节点状态都保持不变，继续传播也不会产生新信息。
把整张 CFG 上所有节点的状态看成一个向量，并把“一轮传播”记为全局函数 $F$。如果：
\[F(S)=S,\]那么 $S$ 就是 $F$ 的 fixed point（不动点）。静态分析通常寻找满足方程的 least fixed point（最小不动点）：它既满足所有传播约束，又在既定抽象域中尽量精确。
从 $\bot$ 开始反复应用单调函数，可以得到：
\[S_0=\bot, \qquad S_{i+1}=F(S_i).\]当 $S_{i+1}=S_i$ 时，分析达到稳定。有限高度的抽象域不会产生无限严格上升链，因此这一迭代会在有限步内结束；无限高度的区间域则可能不断得到 $[0,0]、[0,1]、[0,2]\ldots$，需要下一篇介绍的 widening 来加速收敛。
四、Worklist Algorithm：只重算受影响的节点
最直接的实现可以一遍遍扫描全部 CFG 节点，直到没有状态变化。但大型程序的大多数节点在一次局部更新后都不受影响，重复计算它们既慢又没有必要。
Worklist algorithm（工作列表算法）只保存当前需要重新处理的节点。一个基本的前向版本如下：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
for each node n:
IN[n] = ⊥
OUT[n] = ⊥
IN[entry] = initial_state
worklist = [entry]
while worklist is not empty:
n = remove(worklist)
new_out = F_n(IN[n])
if new_out != OUT[n]:
OUT[n] = new_out
for each successor s of n:
new_in = IN[s] ⊔ OUT[n]
if new_in != IN[s]:
IN[s] = new_in
add s to worklist
这里有两个变化检查。节点输出没有变化时，后继节点不需要重算；后继输入没有变化时，它也不需要重新进入 worklist。不同实现会改变节点选择顺序或一次合并的方式，但核心原则相同：只有新信息出现时，才继续传播。
当 worklist 为空时，没有节点的输入或输出还能被更新，因此所有局部方程同时成立，分析到达了全局不动点。
终止性还依赖几个前提：transfer function 通常需要保持单调，join 不能让状态向下倒退，抽象域则需要阻止无限上升过程。对于有限高度域，最后一点自然满足；对于无限高度域，需要 widening 等额外机制。
五、把整套分析走一遍
现在可以把前四篇的概念接成一条完整流水线：
1
2
3
4
5
6
7
8
9
10
11
12
13
源代码
↓
控制流图 CFG
↓
抽象域与初始状态
↓
节点 Transfer Function
↓
Join + Worklist
↓
Least Fixed Point
↓
分析结果
其中，CFG 决定信息沿哪些边传播，抽象域决定分析器记住什么，transfer function 决定节点怎样更新状态，join 决定路径怎样汇合，worklist 则负责高效求解这些方程。
面对一套新的静态分析定义，可以依次寻找：
- 状态：$\hat{\sigma}$ 保存哪些抽象信息？
- 局部规则：$F_n$ 怎样处理每类语句？
- 合并：多个前驱通过什么 join 合在一起？
- 收敛：循环如何达到 fixed point，是否使用 widening？
这四个问题分别对应数据结构、局部语义、控制流汇合与全局求解。即使论文更换了符号，也很难绕开这套结构。
这些对象及其关系可以用下面的符号表回查：
| 符号 | 常见含义 |
|---|---|
| $F_n$ | 节点 $n$ 的 transfer function |
| $IN[n]$ | 进入节点 $n$ 前的抽象状态 |
| $OUT[n]$ | 执行节点 $n$ 后的抽象状态 |
| $pred(n)$ | 节点 $n$ 的前驱集合 |
| $\sqcup$、$\bigsqcup$ | 合并两个或多个抽象状态 |
| $lfp(F)$ | 全局分析函数 $F$ 的最小不动点 |
| worklist | 等待重新处理的节点集合或队列 |
六、本篇小结
这一篇把“抽象状态”变成了一个真正会运行的分析过程。Transfer function 处理当前节点，join 汇集前驱信息，回边促使节点重新计算，worklist 则持续传播变化，直到所有状态共同达到 least fixed point。
需要记住的核心方程只有两条：
\[IN[n]=\bigsqcup_{p\in pred(n)}OUT[p], \qquad OUT[n]=F_n(IN[n]).\]下一篇 准确、快速，还是可靠？静态分析的工程取舍 将处理这套算法进入真实工程后的难题：无限上升链怎样截断，soundness 与 precision 究竟有什么区别，以及分析器如何在精度、速度和规模之间作出选择。