L’interprétation abstraite est le genre de terme qui pousse les ingénieurs à fermer l’onglet. Ça sonne comme quelque chose qui nécessite un semestre de théorie des treillis pour comprendre. La plupart des développeurs supposent que cela vit dans des papiers de recherche, pas dans des pull requests.

Cette supposition est coûteuse. L’interprétation abstraite est juste un moyen de prouver des choses sur votre code sans l’exécuter. Les outils construits dessus peuvent attraper des déréférencements nuls, des fuites de mémoire et des race conditions que les vérificateurs de types et les linters manquent. La bonne nouvelle : vous n’avez pas besoin de comprendre les connexions de Galois pour l’utiliser. Vous avez besoin d’une config CI fonctionnelle et d’environ vingt minutes.

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

Au cœur de son fonctionnement, l’interprétation abstraite est une technique de preuve automatisée. Elle exécute votre programme, mais au lieu d’utiliser des valeurs réelles, elle utilise des approximations.

Considérez une variable x. Dans une exécution normale, x pourrait contenir 42. En interprétation abstraite, x pourrait contenir “entier positif”. L’analyse suit ces valeurs abstraites à travers chaque chemin de code possible. Si elle peut prouver qu’aucun chemin ne mène à une déréférence nulle, vous êtes en sécurité. Si elle trouve un chemin où x pourrait être nulle à un site de déréférence, elle rapporte un bug potentiel.

La magie est que cela fonctionne pour les boucles et les conditionnelles. L’analyseur calcule des points fixes sur des états abstraits pour pouvoir raisonner sur l’itération illimitée sans réellement itérer pour toujours. C’est ce qui sépare l’interprétation abstraite des outils d’exécution symbolique plus simples qui peinent avec les boucles.

Infer de Facebook est l’outil de production le plus accessible qui utilise cette technique. Il analyse Java, C, C++ et Objective-C en compilant votre code en une représentation intermédiaire et en exécutant une interprétation abstraite compositionnelle sur chaque fonction. Infer met en cache les résultats par fonction, donc les builds incrémentaux sont rapides. C’est la sauce secrète qui le rend viable en CI.

Pourquoi votre linter n’est pas suffisant

Les linters regardent la syntaxe. Les vérificateurs de types regardent les types. L’interprétation abstraite regarde le comportement à travers les chemins.

Un linter peut signaler que vous avez oublié de vérifier le nul. Un vérificateur de types peut imposer qu’une fonction retourne Optional<T>. Mais aucun des deux ne peut fiablement attraper que vous déréférencez un pointeur à la ligne 47 après une série complexe de branches où un chemin le laisse non initialisé. L’interprétation abstraite suit les états possibles de ce pointeur à travers chaque branche et point de fusion.

Le trade-off est le bruit. L’interprétation abstraite produit des faux positifs. Elle peut rapporter une déréférence nulle que votre logique métier garantit qu’elle n’arrive jamais. L’analyseur ne connaît pas vos invariants. Il sait seulement ce que le code permet littéralement.

Les vérificateurs par défaut d’Infer sont réglés pour garder les taux de faux positifs bas, autour de 10-15% pour la plupart des codebases. C’est plus élevé qu’un vérificateur de types, mais les bugs qu’il trouve sont souvent ceux qui passent à travers la revue de code et les tests.

Ajouter Infer à votre pipeline CI

Vous n’avez pas besoin de construire Infer à partir des sources. Facebook publie des images Docker. Voici un workflow GitHub Actions fonctionnel qui analyse un projet Java :

# .github/workflows/infer.yml
name: Abstract Interpretation

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Run Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "mvn compile"
            --
            mvn compile

      - name: Upload report
        uses: actions/upload-artifact@v4
        with:
          name: infer-report
          path: infer-out/report.json

Pour un projet Node.js ou Python, échangez la commande de build. Infer n’analyse pas nativement JavaScript ou Python, mais vous pouvez l’exécuter sur les extensions C/C++ dont ces projets dépendent souvent. Si vous êtes dans un environnement de langage managé pur, vous pouvez toujours obtenir une analyse similaire sensible aux chemins à partir d’outils comme CodeQL ou SonarQube, bien que leurs moteurs sous-jacents diffèrent.

Pour les projets C ou C++, la configuration est encore plus simple :

# .github/workflows/infer-cpp.yml
name: Infer C++ Analysis

on: [pull_request]

jobs:
  infer:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Build with Infer
        uses: docker://ghcr.io/facebook/infer:main
        with:
          args: >
            infer run
            --make-command "make"
            --
            make

Le pattern infer run --make-command intercepte les appels au compilateur pendant votre processus de build normal. Infer extrait la représentation intermédiaire, l’analyse et écrit les résultats dans infer-out/. Vos artefacts de build réels ne sont pas affectés.

Lire la sortie et ajuster les faux positifs

