Decision Procedures for the Formal Analysis of Software [3mm ...

Description

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

Subjects

• Documents
• Knowledge
• Tutoriel
• Tunnel Prado-Carénage
• UFO
• T1
• Theory of a Deadman
• Ligne d'abonné numérique à débit symétrique

Informations

• Published by: Chawyog
• Reads: 207
• Language: English

Exrait

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 x y s s 1 0 = = g y t ( 0 g ∧ ( f z ( 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 + , z a 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