Comment faire confiance à un compilateur?
57 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Comment faire confiance à un compilateur?

-

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
57 pages
Français

Description

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 ...

Sujets

Informations

Publié par
Nombre de lectures 45
Langue Français

Exrait

oyer.LXV)AIRNI(ureire´etru0290cnmoipal51
Comment faire confiance `a un compilateur?
INRIA Paris-Rocquencourt
Colloquium J. Morgenstern, 2009-10-08
Xavier Leroy
-10-081/
.XeLroyI(N
Contexte : les me´ thodes formelles etlav´ericationdeprogrammes
RIA)V´erieruncompilateur0290-10-082/51
NRIA)V´e.Leroy(IX513/080--10920uretalipmocnureir
Intole´ rable !
Le bug
Tolerable ? ´
«nEniofmrtaqieua¸cemmocynsuov,ebally,iste;cugezripouven.» (G´erardBerry,Colle`gedeFrance,17/01/2008.)
NI(y)AIR.XoreLcounilmperV´eri
Lorsque tout cela ne suffit plus ou couˆ te trop cher : lessofmrleelesodth´em matiques)(approches mathe´
Les me´ thodes classiques : Me´thodologieded´eveloppementextrˆemementrigoureuse. Des tests, des tests, et encore des tests.
Le logiciel critique
15/00r2euat84-0109-
V´ericationsurunmode`le Sp´ecications Model checking Preuve manuelle Mod`ele (simplifie´ ) ? Programme source X. Leroy (INRIA) Ve´ rifier un compilateur / 512009-10-08 5
V´ericationsurunmode`le Sp´ecications Model checking Preuve manuelle Mod`ele (simpli´e) ? Programme source X. Leroy (INRIA) Ve´ rifier un compilateur2009-10-08 5 / 51
´eriVionfcatdellemromargorpesme.XtauepmlinuocireV´erRIA)y(INLero
S ´ ifications pec
Preuve de programme
Programme source
Model checking Preuve manuelle Mod`ele (simplifie´ ) ?
Analyse statique
002r01-9680-15/
reL.I(yoAIRNe´V)erincrupiomtelaX
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).
´ Etablirautomatiquementdespropri´et´esdesˆuret´edebase.
Lanalysestatiquepourlasˆuret´e
517/080--10920ur
ateur200uncompil´Vreire(yNIIR)A
nb.
double dotproduct(int n, double * a, double * b) { ... }
L’analyseur statique dit OK s’il peut prouvern <= naetn Il signale un bug potentiel sinon.
<=
15/
int main() {
}
double * a, * b, d ; a = calloc(na, sizeof(double)) ; b = calloc(nb, sizeof(double)) ; /* Remplir a et b */ d = dotproduct(n, a, b) ; ...
Exemple d’analyse statique
01-9880-oreL.X
Astre´e(ENS) : sia[i][0.0,1.5]etb[i][0.0,1.5], alorsdotproduct(10,a,b)[0.0,22.5000007426].
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´esdelarithm´etiquedelamachine: Pas de de´ bordements dans les calculs entiers. Pas de de´ bordements (Inf,NaN) dans les calculs flottants. Bornerlesimpr´ecisionsdescalculsottants.
1/589-001-9002ruetalipmuncoierV´erRIA)(yNIeLor.X
18/0010-00-9ue2rilatcomperuneri
Ait
WCET).
Bornes
(Absint,
le
fines sur
d’exe´ cution
temps
Exemple d’analyse statique
51IRNI´V)AeL.X(yor