单调数据流分析

reaching definitions 的轨迹 ​

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

程序先有 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 对合流运算分配，例如

在格有限高度、只处理入口在图上可达的节点且正确加入边界值的经典框架中，可得到 MFP=MOP。若还保留不可达节点，须另处理空路径族，例如要求相应 transfer 严格保持 $\mathrm{\perp }$；否则非严格的 gen 操作可能在不可达区域凭空生成事实并传入汇合点。只有单调而不分配时，先合流再 transfer 可能比逐路径后合流更粗。

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

跨过程时还要排除调用与返回不匹配的图路径。IFDS公理库IFDS 图可达分析框架IFDS · Interprocedural finite distributive subset problems哪些集合数据流问题能化成有限事实图上的匹配调用返回可达性。利用有限事实域及分配律，把集合transfer拆成单事实边和零事实边，再按合法调用返回路径求解；IDE公理库IDE 值环境分析框架IDE · Interprocedural distributive environment problems每个事实还携带常量等格值时，怎样在路径上组合边函数并在路径间合流。在边上保存值函数，进一步处理copy-constant等环境问题。这些条件比单调性更强，不能把任意已有worklist问题直接替换为IFDS或IDE。

边界与实现责任 ​

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

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

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

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