前言

第五、六节课是关于数据流分析理论的知识,比较抽象难懂,但是能够帮助我们更好地理解之前学习过的数据流分析应用,也能够为未来更加复杂的数据流分析应用奠定基础。

事实上,在听完第五节课后,我并没有立即写笔记。一方面是想让潜意识消化一下知识,另一方面吧,是因为之前读过的一篇论文的阅读笔记还欠着,哈哈。所以我先写了那篇论文的笔记,然后才轮到这篇。有意思的是,写笔记时再看到论文中的“backward data flow analysis”时,我终于能够理解这个词的意思——毕竟之前在南大课程中学过的“存活变量分析”也是一种backward data flow analyais。好!继续学习吧。

再看迭代求解算法

以may&forward analysis为例:

image-20230306112148922

下面从另一种视角来看这个算法:

给定一个有$k$个节点的CFG,迭代算法在每轮迭代中更新每个节点$n$的$OUT[n]$。假设该数据流分析中的值域为$V$,我们可以定义一个k-tuple来表示每次迭代分析后的结果:

$$ (OUT[n_{1}],\ OUT[n_{2}],\ …\ ,\ OUT[n_{k}]) $$

它是集合$(V_{1} \times V_{2}\ …\ \times V_{k})$中的一个元素,这个集合记做$V^{k}$。

每轮迭代可以视作从$V^{k}$中的一个元素到另一个新元素的映射,映射过程就是transfer functions和control-flow handling,我们将这个映射过程抽象为一个函数$F: V^{k} \rightarrow V^{k}$。

在上述抽象的基础上,may&forward analysis算法可以视作不断输出一系列的k-tuple,直到某个k-tuple与上一个k-tuple相同:

$$ iter\ i:\ (v_{1}^{i}, v_{2}^{i},\ …\ , v_{k}^{i}) = X_{i} = F(X_{i-1}) $$

$$ iter\ i+1:\ (v_{1}^{i+1}, v_{2}^{i+1},\ …\ , v_{k}^{i+1}) = X_{i+1} = F(X_{i}) $$

在这时,我们可以得到以下关系:

$$ X_{i} = X_{i+1} = F(X_{i}) $$

我们称满足$X = F(X)$的$X$是一个不动点(fixed point),并称上述迭代算法到达了一个不动点。

对于这样一种算法,我们提出三个问题:

  1. 这个算法能够保证一定能终止(到达不动点/有解)吗?
  2. 如果上一个问题的答案是肯定的,那么只有一个解/不动点吗?如果有多个不动点,哪一个是最好的、或者说最精确的?
  3. 什么时候这个算法能够到达不动点呢?

对于第一个问题,我们曾在《南大软件分析课程笔记|03 数据流分析应用》中简单回答过。这节课和下节课的知识将从数学的角度回答这些问题。本节课我们不会直接回答这些问题,而是先补充一些数学知识。

偏序(Partial Order)

首先是“偏序”的概念。我们将偏序集poset定义为$(P, \preccurlyeq)$,其中符号$\preccurlyeq$在集合$P$上定义了一个名为“偏序”的二元关系,该关系有以下特性:

$$ \forall\ x \in P, x \preccurlyeq x\ \ \text{(Reflexivity)} $$

$$ \forall\ x,y \in P, x \preccurlyeq y \wedge y \preccurlyeq x \Longrightarrow x = y \ \ \text{(Antisymmetry)} $$

$$ \forall\ x,y,z \in P, x \preccurlyeq y \wedge y \preccurlyeq z \Longrightarrow x \preccurlyeq z \ \ \text{(Transitivity)} $$

下面是一些poset的例子:

  • 若$S$表示一个由整数组成的集合,$\preccurlyeq$表示“小于或等于”,那么$(S, \preccurlyeq)$就是一个poset。
  • $S$表示一个由英文单词组成的集合,$\preccurlyeq$表示子串关系。
  • $S$表示$\lbrace a, b, c \rbrace$的幂集(power set),$\preccurlyeq$表示子集关系。

第三个集合的例子可以表示如下,后面我们会多次使用这种图形:

graph TD A("{a, b, c}") --> B("{a, b}") A --> C("{a, c}") A --> D("{b, c}") B --> E("{a}") C --> E D --> E B --> F("{b}") C --> F D --> F B --> G("{c}") C --> G D --> G E --> H("{ }") F --> H G --> H

其实,关于“偏序关系”的理解,个人认为知乎上的一个回答讲得不错:

  • 集合的包含关系是一种偏序。
  • 在整数集中定义偏序:若a能整除b,我们就记为a≺b。

显然它满足序公理。但整数集中,不是任何两个数都存在整除关系,这个关系是局部的(partial),太“偏颇”,于是被称为偏序

所谓“偏序”,有可能是翻译的问题(未求证)。Partial还有“局部的”之义——如果取这个意思,那就容易理解多了。或者说,偏序集中的元素是部分可比较的,不一定是所有元素都可以互相比较。

