Class Analyses as
Abstract Interpretations
of Trace Semantics
Tratto da un testo di:
Fausto Spoto & Thomas Jensen
Brigo Matteo 795685
Vitturi Mattia 787378
1
Sommario






Introduzione
Un semplice linguaggio
Stati concreti
Trace semantics
Watchpoint semantics
Analisi e Valutazioni
2
Introduzione




Studieremo una trace semantic per un semplice
linguaggio imperativo orientato agli oggetti attraverso
l’uso di watchpoints
Per far ciò definiremo una gerarchia di semantiche
Lo scopo è quello di verificare che la semantica che
otterremo alla fine sarà focalizzata sui watchpoint
Ogni astrazione del dominio computazionale arriva
sempre ad una semantica ancora orientata ai watchpoint
3
Gerarchie di semantiche
4
Un semplice linguaggio



Definiamo ora il linguaggio su cui effettueremo le
operazioni di astrazione
Si tratta di un linguaggio object-oriented basato su java
In tale linguaggio ogni espressione ha un tipo
5
I Tipi






Tale tipo può essere int (l’unico tipo base) o una classe
definita dall’utente
Un Type Environment assegna a un insieme finito di
variabili il loro tipo
Id: Insieme di identificatori contente out e this
K: Insieme di classi ordinate da una relazione di
sottoclasse tale che sia una relazione di ordine parziale
completo
Type: l’insieme dei tipi dato da {int} unito a K
Vars: Sottoinsieme di Id contenente ancora out e this
6
Espressioni [1]



Le variabili locali sono introdotte da un costrutto let
I punti del programma dove l’analisi statica deve essere
incentrata devono essere definiti come watchpoint
I booleani sono interi (true se >=0, false altrimenti)
7
Espressioni [2]

La grammatica è definita come segue:

Con:




t  Type, k  K, i  Z, f,m  Id, v,v’,v1,…,vn  Vars
v’≠this.
Gli operatori + e = operano come operatori su interi
Il costrutto let non introduce variabili già presenti in scope
8
Ulteriori definizioni [1]

Una classe contiene:


Variabili locali (fields)
Funzioni (methods)

Un metodo ha un insieme di variabili di input/output
(parameters) in cui è incluso out, che contiene il risultato,
e this, ovvero l’oggetto dove è stato chiamato il metodo

Fields è un insieme di mappe che uniscono ogni classe
con il Type Environment delle sue variabili locali (this
non può essere un field)
9
Ulteriori definizioni [2]



Methods è un insieme di mappe complete che associa i
metodi di ciascuna classe con un insieme finito di
identificatori di metodi
Par è un insieme di mappe che unisce ogni metodo con
il Type Environment dei sui parametri
Code è un insieme di mappe che unisce ogni metodo
con il suo codice sintatticamente corretto e type-checked
10
Assunzioni [1]

Segue una lista di assunzioni fatte sul programma Prog
da analizzare, specificato da una relazione d’ordine
K*, un insieme M, una mappa F appartenente a
Fields, una mappa M appartenente a Methods, una
mappa P appartenente a Pars e una mappa C
appartenente a Code.
11
Assunzioni [2]

Siano k1,k2 appartenenti a K con k1k2, si ha che:
1. dom(F(k1))  dom(F(k2)) e F(k1) | dom(F(k2))= (k2) (i
field sono ereditati);
2. dom(M(k1))  dom(M(k2)) (methods sono ereditati o
overridden);
3. Sia m appartenente a dom(M(k2));
allora pars=dom(P(M(k1)(m)))=dom(P(M(k2)(m)))
(il nome e numero dei parametri in caso di overriding non
varia);
12
Assunzioni [3]
4.
Sia v appartenente a pars\{out, this};
allora P(M(k1)(m))(v)  P(M(k2)(m))(v) (i parametri di input
diversi da this sono una specializzazione upward)
5.
Sia v appartenente a {out, this};
allora P(M(k2)(m))(v)  P(M(k1)(m))(v) (out e this sono una
specializzazione downward)
6.
Sia k appartenente a K e m appartenente a dom(M(k));
allora P(M(k)(m))(this)  k
(la variabile this di un metodo ha un tipo che è superclasse del
tipo della classe del metodo);
7.
Sia v appartenente a M; allora il codice C(v) è type-checked e
tutte le variabili che occorrono sono generate da un construtto
let o sono tra i parametri P(v).
13
Esempio [1]
14
Esempio [2]
15
Stati concreti

