如何证明你的代码没有运行时错误（以及为什么你很可能会放弃尝试）

你的测试套件通过了。你的类型检查器全是绿色。你发布了。两小时后，生产环境在一个没人想到要测试的边界情况上抛出了 IndexError。

测试能发现 bug。类型系统能预防一部分。但两者都无法证明你的程序完全没有运行时错误。要做到这一点，你需要更强力的手段：一种能够同时对所有可能的执行路径进行推理、而无需实际运行代码的方法。

抽象解释正是让这一切成为现实的技术。它为 Astrée、Facebook 的 Infer 以及 Rust 借用检查器中的可靠性保证提供了底层支撑。它也解释了为什么大多数静态分析工具”零误报”的营销宣传都是谎言。

运行时错误是一个可达性问题

运行时错误就是程序执行到达了一个坏状态的操作。除以零、空指针解引用、缓冲区溢出、索引越界。每一个都是因为执行到达了程序中某个不安全的操作点而发生的。

要证明不存在任何运行时错误，你需要证明在每一种可能的执行中，每一个不安全的操作都是不可达的。每一个输入。每一个分支。每一次循环迭代。

除了玩具程序之外，穷举测试是不可能的。符号执行扩展性很差，因为路径爆炸会拖垮你。抽象解释走了一条不同的路：它放弃了对精确值的追踪，转而跟踪能够保证覆盖所有真实执行的近似属性。

抽象解释到底在做什么

抽象解释由 Patrick 和 Radhia Cousot 于 1976 年提出。其核心思想非常优美且简单：运行你的程序，但不是用真实的数字、字符串和指针来计算，而是用一种能够过度近似（over-approximate）真实值的抽象表示来计算。

你可以把它理解为用一次”影子”执行来取代具体执行，这次影子执行只追踪你关心的属性。不是精确知道 x = 42，而是知道 x > 0。不是精确知道 arr 长度为 10，而是知道 arr 非空。

关键的约束是可靠性（soundness）。每一个具体状态都必须被某个抽象状态所表示。如果抽象执行说某个操作是安全的，那么它所代表的所有具体执行都是安全的。代价是精度：如果抽象状态过于模糊，你就会得到误报（对安全操作发出虚假的警告）。

一个具体例子：区间分析

这里有一个最小的抽象解释器，能够证明除以零是不可能的。它用区间来追踪每个变量的可能取值范围。

# A tiny abstract interpreter for interval analysis
from dataclasses import dataclass
from typing import Dict

@dataclass(frozen=True)
class Interval:
    lo: float
    hi: float

    def __contains__(self, val: float) -> bool:
        return self.lo <= val <= self.hi

TOP = Interval(float("-inf"), float("inf"))

def eval_expr(env: Dict[str, Interval], expr) -> Interval:
    if isinstance(expr, int):
        return Interval(float(expr), float(expr))
    if isinstance(expr, str):
        return env.get(expr, TOP)
    if expr[0] == "+":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        return Interval(l.lo + r.lo, l.hi + r.hi)
    if expr[0] == "-":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        return Interval(l.lo - r.hi, l.hi - r.lo)
    if expr[0] == "*":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        products = [l.lo * r.lo, l.lo * r.hi, l.hi * r.lo, l.hi * r.hi]
        return Interval(min(products), max(products))
    if expr[0] == "/":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        if r.lo <= 0 <= r.hi:
            raise ValueError("Possible division by zero")
        return TOP
    raise ValueError(f"Unknown expr: {expr}")

def merge_envs(env1: Dict[str, Interval], env2: Dict[str, Interval]) -> Dict[str, Interval]:
    keys = set(env1) | set(env2)
    result = {}
    for k in keys:
        a = env1.get(k, TOP)
        b = env2.get(k, TOP)
        result[k] = Interval(min(a.lo, b.lo), max(a.hi, b.hi))
    return result

