【课程笔记】南大软件分析课程11——CFL可达性&IFDS

Tattoo

发布日期: 2020-07-22 10:12:37 浏览量: 131
评分:
star star star star star star star star star star_border
*转载请注明来自write-bug.com

最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)
原作者:bsauce
原文链接:https://www.jianshu.com/p/2bd21a34eb8b

首先非常感谢南京大学李樾谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。

推送门南大课件 南大视频课程 北大课件


目录

  1. Infeasible and Realizable Paths——基本概念
  2. CFL-Reachablity(IFDS的理论基础,识别Realizable path)
  3. Overview of IFDS
  4. Supergraph(之前叫iCFG) and Flow Functions
  5. Exploded Supergraph and Tabulation Algorithm
  6. Understanding the Distributivity of IFDS

重点

IFDS:Interprocedural,Finite,Distributive,Subset Problem。

理解CFL-Reachablity,工作机制—括号匹配的过程。

IFDS的大致原理。

哪些问题可以利用IFDS,目标问题是否可以利用IFDS,取决于其是否满足可分配性。

目标:以图可达性分析来进行程序分析,没有了数据流传播的过程。

1.Infeasible and Realizable Paths——基本概念

Infeasible Paths:CFG中实际不会执行到的路径,如不匹配的调用返回边。这种路径可能会影响到程序分析的结果,但静态分析不能完全判定路径是否可达。

Realizable Paths:跨函数调用产生的返回边和对应的callsite边匹配,这样的path。

目标:识别Realizable path,避免沿着Unrealizable path来传播数据分析。

方法CFL-Reachablity


2.CFL-Reachablity(IFDS的理论基础,识别Realizable path)

CFL-Reachablity:path连接A和B,或者说A能到达B,当且仅当path所有边的labels连接起来 是context-free language(CFL)中的一个word(或者说经过CFG语法变换之后可以得到该path word)。CFL是编译原理中的概念,遵循CFG语法。

Context-Free Grammar (CFG):CFG是一个形式化语法,每一个产生的形式都是 SαS \to \alphaα\alpha可以是字符串也可以是空ε\varepsilon)。EgEgSaSbS \to aSbSεS \to \varepsilonContext-Free表示不管S出现在哪(不管上下文),S都可以被替换成aSb/εaSb / \varepsilon

