Pubblicazioni

Autori:

Nikolic, Durica

Titolo:

A General Framework for Constraint-Based Static Analyses of Java Bytecode Programs

Anno:

2013

Tipologia prodotto:

Doctoral Thesis

Tipologia ANVUR:

Altro

Lingua:

Inglese

Formato:

A Stampa

Parole chiave:

Static Analysis; Abstract Interpretation; Java Bytecode; Pointer Analysis; Reachability Analysis; Aliasing Analysis; Constraint-based Analysis

Abstract (italiano):

Questa tesi introduce un generico e parametrizzato framework per analisi statica dei programmi Java bytecode, basato sulla generazione e soluzione dei vincoli. All'interno del framework è possibile gestire sia i flussi di eccezione all'interno di programmi analizzati, sia i side-effect indotti dalle esecuzioni dei metodi che possono modificare la memoria. Questo framework è generico nel senso che diverse istanziazioni dei suoi parametri risultano in diverse analisi statiche capaci di catturare varie proprietà relative alla memoria delle variabili del programma ad ogni punto del programma. Le analisi statiche definite dal framework sono basate su interpretazione astratta, e quindi le proprietà d'interesse sono rappresentate da dei domini astratti. Il framework può essere usato per la definizione sia delle analisi statiche che producono le approssimazioni del tipo "possible" oppure "may", che quelle del tipo "definite" oppure "must". Nel primo caso, il risultato di tali analisi è una sovra-approssimazione di quello che potrebbe essere vero ad un certo punto del programma, mentre nel secondo caso il risultato rappresenta una sotto-approssimazione della situazione reale. Questa tesi fornisce un insieme di condizioni che diverse istanziazioni dei parametri del framework devono soddisfare affinché le analisi statiche definite all'interno del framework siano "sound" (corrette). Quando i parametri istanziati soddisfano tali condizioni, il framework garantisce la correttezza dell'analisi corrispondente all'istanziazione in questione. Il vantaggio di questo approccio è che il designer di una nuova analisi statica deve soltanto mostrare che i parametri da lui istanziati soddisfano i criteri specificati dal framework.In questo modo la dimostrazione di correttezza dell'analisi completa è semplificata. Questa è una caratteristica molto importante del presente lavoro. La tesi introduce due nuove analisi statiche relatve alle proprietà della memoria: la Possible Reachability Analysis Between Program Variables e la Definite Expression Aliasing Analysis. La prima rappresenta un esempio delle analisi "possible" e determina, per ogni punto p del programma, quali sono le coppie ordinate delle variabili <v, w> disponibili a tale punto, tali che v potrebbe raggiungere w al punto p, ovvero, che a partire dalla variabile v è possibile seguire un insieme di locazioni di memoria che portano all'oggetto legato alla variabile w. La seconda analisi è un esempio delle analisi "definite" e determina, per ogni punto p del programma ed ogni variabile v disponibile a tale punto, un insieme di espressioni il cui valore è sempre uguale al valore che la variabile v può avere al punto p, per ogni possibile esecuzione. Entrambe le analisi sono state formalizzate e dimostrate corrette grazie ai risultati teorici del framework introdotto in questa tesi. In più, entrambe le analisi sono state implementate all'interno dell'analizzatore statico per Java e Android chiamato Julia (www.juliasoft.com). Gli esperimenti eseguiti sui programmi reali mostrano che la precisione dei principali tool di Julia (nullness e termination tool) è migliorata rispetto alle versioni precedenti di Julia nelle quali le nuove analisi non erano presenti.

Id prodotto:

76767

Handle IRIS:

11562/546351

depositato il:

11 aprile 2013

ultima modifica:

26 ottobre 2022

Citazione bibliografica:

Nikolic, Durica, A General Framework for Constraint-Based Static Analyses of Java Bytecode Programs

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo