Meta已经发布了超过10万个由静态分析器在代码到达用户之前捕获的缺陷修复。这个工具名为Infer，它是开源的，并且不会运行您的代码。它读取代码，构建代码可能执行的数学模型，并证明某些坏事不可能发生。或者它会找到一条可能发生的路径。

这项技术是抽象解释。它听起来很学术，因为它确实是。帕特里克·库索和拉迪亚·库索在20世纪70年代发明了它，作为不执行程序就能推理程序的方法。彼得·奥汉恩领导的Meta团队采用了这一理论，并将其速度提升到足以在几分钟内分析数百万行移动和服务器代码。结果是一个在差异提交时就发现空指针解引用、内存泄漏、资源泄漏和竞态条件的工具。

问题：动态测试无法覆盖您没想到要运行的路径

单元测试检查代码中的一条路径。集成测试再多检查几条。但一个包含五个条件语句和两个循环的函数有数百条路径，其中大多数在测试套件中从未被执行。

动态测试，即运行代码，只能在您实际执行的路径上发现缺陷。静态分析在您从未想到过的路径上发现缺陷。这就像是用手电筒挨个房间检查入侵者，与证明所有门窗都已上锁之间的区别。

挑战在于，证明真实程序中的事情是困难的。真实程序有循环、递归、堆分配和并发。您无法枚举每个状态。抽象解释通过近似来解决这个问题。

抽象解释的实际含义

抽象解释通过用抽象值而不是具体值来运行程序。

在正常执行中，变量 x 可能保存整数 42。在抽象解释中，x 可能保存抽象值”正数”。分析器不知道 x 是42。它知道 x 大于零。这足以证明如果 y 也是正数，x / y 不会除以零。但这不足以证明 x == 42。抽象解释用精确性换取可计算性。

抽象值的集合称为抽象域。最简单的域是符号域：每个变量为负、零、正或未知。更复杂的域跟踪范围、指针或内存位置是否已被释放。分析器遍历程序，应用每次操作的抽象版本，直到抽象状态停止变化。此时，它找到了一个不动点，即每个程序点处每个可能具体状态的近似值。

循环是难点。一个循环可能运行零次、一次或十亿次。分析器无法将其展开十亿次。相反，它应用一个扩展算子，跳转到过度近似。如果一个变量每次迭代增加一，分析器可能将其抽象值从”正数”扩展为”非负数”并在那里停止。它失去了确切的界限，但保留了证明所需的关键属性。

Infer如何利用双向推理模块化地分析过程

传统的抽象解释将整个程序作为一个整体来分析。这对于有百万行代码的移动应用来说无法扩展。Infer通过一种称为双向推理的技术解决了这个问题。

双向推理让Infer一次分析一个函数。当Infer分析一个函数时，它会发现两件事：函数安全所必须满足的前置条件，以及函数保证的后置条件。这些是自动推断的，而不是由程序员编写的。

下面是一个具体示例。假设Infer看到这个C函数：

void greet(struct Person* p) {
    printf("Hello, %s\n", p->name);
}

Infer推断 greet 要求 p 非空。这就是前置条件。它还推断 greet 不会释放 p 或修改任何可见状态。这就是后置条件。当另一个函数调用 greet 时，Infer会根据推断的前置条件检查调用者。如果调用者可能传递空值，Infer就会报告一个缺陷。

双向推理引擎通过分离逻辑上的符号执行来工作。分离逻辑让Infer能够推理堆所有权：哪个函数拥有哪个内存，以及该内存是否已被释放。这就是Infer擅长在C、C++、Objective-C和Java中发现空指针解引用和内存泄漏的原因。

Infer能捕获什么以及遗漏什么

Infer不是通用的代码检查工具。它针对的是动态发现成本高且在投产中危险的特定缺陷类别。

空指针解引用。 Infer跟踪每个指针是确定为空、确定为非空，还是可能为空。对可能为空的指针进行解引用会触发报告。在Java和Objective-C中，这捕获了最常见的崩溃类型。

内存泄漏。 Infer使用分离逻辑来跟踪堆所有权。如果一个函数分配了内存，却没有释放它或将其返回给调用者，Infer就会报告泄漏。这在C和C++代码库中特别有价值，因为泄漏会在数周的运行时间内累积。

资源泄漏。 文件描述符、套接字和锁也以类似方式被跟踪。如果一个函数打开了一个文件，却在每条路径上都没有关闭它就返回，Infer就会报告泄漏。

竞态条件。 Infer的RacerD模块分析Java并发性。它跟踪哪些线程访问哪些字段，以及这些访问是否受到锁的保护。两个线程在没有同步的情况下访问同一个字段就是一种竞态。

