Meta a livré plus de 100 000 correctifs de bugs qui ont été attrapés par un analyseur statique avant que le code n’atteigne jamais un utilisateur. L’outil s’appelle Infer, il est open source, et il n’exécute pas votre code. Il le lit, construit un modèle mathématique de ce que le code pourrait faire, et prouve que certaines mauvaises choses ne peuvent pas arriver. Ou il trouve un chemin où elles le peuvent.

La technique est l’interprétation abstraite. Ça sonne académique parce que ça l’est. Patrick Cousot et Radhia Cousot l’ont inventée dans les années 1970 comme moyen de raisonner sur des programmes sans les exécuter. L’équipe de Meta, dirigée par Peter O’Hearn, a pris la théorie et l’a rendue assez rapide pour analyser des millions de lignes de code mobile et serveur en minutes. Le résultat est un outil qui trouve les déréférencements de pointeur nul, les fuites de mémoire, les fuites de ressources et les race conditions au moment du diff.

Le problème : le test dynamique ne peut pas couvrir ce que vous n’avez pas pensé à exécuter

Un test unitaire vérifie un chemin à travers votre code. Un test d’intégration en vérifie quelques autres. Mais une fonction avec cinq conditionnelles et deux boucles a des centaines de chemins, et la plupart ne sont jamais exercés dans les suites de tests.

Le test dynamique, c’est-à-dire exécuter le code, ne peut trouver des bugs que sur les chemins que vous exécutez réellement. L’analyse statique trouve des bugs sur des chemins auxquels vous n’avez jamais pensé. C’est la différence entre vérifier votre maison pour des intrus en marchant dans les pièces avec une lampe torche, et vérifier en prouvant que toutes les portes et fenêtres sont verrouillées.

Le défi est que prouver des choses sur des programmes réels est difficile. Les programmes réels ont des boucles, de la récursion, de l’allocation sur le heap et de la concurrence. Vous ne pouvez pas énumérer chaque état. L’interprétation abstraite résout cela en approximant.

Ce que signifie réellement l’interprétation abstraite

L’interprétation abstraite fonctionne en exécutant votre programme sur des valeurs abstraites au lieu de valeurs concrètes.

Dans une exécution normale, une variable x pourrait contenir l’entier 42. Dans une interprétation abstraite, x pourrait contenir la valeur abstraite « positive ». L’analyse ne sait pas que x est 42. Elle sait que x est supérieur à zéro. Cela suffit à prouver que x / y ne divisera pas par zéro si y est aussi positif. Ce n’est pas suffisant pour prouver que x == 42. L’interprétation abstraite échange la précision contre la calculabilité.

L’ensemble des valeurs abstraites s’appelle un domaine abstrait. Le domaine le plus simple est le domaine des signes : chaque variable est soit négative, zéro, positive, ou inconnue. Des domaines plus complexes suivent des plages, des pointeurs, ou si un emplacement mémoire a été libéré. L’analyse itère sur le programme, appliquant des versions abstraites de chaque opération, jusqu’à ce que l’état abstrait cesse de changer. À ce moment, elle a trouvé un point fixe, une approximation de chaque état concret possible à chaque point du programme.

Les boucles sont la partie difficile. Une boucle pourrait s’exécuter zéro fois, une fois, ou un milliard de fois. L’analyseur ne peut pas la dérouler un milliard de fois. Au lieu de cela, il applique un opérateur de widening qui saute à une sur-approximation. Si une variable s’incrémente de un à chaque itération, l’analyseur pourrait élargir sa valeur abstraite de « positive » à « non négative » et s’arrêter là. Il perd la borne exacte, mais conserve la propriété qui importe pour la preuve.

Comment Infer utilise la bi-abduction pour analyser les procédures de manière modulaire

L’interprétation abstraite traditionnelle analyse un programme entier comme un tout. Cela ne passe pas à l’échelle pour une application mobile avec un million de lignes de code. Infer résout cela avec une technique appelée bi-abduction.

La bi-abduction permet à Infer d’analyser une fonction à la fois. Quand Infer analyse une fonction, il découvre deux choses : les préconditions qui doivent être vérifiées pour que la fonction soit sûre, et les postconditions que la fonction garantit. Celles-ci sont inférées automatiquement, pas écrites par le programmeur.

Voici un exemple concret. Supposons qu’Infer voie cette fonction C :

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

Infer infère que greet nécessite que p soit non nul. C’est la précondition. Il infère aussi que greet ne libère pas p ni ne modifie aucun état visible. C’est la postcondition. Quand une autre fonction appelle greet, Infer vérifie l’appelant contre la précondition inférée. Si l’appelant pourrait passer nul, Infer rapporte un bug.

Le moteur de bi-abduction fonctionne par exécution symbolique sur la logique de séparation. La logique de séparation permet à Infer de raisonner sur la propriété du heap : quelle fonction possède quelle mémoire, et si cette mémoire a été libérée. C’est ce qui rend Infer bon pour trouver les déréférencements nuls et les fuites de mémoire en C, C++, Objective-C et Java.

Ce qu’Infer attrape et ce qu’il manque

Infer n’est pas un linter à usage général. Il cible des classes de bugs spécifiques qui sont coûteuses à trouver dynamiquement et dangereuses en production.

Déréférencements de pointeur nul. Infer suit si chaque pointeur est définitivement nul, définitivement non nul, ou peut-être nul. Un déréférencement d’un pointeur peut-être-nul déclenche un rapport. En Java et Objective-C, cela attrape le type de crash le plus courant.

