【课程笔记】南大软件分析课程4—数据流分析基础（课时5...
关于这一节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）和MOP10.常量传播11.Worklist算法重点：上节课是介绍了3种数据流分析迭代算法，本节课将从数学理论的角度来讨论数据流分析，加深对数据流分析算法的理解。1.迭代算法-另一个角度本质：常见的数据流迭代算法，目的是通过迭代计算，最终得到一个稳定的不变的解。（1）理论定义1：给定有k个节点（基本块）的CFG，迭代算法就是在每次迭代时，更新每个节点n的OUT。定义2：设数据流分析的值域是V，可定义一个k-元组：(OUT, OUT, ... , OUT)。是集合 (V1V2 ...Vk) （幂集，记为Vk）的一个元素，表示每次迭代后k个节点整体的值。定义3：每一次迭代可看作是Vk映射到新的Vk，通过转换规则和控制流来映射，记作函数F：VkVk。迭代算法本质：通过不断迭代，直到相邻两次迭代的k-元组值一样，算法结束。（2）图示4-1-迭代算法数学化.png不动点：当Xi = F(Xi)时，就是不动点。问题：·迭代算法是否一定会停止（到达不动点）？·迭代算法如果会终止，会得到几个解（几个不动点）？·迭代几次会得到解（到达不动点）？2.偏序（Partial Order）定义：给定偏序集(P, )，是集合P上的二元关系，若满足以下性质则为偏序集：·∀x∈P,x⊑x 自反性Reflexivity·∀x,y∈P, x⊑y∧y⊑x ⇒ x=y 对称性Antisymmetry·∀x,y∈P, x⊑y∧y⊑z ⇒ x⊑z 传递性Transitivity例子：·P是整数集，表示，是偏序集；若表示<，则显然不是偏序集。·P是英文单词集合，表示子串关系（可以存在两个元素不具有偏序关系，不可比性），是偏序集。3.上下界（Upper and Lower Bounds）（1）定义定义：给定偏序集(P, )，且有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。4-3-1-上下确界示例.png（3）特性·并非每个偏序集都有上下确界。4-3-2-无下确界.png·如果存在上下确界，则是唯一的。利用传递性和反证法即可证明。4.格（Lattice），（半格）Semilattice，全格，格点积（Complete and Product Lattice）都是基于上下确界来定义的。（1）格定义：给定一个偏序集(P,⊑)，∀a,b∈P，如果存在a⊔b和a⊓b，那么就称该偏序集为格。偏序集中的任意两个元素构成的集合均存在最小上界和最大下界，那么该偏序集就是格。例子：·(S, ⊑)中S是整数子集，是，是格点；·(S, ⊑)中S是英文单词集，表示子串关系，不是格点，因为单词pin和sin就没有上确界；·(S, ⊑)中S是{a, b, c}的幂集，表示子集，是格点。（2）半格定义：给定一个偏序集(P,⊑)，∀a,b∈P：当且仅当a⊔b存在（上确界），该偏序集叫做 join semilatice；当且仅当a⊓b存在（下确界），该偏序集叫做 meet semilatice（3）全格定义：对于格点 (S, ) （前提是格点）的任意子集S，⊔S 上确界和⊓S下确界都存在，则为全格complete lattice。
例子：·P是整数集，是，不是全格，因为P的子集正整数集没有上确界。·(S, ⊑)中S是{a, b, c}的幂集，表示子集，是全格。符号： = P ，叫做top； = P，叫做bottom。性质：有穷的格点必然是complete lattice。全格一定有穷吗？不一定，如实数界。（4）格点积定义：给定一组格，L1=(P1, 1)，L2=(P2, 2)，... ，Ln=(Pn, n)，都有上确界i和下确界i，，则定义格点积 Ln = (P, )：1.P = P1...Pn2.(x1, ... xn)(y1, ... yn)(x1y1)...(xnyn)3.(x1, ... xn)(y1, ... yn) = (x1y1, ..., xnyn)4.(x1, ... xn)(y1, ... yn) = (x1y1, ..., xnyn)性质：格点积也是格点；格点都是全格，则格点积也是全格。5.数据流分析框架（via Lattice）数据流分析框架(D, L, F) ：·D—方向·L—格点（值域V，meet或 join操作）·F—转换规则VV。数据流分析可以看做是迭代算法对格点 利用转换规则和 meet/join操作。6.单调性与不动点定理（Monotonicity and Fixed Point Theorem）目标问题：迭代算法一定会停止（到达不动点）吗？（1）单调性定义：函数f: LL，满足∀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, )，是有限的，单调的。4-7-1-迭代算法.png（1）完全lattice证明根据第5小节，迭代算法每个节点（基本块）的值域相当于一个lattice，每次迭代的k个基本块的值域就是一个k-元组。k-元组可看作lattice积，根据格点积性质：若L^k^中每一个lattice都是完全的，则Lk也是完全的。（2）L是有限的迭代算法中，值域是0/1，是有限的，则lattice有限，则Lk也有限。（3）F是单调的函数F：BB中转换函数fi：L → L + BB分支之间的控制流影响（汇聚是join/ meet操作，分叉是拷贝操作）。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之间最长的路径。4-7-3-lattice高度定义.png最坏情况迭代次数：设有n个块，每次迭代只有1个BB的OUT/IN值的其中1位发生变化（则从top→bottom这1位都变化），则最多迭 (n × h) 次。8.从lattice的角度看may/must分析说明：may 和 must 分析算法都是从不安全到安全（是否安全取决于safe-aprroximate过程），从准确到不准确。4-8-1-must_may分析特点.png（1）may分析以 Reaching Definitions分析为例：1.从开始，表示所有定义都不可达，是不安全的结果（因为这个分析的应用目的是为了查错，查看变量是否需要初始化。首先在Entry中给每个变量一个假定义，标记所有变量为都为未初始化状态，表示所有的假定义都无法到达，说明所有变量在中间都进行了赋值，那就不需要对任何变量进行初始化，这是不安全的，可能导致未初始化错误）。2.表示所有Entry中的假定义都可达，从查错角度来说，需要对每个变量都进行初始化，非常安全！但是这句话没有用，我都要初始化的话还做这个分析干嘛？3.Truth：表明最准确的验证结果，假设{a,c}是truth，那么包括其以上的都是safe的，以下的都是unsafe，就是上图的阴影和非阴影。4-8-2-Truth示例.png4.从到，得到的最小不动点最准确，离Truth最近。上面还有多个不动点，越往上越不准。（2）must分析以available expressions分析为例：1.从开始，表示所有表达式可用。如果用在表达式计算优化中，那么有很多已经被重定义的表达式也被优化了（实际上不能被优化），那么该优化就是错误的，不安全！2.表示没有表达式可用，都不需要优化，很安全！但没有用。3.从到，就是从不安全到安全，存在一个Truth，代表准确的结果。4.从到，达到一个最大不动点，离truth最近的最优解。迭代算法转化到lattice上，may/must分析分别初始化为最小值和最大值，最后求最小上界/最大下界。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操作。本质—求这些值的最小上界/最大下界。4-9-1-MOP公式.pngMOP准确性：有些路径不会被执行，所以不准确；若路径包含循环，或者路径爆炸，所以实操性不高，只能作为理论的一种衡量方式。（2）MOP vs 迭代算法4-9-2-MOP与迭代算法比较.png对于以上的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：lattice4-10-1-UNDEF_NAC.png变量值域：所有实数。must分析，所以是UNDEF未定义（unsafe），是NAC非常量（safe）。meet操作：must分析， 。在每个路径汇聚点PC，对流入的所有变量进行meet操作，但并非常见的交和并，所以不满足分配律。·NACv = NAC·UNDEFv = v 未初始化的变量不是我们分析的目标。·cv = ? cc = c c1c2 =NAC（3）F转换函数OUT = gen U (IN - {(x, _})输出 = BB中新被赋值的 U 输入 - BB中相关变量值已经不是f常量的部分。对所有的赋值语句进行分析（不是赋值语句则不管，用val(x)表示x指向的值）：4-10-2-赋值语句操作.png（4）性质：不满足分配律4-10-3-不满足分配律.png可以发现，MOP更准确。F(XY)F(X)F(Y)，但是是单调的。11.Worklist算法本质：对迭代算法进行优化，采用队列来存储需要处理的基本块，减少大量的冗余的计算。4-11-worklist.png参考软件分析——数据流分析2References zcc: https://blog.csdn.net/hahahaqwe123 软件分析——数据流分析2: https://blog.csdn.net/hahahaqwe123/article/details/105875141
页:
[1]