La vérification des programmes par interprétation abstraite

La vérification des programmes par interprétation abstraite Patrick Cousot École normale supérieure Patrick.Cousot@ens.fr www.di.ens.fr/ cousot~ Équipe-projet INRIA Paris–Rocquencourt/CNRS/ENS « Abstraction » Séminaire Chaire d’innovation technologique Liliane Bettencourt Collège de France, 22 février 2008 Pourquoi et comment le monde devient numérique, 22/2/2008 — 1 — P. Cousot1. Exemples classiques de bugs Pourquoi et comment le monde devient numérique, 22/2/2008 — 2 — P. CousotExemples classiques de bugs du calcul en entiers Pourquoi et comment le monde devient numérique, 22/2/2008 — 3 — P. CousotLe programme factorielle (fact.c) #include int fact (intn){ fact(n)=2ˆ3ˆ´´´ˆn int r, i; r = 1; for (i=2; i<=n; i++) { r = r*i; } return r; } int main() { int n; scanf("%d",&n); lire n (tapé au clavier) printf("%d!=%d\n",n,fact(n)); écrire n ! = fact(n) } Pourquoi et comment le monde devient numérique, 22/2/2008 — 4 — P. Cousot(1)Compilation du programme factorielle (fact.c) #include % gcc fact.c -o fact.exec %int fact (intn){ int r, i; r = 1; for (i=2; i<=n; i++) { r = r*i; } return r; } int main() { int n; scanf("%d",&n); (1) Voir la leçon du 8 février 2008 et le sémi-printf("%d!=%d\n",n,fact(n)); naire de Xavier Leroy } Pourquoi et comment le monde devient numérique, 22/2/2008 — 4 — P. CousotExécutions du programme factorielle (fact.c) #include % gcc fact.c -o fact.exec % ./fact.execint fact (intn){ 3int r, i; 3! = 6r = 1; % ./fact.execfor (i=2; i<=n; i++) { 4r = r*i; 4! = 24} % ./fact.execreturn r; } 100 100! = 0int main() { int n; % ./fact.execscanf("%d",&n); 20printf("%d!=%d\n",n,fact(n)); } 20! = -2102132736 Pourquoi et comment le monde devient numérique, 22/2/2008 — 5 — P. CousotÀ la chasse au bug – Les ordinateurs utilisent une arithmétique entière mo- dulaire sur n bits (où n = 16, 32, 64, etc) – Exempled’unereprésentationdesentierssur4bits(en complément à deux): – Seuls les entiers entre -8 et 7 sont représentés sur 4 bits – On obtient 7+2 =`7 7+9 = 0 Pourquoi et comment le monde devient numérique, 22/2/2008 — 6 — P. CousotLe bug est une défaillance du programmeur En machine, la fonction fact(n) ne coincide avec n!= 2ˆ3ˆ::::ˆn sur les entiers que pour 16 n6 12 : Pourquoi et comment le monde devient numérique, 22/2/2008 — 7 — P. CousotEt en OCaml on a un résultat di érent! let rec fact n = if (n = 1) then 1 else n * fact(n-1);; fact(22) `522715136 `522715136fact(n) C OCaml fact(23) 862453760 862453760fact(1) 1 1 fact(24) `775946240 `775946240... ::: ::: fact(25) 2076180480 `71303168fact(12) 479001600 479001600 fact(26) `1853882368 293601280fact(13) 1932053504 `215430144 fact(27) 1484783616 `662700032fact(14) 1278945280 `868538368 fact(28) `1375731712 771751936fact(15) 2004310016 `143173632 fact(29) `1241513984 905969664fact(16) 2004189184 `143294464 fact(30) 1409286144 `738197504fact(17) `288522240 `288522240 fact(31) 738197504fact(18) `898433024 `898433024 fact(32) `2147483648 0fact(19) 109641728 109641728 fact(33) ` 0fact(20) `2102132736 45350912 fact(34) 0 0fact(21) `1195114496 952369152 Pourquoi? Que fait fact(-1)? Pourquoi et comment le monde devient numérique, 22/2/2008 — 8 — P. CousotPreuve d’absence d’erreurs à l’exécution par analyse statique % cat -n fact_lim.c 19 int main() { 1 int MAXINT = 2147483647; 20 int n, f; 2 int fact (int n) { 21 f = fact(n); 3 int r, i; 22 } 4 if (n < 1) || (n = MAXINT) { % astree –exec-fn main fact_lim.c |& grep WARN 5 r = 0; % 6} else { ! Aucune alarme!7 r = 1; 8 for (i = 2; i<=n; i++){ 9 if (r <= (MAXINT / i)) { 10 r = r * i; 11 } else { 12 r = 0; 13 } 14 } 15 } 16 return r; 17 } 18 Pourquoi et comment le monde devient numérique, 22/2/2008 — 9 — P. Cousot