跳转到内容
Jason's Study

Miné 八边形抽象域 — 在区间和多面体之间的甜点

是什么

八边形（octagon）是 Antoine Miné 2001 年提出、2006 年期刊扩展的一种让静态分析器只用两变量带正负号约束就能近似程序状态的抽象域。日常类比：你想圈一群点，多面体是一根能任意斜拉的橡皮筋（贵，能拉但累），区间是横平竖直的盒子（便宜但盲）；八边形就是中间——只允许橡皮筋走 8 个方向（水平、垂直、两条 45 度对角线），便宜又比盒子能斜着兜更多关系。

更具体一点：八边形维护的不变式都长这个样子：

±x ± y ≤ c

也就是任挑两个变量、给它们各配一个正负号、加起来不超过某个常数。在二维平面上，这种约束的交集围出来的图形最多有 8 条边——所以叫八边形。

为什么重要

如果只看历史脉络，1977 年 Cousot 抽象解释提供框架，1978 年 Cousot-Halbwachs 多面体填了最强的关系型数值域。但多面体最坏复杂度是变量数的指数级，工业代码动辄上千变量，跑不动。

不理解 octagon，下面这些问题就讲不清：

  • 为什么 Astrée 给空客 A340/A380 飞控做零警告分析时，默认数值域是 octagon 而不是多面体——便宜十倍
  • 为什么 Frama-C 的 Eva 插件、IKOS（NASA 航天）、Apron 库、Crab-LLVM 几乎都把 octagon 列为内置选项
  • 为什么 2006 年之后大量”轻量关系型”分析域（zone、TVPI、pentagon）都拿 octagon 当对照基线
  • 为什么”区间够用就够用，不够用就上 octagon，再不够才动多面体”成了静态分析师的默认调度顺序

核心要点

整个方法可以拆成 三件事。

  1. 形状被刻意限死：约束只能是 ±x ± y ≤ c。这意味着 x ≤ y、x + y ≤ 10、x − y ≥ 3 都能表达；但 x + 2y ≤ z（系数不是 ±1）或 x + y + z ≤ 5（三变量）就故意放弃。换来的是规则的代数结构，操作能用矩阵搞定。

  2. DBM 数据结构：差分约束矩阵（Difference Bound Matrix）。把 n 个变量每个拆成正负两份，凑成 2n 个”带符号变量”，开一个 2n × 2n 的矩阵，第 (i, j) 格存 vᵢ − vⱼ ≤ c 这一条上界。所有可能的两变量约束都能塞进去。一条 x ≤ 5 实际上转写成 x − 0 ≤ 5，单变量约束自然落入同一框架。

  3. 强闭包当规范化：同一组约束有很多种写法，分析器要能判等。用 Floyd-Warshall 跑一遍最短路径，把矩阵补成”所有蕴含的约束都已写出”的标准形——这一步叫 strong closure，复杂度 O(n³)。规范化之后两个 DBM 才能直接比较、求交、求并。

一句话：形状受限到能用矩阵表示 + 规范化用最短路径 + meet/join/widening 都是矩阵逐格操作。

实践案例

案例 1：区间抓不到、八边形抓得到

i = 0; j = 10;
while (i < j) {
  i = i + 1;
  j = j - 1;
}

退出循环时，区间分析只会告诉你 i ∈ [1, 10]、j ∈ [0, 9]，看不见两者关系。八边形能维护 i + j = 10（即 i + j ≤ 10 且 −i − j ≤ −10 同时成立），于是循环终止时立刻能推出 i = j = 5，下游分析省一大堆误报。

每一步的 DBM 上的运算都是 O(n²) 的逐格更新。整个循环 widening 几次后稳住，分析器就退出迭代。

案例 2：数组越界检查

void f(int n, int a[]) {
  for (int i = 0; i < n; i++) {
    a[i] = ...;  // 越界吗？
  }
}

要证 a[i] 安全需要 0 ≤ i < n。区间域只能告诉你 i ∈ [0, MAX_INT)、n 是参数不知道——无解。八边形维护 i − n ≤ −1（来自 i < n）和 −i ≤ 0（来自循环初始化和 i++），直接证明每次访问安全。这就是 Astrée / Frama-C 在嵌入式 C 里默认开 octagon 的根本原因。

把同样的代码喂给纯区间分析器，要么报误警，要么需要程序员手写注解；用 octagon 后，这一类越界检查几乎全自动通过。这正是工业界愿意为额外的 O(n²) 内存买单的原因。

案例 3：复杂度直观对比

数值域内存一次操作能表达的关系
区间O(n)O(n)单变量上下界
八边形O(n²)O(n³)±x ± y ≤ c
多面体最坏 O(2ⁿ)最坏 O(2ⁿ)任意线性 Ax ≤ b

100 个变量时：区间几 KB、八边形 80KB、多面体可能爆内存。

这张表也是 Astrée 调度数值域的依据——先跑区间，发现关键约束依赖两变量关系再升 octagon，遇到三变量以上才动多面体且只在小范围里跑。

