16.4 为什么完美静态分析不可能

静态分析（static analysis）在不实际执行程序每种可能运行分支的情况下，预测并判定程序在运行时的行为。编译器（Compiler）依靠它来完成诸如常量传播（constant propagation）、活跃变量分析（liveness）、指针别名分析（aliasing）、数组边界检查（bounds check）、死代码消除（dead-code elimination）、代码问题诊断（diagnostic）、安全漏洞扫描与逻辑正确性验证（verification）。这些分析手段虽然极其有用，但在数学上，对于任意图灵完备程序（arbitrary program）的完美分析器（perfect analyzer）是不可能同时满足“总是保证停机”且“能够对每一个非平凡的语义问题（non-trivial semantic question）给出百分之百精确的回答”的。

其直观的理论原因在于：任何对图灵完备语言（Turing-complete program）的分析模型都可以被用于编码和执行另一个任意的图灵机。假设在世界上存在一个完美的静态分析器，它总是能够判定任意程序中的某个特定函数 target() 最终是否会被执行。那么对于任意给定的图灵机描述 M 及其输入 w，我们便可故意构造一个包裹函数（wrapper）：该调用首先负责模拟执行 M(w)，且有且仅当模拟运行正常停机后，才去调用目标函数 target()。此时，这个完美的静态分析器就可以被用来一举判定停机问题（halting problem）。由于停机问题已经被严格证明是不可判定的，因此这种在全局上完美且精准的静态分析器也绝对不可能存在。

莱斯定理（Rice's theorem）将这一不可能性推广到了极致：任意图灵完备程序所计算得到的偏函数（partial function）中，每一个非平凡的语义属性（nontrivial semantic property）在数学上全都是彻底不可判定的。“该程序是否总是返回零”、“该程序是否会接受至少一个输入数据”以及“该程序计算得出的结果是否与声明的技术规格设计完全相同”全都是此类不可能判定的命题。当然，莱斯定理也给出了可判定的边界——如果只判定纯粹的语法属性（syntactic property）（例如：源码中是否包含某个特定的 token、生成的抽象语法树 AST 中是否包含某一特定类型的 node），则是完全可判定的。

精确的路径推理（Path Reasoning）很快就会超出计算资源

即便我们在工程中先退一步，暂不考虑数学上根源的不可判定性（undecidability），即便是在代码行数有限的有界程序中，繁多的执行路径也会带来极高维度的复杂度。n 个相互独立的条件分支（branches）在理论上可以直接产生多达 2^n 条不同的执行路径（paths）；哪怕一个最简单的循环（loop）也会产生无界的执行路径家族；嵌套函数调用（call）乘以调用上下文又会带来爆炸性的上下文敏感关联；在堆上分配的内存（heap allocation）与多重别名指针（aliasing）会迅速无限放大运行状态之间的关联格局；若是再引入并发（concurrency）和多线程，又会在控制流路径之外引入呈几何级数膨胀的各线程间随机指令调度交错（schedule interleavings）。

符号执行（Symbolic execution）技术使用特定的符号值来代替原始的输入数据，并沿着执行路径层层累积路径约束（path constraints）。在实践中，它可以借助 SMT 求解器（solver）来快速剪掉不符合现实的可行分支（infeasible branch）、合并语义等价的内存状态、对循环次数设置硬性的有界硬阈值、对复杂的函数生成调用总结，并优先探索极具分析前途的关键代码段路径。然而，每一次优化技术的选择都在以牺牲分析的精确度（precision）、完备性（completeness）或底层计算开销（cost）为代价。SMT 求解器返回不确定（unknown）也并不属于工具本身开发质量差：因为某些算术关系理论（theory）在数学上原本就是极其困难甚至彻底不可判定的，而生产级求解器自身还必须配备绝对安全的执行时间与物理内存上限（time/memory limit）。

抽象解释（Abstract Interpretation）计算安全近似（sound approximation）

抽象解释（abstract interpretation）使用特定的抽象域（abstract domain），来有界替换原本无限且难以追踪的具体状态空间（concrete state space）。例如，区间域（Interval domain）把变量的值映射到 [0, 10] 等特定的数值区间，而不是去记录运行的每一个具体整数；符号域（sign domain）则只追踪数值的 负数/零/正数 符号特征；指向分析域（points-to domain）则近似表达多重指针可能指向的所有堆内存目标。转换函数（Transfer function）严密描述了每一条底层指令（instruction）应当如何变换现有的抽象状态值（abstract fact），而合流算子（join）则负责在各条控制流路径的汇合点安全合并分析事实。

