【课程笔记】南大软件分析课程4——数据流分析基础

Tattoo

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

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

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

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


关于这一节zcc的笔记已经够完美了,我就直接在他基础上记录了。

目录

  1. 迭代算法-另一个角度
  2. 偏序(Partial Order)
  3. 上下界(Upper and Lower Bounds)
  4. 格(Lattice),半格(Semilattice),全格和格点积(Complete and Product Lattice)
  5. 数据流分析框架(via Lattice)
  6. 单调性与不动点定理(Monotonicity and Fixed Point Theorem)
  7. 迭代算法转化为不动点理论
  8. 从lattice的角度看may/must分析
  9. 分配性(Distributivity)和MOP
  10. 常量传播
  11. Worklist算法

重点

上节课是介绍了3种数据流分析迭代算法,本节课将从数学理论的角度来讨论数据流分析,加深对数据流分析算法的理解。

1.迭代算法-另一个角度

本质:常见的数据流迭代算法,目的是通过迭代计算,最终得到一个稳定的不变的解。

(1)理论

定义1:给定有k个节点(基本块)的CFG,迭代算法就是在每次迭代时,更新每个节点n的OUT[n]。

定义2:设数据流分析的值域是V,可定义一个k-元组(OUT[n1],OUT[n2],..,OUT[nk])(OUT[n_1],OUT[n_2], .. , OUT[n_k])是集合 (V1×V2..×Vk)(V_1 \times V_2 .. \times V_k) (幂集,记为VkV_k)的一个元素,表示每次迭代后k个节点整体的值。

定义3:每一次迭代可看作是Vk映射到新的Vk,通过转换规则和控制流来映射,记作函数F:VkVkF:V_k \rightarrow V_k

迭代算法本质:通过不断迭代,直到相邻两次迭代的k-元组值一样,算法结束。

(2)图示

不动点:当Xi = F(Xi)时,就是不动点。

问题

  • 迭代算法是否一定会停止(到达不动点)?
  • 迭代算法如果会终止,会得到几个解(几个不动点)?
  • 迭代几次会得到解(到达不动点)?

2.偏序(Partial Order)

定义:给定偏序集(P,)(P, \sqsubseteq)\sqsubseteq是集合PP上的二元关系,若满足以下性质则为偏序集:

  • 自反性Reflexivity:∀x∈P, x⊑x

  • 对称性Antisymmetry:∀x,y∈P, x⊑y∧y⊑x ⇒ x=y

  • 传递性Transitivity:∀x,y∈P, x⊑y ∧ y⊑z ⇒ x⊑z

例子

  • P是整数集,\sqsubseteq表示\leq,是偏序集;若\sqsubseteq表示<,则显然不是偏序集

  • P是英文单词集合,\sqsubseteq表示子串关系(可以存在两个元素不具有偏序关系,不可比性),是偏序集

3.上下界(Upper and Lower Bounds)

(1)定义

