Avant de lire la première ligne d’un carnet, on regarde s’il y a quelque chose dedans. Personne ne fait l’inverse. Personne n’ouvre un carnet vide en essayant d’y lire la ligne un, pour ensuite se dire « ah, il était vide, ce n’est pas grave ».

En verbose, cette précaution s’écrit comme ça :

length(i.s) == 0 or byte_at(i.s, 0) > 0

« Le texte est vide, ou son premier octet n’est pas nul. » Si le texte est vide, la question est réglée dès la première moitié, et la seconde, qui lit l’octet numéro zéro, n’a aucune raison d’être posée. D’ailleurs elle ne peut pas l’être : dans un texte vide, il n’y a pas d’octet numéro zéro.

Le 8 octobre, cette ligne protégeait parfaitement le programme quand verbose le compilait en binaire natif. Et ne protégeait rien du tout quand le même programme passait par l’interpréteur, ou par WebAssembly. Voici pourquoi, et ce que ça dit d’un mot aussi simple que « ou ».

Ce que « ou » veut dire, en deux temps

Il y a deux choses distinctes dans un « ou ».

La première est sa valeur : vrai si au moins un des deux côtés est vrai. Tout le monde connaît le tableau :

   gauche   droite   gauche ou droite
   ──────   ──────   ────────────────
   faux     faux     faux
   faux     vrai     vrai
   vrai     faux     vrai
   vrai     vrai     vrai      ← les deux dernières lignes : dès que
                                 la gauche est vraie, le résultat est vrai,
                                 quoi que dise la droite

La seconde est son ordre : qui est calculé, et quand. Et c’est là que tout se joue. Il y a deux façons de calculer gauche ou droite :

  façon « tout d'abord »                façon « court-circuit »
  ──────────────────────                ───────────────────────
  1. calculer gauche                    1. calculer gauche
  2. calculer droite                    2. si gauche est vrai → répondre vrai,
  3. combiner                              s'arrêter là
                                        3. sinon calculer droite, et répondre
                                           ce qu'elle vaut

Sur le papier, les deux donnent la même valeur. Le tableau ne change pas. Mais si calculer la droite peut échouer, les deux façons ne font plus du tout la même chose. La première échoue. La seconde n’y va jamais.

C’est pour ça qu’écrire une garde avec un « ou » a un sens : on compte sur l’ordre. Le court-circuit n’est pas une optimisation qui ferait gagner du temps. C’est la raison pour laquelle la ligne a été écrite.

Un programme, trois exécuteurs

Un programme verbose peut s’exécuter de trois façons. Le compilateur vérifie d’abord la source une seule fois, puis :

                         guard.verbose
                               │
                     vérification de la source
                  (types, lectures, preuves déclarées)
                               │
         ┌─────────────────────┼─────────────────────┐
         ▼                     ▼                     ▼
   interpréteur           binaire natif           module WASM
   (Rust, lit l'arbre     (code x86-64,           (bytecode pour le
    du programme et       un ELF de 585           navigateur ou Node)
    calcule nœud par      octets)
    nœud)

L’interpréteur, c’est quelqu’un qui lit la recette à voix haute et l’exécute étape par étape. Le binaire natif, c’est la recette traduite une fois pour toutes en gestes que le processeur fait directement. Le WASM, c’est la même traduction, mais pour une machine imaginaire que le navigateur sait faire tourner.

Trois traductions d’une même phrase. Elles doivent dire la même chose. Prenons une règle minuscule, et donnons-lui deux textes : "abc" et "".

rule first_byte_or_empty
  input:  i : Input          (un champ s : text)
  output: out : number
  logic:
    out = if length(i.s) == 0 or byte_at(i.s, 0) > 0 then 1 else 0

Le natif : juste depuis le début

On compile, on exécute :

$ ./guard-native abc
1
$ ./guard-native ""
1

Les deux réponses sont bonnes. Et on peut voir pourquoi dans le binaire lui-même. Voici le passage, désassemblé, juste après le calcul de la longueur :

  adresse  instruction             ce que ça fait
  ───────  ──────────────────────  ─────────────────────────────────────────
   12b     cmp  rcx, rax           compare la longueur (rax) à 0 (rcx)
   12e     sete al                 al = 1 si elles sont égales, 0 sinon
   135     test rax, rax           la gauche du « ou » vaut-elle vrai ?
   138     jne  0x1a6              ← si oui : SAUTER à 0x1a6, directement
                                     au « répondre vrai »
   13e     ...                     sinon seulement : recalculer la longueur,
   16a     cmp  rax, rcx             vérifier que l'index 0 est dans le texte,
   178     movzbl (rdx,rax), eax     et lire l'octet

