esL(aRin.Sctiorodu)IntORIA0’CATCIlairotuTn
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
vo2.612/9
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
rtdocuitOLIR)AnI.Ranise(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
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
Scenario 3: an example of program verification
293/11.2ov