停机问题说明，对任意程序做完备且正确的停机判断是不可能的。工程分析工具并没有因此失去意义。它们换了目标：不追求精确理解所有程序，而是用可计算的抽象信息给出有用结论。

抽象解释就是这个方向的代表。它把具体值集合映射到抽象域里，用保守规则模拟程序执行。只要抽象规则覆盖了所有可能的具体行为，分析结果就可以用于告警、优化或拒绝高风险程序。

本文用区间分析做一个最小模型：变量不再保存单个整数，而是保存可能取值范围。

从具体值到抽象值

具体执行关心单个值：

1
2
3
x = 3
y = 5
z = x + y = 8

抽象执行关心值的集合。若只知道 x 在 0 到 10 之间，y 等于 5，就可以推出：

1
2
3
x in [0, 10]
y in [5, 5]
z = x + y => z in [5, 15]

这个结果不精确。z 不一定等于区间里的每个数，但所有可能结果都被包含在 [5, 15] 里。保守性比精确性更重要：不能漏掉可能发生的值。

区间抽象域

区间可以用两个端点表示。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
from dataclasses import dataclass


@dataclass(frozen=True)
class Interval:
    lower: int
    upper: int

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lower + other.lower, self.upper + other.upper)

    def meet_less_than(self, bound: int) -> "Interval":
        return Interval(self.lower, min(self.upper, bound - 1))

    def __str__(self) -> str:
        return f"[{self.lower}, {self.upper}]"

add 是抽象加法。若 x 在 [0, 10]，y 在 [5, 5]，那么 x + y 在 [5, 15]。

meet_less_than 表示条件收窄。若已知 z 在 [5, 15]，又进入了 z < 12 的分支，那么 z 可以收窄到 [5, 11]。

抽象环境

抽象环境把变量名映射到区间。

1
2
3
4
5
Environment = dict[str, Interval]


def render(environment: Environment) -> str:
    return " ".join(f"{name}={interval}" for name, interval in environment.items())

常量赋值会得到单点区间。

1
2
def assign_const(environment: Environment, name: str, value: int) -> Environment:
    return environment | {name: Interval(value, value)}

加法赋值会调用抽象加法。

1
2
def assign_add(environment: Environment, target: str, left: str, right: str) -> Environment:
    return environment | {target: environment[left].add(environment[right])}

条件假设会收窄已有区间。

1
2
def assume_less_than(environment: Environment, name: str, bound: int) -> Environment:
    return environment | {name: environment[name].meet_less_than(bound)}

这些函数没有执行具体程序，只是在抽象域里更新变量可能范围。

完整示例

完整代码如下。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
from dataclasses import dataclass


@dataclass(frozen=True)
class Interval:
    lower: int
    upper: int

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lower + other.lower, self.upper + other.upper)

    def meet_less_than(self, bound: int) -> "Interval":
        return Interval(self.lower, min(self.upper, bound - 1))

    def __str__(self) -> str:
        return f"[{self.lower}, {self.upper}]"


Environment = dict[str, Interval]


def render(environment: Environment) -> str:
    return " ".join(f"{name}={interval}" for name, interval in environment.items())


def assign_const(environment: Environment, name: str, value: int) -> Environment:
    return environment | {name: Interval(value, value)}


def assign_add(environment: Environment, target: str, left: str, right: str) -> Environment:
    return environment | {target: environment[left].add(environment[right])}


def assume_less_than(environment: Environment, name: str, bound: int) -> Environment:
    return environment | {name: environment[name].meet_less_than(bound)}


env: Environment = {"x": Interval(0, 10)}
print("start", render(env))

env = assign_const(env, "y", 5)
print("after y = 5", render(env))

env = assign_add(env, "z", "x", "y")
print("after z = x + y", render(env))

env = assume_less_than(env, "z", 12)
print("after assume z < 12", render(env))

env = assign_add(env, "w", "z", "y")
print("after w = z + y", render(env))

运行结果：

1
2
3
4
5
start x=[0, 10]
after y = 5 x=[0, 10] y=[5, 5]
after z = x + y x=[0, 10] y=[5, 5] z=[5, 15]
after assume z < 12 x=[0, 10] y=[5, 5] z=[5, 11]
after w = z + y x=[0, 10] y=[5, 5] z=[5, 11] w=[10, 16]

读取分析结果

初始环境只知道：

1
x=[0, 10]

执行 y = 5 后，y 是单点区间：

1
y=[5, 5]

执行 z = x + y 后，区间端点相加：

1
z=[5, 15]

进入 z < 12 的分支后，z 的上界从 15 收窄到 11：

1
z=[5, 11]

最后执行 w = z + y，得到：

1
w=[10, 16]

这个结论仍然是近似结果。它没有枚举 x 的每个具体值，也没有证明 w 一定取到区间内所有整数。它只承诺：若前面的抽象信息可靠，w 的具体值不会跑出 [10, 16]。

为什么这是保守近似

抽象解释的关键是包含关系。

1
concrete_values <= abstract_value

抽象值必须覆盖所有具体可能。区间 [5, 15] 可以覆盖 5、6、7 等所有可能结果。即使它包含了一些实际走不到的值，也不会漏掉真实可能发生的值。

这就是静态分析的常见权衡：

目标 代价
不漏报风险 可能误报
分析能终止 结果不完全精确
覆盖更多程序 抽象更粗
结果更精确 分析更慢或更复杂

停机问题把“完备精确分析”挡住以后，工程工具就转向“可终止、可解释、足够有用”的近似分析。

Java 程序员的迁移表

抽象解释概念 Java 工程对照 说明
抽象域 类型、nullability、区间、污点标签 用小信息代表大集合
抽象环境 数据流事实表 每个变量的分析结果
抽象转移函数 flow function / transfer function 语句怎样改变分析事实
条件收窄 if (x != null) 后的类型收窄 分支内精化信息
保守近似 IDE warning / SAST 告警 可接受误报，避免漏掉风险

IDE 里常见的 “这里可能为 null”、“这个分支不可达”、“这个值可能越界” 都可以用类似思路解释。工具并不运行所有路径，而是在抽象域里模拟程序。

模式提炼：精确值换成可计算事实

1
precise_execution -> abstract_execution

抽象解释把不可承受的精确执行换成可计算事实。事实越粗，分析越快但误报更多；事实越细，分析越精确但实现成本更高。

分析目标 常见抽象
空指针 null / non-null / unknown
数组越界 index interval
SQL 注入 tainted / clean
权限检查 authorized / unknown
资源泄漏 open / closed / maybe

这些抽象不需要复刻完整运行时，只需要对目标问题保留足够信息。

当前模型的边界

本文示例没有循环、分支合并和无限区间。真实抽象解释需要处理更多问题：

第一，分支合并需要 join 操作，例如把 [0, 5] 和 [10, 20] 合成 [0, 20]。

第二，循环需要不动点计算。分析器要反复执行抽象转移，直到结果稳定。

第三，区间可能发散，需要 widening 让分析在有限时间内结束。

这些内容足以独立展开。本文只保留最小路径：用区间展示“保守近似怎样代替精确执行”。

练习

第一，给 Interval 增加 subtract，实现 x - y 的抽象结果。

第二，增加 join 方法，把两个区间合并成覆盖两者的区间。

第三，把 meet_less_than 改成同时处理空区间，观察 z < 0 会发生什么。

第四，设计一个 nullability 抽象域：NULL、NON_NULL、UNKNOWN。

参考资料