Теория языков программирования
Статический анализ программ
Facebook Infer запущен на каждом pull request в Facebook, Instagram, WhatsApp, Messenger. 75% найденных им багов подтверждаются разработчиками как реальные. Это 75% signal при масштабе миллиардов строк кода.
- **Airbus A380**: Astree (абстрактный интерпретатор) верифицировал flight control software. Ноль false positives на 130K строк C - практически невозможное достижение
- **Facebook Infer**: 75% precision при анализе PR. Нашёл resource leaks и null dereferences до code review в крупнейших мобильных приложениях мира
- **Clang Static Analyzer**: встроен в Xcode. Apple использует для нахождения memory leaks в Objective-C/Swift. Каждый macOS/iOS разработчик использует это ежедневно
Абстрактная интерпретация
Абстрактная интерпретация - математическая основа статического анализа. Вместо конкретных значений (x=42) используются абстрактные домены (x > 0, x ∈ [1..100]). Анализ sound: если не предупреждает - точно нет ошибки. Цена: ложноположительные предупреждения (false positives).
Astree - абстрактный интерпретатор для C. Верифицировал Airbus A380 primary flight control software (130K строк C) без false positives. Это практическое применение абстрактной интерпретации.
Почему статический анализ на основе абстрактной интерпретации может давать false positives?
Dataflow Analysis
Dataflow analysis вычисляет информацию о данных в каждой точке программы. Forward analysis (что true при входе в BB) и backward analysis (что необходимо при выходе из BB). Итеративное вычисление до fixed point на CFG.
Почему live variable analysis использует backward traversal CFG?
Pointer Analysis
Pointer analysis (alias analysis) - определение: могут ли два указателя указывать на одну и ту же память? Критически важно для оптимизаций. Andersen-style analysis (flow-insensitive, context-insensitive) - базовый алгоритм, O(n^3) сложность.
Почему alias analysis критичен для векторизации (SIMD)?
Линтеры и static analyzers
Промышленные статические анализаторы: Clang Static Analyzer (Cocoa, C++), Infer (Facebook, Java/C/Obj-C), Semgrep (многоязыковой). Применяют ограниченные формы dataflow и pointer analysis для нахождения реальных багов с приемлемым числом false positives.
Статический анализ заменяет тестирование
Статический анализ и testing дополняют друг друга. Анализ находит классы ошибок (null deref, resource leak) для всех путей. Тесты проверяют конкретное поведение
Infer может найти null dereference которое происходит только в определённой последовательности 10 вызовов. Эти пути сложно покрыть тестами. Но тесты проверяют бизнес-логику которую анализ не понимает
Чем Semgrep отличается от традиционных статических анализаторов?
Итоги
- **Абстрактная интерпретация**: абстрактные домены вместо конкретных значений. Sound (нет false negatives) но с false positives
- **Dataflow analysis**: forward (reaching definitions) и backward (live variables). Итерация до fixed point на CFG
- **Pointer/alias analysis**: могут ли два указателя быть одной ячейкой? Критично для SIMD оптимизаций и restrict
- **Линтеры**: Infer (bi-abduction, heap), Semgrep (AST patterns), Clang SA. Дополняют тесты, не заменяют
Связанные темы
Статический анализ применяет теорию к практике:
- IR и оптимизации — Alias analysis и dataflow используются в оптимизациях компилятора
- Property-based testing — Static analysis и property testing - дополняющие подходы к верификации
Вопросы для размышления
- Абстрактная интерпретация sound но не complete - Astree не даёт false negatives. Почему complete анализ (без false positives) невозможен по теореме Райса?
- Rust borrow checker - это форма статического анализа с нулевым runtime overhead. Как он избегает false positives при проверке lifetimes?
- Facebook Infer запускается на каждом PR. Как компания решает проблему разработчиков которые игнорируют предупреждения анализатора?