Meta выпустила более 100 000 исправлений багов, пойманных статическим анализатором до того, как код дошёл до пользователя. Инструмент называется Infer, он open source и не запускает ваш код. Он читает его, строит математическую модель того, что код мог бы делать, и доказывает, что определённые плохие вещи не могут произойти. Или находит путь, где они могут.

Техника — abstract interpretation. Звучит академично, потому что так и есть. Патрик Кузо и Радхия Кузо изобрели её в 1970-х как способ рассуждать о программах без их выполнения. Команда Meta под руководством Питера О’Хирна взяла теорию и сделала её достаточно быстрой, чтобы анализировать миллионы строк мобильного и серверного кода за минуты. Результат — инструмент, который находит null pointer dereference, утечки памяти, утечки ресурсов и race conditions на этапе diff.

Проблема: динамическое тестирование не может покрыть то, что вы не подумали запустить

Unit test проверяет один путь через код. Integration test проверяет ещё несколько. Но функция с пятью условиями и двумя циклами имеет сотни путей, и большинство из них никогда не исполняются в тестовых наборах.

Динамическое тестирование, то есть запуск кода, может найти баги только на путях, которые вы фактически выполняете. Статический анализ находит баги на путях, о которых вы никогда не думали. Это разница между проверкой дома на наличие злоумышленников обходом комнат с фонариком и проверкой путём доказательства, что все двери и окна заперты.

Сложность в том, что доказывать что-либо о реальных программах трудно. Реальные программы имеют циклы, рекурсию, heap allocation и concurrency. Нельзя перечислить каждое состояние. Abstract interpretation решает это приближением.

Что на самом деле означает abstract interpretation

Abstract interpretation работает, запуская программу на абстрактных значениях вместо конкретных.

При нормальном выполнении переменная x может содержать целое число 42. При abstract interpretation x может содержать абстрактное значение «положительное». Анализатор не знает, что x равно 42. Он знает, что x больше нуля. Этого достаточно, чтобы доказать, что x / y не поделит на ноль, если y тоже положительное. Недостаточно, чтобы доказать, что x == 42. Abstract interpretation жертвует точностью ради вычислимости.

Множество абстрактных значений называется abstract domain. Простейший домен — домен знаков: каждая переменная либо отрицательная, ноль, положительная, или неизвестная. Более сложные домены отслеживают диапазоны, указатели или было ли освобождено место в памяти. Анализатор итерирует по программе, применяя абстрактные версии каждой операции, пока абстрактное состояние не перестанет меняться. В этот момент он нашёл fixed point — приближение каждого возможного конкретного состояния в каждой точке программы.

Циклы — сложная часть. Цикл может выполниться ноль раз, один раз или миллиард раз. Анализатор не может развернуть его миллиард раз. Вместо этого он применяет widening operator, который прыгает к over-approximation. Если переменная инкрементируется на единицу за итерацию, анализатор может расширить её абстрактное значение с «положительное» до «неотрицательное» и остановиться. Теряется точная граница, но сохраняется свойство, важное для доказательства.

Как Infer использует bi-abduction для модульного анализа процедур

Традиционная abstract interpretation анализирует всю программу целиком. Это не масштабируется на мобильное приложение в миллион строк кода. Infer решает это техникой bi-abduction.

Bi-abduction позволяет Infer анализировать по одной функции за раз. Когда Infer анализирует функцию, он обнаруживает две вещи: preconditions, которые должны выполняться для безопасности функции, и postconditions, которые функция гарантирует. Они выводятся автоматически, а не пишутся программистом.

Вот конкретный пример. Предположим, Infer видит эту функцию на C:

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

Infer выводит, что greet требует, чтобы p был non-null. Это precondition. Он также выводит, что greet не освобождает p и не модифицирует видимое состояние. Это postcondition. Когда другая функция вызывает greet, Infer проверяет вызывающую сторону на соответствие выведенному precondition. Если вызывающая сторона может передать null, Infer сообщает о баге.

Движок bi-abduction работает через symbolic execution над separation logic. Separation logic позволяет Infer рассуждать о владении heap: какая функция владеет какой памятью, и была ли эта память освобождена. Именно это делает Infer хорошим в поиске null dereference и утечек памяти в C, C++, Objective-C и Java.

Что ловит Infer, а что пропускает

Infer — не универсальный линтер. Он нацелен на конкретные классы багов, которые дорого находить динамически и которые опасны в production.

Null pointer dereference. Infer отслеживает, является ли каждый указатель определённо null, определённо non-null или maybe null. Разыменование maybe-null указателя вызывает отчёт. В Java и Objective-C это ловит самый распространённый тип краша.