Le saut à l’adresse 0x138 est le court-circuit, en une instruction de six octets. Avec "", la gauche est vraie, le processeur saute, et l’instruction qui lit l’octet à 0x178 n’est jamais atteinte.

L’interpréteur : la recette lue dans le mauvais ordre

Même règle, mêmes entrées, mais par l’interpréteur, sur le code tel qu’il était avant le 8 octobre :

$ printf '[{"s":"abc"},{"s":""}]' | verbosec guard.verbose --run first_byte_or_empty --stdin --json
runtime error: byte_at index out of range: index=0, length=0

Le texte vide fait tout échouer. La garde est là, elle est juste, et elle ne sert à rien.

Le code de l’interpréteur expliquait tout en trois lignes. Pour une opération binaire, il faisait ceci :

  let l = eval_expr(left,  ...)?;     ① calculer la gauche
  let r = eval_expr(right, ...)?;     ② calculer la droite   ← échoue ici
  match (op, l, r) {
      (Or, Bool(a), Bool(b)) => Ok(Bool(a || b)),   ③ combiner
      ...

C’est la façon « tout d’abord ». Le || de la troisième ligne court-circuite bien, en Rust. Mais il arrive trop tard : quand on arrive à lui, r a déjà été calculé, et le calcul a déjà échoué. Un court-circuit qui s’applique à deux valeurs déjà connues ne protège rien.

Déroulons l’exécution avec s = "", pas à pas :

   étape   ce que l'interpréteur calcule          valeur
   ─────   ─────────────────────────────────────  ───────────────────────
     1     length("")                             0
     2     0 == 0                                 vrai        ← gauche
     3     byte_at("", 0)                         ✗ erreur : index 0,
                                                    longueur 0
     —     (on n'arrive jamais à « vrai || ... »)

La correction (PR #267) traite and et or avant le chemin général, et décide à partir de la gauche seule :

  let l = eval_expr(left, ...)?;
  si l'opérateur est « and » ou « or » :
      si (and et l est faux) ou (or et l est vrai) :
          répondre l, sans jamais regarder la droite
      sinon :
          calculer la droite, exiger un booléen, répondre sa valeur

Après :

$ printf '[{"s":"abc"},{"s":""}]' | verbosec guard.verbose --run first_byte_or_empty --stdin --json
[{"out":1},{"out":1}]

Deux précisions qui comptent. D’abord, la vérification de la source regarde toujours les deux côtés : types, lectures déclarées, preuves. Une garde à l’exécution n’excuse pas une erreur de type dans la branche qu’elle protège. Ensuite, le binaire natif compilé avant et après la correction est identique à l’octet près (585 octets, cmp ne voit aucune différence). Le correctif n’a touché que l’interpréteur, et la preuve est mesurable.

Le WASM : un « ou » fait avec un OU binaire

WebAssembly ne sait pas encore lire un octet dans un texte, en verbose. On prend donc une autre garde, du même genre, avec une division :

    ok = i.n == 0 or 10 / i.n > 0      « n vaut zéro, ou dix divisé par n est positif »

Avec n = 0, la gauche est vraie, et la division par zéro de droite ne devrait jamais avoir lieu. Le module d’avant, 59 octets, exécuté dans Node :

safe_ratio(0) -> trap: divide by zero
safe_ratio(5) = 1

Et voici pourquoi, dans le module lui-même, désassemblé en texte :

  AVANT (59 octets)                       APRÈS (65 octets)
  ─────────────────                       ─────────────────
  local.get 0  ;; n                       local.get 0  ;; n
  i64.const 0                             i64.const 0
  i64.eq       ;; gauche : n == 0         i64.eq       ;; gauche : n == 0
  i64.extend_i32_u                        i64.extend_i32_u
  i64.const 10                            i64.eqz      ;; la gauche est-elle fausse ?
  local.get 0                             if (result i64)
  i64.div_s    ;; ← 10 / 0 : piège          i64.const 10
  i64.const 0                               local.get 0
  i64.gt_s                                  i64.div_s  ;; seulement ici
  i64.extend_i32_u                          i64.const 0
  i64.or       ;; combiner les deux         i64.gt_s
  i32.wrap_i64                              i64.extend_i32_u
                                          else
                                            i64.const 1 ;; vrai, sans diviser
                                          end
                                          i32.wrap_i64

À gauche, le « ou » est traduit par i64.or, un OU bit à bit entre deux nombres. Pour produire deux nombres, il faut d’abord les calculer tous les deux : la division a lieu à chaque fois. C’est exactement la façon « tout d’abord », écrite en bytecode.

À droite (PR #270), un if qui porte un résultat. La division est rangée dans la branche qui ne s’exécute que si la gauche est fausse. Six octets de plus par « ou ». Pas de variable temporaire, pas de mémoire, juste un aiguillage :

safe_ratio(0) = 1
safe_ratio(5) = 1

Le quatrième endroit : dans le compilateur

Il restait un exécuteur auquel on ne pense pas, parce qu’il ne tourne pas au moment où le programme tourne : le compilateur lui-même.

Quand une expression ne dépend que de constantes, le compilateur la calcule une bonne fois pour toutes et met le résultat dans le binaire. C’est le pliage de constantes. 2 + 3 devient 5 avant même que le programme existe. C’est une bonne idée. Sauf quand le compilateur plie aussi ce que le programme n’aurait jamais calculé :

    ok = 1 == 1 or (-9223372036854775807 - 1) / -1 > 0

La gauche est vraie, toujours. La droite divise le plus petit entier 64 bits par moins un, une opération qui n’a pas de résultat (il dépasse la capacité d’un entier 64 bits) et qui ne doit donc jamais avoir lieu. Elle n’a d’ailleurs aucune raison d’avoir lieu : la gauche a déjà répondu.

Avant la PR #268, compiler cette ligne en natif donnait :

thread '<unnamed>' panicked at src/optimizer.rs:614:51:
attempt to divide with overflow

Ce n’est pas le programme qui plante. C’est le compilateur, en train de « préparer » une branche que le programme aurait sautée. L’optimiseur avait décidé tout seul que tout ce qui est constant peut être calculé d’avance. La règle corrigée est plus modeste : un calcul qui peut échouer et qui n’a pas de résultat valide reste une opération, et c’est le flot d’exécution, avec son court-circuit, qui décide s’il a lieu. Même chose pour calcul * 0 : la valeur sera zéro, mais si calcul peut échouer, il doit encore être évalué, à sa place.

Après :

$ ./fold-after 1
true

Un binaire natif de 480 octets, qui ne contient la division que dans la branche jamais prise.

Ce que ça apprend

Trois exécuteurs, et un quatrième caché dans le compilateur. Un seul avait raison. Les trois autres donnaient la bonne valeur au « ou », chaque fois qu’ils arrivaient au bout, et se trompaient sur l’ordre. On ne voit pas ce genre d’écart en testant des cas qui marchent : "abc" passait partout. Il faut le cas que la garde existe pour protéger, le texte vide, le diviseur nul, et le faire passer par chaque chemin.

C’est ce que font maintenant les tests de verbose : une table de vérité complète, des textes vides, avec un NUL, en UTF-8 multi-octets, des gardes imbriquées, des divisions sautées et des divisions requises, exécutés sur les modules WASM réels dans Node, comparés à l’interpréteur. Et, comme contrôle inverse, le corpus de 194 exemples compilé avant et après : 190 binaires natifs identiques à l’octet, et les quatre refus inchangés.

La limite, nommée comme d’habitude. WebAssembly ne sait toujours pas lire un octet dans un texte, d’où la division dans l’exemple. L’interpréteur et le natif ne traitent pas encore le dépassement arithmétique de la même façon, et la documentation le dit au lieu de prétendre à une parité complète. Et verbose n’a toujours pas de tag depuis la v0.10.0, environ cent quarante-quatre commits plus loin.

Un « ou » ne demande pas seulement si l’un des deux est vrai. Il promet de ne pas aller voir le second quand le premier a répondu. Trois traductions sur quatre avaient oublié la promesse.