视频： 南京大学《软件分析》课程 06（Data Flow Analysis - Foundations II 课程主页：Static Program Analysis | Tai-e (pascal-lab.net) 笔记参考：(34条消息) 软件分析——数据流分析2_zcc今天好好学习了吗的博客-CSDN博客 (33条消息) 【课程笔记】南大软件分析课程—16课时完整版_bsauce的博客-CSDN博客_南京大学软件分析笔记 PPT： https://cs.nju.edu.cn/tiantan/software-analysis/DFA-FD.pdf

将不动点定理应用于算法

第 5 节课向我们介绍了不动点定理：完全 lattice 且是单调的、有限的，那么存在不动点且从⊤开始迭代找得到最大不动点和从⊥开始迭代找得到最小不动点；现在的问题是：如何关联迭代算法和不动点理论（那么就能证明算法解存在、且最优） image. png 依据不动点定理的条件，我们只需要证明 CFG 是个 complete lattice + 证明转移函数是单调的。

  • 因为每一个 $v_i$ 都是 complete&finite lattices 那么，他们的笛卡尔积得到的 product lattice 也是 complete&finite 的（lattice 的性质）
  • 转移函数有两步：第一步对每个 node 应用转移函数，第二步是进行 join 或 meet 处理。
    • 第一步的转移函数中就是 gen 和 kill 操作，而 gen 和 kill 操作是固定的，结果只能是 0 变成 1 或者 1 变成 1，显然单调。
      • 这里我琢磨了好久，要注意的是这里的转移函数是每次迭代的转移函数，而不是 BBs 之间的转移函数。BBs 之间转移函数的时候是可能将上一个 BB 位向量中的 1 kill 为 0，此时比较的是上一个 BB 和当前 BB 的位向量；但是在迭代层面我们去比较的是当前 BB 在上一次迭代和这次迭代的位向量，因为 gen 和 kill 操作是固定的，结果只能是 0 变成 1 或者 1 变成 1，所以是单调的。
    • 第二步需要分别证明 join 和 meet 是单调的
      • image.png
      • Meet 证明方法同上

至此，我们将不动点定理与我们的算法联系起来了，迭代算法是可以终止的（到达不动点），并且不动点是最小或者最大不动点 下面来解答第三个问题，算法什么时候达到不动点（复杂度问题）

迭代算法的复杂度

Lattice 的高度（深度）

Top 到 Bottom 最长的路径 image.png 那么可以说 lattice 的深度最长的情况就是 BB 中 node 的个数（变量的个数）

最坏的迭代次数

最坏的情况就是每次迭代只会改变位向量中的一位，并且不动点在位向量全为 1 处，所以最坏的迭代次数就是 h * k 次（这里存疑）。

  • 关于最坏迭代次数那里，h * k 理解不了啊，我觉得最坏就是 h 吧。就拿老师的那个例子来说最坏应该是 3x3=9，但是迭代不应该是空到第一层然后第二层然后第三层一共 3 次吗，如果非要 9 次的话，空到第一层还又要回到空，然后空到第一层另外的两个，这是 3 次，然后第一层到第二层和第二层到第三层同理一共 9 次。感觉这个 9 次不对吧。

从 lattice 的角度来看 may 和 must 分析

