Cousot-Halbwachs 凸多面体域 — 让分析器自己发现变量间的线性关系

是什么

凸多面体域（Convex Polyhedra Domain）是 Cousot 和 Halbwachs 1978 年提出的一种让静态分析器自己发现「程序里多个变量之间满足什么线性关系」的方法。日常类比：你有一堆散落在桌面上的点，想用一根橡皮筋把它们全部圈起来——区间分析只能给每个变量一个独立的盒子（盒子永远是横平竖直的），多面体能把橡皮筋斜着拉，于是「i 永远不超过 j」「x + y 总等于 10」这种联合关系也能被兜进去。

更具体地说：把 n 个程序变量看成 n 维空间里的一个点，程序运行所有可能的状态拟合成空间中一个凸多面体——表示成 Ax ≤ b 这样的一组线性不等式。分析器的任务就是在每个程序点维护这样一个多面体，并随着程序前进不断更新。

为什么重要

这是 1977 年 Cousot-Cousot 抽象解释框架之后第一个真正工业级好用的关系型数值域。理论框架告诉你”格 + Galois connection + 不动点”，但具体格选什么没人知道——Halbwachs 把多面体填进去，让 1977 的骨架第一次有了肉。

不理解它，下面这些现象都讲不清：

• 为什么 Astrée（验证 A380 飞控零运行时错误）一类工具要用 octagon、TCM 等”弱化多面体”——因为完整多面体太贵
• 为什么 Apron / ELINA / NewPolka / Crab-LLVM 这些现代分析器都把”polyhedra”当成内置数值域之一
• 为什么 Polyspace、Infer 检查整数溢出、数组越界时常常能一眼看出”i < n”，而单元测试漏的就是这种
• 为什么区间域（Interval）和多面体域并存，永远没被互相替代——一个便宜但盲，一个贵但全

核心要点

整个方法可以拆成 三件事。先约定符号：⊥（bottom，“无可达状态”），⊤（top，“任何状态都可能”）。

1. 两种等价表示：一个多面体可以用 H-rep（约束式：一堆 Ax ≤ b 的不等式）描述，也可以用 V-rep（生成元式：一组顶点 + 一组射线）描述。Chernikova 算法负责两种表示来回转换。听起来折腾，但做不同操作时换不同表示更快——求交集（meet）用 H-rep 拼一拼就行，求凸包（join）用 V-rep 把顶点合并最方便。

2. 三个核心算子：

   • meet（∧）= 交集：两条路径汇合时，把两个多面体相交，约束变多
   • join（∨）= 凸包：if-else 分支汇合时取两个多面体的凸包（最小的能包住二者的多面体），约束变松
   • widening（∇）= 加速收敛：循环迭代时多面体可能越长越大，永远不收敛——widening 直接丢掉那些每轮都在变的不等式，强制几步内稳住

3. 不动点迭代：把每个程序点的多面体当成变量，从 ⊥ 出发反复用上述算子推到收敛。Tarski 定理保证存在最小不动点；widening 保证有限步内一定到达。

一句话总结：用多面体当抽象域，用 H-rep/V-rep 灵活切换做运算，用 widening 强制收敛。

实践案例

案例 1：区间域抓不到的关系

i = 0;
j = 10;
while (i < j) {
  i = i + 1;
  j = j - 1;
}
// 循环结束后 i == j == 5？

区间域只能告诉你 i ∈ [0, 10]、j ∈ [0, 10]——已经够松了。但多面体域能维护 i + j == 10 这条等式，循环每一轮都成立，所以它能直接证明退出时 i == j 且 i + j == 10。

案例 2：循环不变式自动生成

for (int k = 0; k < n; k++) {
  a[k] = 0;
}

多面体分析自动得出循环里始终有 0 ≤ k < n，循环出口处 k == n。下游优化（比如证明 a[k] 不越界）就直接拿这个不变式用。这就是为什么 Polyspace 这类工具能”无注解直接给越界证明”。

案例 3：widening 救场

i = 0;
while (cond) i = i + 1;

不加 widening：每轮迭代多面体从 i = 0 变成 0 ≤ i ≤ 1、0 ≤ i ≤ 2、0 ≤ i ≤ 3…永远不收敛。widening 看到「上界一直在变」直接把上界丢掉，第二轮就稳定到 0 ≤ i，分析终止。代价是丢了精度——但能跑完比精确但跑不完强。

案例 4：和区间域的精度对比

程序点不变式	区间域	多面体域
初始 i = 0; j = 10	i ∈ [0,0], j ∈ [10,10]	i = 0 ∧ j = 10（同时 i + j = 10）
循环中	i ∈ [0,5], j ∈ [5,10]	i + j = 10 ∧ i ≤ j ∧ i ≥ 0
出口	i ∈ [5,10], j ∈ [0,5]	i = j = 5（精确）

区间永远是横平竖直的盒子，跨变量约束这一栏全是空的；多面体能把斜线关系写进去——这就是”关系型数值域”价值的最直白说明。

踩过的坑

1. 复杂度对维度极敏感：n 个变量的多面体，最坏情况下约束数和顶点数关于 n 指数级。工程上分析超过 20 个变量就明显拖慢，上百个变量基本不可用——所以工业工具会按函数局部限定变量子集。

