0%

静态程序分析课程笔记(IFDS)

Feasible and Realizable Paths

(In)Feasible Paths

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

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

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

image-20200912200105336

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

image-20200912201058304

尽管 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:

image-20200912202526474

如上所示,(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”标签。

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

image-20200912210706949

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

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$的可达路径。

image-20200913152829431

MRP

IFDS能够提供MRP的分析。

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

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

而 MRP 的分析结果为:

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

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)。

image-20200913155502967

每个调用存在三类边,如下图所示:

  • 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$(蓝色),表示调用完成返回原上下文。

image-20200913155944787

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.

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

image-20200913161605544

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

  2. 对于x=0x被赋值,将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$:

image-20200913164759047

  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$;最后若输入除ab以外的值,符合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^#$:

image-20200913175721703

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

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

image-20200913175500202

Tabulation Algorithm

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

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

image-20200913194055052

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

image-20200913194557198

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

image-20200913195133207

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

image-20200913180807055

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

此外,增加summary edge,连接$\langle Call, d_m\rangle \rightarrow \langle Ret, d_n \rangle$,作为记忆,下次做该函数调用时不需要重复计算被调函数内部的path:

image-20200913195831242

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$边,因此分析结果是错误的,而若加上别名分析,因为又是多输入,因此指针分析也不满足分配性。

image-20200913202232341

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:

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