Meta hat über 100.000 Bugfixes ausgeliefert, die von einem Static Analyzer gefunden wurden, bevor der Code jemals einen Nutzer erreicht hat. Das Tool heißt Infer, ist Open Source und führt Ihren Code nicht aus. Es liest ihn, baut ein mathematisches Modell dessen, was der Code tun könnte, und beweist, dass bestimmte schlechte Dinge nicht passieren können. Oder es findet einen Pfad, auf dem sie es können.

Die Technik ist Abstract Interpretation. Sie klingt akademisch, weil sie es ist. Patrick Cousot und Radhia Cousot erfanden sie in den 1970ern als Methode, um über Programme zu reasonen, ohne sie auszuführen. Metas Team unter der Leitung von Peter O’Hearn nahm die Theorie und machte sie schnell genug, um Millionen Zeilen Mobile- und Server-Code in Minuten zu analysieren. Das Ergebnis ist ein Tool, das Null-Pointer-Dereferenzierungen, Memory Leaks, Resource Leaks und Race Conditions zum Diff-Zeitpunkt findet.

Das Problem: Dynamisches Testing kann nicht abdecken, was man nicht zu laufen bringt

Ein Unit Test prüft einen Pfad durch Ihren Code. Ein integration test prüft ein paar mehr. Aber eine Funktion mit fünf Conditionals und zwei Loops hat hunderte Pfade, und die meisten werden niemals in Test-Suites ausgeführt.

Dynamisches Testing – also das Ausführen des Codes – kann nur Bugs auf Pfaden finden, die man tatsächlich ausführt. Static Analysis findet Bugs auf Pfaden, an die man nie gedacht hat. Es ist der Unterschied zwischen dem Prüfen Ihres Hauses auf Eindringlinge, indem Sie mit einer Taschenlampe durch die Zimmer gehen, und dem Prüfen, indem Sie beweisen, dass alle Türen und Fenster verschlossen sind.

Die Herausforderung ist, dass das Beweisen von Aussagen über echte Programme schwer ist. Echte Programme haben Loops, Rekursion, Heap-Allocation und Concurrency. Man kann nicht jeden State aufzählen. Abstract Interpretation löst das durch Approximation.

Was Abstract Interpretation tatsächlich bedeutet

Abstract Interpretation funktioniert, indem das Programm auf abstrakten Werten statt auf konkreten ausgeführt wird.

Bei einer normalen Ausführung hält eine Variable x vielleicht den Integer 42. Bei einer Abstract Interpretation hält x vielleicht den abstrakten Wert „positiv“. Die Analyse weiß nicht, dass x 42 ist. Sie weiß, dass x größer als null ist. Das reicht, um zu beweisen, dass x / y nicht durch null teilt, wenn y ebenfalls positiv ist. Es reicht nicht, um zu beweisen, dass x == 42. Abstract Interpretation tauscht Präzision gegen Berechenbarkeit ein.

Die Menge der abstrakten Werte heißt Abstract Domain. Die einfachste Domain ist die Sign-Domain: Jede Variable ist entweder negativ, null, positiv oder unbekannt. Komplexere Domains tracken Ranges, Pointer oder ob ein Memory-Location freigegeben wurde. Die Analyse iteriert über das Programm, wendet abstrakte Versionen jeder Operation an, bis der abstrakte State sich nicht mehr ändert. Dann hat sie einen Fixpunkt gefunden – eine Approximation jedes möglichen konkreten States an jedem Programm-Punkt.

Loops sind der schwierige Teil. Ein Loop könnte null Mal, ein Mal oder eine Milliarde Mal laufen. Der Analyzer kann ihn nicht eine Milliarde Mal unrollen. Stattdessen wendet er einen Widening-Operator an, der zu einer Über-Approximation springt. Wenn eine Variable pro Iteration um eins inkrementiert, könnte der Analyzer ihren abstrakten Wert von „positiv“ auf „nicht-negativ“ erweitern und dort stoppen. Er verliert die exakte Grenze, behält aber die Eigenschaft, die für den Beweis wichtig ist.

Wie Infer Bi-Abduction nutzt, um Prozeduren modular zu analysieren

