← 13 - UNSAT cores | README Z3-Python

14. Bit-vectors : verifier le debordement arithmetique

Jusqu’ici nous avons raisonne sur des entiers non bornes (Int) ou des reels exacts (Real). Mais un ordinateur calcule sur des entiers bornes : un uint32 ne peut pas depasser 2^32 - 1, et l’addition enveloppe (wraps) modulo 2^32 quand la somme depasse. Ce debordement (overflow) est la source de bugs legendaires (Ariane 5, OpenSSL, Pac-Man) et la cible centrale de la verification formelle de code. Z3 traite les entiers machines via la théorie des bit-vectors (BitVec, SMT-LIB BV) : un vecteur de n bits interprete comme un entier modulo 2^n, avec addition/multiplication/comparaisons/bit-a-bit tous decidables. Ce notebook demontre la capacite distinctive de cette théorie : prouver qu’un debordement est inevitable (ou impossible) sur le domaine machine tout entier - pas seulement le constater sur des valeurs fixes. > Port pyz3 du notebook C# 15_BitVectors_Overflow.ipynb. EPIC #1206, Prong B. (Le bloc DSL [BitVecWidth(n)] du C#, spécifique a Z3.Linq, n’est pas porte ; l’API brute pyz3 BitVec fait le même travail.)

from z3 import *
print("Imports OK : z3-solver (theorie BitVec)")
Imports OK : z3-solver (theorie BitVec)

Lecture : une théorie de décision, pas une approximation

from z3 import * ne fixe aucune théorie : c’est la sorte des variables qui la choisit. Ce notebook travaille en BitVec(..., 32), c’est-à-dire en arithmétique modulaire sur 32 bits, où l’addition est exacte modulo 2^32. C’est ce qui le distingue du notebook 12 : là-bas Real donnait des rationnels exacts et non bornés, ici les valeurs sont bornées par construction et l’enveloppement n’est pas une erreur d’arrondi mais la sémantique même de l’opération.

La conséquence est que Z3 reste une théorie de décision dans ce fragment : tout énoncé du langage des bit-vectors admet une réponse sat ou unsat en temps fini, et cette réponse ne dépend ni d’un pas d’itération ni d’un échantillonnage. C’est ce qui autorise à prouver des propriétés de débordement plutôt qu’à les tester.

1. La théorie des bit-vectors (SMT-LIB BitVec)

Un bit-vector est une suite de n bits interpretee comme un entier modulo 2^n. Z3 en fait une théorie de decision (pas une approximation) : l’addition, la multiplication, les comparaisons et les opérations bit-a-bit sont définies modulo 2^n et decidables. En pyz3, BitVec('x', 32) créé un vecteur de 32 bits, BitVecVal(v, 32) une valeur, ULT/UGE les comparaisons non signees, Extract(hi, lo, x) l’extraction de champ. La distinction cle : Int (non borne, a + b >= a toujours vrai pour b >= 0) vs BitVec (borne, a + b peut envelopper et devenir < a). C’est cette borne fixe qui rend le debordement expressible - et decidable.

2. Le debordement se produit (et Z3 le calcule)

Additionnons deux valeurs dont la somme mathematique depasse 2^32. En uint32, 3 000 000 000 + 1 500 000 000 = 4 500 000 000 mathematiquement, mais la valeur machine enveloppe (retranche 2^32). Z3 calcule la valeur exacte après enveloppement.

# Deux valeurs dont la somme depasse 2^32 = 4 294 967 296
a = BitVecVal(3000000000, 32)   # 3 milliards : tient en uint32
b = BitVecVal(1500000000, 32)   # 1,5 milliard
somme = simplify(a + b)         # addition modulo 2^32
print("a = %d" % a.as_long())
print("b = %d" % b.as_long())
print("a + b (mathematique) = %d" % (a.as_long() + b.as_long()))
print("a + b (uint32, apres enveloppement) = %d" % somme.as_long())
print("-> La valeur machine (%d) est INFERIEURE a a (%d) : il y a eu debordement." % (somme.as_long(), a.as_long()))
a = 3000000000
b = 1500000000
a + b (mathematique) = 4500000000
a + b (uint32, apres enveloppement) = 205032704
-> La valeur machine (205032704) est INFERIEURE a a (3000000000) : il y a eu debordement.

Lecture : le retournement du comparateur