对于追求零漏报的安全性证明分析（safety analysis），抽象机制通常会执行过近似（over-approximate）：即能保证代表了程序运行的每一个具体的可能物理行为，但也可能会悲观地引入该代码在现实中不可能会发生的虚无行为。这极利于做出安全的警告与证明（sound proof）。例如，若除数 d 在分析出的抽象区间内彻底排除了零，分析器就能斩钉截铁地向开发者证明该处绝不会发生被零除故障（division-by-zero）；然而如果计算出的区间包含了零，静态分析器（analyzer）就必须发出安全警告，哪怕多变量之间的隐含约束关系在实际执行中使得除数绝对不可能为零——这就是分析精度（precision）丢失所必然带来的虚警/误报（false positive）。

分析循环迭代（loop）的代码则需要求取数学上的不动点（fixed point）。在单调递增（monotone）的转换函数作用下，有限高度的抽象域（Finite-height domain）可以保证迭代一定会快速收敛；但在诸如 [0,0]、[0,1]、[0,2] ... 这样具有无限上升链（infinite ascending chain）的区间域中，分析为了防止陷入死循环，必须强行使用加宽算子（widening），直接跃迁跳跃到 [0,+∞] 等稳定的安全过近似事实。之后，变窄收缩阶段（narrowing phase）可巧妙利用循环的守卫条件（loop guard）收回部分悲观丢失的约束。Widening 的调用时机与抽象域设计（domain design）会强烈影响最终的分析精度和运行时间。

可靠性、完备性与终止性（Termination）不可兼得

针对具体的缺陷发现属性（bug properties）而言，可靠性（soundness）通常意味着在建模拟下的分析域中绝对不会漏掉任何一个真实的 bug，为此不惜允许误报（false positive）；完备性（completeness）则意味着每一个报告的错误都必定对应着一个在特定输入下一定会真实发生的 bug，为此绝不容许出现误报（false positive）。在具体讨论安全证明（safety proof）或缺陷凭证（bug witness）时，这两个术语在不同场景下的引申方向可能会发生变化，因此任何静态分析器都必须极为明确地宣示自己的契约（contract）。

面对具有强表达力的丰富图灵完备程序，一个能在有限时间内终止的分析算法（terminating analysis）在理论上逆向来看，不可能同时做到完美的可靠（sound）且完备（complete）。在实践中，所有的工业级工具都必须根据业务重心进行选择折中：安全校验器（sound verifier）在由于数值精度丢失而无法严格证明安全时，选择向用户诚实地返回不确定/警告（unknown/warning）；缺陷查找器（bug finder）则主动牺牲可靠性保证（即允许漏报），以此换取极少、且极高置信度的精准缺陷报告（issue）；有界模型检测器（bounded checker）保证仅在给定的有界阈值限制（limits）内提供完美的精确；而动态运行时净化器（dynamic sanitizer）则完全放弃静态探查，仅在实际执行的代码路径（paths）上收集最确凿、具体的内存破坏物理证据（concrete evidence）。

此外，分析依据的具体契约模型也极为重要。一个分析器（Analyzer）在数学上可能针对某种特定内存模型（memory model）下的顺序单线程代码（sequential code）是绝对可靠的（sound），但如果在工业界实现中由于贪图简单，而宽泛乐观地对反射（reflection）、底层原生代码调用（native call）、多线程并发下的数据竞争（data race）或语言未定义行为（undefined behavior）进行了脱离物理现实的粗糙忽略建模，其最终在应用中依然会集于不确实（unsound）。“可靠（Sound）”在技术世界中永远只能代表：相对于声明的语言规范精确语义（language semantics）与环境条件假设（environmental assumptions）而言是可靠的。

优秀的现代工具应当非常大方地向用户沟通并具化所有的“计算不确定性（uncertainty）”：将分析结果清晰地细分为：已经明确的绝对缺陷（definite error）、可能的潜在错误（possible error）、当前尚未证实的约束契约（unproved obligation）、由于超时（timeout）而中断的分析、暂不支持的高级语言功能（unsupported feature）以及预设的前提假设契约（assumed contract），并主动提供供用户直接检查的清晰代码排查路径或归纳不变量（trace/invariant）。数学上的理论边界并没有把静态推理（static analysis）贬低为无端的盲目猜测：它深刻地启示了我们——在面对不可判定的深渊时，唯有高度局部的透明近似估计（approximation）与合理限定的契约保证（guarantee），才是一切强大且备受程序员信赖的现代编译器静态推理体系与编译器辅助工具（compiler tooling）的诚实物理工程基石。