Traditionelle Abstract Interpretation analysiert ein ganzes Programm als Ganzes. Das skaliert nicht für eine Mobile-App mit einer Million Zeilen Code. Infer löst das mit einer Technik namens Bi-Abduction.

Bi-Abduction erlaubt Infer, eine Funktion nach der anderen zu analysieren. Wenn Infer eine Funktion analysiert, entdeckt es zwei Dinge: die Preconditions, die gelten müssen, damit die Funktion sicher ist, und die Postconditions, die die Funktion garantiert. Diese werden automatisch inferiert, nicht vom Programmierer geschrieben.

Hier ist ein konkretes Beispiel. Angenommen, Infer sieht diese C-Funktion:

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

Infer inferiert, dass greet erfordert, dass p non-null ist. Das ist die Precondition. Es inferiert auch, dass greet p nicht freigibt und keinen sichtbaren State modifiziert. Das ist die Postcondition. Wenn eine andere Funktion greet aufruft, prüft Infer den Caller gegen die inferierte Precondition. Wenn der Caller möglicherweise null übergibt, meldet Infer einen Bug.

Die Bi-Abduction-Engine arbeitet durch Symbolic Execution über Separation Logic. Separation Logic erlaubt Infer, über Heap-Ownership zu reasonen: Welche Funktion besitzt welchen Memory, und ob dieser Memory freigegeben wurde. Das ist es, was Infer so gut darin macht, Null-Dereferenzierungen und Memory Leaks in C, C++, Objective-C und Java zu finden.

Was Infer erkennt und was es verpasst

Infer ist kein Allzweck-Linter. Es zielt auf spezifische Bug-Klassen ab, die dynamisch teuer zu finden sind und in der Produktion gefährlich sind.

Null-Pointer-Dereferenzierungen. Infer trackt, ob jeder Pointer definitiv null, definitiv non-null oder vielleicht null ist. Eine Dereferenzierung eines Maybe-Null-Pointers löst einen Report aus. In Java und Objective-C fängt das den häufigsten Crash-Typ ab.

Memory Leaks. Infer nutzt Separation Logic, um Heap-Ownership zu tracken. Wenn eine Funktion Memory alloziert und es weder freigibt noch an einen Caller zurückgibt, meldet Infer einen Leak. Das ist besonders wertvoll in C- und C++-Codebases, in denen Leaks sich über Wochen Uptime ansammeln.

Resource Leaks. File Descriptors, Sockets und Locks werden ähnlich getrackt. Wenn eine Funktion eine Datei öffnet und auf jedem Pfad ohne Schließen zurückkehrt, meldet Infer den Leak.

Race Conditions. Infers RacerD-Modul analysiert Java-Concurrency. Es trackt, welche Threads auf welche Felder zugreifen und ob diese Zugriffe durch Locks geschützt sind. Zwei Threads, die auf dasselbe Feld ohne Synchronisation zugreifen, ergeben einen Race.

Infer erkennt nicht alles. Es verpasst Bugs, die Reasoning über numerische Präzision, String-Inhalte oder komplexe Aliasing-Patterns erfordern. Es ist auch by Design unsound: Es kann Bugs verpassen, um False Positives niedrig zu halten. Ein Static Analyzer, der bei jedem Diff wolfcries, wird deaktiviert. Metas internes Deployment hielt Infers False-Positive-Rate unter 10 %, weshalb Entwickler seine Reports tatsächlich beachten.

Infer auf eigenem Code ausführen

Infer ist Open Source und unterstützt C, C++, Objective-C, Java und (experimentell) Rust und Swift. Der einfachste Weg, es auszuprobieren, ist mit einem Java- oder C-Projekt.

Installieren Sie Infer über Homebrew oder Docker:

# macOS
brew install infer

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

Für ein Java-Projekt mit Maven:

infer run -- mvn compile

Für ein C-Projekt mit Make:

infer run -- make

Infer kompiliert Ihren Code, baut einen Control-Flow-Graph und führt die Analyse aus. Die Ausgabe ist eine Menge von Bug-Reports mit Dateinamen, Zeilennummern und der verletzten inferierten Precondition.

Hier ist ein minimales C-Beispiel, das Infer flaggen wird:

// 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;
}

Das Ausführen von infer run -- cc leak.c produziert:

leak.c:5: error: MEMORY_LEAK
  memory dynamically allocated by call to `malloc()` at line 5 is not reachable after line 7

Infer erkennt auch die Null-Dereferenzierung in diesem Beispiel:

// 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
}

Warten Sie, eigentlich wird Infer das obige nicht melden. Die Funktion print_length handhabt ein null-Argument sicher. Infer meldet nur, wenn eine Dereferenzierung auf einem möglicherweise null-Pointer ohne Prüfung passiert. Hier ist eines, das triggert:

// 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 trace den Pfad von call_unsafe durch unsafe_print und meldet, dass s null ist, wenn s[0] evaluiert wird.

Der Trade-off: Geschwindigkeit versus Präzision

Infers modulares Design macht es schnell genug, um bei jedem Pull Request bei Meta zu laufen. Aber Modularität führt zu Approximation. Wenn Infer eine Funktion analysiert, kennt es nicht den exakten Calling Context. Es inferiert Preconditions, die konservativ sind, also möglicherweise stärker als nötig. Eine stärkere Precondition bedeutet weniger gemeldete Bugs am Call-Site, aber auch weniger False Positives.

Das ist die zentrale Spannung in der Static Analysis. Ein sound Analyzer meldet jeden Bug, ertränkt einen aber in False Positives. Ein unsound Analyzer wie Infer hält Entwickler zufrieden, indem er nur Bugs meldet, bei denen er sicher ist. Die Bugs, die er verpasst, sind die Kosten der Adoption.

Infers Bi-Abduction-Engine hat auch Probleme mit globalem State und komplexen Callbacks. Wenn Ihr Java-Code eine anonyme innere Klasse an einen Executor übergibt, kann Infer den Überblick verlieren, welcher Thread welche Methode ausführt. RacerD handhabt gängige Patterns, verpasst aber subtile Races, die Condition Variables oder Atomic Fields involvieren.

Wann man Static Analysis adoptieren sollte und wann nicht

Sie sollten Infer in Betracht ziehen, wenn Sie nativen Code, Mobile-Apps oder Server-Code in C-Family- oder Java-Sprachen ausliefern. Die Bugs, die es findet – Null-Dereferenzierungen, Leaks, Races – sind genau die, die Production-Crashes und Sicherheitslücken verursachen.

Sie sollten nicht erwarten, dass Infer Ihre Test-Suite ersetzt. Static Analysis und dynamisches Testing sind komplementär. Tests verifizieren, dass Ihr Code das tut, was Sie beabsichtigen, mit den Inputs, die Sie gewählt haben. Static Analysis verifiziert, dass Ihr Code das nicht tut, was Sie verbieten, mit jedem Input.

Wenn Ihre Codebase in Python, Ruby oder JavaScript ist, ist Infer nicht das richtige Tool. Diese Sprachen haben nicht die statische Typ-Information, die Infer nutzt, um sein abstraktes Modell zu bauen. Für dynamische Sprachen fangen Type Checker wie mypy oder pyright eine andere Klasse von Fehlern ab.

Das Fazit

Metas 100.000 Bugfixes sind keine Marketing-Zahl. Sie sind die Ausgabe eines Tools, das bei jedem Diff läuft, Code ohne Ausführung analysiert und Bugs meldet, die kein Test gefunden hätte. Die zugrundeliegende Technik, Abstract Interpretation, ist Jahrzehnte alt. Die Ingenieursleistung ist, sie schnell und präzise genug zu machen, dass Entwickler sie nicht abschalten.

Sie brauchen nicht Metas Infrastruktur, um zu profitieren. Installieren Sie Infer, zeigen Sie es auf Ihr Build-System und lassen Sie es auf einem Modul laufen, das Sie ängstigt. Das Memory-Management-Modul, die Concurrency-Layer, die C-Interop-Boundary. Beheben Sie die Leaks und Null-Dereferenzierungen, die es findet. Dann fügen Sie es zu CI hinzu und halten Sie die Bug-Count davon ab, zu wachsen.

Abstract Interpretation ist keine Magie. Es ist Mathematik, angewandt auf Code, mit all den Approximationen und Trade-offs, die das mit sich bringt. Aber es ist Mathematik, die echte Bugs in echten Codebases findet, und das macht sie wert, sie zu kennen.