4 500 000 000 devient 205 032 704, et ce n’est pas un artefact d’affichage : en uint32 l’addition est modulo 2^32, donc 4 500 000 000 - 4 294 967 296 = 205 032 704. Le détail qui mérite qu’on s’arrête est le dernier : la somme machine est inférieure à l’opérande a (205 032 704 < 3 000 000 000). C’est la signature du débordement non signé, et c’est ce qui rend le prédicat somme < a correct pour le détecter — une addition qui reste dans les bornes ne peut pas produire une somme inférieure à l’un de ses termes positifs.

Retenez ce retournement : il fonde les deux sections suivantes, qui posent la même inégalité — d’abord sur des valeurs fixées, puis sur des variables symboliques.

3. Caracteriser le debordement : somme < a (unsigned)

Pour des valeurs fixes, on peut demander au solveur si la condition de debordement tient. En arithmetique non signee, somme < a (unsigned less-than, ULT) est vrai ssi l’addition a enveloppe : la somme “revient avant” le premier operande.

# Pour a, b fixes : la condition somme < a (unsigned) est-elle vraie ?
s = Solver()
s.add(ULT(somme, a))   # somme < a  (unsigned less-than) = debordement
st = s.check()
print("Requete 'somme < a' pour a=3e9, b=1.5e9 : %s" % st)
if st == sat:
    print("-> SAT : ULT(somme, a) tient, le debordement est confirme.")
Requete 'somme < a' pour a=3e9, b=1.5e9 : sat
-> SAT : ULT(somme, a) tient, le debordement est confirme.

Lecture : constater n’est pas prouver

somme est ici une expression construite à partir de deux valeurs concrètes, pas une variable libre. Le sat répond donc à une question déjà instanciée : « pour ces deux nombres-là, la condition de débordement tient-elle ? ». La réponse est oui, et elle se vérifie à la main.

Cette section sert d’étalon : elle fixe la sémantique de ULT (unsigned less-than, qui compare 205 032 704 et 3 000 000 000 comme des entiers positifs) avant que la section suivante ne passe aux variables symboliques — là où plus aucune valeur n’est fixée et où la réponse ne se vérifie plus sur une calculette.

4. Prouve symbolique : x, y >= 2^31 implique x + y deborde

Le vrai pouvoir de la théorie BitVec n’est pas de constater un debordement sur des valeurs fixes, mais de prouver qu’il est inevitable pour toute une classe d’entrees. Prouvons : pour tout x, y >= 2^31 (la moitie superieure de l’intervalle uint32), x + y deborde. Technique : par refutation. Si la propriete etait fausse, il existerait x, y >= 2^31 avec somme >= x (pas de debordement). On demande au solveur un tel contre-exemple - s’il repond unsat, la propriete est prouvee.

# Pour x, y SYMBOLES (quelconques), prouvons : x,y >= 2^31  =>  x+y deborde
x = BitVec('x', 32)
y = BitVec('y', 32)
sxy = x + y

preconditions = And(
    UGE(x, BitVecVal(0x80000000, 32)),   # x >= 2^31 = 2 147 483 648
    UGE(y, BitVecVal(0x80000000, 32))    # y >= 2^31
)
pas_debord = UGE(sxy, x)                  # somme >= x  = pas de debordement

# Nions la propriete : preconditions ET pas de debordement
s2 = Solver()
s2.add(preconditions)
s2.add(pas_debord)
st2 = s2.check()
print("' x,y >= 2^31 ET somme >= x (pas de debord) ' : %s" % st2)
if st2 == unsat:
    print("  -> UNSAT : Z3 PROUVE que pour x,y >= 2^31, le debordement est inevitable.")
else:
    print("  -> SAT : contre-exemple trouve (le theoreme est faux).")
' x,y >= 2^31 ET somme >= x (pas de debord) ' : unsat
  -> UNSAT : Z3 PROUVE que pour x,y >= 2^31, le debordement est inevitable.

Lecture : le quantificateur implicite

La formule soumise au solveur est preconditions ET pas_de_debord, et le résultat est unsat. Lisez-le comme un énoncé quantifié : il n’existe pas de x, y vérifiant à la fois x, y >= 2^31 et « pas de débordement ». La négation étant insatisfiable, l’implication « x, y >= 2^31 entraîne un débordement » est valide pour toutes les valeurs.

