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

roger

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

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

目录：

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[n]。

定义2：设数据流分析的值域是V，可定义一个k-元组：(OUT[n1], OUT[n2], ... , OUT[nk])。是集合 (V1

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

V2 ...

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

Vk) （幂集，记为Vk）的一个元素，表示每次迭代后k个节点整体的值。

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

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

Vk。

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

（2）图示

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

4-1-迭代算法数学化.png

不动点：当Xi = F(Xi)时，就是不动点。

问题：

·迭代算法是否一定会停止（到达不动点）？·迭代算法如果会终止，会得到几个解（几个不动点）？·迭代几次会得到解（到达不动点）？

2.偏序（Partial Order）

定义：给定偏序集(P,

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

)，

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

是集合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是整数集，

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

表示

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

，是偏序集；若

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

表示<，则显然不是偏序集。·P是英文单词集合，

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

表示子串关系（可以存在两个元素不具有偏序关系，不可比性），是偏序集。

3.上下界（Upper and Lower Bounds）（1）定义

定义：给定偏序集(P,

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

)，且有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—数据流分析基础（课时5...

4-3-1-上下确界示例.png（3）特性

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

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

4-3-2-无下确界.png

·如果存在上下确界，则是唯一的。利用传递性和反证法即可证明。

4.格（Lattice），（半格）Semilattice，全格，格点积（Complete and Product Lattice）

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

（1）格

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

例子：

·(S, ⊑)中S是整数子集，

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

是

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

，是格点；·(S, ⊑)中S是英文单词集，

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

表示子串关系，不是格点，因为单词pin和sin就没有上确界；·(S, ⊑)中S是{a, b, c}的幂集，

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

表示

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

子集，是格点。

（2）半格

定义：给定一个偏序集(P,⊑)，∀a,b∈P：当且仅当a⊔b存在（上确界），该偏序集叫做 join semilatice；

当且仅当a⊓b存在（下确界），该偏序集叫做 meet semilatice

（3）全格

定义：对于格点 (S,

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

) （前提是格点）的任意子集S，⊔S

　　上确界和⊓S下确界都存在，则为全格complete lattice。

例子：

·P是整数集，

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

是

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

，不是全格，因为P的子集正整数集没有上确界。·(S, ⊑)中S是{a, b, c}的幂集，

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

表示

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

子集，是全格。

符号：

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

=

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

P ，叫做top；

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

=

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

P，叫做bottom。

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

（4）格点积

定义：给定一组格，L1=(P1,

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

1)，L2=(P2,

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

2)，... ，Ln=(Pn,

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

n)，都有上确界

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

i和下确界

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

i，，则定义格点积 Ln = (P,

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

)：

1.P = P1

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

...

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

Pn2.(x1, ... xn)

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

(y1, ... yn)

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

(x1

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

y1)

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

...

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

(xn

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

yn)3.(x1, ... xn)

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

(y1, ... yn) = (x1

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

y1, ..., xn

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

yn)4.(x1, ... xn)

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

(y1, ... yn) = (x1

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

y1, ..., xn

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

yn)

性质：格点积也是格点；格点都是全格，则格点积也是全格。

5.数据流分析框架（via Lattice）

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

·D—方向·L—格点（值域V，meet

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

或 join

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

操作）·F—转换规则V

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

V。

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

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

目标问题：迭代算法一定会停止（到达不动点）吗？

（1）单调性

定义：函数f: L

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

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,

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

)，是有限的，单调的。

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

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

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

/ meet

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

操作，分叉是拷贝操作）。

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—数据流分析基础（课时5...

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—数据流分析基础（课时5...

4-8-1-must_may分析特点.png（1）may分析

以 Reaching Definitions分析为例：

1.从

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

开始，

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

表示所有定义都不可达，是不安全的结果（因为这个分析的应用目的是为了查错，查看变量是否需要初始化。首先在Entry中给每个变量一个假定义，标记所有变量为都为未初始化状态，

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

表示所有的假定义都无法到达，说明所有变量在中间都进行了赋值，那就不需要对任何变量进行初始化，这是不安全的，可能导致未初始化错误）。2.

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

表示所有Entry中的假定义都可达，从查错角度来说，需要对每个变量都进行初始化，非常安全！但是这句话没有用，我都要初始化的话还做这个分析干嘛？3.Truth：表明最准确的验证结果，假设{a,c}是truth，那么包括其以上的都是safe的，以下的都是unsafe，就是上图的阴影和非阴影。

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

4-8-2-Truth示例.png

4.从

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

到

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

，得到的最小不动点最准确，离Truth最近。上面还有多个不动点，越往上越不准。

（2）must分析

以available expressions分析为例：

1.从

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

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

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

表示没有表达式可用，都不需要优化，很安全！但没有用。3.从

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

到

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

，就是从不安全到安全，存在一个Truth，代表准确的结果。4.从

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

到

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

，达到一个最大不动点，离truth最近的最优解。

迭代算法转化到lattice上，may/must分析分别初始化为最小值

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

和最大值

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

，最后求最小上界/最大下界。

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—数据流分析基础（课时5...

4-9-1-MOP公式.png

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

（2）MOP vs 迭代算法

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

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：lattice

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

4-10-1-UNDEF_NAC.png

变量值域：所有实数。must分析，所以

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

是UNDEF未定义（unsafe），

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

是NAC非常量（safe）。

meet操作：must分析，

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

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

·NAC

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

v = NAC·UNDEF

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

v = v 未初始化的变量不是我们分析的目标。·c

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

v = ? c

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

c = c c1

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

c2 =NAC

（3）F转换函数

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

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

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

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

4-10-2-赋值语句操作.png

（4）性质：不满足分配律

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

4-10-3-不满足分配律.png

可以发现，MOP更准确。F(X

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

Y)

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

F(X)

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

F(Y)，但是是单调的。

11.Worklist算法

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

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

4-11-worklist.png参考

软件分析——数据流分析2[2]

References

[1] zcc: https://blog.csdn.net/hahahaqwe123[2] 软件分析——数据流分析2: https://blog.csdn.net/hahahaqwe123/article/details/105875141

---