Per rappresentare valori concreti abbiamo bisogno di valori interi,
nil e location ovvero la posizione in memoria dove si trova il dato

Nei dati concreti vi sarà un environment dove sono definite le
variabili e una memory dove sarà rappresentata la mappa che
unisce variables a locations
16
Environment

E’ costituito da coppie Type  Value dove:



Value rappresenta un valore intero, una location o nil
Se Type è intero Value sarà intero, mentre varrà nil o una
location nel caso in cui Type sia appartenente a K
La correttezza di tipo ci assicura che:


non ci siano puntatori pendenti
le variabili siano collegate a locations che contengono
oggetti permessi dal loro environment
17
Possibili stati


I possibili stati in un certo punto del programma sono
dati dalle coppie (variabile,valore associato)Memoria
La variabile this non potrà avere valore nil


Questo porterà ad una semplificazione sostanziale durante lo
studio delle analisi
Tale definizione è consistente con la specifica di Java
18
Operazioni sugli stati [1]
19
Operazioni sugli stati [2]
20
Semantica delle operazioni
La put_field(σ1)(σ2) memorizza il valore res dello stato σ2 in v, che
altro non è che la variabile fornito da σ1 nell’oggetto o.
21
Trace semantic [1]

Sia T un insieme di sequenze non vuote di
computazioni, dove σ rappresenta ciascuna traccia. Una
sequenza di tracce sarà:





Convergente, qualora la sua denotazione possa essere
completamente computata e la sua esecuzione termina
Divergente, qualora un pezzo di codice esegua un loop infinito
Parziale, qualora una parte di codice non possa
completamente eseguita se contiene metodi non stabili
σ1  …  σn rappresenta una computazione
convergente
I watchpoint sono rappresentati dalle frecce identificate
con una etichetta ( l )
22
Trace semantic [2]

Sia t appartenente a T:




fst(t) indica il primo stato di t
con(t): indica che t è convergente
Se con(t) allora l’ultimo stato di t è lst(t)
I comandi e le espressioni sono identificati ad una
mappa da uno stato iniziale a una traccia t. Per le
espressioni se con(t) allora lst(t)(res) è il valore
dell’espressione.
23
Trace semantic [3]

L’ordinamento sulle tracce viene fatto dando una
semantica a punti fissi alle istruzioni iterative (istruzione
while) ed ai metodi ricorsivi.


L’istruzione while viene trattata seguendo il pattern standard
definito per le semantiche denotazionali while-loops
L’ordinamento sulle tracce è un CPO
24
Operazioni sulle tracce [1]
Firma delle operazioni sulle tracce
25
Operazioni sulle tracce [2]
26
Watchpoint semantics [1]



Siamo dunque interessati unicamente alle transizioni
etichettate
Queste ultime possono essere individuate tramite la
collezione di stati che sono preceduti da una transizione
etichettata
Possiamo definire un’astrazione:
w: T  (Label  P(Σ))
27
Perché una nuova semantica?

Per definizione w(t) è più astratto di t e richiede meno
spazio in memoria, ciò è dovuto a




Una computazione a punti fissi più astratta richiede meno
iterazioni
Possiamo unire più watchpoint durante il calcolo dei punti fissi
(come nel caso di while e do c, dove c ha un watchpoint)
Le strutture dati sono più piccole
Si elimina l’operazione di widening necessaria nelle trace
semantic per evitare tracce infinite
28
Watchpoint semantics [2]