定义:给定偏序集(P, \sqsubseteq),且有P的子集S⊆P:

  • ∀x∈S, x⊑u, 其中u∈P,则u是子集S的上界 (注意,u并不一定属于S集

  • ∀x∈S, l⊑x, 其中l∈P,则l是S的下界

最小上界:least upper bound(lub 或者称为join),用⊔S表示。上确界?

定义:对于子集S的任何一个上界u,均有⊔S⊑u。

最大下界:greatest lower bound(glb 或者称为meet),用⊓S表示。下确界?

定义:对于子集S的任何一个下界l,均有l⊑⊓S。

(2)示例

若S只包含两个元素,a、b(S = {a, b})那么上界可以表示为a⊔b,下界可以表示为a⊓b。

(3)特性

  • 并非每个偏序集都有上下确界

  • 如果存在上下确界,则是唯一的

利用传递性和反证法即可证明。

4.格(Lattice),(半格)Semilattice,全格,格点积(Complete and Product Lattice)

都是基于上下确界来定义的。

(1)格

定义:给定一个偏序集(P,⊑),∀a,b∈P,如果存在a⊔b和a⊓b,那么就称该偏序集为格。偏序集中的任意两个元素构成的集合均存在最小上界和最大下界,那么该偏序集就是格。

例子

  • (S, ⊑)中S是整数子集,\sqsubseteq\leq,是格点

  • (S, ⊑)中S是英文单词集,\sqsubseteq表示子串关系,不是格点,因为单词pin和sin就没有上确界

  • (S, ⊑)中S是{a, b, c}的幂集,\sqsubseteq表示\subseteq子集,是格点

(2)半格

定义:给定一个偏序集(P,⊑),∀a,b∈P:

  • 当且仅当a⊔b存在(上确界),该偏序集叫做 join semilatice

  • 当且仅当a⊓b存在(下确界),该偏序集叫做 meet semilatice

(3)全格

定义:对于格点 (S, \sqsubseteq) (前提是格点)的任意子集S,⊔S上确界和⊓S下确界都存在,则为全格complete lattice。

例子

  • P是整数集,\sqsubseteq\leq,不是全格,因为P的子集正整数集没有上确界

  • (S, ⊑)中S是{a, b, c}的幂集,\sqsubseteq表示\subseteq子集,是全格

符号=P\top = \sqcup P,叫做top;=P\perp = \sqcap P,叫做bottom。

性质:有穷的格点必然是complete lattice。全格一定有穷吗? 不一定,如实数界[0, 1]。

(4)格点积

定义:给定一组格,L1=(P1,1)L_1=(P_1, \sqsubseteq 1)L2=(P2,2)L_2=(P_2, \sqsubseteq 2),.. ,Ln=(Pn,n)L_n=(P_n, \sqsubseteq n),都有上确界i\sqcup i和下确界i\sqcap i,则定义格点积 Ln=(P,)Ln = (P, \sqsubseteq)

P=P1×..×PnP = P_1 \times .. \times P_n

(x1,..xn)(y1,..yn)(x1y1)..(xnyn)(x_1, .. x_n) \sqsubseteq (y_1, .. y_n) \Leftrightarrow (x_1 \sqsubseteq y_1) \wedge .. \wedge (x_n \sqsubseteq y_n)

(x1,..xn)(y1,..yn)=(x1y1,..,xnyn)(x_1, .. x_n) \sqcup (y_1, .. y_n) = (x1 \sqcup y_1, .., x_n \sqcup y_n)

(x1,..xn)(y1,..yn)=(x1y1,..,xnyn)(x_1, .. x_n) \sqcap (y_1, .. y_n) = (x_1 \sqcap y_1, .., x_n \sqcap y_n)

性质:格点积也是格点;格点都是全格,则格点积也是全格。

5.数据流分析框架(via Lattice)

数据流分析框架(D, L, F) :

  • D—方向

  • L—格点(值域V,meet \sqcap 或 join \sqcup 操作)

  • F—转换规则VVV \rightarrow V

数据流分析可以看做是迭代算法格点 利用转换规则meet/join操作

6.单调性与不动点定理(Monotonicity and Fixed Point Theorem)

目标问题:迭代算法一定会停止(到达不动点)吗?

(1)单调性

定义:函数f:LLf: L \rightarrow L,满足∀x,y∈L,x⊑y⇒f(x)⊑f(y),则为单调的。

(2)不动点理论

定义:给定一个完全lattice(L,⊑),如果f:L→L是单调的,并且L有限

那么我们能得到最小不动点,通过迭代:f(⊥),f(f(⊥)),…,fk(⊥)直到找到最小的一个不动点。

同理 我们能得到最大不动点,通过迭代:f(⊤),f(f(⊤)),…,fk(⊤)直到找到最大的一个不动点。

(3)证明

不动点的存在性;

最小不动点证明。

7.迭代算法转化为不动点理论

问题:我们如何在理论上证明迭代算法有解有最优解何时到达不动点?那就是将迭代算法转化为不动点理论。因为不动点理论已经证明了,单调、有限的完全lattice,存在不动点,且从⊤开始能找到最大不动点,从⊥开始能找到最小不动点。

目标:证明迭代算法是一个完全lattice(L,)lattice(L, \sqsubseteq),是有限的,单调的。

(1)完全lattice证明

根据第5小节,迭代算法每个节点(基本块)的值域相当于一个lattice,每次迭代的k个基本块的值域就是一个k-元组。k-元组可看作lattice积,根据格点积性质:若Lk中每一个lattice都是完全的,则Lk也是完全的。

(2)L是有限的

迭代算法中,值域是0/1,是有限的,则lattice有限,则Lk也有限。

(3)F是单调的

函数F:BB中转换函数fi:L → L + BB分支之间的控制流影响(汇聚是join \sqcup / meet \sqcap 操作,分叉是拷贝操作)。

  1. 转换函数:BB的gen、kill是固定的,值域一旦变成1,就不会变回0,显然单调。

  2. join/meet操作:L × L → L 。证明:∀x,y,z∈L,且有x⊑y需要证明x⊔z⊑y⊔z。

总结:迭代算法是完全lattice,且是有限、单调的,所以一定有解、有最优解。

(4)算法何时到达不动点?

定义lattice高度—从lattice的top到bottom之间最长的路径。

最坏情况迭代次数:设有n个块,每次迭代只有1个BB的OUT/IN值的其中1位发生变化(则从top→bottom这1位都变化),则最多迭 (n × h) 次。

8.从lattice的角度看may/must分析

说明:may 和 must 分析算法都是从不安全到安全(是否安全取决于safe-aprroximate过程),从准确到不准确。

(1)may分析

以 Reaching Definitions分析为例:

  1. \perp开始,\perp表示所有定义都不可达,是不安全的结果(因为这个分析的应用目的是为了查错,查看变量是否需要初始化。首先在Entry中给每个变量一个假定义,标记所有变量为都为未初始化状态,\perp表示所有的假定义都无法到达,说明所有变量在中间都进行了赋值,那就不需要对任何变量进行初始化,这是不安全的,可能导致未初始化错误)。

  2. \top表示所有Entry中的假定义都可达,从查错角度来说,需要对每个变量都进行初始化,非常安全!但是这句话没有用,我都要初始化的话还做这个分析干嘛?

  3. Truth:表明最准确的验证结果,假设{a,c}是truth,那么包括其以上的都是safe的,以下的都是unsafe,就是上图的阴影和非阴影。

  4. \perp\top,得到的最小不动点最准确,离Truth最近。上面还有多个不动点,越往上越不准。

(2)must分析

以available expressions分析为例:

  1. \top开始,表示所有表达式可用。如果用在表达式计算优化中,那么有很多已经被重定义的表达式也被优化了(实际上不能被优化),那么该优化就是错误的,不安全

  2. \perp表示没有表达式可用,都不需要优化,很安全!但没有用。

  3. \top\perp,就是从不安全到安全,存在一个Truth,代表准确的结果。

  4. \top\perp,达到一个最大不动点,离truth最近的最优解。

迭代算法转化到lattice上,may/must分析分别初始化为最小值\perp和最大值\top,最后求最小上界/最大下界。

9.分配性(Distributivity)和MOP

目的:MOP(meet-over-all-paths)衡量迭代算法的精度。

(1)概念

定义:最终将所有的路径一起来进行join/meet操作。

路径P = 在cfg图上从entry到基本块si的一条路径(P = Entry → s1 → s2 → … → s~i )。

路径P上的转移函数Fp:该路径上所有语句的转移函数的组合fs1,fs2,… ,fsi-1,从而构成FP。

MOP:从entry到si所有路径的FP的meet操作。本质—求这些值的最小上界/最大下界。

MOP准确性:有些路径不会被执行,所以不准确;若路径包含循环,或者路径爆炸,所以实操性不高,只能作为理论的一种衡量方式。

(2)MOP vs 迭代算法

对于以上的CFG,抽象出itter和MOP公式。

证明

  1. 根据最小上界的定义,有x⊑x⊔y和 y⊑x⊔y。

  2. 由于转换函数是单调的,则有F(x)⊑F(x⊔y)和F(y)⊑F(x⊔y),所以F(x⊔y)就是F(x)和F(y)的上界。

  3. 根据定义,F(x)⊔F(y)是F(x)和F(y)的最小上界。

  4. 所以F(x)⊔F(y)⊑F(x⊔y)。

结论:所以,MOP更准确。若F满足分配律,则迭代算法和MOP精确度一样 F(x⊔y)=F(x)⊔F(y)。一般,对于控制流的join/meet,是进行集合的交或并操作,则满足分配律。

10.常量传播 (constant propagation)

问题描述:在程序点p处的变量x,判断x是否一定指向常量值。

类别must分析,因为要考虑经过p点所有路径上,x的值必须都一样,才算作一定指向常量。

表示:CFG每个节点的OUT是pair(x, v)的集合,表示变量x是否指向常数v。

数据流分析框架(D, L, F)

(1)D:forward更直观

(2)L:lattice

变量值域:所有实数。must分析,所以\top是UNDEF未定义(unsafe),\perp是NAC非常量(safe)。

meet操作:must分析, \sqcap。在每个路径汇聚点PC,对流入的所有变量进行meet操作,但并非常见的交和并,所以不满足分配律

  • NACv=NACNAC \sqcap v = NAC

  • UNDEFv=vUNDEF \sqcap v = v 未初始化的变量不是我们分析的目标

  • cv=?cc=c c1c2=NACc \sqcap v = ? c \sqcap c = c \space c1 \sqcap c2 =NAC

(3)F转换函数

OUT[s] = gen U (IN[s] - {(x, _})

输出 = BB中新被赋值的 U 输入 - BB中相关变量值已经不是f常量的部分。

对所有的赋值语句进行分析(不是赋值语句则不管,用val(x)表示x指向的值):

(4)性质:不满足分配律

可以发现,MOP更准确。F(XY)F(X)F(Y)F(X \sqcap Y) \sqsubseteq F(X) \sqcap F(Y),但是是单调的。

11.Worklist算法

本质:对迭代算法进行优化,采用队列来存储需要处理的基本块,减少大量的冗余的计算。

上传的附件

发送私信

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

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