Fuites de mémoire. Infer utilise la logique de séparation pour suivre la propriété du heap. Si une fonction alloue de la mémoire et ne la libère pas ni ne la retourne à un appelant, Infer rapporte une fuite. C’est particulièrement précieux dans les codebases C et C++ où les fuites s’accumulent sur des semaines d’uptime.

Fuites de ressources. Les descripteurs de fichier, les sockets et les locks sont suivis de manière similaire. Si une fonction ouvre un fichier et retourne sans le fermer sur chaque chemin, Infer rapporte la fuite.

Race conditions. Le module RacerD d’Infer analyse la concurrence en Java. Il suit quels threads accèdent à quels champs et si ces accès sont protégés par des locks. Deux threads accédant au même champ sans synchronisation est une race.

Infer n’attrape pas tout. Il manque des bugs qui nécessitent un raisonnement sur la précision numérique, le contenu des chaînes, ou des patterns d’aliasing complexes. Il est aussi unsound par conception : il peut manquer des bugs pour garder les faux positifs bas. Un analyseur statique qui crie au loup à chaque diff se fait désactiver. Le déploiement interne de Meta a maintenu le taux de faux positifs d’Infer sous 10 %, ce qui fait que les développeurs agissent réellement sur ses rapports.

Exécuter Infer sur votre propre code

Infer est open source et supporte C, C++, Objective-C, Java, et (expérimentalement) Rust et Swift. La façon la plus simple de l’essayer est sur un projet Java ou C.

Installez Infer via Homebrew ou Docker :

# macOS
brew install infer

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

Pour un projet Java utilisant Maven :

infer run -- mvn compile

Pour un projet C utilisant Make :

infer run -- make

Infer compile votre code, construit un graphe de flux de contrôle et exécute l’analyse. La sortie est un ensemble de rapports de bugs avec des noms de fichier, des numéros de ligne et la précondition inférée qui a été violée.

Voici un exemple minimal en C qu’Infer signalera :

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

Exécuter infer run -- cc leak.c produit :

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

Infer attrape aussi la déréférence nulle dans cet exemple :

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

Attendez, en fait Infer ne rapportera pas ce qui précède. La fonction print_length gère de manière sûre un argument nul. Infer ne rapporte que quand une déréférence a lieu sur un pointeur possiblement nul sans vérification. En voici un qui déclenchera :

// 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 le chemin depuis call_unsafe à travers unsafe_print et rapporte que s est nul quand s[0] est évalué.

Le compromis : vitesse versus précision

La conception modulaire d’Infer le rend assez rapide pour s’exécuter à chaque pull request chez Meta. Mais la modularité introduit une approximation. Quand Infer analyse une fonction, il ne connaît pas le contexte d’appel exact. Il infère des préconditions qui sont conservatrices, ce qui signifie qu’elles peuvent être plus fortes que nécessaire. Une précondition plus forte signifie moins de bugs rapportés au site d’appel, mais aussi moins de faux positifs.

C’est la tension centrale dans l’analyse statique. Un analyseur sound rapporte chaque bug, mais vous noie dans les faux positifs. Un analyseur unsound comme Infer garde les développeurs heureux en ne rapportant que les bugs dont il est sûr. Les bugs qu’il manque sont le coût de l’adoption.

Le moteur de bi-abduction d’Infer a aussi du mal avec l’état global et les callbacks complexes. Si votre code Java passe une classe interne anonyme à un executor, Infer peut perdre la trace de quel thread exécute quelle méthode. RacerD gère les patterns communs mais manque les races subtiles impliquant des variables de condition ou des champs atomiques.

Quand adopter l’analyse statique et quand l’ignorer

Vous devriez envisager Infer si vous livrez du code natif, des apps mobiles ou du code serveur dans des langages de la famille C ou Java. Les bugs qu’il trouve — déréférencements nuls, fuites, races — sont exactement ceux qui causent des crashes en production et des vulnérabilités de sécurité.

Vous ne devriez pas attendre d’Infer qu’il remplace votre suite de tests. L’analyse statique et le test dynamique sont complémentaires. Les tests vérifient que votre code fait ce que vous avez l’intention avec les inputs que vous avez choisis. L’analyse statique vérifie que votre code ne fait pas ce que vous interdisez avec n’importe quel input.

Si votre codebase est en Python, Ruby ou JavaScript, Infer n’est pas le bon outil. Ces langages manquent de l’information de type statique qu’Infer utilise pour construire son modèle abstrait. Pour les langages dynamiques, les type checkers comme mypy ou pyright attrapent une classe différente d’erreurs.

La conclusion

Les 100 000 correctifs de bugs de Meta ne sont pas un chiffre marketing. C’est la sortie d’un outil qui s’exécute à chaque diff, analyse du code sans l’exécuter et rapporte des bugs qu’aucun test n’aurait attrapés. La technique sous-jacente, l’interprétation abstraite, a des décennies d’existence. La réussite d’ingénierie est de la rendre assez rapide et précise pour que les développeurs ne la désactivent pas.

Vous n’avez pas besoin de l’infrastructure de Meta pour en bénéficier. Installez Infer, pointez-le sur votre système de build et exécutez-le sur un module qui vous fait peur. Le module de gestion mémoire, la couche de concurrence, la frontière d’interopérabilité C. Corrigez les fuites et déréférencements nuls qu’il trouve. Puis ajoutez-le à CI et empêchez le nombre de bugs d’augmenter.

L’interprétation abstraite n’est pas de la magie. C’est des mathématiques appliquées au code, avec toutes les approximations et compromis que cela implique. Mais c’est des maths qui trouvent de vrais bugs dans de vraies codebases, et ça la rend digne d’être connue.