Vogliamo osservare gli stati solo nei watchpoint. Quindi:



Vedremo una traccia come un insieme di stati,
Un insieme di stati per ogni watchpoint.
Le watchpoint bags sono l’insieme di possibili Type
Environment ottenibili da una etichetta l.

Nota: vengono usate per raccogliere informazioni sui
watchpoint.
29
Da traces a watchpoint traces

L’astrazione da traces a watchpoint traces avviene
grazie alla funzione

Dove la funzione w(t) appartiene ad una watchpoint bag
e αw è la funzione che trasforma la traccia in una
watchpoint traces.
30
Watchpoint semantic statica



Serve per ottenere informazioni sulle proprietà degli stati
Si tratta di una AI di una semantica statica e possiamo
ancora chiamarla statica
Parte dell’informazione viene persa durante l’astrazione,
che unisce tutti i percorsi di esecuzione in una
watchpoint trace statica
31
Esempio
L’insieme delle tracce S è tale che, se lo stato finale è
σ1 non viene osservato nessun watchpoint e αst non
contiene più questa informazione
32
Watchpoint semantic astratta




La WS statica usa elementi del P(Σ), elementi del
watchpoint bag e denotazioni statiche.
La WS astratta riduce questi elementi alle operazioni
sulle denotazioni statiche.
La WS astratta è dunque una semplificazione della WS
statica
Sarà la WS usata dalle nostre Class Analyses
33
Analisi e Valutazioni

Definiamo 3 class analyses:



Rapid type analysis (rt)
Dataflow analysis (df)
Constraint analysis (ps)

Per ognuna di queste viene definito un dominio astratto
e le operazioni astratte ottimali che induce

Quali sono gli obiettivi?


Mostrare la relazione tra tempo e lo spazio necessari per
numero di watchpoints analizzati
Dimostrare l’efficacia del framework proposto per il test di
analisi
34
Rapid Type Analysis

In termini di AI, questa tecnica equivale a definire
un’astrazione che raccoglie le classi degli oggetti nella
memoria degli stati




Raccoglie l’insieme N di classi create dal comando new
Le classi di una espressione e in un type environment  sono
N ∩ ↓type(e)
Deve contenere una classe compatibile con il tipo di this
Nota: ha una bassa precisione, ma la sua importanza è
data dalla sua applicabilità
35
Dataflow Analysis



Ogni variabile è approssimata per eccesso dall’insieme
delle classi degli oggetti limitati a tale variabile negli stati
concreti
I campi sono astratti nella loro approssimazione
peggiore
Un environment astratto mappa variabili a valori astratti
consistenti con il loro tipo
36
Constraint analysis





Ad ogni variabile di programma e campo è dato un insieme di
classi
Tali insiemi sono correlati tra di loro da delle restrizioni che
modellano il dataflow del programma
Il suo dominio è composto da un abstract environment, identico a
quello dell’analisi df, e da una memoria astratta (ossia un
abstract environment per i fields delle classi)
Si suppone che i fields possano essere identificati unicamente
dal loro nome
Poiché la WS definita è flow sensitive, la stessa variabile può
avere approssimazioni diverse in punti diversi del programma
37
Valutazioni Sperimentali


E’ stato usato per eseguire i test un analizzatore
chiamato LOOP (Localized for Object-Oriented
Programs), che fornisce un’implementazione in
PROLOG della WS presentata
Per effettuare i benchmark sono stati usate come
applicazioni di test 4 programmi:





clone
visit
inv
figures
La macchina su cui sono stati effettuati i test è un
Pentium III 660Mhz con 512MB di RAM
38
LOOP





analyser: implementa la semantica a tracce
semantic: implementa le sue operazioni
combinators: le operazioni sono compilate come
chiamate a metodo
typenv: implementa il type environment
aux: implementa funzioni ausiliarie
39
Esempi di Analisi: rt
40
Esempi di Analisi: df
41
Esempi di Analisi: ps
42
Risultati
43