Ваш набор тестов проходит. Ваш type checker зелёный. Вы выкладываете в прод. Через два часа продакшен выдаёт IndexError на граничном случае, который никому не пришло в голову протестировать.

Тесты находят баги. Типы предотвращают некоторые из них. Ни то, ни другое не доказывает, что ваша программа свободна от ошибок времени выполнения. Для этого нужно нечто более сильное: способ рассуждать о всех возможных выполнениях сразу, не запуская код.

Абстрактная интерпретация — это техника, которая делает это возможным. Она лежит в основе статических анализаторов внутри Astrée, Infer от Facebook и гарантий корректности в borrow checker Rust. Она же объясняет, почему большая часть маркетинга статических анализаторов о «нулевом количестве ложных срабатываний» — ложь.

Ошибки времени выполнения — это проблема достижимости

Ошибка времени выполнения — это просто операция, которая достигает плохого состояния. Деление на ноль, разыменование null, переполнение буфера, выход за границы индекса. Каждая из них происходит потому, что выполнение достигает точки программы, где операция небезопасна.

Чтобы доказать отсутствие ошибок времени выполнения, нужно доказать, что каждая небезопасная операция недостижима в каждом возможном выполнении. При любых входных данных. В любой ветке. На любой итерации цикла.

Исчерпывающее тестирование невозможно для чего-либо, кроме игрушечных программ. Символьное выполнение плохо масштабируется, потому что взрыв числа путей вас убивает. Абстрактная интерпретация идёт другим путём: она отказывается от знания точных значений и вместо этого отслеживает приблизительные свойства, которые гарантированно покрывают каждое реальное выполнение.

Что на самом деле делает абстрактная интерпретация

Абстрактная интерпретация была введена Патриком и Радией Кузо в 1976 году. Ключевая идея прекрасно проста: запускайте программу, но вместо вычислений с реальными числами, строками и указателями вычисляйте с абстрактными представлениями, которые завышают (over-approximate) реальные значения.

Представьте это как замену конкретного выполнения «теневым» выполнением, которое отслеживает свойства, важные для вас. Вместо того чтобы знать x = 42, вы можете знать x > 0. Вместо того чтобы знать, что arr имеет длину 10, вы можете знать, что arr не пуст.

Ключевое ограничение — корректность (soundness). Каждое конкретное состояние должно быть представлено некоторым абстрактным состоянием. Если абстрактное выполнение говорит, что операция безопасна, то каждое конкретное выполнение, которое оно представляет, безопасно. Цена — точность: если абстрактное состояние слишком расплывчатое, вы получаете ложные срабатывания (предупреждения о безопасных операциях).

Конкретный пример: интервальный анализ

Вот минимальный абстрактный интерпретатор, который доказывает невозможность деления на ноль. Он отслеживает возможный диапазон каждой переменной с помощью интервалов.

# A tiny abstract interpreter for interval analysis
from dataclasses import dataclass
from typing import Dict

@dataclass(frozen=True)
class Interval:
    lo: float
    hi: float

    def __contains__(self, val: float) -> bool:
        return self.lo <= val <= self.hi

TOP = Interval(float("-inf"), float("inf"))

def eval_expr(env: Dict[str, Interval], expr) -> Interval:
    if isinstance(expr, int):
        return Interval(float(expr), float(expr))
    if isinstance(expr, str):
        return env.get(expr, TOP)
    if expr[0] == "+":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        return Interval(l.lo + r.lo, l.hi + r.hi)
    if expr[0] == "-":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        return Interval(l.lo - r.hi, l.hi - r.lo)
    if expr[0] == "*":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        products = [l.lo * r.lo, l.lo * r.hi, l.hi * r.lo, l.hi * r.hi]
        return Interval(min(products), max(products))
    if expr[0] == "/":
        l = eval_expr(env, expr[1])
        r = eval_expr(env, expr[2])
        if r.lo <= 0 <= r.hi:
            raise ValueError("Possible division by zero")
        return TOP
    raise ValueError(f"Unknown expr: {expr}")

def merge_envs(env1: Dict[str, Interval], env2: Dict[str, Interval]) -> Dict[str, Interval]:
    keys = set(env1) | set(env2)
    result = {}
    for k in keys:
        a = env1.get(k, TOP)
        b = env2.get(k, TOP)
        result[k] = Interval(min(a.lo, b.lo), max(a.hi, b.hi))
    return result

