P5-6
2021-04-28 14:54:57 1 举报AI智能生成
南大软件分析P5
作者其他创作
大纲/内容
以另一种方式来看迭代算法
如何看待
给定一个具有k个节点的CFG（程序），迭代算法将在每次迭代中为每个节点n更新OUT [n]。
假设数据流分析中值的域为V，那么我们可以定义一个k元组。
(OUT[n1], OUT[n2], …, OUT[nk])
Vk表示为的集合（V1×V2…×Vk）的一个元素值，以保存每次迭代后的分析值。
（注：元素值Vk中的k应该在V的右上角，表示值域V上的k元组）
(OUT[n1], OUT[n2], …, OUT[nk])
Vk表示为的集合（V1×V2…×Vk）的一个元素值，以保存每次迭代后的分析值。
（注：元素值Vk中的k应该在V的右上角，表示值域V上的k元组）
通过应用传递函数和控制流处理（抽象为函数F），可以将每次迭代视为将Vk的元素值映射到Vk的新元素值的函数F：Vk→Vk
然后，该算法迭代输出一系列k元组，直到两个连续迭代中前一个k元组与后一个相同为止。
迭代过程
如果X = F（X），则X是函数F的不动点
上图的迭代过程中，就到达了一个不动点Xi
思考
迭代算法（或IN/OUT方程系统）为数据流分析提供了一个解决方案。
（1）是否保证算法可以终止或到达固定点，或者始终有解决方案？
（2）如果是这样，是否只有一种解决方案或只有一个固定点？
如果解决方案不止一个，那么我们的解决方案是最好的（最精确的）吗？
（3）算法何时会达到固定点，或者何时才能获得解决方案？
（2）如果是这样，是否只有一种解决方案或只有一个固定点？
如果解决方案不止一个，那么我们的解决方案是最好的（最精确的）吗？
（3）算法何时会达到固定点，或者何时才能获得解决方案？
要回答这些问题，需要先学习一些数学知识。
Partial Order（偏序）
定义
我们将偏序集poset定义为一对（P，⊑），其中⊑是二进制关系，
它定义了P上的偏序，并且具有以下属性：
它定义了P上的偏序，并且具有以下属性：
例子1
例子2
例子3
partial意味着，P中的一对元素值可能是没有⊑关系的（incomparable），
换句话说，不必每对set元素都必须满足顺序⊑，
例如，例子3中的字符串sin和pin之间就不存在子字符串的关系。
换句话说，不必每对set元素都必须满足顺序⊑，
例如，例子3中的字符串sin和pin之间就不存在子字符串的关系。
例子4
partial -> incomparable：{a}和{b}之间也不存在子集关系。
Upper and Lower Bounds（上界和下界）
定义
上界、下界
给定一个偏序集poset(P,⊑),且S⊆P，
如果对u∈P，∀x∈S，有x⊑u，我们说u是S的上界（upper bound）。
如果对l∈P，∀x∈S，l⊑x，则是S的下界（lower bound）。
如果对u∈P，∀x∈S，有x⊑u，我们说u是S的上界（upper bound）。
如果对l∈P，∀x∈S，l⊑x，则是S的下界（lower bound）。
最小上界、最大下界
我们定义S的最小上界（lub或join），写为⊔S。对于S的每个上界u，有⊔S⊑u。
我们定义S的最大下界（glb或meet），写为⊓S，对于S的每个下界l，有l⊑⊓S。
我们定义S的最大下界（glb或meet），写为⊓S，对于S的每个下界l，有l⊑⊓S。
通常，如果S仅包含两个元素a和b（S = {a，b}），则
⊔S可以写成a⊔b（a和b的join），
⊓S可以写成a⊓b（a和b的meet）。
⊔S可以写成a⊔b（a和b的join），
⊓S可以写成a⊓b（a和b的meet）。
一些属性
（1）不是每个偏序集poset都有lub或glb
（2）但是，如果poset有lub或glb，那么lub和glb将是唯一的
（2）的证明
Lattice, Semilattice, Complete and Product Lattice
Lattice
定义
给定一个偏序集poset（P，⊑），∀a，b∈P，
如果a⊔b和a⊓b存在，则（P，⊑）称为lattice
如果a⊔b和a⊓b存在，则（P，⊑）称为lattice
即，如果poset的每对元素都具有最小的上界和最大的下界，则偏序集poset是一个lattice
lattice就是一个poset，是一个特殊的poset
例子1
例子2
例子3
从上面的例子可以看到，a⊔b操作得到的一定是最小上界，而不是其他的更大的上界。⊓同理。
Semilattice
也即，对于poset中任意的一对元素值，只存在最小上界和最大下界，不存在其他更大的上界和更小的下界。
Complete Lattice
也即，对于poset中任意的一组元素值（子集），最小下界和最大上界都存在。
例子1
例子2
性质
注意：lattice可以是无限的偏序集，因为从定义可知，最小上界和最大下界是针对无限集中的任意两个元素值而言的。
Product Lattice
定义
性质
Data Flow Analysis Framework via Lattice
一个数据流框架 (D, L, F) 由以下3部分组成：
（1）D：数据流的方向：正向、反向，
（2）L：包含值的V域和⊔（join）、⊓（meet）操作符的lattice，
（3）F：一组从域V到域V的转换函数。
（1）D：数据流的方向：正向、反向，
（2）L：包含值的V域和⊔（join）、⊓（meet）操作符的lattice，
（3）F：一组从域V到域V的转换函数。
数据流分析可以看作是迭代地应用传递函数，以及对lattice的值进行join/meet运算
Monotonicity and Fixed Point Theorem
回顾“以另一种方式来看迭代算法”中思考的3个问题
Monotonicity（单调性）
定义
Fixed-Point Theorem（不动点定理）
定义
两个证明
不动点的存在性
不动点是最小（最大）的
不动点是最大的的证明同上
把迭代算法和不动点定理关联起来
如上所示的是lattice上函数的属性（不动点定理）。 我们不能说迭代算法也具有该特性，除非我们可以将迭代算法与不动点定理联系起来。
将迭代算法和不动点定理联系起来
如果product lattice Lk中的k个lattice都是complete和finite的，即(L,L,...,L)，
则Lk也是complete和finite的。
则Lk也是complete和finite的。
在每次迭代中，都等同于认为我们应用了函数F，该函数由
（1）传递函数fi：每个节点的 L→L
（2）join / meet函数⊔/⊓：L×L→L 用于控制流汇合
（1）传递函数fi：每个节点的 L→L
（2）join / meet函数⊔/⊓：L×L→L 用于控制流汇合
证明函数F是单调的
基于（1）迭代算法和不动点定理是能够联系起来的，（2）函数F是单调的，则，不动点定理能够应用在数据流分析的迭代算法上。
目前三个问题只剩下一个问题
迭代算法什么时候会到达不动点
#iterations的最坏情况：CFG中lattice的高度与节点数的乘积
May/Must Analysis, A Lattice View
MOP and Distributivity
Meet-Over-All-Paths Solution (MOP)
Ours (Iterative Algorithm) vs. MOP
Bit-vector或者Gen/Kill问题（给join/meet分别设置为并/交）是可分配的（分布式的）。
但是也有一些分析不是分布式的。
Constant Propagation
Lattice
未初始化变量不是我们常量传播分析的重点
在每条路径汇合的PC上，我们都应对该PC上传入数据流值中的所有变量应用“ meet”
Transfer Function
Nondistributivity
Worklist Algorithm
工作列表算法是迭代算法的一种优化
0 条评论
下一页