Infer并不能捕获所有缺陷。它会遗漏需要对数值精度、字符串内容或复杂别名模式进行推理的缺陷。它在设计上也是不健全的：为了保持低误报率，它可能会遗漏缺陷。一个在每次差异提交时都喊狼来了的静态分析器会被禁用。Meta的内部部署将Infer的误报率控制在10%以下，这就是开发人员真正会对其报告采取行动的原因。

在您的代码上运行Infer

Infer是开源的，支持C、C++、Objective-C、Java，以及（实验性地）Rust和Swift。最简单的尝试方式是在Java或C项目上。

通过Homebrew或Docker安装Infer：

# macOS
brew install infer

# Or via Docker
docker run --rm -v $(pwd):/repo infer/infer infer run -- make -C /repo

对于使用Maven的Java项目：

infer run -- mvn compile

对于使用Make的C项目：

infer run -- make

Infer会编译您的代码，构建控制流图，并运行分析。输出是一组带有文件名、行号和被违反的推断前置条件的缺陷报告。

下面是一个Infer会标记的最小C示例：

// leak.c
#include <stdlib.h>

int* allocate_but_leak(void) {
    int* p = malloc(sizeof(int));
    *p = 42;
    // forgot to return p or free it
    return NULL;
}

运行 infer run -- cc leak.c 会产生：

leak.c:5: error: MEMORY_LEAK
  memory dynamically allocated by call to `malloc()` at line 5 is not reachable after line 7

Infer还会捕获下面这个示例中的空指针解引用：

// null.c
#include <stdio.h>

void print_length(const char* s) {
    if (s != NULL) {
        printf("%zu\n", strlen(s));
    }
}

void unsafe_call(void) {
    print_length(NULL);  // Infer reports this
}

等等，实际上Infer不会报告上面的情况。print_length 函数安全地处理了空参数。Infer只在可能为空的指针在没有检查的情况下被解引用时才会报告。下面是一个会触发的情况：

// null_bad.c
#include <stdio.h>

void unsafe_print(const char* s) {
    // No null check before dereference
    printf("first char: %c\n", s[0]);
}

void call_unsafe(void) {
    unsafe_print(NULL);  // Infer reports this
}

Infer追踪从 call_unsafe 经过 unsafe_print 的路径，并报告在计算 s[0] 时 s 为空。

权衡：速度与精度

Infer的模块化设计使其快到足以在Meta的每次拉取请求上运行。但模块化会引入近似。当Infer分析一个函数时，它不知道确切的调用上下文。它推断的前置条件是保守的，意味着它们可能比必要的更强。更强的前置条件意味着在调用点报告的缺陷更少，但误报也更少。

这是静态分析中的核心张力。一个健全的分析器会报告每个缺陷，但会让您淹没在误报中。像Infer这样的不健全分析器通过只报告它有把握的缺陷来让开发人员满意。它遗漏的缺陷就是采用的代价。

Infer的双向推理引擎也难以处理全局状态和复杂的回调。如果您的Java代码将匿名内部类传递给执行器，Infer可能会丢失哪个线程运行哪个方法的跟踪。RacerD处理常见模式，但会遗漏涉及条件变量或原子字段的微妙竞态。

何时采用静态分析，何时跳过

如果您发布的是原生代码、移动应用或C族语言或Java的服务器代码，您应该考虑使用Infer。它发现的缺陷——空指针解引用、泄漏、竞态——正是导致投产崩溃和安全漏洞的那些。

您不应该期望Infer取代您的测试套件。静态分析和动态测试是互补的。测试验证您的代码在您选择的输入上做了您打算做的事情。静态分析验证您的代码在任何输入上都没有做您禁止的事情。

如果您的代码库是Python、Ruby或JavaScript，Infer不是合适的工具。这些语言缺乏Infer用来构建其抽象模型的静态类型信息。对于动态语言，像mypy或pyright这样的类型检查器会捕获不同类别的错误。

结论

Meta的10万个缺陷修复不是一个营销数字。它是一个在每次差异提交时运行、在不执行代码的情况下分析代码、并报告任何测试都无法捕获的缺陷的工具的产出。底层技术抽象解释已有数十年的历史。工程成就在于让它快到足够精确，以至于开发人员不会关掉它。

您不需要Meta的基础设施就能受益。安装Infer，指向您的构建系统，然后在一个让您担心的模块上运行它。内存管理模块、并发层、C互操作边界。修复它发现的泄漏和空指针解引用。然后将其添加到CI中，防止缺陷数量增长。

抽象解释不是魔法。它是应用于代码的数学，带有所有随之而来的近似和权衡。但它是能在真实代码库中发现真实缺陷的数学，这使它值得了解。