(关于 may 和 must 分析可以看一下数据流分析 1）

  • may analysis：输出的信息可能是正确的（也有可能是错误的），所以是过近似的分析
  • must analysis：输出的信息一定是正确的，所以是欠近似分析

选择 may 或者 must 分析都是为了分析结果的安全性（注意是安全性而不是正确性） 我个人的理解就是：

  • may 分析就像是或操作，但凡只有 1 条路径是满足我分析要求的，may 分析就为真。
    • 比如可达性分析的应用——查看哪个变量没有初始化，只要有一条路径没有初始化，那么我的输出就是真，此时输出的信息不完全正确，因为其他路径对变量初始化了，但是这样的分析结果是安全的，因为不能存在没有初始化的变量
  • Must 分析就像是与操作，必须所有路径都满足我分析的要求，才是真
    • 比如 available 表达式的分析的应用——将表达式最后的执行结果保存方便后续的使用（不用每次都计算表达式），这就要求每一条路径都是 available，所以需要每一条路都为真，那么最后的结果才是真。
  • 注意 may 和 must 分析需要针对具体案例具体分析，有的时候正确性和安全性其实是矛盾的。

首先，无论是 may 还是 must 分析，都是从不安全的状态逐渐迭代到安全的状态（不动点），而且相反的是从准确的状态到不准确的状态。

May 分析（以可达性分析举例）

image.png 就像这个图显示的一样，bottom 表示没有定义可达（意思就是变量在所有的路径都初始化了），显然这样的结果是不安全的，但是精度（正确性）是最高的，因为输出的结果是“每条路径都没有定义可达”。 而 top 表示所有的定义都有可能可达，这样的结果是安全的，但是精度最低，因为这句话就是个废话。比如你在分析变量是否都被初始化，输出的结果是变量可能被初始化也可能没有被初始化。（注意这里的安全和精度是针对你的分析结论，而不是分析的那个程序。） Bottom 和 top 都不是我们想要的结果，所以引入一个概念 truth 来划分 safe 和 unsafe - 这里说一下我对 truth 的理解，老师说 truth 表示的是程序对所有输入的动态输出的集合，那么可以理解为这个椭圆里面的 lattices 并不是全是真实的 lattices，只是一个 lattices 的取值空间，实际上对应到分析的程序而言，输出得到的 lattices 的集合在这个椭圆（取值空间）中的点，我们称之为 truth，以此为边界，划分了 safe 和 unsafe。 - 同时老师也提到了为什么我们分析一定是 safe 的呢，是因为我们在 cfg 中依据 BBs 中的指令设计的转移函数就是 safe 的。

Ok，现在我们知道了这个椭圆从下到上从不安全而准确逐渐变化为安全而准确，并且我们的分析得到的不动点也在安全区，那么对于众多的不动点，我们选择那个最准确的，也就是最靠近 bottom 的——最小不动点。而我们的迭代算法得到的恰好就是这个最小不动点。

Must 分析（以available expressions分析为例）

image.png 分析同上，不再赘述 ## 从“最小步伐”的角度来简要证明最小/最大不动点 将迭代算法转换到 lattice 上，考虑到了 f : L → L ，这个函数本质上就是算法中的转换函数和 join/mmet 操作构成的。 - 转换函数实际上是固定的，只要 BB 确定，那么其 kill 和 gen 是固定的，所以在 lattice 上走的步数是确定的 - join/mmet：lattice 上就是求两个值的最小上界/最大下界，那么其走的步数也是最小的

=> 所以，函数在 lattice 上是走的最小步数，那么得到的不动点一定是离出发点最近的（从 bottom 出发就是最小不动点，从 top 出发就是最大不动点）

MOP

Meet-over-all-paths solution （是衡量精度的） image.png MOP 就是将 entry 到某个 BB 的所有路径的转移函数合为一个整体函数 $F_P$，$MOP[S_i]=\cup /\cap F_p(OUT[Entry])$ MOP 是有如下几个特点 image.png

  • Not executable 就是有的路径实际上是不会被执行的，因为在分析的时候会有一些冗余的路径，所以就导致了 MOP 实际上不是很准确
  • 同时因为要遍历所有的路径，所以它是没有边界的（unbounded），而且如果程序很大还会有路径爆炸的问题，所以它又是不可枚举的（not enumerable），所以它难以操作

综上，MOP 这个方法可能不准确，实际操作性不高，是理论上的一个衡量方式。

将 MOP 和我们迭代算法进行比较来更好的理解 MOP

image.png 对于以上的这个例子 迭代算法： $IN[S_4​]=fS_3​​(fS_1​​(OUT[entry])\cup fS_2​​(OUT[entry]))$ MOP: $IN[S_4​]=fS_3​​(fS_1​​(OUT[entry]))\cup fS_3​​(fS_2​(OUT[entry]))$ 所以迭代算法和 MOP 的计算区别在于： 迭代算法是：$F(x\cup y)$ MOP 是：$F(x)\cup F(y)$ 我们可以来证明一下这两种方式哪种更精准： ![image.png](https://gitee.com/juhuahua/chart-bed/raw/master/20230202184735.png) 迭代算法的结果是 MOP 结果的上界，说明 MOP 更精准些，但是如果函数 F 满足分配律（distributive）那么两者就会相等，精准度是一样的。而我们迭代算法中的 bit-vector（位向量）或者是 gen/kill 问题（对于 join/meet 是进行集合的交或并操作）是满足分配律的。 接下来要讲一个不是 distributive 的算法 # Constant propagation 常量传播 定义：给定一个变量 x 在程序点 p，判断是否在 p 时，x 能确保有个常量 显然这是个 must 分析 对于产量传播的分析中，CFG 中每个 node 的 OUT 都是一个 pairs（x, v），x 表示变量，v 表示 node 之后 x 的值。 接下来我们看看对于这个分析，它的数据流框架（D，L，F）（方向，lattices，转移函数）是什么。 ## 方向 forwards ## Lattice image.png 如果是 must 分析，那么就是从上到下迭代，UNDEF（undefined） 到 NAC（not a constant）是从不安全且高精度到安全低精度。UBDEF 表示变量都还没有定义，NAC 表示没有一个是常量。中间的数字表示变量值可以是任何一个实数。 在这个 lattice 上的 meet 操作也有些许的不同： image.png ## 转移函数 $F:OUT[s]=gen \cup (IN[s]-\{(x, \_ )\})$ Gen 的规则如下： image.png （val (x) 表示取变量 x 的值) 现在我们 D，L，F 都明确了，我们来看一看为啥说常量传播是不满足分配率的。

不满足分配率

如下例所示 image.png

Worklist Algorithm

实际分析中其实是不会用迭代算法的，worklist algorithm 是对迭代算法的优化。 优化点：迭代算法中只要有一个 node 的 out 发生变化，那么我们就会重新计算全部的 note 的 out，但是其实有很大一部分的 node 的 out 已经达到不动点，所以 worklist 算法的优化就是将 out 发生变化的 node 的后继 node 放入 worklist，算法每次只计算 worklist 数组中的 node 的 out。 image.png

总结

最后我们来梳理一遍第六节课的内容。

  • 首先我们想要知道我们的迭代算法是否可以达到不动点，并且达到的不动点是不是最优的，所以我们得看迭代算法是否满足不动点定理的条件
    • 有限
    • 单调
  • 接下来我们讨论了迭代算法的复杂度，知道了最坏的迭代次数
  • 然后我们从 lattice 的角度重新审视了 may 和 must 分析，这里的两个图非常直观明了。
  • 接着我们用 MOP 来衡量了一下迭代算法的精度
    • 指出了满足分配律的转移函数的算法的精度和 MOP 一样
    • 同时也介绍了一种不满足分配律的分析
  • 最后给出了迭代算法的优化。