Abstract interpretation — это тот термин, от которого инженеры закрывают вкладку. Звучит так, будто нужен семестр теории решёток, чтобы понять. Большинство разработчиков предполагают, что это живёт в научных статьях, а не в pull request.

Это предположение дорого обходится. Abstract interpretation — это просто способ доказывать вещи о вашем коде без его выполнения. Инструменты, построенные на ней, могут ловить null dereference, утечки памяти и race conditions, которые пропускают type checker и linter. Хорошая новость: вам не нужно понимать связи Галуа, чтобы использовать её. Нужен рабочий CI-конфиг и около двадцати минут.

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

По сути, abstract interpretation — это автоматизированная техника доказательства. Она запускает вашу программу, но вместо реальных значений использует приближения.

Рассмотрим переменную x. При нормальном выполнении x может содержать 42. При abstract interpretation x может содержать “положительное целое”. Анализ отслеживает эти абстрактные значения через каждый возможный путь кода. Если он может доказать, что ни один путь не ведёт к null dereference, вы в безопасности. Если он находит путь, где x могла бы быть null на сайте разыменования, он сообщает о потенциальном баге.

Магия в том, что это работает для циклов и условий. Анализатор вычисляет fixed points над абстрактными состояниями, чтобы рассуждать о неограниченной итерации, не итерируясь на самом деле вечно. Это то, что отличает abstract interpretation от более простых инструментов символьного выполнения, которые испытывают трудности с циклами.

Infer от Facebook — самый доступный production-инструмент, использующий эту технику. Он анализирует Java, C, C++ и Objective-C, компилируя ваш код в промежуточное представление и запуская compositional abstract interpretation на каждой функции. Infer кэширует результаты по функциям, поэтому инкрементальные сборки быстры. Это секретный соус, который делает его жизнеспособным в CI.

Почему вашего linter недостаточно

Linter смотрят на синтаксис. Type checker смотрят на типы. Abstract interpretation смотрит на поведение через пути.

Linter может отметить, что вы забыли проверить на null. Type checker может обеспечить, чтобы функция возвращала Optional<T>. Но ни один не может надёжно поймать, что вы разыменовываете указатель на строке 47 после сложной серии ветвлений, где один путь оставляет его неинициализированным. Abstract interpretation отслеживает возможные состояния этого указателя через каждую ветвь и точку слияния.

Компромисс — шум. Abstract interpretation производит false positives. Она может сообщить о null dereference, который ваша бизнес-логика гарантирует, что никогда не случится. Анализатор не знает ваших инвариантов. Он знает только то, что код буквально позволяет.

Default checker Infer настроены на поддержание низкого уровня false positives, около 10-15% для большинства codebases. Это выше, чем у type checker, но баги, которые он находит, часто те, что проскальзывают через code review и тестирование.

Добавление Infer в CI-пайплайн

Вам не нужно собирать Infer из исходников. Facebook публикует Docker-образы. Вот рабочий workflow GitHub Actions, который анализирует Java-проект:

# .github/workflows/infer.yml
name: Abstract Interpretation

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Run Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "mvn compile"
            --
            mvn compile

      - name: Upload report
        uses: actions/upload-artifact@v4
        with:
          name: infer-report
          path: infer-out/report.json

Для проекта Node.js или Python поменяйте команду сборки. Infer не анализирует нативно JavaScript или Python, но вы можете запустить его на C/C++ расширениях, от которых эти проекты часто зависят. Если вы находитесь в чисто управляемой языковой среде, вы всё ещё можете получить аналогичный path-sensitive анализ от инструментов вроде CodeQL или SonarQube, хотя их базовые движки отличаются.

Для проектов на C или C++ настройка ещё проще:

# .github/workflows/infer-cpp.yml
name: Infer C++ Analysis

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Build with Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "make"
            --
            make

Паттерн infer run --make-command перехватывает вызовы компилятора во время вашего обычного процесса сборки. Infer извлекает промежуточное представление, анализирует его и записывает результаты в infer-out/. Ваши реальные артефакты сборки не затронуты.

Чтение вывода и настройка false positives

