Interpretazione Astratta

Tino Cortesi Analisi e Verifica di Programmi 2

Astrazione: selezionare una proprieta’

Tino Cortesi Analisi e Verifica di Programmi 3

Astrazione: selezionare una (delle)

proprieta’

Tino Cortesi Analisi e Verifica di Programmi 4

Astrazione e correttezza

Tino Cortesi Analisi e Verifica di Programmi 5

Astrarre un insiemi di punti nel piano…

Tino Cortesi Analisi e Verifica di Programmi 6

Interpretazione AstrattaUna tecnica utilizzata da quasi 30 anni (Patrick e Radhia Cousot, 1977) per trattare in modo sistematico astrazioni e approssimazioniNata per descrivere analisi statiche di programmi imperativi e provarne la correttezza. Sviluppata soprattutto su linguaggi dichiarativi (logici e funzionali)Vista oggi come tecnica generale per ragionare su semantiche a diversi livelli di astrazioneApplicata con successo a sistemi distribuiti per verifica di programmi (correttezza – sicurezza)

Tino Cortesi Analisi e Verifica di Programmi 7

L’idea generaleil punto di partenza è la semantica concreta, ovvero una funzione che assegna significati ai comandi di un programma in un dominio fissato di computazione.un dominio astratto, che modella alcune proprietà delle computazione concrete, tralasciando la rimanente informazione (dominio di computazione astratto)derivare una semantica astratta, che permetta di eseguire il programma sul dominio astratto per calcolare la proprietà che il dominio astratto modella.applicando un algoritmo di punto fisso sarà quindi possibile calcolare staticamente una approssimazione corretta della semantica astratta

Tino Cortesi Analisi e Verifica di Programmi 8

Semantica concretaConsideriamo un linguaggio molto limitato, che permette unicamente di operare su moltiplicazioni di interi.La semantica di questo linguaggio si può descrivere mediante una funzione definita da:

1 2 1 2

|

:

( )

( ) ( ) ( )

e i e e

Exp I nt

i i

e e e e

Tino Cortesi Analisi e Verifica di Programmi 9

Semantica astrattaPossiamo considerare un’astrazione della semantica concreta (semantica astratta) che calcola solo il segno

delle espressioni

1 2 1 2

:Exp ,-,0

if 0 0( ) 0 if 0 0

if 0 0 0 0 0

( ) ( ) ( ) 0

i

i i

i

e e e e

Tino Cortesi Analisi e Verifica di Programmi 10

CorrettezzaPossiamo dimostrare che questa astrazione è corretta, ovvero che predice correttamente il segno delle espressioni.La dimostrazione è per induzione strutturale sull’espressione e, ed utilizza le proprietà della moltiplicazione tra interi (il prodotto di due positivi è positivo, ecc.).

( ) 0 ( )

( ) 0 ( ) 0

( ) 0 ( )

e e

e e

e e

Tino Cortesi Analisi e Verifica di Programmi 11

Una prospettiva diversaPossiamo associare ad ogni valore astratto l’insieme di

valori concreti che esso rappresenta:

: { ,0, } 2

( ) | 0

(0) 0

( ) | 0

I nt

i i

i i

Tino Cortesi Analisi e Verifica di Programmi 12

ConcretizzazioneLa funzione di concretizzazione mappa un valore astratto in un insieme di valori concretiIndichiamo con D il dominio concreto e con A il dominio astratto

( ) ( ( ))e e

Exp

A

2D

Tino Cortesi Analisi e Verifica di Programmi 13

Interpretazione AstrattaQuesta è una Interpretazione Astratta.

Una computazione in un dominio astrattoIn questo caso, il dominio è {+,0,-}.

La semantica astratta è corretta è un’approssimazione della semantica concreta

La funzione di concretizzazione stabilisce la connessione tra i due domini

Tino Cortesi Analisi e Verifica di Programmi 14

Aggiungiamo -Aggiungiamo al nostro tiny language l’operatore unario di cambiamento di segno

( ) ( ) 0

0( ) ( )

e e

e e

Tino Cortesi Analisi e Verifica di Programmi 15

Aggiungiamo +Aggiungere l’addizione è più complesso, in quanto il dominio astratto non è chiuso rispetto a questa operazione

