跳转到内容
Jason's Study

Bi-Abduction — 让静态分析自动猜出函数缺什么前提

是什么

Bi-abduction（双向溯因）是一套**让静态分析器自己猜出每个函数”需要什么前提、留下什么副作用”**的算法。日常类比：像一个侦探不仅推凶手是谁（缺的前提），还顺手列出现场没动过的家具（不变的部分），两件事一次完成。

具体地说，传统形状分析要求你先告诉它”这个函数被怎么调用”，它才能往下推。Bi-abduction 反过来：你只把函数代码丢给它，它自己反推一份”为了让这段代码不崩，调用者至少要给我一个非空链表”，再附一份”我没动这块堆”。

这就是 Facebook Infer 的核心引擎——能在百万行 Java/Objective-C/C 代码上跑分钟级，每天给 Meta 程序员发”你这次提交可能 NPE”的核心理论。

为什么重要

不理解 bi-abduction，下面这些事说不通：

  • 为什么 2010 年之前的形状分析只能跑几千行代码，2015 年 Infer 能跑 Facebook 全代码库
  • 为什么 Infer 不需要你写注解（不像 Coq / Dafny）也能查出空指针
  • 为什么 Facebook 2015 年花 1500 万美元收购 Monoidics（这篇论文作者的公司）
  • 为什么”分离逻辑”这套学院派理论 7 年内就进了工业 CI

核心要点

Bi-abduction 在 分离逻辑（reynolds-separation-logic）的基础上，把”推一个公式”改成”同时推两个未知”。

分离逻辑回顾：H1 * H2 表示堆被切成两块互不重叠。{P} c {Q} 是 Hoare 三元组——执行前堆满足 P，执行后满足 Q。最关键的 frame rule：

{P} c {Q}
─────────────────  （F 是 c 不碰的那块堆）
{P * F} c {Q * F}

普通溯因（abduction）：已知 H1，目标 H2，找一个 M 使 H1 * M ⊢ H2——即”H1 还差什么才能推出 H2”。

双向溯因（bi-abduction）：同时找 anti-frame M 和 frame F：

H1 * M  ⊢  H2 * F
  • M = 调用者必须额外提供的前提（缺的那块）
  • F = 这段代码没碰、原样保留的那块

用法：分析函数 f(x) 时，一句句往下推，每碰到 x->next 就发现”我需要 x 是非空 cell”。bi-abduction 把这条要求加进 M。整段代码扫完，得到 {pre} f(x) {post} 一对摘要。不需要谁告诉你 f 怎么被调用。

实践案例

案例 1：分析一个最简单的函数

void f(node *x) {
    x->next = 0;
}

bi-abduction 推理过程：

  1. 起点假设堆是空 emp
  2. 读到 x->next → 需要 x 指向某个 cell，否则崩。bi-abduction 加 M：x ↦ _
  3. 写完 x->next = 0 → 后置变成 x ↦ 0
  4. 输出摘要：{x ↦ _} f(x) {x ↦ 0}

注意：没有人告诉它 x 应该非空。它自己反推出来。

案例 2：组合多个函数（compositional）

void g(node *y) { f(y); f(y); }

g 调用 f 两次。bi-abduction 用 f 的摘要 {x ↦ _} f(x) {x ↦ 0} 拼起来：

  • 第一次调用：需要 y ↦ _，调完变成 y ↦ 0
  • 第二次调用：需要 y ↦ _——这次 y 已经是 0，匹配（0 也是某个值）
  • 最终摘要：{y ↦ _} g(y) {y ↦ 0}

关键：分析 g 时没重新看 f 的代码，只用摘要。这就是 compositional——每个函数独立分析一次，调用时复用结果。百万行代码因此可行。

案例 3：链表遍历的递归归纳

void clear(list *l) {
    if (l) { clear(l->next); free(l); }
}

bi-abduction 配合抽象（把具体堆图归纳成 list(l) 谓词）推出：

{list(l)} clear(l) {emp}

整条链表清干净，堆变空。这是 sagiv-shape-analysis 的目标，但 Sagiv 法要全程序信息；bi-abduction 只看 clear 一个函数就能给出。

踩过的坑

  1. abduction 解不唯一：H1 * M ⊢ H2 可能有无数个 M（M 可以加任何无关谓词）。算法要选最弱的 M——只加必要的。否则函数摘要会越滚越大。

  2. frame 也不唯一：同理，F 要选最强的（包含所有无关部分）。bi-abduction 用一套启发式同时优化两边。

  3. 不一定能找到摘要：有些函数（比如带循环的复杂操作）算法找不出来——这时 Infer 会放弃这个函数，不报错也不保证正确。这是工程取舍：宁可漏报也不假报。

  4. 抽象域要选对：bi-abduction 本身是框架，配什么谓词（list / tree / DAG）决定能查什么 bug。Infer 用了一套定制谓词来抓 NPE 和资源泄漏。

适用 vs 不适用场景

适用：

  • 大规模代码库的轻量级形状分析（NPE、use-after-free、资源泄漏）
  • 每次只能看到 diff 的增量分析（CI 集成）
  • 没有完整调用图的库代码分析

不适用：

历史小故事（可跳过）

  • 2001：Reynolds-O’Hearn 发表分离逻辑，证明能优雅处理堆，但工具化困难
  • 2006：Distefano-O’Hearn-Yang 写出第一个能跑的形状分析 Smallfoot，但要手标 pre/post
  • 2009：本文——把 abduction 从 Hoare 推向”双向”，第一次让分析器自动推出摘要
  • 2009：作者们成立 Monoidics 公司，把算法做成商业工具 Infer
  • 2013：Facebook 引入 Infer，每天扫所有 Android/iOS 提交
  • 2015：Facebook 收购 Monoidics，开源 Infer
  • 至今：AWS、Mozilla、Spotify、Uber 都在用变体

学到什么

  1. “反过来推”是个独立的能力——演绎是已知前提推结论，溯因（abduction）是已知结论反推前提，bi-abduction 同时干两件
  2. 分离逻辑的 frame rule 是工业级分析能 scale 的根因——它把”我没碰的部分”形式化，从而支持组合
  3. 学术 → 工程这条路在 PL 里走得最快：2009 论文，2013 工业部署，2015 开源
  4. Compositional 是大规模静态分析的必经之路——任何要求”全程序信息”的方法都进不了 CI

延伸阅读

关联

反向链接