Comment faire confiance à un compilateur?

Xavier Leroy

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

• informatique

Informations

• Publié par: Nishor
• Nombre de lectures: 70
• Langue: Français

Extrait

oyer.LXV)AIRNI(urefiire´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 ´ erificationdeprogrammes

RIA)V´erifieruncompilateur0290-10-082/51

NRIA)V´e.Leroy(IX513/080--10920uretalipmocnurefiir

Intole´ rable !

Le bug

Tolerable ? ´

«nEniofmrtaqieua¸cemmocy’nsuov,ebally,ist’e;cugezripouven.» (G ´ erardBerry,Colle ` gedeFrance,17/01/2008.)

NI(y)AIR.XoreLcounilmperV´erifi

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 ´ erificationsurunmode ` le Sp ´ ecifications Model checking Preuve manuelle Mod ` ele (simplifie´ ) ? Programme source X. Leroy (INRIA)  Ve´  rifier un compilateur / 512009-10-08 5

V ´ erificationsurunmode ` le Sp ´ ecifications Model checking Preuve manuelle Mod ` ele (simplifi ´ e) ? Programme source X. Leroy (INRIA)  Ve´  rifier un compilateur2009-10-08 5 / 51

´eriVionfficatdellemromargorpesme .XtauepmlinuocfiireV´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)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).

´ Etablirautomatiquementdespropri ´ et ´ esdesˆuret ´ edebase.

L’analysestatiquepourlasˆuret ´ e

517/080--10920ur

ateur200uncompil´Vrefiire(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 ´ esdel’arithm ´ etiquedelamachine: Pas de de´  bordements dans les calculs entiers. Pas de de´  bordements (Inf,NaN) dans les calculs flottants. Bornerlesimpr ´ ecisionsdescalculsflottants.

1/589-001-9002ruetalipmuncoifierV´erRIA)(yNIeLor.X

18/0010-00-9ue2rilatcomperunerifi

Ait

WCET).

Bornes

(Absint,

le

fines sur

d’exe´ cution

temps

Exemple d’analyse statique

51IRNI´V)AeL.X(yor