RICERCA ITALIANA     

Programma di ricerca

AIDA - Interpretazione Astratta: Progettazione e Applicazioni

Università di riferimento

Università degli Studi di PARMA - MATEMATICA - PARMA(PR)

Responsabile dell'Unità di ricerca

Roberto BAGNARA

Descrizione

La maggior parte del lavoro dell'unità di ricerca verrà condotta nel contesto del Workpackage 1 (Analisi Statica) del progetto e riguarderà la specifica, progettazione ed implementazione di domini ed operatori astratti, ivi inclusi quegli operatori, come i widening ed i narrowing, che possono essere utilizzati per forzare o accelerare la convergenza del calcolo astratto. In particolare, l'obiettivo principale di questa ricerca è lo studio teorico e l'implementazione effettiva di una libreria di domini astratti numerici funzionalmente completi, robusti e riutilizzabili: intervalli, differenze e divisioni vincolate, ottagoni, poliedri convessi, griglie e Z-poliedri. Alcune operazioni sul dominio dei poliedri convessi sono caratterizzate da una complessità esponenziale nel caso pessimo, sia in tempo che in spazio. D'altra parte, il dominio degli intervalli, pur essendo molto più semplice da un punto di vista computazionale, spesso restituisce approssimazioni troppo grossolane. Una soluzione intermedia è data dai domini delle differenze vincolate e degli ottagoni. Gli utilizzatori industriali di strumenti di analisi statica hanno spesso bisogno della precisione fornita dai domini astratti più accurati; al tempo stesso, però, hanno bisogno di una qualche forma di controllo sul consumo delle risorse tempo e spazio di memoria, in quanto risultati approssimati ottenuti entro un dato intervallo di tempo sono preferibili rispetto a risultati più precisi, ma disponibile solo ad una data non meglio precisata. Perseguiremo pertanto l'obiettivo di una combinazione dinamica del dominio dei poliedri con questi domini di vincoli più semplici al fine di consentire un buon compromesso tra precisione e scalabilità. L'analisi statica o procedura di verifica, per default, dovrebbe considerare i domini più descrittivi (e costosi), come quello dei poliedri convessi, e specificare per ogni operazione una limitazione sulle risorse (tempo di calcolo, occupazione di memoria, valore massimo dei coefficienti numerici). Quando il calcolo di una operazione eccede i limiti fissati, si utilizza un algoritmo più semplice e meno accurato, ma che fornisce un risultato corretto ai fini di un'interpretazione astratta, ovvero tale che il poliedro risultante è un sovrainsieme del risultato esatto. L'algoritmo meno preciso può operare uno o più cambi di rappresentazione, per esempio approssimando un poliedro utilizzando un sistema di differenze vincolate o di intervalli e calcolando l'operazione su questi domini semplificati. Il risultato può quindi essere convertito all'indietro in un poliedro convesso. L'obiettivo finale è la realizzazione di una libreria robusta di operatori sui poliedri in grado di gestire molte centinaia (potenzialmente migliaia) di vincoli su spazi con un numero elevato di dimensioni. È importante notare che tale scenario è proponibile solo se tutti i domini astratti coinvolti sono progettati ed implementati in maniera da poter consistentemente reagire, senza perdita di risorse di sistema, ad eventi quali la scadenza di un timeout o un'eccezione lanciata dalle routine di allocazione della memoria. Il fatto di aver raggiunto questo obiettivo per la ``Parma Polyhedra Library'' [BRZH02], che sarà la componente chiave nella libreria di domini astratti numerici, è quindi un punto essenziale. Altre caratteristiche importanti che devono essere possedute da tutte le componenti della libreria sono: il supporto per tutti gli operatori richiesti da un interprete astratto; l'interoperabilità, ovvero la possibilità di costruire una descrizione di un tipo approssimando una descrizione di un altro tipo; la definizione di operatori di decomposizione dello spazio vettoriale al fine di velocizzare l'esecuzione [HMPV03]; la disponibilità, per ogni operatore, di un database di test di non-regressione.
Intervalli Un buon dominio astratto per gli intervalli è desiderabile non solo come dominio di fall-back, ovvero il dominio più efficiente (anche se non molto preciso) da utilizzare quando tutti gli altri tentativi sono falliti, ma anche come ingrediente chiave per l'implementazione di domini più complessi come le differenze ed le divisioni vincolate [Dav87, Bag97]. Sfortunatamente, nessuna delle librerie di intervalli esistenti è adeguata per costituire la base di un tale dominio astratto. Le librerie disponibili o mancano del supporto per gli intervalli non chiusi (così che non sono in grado di rappresentare vincoli della forma `ax < b'), oppure non forniscono il supporto adeguato per le approssimazioni nel senso della correttezza parziale (ad esempio, la divisione per un intervallo contenente lo zero genera un errore a tempo di esecuzione invece di restituire l'intervallo contenente il risultato sotto l'assunzione che la divisione concreta approssimata non fosse una divisione per zero), oppure ignorano gli errori di arrotondamento e sono pertanto scorrette. Per esempio, la libreria filib++ [LTW<sup>+</sup>01], che è molto sofisticata e ben considerata all'interno del suo campo di applicazione, soffre dei primi due problemi menzionati. Verrà pertanto studiato ed implementato un dominio astratto completo basato sugli intervalli. Tali intervalli saranno parametrici rispetto ad alcune caratteristiche e supporteranno sia estremi chiusi che aperti. Sarà possibile scegliere gli estremi in una serie di domini numerici, inclusi gli interi nativi, gli interi a precisione illimitata, i razionali ed i numeri in virgola mobile nativi. Nel caso dei numeri in virgola mobile saranno resi disponibili vari metodi per controllare il tipo di arrotondamento, con diverse caratteristiche relative alla portabilità ed all'efficienza. Indipendentemente dal tipo degli estremi, saranno supportati sia intervalli di numeri reali che di interi.
Differenze e divisioni vincolate Un dominio di differenze vincolate consente di esprimere la relazione tra due quantità per mezzo di insiemi finiti di vincoli della forma `x-y in S', dove `S' è un sottoinsieme dei reali [Dav87]. La prima proposta di utilizzo per l'analisi statica di questa ed altre descrizioni originate nel campo dell'intelligenza artificiale si è avuta in [BGL92, BGL93] ed è stata ulteriormente elaborata in [Bag97, capitolo 5]. Avendo a disposizione un dominio adeguato per gli intervalli (estesi), l'implementazione delle operazioni di base sulle differenze vincolate è relativamente semplice. Però, come nel caso degli ottagoni (si veda più avanti), per alcune operazioni importanti, come il widening, al momento attuale non sono note realizzazioni efficienti. È quindi richiesto un ulteriore lavoro teorico che consenta di ottenere per questo dominio la completezza funzionale desiderata. Per gli operatori di widening, si prevede di utilizzare le idee presentate in [BHRZ03, BHZ03b]. Fissata una base per i logaritmi, un sistema di divisioni vincolate cattura le relazioni della forma `log |x| - log |y| in S' [Bag97]. Le divisioni vincolate presentano somiglianze con le differenze vincolate e molti aspetti dell'implementazione possono essere riciclati. Rimane però molto lavoro da fare, sia a livello teorico che a livello pratico, per trasformare questa idea in un vero e proprio dominio astratto. Si noti che il dominio delle divisione vincolate coinvolge vincoli non lineari. La necessità, in alcune applicazioni dell'analisi statica, di andare oltre il potere espressivo dei vincoli lineari è stata recentemente sottolineata in [BCC<sup>+</sup>03], dove si mostra come un dominio basato su ellissoidi sia stato cruciale per il successo di una specifica analisi. Riteniamo che il dominio delle divisioni vincolate sarà utile per analisi quali l'identificazione di overflow a tempo di compilazione.
Ottagoni e oltre Il dominio degli ottagoni è noto essere caratterizzato da costi computazionali ragionevoli, sebbene il costo cubico (nel numero delle variabili) sia applicabile solo ad una parte delle operazioni di interesse. I limiti dell'attuale definizione (e quindi dell'implementazione) di questo dominio sono: l'aggiunta di un vincolo lineare può essere effettuata efficientemente solamente nel caso di vincoli di forma speciale; il calcolo delle immagini affini dirette ed inverse è definito solo per una classe limitata di trasformazioni affini; non è disponibile una specifica efficiente per l'operazione di time-elapse [HPR97], utile per l'analisi dei sistemi ibridi lineari; non è disponibile un vero e proprio operatore di widening: solo operatori di estrapolazione che non garantiscono la convergenza dell'analisi. In aggiunta, nessuna implementazione supporta i vincoli stretti, per cui non è possibile definire ottagoni non necessariamente chiusi (NNC). In questo progetto intendiamo superare tutte queste limitazioni. In particolare, saranno ricercati algoritmi efficienti per realizzare le operazioni sopra elencate, utilizzando le tecniche descritte in [BHRZ03, BHZ03b] per fornire il dominio di veri e propri operatori di widening ad elevata precisione. In una prima fase, sarà sperimentata un'implementazione degli ottagoni basata su matrici di differenze vincolate [Min01]. Si passerà quindi all'implementazione proposta in [Bag97], che prevede la rappresentazione degli ottagoni come grafi di vincoli sulle classi di intervalli descritte precedentemente. Questo porterà immediatamente alla definizione di un dominio di ottagoni non necessariamente chiusi e consentirà una generalizzazione verso domini astratti più espressivi degli ottagoni, comunque caratterizzati da una complessità computazionale accettabile.
Poliedri convessi Per quanto riguarda il dominio dei poliedri convessi, ci proponiamo di studiare algoritmi specializzati per classi ristrette di poliedri che sono comunemente utilizzate in molte applicazioni. Un esempio è la classe dei poliedri non negativi (per approssimare i sottoinsiemi dello spazio vettoriale i cui elementi hanno coordinate maggiori od uguali a zero). La ``Parma Polyhedra Library'' sarà anche estesa con un'implementazione efficiente dell'algoritmo del simplesso: questo consentirà, a sua volta, l'aggiunta di alcune nuove funzionalità quali il calcolo efficiente dell'inviluppo di due poliedri come approssimazione del loro inviluppo poliedrale convesso. Considereremo anche il problema della manipolazione di poliedri NNC, ovvero poliedri che possono essere descritti da sistemi di vincoli nei quali possono comparire disuguaglianze strette. Tali disuguaglianze sono importanti, ad esempio, per modellare facilmente il caso di regioni temporali che non si intersecano, come accade spesso nel caso di applicazioni in cui siano presenti concorrenza, protocolli di sincronizzazione, interazioni asincrone e vincoli temporali. Le implementazioni disponibili basate sul metodo della doppia descrizione codificano i poliedri NNC come poliedri chiusi in uno spazio vettoriale di dimensione superiore. Sebbene questa codifica consenta di riutilizzare una parte sostanziale del codice (quasi) invariata, alcuni degli operatori risultanti incorrono in perdite di efficienza o precisione evitabili. Per esempio, una potenziale perdita di precisione si ha quando la convergenza del calcolo di punto fisso viene forzata applicando il widening alla rappresentazione chiusa del poliedro NNC. Tale imprecisione può essere evitata definendo un operatore di widening specifico per i poliedri NNC. Come ulteriore esempio, il calcolo di una rappresentazione in forma minima per un poliedro NNC può comportare perdite di efficienza nel prosieguo della computazione, in quanto le procedure di minimizzazione non sono incrementali: la minimizzazione della rappresentazione a vincoli rende invalida la rappresentazione a generatori (e viceversa). Una possibile soluzione potrebbe essere data dall'adozione sistematica di tecniche di computazione lazy. Un'altra possibilità è la specifica di procedure di minimizzazione completamente incrementali, ovvero che consentano non solo l'aggiunta ma anche la rimozione di vincoli/generatori.
Griglie e Z-poliedri Molte applicazioni dell'analisi statica, come il buffer overflow, l'analisi di terminazione e la parallelizzazione automatica, devono calcolare valori su domini discreti. Candidati per tali applicazioni sono i domini astratti aventi per elementi dei reticoli di vettori a coordinate intere [Anc91, BK97, CL98, DRS01, Gra91, LW97, Pug92]. Per molte applicazioni, però, tali domini sono inadeguati, perché i valori di interesse possono essere non interi oppure le componenti dei reticoli possono essere insiemi di vettori, invece di singoli vettori [Gra97, Mas93]. Ci proponiamo di fornire una definizione generica di dominio di griglie, i cui elementi sono reticoli aventi per componenti altri elementi di domini astratti numerici [Gra97, Mas93]. Tali domini saranno dotati di tutti gli operatori necessari per la loro applicazione all'analisi statica. Un dominio particolarmente importante ed utile che usa questo tipo di griglie è quello degli Z-poliedri, i cui elementi sono definiti dall'intersezione di un poliedro con una griglia discreta (a coordinate intere) [Anc91, NR00, QRR96]. Le operazioni su questo dominio sono spesso inefficienti o non completamente specificate. Molto lavoro di ricerca è quindi richiesto per la rigorosa formalizzazione ed implementazione dei domini a griglia e, basandosi su questi, per il progetto di un vero e proprio dominio di griglie poliedrali. Oltre allo studio, progettazione ed implementazione dei domini astratti, l'unità di ricerca di Parma seguirà da vicino la loro applicazione a problemi di analisi statica, in collaborazione con le altre unità del progetto e con altri gruppi di ricerca (si veda http:/www.cs.unipr.it/ppl/Credits/).
Applicazioni all'analisi di complessità Nel contesto del Workpackage 5 (Vincoli) del progetto ci proponiamo di studiare il problema di fornire un'analisi di complessità completamente automatica, di fronte al quale l'unità di ricerca si trova in una situazione privilegiata. Infatti, al fine di affrontare questo problema, si vorrebbero combinare il lavoro sui domini numerici astratti delineato sopra con il nostro lavoro sulla soluzione automatica di relazioni di ricorrenza (si vedano http://www.cs.unipr.it/purrs/ e [BZZ03, BZ04]). Un modo di esprimere una tale combinazione di informazioni su data-flow e control-flow è per mezzo di un'integrazione ad accoppiamento lasco dei corrispondenti sistemi di vincoli, mantenendo sotto controllo la complessità delle interazioni risultanti. Le relazioni di ricorrenza possono essere viste come vincoli su sequenze di numeri reali che mettono in corrispondenza la dimensione di un problema (una misura di alcuni dei parametri di input) con una limitazione superiore o inferiore della quantità di risorse necessarie per la sua soluzione (ad esempio, il numero di passi della computazione). Oltre ad approfondire lo studio dei metodi automatici per risolvere o approssimare le relazioni di ricorrenza, verrà investigato il problema della loro estrazione dal sistema software analizzato, un'operazione che di solito nasconde ulteriori forme di approssimazione che possono notevolmente influenzare l'accuratezza complessiva dell'analisi. Per fornire una proof-of-concept preliminare, ci concentreremo su di un opportuno frammento di Objective CAML ed estenderemo le tecniche a sottoinsiemi più grandi del linguaggio in fasi successive. Quando saranno considerati gli aspetti object-oriented del linguaggio, un'analisi di complessità accurata dovrà basarsi sulle analisi di classe e di escape, che prevediamo di realizzare per mezzo dell'integrazione di vincoli insiemistici [DPPR00].