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是我们定义出的一类较简单就能判定的路(用带标号的括号序即可)。很显然\(UP\subseteq 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的流程如下
对P建supergraph \(G^*\) 并根据具体问题Q定义边上的flow function
对P建exploded supergraph(听起来就好中二) \(G^{\sharp}\)
对Q的求解就转化为对\(G^{\sharp}\)应用tabulation algorithm求图可达性问题(MRP Solutions)
分配律的定义:
\(f(A\sqcup B)=f(A)\sqcup f(B)\)
通常证明不符合只需要找范例就行了。尝试证明Constprop和Pointer Analysis的分配性质:
在Constprop中,令\(A=\left\{\;(x,1)\;\right\}\),\(B=\left\{\;(y,2)\;\right\}\),处理语句
z=x+y;
则\(f(A)\sqcup f(B)=\left\{\;(x,1),(z,\text{NAC})\;\right\}\sqcup\left\{\;(y,2),(z,\text{NAC})\;\right\}=\left\{\;(x,1),(y,2),(z,\text{NAC})\;\right\}\)
而\(f(A\sqcup B)=f(\left\{\;(x,1),(y,2)\;\right\})=\left\{\;(x,1),(y,2),(z,3)\;\right\}\),不符合分配律
PPT给了一个简单的判断法则:若求一个结果需要考虑多个(大于一个)元素的值,则不是可分配的。
在Pointer
Analysis中,对变量的转移函数需要实现对象的别名分析(即语句x=y;
需要考虑变量y
指向对象的所有别名),这样就涉及到了多个变量,根据简单的判断法则是不可分配的。
看完Overview有一个猜测,大概的想法如下:
既然解决的是集合问题,那么就可以对每个点拆点。
supergraph的定义使得一条边能连接多个点,这样就可以表述集合之间的transfer关系
根据分配律可以把集合的映射变为单独元素的映射构成的集合,这样就可以对点连边了
这样CFG中一个点n是否包含元素x就变成了\(G^{\sharp}\)中<n,x>点是否从起点可达
猜完继续看视频
Supergraph
首先定义一个单独过程p的flow graph \(G_p\):
\(G_p\) 是一个有向图,除basic blocks外,还包含一对唯一的起点 \(start_p\) 和终点 \(end_p\),函数/方法调用以一对相邻节点 \(call_m\) 和 \(ret_m\) 表示
\(G_p\) 中的边除正常函数内的控制流连边外,还包含三类跨函数的边(\(call_m\rightarrow start_m\),\(end_m\rightarrow ret_m\),\(call_m\rightarrow ret_m\))
\(G^*\) 由一系列图 \(G_1,G_2\ldots\) 和跨函数间的边组成,即每个函数/过程都有自己的图
发现确实猜对了.....感觉就索然无味
需要注意的一个小细节就是拆点的时候空集需要特殊处理。为了方便可以加入特殊点\(\varnothing\)表示空集
注意到如下事实:
\(A\sqcup\varnothing=A\)
\(f(A\sqcup\varnothing)=f(A)\sqcup f(\varnothing)\)
\(f(A)\sqcup\varnothing=f(A)\)
因此可以认为任意作用在非空集合\(A\)上的函数\(f(A)\)实际上为\(f(A\sqcup\varnothing)=f(A)\sqcup f(\varnothing)\),而\(A\)中不可再分离出\(\varnothing\)
这就表示我们需要连\(\varnothing\rightarrow\varnothing\)的边,同时在其余的\(f(A)\)中去掉\(f(\varnothing)\)中的元素
有一些常数的小优化。比如说假设做完了方法p的方法内分析,那么对于所有调用了方法p的连通性其实都已经确定了