静态程序分析课程笔记（IFDS）

Feasible and Realizable Paths

(In)Feasible Paths

Infeasible Paths: Paths in CFG that do not correspond to actual executions.

程序在CFG中会存在不被执行到路径，这些路径会污染分析结果，给静态分析带来不利影响。

然而，静态程序分析无法判断一个边是否能被执行到，例如下面代码，语义上认为程序不会走 r=-1 的路径，但是age是函数的输入，静态分析无法判断：

然而，静态分析可以识别部分不可行的路径，如下图：

尽管 r=-1 无法避免，但是在call foo(30) -> exit foo -> x=return foo这个不可行边是可以分析出的。

Realizable Paths

Realizable Paths: The paths in which “returns” are matched with corresponding “calls”.

所谓 Realizable Paths 即指那些与调用点相对应的返回路径，注意 Realizable Paths 不一定可执行，但是 unrealizable paths 一定不可执行。

判断这些边是否 realizable 的一个思路是在调用和返回边上加 “(“ 和 “)”，接着就可以用括号匹配的方式判断路径是否realizable：

如上所示，(1只能匹配)1，(2只能匹配)2。

CFL-Reachability

具体来说，用 CFL-Reachability 解决路径realizable问题：

CFL-Reachability: A path is considered to connect two nodes A and B, or B is reachable from A, only if the concatenation of the labels on the edges of the path is a word in a specified context-free language.

简单说，在边上添加label，那么一个路径realizable即这个路径上的边label组成了一个word，这个word是符合定义的上下文无关文法（CFL）的。

上下文无关文法由上下文无关语法（CFG, context-free grammar）定义——编译原理中的概念，详情见附录。

路径 realizable 问题被CFL转化为部分括号匹配问题（Partially Balanced-Parenthesis Problem）：