踩过的坑

  1. 三变量关系无能为力：x + y + z ≤ 100 这种分析不到。如果程序里这种约束多，octagon 退化成区间的精度，只是更慢。
  2. 非线性算子全靠区间兜底：z = x * y、z = x / y、z = x % y——这些 octagon 直接转交给区间域，回头再升回来，精度损失累计。
  3. 强闭包必须做完才能比较：忘了规范化就 join 两个 DBM，结果可能是错的（不等价的矩阵被当成不等）。所有现代实现把 closure 当强制前置步骤。
  4. widening 设计敏感：循环里约束如果一直在长大（如 i++），不做 widening 会无穷迭代。Miné 论文给的标准 widening 是”上一轮稳定的约束保留，变化的约束直接丢”——简单粗暴但保证收敛。
  5. 变量数很大时 O(n³) 也吃力：上万变量级别，octagon 的强闭包都跑不动。Astrée 用”打包（packing）“——把变量切成几十人一组的小簇分别分析，组间退化成区间。
  6. 浮点处理需要小心：约束系数若是浮点，DBM 里的更新要做正确舍入，否则会偏向不安全那一侧（漏报）。Miné 在论文里专门花一节讨论 IEEE 754 与抽象域的兼容。
  7. 变量替换语义复杂：赋值 x = 2*y + 1 这种”系数不是 ±1”的算子在 octagon 里没有精确转移函数，要么放弃精度求一个最佳上近似，要么转交其他域。

适用 vs 不适用场景

适用：

  • 嵌入式 C/C++ 控制软件——飞控、汽车 ECU、医疗设备控制器（Astrée 的主战场）
  • 数组越界、整数溢出、除零检查——i < n 这类两变量约束密集的情形
  • 中等规模程序（几十到几百变量），需要比区间精度更高但跑得起的场合
  • 作为多分析域组合中的”中间层”，区间不够时先用 octagon 试，再不够升多面体

不适用：

  • 程序里关键约束含三变量及以上线性关系 → 直接上多面体（cousot-halbwachs-polyhedra-1978）
  • 关键约束是非线性（多项式、模算术）→ 用 SMT 求解器或专用域
  • 变量极多（上万级）且耦合紧 → octagon 的 O(n²) 内存吃不消，要靠变量打包或专用降维域
  • 形状/堆分析（链表、树）→ 这是 sagiv-shape-analysis 的领域，与数值域正交

历史小故事（可跳过）

  • 1977 年：Cousot-Cousot 提出抽象解释总框架，但具体数值域选什么没有规定。
  • 1978 年：Cousot 和 Halbwachs 提出凸多面体域。理论上最强，但实测中变量一多就指数爆炸。
  • 1992-1996 年：差分约束系统（difference constraints）和 DBM 数据结构在调度、实时验证（UPPAAL 等）里成熟。
  • 2001 年：Antoine Miné 在 AST 2001 首次提出八边形——把 DBM 嫁接到抽象解释，复杂度从指数压到立方。
  • 2003 年：Astrée 选定 octagon 作为默认数值域之一，首次给 A340 飞控跑出零警告。
  • 2006 年：Miné 在 HOSC 期刊发表完整版（70 页），含所有算子的形式定义、最优性证明、复杂度分析。这就是本篇笔记的对象。
  • 后续：Apron 库（Bertrand Jeannet 等）把 octagon 做成可复用 C 库，进入 Frama-C、IKOS、Crab-LLVM、Sparrow 等十多个分析器。Miné 后来去 Sorbonne 当教授，继续做 Astrée 商业化（AbsInt 公司）。

学到什么

  1. 甜点定理：在表达力 vs 复杂度的连续谱上，故意丢掉一部分表达力换来工程可用，往往比”全都要”赢——octagon 之于多面体，就是 SQLite 之于 Postgres。
  2. 形状决定数据结构：约束限定到 ±x ± y ≤ c 之后，所有信息能塞进矩阵，所有操作变成矩阵逐格运算——这是把抽象域真正”工程化”的关键一招。
  3. 规范化是判等前提：同一对象的多种表示必须能映射到唯一标准形，否则比较、缓存、收敛检测都会出错。强闭包就是 octagon 的标准形。
  4. 理论 → 工程隔 25 年：1977 抽象解释 → 2001/2006 octagon 落地 → 2003 Astrée 给空客出零警告报告。这个周期在静态分析里很典型。
  5. 少一些表达力，多一些落地：放弃三变量约束没让 octagon 在工业里被淘汰，反而成了主力——理论上更弱的工具反而被用得更多，这种反直觉在系统设计里反复出现。

延伸阅读

关联

一句话回顾

把约束限定到 ±x ± y ≤ c，用 2n × 2n 的矩阵存所有可能的两变量约束，用 Floyd-Warshall 强闭包做规范化，meet/join/widening 全是矩阵逐格运算——这就是 octagon。它放弃了多面体的大部分表达力，换来内存 O(n²) 与运算 O(n³) 的工程可行性，从而在 Astrée、Frama-C、IKOS 等工业级分析器里成为默认主力。这是”丢一点表达力换一截可用性”在静态分析里的标志案例。