前面几节中提出的思想可以通过一个工作列表算法结合在一起，得到一个强大的分析框架，称为IFDS（Interprocedural, Finite, Distributive, Subset）[RHS95]。 IFDS涵盖了流敏感分析，其中抽象状态的格是$\mathcal{P}(D)$的形式，其中D是有限集合，并且所有的转移函数都具有分配律。对于满足这些限制的分析问题，该框架在多项式时间内提供了完全的上下文敏感分析。

    集合 D 中的元素表示数据流事实，例如，“变量 x 可能未初始化”。目标程序被表示为一个过程间控制流图（如第8.1节所述），其中每个节点 v 由一个传递函数 t_v: P(D) -> P(D) 描述，如第9.3节所解释的那样，以二分图的形式表示。该框架通常应用于前向分析；可以通过反转 CFG 边和点，并交换函数入口和出口节点的角色来执行后向分析。格的偏序关系序通常是 $\\subseteq$，但 $\\supseteq$也可以工作。

    目标程序的遍历控制流图（exploded CFG）中，对于每个 CFG 节点 v 和元素 $d \\in D \\cup {\\bullet }$ 的对<v, d>，都有一个节点来对应。如果 t_v 的二分图中存在边 d1 → d2，并且 CFG 中有从节点 v1 到节点 v2 的边，即 v2 是 v1 的后序，那么exploded CFG 就有一条边从 (v1; d1) 到 (v2; d2)，表示为 $<v_1, d_1> \\rightarrow <v_2, d_2>$。让 E 表示给定程序的所有这样的边的集合。参数传递和返回值的流动可以像第9.1节中的赋值一样处理。对于不受函数调用影响的局部变量，从调用节点到其调用后节点的直接数据流也可以类似地建模。

    作为一个例子，令Vars={x,y,z}，v是一个赋值语句 x = y + z，并且v’是v的前序节点，那么对于可能未初始化变量分析中应用赋值语句的转移函数，E就会包含如下的边：（v‘处yz，那么赋值之后就是xyz，边就是转移函数定义的求值的过程）

Exploded CFG有一个很好的性质，对于一个数据流事实或者结果 $d \in D$在节点v处成立，那么当且仅当<v,d>可以从$<entry_{main}, \bullet>$经过过程间一条合法的路径可达才行。

    IFDS算法分为两个阶段，类似于第9.2节中可能未初始化变量分析的另一种表述。第一个阶段（对应于第9.2节中的预分析阶段）称为表格算法（tabulation algorithm）。它逐步构建了一组路径边记做为 $\\mathbf{P}$，每一条边表示为 $<v_1, d_1> \\leadsto <v_2, d_2>$，其中v1是函数入口节点，v2是与v1相同函数中的CFG节点，而$d_1,d_2 \\in D \\cup {\\bullet}$。其思想是，对于节点v2，路径边集合 $\\{<v_1,d_1> \\leadsto <v_2,d_2> \\in \\mathbf{P} | d_1,d_2 \\in D \\cup \\{\\bullet\\} \\}$ 构成了v2的跳转函数的二分图表示（参见第112页），它将包含v2的函数入口v1处的数据流事实与v2处的数据流事实相关联。然而，可达性的处理略有不同。IFDS中的可达性不是在特定上下文中跟踪函数的可达性（如第9.1节中可能未初始化变量分析的原始表述）或独立于上下文跟踪函数的可达性（如第9.2节中的替代分析表述）；而是在个别数据流事实的级别上进行跟踪的：只有在我们已经确定<v1,d1>可能从程序入口可达时，才将路径边 $<v_1, d_1> \\leadsto <v_2, d_2>$添加到 P 中。

第一阶段

路径边是根据不同类型的CFG节点的以下约束条件构建的最小解。因此，在这个分析阶段使用的格是路径边的幂集格（powerset lattice）。

1. 第一条规则描述的是对于程序的入口总是可达：

   

2. 假设v是一个函数的入口节点，v1是v的一个前序节点并且v1是一个调用节点，v0是包含v1的函数的入口节点，第二条规则描述的是数据流事实沿着可达性从调用节点到被调用的入口节点：

   

   初看上去，这条规则错了（v到v）；但是在第一阶段我们不传递数据流事实（这是第二阶段的任务），我们在第一阶段只构建路径的可达边，也就是那些从主函数入口可以到达的边。新边$<v, d_3> \leadsto <v, d_3>$的含义是<v,d3>这个情况是可以从主函数到达的。

3. v’是调用节点，v是调用后的节点，v0是这两个节点所在函数的入口节点，w是v’的一个后继，w‘是v的一个前序，我们用第三条规则描述数据流事实从v0到v’最后到达v：

   

   可以通过如下图来表示规则三，其中实线和虚线分别表示E和P里面的边，厚虚线表示先加入的边。注意这条规则利用w’这个退出节点的路径边作为被调用函数的一个摘要，数据流在可行的边之间进行跨函数流动，这是获得想要的上下文敏感的基础。

   

4. 第四条规则描述函数内部的状态，从一个调用节点v’到调用之后的节点v，其中v0是函数的入口节点：

   

   这条规则同样适用于任何其他节点v，这个v带有一个前序v’，并且v0是函数的入口，这是描述过程内数据流动的通用形式。

对于上述规则，可以简单的通过work-list算法得到最小结果集合。

第二阶段

第二阶段（对应9.2节的主分析阶段）用于计算分析最终的结果，这个过程简单并且完全是过程内分析：对于任何CFG节点v的抽象状态 $[[v]] \in \mathcal{P}(D)$，可以直接从v的路径边来获得，假设v0是v同一个函数的入口节点，那么：

这个能够工作的原因是，第一阶段已经分析出有一条可达的边从v0到v，当切仅当数据流d2可能在v满足。因为在第一阶段对于单个数据流事实精确的跟踪，第二阶段相比于9.2节的主分析要简单很多。

    在继续运行示例时，可以通过设置D = Vars来实例化IFDS框架，即分析可能未初始化的变量。这里的Vars表示被分析程序中的变量集合，并根据第9.1节中的转移函数以及上述程序CFG中的控制流边来定义exploded CFG中的边E。