• 对于每一个右括号“)i” 都需要有一个对应的左括号“(i”，但反之则不需要——函数调用的边是一定可达的；
• 对于每个调用点i，将其调用边加 “(i” 的标签，将其返回边加 “)i”的标签；
• 对于其他边添加“e”标签。

如此可以定义如下上下文文法：

符合这套文法的路径就是可达的。

Overview of IFDS

IFDS[1] 实际是 Interprocedural, Finite, Distributive, Subset Problem，即 IFDS 是用来解决过程间数据流分析（interprocedural data flow）的问题，而这些问题还需满足一下条件1. 分析的domain是有限的（finite）；2. flow function满足分配率（distributive）；3. 是一个子集类型的问题（subset problem）。

下面回顾一下先前数据流分析的一些例子是否满足：

• distributive：$F$ 在$\sqcup$上满足分配率，gen-kill的问题都满足；
• finite：前三个问题是，但有些问题的domain是infinite的，如constant propagation；
• subset problem：对集合操作的问题，前三个问题都是。

Overview

如下图所示，对于一个给定程序 P，以及一个数据流分析问题 Q：

• 首先构建 supergraph $G^*$，接着定义$Q$ 的flow functions（类似于先前的转换函数）；
• 将flow functions转化为representation relations，应用于$G^*$，得到exploded supergraph $G^#$；
• 将问题 Q 转化为图 $G^#$ 上的可达性问题，应用 Tabulation algorithm 计算可达性，如：问题Q为Reaching Definitions（在程序点n处，变量 $d$ 是否有新定义，data fact $d \in MRP_n$），那么问题转化为在图 $G^#$ 上是否有从$\rightarrow$的可达路径。

MRP

IFDS能够提供MRP的分析。

回忆先前分析，对于一个路径 $p$，定义转换函数为 $pf_p$，那么 $pf_{p}=f_{n} \circ \ldots \circ f_{2} \circ f_{1}$

那么从start至n的路径$Paths(start, n)$，MOP 的分析结果为：

$$\mathrm{MOP}_{n}=\sqcup_{p \in \mathrm{Paths}(\text {start}, n)} p f_{p}(\perp)$$

而 MRP 的分析结果为：

$$\operatorname{MRP}_{n}=\sqcup_{p \in \operatorname{RPaths}(s t a r t, n)} p f_{p}(\perp)$$

区别就在于 MRP 只分析Reachable Path，因此 MRP 比MOP更准确：

$$MRP_n \sqsubseteq MOP_n$$

Supergraph and Flow Functions

Supergraph

在IFDS中，程序被表示为Supergraph，记为$G^=(N^,E^*)$，如下图所示：

• $G^*$ 是所有函数内控制流图（$G_1$, $G_2$,…）的集合；
• 每一个控制流图 $G_p$ 有一个唯一开始节点 $s_p$ 和结束节点 $e_p$；
• 每一个过程间调用都存在一个$Call_p$节点（call node）和$Ret_p$节点（return-site node）。

每个调用存在三类边，如下图所示：

• call-to-return-site edge：连接$Call_p$至$Ret_p$的边（紫色）；
• call-to-start edge：连接$Call_p$至$s_p$的边（绿色），表示从call-site至调用函数入口；
• exit-to-return-site edge：连接$e_p$至$Ret_p$（蓝色），表示调用完成返回原上下文。

Flow Function

Flow function定义为匿名函数，形式为$\lambda e_{p a r a m} \cdot e_{b o d y}$，即“输入.函数体”。

假设对“未初始化变量”问题设计Flow Function：

Possibly-uninitialized variables: for each node $n∈N^*$, determine the set of variables that may be uninitialized before execution reaches n.

注意演示时对每个边设计函数，真实情况下只需要对四种类型的边做定义，而不是所有边手工定义。

1. 程序初始化，可见 x, g 都没有赋值，因此将其加入未定义集合$S$中；

2. 对于x=0，x被赋值，将x从集合中剔除；

3. 对于$Call_p \rightarrow S_p$，将实参x状态赋值到形参a上，即<x/a>；

4. 对于a=a-g，如果a或g未定义，那么赋值会出错，将a加入未定义集合，否则赋值成功，将a从未赋值集合中去除；
5. 对于$e_p \rightarrow Ret_p$，在集合中删去形参 a 的分析结果；
6. 对于$Call_p \rightarrow Ret_p$，与先前过程间分析结果类似，考虑到g是全局变量，那么在$Call_p \rightarrow S_p$时，g的状态也会在集合中传过去，调用完g是否定义是由 P()实现决定的（是否定义的结果从$e_p \rightarrow Ret_p$这条边传过来），$Ret_p$会做 $\cup$ 操作，因此这里需要删除 g，保证更准确的结果。

Exploded Supergraph and Tabulation Algorithm

Build Exploded Supergraph

首先需要将 Flow Function转换为 representation relation， representation relations 可用一个二分图表示，图中有 2(D+1) 个节点（至多 $(D+1)^2$ 条边），$D$ 先前也介绍过，作为dataflow facts的集合（集合必须是有限的），这里就是变量的数量。

一个Flow function $f$ 的 representation relation定义为$R_f$， $R_f\subseteq (D\cup 0) \times (D\cup 0)$，实际上就是映射了$f \rightarrow edges$：

1. $R_f=\{(0,0)\}$，无条件加一条$0\rightarrow 0$边，下文会解释该边的作用；

2. $R_f=\{(0,y)\mid y\in f(\emptyset)\}$，对于f(_){return (y,_)}的function，增加$0\rightarrow y$；

3. $R_f=\{(x, y) \mid y \notin f(\emptyset) \text { and } y \in f(\{x\})\}$，对于f(x,_){return (y,_)}的function，增加$x\rightarrow y$。

以图上四个function为例：

• 对于$\lambda\text{ } \mathrm{S} \cdot(\mathrm{S}-\{\mathrm{a}\}) \cup\{\mathrm{b}\}$，首先无条件添加$0\rightarrow 0$边；接着由于其总会返回b，因此符合2，增加$0\rightarrow b$；最后若输入除a，b以外的值，符合3，添加$c\rightarrow c$；

• 对于$\lambda\text{ } ifthenelse$，因为有f(a,_){return(a,b,_)}，因此增加$a\rightarrow a,a\rightarrow b$，其他同上。

从此之后，分析不再需要flow function，只需要将Relations在Supergraph上画出即可。

根据Representation Relations可以得到$G^#$：

为何要添加 $0\rightarrow 0$ 的边；

对与一个程序点p，其结果是由多个flow function影响，而在IFDS上影响的结果由图的可达性表示，考虑有$\lambda \text{ } S \cdot \{a\}$这一个function，若没有$0\rightarrow0$，那么a无法可达，分析结果错误：

Tabulation Algorithm

通过图可达性推导Possibly-uninitialized variables，还需最后一步，即判断路径是否成立。

例如对于$e_{main}$节点下的$g$，可以找到$\langle S_{main},0\rangle \rightarrow \langle e_{main},g\rangle$的合法路径，因此g有可能不存在定义：

而对于$Print(a,g)$节点下的g，尽管其存在路径，但是路径合法，因此g不存在集合中，即g一定是已定义的。

计算图中点的可达性即Tabulation Algorithm，如下图所示，对于从$\langle S_{main},0\rangle $可达的点用蓝色点表示，该算法就是找出这些可达（蓝色）的点。

算法内容如下，其复杂度为$O(ED^3)$，课程中并没有时间说明时间细节：

算法中主要思想是在每个exit node处进行CFL-Reachability 检查，而其他node之间自然可达（绿色）；

此外，增加summary edge，连接$\langle Call, d_m\rangle \rightarrow \langle Ret, d_n \rangle$，作为记忆（e.g., $a\rightarrow \{b\}$, $b\rightarrow\{b, c\}$），下次做该函数调用时不需要重复计算被调函数内部的path：

Function summary

对于程序中的库调用函数，可以体现做函数摘要，如下图所示：

只要在库上跑一遍 IDFS 就可以得到函数摘要：

函数摘要不需要保存函数内部转换过程（蓝色线），只需要保存转换结果（红色线），但是这样的话做摘要就得计算每个变量的可达性，即复杂度是$O(n^2)$，n为变量个数（还包括全局变量）。

函数摘要实际上形式是$f: \langle gen, kill\rangle$，换句话说$f(x)=gen\cup(x-kill)$，函数执行初始值为$\langle\{\},\{\}\rangle$）

在函数内做数据流分析，transfer为$\left(g_{1}, k_{1}\right) \circ\left(g_{2}, k_{2}\right)=\left(g_{2} \cup\left(g_{1}-k_{2}\right), k_{1} \cup k_{2}\right)$：

$$\begin{aligned} f_{2} \circ f_{1}(x) &=gen_{2} \cup\left(\left(gen_{1} \cup\left(x-kill_{1}\right)\right)-kill_{2}\right) \\ &=\left(gen_{2} \cup\left(gen_{1}-kill_{2}\right)\right) \cup\left(x-\left(kill_{1} \cup kill_{2}\right)\right)\\ \end{aligned}$$

汇聚点操作为$\left(g_{1}, k_{1}\right) \sqcap\left(g_{2}, k_{2}\right)=\left(g_{1} \cup g_{2}, k_{1} \cap k_{2}\right)$：

$$\begin{aligned} \left(f_{1} \sqcap f_{2}\right)(x) &=f_{1}(x) \sqcap f_{2}(x) \\ &=\left(g e n_{1} \cup\left(x-k i l l_{1}\right)\right) \cup\left(g e n_{2} \cup\left(x-k i l l_{2}\right)\right) \\ &=\left(g e n_{1} \cup g e n_{2}\right) \cup\left(x-\left(k i l l_{1} \cap k i l l_{2}\right)\right) \end{aligned}$$

通过证明，可见用以上方法做出来的函数摘要进行数据流分析，分析结果和原数据流分析完全相同(具有单调性、分配性和正确性)。

这里个人有个疑惑，考虑如下代码：

interface Adder { String add(String a,String b);}
class Adder1 implements Adder{
    public String add(String a, String b){
        return a+b;
    }
}
class Adder2 implements Adder{
    public String add(String a, String b){
        return a+"b";
    }
}
class AdderAgent implements Adder{
    private Adder adder;
    public AdderAgent(Adder a){
        this.adder = a;
    }
    public String add(String a, String b){ // summary this
        return this.adder.add(a,b);
    }
    public static String add(Adder adder, String a, String b){ // summary this
        return adder.add(a,b);
    }
}

如果需要对AdderAgent.add(Adder adder, String a, String b)做函数摘要，那么其因为依赖于adder的实现，就可能需要做两份摘要，即若adder=Adder1时，其摘要是$\langle(ret\rightarrow a+b),(ret\rightarrow any)\rangle$，若adder=Adder2时，其摘要是$\langle(ret\rightarrow a),(ret\rightarrow any)\rangle$，也就是说，要做两份函数摘要，这里份数取决于Adder子类的个数。

此外，对AdderAgent.add(String a, String b)还要保存其成员变量（self.adder）的类型。

Understanding the Distributivity of IFDS

IFDS不能做Flow function不满足分配性（$F(x \wedge y) \neq F(x) \wedge F(y)$）的数据流分析。

以常量传播为例，考虑z=x+y，设计的Flow function为$(x,y,_)\rightarrow(x+y,_)$，可以看到一个输出是两个输入“同时”决定的，在representation relation中是无法表示的，换句话说，IFDS只能描述data fact（点）和propagation（边）能被独立处理的分析问题（按个人理解，IFDS能处理的一个原子操作就是$a \rightarrow b$，可以独立表示$a\rightarrow b,c\rightarrow b,b\rightarrow b$，而不能表示$a\wedge c \rightarrow b$）。

同样，IFDS不能用于指针分析，如下图所示，当处理z=y.f语句时，由于没有别名信息，无法连接$x\rightarrow y.f$边，因此分析结果是错误的，而若加上别名分析，因为又是多输入，因此指针分析也不满足分配性。

IDE（Interprocedural，Distributive，Environment problem）作为IFDS的优化，可以解决infinite的问题，但是仍需满足distributive。

总结

本节课讲了IFDS的大致思路，详细还需看最初的论文，注意IFDS和传统的content-sensitive是没有可比性的。

Appendix: Context-free Grammar

CFG is a formal grammar in which every production is of the form:

$$S \rightarrow \alpha$$

where $S$ is a single nonterminal and $\alpha$ could be a string of terminals and/or nonterminals,or empty.

简单说上下文无关文法定义了一个句子的生成规范，即 $S\rightarrow \alpha$ ，其中$S$为一个非终结符，$\alpha$可以使一个终结/非终结符号，或者是空($\varepsilon$)。

例如有如下上下文无关文法：

• $S \rightarrow aSb$
• $S \rightarrow \varepsilon$

那么可以生成一下句子”ab“，“aabb”，…

上下文无关文法与上下文相关（Context-sensitive）文法的区别就在于语句生成规则，无关文法可以无视上下文随意应用规则，而相关文法的每个规则是在上下文下才成立的。

References

1. Precise Interprocedural Dataflow Analysis via Graph Reachability. Thomas Reps, Susan Horwitz, and Mooly Sagiv, POPL’95