Decision Procedures for the Formal Analysis of Software [3mm ...
24
pages
English
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
24
pages
English
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
Decision Procedures for the
Formal Analysis of Software
Tutorial Overview
D. Déharbe, P. Fontaine,SilvioRanise, C. Ringeissen
UFRN (Natal, Brasil) andLORIA&INRIA Lorraine(Nancy,France)
Tutorial ICTAC’06 — November 21, 2006
S.Ranise (LORIA) Introduction TutorialICTAC’06 Nov. 21 1/29 Outline
1 Program Verification and Logic
2 Some scenarios
Scenario 1: an optimizing compilerio 2: revisited
Scenario 3: program verification
3 SMT problems and solvers
4 SMT Lib Initiative
5 Tutorial Timetable
S.Ranise (LORIA) Introduction TutorialICTAC’06 Nov. 21 2/29 Program Verification and Logical Problems
Many approaches to software verification:
Hoare logic (e.g., Why tool)
software model checking (e.g., SLAM)
program analysis (e.g., Jahob)
require to discharge some proof obligations, i.e.
checkingthatsomeformula,usually,offirst orderlogicwith
equality(FOLE)isvalidw.r.t.(modulo)agiventheory
modeling
I the user defined data types of the software system under scrutiny
I the memory model used by the programming language
I its type system, ...
For such program verification techniques, it is of crucial importance to
have reasoning tools which are both
scalable
predictable, and
expressive
S.Ranise (LORIA) Introduction TutorialICTAC’06 Nov. 21 4/29 Scenario 1: what is an (optimizing) compiler?
Definition (Compilers)
Special programs that take instructions written in a high level language
(e.g., C, Pascal) and convert it into machine language or code the
computer can understand.
Example
Consider the ...
Voir
Formal Analysis of Software
Tutorial Overview
D. Déharbe, P. Fontaine,SilvioRanise, C. Ringeissen
UFRN (Natal, Brasil) andLORIA&INRIA Lorraine(Nancy,France)
Tutorial ICTAC’06 — November 21, 2006
S.Ranise (LORIA) Introduction TutorialICTAC’06 Nov. 21 1/29 Outline
1 Program Verification and Logic
2 Some scenarios
Scenario 1: an optimizing compilerio 2: revisited
Scenario 3: program verification
3 SMT problems and solvers
4 SMT Lib Initiative
5 Tutorial Timetable
S.Ranise (LORIA) Introduction TutorialICTAC’06 Nov. 21 2/29 Program Verification and Logical Problems
Many approaches to software verification:
Hoare logic (e.g., Why tool)
software model checking (e.g., SLAM)
program analysis (e.g., Jahob)
require to discharge some proof obligations, i.e.
checkingthatsomeformula,usually,offirst orderlogicwith
equality(FOLE)isvalidw.r.t.(modulo)agiventheory
modeling
I the user defined data types of the software system under scrutiny
I the memory model used by the programming language
I its type system, ...
For such program verification techniques, it is of crucial importance to
have reasoning tools which are both
scalable
predictable, and
expressive
S.Ranise (LORIA) Introduction TutorialICTAC’06 Nov. 21 4/29 Scenario 1: what is an (optimizing) compiler?
Definition (Compilers)
Special programs that take instructions written in a high level language
(e.g., C, Pascal) and convert it into machine language or code the
computer can understand.
Example
Consider the ...
Tutorial Overview
D. Déharbe, P. Fontaine, Silvio Ranise , C. Ringeissen
Decision Procedures for the Formal Analysis of Software
291/21v.No6-
UFRN (Natal, Brasil) and LORIA & INRIA-Lorraine (Nancy, France)
Tutorial ICTAC’06 — November 21, 2006
2
3
Outline
Some scenarios Scenario 1: an optimizing compiler Scenario 2: optimizing compiler revisited Scenario 3: program verification
9/2
Program Verification and Logic
Tutorial Timetable
1
SMT-Lib Initiative
5
SMT problems and solvers
4
tionoducrialTuto’C60CIAT2.21N-voIntrRIA)e(LOanisSR.
Program Verification and Logical Problems
9
Many approaches to software verification: Hoare logic (e.g., Why tool) software model checking (e.g., SLAM) program analysis (e.g., Jahob) require to discharge some proof obligations, i.e. checking that some formula, usually, of first-order logic with equality (FOLE) is valid w.r.t. (modulo) a given theory modeling I the user-defined data types of the software system under scrutiny I the memory model used by the programming language I its type system, ...
For such program verification techniques, it is of crucial importance to have reasoning tools which are both scalable predictable , and expressive
SR.naise(LORIA)IntroditcuuTnoirotCIlaC’TA-N06.2ov/214
Problem : sub-expressions are needlessly re-computed !
Scenario 1: what is an (optimizing) compiler ?
Example Consider the following simple program fragment in C:
Definition (Compilers) Special programs that take instructions written in a high level language (e.g., C, Pascal) and convert it into machine language or code the computer can understand.
... int x,y,z; s0: ... /* y and z are initialized */ s1: x = (y+z) * (y+z) * (z+y) * (z+y); ...
dortnI)AuTnoitcuICalrito-N06C’TA.RanSLORIise(
Scenario 1: an (optimizing) compiler
int x,y,z; s0: ... /* y and z are initialized */ s1: x = (y+z) * (y+z) * (z+y) * (z+y) ;
into
int x,y,z; int aux1,aux2 ; t0: ... /* y and z are initialized */ t1: aux1 = (y+z); t2: aux2 = (z+y); t3: x = aux1 * aux1 * aux2 * aux2;
which avoids the re-computation of sub-expressions !
Example (cont’d) By exploiting only the syntactic structure of sub-expressions, transform
v.217/29CA0’-6oNroaiIlTCudortnI)tuTnoitcniRaS.IAOR(Lse
Correctness of the compiler as a logical problem Example (cont’d) QUESTION : how can we guarantee that the value stored in x after the computation of the transformed program is equal to that in x after the computation of the source ? ANSWER : ignore the arithmetic properties of all arithmetic operations and consider them as uninterpreted functions (UF) (i.e. + ❀ f and ∗ ❀ g ). Then, discharge the following proof obligation: 0 xy ss 10 == gy t ( 0 g ∧ ( fz ( s y 0 s 0 , = z s z 0 t 0 ) , f ( y s 0 , z s 0 )) , g ( f ( z s 0 , y s 0 ) , f ( z s 0 , y s 0 ))) ∧∧ 1 T UF | = aux1 t 1 = f ( y t 0 , z t 0 ) ∧ ⇒ x s 1 = x t 3 B @ aux2 t 2 = f ( z t 0 , y t 0 ) ∧ A C x t 3 = g ( g ( aux1 t 1 , aux1 t 1 ) , g ( aux2 t 2 , aux2 t 2 )) What is T UF ? S. Ranise (LORIA) Introduction Tutorial ICTAC’06 - Nov. 21 8 / 29
T UF is the set of sentences which are true in the class of all structures satisfying the above axioms (i.e., models of T UF ) How do we reason in T UF ? In particular, how can we design techniques to reason in T UF ?
The following axioms stipulates that = is a congruence relation (i.e., a reflexive, symmetric, and transitive relation closed under substitution of equals by equals)
A definition of T UF and ...
∀ x . ( x = x ) ∀ x , y . ( x = y ⇒ y = x ) ∀ x , y , z . ( x = y ∧ y = z ⇒ x = z ) ∀ ... x , y ... ( x = y ⇒ f ( ... x ... ) = f ( ... y ... )) for each function symbol f
19.29/2TutotionoducIntrN-vo’C60CIATirla)AIROL(esinaR.S
Example (cont’d) By exploiting the syntactic structure of sub-expressions and properties of + , transform
int x,y,z; s0: ... /* y and z are initialized */ s1: x = (y+z) * (z+y);
into
int x,y,z; int aux ; t0: ... /* y and z are initialized */ t1: aux = (y+z); t2: x = aux * aux;
which avoids the re-computation of sub-expressions !
Scenario 2: a more complex (optimizing) compiler
92/0112.voN-60C’TAICalritoTuon
Example (cont’d) QUESTION : how can we guarantee that the value stored in x after the computation of the transformed program is equal to that in x after the computation of the source ? ANSWER : ignore the arithmetic properties of * and consider it as an uninterpreted function g . Then, discharge the following proof obligation:
0 y s 0 = y t 0 ∧ z s 0 = z t 0 ∧ 1 x s 1 = g ( y s 0 + z s 0 , z s 0 + y s 0 ) ∧ T UF ∪ T LA | = B @ aux t 1 = y t 0 + , za t 0 ux t 1 ) ∧ A C ⇒ x s 1 = x t 2 x t 2 = g ( aux t 1
What is T LA ? What does it mean T UF ∪ T LA ? Why can we not ignore the arithmetic properties of + ?
29
Revisiting the correctness of the compiler
111/IROLnI)AnaR.(esiTuonritoodtrtiucS
A definition of T LA , T UF ∪ T LA , and ...
T LA the set of all the sentences that are true in the structure of the integer numbers interpreting + as addition T UF ∪ T LA is the combination of T UF and T LA , i.e. the set of all the sentences that are true in the structure of the integer numbers interpreting + as addition and all other function symbols as uninterpreted How do we reason in T UF ? How do we reason in T LA ? How do we reason in T UF ∪ T LA ? In particular, can we modularly re-use our techniques to reason in T UF and T LA for their union ?
ICTArial-NovC’06
I/O : program Prg manipulating a square matrix r of dimension n What : Prg updates only the elements on the diagonal of r Property : Check that if the matrix r is symmetric before the execution of Prg , then the matrix r 0 (obtained by the execution of Prg with r as input) is also symmetric
Scenario 3: an example of program verification
293/11.2ov