上界和下界(Upper/Lower Bounds)

了解完偏序的概念,接下来是在偏序集上定义的上界和下界的概念。

给定一个偏序集$(P, \preccurlyeq)$和它的子集$S$($S \subseteq P$),我们说$u \in P$是$S$的一个上界,当且仅当$\forall\ x \in S,\ x \preccurlyeq u$;类似地,$l \in P$是$S$的一个下界,当且仅当$\forall\ x \in S,\ l \preccurlyeq x$。

若$S$是由下图中绿色部分组成的集合,那么$\lbrace a, b, c \rbrace$就是$S$的上界,$\lbrace\ \rbrace$是$S$的下界:

graph TD A("{a, b, c}") --> B("{a, b}") A --> C("{a, c}") A --> D("{b, c}") B --> E("{a}") C --> E D --> E B --> F("{b}") C --> F D --> F B --> G("{c}") C --> G D --> G E --> H("{ }") F --> H G --> H style B fill:#11ee88 style C fill:#11ee88 style E fill:#11ee88 style F fill:#11ee88 style H fill:#11ee88

在此基础上,我们定义最小上界(叫做lub或join),记为$\lfloor \rfloor S$,对于$S$的每一个上界$u$,有$\lfloor \rfloor S \preccurlyeq u$;类似地,定义最大下界(叫做glb或meet),记为$\lceil \rceil S$,对于$S$的每一个下界$l$,有$l \preccurlyeq \lceil \rceil S$。

还是以集合为例,若$S$是由下图中绿色部分组成的集合,则$\lbrace a, b, c \rbrace$和$\lbrace a, b \rbrace$都是它的上界,后者还是最小上界;$\lbrace\ \rbrace$则是$S$的唯一下界,因此也是最大下界:

graph TD A("{a, b, c}") --> B("{a, b}") A --> C("{a, c}") A --> D("{b, c}") B --> E("{a}") C --> E D --> E B --> F("{b}") C --> F D --> F B --> G("{c}") C --> G D --> G E --> H("{ }") F --> H G --> H style B fill:#11ee88 style E fill:#11ee88 style F fill:#11ee88

若$S$只包含两个元素$a$和$b$,我们也可以将$\lfloor \rfloor S$写为$a \lfloor \rfloor b$,将$\lceil \rceil S$写为$a \lceil \rceil b$。

下面是关于上下界的两个特性:

  1. 不是所有的poset都有lub或glb。
  2. 如果一个poset有lub或glb,它一定是唯一的。这一点可以借助偏序关系的antisymmetry特点证明。

Lattice, Semilattice, Complete and Product Lattice

终于到格(lattice)的概念了!先说两句题外话:我发现写作时中英混用确实是比较舒服的,有的东西用中文表达会更加简洁清晰,有的东西用英文表达则会比较好,因为对应的中文翻译不一定能完全表达原词的意思。毕竟是写博客,比较自由,我也就不拘束于特定的表达了。

首先看一下格的定义:给定一个偏序集$(P, \preccurlyeq)$,$\forall\ a,b \in P$,如果$a \lfloor \rfloor b$和$a \lceil \rceil b$均存在,那么$(P, \preccurlyeq)$称为格。换句话说,一个偏序集是格,当且仅当其所有“元素对”构成的子集的最小上界和最大下界都存在。

接下来是半格(semilattice),它放宽了格的概念:如果$a \lfloor \rfloor b$存在,该偏序集就是一个join semilattice;如果$a \lceil \rceil b$存在,它就是一个meet semilattice。不必同时满足两个约束。

完全格(complete lattice)则在格的定义上加强了约束:对于给定偏序集$(P, \preccurlyeq)$,它的任意子集$S$的最小上界和最大下界都存在,则$(P, \preccurlyeq)$才能被称为完全格。幂集就是一种完全格。事实上,所有有限格(finite lattice,即$P$是有限集合)都是完全格。

每个完全格$(P, \preccurlyeq)$都有一个最大元素$\top = \lfloor \rfloor P$,称作top,一个最小元素$\bot = \lceil \rceil P$,称作bottom。

乘积格(Product Lattice)稍微复杂一些:给定一系列格$L_{1} = (P_{1}, \preccurlyeq_{1}), L_{2} = (P_{2}, \preccurlyeq_{2}),\ …\ , L_{n} = (P_{n}, \preccurlyeq_{n})$,如果对于所有$i$,$(P_{i}, \preccurlyeq_{i})$都有$\lfloor \rfloor _{i}$和$\lceil \rceil _{i}$,那么我们可以定义一个乘积格$L^{n} = (P, \preccurlyeq)$如下:

$$ P = P_{1} \times\ …\ \times P_{n} $$