C’est un changement de nature par rapport à la section précédente : Z3 ne teste plus un cas, il caractérise tout un demi-espace. Le seuil 2^31 = 2 147 483 648 n’est pas arbitraire — c’est exactement la moitié de 2^32, donc la plus petite valeur à partir de laquelle la somme de deux opérandes égaux sort du domaine représentable.

5. Prouve de surete : p, q < 1000 implique p + q ne deborde pas

Symetrique du précédent : prouvons une garantie de surete. Pour tout p, q < 1000, l’addition uint32 ne deborde jamais. Même technique par refutation : s’il existait p, q < 1000 avec debordement, le solveur les trouverait ; unsat prouve la surete.

# Propriete : si p < 1000 ET q < 1000, alors p+q ne deborde pas (somme >= p)
p = BitVec('p', 32)
q = BitVec('q', 32)
spq = p + q

petites = And(
    ULT(p, BitVecVal(1000, 32)),
    ULT(q, BitVecVal(1000, 32))
)
debord = ULT(spq, p)   # debordement = somme < p

# Nions : petites ET debordement -> UNSAT prouve ' petites => pas de debordement '
s3 = Solver()
s3.add(petites)
s3.add(debord)
st3 = s3.check()
print("' p,q < 1000 ET debordement ' : %s" % st3)
if st3 == unsat:
    print("  -> UNSAT : Z3 PROUVE que pour p,q < 1000, l'addition uint32 ne deborde jamais.")
else:
    print("  -> SAT : contre-exemple trouve (improbable).")
' p,q < 1000 ET debordement ' : unsat
  -> UNSAT : Z3 PROUVE que pour p,q < 1000, l'addition uint32 ne deborde jamais.

Lecture : la même preuve, retournée

Le notebook refait le raisonnement dans l’autre sens : au lieu de « au-dessus de la borne le débordement est inévitable », il établit « en dessous de 1000 il est impossible ». Là encore c’est un unsat qui porte la preuve, et là encore le seuil est là où on l’attend : 1000 + 1000 = 2000 reste très loin de 2^32, aucune enveloppe n’est atteignable.

La symétrie des deux sections dit quelque chose d’utile au praticien : une même théorie sert à détecter un risque et à certifier son absence, les deux requêtes ayant exactement la même forme — préconditions et négation de la propriété. C’est ce schéma qui se transpose à la vérification de bornes dans un parseur binaire ou un contrat intelligent.

6. Combiner arithmetique et bit-a-bit : extraction de champ

La théorie BitVec ne se limite pas a l’arithmetique : elle raisonne aussi au niveau bit. Extract(hi, lo, n) extrait les bits lo a hi d’un vecteur. Question : existe-t-il un n non nul dont les deux octets de poids faible sont egaux ? Z3 produit un temoin concret.

# Combiner arithmetique et bit-a-bit : extraction de champ
n = BitVec('n', 32)

# Extraire l'octet de poids faible (bits 0-7) et l'octet suivant (bits 8-15)
octet0 = Extract(7, 0, n)    # bits 7..0   -> BV8
octet1 = Extract(15, 8, n)   # bits 15..8  -> BV8

# Question : existe-t-il n NON NUL tel que octet0 == octet1 ?
s4 = Solver()
s4.add(octet0 == octet1)
s4.add(n != BitVecVal(0, 32))   # forcer un temoin non trivial
st4 = s4.check()
print("' octet bas == octet suivant ' : %s" % st4)
if st4 == sat:
    m4 = s4.model()
    vn = m4[n].as_long()
    print("  Temoin : n = %d = 0x%08X" % (vn, vn))
    print("    octet0 (bits 7..0)  = 0x%02X" % (vn & 0xFF))
    print("    octet1 (bits 15..8) = 0x%02X" % ((vn >> 8) & 0xFF))
print()
print("-> Extract + egalite = raisonnement au niveau champ binaire (protocoles, formats).")
' octet bas == octet suivant ' : sat
  Temoin : n = 4227792896 = 0xFBFF0000
    octet0 (bits 7..0)  = 0x00
    octet1 (bits 15..8) = 0x00

-> Extract + egalite = raisonnement au niveau champ binaire (protocoles, formats).

Lecture du témoin : 0xFBFF0000

Le solveur ne s’est pas contenté de rendre sat : il a fourni un témoin concret, n = 4 227 792 896 = 0xFBFF0000, et le notebook en décompose les deux octets bas — 0x00 pour les bits 7..0, 0x00 pour les bits 15..8. Les deux octets comparés sont donc égaux, ce qui satisfait octet0 == octet1.

