RICERCA ITALIANA     

Programma di ricerca

AIDA2007 - Interpretazione Astratta: Progettazione e Applicazioni

Università di riferimento

Università degli Studi di PARMA - MATEMATICA - ()

Responsabile dell'Unità di ricerca

Roberto Bagnara

Descrizione

INTRODUZIONE

L'obiettivo del progetto è investigare sull'applicazione di tecniche di interpretazione astratta allo scenario più realistico: applicazioni scritte da comuni programmatori in linguaggi di largo uso come C, C++ e Java. Per poter influire positivamente su tale scenario, ogni soluzione proposta deve essere integrabile con il software, gli ambienti e le pratiche di programmazione esistenti nonché con le conoscenze comunemente possedute dai programmatori.

WP1: PROGETTAZIONE DI INTERPRETAZIONI ASTRATTE

Task PR-1.1: Domini astratti per l'analisi dei puntatori e dell'aliasing in programmi C e Java

Il dominio proposto in [EGH94] per l'analisi dei puntatori sullo stack nei programmi C consente di definire un'analisi, dipendente dal contesto e dal controllo di flusso, in grado di catturare sia la possibilità sia la presenza certa di aliasing, incluse alcune proprietà dei puntatori ad array e struct. Un ragionamento preciso sulla correttezza e precisione dell'approccio di [EGH94] è complicato dalla mancanza di una specifica formale. Vogliamo quindi riprogettare ed implementare una variante di questo dominio astratto, mettendo una cura particolare nel chiarire tutte le ipotesi che stanno alla base delle dimostrazioni di correttezza dell'analisi e prendendo come semantica concreta di riferimento quella specificata dallo standard del linguaggio C [Int99], possibilmente arricchita dalla formalizzazione di alcuni comportamenti dipendenti dall'implementazione. Questo consentirà una migliore separazione tra le scelte progettuali che sono imposte dalla natura conservativa dell'analisi, rispetto a quelle che sono adottate per semplificarne l'implementazione o per migliorarne l'efficienza e la scalabilità; inoltre, una specifica più accurata permetterà lo studio formale delle dipendenze e possibili sinergie tra l'analisi dei puntatori ed altre analisi di proprietà di safety.

Per l'analisi di aliasing nei programmi Java, studieremo la definizione di un framework concettuale comune all'interno del quale possano essere inquadrate la maggior parte delle proposte che si trovano in letteratura. In ciò prendiamo spunto dalla situazione che si ha nel campo della programamzione logica, dove quasi tutte le analisi sono ottenute come astrazione della stessa semantica, basata sull'insieme delle parti delle sostituzioni con gli operatori di ridenominazione, proiezione ed unificazione [CFW96]. In particolare, pensiamo di riformulare molte delle note varianti di analisi di aliasing e di shape come astrazioni di una stessa semantica denotazionale, sensibile al flusso di esecuzione e al contesto. Ciò consentirà il confronto formale tra i principali punti di forza e debolezza dei vari approcci, nonché la possibilità di separare il problema della rappresentazione delle informazioni dei domini astratti dalla specifica dei corrispondenti algoritmi per il calcolo dell'analisi. Basando gli studi su di una solida semantica denotazionale, sarà inoltre possibile investigare nuovi domini ed operatori astratti. Per esempio, [SS05] introduce un'analisi di pair-sharing che si ispira ad un noto dominio astratto sviluppato per l'analisi di programmi logici. Pur non essendo particolarmente precisa, tale analisi ha buone doti di scalabilità. La precisione potrebbe migliorare combinando il dominio con altre proprietà, quali la costanza o altri tipi di informazione strutturale. Vorremmo inoltre studiare l'applicabilità al caso in esame di altre proprietà e domini sviluppati nel contesto dei linguaggi logici, quali la linearità e set-sharing.

Task PR-1.2: Domini numerici scalabili e precisi

Esiste un'ampia letteratura sul progetto di domini astratti numerici: da semplici proprietà non relazionali (ad esempio intervalli e congruenze non relazionali) a domini che codificano proprietà relazionali ben più complesse (insiemi di poliedri convessi, disuguaglianze polinomiali ecc.). La questione è come ci si possa avvicinare all'efficienza e scalabilità dei domini più semplici ottenendo una precisione confrontabile con quella dei domini più complessi. La maggior parte degli studi in corso, nella ricerca di compromessi vantaggiosi, esplora lo spazio esistente tra gli estremi sopra menzionati. In questo progetto, affronteremo il problema:

1) progettando operatori approssimati che consentano di cedere precisione, in modo controllato e in contesti determinati, in cambio di efficienza (nuove euristiche di widening [CC76,CC77,CC92a], versioni non ottimali degli operatori di transizione di stato, partizionamenti dello spazio delle variabili [CCF+05], ...);

2) progettando nuove combinazioni dei domini esistenti e dei corrispondenti operatori per integrarli efficacemente.