def analyze(program, env: Dict[str, Interval]) -> Dict[str, Interval]:
    env = dict(env)
    for stmt in program:
        if stmt[0] == "assign":
            _, var, expr = stmt
            env[var] = eval_expr(env, expr)
        elif stmt[0] == "if":
            _, cond, true_branch, false_branch = stmt
            t_env = analyze(true_branch, dict(env))
            f_env = analyze(false_branch, dict(env))
            env = merge_envs(t_env, f_env)
        elif stmt[0] == "while":
            _, cond, body = stmt
            old = dict(env)
            for _ in range(10):
                new = analyze(body, dict(old))
                changed = False
                for k in set(old) | set(new):
                    prev = old.get(k, TOP)
                    curr = new.get(k, TOP)
                    widened = Interval(min(prev.lo, curr.lo), max(prev.hi, curr.hi))
                    if widened.lo != prev.lo or widened.hi != prev.hi:
                        changed = True
                    old[k] = widened
                if not changed:
                    break
            env = old
    return env

# Example program: y = 10 / (x + 1) where x >= 0
program = [
    ("assign", "t", ("+", "x", 1)),
    ("assign", "y", ("/", 10, "t")),
]

# This should pass: x >= 0 means t >= 1, so no division by zero
safe_env = analyze(program, {"x": Interval(0, 100)})
print("Safe env:", safe_env)

# This should fail: x could be -1
try:
    bad_env = analyze(program, {"x": Interval(-5, 5)})
except ValueError as e:
    print("Caught:", e)

Запустите его. Первый случай доказывает безопасность, потому что интервал для t равен [1.0, 101.0], что исключает ноль. Второй случай корректно помечает риск, потому что t может быть равен нулю, когда x равен -1.

Обработчик if объединяет обе ветки, беря объединение интервалов. Обработчик while итерируется, пока интервалы перестанут расти (неподвижная точка). Это сердце абстрактной интерпретации: вы жертвуете точными значениями ради гарантированных завышенных приближений, и доказываете безопасность, показывая, что плохое состояние лежит за пределами приближения.

Где это ломается: стена точности

Пример выше — игрушечный. В реальных программах есть псевдонимы, рекурсия, распределение памяти в куче и циклы с зависящими от данных границами. Каждый из них разрушает точность предсказуемым образом.

Рассмотрим цикл, который инкрементирует i от 0 до 100. Наивный интервальный анализ может расширить i до [0, +inf) и никогда не восстановить верхнюю границу. Нужны реляционные домены (такие как полиэдры или октаэдры), чтобы отслеживать, что i <= 100. Эти домены имеют кубическую или экспоненциальную сложность от числа переменных. Для программы с 1000 переменными вы не запустите анализ полиэдров.

Именно поэтому коммерческие инструменты делают разный выбор. Astrée использует тщательно подобранную решётку абстрактных доменов, настроенную вручную для встраиваемого C. Infer использует логику разделения (separation logic) и би-абдукцию для масштабирования на миллионы строк мобильного кода, но отказывается от корректности для некоторых особенностей языка. Borrow checker Rust по сути является абстрактным интерпретатором с одним, чрезвычайно точным доменом: владение (ownership).

Компромиссы, которых нельзя избежать

Корректность, точность и масштабируемость. Выберите два.

Звуковой анализатор с высокой точностью не масштабируется дальше small modules. Масштабируемый, корректный анализатор утопит вас в ложных срабатываниях. Масштабируемый, точный анализатор пропустит реальные баги.

Ваш выбор абстрактного домена — это ручка настройки. Интервалы быстрые и неточные. Полиэдры точные и медленные. Абстракция предикатов находится посередине и лежит в основе большинства верификаторов программного обеспечения.

Как на самом деле это использовать

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

Для C и встраиваемых систем Astrée и Frama-C — это зрелые варианты. Плагин EVA Frama-C выполняет интервальный и памятный анализ на реальном коде C.

Для Rust система типов уже кодирует абстрактный домен владения. Miri — интерпретатор, а не абстрактный интерпретатор, но он ловит неопределённое поведение, которое пропускает система типов.

Для кода общего назначения Infer от Meta — это ближайшая к масштабируемому абстрактному интерпретатору вещь для Java, C++ и Objective-C. Он находит реальные баги с разыменованием null и утечками памяти в production codebases.

Если хотите поэкспериментировать, начните с простого анализа знаков или интервального анализа на языке, который распарсите сами. Dragon Book освещает анализ потока данных. Книга Nielson и Nielson Principles of Program Analysis — это стандартная ссылка на абстрактную интерпретацию в частности.

Доказательство отрицания

Абстрактная интерпретация не сделает ваш код свободным от багов. То, что она даёт — это математическая основа для доказательства невозможности конкретных классов ошибок времени выполнения. Это доказательство так же хорошо, как ваш абстрактный домен, ваша стратегия расширения (widening) и ваша готовность терпеть ложные срабатывания.

Большинство команд получают больше пользы от хороших тестов и корректной системы типов. Но когда вы пишете код, где ошибка времени выполнения означает, что спутник падает с неба, абстрактная интерпретация — это то, как вы спите по ночам.