23/11/06 Dino Puller 1

Analisi statica in tempo reale con Analisi statica in tempo reale con domini numericidomini numerici

Facoltà di scienze MM.FF.NN.

Università degli studi di Verona

23/11/06 Dino Puller 2

Obiettivi della tesiObiettivi della tesi

Creare un analizzatore statico che operi in tempo reale

Migliorare la precisione del dominio astratto degli intervalli

23/11/06 Dino Puller 4

Analisi staticaAnalisi statica

Indispensabile per progetti mission-critical

Riduce il numero di bugRiduce il tempo di verificaSvantaggi:

– Nuova fase nel ciclo di vita del software– L’analisi può essere lunga

23/11/06 Dino Puller 5

Idea: Analisi in tempo realeIdea: Analisi in tempo reale

Ambiente di sviluppo con analisi statica integrata– Interpretazione astratta

Ad ogni modifica del codice mostri le invarianti calcolate

23/11/06 Dino Puller 6

ProblemiProblemi

Impossibile per un intero progettoLinguaggi troppo complessi

– Side effect– Strutture dati

Chiamata a funzione– Ricorsione– Virtualmente un singolo algoritmo può

essere troppo lungo

23/11/06 Dino Puller 7

SoluzioniSoluzioni

Analisi di un singolo algoritmo– Raramente supera le cento righe

Nuovo linguaggio “Toy” più semplice:– Intervalli interi– If, while, chimata a funzione– Nessuna struttura dati– Ricorsione vietata

Cache di chiamate a funzione:– Chiave: Nome funzione + parametri– Risultato: invariante calcolata

23/11/06 Dino Puller 8

Metodi di analisiMetodi di analisi

Dominio astratto degli intervalli Linearizzazione Linearizzazione + Dominio di costanti

simbolicheNuove tecniche: Intervalli + Semplificazione algebrica +

Dominio di costanti simboliche Semplificazione algebrica + Dominio di costanti

simboliche + Linearizzazione

23/11/06 Dino Puller 9

LinearizzazioneLinearizzazione

Riscrive espressioni lavorando sulla sintassi Può semplificare gli addendi Esempio:

X ← [0, 1]

Y ← [0, 10]

Z ← [0, 20]

T ← X × Y − X × Z + Z T → [0, 30]

23/11/06 Dino Puller 10

Dominio di costanti simbolicheDominio di costanti simboliche

Ad ogni assegnamento propaga espressioni Esempio:

X ← [0, 5]

T ← X

Y ← T − 2 × X Diventa: Y ← X − 2 × X Con la linearizzazione: Y → − X

23/11/06 Dino Puller 11

Svantaggi della linearizzazioneSvantaggi della linearizzazione

La linearizzazione semplifica solo somme e sottrazioni

Usa tecniche euristicheSfrutta la forma affine che non è capace

di gestire i prodotti

23/11/06 Dino Puller 12

Algebra simbolicaAlgebra simbolica

Esempio:a ← [1, 5]b ← [−5, 5]c ← [1, 5]d ← a + b − az ← a × b/a − d

Linearizzazione + dominio di costanti

z → [−20, 20] Algebra simbolica

z → [0, 0]

Rappresentazione di espressioni algebriche in forma letterale–Simile a quella usata in analisi matematica–Gestita da alberi simbolici–Fa uso del Dominio delle costanti simboliche

23/11/06 Dino Puller 13

Metodo mistoMetodo misto

In alcuni casi la linearizzazione è superiore perché valuta espressioni per cercare nuove semplificazioni

Metto tutto assieme:1. Semplifico con l’algebra simbolica

2. Uso la linearizzazione per ulteriori semplificazioni

23/11/06 Dino Puller 14

L’analizzatore in azioneL’analizzatore in azione

Filmato del programma

23/11/06

23/11/06 Dino Puller 16

Il resto della divisioneIl resto della divisione

a ← [0 ,10]

b ← 3

c ← mod(a,b)Con ogni metodo di analisi:

c → [−9, 10]

23/11/06 Dino Puller 17

EuclideEuclide

a ← [0 ,10]b ← 3c ← mcd(a,b)c → [1,+∞] perché abbiamo un ciclo e

mod cresce anziché diminuire Restrizione

mod ← clamp (mod, 0 , y−1)c → [1,3]

while y>0 do

z ← x

x ← y

y ← mod (z,y)

end

23/11/06 Dino Puller 18

Divisione per ZeroDivisione per Zero

Introduciamo un errore

while y>=0 do

z ← x

x ← y

y ← mod( z , y )

end

MCD:mcd → [⊥]x → [⊥]y → [⊥]z → [0, 10]

23/11/06 Dino Puller 19

Ciclo infinitoCiclo infinito

X ← 0

while x < 100 do

x ← x − 1

end x → [ ]⊥

– Operazione svolta¬ Guardia = [100 , +]lfp(x) = [-,0][100 , +] ∩ [-,0] =

23/11/06 Dino Puller 20

Un problema di fisicaUn problema di fisica

Calcolo dell’accelerazione del centro di massa

g ← [9 ,10]

m ← [1 ,10]

r ← [1 ,5]

s i n _ a l f a ← 1/2

Ia ← 3 × m × r × r / 2

Acm ← m × g × r × r × s i n _ a l f a / I a

Intervalli/linearizzazione

Ia → [1, 375]Acm → [0, 1667]

Algebra simbolica

Ia → [1, 375]Acm → [3, 7]

23/11/06 Dino Puller 21

Software di bordoSoftware di bordo

Altimetro– Calcolato in base alla pressione interpolando

valori da una tabella altitude → [ ]⊥ Dopo modifica a interpolate semanticamente

equivalente interpolate ← interp( x, x∪ ∪ 0, x∪ 1 , y∪ 0 , y∪ 1 )

∪interpolate ← interp(x, x0, x1 , y0 , y1 ) altitude → [0, 20669] Risultato corretto

23/11/06 Dino Puller 22

Risultati ottenutiRisultati ottenuti

Sviluppato un prototipo capace di– Analisi statica in tempo reale– Gestire intervalli di test– Cache per evitare analisi inutili– 5 metodi di analisi– Allarmi

• Overflow• Underflow• Divisione per zero• Non terminazione dei cicli

23/11/06 Dino Puller 23

Commenti sugli esempiCommenti sugli esempi

Verificati 6 programmi– 2 programmi senza allarmi– 2 allarmi positivi– 2 falsi allarmi

• eliminato grazie alla funzione di restrizione• eliminato modificando interpolate mantenendola

semanticamente equivalenteRisultati indipendenti dal metodo di analisi

– Eccetto nel problema di fisica

23/11/06 Dino Puller 24

ConclusioniConclusioni

Dimostrata la fattibilità di una analisi statica in tempo reale

Dimostrata la correttezza di algoritmi– seppur con qualche modifica– usando il dominio astratto degli intervalli

Individuato allarmi positiviDimostrata l'utilità di riscrittura delle

espressioni per migliorare domini astratti

23/11/06 Dino Puller 25

Lavori futuriLavori futuri

Aggiungere nuovi domini astratti– Ottagoni– Poliedri

Potenziare la semplificazione algebrica con nuove regole– Raccogliere a fattor comune

Trasformazioni semantiche equivalenti non solo su espressioni