软件分析笔记9 CFL-R&IFDS

这一节主要讨论针对CFG中的路径的优化

Feasible & Realizable Paths

Infeasible Paths: paths that do not correspond to actual executions

Unrealizable Paths: paths whose "returns" are not matched with corresponding "calls"

定义的引入很直观，动态运行时并非所有路都会被执行，因此需要区分各类假边。IP是一类难以鉴别的路(why?)，而UP是我们定义出的一类较简单就能判定的路(用带标号的括号序即可)。很显然(UPsubseteq IP)，即call和ret不匹配的路必然不会被动态执行。那么我们就可以针对UP进行优化来达到减少IP的目的。

于是我们就可以通过在边上加标号的方式来获得某path的标号序列，并通过这个序列来判断其Realizability

如果用上下文无关语言(CFL=Context Free Language)对括号序列(合法Call序列)进行识别，那么这样的可达性就叫做CFL-Reachability

注意到CFL可以用一个有限状态自动机(DFA)的接受集表示，因此只需要对CFL建出DFA，然后在传播状态的时候顺便传一下DFA的状态就可以无缝升级原来的做法了

IFDS

IFDS = Interprocedural,Finite,Distributive,Subset Problem

IFDS是一个分析框架，用于一类满足上述四个要求的分析问题

IFDS提供了MRP(Meet-over-all-Realizable-Paths)问题的解

作为对比，最早的朴素迭代算法提供了MOP(Meet-Over-all-Paths)问题的解

Overview

给定程序P，数据流分析问题Q，IFDS的流程如下

1. 对P建supergraph (G^*)​ 并根据具体问题Q定义边上的flow function

2. 对P建exploded supergraph(听起来就好中二) (G^{#})​

3. 对Q的求解就转化为对(G^{#})​应用tabulation algorithm求图可达性问题(MRP Solutions)

分配律的定义：

(f(Asqcup B)=f(A)sqcup f(B))​

通常证明不符合只需要找范例就行了。尝试证明Constprop和Pointer Analysis的分配性质：

在Constprop中，令(A=left{;(x,1); ight})，(B=left{;(y,2); ight})，处理语句 z=x+y;

则(f(A)sqcup f(B)=left{;(x,1),(z, ext{NAC}); ight}sqcupleft{;(y,2),(z, ext{NAC}); ight}=left{;(x,1),(y,2),(z, ext{NAC}); ight})​​

而(f(Asqcup B)=f(left{;(x,1),(y,2); ight})=left{;(x,1),(y,2),(z,3); ight})​，不符合分配律

PPT给了一个简单的判断法则：若求一个结果需要考虑多个(大于一个)元素的值，则不是可分配的。

在Pointer Analysis中，对变量的转移函数需要实现对象的别名分析(即语句x=y;需要考虑变量y指向对象的所有别名)，这样就涉及到了多个变量，根据简单的判断法则是不可分配的。

看完Overview有一个猜测，大概的想法如下：

1. 既然解决的是集合问题，那么就可以对每个点拆点。
2. supergraph的定义使得一条边能连接多个点，这样就可以表述集合之间的transfer关系
3. 根据分配律可以把集合的映射变为单独元素的映射构成的集合，这样就可以对点连边了
4. 这样CFG中一个点n是否包含元素x就变成了(G^{#})中<n,x>点是否从起点可达

猜完继续看视频

Supergraph

首先定义一个单独过程p的flow graph (G_p)：

1. (G_p) 是一个有向图，除basic blocks外，还包含一对唯一的起点 (start_p) 和终点 (end_p)，函数/方法调用以一对相邻节点 (call_m) 和 (ret_m)​​​ 表示
2. (G_p) 中的边除正常函数内的控制流连边外，还包含三类跨函数的边((call_m ightarrow start_m)，(end_m ightarrow ret_m)，(call_m ightarrow ret_m))

(G^*) 由一系列图 (G_1,G_2ldots) 和跨函数间的边组成，即每个函数/过程都有自己的图

发现确实猜对了.....感觉就索然无味

需要注意的一个小细节就是拆点的时候空集需要特殊处理。为了方便可以加入特殊点(varnothing)表示空集

注意到如下事实：

1. (Asqcupvarnothing=A)
2. (f(Asqcupvarnothing)=f(A)sqcup f(varnothing))
3. (f(A)sqcupvarnothing=f(A))

因此可以认为任意作用在非空集合(A)​​上的函数(f(A))​​实际上为(f(Asqcupvarnothing)=f(A)sqcup f(varnothing))​​，而(A)​中不可再分离出(varnothing)​

这就表示我们需要连(varnothing ightarrowvarnothing)的边，同时在其余的(f(A))中去掉(f(varnothing))​中的元素

有一些常数的小优化。比如说假设做完了方法p的方法内分析，那么对于所有调用了方法p的连通性其实都已经确定了