Compositional Shape Analysis by means of Bi-Abduction

[skyleaworlder]

https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=fcd1369ee602ec4437c8c46d444bcd43467aa48f
https://www.researchgate.net/publication/220431326_Compositional_Shape_Analysis_by_Means_of_Bi-Abduction (这篇更详细)

Cristiano Calcagno
Imperial College, London
[email protected]

Dino Distefano Peter O’Hearn Hongseok Yang
Queen Mary, University of London
{ddino,ohearn,hyang}@dcs.qmul.ac.uk

from https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=infer+biabduction&btnG=

[skyleaworlder]

Abduction 讲究的是根据 “结果” 与 “部分原因” 推导不全另一部分原因。如：我看到 a 和 b 走在一起，根据他们本来不是很熟且今天是 5.20，我合理推断这是因为 a 对 b 表白成功导致的。Biabduction 则是连 “结果” 也不知道全貌：

首先根据 abduction 得出 anti-frame，然后再根据 A 与 anti-frame 推导 frame。

[skyleaworlder]

文中对有一套用于抽象堆栈的符号系统：

• Heap 在表示上可将其理解成一个从 Location 映射到 Value 的 map；或者理解成内存上一块连续的空间，特定的 Location 上对应着一些值；
• Stack 是变量到具体值的映射，比如 val a = 2，这里的 $a$ 在 Stack 就表示成 $a \to 2$。

• $\prod$ 表示表达式构成的约束关系，如 $x + y < 2$；
• $\sum$ 表示堆的空间关系，即变量与堆地址 / 堆上值的指向关系；
  • $emp$ 表示空堆，按我的理解是 “大小为 0” 的堆；
  • $true$ 按我的理解是 “满足任何条件的堆”，如此说来，$true$ 也可以是 $emp$。
• $\Delta$ 和 $H$ 的区别按照我的理解就只是在 abduction 公式里面的设定，应该不具备特别大的意义。

[skyleaworlder]

文章后面给出了 abduction rules，这里一一介绍它们的含义，但我的理解比较粗浅，有可能错误。

好吧我第一个就没看懂，我想问为什么 $X$ 不在 $H_2$ 的 LVar (Logical Variables) 里，还能在 $H_1$ 里面？

就是说，如果现在有一个 $(\prod \land \sum) * [M] \triangleright H$ 已经成立了，并且我单靠 $(\prod \land \sum)$ 就能推出来一个 $\prod'$，那么可以额外分离出一个 $\exists X.\prod' \land \sum'$，这里的 $\sum'$ 是满足 $\prod \land \prod'$ 的。

和上两条不一样，这是要改变 $H_1 / M / H_2$ 三方的内容。从表现上来看，就是 “如果我的 $H_1$ 拆得出一个等式，或者说有一个等量关系，那我可以把这个等量关系放到 $[M]$ 里面，让这个关系作为新的 $H_1 / H_2$ 中指向关系推导的桥梁。”

这两个一样，所以就一起说了。

• ls-right 指的是 “假设目前 $H_2$ 里拆得出一个链表关系，如果在 $H_1$ 一侧有 ‘这个链表可以往左延伸得更长’ 的信息，那么可以把这两个关系整合在一起合成一个大链表”；
• ls-left 指的是 “现在的 $H_1$ 已经有一段链表了，且可以由这个信息推出 $H_2$。那么如果我把 $H_1$ 里面的短链表换成同尾的长链表，在这个基础下 $H_2$ 也得补全更多的关于 ‘新头指向旧头’ 的信息”。

两个 base 是无条件成立。

• base-emp 的意思是：反正是小推大，多约束推少约束。如果堆上没有约束要求，可以在 abduction 的时候直接把 $H_2$ 推给 $M$。
• base-true 的意思是：虽然 $H_1$ 可能有堆空间约束，但是可以无限放宽约束条件，让 $H_2$ 拥有一个满足所有条件的堆 true。同时也不管 $H_1$ 里面到底有什么 pure formula，直接用 $[M]$ 一样的 $\prod$。

没啥，就是 $[M] / H_2$ 同时加堆空间约束，

[skyleaworlder]

在完成对上述 logic rules 的解释后，文中给出了 Bi-Abduction 的算法，其实很简单：

Frame 可以理解成正常的推导，根据 $H_0$ 和右侧已有的 $H_1$，去推测还可以生成一些不 fail 的 $L$ 使这个式子的右侧约束更多，表示的范围更小。

Abduction 就是上面提到的那样。因此，Bi-Abduction 是：

[skyleaworlder]

文中后面几个段落就不再局限于上面的 lseg 语言了，加入了新的 if 以及 while，因为接下来的部分讲的是 “使用 biabduction 生成 procedure summary”：

这里我不清楚我有没有理解对，我认为这里有必要说一说：

• $H$ 这里表示 / 展示 / 假设的应该是 “在执行这个 swap 之前的符号堆情况”；
• $x \to a' * y \to b'$ 就是 “要进入 swap 所必须满足的条件”，这个 “必须” 是 swap 本身 signature 的要求：“swap(x, y) 要求 x 和 y 指向两个 logic variable”；
• 因此这里需要 $BiAbduction(H, x \to a' * y \to b')$ ，这个计算的结果是：
  • 为了进入 swap 所必要的条件 $M$；
  • 进入 swap 之后还留存着的条件 $L$。
• $F$ 指的是 “当前语句执行的前置条件”，这个前置条件在算法里也可以 update。

可以看到这里的 Rename，在 Bi-Abduction 计算后，会对计算结果进行重命名，然后修改 $F$ 和 $H$ 。

Rename 的结果是： $(e', b', M_0)$ ，这里的 $e' = (y, d)$, $b' = (a', b')$, $M_0 = (b \to d)$。根据 Abstract Semantics 对 $R$ 的重新赋值可知要把 $M_0$ 与 $F$ 合在一起。根据 swap 的 summary，就可以得出在给定符号堆 $H$ 的前提下，执行完 swap 后的符号堆是： $v = 0 \land x \to d * y \to y * z \to 0$。

这个例子想要说明的是：

• 在算法处理程序前，这个 swap 函数的 precondition $F$ 是缺失的 & 符号堆的情况已确定；
• 通过这一套算法后，可以进一步补全 swap 的 precondition，同时得到了 swap 执行后符号堆的变化结果。

[skyleaworlder]

文中后面基于前面的 BiAbduction 推导 precondition $F$ 与 symbolic heap states $H$，给出了过程间摘要分析算法，也就是论文中的 “Top Level Algorithm”：

原来这里用的是不动点，InferPre 与 InferSpec 交错计算直到 $P$ 与 $T$ 收敛为止。

[skyleaworlder]

这篇论文属于没读好，以后理解到了更多的会来补充。