Infer выводит результаты в infer-out/report.json и человекочитаемый infer-out/report.txt. Типичное обнаружение выглядит так:

src/parser.c:142: error: NULL_DEREFERENCE
  pointer `node` last assigned on line 138 could be null and is dereferenced at line 142, column 5

Сообщение говорит вам переменную, где она была присвоена и где происходит разыменование. Вы можете проследить путь в своём редакторе.

Если Infer слишком шумный, вы можете подавить конкретные checker или аннотировать код, чтобы пропустить анализ:

// src/parser.c
// infer-ignore: the parent check guarantees node is non-null here
node->value = parsed;

Или отключить конкретные checker глобально:

infer run --make-command "make" --no-bufferoverrun --

Buffer overrun checker особенно склонен к false positives на коде со сложной арифметикой указателей. Обычно я отключаю его на legacy C codebases и оставляю активными checker null dereference и memory leak. Эти двое находят реальные баги на уровне, который оправдывает время ревью.

Компромисс времени сборки

Abstract interpretation не бесплатна. Полный запуск Infer на проекте C++ среднего размера может занять в 2-4 раза дольше обычной сборки. Инкрементальный анализ помогает: при последующих запусках Infer повторно анализирует только изменённые функции и их зависимости. На практике это означает, что 10-минутная сборка может стать 15-20 минут на чистом CI-запуске, но 3-5 минут на инкрементальных запусках.

Если ваш CI-бюджет ограничен, запускайте Infer на pull requests, но не на каждом push в main. Или запускайте его ночью. Баги, которые он находит, обычно стоят задержки, но правильная частота зависит от терпимости вашей команды к времени CI.

Ещё один вариант — запускать Infer локально перед push. Тот же Docker-образ работает на любой машине с установленным Docker:

docker run --rm -v $(pwd):/workspace -w /workspace \
  ghcr.io/facebook/infer:main \
  infer run --make-command "make" --

Что Infer не ловит

Infer композиционален. Он анализирует функции изолированно и использует summaries для моделирования callers и callees. Это делает его масштабируемым, но означает, что межфункциональные баги, чувствительные к путям, требующие анализа полного графа вызовов, могут проскользнуть.

Он также не находит логические баги. Если ваш код безопасно разыменовывает указатель, но использует неправильное значение, Infer молчит. Это checker безопасности, не oracle корректности.

Баги concurrency ограничены. У Infer есть checker race conditions, но он экспериментальный и производит достаточно false positives, чтобы большинство команд оставляли его выключенным.

Что делать дальше

Начните с малого. Выберите один проект на компилируемом языке и добавьте workflow GitHub Actions выше. Пусть он запускается на следующих нескольких pull requests. Просмотрите результаты со своей командой и постройте suppression list для шума.

Через неделю у вас будет понимание, стоит ли сигнал времени CI. По моему опыту, первый запуск на существующей C или Java codebase всегда находит хотя бы один null dereference, который code review пропустил. Обычно этого достаточно, чтобы оправдать его сохранение.

Если вы хотите углубиться, документация Infer охватывает написание custom checker на OCaml. Вот где PhD пригождается. Для всего остального default checker и Docker-образа достаточно.

FAQ

Что такое abstract interpretation простыми словами? Это техника статического анализа, которая приближает поведение вашей программы, чтобы доказывать свойства вроде “этот указатель никогда не null”, без фактического выполнения кода.

Infer бесплатен? Да. Infer — open source под лицензией MIT и поддерживается Meta.

Как Infer сравнивается с SonarQube? SonarQube использует смесь pattern matching, taint analysis и некоторого более глубокого анализа в зависимости от языка. Infer специально построен на abstract interpretation и является path-sensitive способами, в которых SonarQube обычно не является для C, C++, Java и Objective-C.

Могу ли я запускать Infer на JavaScript или Python? Не напрямую. Infer анализирует компилируемые языки. Для JavaScript и Python рассмотрите CodeQL или type-aware linters вроде ESLint со строгими правилами или Pyright.

Значительно ли Infer замедляет CI? Полный анализ занимает в 2-4 раза больше времени сборки. Инкрементальный анализ на pull requests намного быстрее, обычно добавляя несколько минут.