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/29Outline 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/29Program 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/29Scenario 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 ...
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
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
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
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
vo2.60N-AT’ClaCI
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
cudortnIotuTnoitisan.RSA)RILOe(/2922.11
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
uctionTuA)IntrodAT’C60N-otirlaCI(esiIROLSnaR.
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