单调数据流分析

分析框架的四个部件 ​

单调数据流框架包含控制流图公理库控制流图Control-flow graph · Program control-flow graph以基本块或程序点为节点、以可能的执行转移为边表示过程内控制流的有向图。 $G=(V,E)$、性质完备格公理库完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。 $(L,⊑)$、每个节点或边的单调公理库偏序集上的单调映射Monotone map on posets · Order-preserving map · Isotone map在偏序之间保持次序的映射，以及它作为单调算子参与不动点迭代时的基本结构。 transfer $f_v:L\to L$，以及边界值。

前向 may 分析的典型方程是

$$IN[v]=\underset{u\in pred(v)}{⨆}OUT[u],OUT[v]=f_v(IN[v]).$$

后向分析把前驱换成后继，方程方向反转。must 分析可能使用 meet 或反向信息序；符号 $\bigsqcup$ 的语义必须与“更大代表更多可能”约定一致。

方程整体定义 $L^V$ 上的单调算子，因此由 Knaster–Tarski 定理有最小不动点。算法目标是计算或可靠逼近该解。

reaching definitions 的轨迹 ​

分析每个程序点可能到达的赋值定义集合。格为定义集合的幂集，次序是包含，join 是并集。赋值节点 $v$ 的 transfer 为

$$f_v(X)=ge{n}_v\cup (X\setminus kil{l}_v).$$

程序先有 d1: x:=0，随后分支一执行 d2: x:=1，分支二不改 $x$。到汇合点，第一条路径的 OUT 含 $d2$，第二条含 $d1$，join 得 $\{d1,d2\}$。

这不表示两个定义会在同一次运行同时给 $x$ 赋值为当前值；它表示任一者都可能是汇合处最近到达定义。may 事实用并集合流正是为了覆盖两条路径。

若后续执行 d3: x:=2，kill 删除 $d1,d2$，gen 加入 $d3$，输出只含 $d3$。漏掉 kill 会保持可靠却产生多余定义，错误多做 kill 则可能漏掉真实到达定义。

Worklist 求解 ​

初始化入口边界和其余节点的 $\mathrm{\perp }$，把可能变化的节点加入 worklist。每次重算 $IN/OUT$；只有输出改变时，才把受影响后继重新入队。

在有限高度格上，每个节点值只能严格上升有限次，故算法终止。若最大链高为 $h$，粗略更新次数受 $O(|V|h)$ 控制，单次 transfer 和 join 成本还要另计。

worklist 顺序影响中间更新次数，不影响有限单调框架的最小不动点。循环头优先、reverse postorder 常更快，但不是正确性的必要条件。

无限高度域需要 widening 或其他加速；普通“值看起来变化很小”不是合法停止标准。

MFP 与 MOP ​

maximum fixed-point/minimum fixed-point solution（依次序约定也称 MFP）是数据流方程的不动点结果。meet-over-all-paths（MOP）则对每条可执行 CFG 路径分别复合 transfer，再在目标点合流。

单调性通常保证迭代解对 MOP 可靠，但二者未必相等。若 transfer 对合流运算分配，例如

$$f(x\bigsqcup y)=f(x)\bigsqcup f(y),$$

经典框架下可得到 MFP=MOP。只有单调而不分配时，先合流再 transfer 可能比逐路径后合流更粗。

MOP 仍按 CFG 路径计算，可能包含语义上不可行路径。要逼近真正收集语义，还需 path feasibility 或更强关系分析；“对所有图路径”不等于“对所有真实执行且仅这些执行”。

边界与实现责任 ​

transfer 必须匹配节点粒度：基本块 transfer 应按块内语句顺序复合，不能把非交换赋值当集合无序处理。异常边、调用返回和别名写入若不在 CFG/transfer 中，会破坏全局可靠性。

前向/后向描述信息传播方向，不直接等于 may/must。reaching definitions 是前向 may，liveness 是后向 may；available expressions 常是前向 must。两个维度要分别声明。

分析结果是程序点性质，不是运行时监控日志。它以静态全称覆盖换取保守性，具体警报能否消除取决于格和 transfer 的表达精度。

稀疏分析会只在定义—使用链或 SSA 值变化处传播，而不为每个 CFG 节点保存同样事实。它可以减少无效更新，但需要证明稀疏图与原数据流方程等价。把节点删少并不自动保持解；phi 节点、异常使用和内存别名若遗漏，稀疏结果可能比原方程更“漂亮”却不可靠。

参考资料

• Gary A. Kildall, “A Unified Approach to Global Program Optimization,” POPL, 1973, pp. 194–206。
• Kam and Ullman, “Monotone Data Flow Analysis Frameworks,” Acta Informatica 7, 1977, pp. 305–317。
• Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Principles of Program Analysis, Springer, 1999, Chs. 2–3。