Infer produit des résultats dans infer-out/report.json et un infer-out/report.txt lisible par l’humain. Un résultat typique ressemble à ceci :

src/parser.c:142: error: NULL_DEREFERENCE
  pointer `node` last assigned on line 138 could be null and is dereferenced at line 142, column 5

Le message vous indique la variable, où elle a été assignée et où la déréférence se produit. Vous pouvez tracer le chemin dans votre éditeur.

Si Infer est trop bruyant, vous pouvez supprimer des vérificateurs spécifiques ou annoter le code pour sauter l’analyse :

// src/parser.c
// infer-ignore: the parent check guarantees node is non-null here
node->value = parsed;

Ou désactiver des vérificateurs spécifiques globalement :

infer run --make-command "make" --no-bufferoverrun --

Le vérificateur de buffer overflow est particulièrement sujet aux faux positifs sur du code avec une arithmétique de pointeurs complexe. Je le désactive généralement sur les codebases C legacy et laisse les vérificateurs de déréférence nulle et de fuite de mémoire actifs. Ces deux-là trouvent de vrais bugs à un taux qui justifie le temps de revue.

Le trade-off du temps de build

L’interprétation abstraite n’est pas gratuite. Un run Infer complet sur un projet C++ de taille moyenne peut prendre 2-4x plus de temps qu’un build normal. L’analyse incrémentale aide : sur les exécutions suivantes, Infer ne réanalyse que les fonctions modifiées et leurs dépendances. En pratique, cela signifie qu’un build de 10 minutes pourrait devenir 15-20 minutes sur un run CI propre, mais 3-5 minutes sur des runs incrémentaux.

Si votre budget CI est serré, exécutez Infer sur les pull requests mais pas sur chaque push vers main. Ou exécutez-le chaque nuit. Les bugs qu’il trouve valent généralement la latence, mais la bonne fréquence dépend de la tolérance de votre équipe pour le temps de CI.

Une autre option est d’exécuter Infer localement avant de push. La même image Docker fonctionne sur n’importe quelle machine avec Docker installé :

docker run --rm -v $(pwd):/workspace -w /workspace \
  ghcr.io/facebook/infer:main \
  infer run --make-command "make" --

Ce qu’Infer n’attrape pas

Infer est compositionnel. Il analyse les fonctions de manière isolée et utilise des résumés pour modéliser les callers et callees. Cela le rend scalable, mais cela signifie que les bugs sensibles aux chemins entre fonctions qui nécessitent d’analyser le graphe d’appels complet peuvent passer à travers.

Il ne trouve pas non plus les bugs de logique. Si votre code déréférence un pointeur en toute sécurité mais utilise la mauvaise valeur, Infer reste silencieux. C’est un vérificateur de sécurité, pas un oracle de correction.

Les bugs de concurrence sont limités. Infer a un vérificateur de race condition, mais il est expérimental et produit assez de faux positifs pour que la plupart des équipes le laissent désactivé.

Que faire ensuite

Commencez petit. Choisissez un projet avec un langage compilé et ajoutez le workflow GitHub Actions ci-dessus. Laissez-le tourner sur les prochains pull requests. Passez en revue les résultats avec votre équipe et construisez une liste de suppression pour le bruit.

Après une semaine, vous aurez une idée de si le signal vaut le temps de CI. D’après mon expérience, le premier run sur une codebase C ou Java existante trouve toujours au moins une déréférence nulle que la revue de code a manquée. C’est généralement suffisant pour justifier de le garder.

Si vous voulez aller plus loin, la documentation d’Infer couvre l’écriture de vérificateurs personnalisés en OCaml. C’est là que le doctorat est utile. Pour tout le reste, les vérificateurs par défaut et une image Docker suffisent.

FAQ

Qu’est-ce que l’interprétation abstraite en termes simples ? C’est une technique d’analyse statique qui approxime comment votre programme se comporte pour prouver des propriétés comme “ce pointeur n’est jamais nul” sans réellement exécuter le code.

Infer est-il gratuit ? Oui. Infer est open source sous licence MIT et maintenu par Meta.

Comment Infer se compare-t-il à SonarQube ? SonarQube utilise un mélange de pattern matching, d’analyse de contamination et d’analyse plus profonde selon le langage. Infer est spécifiquement construit sur l’interprétation abstraite et est sensible aux chemins d’une manière dont SonarQube ne l’est généralement pas pour C, C++, Java et Objective-C.

Puis-je exécuter Infer sur JavaScript ou Python ? Pas directement. Infer analyse les langages compilés. Pour JavaScript et Python, envisagez CodeQL ou des linters conscients des types comme ESLint avec des règles strictes ou Pyright.

Est-ce qu’Infer ralentit significativement la CI ? Une analyse complète prend 2-4x le temps de build. L’analyse incrémentale sur les pull requests est beaucoup plus rapide, ajoutant généralement quelques minutes.