def analyze(program, env: Dict[str, Interval]) -> Dict[str, Interval]:
    env = dict(env)
    for stmt in program:
        if stmt[0] == "assign":
            _, var, expr = stmt
            env[var] = eval_expr(env, expr)
        elif stmt[0] == "if":
            _, cond, true_branch, false_branch = stmt
            t_env = analyze(true_branch, dict(env))
            f_env = analyze(false_branch, dict(env))
            env = merge_envs(t_env, f_env)
        elif stmt[0] == "while":
            _, cond, body = stmt
            old = dict(env)
            for _ in range(10):
                new = analyze(body, dict(old))
                changed = False
                for k in set(old) | set(new):
                    prev = old.get(k, TOP)
                    curr = new.get(k, TOP)
                    widened = Interval(min(prev.lo, curr.lo), max(prev.hi, curr.hi))
                    if widened.lo != prev.lo or widened.hi != prev.hi:
                        changed = True
                    old[k] = widened
                if not changed:
                    break
            env = old
    return env

# Example program: y = 10 / (x + 1) where x >= 0
program = [
    ("assign", "t", ("+", "x", 1)),
    ("assign", "y", ("/", 10, "t")),
]

# This should pass: x >= 0 means t >= 1, so no division by zero
safe_env = analyze(program, {"x": Interval(0, 100)})
print("Safe env:", safe_env)

# This should fail: x could be -1
try:
    bad_env = analyze(program, {"x": Interval(-5, 5)})
except ValueError as e:
    print("Caught:", e)

运行它。第一个案例证明了安全性，因为 t 的区间是 [1.0, 101.0]，排除了零。第二个案例正确地标记了风险，因为当 x 为 -1 时，t 可能为零。

if 的处理方式通过对两个分支取区间的并集来合并它们。while 的处理方式则迭代直到区间停止增长（即到达不动点）。这就是抽象解释的核心：你用精确值换取有保证的过度近似，并通过证明坏状态位于近似范围之外来证明安全性。

哪里会出问题：精度墙

上面的例子只有玩具级别的大小。真实程序中有别名、递归、堆分配，以及数据相关的循环边界。每一个都会以可预见的方式摧毁精度。

考虑一个将 i 从 0 递增到 100 的循环。一个朴素的区间分析可能会将 i 加宽到 [0, +inf)，并且永远无法恢复上界。你需要关系型域（如多面体或八面体）来追踪 i <= 100。这些域的时间复杂度随变量数量呈立方或指数增长。对于一个有 1000 个变量的程序，你是不可能运行多面体分析的。

这就是商业工具做出不同选择的原因。Astrée 使用经过精心设计的抽象域格（lattice），并针对嵌入式 C 进行了手工调优。Infer 使用分离逻辑和双向演绎（bi-abduction）来扩展到数百万行移动代码，但它在某些语言特性上放弃了可靠性。Rust 的借用检查器本质上就是一个抽象解释器，只不过它只有一个极其精确的域：所有权。

你无法回避的权衡

可靠性、精度和可扩展性。三选二。

一个既可靠又高精度的分析器无法扩展到small modules之外。一个可扩展且可靠的分析器会用误报淹没你。一个可扩展且高精度的分析器会漏掉真实的 bug。

你对抽象域的选择就是那个调节旋钮。区间分析快但精度低。多面体精确但速度慢。谓词抽象处于中间地带，并且驱动了大多数软件模型检查器。

如何实际使用它

你大概不会自己写一个抽象解释器。你会使用已经存在的。

对于 C 和嵌入式系统，Astrée 和 Frama-C 是成熟的选项。Frama-C 的 EVA 插件可以对真实世界的 C 代码进行区间和内存分析。

对于 Rust，类型系统本身就已经编码了一个所有权抽象域。Miri 是一个解释器，不是抽象解释器，但它能捕获类型系统遗漏的未定义行为。

对于通用代码，来自 Meta 的 Infer 是最接近可扩展抽象解释器的工具，支持 Java、C++ 和 Objective-C。它能在生产codebases中发现真实的空指针解引用和内存泄漏 bug。

如果你想自己动手实验，可以从你自己解析的语言上做简单的符号分析或区间分析开始。《龙书》涵盖了数据流分析。Nielson 和 Nielson 的《Principles of Program Analysis》是专门针对抽象解释的标准参考书。

证明否定

抽象解释不会让你的代码完全没有 bug。它给你的是一个数学框架，用于证明特定类别的运行时错误是不可能的。这个证明的质量只取决于你的抽象域、你的加宽策略，以及你对误报的容忍度。

大多数团队从优秀的测试和可靠的类型系统中获得的价值更大。但当你编写的代码一旦出现运行时错误就意味着一颗卫星从天上掉下来时，抽象解释就是让你晚上能睡个好觉的方法。