$$ (x_{1},\ …\ , x_{n}) \preccurlyeq (y_{1},\ …\ , y_{n}) \Leftarrow \Rightarrow (x_{1} \preccurlyeq y_{1}) \wedge \ …\ \wedge (x_{n} \preccurlyeq y_{n}) $$

$$ (x_{1},\ …\ , x_{n})\ \lfloor \rfloor\ (y_{1},\ …\ , y_{n}) \Leftarrow \Rightarrow (x_{1} \lfloor \rfloor_{1} y_{1},\ …\ , x_{n} \lfloor \rfloor_{n} y_{n}) $$

$$ (x_{1},\ …\ , x_{n})\ \lceil \rceil\ (y_{1},\ …\ , y_{n}) \Leftarrow \Rightarrow (x_{1} \lceil \rceil_{1} y_{1},\ …\ , x_{n} \lceil \rceil_{n} y_{n}) $$

很容易证明,乘积格也是格,完全格构成的乘积格也是完全格。

基于格的数据流分析框架

现在,我们再次回到数据流分析上,定义一个基于格的数据流分析框架$(D, L, F)$:其中$D$指的是数据流的方向,包括前向和后向;$L$指的是由值域$V$和一个meet或join操作符构成的格;$F$指的是从$V$到$V$的一系列transfer functions。

实际上,数据流分析可以视作在格上不断迭代应用transfer functions和meet/join操作:

image-20230314192139922

单调性(Monotonicity)和不动点(Fixed Point)定理

在本课的最后一部分,我们来学习单调性和不动点定理。老规矩,首先看一下定义吧:

单调性

函数$f: L \rightarrow L$($L$是格)是单调的,当且仅当$\forall\ x,y \in L$,$x \preccurlyeq y \Longrightarrow f(x) \preccurlyeq f(y)$。

不动点定理

给定一个完全格$(L, \preccurlyeq)$,如果$f: L \rightarrow L$是单调的且$L$是有限的,那么:

  1. $f$的最小不动点可以通过以下方式得到:不断迭代计算$f(\bot), f(f(\bot)),\ …\ , f^{k}(\bot))$,直到到达一个不动点。
  2. $f$的最大不动点可以通过类似的方式得到:不断迭代计算$f(\top), f(f(\top)),\ …\ , f^{k}(\top))$,直到到达一个不动点。

如何证明不动点定理呢?我们可以分两步走:首先证明不动点的存在,继而证明按照前述方式找到的不动点是最小不动点。最小和最大不动点的证明是类似的,我们来看一下最小不动点的证明过程。

1. 证明不动点的存在

前面我们提到,最小元素$\bot = \lceil \rceil L$是格上的最小元素,且$f$是单调的,因此我们可以得到:

$$ \bot \preccurlyeq f(\bot) \preccurlyeq f^{2}(\bot) \preccurlyeq\ …\ f^{H}(\bot) $$

而$L$又是有限的,假设其高度为$H$,则上述数列的上限就是$f^{H}(\bot)$。当$i>H$时,根据鸽笼原理,存在$k$和$j$使得$f^{k}(\bot) = f^{j}(\bot)$,假设$k < j \leq H + 1$。结合$f$是单调的,又有$f^{k}(\bot) \preccurlyeq\ …\ \preccurlyeq f^{j}(\bot)$,因此可得$f^{Fix} = f^{k}(\bot) =\ …\ = f^{j}(\bot)$。故不动点存在。

注:格的高度的概念出现在下一节,指的是在格上从top到bottom的最长路径。

2. 证明该不动点是最小不动点

这里我们使用归纳法证明:

  1. 假设还有一个不动点$x$,使得$x = f(x)$。由于$\bot$是最小元素,结合函数单调性,可得$f(\bot) \preccurlyeq f(x)$。
  2. 假设$f^{i}(\bot) \preccurlyeq f^{i}(x)$,那么结合函数单调性,我们有$f^{i+1}(\bot) \preccurlyeq f^{i+1}(x)$。
  3. 因此,我们得证$f^{i}(\bot) \preccurlyeq f^{i}(x)$。又因为$x$是不动点,故$f^{i}(\bot) \preccurlyeq f^{i}(x) = x$。
  4. 最终有$f^{Fix} = f^{k}(\bot) \preccurlyeq f^{k}(x) = x$,证毕。

总结与思考

本节课,我们学习了偏序、格、格上的函数单调性和不动点定理等重要知识。关于数据流分析的迭代算法,我们提出了三个问题,但是本节课并未直接回答这三个问题,因为我们尚未将数据流分析算法和不动点定理关联起来,这些将是下节课的内容。

学习之余,我还看了李樾老师在南大的一堂SICP课的后半节课的视频,主题是“大学除了专业知识,还应该学些什么?”。李樾老师讲得非常好,可以看出是一位拥有人文情怀的老师。

今天连续输出了两篇文章,另一篇ELOISE论文笔记算是填之前留下的坑,但是这些东西真的很有意思。好,那么就继续探索吧。