Notez la contrainte n != 0 ajoutée explicitement : sans elle, le témoin trivial n = 0 aurait suffi et n’aurait rien montré. C’est le réflexe à garder devant un sat qui paraît trop facile — vérifier que la requête n’admet pas une solution dégénérée avant de lire le témoin. Extract est ce qui permet de raisonner au niveau champ plutôt qu’au niveau entier : protocoles réseau, formats de fichier, registres, partout où la question porte sur des bits précis et non sur la valeur globale.

7. Pourquoi la largeur fixe : BitVec vs Int

Le predicat non-trivial a + b < a avec b >= 1 illustre ce que la largeur fixe achete : - Sur des bit-vectors 4 bits (modulo 16), a + b peut envelopper et devenir < a -> le solveur trouve un temoin (sat).

  • Sur des entiers non bornes (Int), a + b < a avec b >= 1 est impossible -> unsat.

Ce contraste EST la sémantique de la théorie BitVec : sans la largeur fixe, le debordement est inexpressible. C’est pourquoi la verification de code machine (entiers bornes) exige BitVec, pas Int.

# Le meme predicat ' a + b < a, b >= 1 ' sur BitVec 4 bits vs entiers non bornes

# (a) BitVec 4 bits : l'addition enveloppe modulo 16 -> temoin possible
ra = BitVec('a', 4)
rb = BitVec('b', 4)
sBv = Solver()
sBv.add(UGE(rb, BitVecVal(1, 4)))    # b >= 1  (unsigned)
sBv.add(ULT(ra + rb, ra))            # a + b < a  (unsigned) = debordement
stBv = sBv.check()
print("BV4 : ' a+b < a avec b>=1 ' -> %s" % stBv)
if stBv == sat:
    mBv = sBv.model()
    wa = mBv[ra].as_long(); wb = mBv[rb].as_long()
    print("  Temoin : a=%d, b=%d -> (a+b) mod 16 = %d < a=%d  (enveloppe)" % (wa, wb, (wa + wb) % 16, wa))
print()
# (b) Entiers non bornes : aucun debordement possible
ia = Int('a')
ib = Int('b')
sInt = Solver()
sInt.add(ia >= 0)
sInt.add(ib >= 1)
sInt.add(ia + ib < ia)               # a + b < a  sur les entiers
print("Int : meme predicat sur entiers non bornes -> %s  (aucun debordement)" % sInt.check())
BV4 : ' a+b < a avec b>=1 ' -> sat
  Temoin : a=13, b=3 -> (a+b) mod 16 = 0 < a=13  (enveloppe)

Int : meme predicat sur entiers non bornes -> unsat  (aucun debordement)

Lecture : ce que la largeur fixe achète

Deux résultats opposés sur le même prédicat a + b < a avec b >= 1 :

  • en BV4, sat, avec le témoin a = 13, b = 3 : (13 + 3) mod 16 = 0, et 0 < 13 ;
  • en Int, unsat : sur les entiers non bornés, ajouter un b positif ne peut pas faire diminuer a.

Ce couple est la démonstration la plus nette de la section. La théorie Int ne peut pas exprimer le débordement — l’énoncé y est simplement faux — alors que BitVec le rend vrai et décidable. Choisir la théorie est donc un acte de modélisation, pas un détail d’implémentation : un débordement non modélisé n’apparaît pas comme « non prouvé » mais comme « prouvé impossible ». C’est exactement le motif des erreurs qui échappent à un raisonnement mené en arithmétique non bornée.

8. Ce que ce notebook a demontre

Quatre capacites de la théorie BitVec, inaccessibles a Int (non borne) ou au calcul numérique classique : 1. Calcul exact après enveloppement - la valeur machine reelle (3e9+1.5e9 = 205032704 après wrap), pas une approximation.

  1. Preuve d’inevitabilite (unsat) - pour toute entree x,y >= 2^31, le debordement est force, prouve sur tout le domaine.

  2. Preuve de surete (unsat) - pour toute entree p,q < 1000, l’addition ne deborde jamais, garantie formelle.

  3. Raisonnement au niveau bit - extraction de champs, egalite d’octets, temoin concret produit par le solveur.