Per questo lavoro, l'esperienza maturata dall'unità di Parma sul progetto di domini numerici e operatori di widening sarà molto utile [BDH+07,BHZ05,BHMZ05,BHRZ05,BHZ06]. L'implementazione e la sperimentazione avverranno nel contesto della Parma Polyhedra Library (PPL) [BHZ08].

E' rilevante il fatto che ricercatori dell'unità di Parma prenderanno attivamente parte al progetto GlobalGCC (GGCC) del programma ITEA (Information Technology for European Advancement), il cui obiettivo è quello di estendere la GNU Compiler Collection (GCC) con tecniche di analisi statica globale. Le analisi statiche di GGCC saranno al livello della rappresentazione interna GIMPLE, e saranno così utilizzabili per tutti i linguaggi sorgente ed i sistemi target supportati da GCC. Le analisi di proprietà numeriche di GGCC saranno basate sulla PPL. Il consorzio GGCC (che comprende, tra gli altri, Bertin Technologies, CEA-LIST, INRIA-Futurs, Mandriva, Telefonica I+D e UPM) sta lavorando ad una modifica del progetto che prevede l'integrazione dell'Università di Parma. La sinergia tra GGCC e il presente progetto è chiara: sui problemi di scalabilità e precisione l'unità di Parma potrà lavorare nello scenario più realistico possibile.


WP2: ANALISI STATICA MEDIANTE INTERPRETAZIONE ASTRATTA

Task PR-2.1: Definizione di uno schema di analisi modulare e generico

Studieremo i problemi collegati al progetto e all'implementazione di uno schema generico di analizzatori statici per i linguaggi imperativi di largo uso. Lo schema sarà istanziato su analisi dei puntatori e dei valori delle variabili numeriche e booleane (tali variabili possono essere del programma o fittizie per rappresentare, ad esempio, la dimensione dei buffer allocati o la presenza dei terminatori di stringa). Le innovazioni principali che ci interessa introdurre sono la flessibilità e la generalità, sia in termini delle proprietà che in termini del linguaggio analizzato. Da una parte, studieremo tecniche di analisi generale che, seppure indipendenti dalle specifiche proprietà, consentano di sfruttare appieno l'informazione fornita dai domini più sofisticati (ad esempio quelli relazionali). D'altro canto, faremo sì che tutte le caratteristiche "critiche" degli odierni linguaggi imperativi (come le eccezioni, i puntatori e i meccanismi di controllo non strutturati) siano convenientemente approssimate dalla semantica astratta che formalizza il processo di analisi. Crediamo che, a tale scopo, gli approcci basati su regole [CC92b,Sch98] siano particolarmente promettenti.

Task PR-2.2: Annotazione di programmi

C, C++ e Java forniscono solo un supporto rudimentale per la specifica delle conoscenze, intenzioni e attese degli sviluppatori. Le possibilità di specificare queste insieme al codice vero e proprio può essere vantaggiosamente sfruttata per realizzare strumenti di sviluppo migliori. Il nostro interesse a dotare di questa possibilità i linguaggi di programmazione più usati ha anche altre motivazioni: la possibilità di annotare i sorgenti con vari tipi di asserzioni consente di modularizzare il progetto di analizzatori (i quali potrebbero così essere facilmente combinati in cascata) e di acquisire fiducia nella loro implementazione (utilizzando diversi prototipi, l'uno per controllare l'altro). Studieremo la specifica di un linguaggio di asserzioni, nello stile di [HPB00], che dovrebbe consentire al programmatore di codificare nel programma le condizioni logiche che garantiscono che lo stesso sia immune da una certa classe di errori e/o rispetti i limiti imposti dalle politiche di allocazione delle risorse. Il linguaggio di asserzioni sarà estensibile per adattarsi a specifici domini applicativi e non sarà limitato a teorie decidibili (come quelle usate nei sistemi basati sul controllo dei tipi), consentendo così di combinare controlli statici e dinamici delle proprietà. La disponibilità di un linguaggio di asserzioni espressivo sarà sfruttata anche per abilitare la comunicazione dall'analizzatore al programmatore: lo strumento di analisi sarà in grado di annotare automaticamente il programma con una selezione delle proprietà scoperte dall'analisi. L'obiettivo è quello di ottenere un ambiente di sviluppo fortemente integrato, dove il feedback derivante dal confronto delle proprietà attese e quelle calcolate potrà dare vita ad un processo di raffinamento sinergico, con benefici sia per lo sviluppo che per il debugging delle applicazioni. Ad esempio:

1) asserzioni ritenute importanti dai programmatori possono essere marcate in modo che l'analizzatore le usi come "suggerimenti" (abilitando, tra l'altro, quei meccanismi, come il widening-up-to [HPR97], demandati a preservare la precisione dell'analisi in quello specifico contesto);

2) l'analizzatore, ove possibile, può marcare come verificate o refutate quelle asserzioni che ha potuto mostrare vere o false, eventualmente semplificandone altre.

