Comment faire confiance a` un compilateur?Xavier LeroyINRIA Paris RocquencourtColloquium J. Morgenstern, 2009 10 08X. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 1 / 51Contexte : les methodes´ formelleset la ver´ ification de programmesX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 2 / 51Le bug«En informatique, il y a le bug; c’est comme c¸a, vous n’y pouvez rien.»(Ger´ ard Berry, College` de France, 17/01/2008.)Toler´ able? Intoler´ able!X. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 3 / 51Le logiciel critiqueLes methodes´ classiques :´ ´ ˆMethodologie de developpement extremement rigoureuse.Des tests, des tests, et encore des tests.Lorsque tout cela ne suffit plus ou couteˆ trop cher :les methodes´ formelles (approches mathematiques)´X. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 4 / 51Ver´ ification sur un modele`Specifications´Model checkingPreuve manuelle`Modele(simplifie)´?ProgrammesourceX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 5 / 51Ver´ ification sur un modele`Specifications´Model checkingPreuve manuelle`Modele(simplifie)´?ProgrammesourceX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 5 / 51Ver´ ification formelle de programmesSpecifications´Model checkingPreuve manuelleAnalyse statique`Modele(simplifie)´Preuve de programme?ProgrammesourceX. Leroy (INRIA) Ver´ ifier un compilateur 2009 10 08 6 / 51L’analyse statique pour la suretˆ e´´Etablir automatiquement des propriet´ es´ de ...
Model checking Preuve manuelle Mod`ele (simplifie´ ) ?
Analyse statique
002r01-9680-15/
reL.I(yoAIRNe´V)fierincrupiomtelaX
Exemple:sˆurete´delame´moireenC. Acce` s aux tableaux dans les bornes. (Pas debuffer overrun.) Pas d’ ` s au pointeur nul. acce Pas d’acc ` `f ee; pas de doublefree. es apres unr
Signaler les erreurs potentielles (debugging statique).
Fluctuat(CEA) : si lesa[i]etb[i]sont exacts a`p`rsea,olsr dotproduct(10,a,b)est exact a`P()pres. `
Exemple d’analyse statique
Propri´et´esdel’arithm´etiquedelamachine: Pas de de´ bordements dans les calculs entiers. Pas de de´ bordements (Inf,NaN) dans les calculs flottants. Bornerlesimpr´ecisionsdescalculsflottants.