部分括号匹配问题(Partially Balanced-Parenthesis):利用CFL来解决括号匹配问题,以识别Realizable path

  • 部分——有)i一定要有(i,反之有(i不一定要有)i,也即可以调用子函数而不返回。

  • 标记,调用边——(i;返回边——)i;其他边——e。

CFL-Reachablity:若path word(所有edge的label连起来组成的单词)可用CFL L(realizable)表示(可进行各种替换),则为Realizable Path。示例如下,(1(2e)2)1(_1(_2e)_2)_1(3就是边的label相连接形成的,绿色是可匹配的部分,realizable可被替换为matched realizable(i realizableε\varepsilon。语法替换规则如下,这也是一个CFL语言示例:

利用CFL分析Realizable Path示例:右边显然不是Realizable Path

3.Overview of IFDS

IFDS含义:Interprocedural,Finite,Distributive,Subset Problem。Interprocedural—全程序分析,Finite—域有限(如live variables、definitions),DistributiveTransfer Function满足f(ab)=f(a)f(b)f(a \cup b)=f(a) \cup f(b),Subset—子集问题。

利用图可达性的程序分析框架:采用的操作——Meet-Over-All-Realizable-Paths(MRP),MRPnMOPnMRPn \sqsubseteq MOPn。MOP对所有路径进行meet操作,MRP只对realizable path进行meet操作,更准确。

IFDS步骤:给定程序P,数据流分析问题Q。

  • 1.构造P的supergraph GG^*,根据问题Q定义GG^*上每条边的流函数。

  • 2.构造P的exploded supergraph GG ^ \sharp,将流函数转化为Representation relation(分解后变成小子图形式)

  • 3.问题Q变成图可达性问题(寻找MRP解),对GG ^ \sharp采用Tabulation算法。n—程序点,data fact dMRPnd \in MRPn,当且仅当GG ^ \sharp中存在一条<Smain,0><n,d><Smain, 0> \to <n, d>realizable path

4.Supergraph(之前叫iCFG) and Flow Functions

(1)IFDS步骤一:构造Supergraph

说明:之前叫iCFG,给每个node定义transfer function;现在叫做Supergraph,给每个edge定义transfer function

SupergraphG=(N,E)G^*=(N^*, E^*)

  • GG^*包含所有的流图G1G_1, G2G_2, … (每个函数对应一个流图,本例对应GmainG_{main}GpG_p);

  • 每个流图GpG_p都有个开始节点sps_p和退出节点epe_p

  • 每个函数调用包含调用节点CallpCall_p + 返回节点RetpRet_p

  • 函数调用有3类边:

    • 过程内call-to-return-site边,从CallpRetpCall_p \to Ret_p

    • 过程间call-to-start边,从CallpspCall_p \to s_psps_p是被调用函数的开头);

    • 过程间exit-to-return-site边,从epRetpe_p \to Ret_pepe_p是被调用函数的结尾)。

(2)IFDS步骤一:设计流函数

问题Q:假设问题Q是找可能未被初始化的变量,对每个节点nNn \in N^*,找到执行到n时可能未被初始化的变量集合。

说明λ\lambda——lambda 中’.’左侧的S表示输入的集合,右边表示对S的操作。对于未初始化变量问题,遇到var x;指令则 λS.Sx\lambda S.S \cup {x}—加入x变量;如遇x:=...;指令则λS.Sx \lambda S.S-{x}—去掉x;遇到无关指令则λS.S \lambda S.S—不变。

示例

  • call-to-callee把与callee直接相关信息传递进去,如用形参替换实参;

  • exit-to-return边把形参相关信息剔除;

  • call-to-return-site只传递局部变量,排除全局变量g,降低误报。全局变量已经传入到被调用函数进行处理了,全局变量是否被初始化取决于被调用函数。

5.Exploded Supergraph and Tabulation Algorithm

(1)IFDS步骤二:构造exploded supergraph

Exploded Supergraph GG ^ \sharp:将trans func转换成边的关系representation relations(graph),每个流函数变成了有2(D+1)个节点,边数最多(D+1)2,D表示dataflow facts元素个数(如待分析的变量个数)。GG^*中每个结点n被分解成D+1个结点,每条边n1n2n_1 \to n_2被分解成representation relation

representation relation:用Rf表示,流函数-f。Rf(D0)×(D0)R_f \subseteq (D \cup 0) \times (D \cup 0)RfR_f规则如下:

  1. 000 \to 0始终有一条边;

  2. 0d10 \to d_1yf()y \in f( \varnothing) 若没有任何输入也能得到y,则加上该边;

  3. d1d2d_1 \to d_2,y可以从x得到,但不能从0得到,则加上该边;

  4. 还有一条,didid_i \to d_i,与did_i无关时自己连自己,保持可达性。

示例

(1)输入S是什么输出就是什么,1/3;

(2)无论什么输入,都输出{a},1/2;

(3)b是无条件产生,所以0→b,a不能往下传了,b已经从0可达了就不用加b→b,c不受影响,也即无论有关a和b的事实之前是什么样,都不再重要;

(4)b通过a得到所以a→b,不影响a、c的传递。注意,这里的值不是说变量在程序中真正的值是多少,而是说有关此变量的数据流事实的值是什么,如a的值可以为被初始化了未被初始化两种,对应的集合即不包括和包括a。

问题:为什么需要000 \to 0的边?以往数据流分析中,确定程序点(结点)p是否包含data fact a,是看a是否在OUT[p]中;IFDS中,是看<smain,0><s_{main}, 0>是否能到达<p, a>。如果没有000 \to 0的边,则无法完全连通,所以000 \to 0又称为Glue Edge

构建GG^ \sharp示例:最后能从<smain,0><emain,g><s_{main}, 0> \to <e_{main}, g>(要通过realizable paths),则emaine_{main}点的g是可能未初始化的。emaine_{main}处的x和nPrint(a,g)n_{Print(a,g)}处的g都是初始化过的,因为从smains_{main}不可达(不能通过non-realizable paths——绿色线)。

(2)IFDS步骤三:Tabulation算法——判断是否可达

说明:实心圈表示从<smain,0><s_{main}, 0>通过realizable paths可达,空心圈表示不可达。

目标:给定exploded supergraph GG^ \sharp,Tabulation算法通过寻找从<smain,0><s_{main}, 0>的所有realizable paths来确定MRP解。也即n—程序点,data fact dMRPnd \in MRPn,当且仅当GG^ \sharp中存在一条<Smain,0><n,d><S_{main}, 0> \to <n, d>realizable path

Tabulation算法:复杂度是O(ED3)O(ED^3),E—supergraph的边数,D是域中待分析元素的个数。主要工作:括号匹配+路径探索。主要就是处理调用边、返回边、总结边,将间接可达的两结点直接连起来,每个结点用Xn存储当前所有可达的data fact

  1. calledProc: 把函数调用结点(call)和代表被调用函数名关联上

  2. returnSite: 把call结点和return结点连起来

  3. callers: 把函数名映射到call结点所形成的集合关联

  4. procOf: 把函数结点和它的函数主体关联

Tabulation算法工作原理:假设只关注1个data fact,p’被p和p’’同时调用。

  • 处理括号匹配:每次处理到返回点epe_{p^{\prime}}时,开始括号匹配(call-to-return匹配),找到调用点(Callp,Callp)(Callp, Call{p^{\prime \prime}})和相应的返回点(Retp,Retp)(Retp, Ret{p^{\prime \prime}})

  • 处理总结边——SummaryEdge:总结边—<Call,dm><Ret,dn><Call,d_m> \to <Ret,d_n>,表示dmd_m通过调用pp^{\prime}能到达pnp_n,要避免重复处理pppp^{\prime \prime}中调用同一函数pp^{\prime}(优化)。

Tabulation算法优点:传统的worklist算法是利用了queue的特性,每次循环只考虑与被改变值结点的相关结点。论文中用于解决图可达问题的Tabulation 算法是基于worklist的动态规划算法,比传统worklist算法考虑interprocedure问题更精确也更省时。

6.Understanding the Distributivity of IFDS

问题:不能用IFDS进行常量传播分析、指针分析。

原因:由IFDS的框架决定,一次只能处理1个变量。例如,表示若x和y都存在则…,无法表示这种关系。不满足F(x^y)=F(x)^F(y)

总结:给定语句S,如果输出取决于多个输入的data fact,则该分析不具备可分配性,不能用IFDS表达。IFDS中,每个data fact(圆圈)与其传播(边)都可以各自处理,且不影响最终结果。

指针分析:箭头表示变量是否指向new T,但由于缺乏别名信息alias(x,y) / alias(x.f,y.f),导致分析结果错误。归根结底,要想在IFDS中获取别名信息alias(x,y),需要考虑多个输入data fact(x、y),所以不能用IFDS。

参考

用求解图内节点是否可达的算法来解决IFDS问题

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

93
文章数
34
评论数
最近文章
eject