Task PR-2.3: Analisi di correttezza della manipolazione di stringhe

Studieremo un approccio trasformazionale al problema di assicurare la correttezza delle operazioni sulle stringhe nei programmi C (string cleanness). L'approccio consiste nel trasformare un programma, P, che usa stringhe in un'altro, P', dove gli array di caratteri e i puntatori sono sostituiti da strutture ad hoc e dove sono state inserite delle asserzioni. La trasformazione avrà le seguenti proprietà: (1) sarà completamente automatica; (2) se P' non può violare nessuna delle sue asserzioni, allora ogni esecuzione di P sarà esente da errori nella manipolazione delle stringhe. Le stringhe saranno sostituite da strutture che astraggono la loro semantica per mezzo di variabili intere e booleane (per modellare, ad esempio, la dimensione del buffer allocato, la posizione di un puntatore all'interno del buffer, e la presenza dei terminatori). Le asserzioni modellano la correttezza delle operazioni sulle stringhe: ad esempio, prescrivono che la posizione di un puntatore che accede ad un buffer sia non negativa e non superi la dimensione del buffer. Il problema della string cleanness è così trasformato in un problema che richiede ragionamento su interi, booleani e puntatori: le tecniche di interpretazione astratta e analisi statica sviluppate in questo progetto consentiranno, sperabilmente, di avere un numero basso di falsi positivi. L'idea ha origine dai lavori di Dor, Ellenbogen, Rodeh e Sagiv [DRS01, DRS03, Ell04], ma nella loro soluzione ogni stadio del processo di verifica (pre-processing, trasformazione, analisi dei puntatori, analisi degli interi) è fortemente dipendente dagli altri e li vincola in modo severo. Questa è una delle ragioni per le quali iCSSV (interprocedural C String Static Verifier) ha avuto un successo solo parziale [Ell04]. L'approccio che abbiamo in mente è più modulare e ci consentirà di sfruttare gli sviluppi delle tecniche di analisi dei puntatori e degli interi. Inoltre, diversamente dal caso di iCSSV, saremo in grado di usare un'analisi combinata di puntatori e interi, forse riducendo il numero di falsi positivi. Va osservato che, sia nel nostro approccio che in quello di [DRS01, DRS03, Ell04], ogni puntatore e buffer richiede diverse variabili (booleane e intere): certamente ciò porterà ad esacerbare il conflitto tra complessità e precisione, rendendo quindi il lavoro del WP1 ancor più importante.

Task PR-2.4: Analisi di terminazione e complessità

L'analisi di terminazione per codice C è complessa, a causa di diversi fattori, che la differenziano significativamente (ma non completamente) dall'analisi di terminazione per linguaggi logici, per la quale esistono già tecniche piuttosto sofisticate. In particolare:

- C è un linguaggio imperativo nel quale il processo di calcolo evolve per mezzo di assegnamenti distruttivi. E' quindi fondamentale poter prevedere, con una buona approssimazione, l'effetto che un assegnamento distruttivo ad un campo di una struttura dati potrà avere sulle altre strutture dati. A tal fine servono informazioni sui puntatori e dunque questa ricerca ha una naturale relazione con lo sviluppo di un'analisi dei puntatori per il C, altro obiettivo dell'unità di Parma.

- In C i costrutti che possono dare luogo a non terminazione sono i comandi iterativi (while, do-while, for), le chiamate di funzione mutuamente ricorsive, e le istruzioni goto. A quanto sappiamo, nessuno degli approcci esistenti (sia per il linguaggio C che per altri linguaggi) ha mai preso in considerazione tutte queste possibilità contemporaneamente.

Intendiamo strutturare le nostre analisi di terminazione per C nel modo seguente:

1) Ricostruzione dei cicli nel controllo. Vengono identificate le sorgenti di possibile non terminazione: cicli espliciti, chiamate di funzione ricorsive e salti all'indietro.

2) Ricostruzione dei cicli nei dati. Sfruttando i risultati dell'analisi dei puntatori viene analizzata la ciclicità delle strutture dati. Questa informazione serve nel successivo passo 3.

3) Generazione di vincoli: a) sui valori delle variabili numeriche; b) sulla lunghezza massimale di un percorso di puntatori seguito a partire da ciascuna variabile (path-length analysis). Pensiamo di adattare quest'ultima analisi, già formalizzata da Spoto (unità di Verona) per il linguaggio Java [SHP06], al linguaggio C.

4) Sintesi di funzioni di ranking. I vincoli così generati vengono elaborati con tecniche automatiche che cercano di identificare una funzione di misura (norma) che, oltre ad essere limitata inferiormente, ad ogni iterazione di un ciclo (comunque realizzato) decresca di una quantità limitata inferiormente da una costante positiva. Tali proprietà garantiscono che la funzione trovata sia una funzione di terminazione per il programma.