IFDS 图可达分析框架

普通数据流函数接收一整袋事实，似乎需要为 $2^{|D|}$ 种输入都存一份结果。分配律允许把整袋拆成单个事实：无条件产生的那部分单独记，剩下每个输入事实各自贡献输出。函数因此变成至多 $(|D|+1{)}^2$ 条边。

比如污染传播 y=x 的规则是“保留除y以外的旧污染，若x污染则y污染”。它只需要一条 $x\to y$ 依赖边，不需要等x和另一个变量同时出现。反之，若某个输出只在x与z都具备时才产生，就无法用一条普通单源边表达这个合取。

手算污染事实 ​

取 $D=\{x,y,z\}$。语句 y=x 对输入S的转移是

它的图含 $0\to 0$、$x\to x$、$x\to y$、$z\to z$，但没有 $y\to y$，因为赋值覆盖了y原有污染。输入 $\{x,z\}$ 产生 $\{x,y,z\}$；输入只有 $\{y\}$ 时结果为空。

语句 x=source() 无条件令x污染，所以有 $0\to x$；x=clean() 则删除所有到输出x的事实边。其他未被写入变量保留恒等边。使用零事实能区分“没有污染事实但程序可达”和“这个程序点根本不可达”。

两次调用共用摘要，仍各自返回 ​

令 copy(p){ return p; }，主程序为

x = source()
y = copy(x)           // c1
z = copy(clean())     // c2
sink(z)

调用边将污染的实参x映到copy的形参p；过程体的摘要把入口p映到出口返回值ret。匹配的返回边在 $c_1$ 将ret映到y，因此y污染；$c_2$的实参干净，没有p污染输入，故不会产生z污染。零事实仍通过第二次调用，表示该调用确实执行，但它不等同于“参数污染”。

若允许第一调用的p事实经过程出口直接回到 $c_2$，就会把z标为污染并误报sink。IFDS复用的是“输入p会导致输出ret”的摘要边，不是把第一次调用收集到的所有输出事实无条件交给每个调用者。

一个不符合IFDS条件的转移 ​

令 $D=\{a,b,c\}$，规定只有a、b同时存在才产生c，其他事实不保留：

则 $h(\{a\}\cup \{b\})=\{c\}$，但 $h(\{a\})\cup h(\{b\})=\varnothing$。它单调却不分配。硬套逐事实边会漏掉c；加边 $a\to c$ 或 $b\to c$ 又会在缺少另一事实时过度产生。可以更换事实域编码组合条件，但域大小和算法问题已改变，不能忽略这份代价。

Tabulation怎样处理递归 ​

求解器保存形如 $(e_f,d_{in})⇝(v,d)$ 的路径事实：从过程f入口的一个输入事实出发，有一条不越出本调用层的合法路径能到达v上的d。发现新路径事实后沿普通边延伸；到调用点时，将相关输入事实传到被调入口，并登记这个调用者正等待哪些返回摘要。

当某条路径抵达被调过程出口，就生成入口事实到出口事实的摘要。把它接到已登记的匹配调用边和返回边上，继续调用者的同层路径。若摘要先出现、调用者后出现，也必须立即应用已有摘要；若调用者先登记、摘要后出现，则由新摘要唤醒等待者。两种信息到达顺序都处理，才不会漏掉递归迭代中较晚建立的关系。

调用点到返回点的旁路边用于传播不受该调用影响的事实，不能把可能被过程写坏的全局变量也当成无条件保持。实参映射、返回映射与副作用本身属于分析的输入模型；tabulation不能修复这些边上错误的流函数。

有限过程点和有限D使可保存的入口到程序点事实对有限，规则只增不减，所以迭代终止。每条新摘要由匹配调用和已有同层路径构成，保证可靠；反方向按合法路径的嵌套调用结构归纳，保证所有必要摘要最终生成。因此结果恰为给定图和转移的MVP。

成本与可检查输出 ​

设原过程间图有 $E$ 条边、$N$ 个程序点，$d=|D|$。把额外的零事实计入后，经典 tabulation 的传播时间界可写为 $O(E(d+1{)}^3)$；输入读取与程序点初始化的 $O(N+E)$ 成本另计。这个传播界计的是恰当索引和去重后的事实组合，不是任意反复扫描实现都自动满足。路径边空间通常按 $O(N(d+1{)}^2)$ 估计，另加原图和摘要索引。这样也覆盖 $D=\varnothing$ 而零事实仍存在的情况；当 $d\ge 1$ 时，与惯用的 $O(E{d}^3)$、$O(N{d}^2)$ 同阶。

算法输出可以保留每个摘要的推导来源。检查一个污染告警时，就能沿事实边和匹配调用返回恢复见证；但见证仍是一条抽象合法路径，若分支条件不相容，还需要后续可行性检查。IDE公理库IDE 值环境分析框架IDE · Interprocedural distributive environment problems每个事实还携带常量等格值时，怎样在路径上组合边函数并在路径间合流。进一步在这些依赖边上附值函数，让事实携带常量等信息。

单元任务与解答 ​

给出上面两次copy调用的全部污染来源，判断sink(z)是否应报警。解答是：唯一源边 $0\to x$；$c_1$有 $x\to p$，过程摘要有 $p\to ret$，其返回边有 $ret\to y$。$c_2$不存在污染实参到p的边，且没有无条件生成p的零事实边，所以z不在MVP中，sink(z)不报警。

验收应另外给出错误普通可达法的假见证：经$c_1$进入copy后沿$c_2$返回。把这条轨迹的调用标签和返回标签写出来，就能独立判定它为何不属于IFDS允许的路径。