整点抽象的

下面默认 $x\le y$ 意味着 $x$ 比 $y$ 更精确，$y$ 比 $x$ 更保守。

Galois connection

说的是这么一件事情：

如果给定了

1. 程序的语义 $f_{s}$ 和所有可能的执行状态 $\Sigma_s=\Set{\sigma_s}$
2. 分析的语义 $f_{a}$ 和所有可能的分析状态 $\Sigma_a=\Set{\sigma_{a}}$
3. 指派函数 $\alpha\colon2^{\Sigma_s}\to\Sigma_a$，将给定的执行状态集抽象成分析状态
4. 指派函数 $\gamma\colon\Sigma_a\to2^{\Sigma_s}$，将给定的分析状态还原为可能的执行状态集

并且有如下性质：

1. $\forall x,x\subseteq\gamma(\alpha(x))$：抽象后再还原可能丢精度，但仍是保守估计（不会低估）
2. $\forall y,\alpha(\gamma(y))\le y$：还原后再抽象不会损失精度

那么 $(\alpha,\gamma)$ 就称为一对 galois connection

需要注意，通常 $\alpha$ 是构造的，$\gamma$ 往往是 $\alpha$ 的伴随产物（这也意味着通常有 $\alpha\circ\gamma=\text{id}$），因此上面两个条件也在说：

1. 抽象必须保守
2. 抽象要尽可能避免丢精度

随机附赠的性质有：

• $\alpha(\bigcup A)=\bigcup_{a\in A}\alpha(a)$
• $\gamma(\bigcap A)=\bigcap_{a\in A}\gamma(a)$
• $\alpha(\bot)=\bot$，$\gamma(\top)=\top$

Soundness

当我们说一个分析 sound 的时候，说的就是 $\forall \sigma, \alpha(f_s(\sigma))\le f_a(\alpha(\sigma))$

Optimality

对于给定的 $\Sigma_a$，最精确的分析 $f_a$ 由 $f_a=\alpha\circ f_s\circ\gamma$ 给出

简单证明一下：

任取单调、sound $g\colon \Sigma_a\to\Sigma_a$，由 $g$ sound 立刻有 $\forall \sigma_a\in\Sigma_a, \alpha(f_s(\sigma_a))\le g(\alpha(\sigma_a))$

这说明 $\forall \sigma_s\in\Sigma_s, \alpha(f_s(\gamma(\sigma_s)))\le g(\alpha(\gamma(\sigma_s)))$。根据定义，$\alpha(\gamma(\sigma_s))\le \sigma_s$；$g$ 单调，$g(\alpha(\gamma(\sigma_s)))\le g(\sigma_s)$

串起来就是 $\alpha\circ f_s\circ\gamma\le g$，由 $g$ 的任意性可知 $\alpha\circ f_s\circ\gamma$ 最优。

这告诉我们对于给定的格抽象，理论上总是存在一个最优的抽象解释器：粗暴地把抽象状态具体化，交给具体语义的解释器执行，最后把可能的结果收集起来再抽象。

这里有个比较重要的点是这样的：即便所有的原子操作语义都做到了最优抽象，它们的组合也可能达不到最优。

办法：

1. 对组合后的原子操作建模，扩大上下文。比如直接对数组（ptr offset deref => array load）和对象（ptr offset deref => load field）操作整体建模
2. 做一些语义等价但利于分析的程序变换。比如用易于分析的 IR、做优化