Утечки памяти. Infer использует separation logic для отслеживания владения heap. Если функция выделяет память и не освобождает её и не возвращает вызывающей стороне, Infer сообщает об утечке. Это особенно ценно в codebases на C и C++, где утечки накапливаются за недели аптайма.

Утечки ресурсов. File descriptors, sockets и locks отслеживаются аналогично. Если функция открывает файл и возвращается, не закрыв его на каждом пути, Infer сообщает об утечке.

Race conditions. Модуль RacerD Infer анализирует concurrency в Java. Он отслеживает, какие потоки обращаются к каким полям и защищены ли эти обращения locks. Два потока, обращающихся к одному полю без синхронизации, — это race.

Infer не ловит всё. Он пропускает баги, требующие рассуждений о числовой точности, содержимом строк или сложных паттернах aliasing. Он также by design unsound: может пропускать баги, чтобы держать false positives низкими. Статический анализатор, который кричит волк на каждом diff, отключается. Внутреннее развёртывание Meta держало уровень false positives Infer ниже 10%, поэтому разработчики реально реагируют на его отчёты.

Запуск Infer на собственном коде

Infer — open source и поддерживает C, C++, Objective-C, Java и (экспериментально) Rust и Swift. Самый простой способ попробовать — на Java или C проекте.

Установите Infer через Homebrew или Docker:

# macOS
brew install infer

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

Для Java проекта с Maven:

infer run -- mvn compile

Для C проекта с Make:

infer run -- make

Infer компилирует код, строит control-flow graph и запускает анализ. Вывод — набор отчётов о багах с именами файлов, номерами строк и нарушенным выведенным precondition.

Вот минимальный пример на C, который Infer отметит:

// 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 dereference в этом примере:

// 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 безопасно обрабатывает null-аргумент. Infer сообщает только когда dereference происходит на possibly-null указателе без проверки. Вот пример, который сработает:

// 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 — null, когда вычисляется s[0].

Компромисс: скорость против точности

Модульная архитектура Infer делает его достаточно быстрым для запуска на каждом pull request в Meta. Но модульность вносит приближение. Когда Infer анализирует функцию, он не знает точного calling context. Он выводит preconditions, которые консервативны, то есть могут быть сильнее, чем необходимо. Более сильный precondition означает меньше сообщаемых багов на месте вызова, но и меньше false positives.

Это центральное напряжение в статическом анализе. Sound analyzer сообщает каждый баг, но топит вас в false positives. Unsound analyzer вроде Infer держит разработчиков довольными, сообщая только баги, в которых он уверен. Баги, которые он пропускает, — цена adoption.

Би-abduction движок Infer также испытывает трудности с глобальным состоянием и сложными callback. Если ваш Java-код передаёт анонимный inner class в executor, Infer может потерять отслеживание того, какой поток выполняет какой метод. RacerD справляется с распространёнными паттернами, но пропускает тонкие races, связанные с condition variables или atomic fields.

Когда внедрять статический анализ, а когда пропустить

Стоит рассмотреть Infer, если вы поставляете нативный код, мобильные приложения или серверный код на языках семейства C или Java. Баги, которые он находит — null dereference, утечки, races — это именно те, что вызывают production crashes и уязвимости безопасности.

Не стоит ожидать, что Infer заменит ваш test suite. Статический анализ и динамическое тестирование дополняют друг друга. Тесты проверяют, что код делает то, что вы намеревались, на выбранных вами входных данных. Статический анализ проверяет, что код не делает того, что вы запретили, на любых входных данных.

Если ваша codebase на Python, Ruby или JavaScript, Infer — не тот инструмент. Эти языки не имеют статической типовой информации, которую Infer использует для построения абстрактной модели. Для динамических языков type checker вроде mypy или pyright ловят другой класс ошибок.

Вывод

100 000 исправлений багов Meta — не маркетинговое число. Это результат работы инструмента, который запускается на каждом diff, анализирует код без выполнения и сообщает о багах, которые не поймал бы ни один тест. Базовая техника, abstract interpretation, существует десятилетия. Инженерное достижение — сделать её достаточно быстрой и точной, чтобы разработчики не отключали её.

Не нужна инфраструктура Meta, чтобы получить пользу. Установите Infer, направьте на свою систему сборки и запустите на модуле, который вас пугает. Модуль управления памятью, concurrency-слой, граница C interop. Исправьте утечки и null dereference, которые он найдёт. Затем добавьте в CI и не давайте счётчику багов расти.

Abstract interpretation — не магия. Это математика, применённая к коду, со всеми приближениями и компромиссами, которые это влечёт. Но это математика, которая находит реальные баги в реальных codebases, и это делает её стоящей знать.