首页  思维导图  详情



 



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元组）

通过应用传递函数和控制流处理（抽象为函数F），可以将每次迭代视为将Vk的元素值映射到Vk的新元素值的函数F：Vk→Vk

然后，该算法迭代输出一系列k元组，直到两个连续迭代中前一个k元组与后一个相同为止。

迭代过程

如果X = F（X），则X是函数F的不动点

上图的迭代过程中，就到达了一个不动点Xi

思考

迭代算法（或IN/OUT方程系统）为数据流分析提供了一个解决方案。

（1）是否保证算法可以终止或到达固定点，或者始终有解决方案？ （2）如果是这样，是否只有一种解决方案或只有一个固定点？ 如果解决方案不止一个，那么我们的解决方案是最好的（最精确的）吗？ （3）算法何时会达到固定点，或者何时才能获得解决方案？

要回答这些问题，需要先学习一些数学知识。

Partial Order（偏序）

定义

我们将偏序集poset定义为一对（P，⊑），其中⊑是二进制关系， 它定义了P上的偏序，并且具有以下属性：

例子1

例子2

例子3

partial意味着，P中的一对元素值可能是没有⊑关系的（incomparable）， 换句话说，不必每对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）。

最小上界、最大下界

我们定义S的最小上界（lub或join），写为⊔S。对于S的每个上界u，有⊔S⊑u。 我们定义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）。

一些属性

（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

即，如果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的转换函数。

数据流分析可以看作是迭代地应用传递函数，以及对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的。

在每次迭代中，都等同于认为我们应用了函数F，该函数由 （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

工作列表算法是迭代算法的一种优化

 收藏

立即使用

P15

 收藏

立即使用

P14

 收藏

立即使用

P16

 收藏

立即使用

czgggggggg

职业：研究生

去主页

 Collect

Get Started

Information flow between Oracle Projects and Primavera P6 v8

 Collect

Get Started

我-p2p

 Collect

Get Started

p5_client_init_workflow

 Collect

Get Started

p2p投资





0 条评论

下一页