Ces quatre postures font de BitVec la théorie canonique de la verification formelle : prouver qu’un code (compilateur, crypto, protocole) respecte ses bornes sur toutes les entrees possibles, pas seulement sur les cas testes.

9. Exercices

Les trois exercices ci-dessous vous font manipuler BitVec sur des variantes : debordement signe vs non signe (1), borne exacte du debordement pour t + t (2), produit qui deborde (3). Chaque stub est self-contained : les fonctions (BitVec, BitVecVal, ULT/UGE, Solver) sont définies dans les sections précédentes.

Exercice 1 - Deborde signe mais pas non signe

Trouvez a, b tels que a + b deborde en signe (la somme devient negative, somme < 0 signed) mais PAS en non signe (somme >= a unsigned reste vrai). Indice : choisissez a, b proches de 2^31 - 1 (la limite positive d’un int32 signe).

Étapes : a, b = BitVecVal(..., 32) ; verifier UGE(somme, a) vrai (pas de debord non signe) MAIS simplify(somme < 0) … attention, < 0 en pyz3 sur BitVec est signe par defaut.

# Exercice 1 : a+b deborde en SIGNE mais pas en non signe
# TODO etudiant :
# Etape 1 : a, b proches de 2^31 - 1 (int32 max signe)
# Etape 2 : UGE(somme, a) vrai (pas de debord non signe)
# Etape 3 : mais la somme < 0 en signe (debord signe -> negatif)
result = None  # TODO etudiant
print("Exercice 1 a completer : debordement signe vs non signe")
Exercice 1 a completer : debordement signe vs non signe

Exercice 2 - Borne exacte du debordement pour t + t

Pour a = b = t, a partir de quelle plus petite valeur de t l’addition t + t deborde-t-elle (en unsigned) ? Prouvez que t >= 2^31 implique debordement, et que t = 2^31 - 1 ne deborde pas.

Étapes : tt = t + t ; debord = ULT(tt, t) ; solver avec t >= 2^31 -> sat ; avec t == 2^31 - 1 -> pas de debord.

# Exercice 2 : borne exacte du debordement pour a=b=t
# TODO etudiant :
# Etape 1 : t = BitVec('t', 32) ; tt = t + t ; debord = ULT(tt, t)
# Etape 2 : solver.add(t >= 2^31, debord) -> sat (debord a partir de 2^31)
# Etape 3 : solver t == 2^31 - 1, debord -> unsat (pas de debord juste sous la borne)
result = None  # TODO etudiant
print("Exercice 2 a completer : borne exacte du debordement pour t+t")
Exercice 2 a completer : borne exacte du debordement pour t+t

Exercice 3 - Prouver que 65536 * 65536 deborde en BV32

65536 = 2^16, donc 65536 * 65536 = 2^32, qui en uint32 vaut exactement 0 (enveloppe complet). Prouvez que le produit deborde : produit < 65536 (unsigned), ou directement produit == 0.

Étapes : m1 = m2 = BitVecVal(65536, 32) ; produit = m1 * m2 ; solver.add(produit == 0) -> sat (preuve que le produit enveloppe a 0).

# Exercice 3 : prouver que 65536 * 65536 deborde en BV32
# TODO etudiant :
# Etape 1 : m1 = BitVecVal(65536, 32) ; m2 = BitVecVal(65536, 32)
# Etape 2 : produit = m1 * m2  (multiplication modulo 2^32)
# Etape 3 : solver.add(produit == 0) -> sat (preuve : 2^32 mod 2^32 = 0)
result = None  # TODO etudiant
print("Exercice 3 a completer : prouvez que 65536 * 65536 = 0 en BV32")
Exercice 3 a completer : prouvez que 65536 * 65536 = 0 en BV32

Conclusion

La théorie des bit-vectors de Z3 est l’outil canonique de la verification formelle de code. La ou Int (entiers non bornes) rend le debordement inexpressible, BitVec modelise l’arithmetique machine exacte (modulo 2^n) et permet de prouver des proprietes de surete ou d’inevitabilite sur tout le domaine des entrees.

Cette serie Z3-Python (notebooks 01 a 14) couvre maintenant les grandes théories du solveur : entiers et optimisation (01-11), reels exacts (12), diagnostic par UNSAT cores (13), et ici l’arithmetique machine bornee (14). Chacune exerce une capacite distincte qu’aucune approche numérique classique ne peut reproduire : decision exacte, non pas approximation.

Retour au sommet