Votre suite de tests passe. Votre vérificateur de types est vert. Vous livrez. Deux heures plus tard, la production génère une IndexError sur un cas limite auquel personne n’a pensé à tester.

Les tests trouvent des bugs. Les types en préviennent certains. Aucun des deux ne prouve que votre programme est exempt d’erreurs d’exécution. Pour cela, vous avez besoin de quelque chose de plus fort : un moyen de raisonner sur toutes les exécutions possibles, toutes à la fois, sans exécuter le code.

L’interprétation abstraite est la technique qui rend cela possible. Elle alimente les analyseurs statiques à l’intérieur d’Astrée, d’Infer de Facebook, et les garanties de sûreté du vérificateur d’emprunts de Rust. Elle explique aussi pourquoi la plupart du marketing « zéro faux positif » pour l’analyse statique est un mensonge.

Les erreurs d’exécution sont un problème d’atteignabilité

Une erreur d’exécution n’est qu’une opération qui atteint un mauvais état. Division par zéro, déréférencement nul, dépassement de tampon, index hors limites. Chacune survient parce que l’exécution atteint un point du programme où l’opération est dangereuse.

Pour prouver qu’aucune erreur d’exécution n’existe, vous devez prouver que chaque opération dangereuse est inatteignable dans chaque exécution possible. Chaque entrée. Chaque branche. Chaque itération de boucle.

Les tests exhaustifs sont impossibles pour tout programme autre que jouet. L’exécution symbolique ne passe pas bien à l’échelle car l’explosion des chemins vous tue. L’interprétation abstraite emprunte une route différente : elle renonce à connaître les valeurs exactes, et suit à la place des propriétés approximatives garanties pour couvrir chaque exécution réelle.

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

L’interprétation abstraite a été introduite par Patrick et Radhia Cousot en 1976. L’idée centrale est d’une beauté simple : exécutez votre programme, mais au lieu de calculer avec des nombres réels, des chaînes et des pointeurs, vous calculez avec des représentations abstraites qui sur-approximent les valeurs réelles.

Imaginez que vous remplacez votre exécution concrète par une exécution « d’ombre » qui suit les propriétés qui vous intéressent. Au lieu de savoir que x = 42, vous savez peut-être que x > 0. Au lieu de savoir que arr a une longueur de 10, vous savez peut-être que arr n’est pas vide.

La contrainte clé est la sûreté (soundness). Chaque état concret doit être représenté par un état abstrait. Si l’exécution abstraite dit qu’une opération est sûre, alors chaque exécution concrète qu’elle représente est sûre. Le prix est la précision : si l’état abstrait est trop vague, vous obtenez des faux positifs (avertissements fallacieux sur des opérations sûres).

Un exemple concret : l’analyse par intervalles

Voici un interpréteur abstrait minimal qui prouve que la division par zéro est impossible. Il suit la plage possible de chaque variable à l’aide d’intervalles.

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

Exécutez-le. Le premier cas prouve la sûreté car l’intervalle de t est [1.0, 101.0], ce qui exclut zéro. Le second cas signale correctement le risque car t peut être zéro lorsque x vaut -1.

Le gestionnaire de if fusionne les deux branches en prenant l’union des intervalles. Le gestionnaire de while itère jusqu’à ce que les intervalles cessent de croître (un point fixe). C’est le cœur de l’interprétation abstraite : vous troquez les valeurs exactes contre des sur-approximations garanties, et vous prouvez la sûreté en montrant que l’état dangereux se situe en dehors de l’approximation.

Où cela s’effondre : le mur de la précision

L’exemple ci-dessus est de taille jouet. Les programmes réels ont de l’aliasage, de la récursivité, des allocations sur le tas, et des boucles avec des bornes dépendantes des données. Chacun détruit la précision de manière prévisible.

Considérez une boucle qui incrémente i de 0 à 100. Une analyse naïve par intervalles pourrait élargir i à [0, +inf) et ne jamais récupérer la borne supérieure. Vous avez besoin de domaines relationnels (comme les polyèdres ou les octogones) pour suivre que i <= 100. Ces domaines sont cubiques ou exponentiels en nombre de variables. Pour un programme avec 1 000 variables, vous n’exécutez pas une analyse par polyèdres.

C’est pourquoi les outils commerciaux font des choix différents. Astrée utilise un treillis soigneusement choisi de domaines abstraits, affiné à la main pour le C embarqué. Infer utilise la logique de séparation et la bi-abduction pour passer à l’échelle sur des millions de lignes de code mobile, mais il renonce à la sûreté pour certaines fonctionnalités du langage. Le vérificateur d’emprunts de Rust est essentiellement un interpréteur abstrait avec un seul domaine extrêmement précis : la propriété.

Des compromis que vous ne pouvez éviter

Sûreté, précision et passage à l’échelle. Choisissez-en deux.

Un analyseur sûr avec une haute précision ne passera pas à l’échelle au-delà de small modules. Un analyseur extensible et sûr vous noiera dans les faux positifs. Un analyseur extensible et précis manquera de vrais bugs.

Votre choix de domaine abstrait est le bouton de réglage. Les intervalles sont rapides et imprécis. Les polyèdres sont précis et lents. L’abstraction par prédicats se situe au milieu et alimente la plupart des vérificateurs de modèles logiciels.

Comment utiliser cela concrètement

Vous n’écrirez probablement pas votre propre interpréteur abstrait. Vous utiliserez un outil qui existe déjà.

Pour le C et les systèmes embarqués, Astrée et Frama-C sont les options matures. Le greffon EVA de Frama-C effectue des analyses par intervalles et mémoire sur du code C réel.

Pour Rust, le système de types encode déjà un domaine abstrait de propriété. Miri est un interpréteur, pas un interpréteur abstrait, mais il attrape les comportements indéfinis que le système de types manque.

Pour du code généraliste, Infer de Meta est l’outil le plus proche d’un interpréteur abstrait extensible pour Java, C++ et Objective-C. Il trouve de vrais bugs de déréférencement nul et de fuites mémoire dans des production codebases.

Si vous voulez expérimenter, commencez par une analyse simple des signes ou par intervalles sur un langage que vous analysez vous-même. Le Dragon Book couvre l’analyse de flux de données. L’ouvrage de Nielson et Nielson, Principles of Program Analysis, est la référence standard pour l’interprétation abstraite en particulier.

Prouver le négatif

L’interprétation abstraite ne rendra pas votre code exempt de bugs. Ce qu’elle vous donne, c’est un cadre mathématique pour prouver que des classes spécifiques d’erreurs d’exécution sont impossibles. Cette preuve n’est aussi bonne que votre domaine abstrait, votre stratégie d’élargissement, et votre volonté de tolérer les faux positifs.

La plupart des équipes retirent plus de valeur de bons tests et d’un système de types sûr. Mais lorsque vous écrivez du code où une erreur d’exécution signifie qu’un satellite tombe du ciel, l’interprétation abstraite est ce qui vous permet de dormir tranquille.