A quale valore astratto corrisponde il risultato della somma di due numeri interi con segno opposto?

1 2 1 2

1 2 1 2

0( ) ( ) ( ) ?

( ) ( ) ( ) 0 0

?

e e e e

e e e e

Tino Cortesi Analisi e Verifica di Programmi 16

SoluzioneAggiungiamo un nuovo elemento astratto che rappresenta un qualsiasi numero intero

0 T

T T(T) I nt 0 0 T

T T

T T T T T

Tino Cortesi Analisi e Verifica di Programmi 17

Estendere le altre operazioni

Avendo aggiunto un elemento al dominio astratto, è necessario estendere le operazioni astratte già definite

0 T

0 T0 T

0 0 0 0 00 T

0 T

T T 0 T T

Tino Cortesi Analisi e Verifica di Programmi 18

Esempi

((1 2) 3) 0

((1 2) 3) ( ) ( ) T

((5 5) 6) 31

((5 5) 6) ( )

In alcuni casi c’è perdita di informazione dovuta alle operazioni

In altri casi non c’è perdita di informazione

Tino Cortesi Analisi e Verifica di Programmi 19

Aggiungiamo /Aggiungere la divisione intera (con resto) / non da problemi, eccetto il caso della divisione per 0.Se dividiamo gli intero di un insieme di interi per 0 che risultato otteniamo? L’insieme vuoto. Questo è rappresentato da un nuovo elemento, , rispetto al quale si devono estendere le altre operazioni

/ 0 T

0 T

0( ) 0 T

T T 0 T T

x

x

Tino Cortesi Analisi e Verifica di Programmi 20

Il dominio astrattoIl dominio astratto è un reticolo completoL’ordine parziale è coerente con la funzione di concretizzazione:

Ogni sottoinsieme ha un least upper bound (lub) ed un greatest lower bound (glb): è un reticolo completo

0

T

( ) ( )x y x y

Tino Cortesi Analisi e Verifica di Programmi 21

La funzione di astrazioneAlla funzione di concretizzazione corrisponde una funzione di astrazione .La funzione mappa insiemi di valori concreti in un valore astratto (il più piccolo che li rappresenta tutti).Nel nostro esempio,

I nt:2 A

( ) lub | 0 , 0| 0 , | 0

( ) ({ })

S i i S S i i S

i i

Tino Cortesi Analisi e Verifica di Programmi 22

Definizione GeneraleUna Interpretazione Astratta consiste in:

Un dominio astratto A ed un dominio concreto D A e D reticoli completi. L’ordine riflette la precisione (più piccolo = più preciso)Funzioni di concretizzazione e di astrazione monotone, che formino una inserzione di Galois.Una funzione che astrae correttamente la semantica (operazioni astratte).

Inserzione di Galois:

2 . ( ( ))

. ( ( ))

Dx x x

a A x x

Tino Cortesi Analisi e Verifica di Programmi 23

Un altro esempiosign(x) , if x= bot

{y|y>0}, if x= +{y|y0}, if x= 0+{0}, if x= 0{y|y0}, if x= 0-{y|y<0}, if x= - ZZ, if x= top

signy) = glb dibot , if y= - , if y {z| z < 0}0- , if y {z | z 0}0 , if y {0}0+ , if y {z | z 0}+ , if y {z | z 0}top , if y ZZ

0-

top

0 - +

bot

0+

sign({0,1,3})= 0+

sign(0+) {0,1,3}, {3,34,2}, ...

sign(sign({0,1,3})) {0,1,3}

sign(sign(0+)) = 0+

Tino Cortesi Analisi e Verifica di Programmi 24

Inserzioni di Galois(CC, )(AA, ): AA CC (concretizzazione):CC AA (astrazione)

monotonexCCx xyAAyysi determinano a

vicenda

C A

Tino Cortesi Analisi e Verifica di Programmi 25

Astrarre una funzione in modo ottimale: f# = f

Abstract domain

Concrete domain

f

f#

Operazioni astratte

Tino Cortesi Analisi e Verifica di Programmi 26

Astrazioni come chiusureIl dominio astratto può essere ottenuto dividendo il dominio concreto in sottoinsiemi (non disgiunti) ai.

La funzione di astrazione mappa un sottoinsieme del dominio nel più piccolo di questi ai che lo contiene.