2. widening 策略选错会丢精度：标准 widening 看上一轮多面体，把”这一轮变松了的不等式”扔掉。如果策略太激进，刚学到的有用关系（比如 i ≤ j）可能立刻被扔，分析变得几乎和区间一样松。后来出现了 widening with thresholds、narrowing 等改良。

3. 整数 vs 实数语义错位：多面体本质是实数（或有理数）域上的凸集，无法表达”x 是奇数""x 是 2 的幂”。要补这部分得叠 congruence 域或同时跑别的分析。

4. Chernikova 转换是性能黑洞：H-rep ↔ V-rep 切换在最坏情况下指数级，工程实现要缓存一份”双重描述”避免反复转。Apron 库就是干这件事的成熟工程产物。

适用 vs 不适用场景

适用：

• 需要发现跨变量线性关系（边界、循环不变式、数组索引安全）
• 验证关键代码块（几十个变量以内）的数值正确性
• 作为更复杂分析（如 Astrée）的子模块，用在精度比性能更重要的地方

不适用：

• 大型代码库的全程序分析——太贵，要降级到 octagon、interval、box
• 需要表达非线性关系（如 x = y * z）——多面体只刻画线性
• 整除性、奇偶性、位运算 — 必须叠别的域

它和别的数值域怎么取舍

抽象解释家族里数值域是一条谱系，按”能表达多少 / 多贵”排：

• interval（区间）：每变量一个独立 [lo, hi]，最便宜，零关系表达
• zone：能表达 x − y ≤ c（差约束），比区间多一点关系，仍便宜
• octagon（Miné 2001）：能表达 ±x ± y ≤ c（八角形），中等成本，被 Astrée 重用
• TCM / pentagon：octagon 的工程改良，覆盖工业代码常见模式
• polyhedra（本篇）：任意 Σ aᵢxᵢ ≤ b 线性约束，最强但最贵
• ellipsoid / 二次域：能表达非线性圆锥关系，几乎不用

工程取舍：把每个函数按规模/重要性挑域。飞控关键代码可以全多面体；通用代码默认 octagon；超大循环退到区间。

历史小故事（可跳过）

• 1977 年：Cousot 夫妇在 POPL 发表抽象解释框架——纯理论，没填具体域
• 1978 年：Patrick Cousot 和博士生 Nicolas Halbwachs 在 POPL 跟进，把”凸多面体”填进框架，给出第一个工业级实用关系型域
• 1980-90s：Halbwachs 转向同步语言，与人共同设计 Lustre（Esterel 家族），后来成为空客飞控、地铁信号系统标配
• 2000s：Bertrand Jeannet 等人写出 NewPolka / Apron 库，把多面体域作为开源组件普及
• 2010s+：苏黎世联邦理工 Pavol Bielik、Martin Vechev 团队的 ELINA 用并行+剪枝把多面体推到几千变量也能算

学到什么

1. 理论框架要靠具体域才能跑起来——1977 给地基，1978 给第一栋房
2. 同一对象，多种表示：H-rep 和 V-rep 各擅长一类操作，工程上”按需切换”是核心套路
3. 精度 vs 可终止永远在拉锯，widening 是这场拉锯里最务实的妥协
4. 理论 → 算法 → 工程产品这条 30-40 年长链清晰可见：1977 框架、1978 多面体、2000s Apron、2010s ELINA
5. 找到正确的抽象层很难：一旦找对（如本篇的多面体），它会成为整个领域的默认起点几十年

延伸阅读

• 论文 PDF：Cousot-Halbwachs 1978（13 页，密度极高）
• Apron 库：antoinemine/apron — 工业级数值抽象域 C 库，含多面体
• ELINA 库：eth-sri/ELINA — 苏黎世联邦理工的并行高性能版本
• 教程：Antoine Miné 的 Tutorial on Static Inference of Numeric Invariants
• cousot-abstract-interpretation —— 这篇论文的理论母体
• feautrier-polyhedral —— 同样用多面体，但目的不同（调度而非过近似）

关联

• cousot-abstract-interpretation —— 1977 抽象解释框架；本篇是它第一个工业级实例
• feautrier-polyhedral —— 1992 多面体调度；用多面体表达迭代域，求精确仿射变换
• astree —— 工业静态分析器；用弱化多面体（octagon、TCM）跑飞控代码
• kildall-dataflow —— 数据流分析的格论框架；多面体域是它的高维亲戚
• sagiv-shape-analysis —— 形状分析；和数值多面体并列，做指针/堆结构那一边
• steensgaard-pointer —— 指针分析；多面体补不上指针那一块，要互补

反向链接

• apron-2009 —— Apron — 把区间/八边形/多面体塞进同一个插槽
• astree —— ASTRÉE 分析器 — 让飞机控制代码的静态分析做到零警告
• cousot-abstract-interpretation —— Cousot 抽象解释 — 给静态分析一套统一数学框架
• feautrier-polyhedral —— Feautrier 多面体调度 — 把循环并行化变成解几何方程
• kildall-dataflow —— Kildall 数据流框架 — 用一套格论统一所有全局编译优化
• mine-octagon-2006 —— Miné 八边形抽象域 — 在区间和多面体之间的甜点
• sagiv-shape-analysis —— Sagiv 参数化形状分析 — 用三值逻辑证明链表树仍是链表树
• steensgaard-pointer —— Steensgaard 指针分析 — 用等价合并把指针分析压到几乎线性