Die Testsuite ist grün. Der Typchecker ist grün. Man deployt. Zwei Stunden später wirft die Produktion einen IndexError bei einem Edge-Case, an den niemand gedacht hat.

Tests finden Bugs. Typen verhindern einige. Keines von beidem beweist, dass ein Programm frei von Laufzeitfehlern ist. Dafür braucht man etwas Stärkeres: eine Möglichkeit, über jede mögliche Ausführung gleichzeitig zu argumentieren, ohne den Code auszuführen.

Abstrakte Interpretation ist die Technik, die das möglich macht. Sie treibt die statischen Analysatoren in Astrée, Facebooks Infer und die Korrektheitsgarantien in Rusts Borrow-Checker an. Sie erklärt auch, warum das meiste Marketing für „null Falschmeldungen“ bei statischer Analyse eine Lüge ist.

Laufzeitfehler sind ein Erreichbarkeitsproblem

Ein Laufzeitfehler ist einfach eine Operation, die einen schlechten Zustand erreicht. Division durch null, Null-Dereferenzierung, Pufferüberlauf, Index außerhalb der Grenzen. Jeder davon passiert, weil die Ausführung einen Programmpunkt erreicht, an dem die Operation unsicher ist.

Um zu beweisen, dass kein Laufzeitfehler existiert, muss man beweisen, dass jede unsichere Operation in jeder möglichen Ausführung unerreichbar ist. Jeder Input. Jeder Branch. Jede Schleifeniteration.

Exhaustives Testen ist für alles außer Spielzeugprogrammen unmöglich. Symbolische Ausführung skaliert schlecht, weil die Pfadexplosion einen umbringt. Abstrakte Interpretation geht einen anderen Weg: Sie gibt auf, exakte Werte zu kennen, und verfolgt stattdessen ungefähre Eigenschaften, die garantiert jede reale Ausführung abdecken.

Was abstrakte Interpretation wirklich tut

Abstrakte Interpretation wurde 1976 von Patrick und Radhia Cousot eingeführt. Die Kernidee ist wunderbar einfach: Das Programm ausführen, aber statt mit echten Zahlen, Strings und Pointern zu rechnen, rechnet man mit abstrakten Repräsentationen, die die echten Werte überapproximieren.

Man kann es sich so vorstellen, dass man die konkrete Ausführung durch eine „Schatten“-Ausführung ersetzt, die die Eigenschaften verfolgt, die einen interessieren. Statt zu wissen, dass x = 42, weiß man vielleicht, dass x > 0. Statt zu wissen, dass arr die Länge 10 hat, weiß man vielleicht, dass arr nicht leer ist.

Die wichtigste Einschränkung ist Korrektheit (Soundness). Jeder konkrete Zustand muss durch einen abstrakten Zustand repräsentiert werden. Wenn die abstrakte Ausführung sagt, dass eine Operation sicher ist, dann ist jede konkrete Ausführung, die sie repräsentiert, sicher. Der Preis ist Präzision: Wenn der abstrakte Zustand zu vage ist, bekommt man Falschmeldungen (Fehlalarme über sichere Operationen).

Ein konkretes Beispiel: Intervallanalyse

Hier ist ein minimaler abstrakter Interpreter, der beweist, dass eine Division durch null unmöglich ist. Er verfolgt den möglichen Bereich jeder Variable mithilfe von Intervallen.

# 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)

Ausführen. Der erste Fall beweist Sicherheit, weil das Intervall für t [1.0, 101.0] ist, das null ausschließt. Der zweite Fall markiert das Risiko korrekt, weil t null sein kann, wenn x -1 ist.

Der if-Handler führt beide Branches zusammen, indem er die Vereinigung der Intervalle bildet. Der while-Handler iteriert, bis die Intervalle aufhören zu wachsen (ein Fixpunkt). Das ist das Herz der abstrakten Interpretation: Man tauscht exakte Werte gegen garantierte Überapproximationen und beweist Sicherheit, indem man zeigt, dass der schlechte Zustand außerhalb der Approximation liegt.

Wo es scheitert: Die Präzisionsgrenze

Das obige Beispiel ist Spielzeuggröße. Echte Programme haben Aliasing, Rekursion, Heap-Allokationen und Schleifen mit datenabhängigen Grenzen. Jeder davon zerstört Präzision auf vorhersehbare Weise.

Betrachte eine Schleife, die i von 0 bis 100 inkrementiert. Eine naive Intervallanalyse könnte i zu [0, +inf) verbreitern und die obere Grenze nie wieder zurückgewinnen. Man braucht relationale Domains (wie Polyeder oder Oktagonen), um i <= 100 zu verfolgen. Diese Domains sind kubisch oder exponentiell in der Anzahl der Variablen. Für ein Programm mit 1.000 Variablen führt man keine Polyederanalyse durch.

Deshalb treffen kommerzielle Tools unterschiedliche Entscheidungen. Astrée verwendet einen sorgfältig ausgewählten Verband abstrakter Domains, handoptimiert für Embedded-C. Infer verwendet Separationslogik und Bi-Abduktion, um auf Millionen Zeilen mobiler Code zu skalieren, gibt aber für einige Sprachfeatures die Korrektheit auf. Rusts Borrow-Checker ist im Grunde ein abstrakter Interpreter mit einer einzigen, extrem präzisen Domain: Ownership.

Kompromisse, die man nicht vermeiden kann

Korrektheit, Präzision und Skalierbarkeit. Wähle zwei.

Ein korrekter Analysator mit hoher Präzision wird nicht über small modules hinausskalieren. Ein skalierbarer, korrekter Analysator wird einen in Falschmeldungen ertränken. Ein skalierbarer, präziser Analysator wird echte Bugs übersehen.

Die Wahl der abstrakten Domain ist der Einstellknopf. Intervalle sind schnell und unpräzise. Polyeder sind präzise und langsam. Prädikatenabstraktion liegt in der Mitte und treibt die meisten Software-Model-Checker an.

Wie man das wirklich nutzt

Man wird wahrscheinlich nicht seinen eigenen abstrakten Interpreter schreiben. Man wird einen verwenden, der bereits existiert.

Für C und Embedded-Systeme sind Astrée und Frama-C die ausgereiften Optionen. Frama-Cs EVA-Plugin führt Intervall- und Speicheranalyse auf echtem C-Code durch.

Für Rust kodiert das Typsystem bereits eine Ownership-Abstract-Domain. Miri ist ein Interpreter, kein abstrakter Interpreter, aber es fängt undefiniertes Verhalten ab, das das Typsystem übersieht.

Für Allzweckcode ist Infer von Meta das, was einem skalierbaren abstrakten Interpreter für Java, C++ und Objective-C am nächsten kommt. Es findet echte Null-Dereferenzierungs- und Speicherleck-Bugs in production codebases.

Wer experimentieren möchte, sollte mit einer einfachen Vorzeichenanalyse oder Intervallanalyse auf einer selbst geparsten Sprache beginnen. Das Dragon Book behandelt Datenflussanalyse. Nielson und Nielsons Principles of Program Analysis ist die Standardreferenz speziell für abstrakte Interpretation.

Die negative Beweisführung

Abstrakte Interpretation wird den Code nicht fehlerfrei machen. Was sie bietet, ist ein mathematisches Framework, um zu beweisen, dass bestimmte Klassen von Laufzeitfehlern unmöglich sind. Dieser Beweis ist nur so gut wie die abstrakte Domain, die Verbreiterungsstrategie und die Bereitschaft, Falschmeldungen zu tolerieren.

Die meisten Teams bekommen mehr Wert aus guten Tests und einem soliden Typsystem. Aber wenn man Code schreibt, bei dem ein Laufzeitfehler bedeutet, dass ein Satellit vom Himmel fällt, ist abstrakte Interpretation das, was einen nachts ruhig schlafen lässt.