Strumenti di Verifica e Validazione di Codice Java

Florian Daniel, Federico M. Facca, Stefano Modafferi and Enrico MussiDipartimento di Elettronica e Informazione

Via Ponzio 34/5, 20133Milano, Italy

[daniel, facca, modafferi, mussi]@elet.polimi.it

ABSTRACTSistemi informatici sempre piu complessi sono ormai costan-temente parte della vita di tutti i giorni di milioni di persone.Le applicazioni software che gestiscono questi sistemi infor-matici diventano man mano sempre piu grosse e di!cili dagestire e per questo l’incidenza del numero di bug al lorointerno e diventata sempre piu alta. La creazione di un soft-ware perfetto, ossia senza bug, e un obiettivo, che teoremie anni di esperienza, hanno dimostrato impossibile. Tut-tavia, con le conoscenze attuali, e possibile fare molto di piudi quanto e stato fatto in passato per ricercare automatica-mente bug all’interno del software. Java negli ultimi anni estato al centro delle attenzioni dei programmatori per varimotivi tra cui spicca la portabilita, questo ha fatto sı chemolti si siano interessati all’opportunita di studiare metodiper la verifica e la validazione di programmi Java. Alcunidei tool piu recenti consento di e"ettuare verifiche senza im-pattare notevolmente sui tempi di sviluppo, permettendonequindi l’impiego per qualsiasi tipo di applicazione. Questoarticolo presenta un insieme di tool che, sfruttando tecnichediverse, si propongono di verificare e validare applicazionisviluppate in Java.

1. INTRODUZIONELa validazione e la verifica delle applicazioni software e unatematica che sta suscitando molti interessi non solo nell’am-bito della ricerca ma anche in ambito industriale. I ciclidi sviluppo e mantenimento di applicazioni software semprepiu complessi, non possono essere, come l’esperienza ha piuvolte dimostrato, immuni ai bug e spesso questi bug possonoavere anche e"etti disastrosi. Per questo motivo in moltiambiti industriali la verifica e la validazione del software ediventato uno degli step fondamentali del ciclo di sviluppodel software, soprattutto nel caso di sistemi critici.Oggi sono disponibili una serie di tool con un grande poten-ziale per aiutare gli sviluppatori nella ricerca degli errori diprogrammazione, alcuni dei quali non sarebbero facilmenteindividuabili altrimenti. Alcuni di questi tool sono anchein grado di rilevare automaticamente sia deadlock che vio-

lazioni delle sezioni critiche, due tra le piu critiche tipologiedi errori che spesso causano gravi problemi ai software inesecuzione.

I tool che si occupano di analisi del software alla ricercadi bug possono essere distinti in due categorie principali aseconda di come avviene la verifica.

• Analisi dinamica: esegue il codice dell’applicazionee durante l’esecuzione e"ettua una serie di analisi perverificare la correttezza dell’output prodotto. E unmetodo rapido, ma fortemente legato alla capacita delletest suite usate di coprire tutti gli aspetti critici delcodice analizzato.

• Analisi statica: verifica il software senza eseguirlo.Fa uso di diverse tecniche tra cui i bug pattern e imodelli per la rappresentazione del codice e delle sueproprieta. L’analisi statica puo essere piu o meno dis-pendiosa in termini di tempo e di costo computazionalea seconda delle tecniche usate.

In base al tool utilizzato e al tipo di bug ricercati, il risultatopuo essere piu o meno preciso. Comunque nessun tool e ingrado di dare la certezza dell’assenza di bug nel codice. Laricerca di errori di programmazione so"re essenzialmente didue problematiche:

• falsi positivi: alcuni dei problemi individuati in re-alta non lo sono. Questo tipo di problema non e critico,ma, se in quantita eccessiva, porta all’inutilizzabilitadel tool perche richiede un ulteriore tempo di analisidell’output per distinguere i bug reali dai falsi allarmi.

• falsi negativi: non tutti i bug presenti nel codicevengono individuati. Questo tipo di problema e criti-co perche non rileva potenziali problemi. Per ridurrele occorrenze di questo tipo di inconveniente piuttostoche e"ettuare analisi general purpose e possibile ef-fettuare delle analisi di codice mirate alla verifica dispecifiche proprieta e quindi piu precise.

In questo articolo noi ci concentriamo su alcuni tool che sioccupano della validazione e della verifica di applicazioniJava [16]. I tool presi in considerazione dalla nostra analisie"ettuano tutti un’analisi di tipo statico: FindBugs, PMD,

Esc/Java2, Java Pathfinder e Bandera. In Figura 1 ven-gono riassunti alcuni dettagli sui tool, quali le interfacce edi metodi di verifica utilizzati.

Nome Input Interf. TecnologiaFindBugs Bytecode CL,Gui Syntax,

DataflowPMD Source CL,Gui SyntaxEsc/Java2 Source +

AnnotationCL,Gui Theorem

ProvingPathfinder Source CL Model CeckingBandera Source CL,Gui Model Cecking

Figure 1: Riepilogo dei Tool

L’articolo e organizzato come segue: le Sezioni 2 e 3 mostra-no i tool FindBugs e PMD; in Sezione 4 viene presentato iltool Esc/Java2; la Sezione 5, dopo un’introduzione alle tec-niche di Model Checking, presenta il tool Java PathFinder;nella Sezione 6 viene introdotto il tool Bandera; e infine,la Sezione 7 presenta un confronto fra i tool e riporta leconclusioni a cui siamo giunti analizzando i tool.

2. FINDBUGSFindBugs [19] e un prodotto open source originalmente svilup-pato da Bill Poth e correntemente mantenuto da Bill Pughe David Hovemeyer. Codice sorgente Java e la documen-tazione possono essere scaricati gratuitamente dal sito http://find-bugs.sourceforge.net.

All’interno della famiglia degli strumenti di analisi di codiceJava FindBugs e probabilmente uno dei tool piu intuitivi,perche si avvicina molto al nostro modo di interpretare eleggere codice sorgente. Questo perche, fra le varie tec-niche di analisi statica esistenti, FindBugs adotta un ap-proccio basato sulla scoperta di cosiddetti bug pattern al-l’interno del codice da analizzare [15]. Tali pattern sonoframmenti o strutture di codice sorgente o combinazioni diistruzioni che molto probabilmente rappresentano errori diprogrammazione, e la loro natura prettamente sintattica fa-cilita la comprensione dei rispettivi warnings da parte deiprogrammatori.

Prima di entrare meglio nei dettagli dell’analisi basata subug pattern, pero, e importante notare che FindBugs is-peziona possibili errori di programmazione e non rappresen-ta un tool di verifica dello stile di programmazione. Verifi-catori di stile esaminano il codice per determinare se questorispetta o meno determinate regole stilistiche, come quelleadottate all’interno di un progetto software che coinvolga piuprogrammatori diversi. Tali regole, infatti, servono soprat-tutto per mantenere uno stile di codifica coerente in tuttoil progetto, cosa che, di conseguenza, aumenta la leggibilitae la manutenibilita del codice. In generale pero, non man-tenere uno stile accordato, non deve per forza risultare inun errore.

2.1 Pattern e Detector built-inPer il riconoscimenti dei bug pattern sintattici, FindBugsfornisce un’architettura modulare che permette di aggiun-gere opportuni detector, uno per ciascun pattern da riconoscere.Tramite questi detector si specificano le proprieta e la strut-

tura dei pattern in una maniera esplicita e dichiarativa di-rettamente in codice Java. FindBugs non analizza diretta-mente il codice sorgente Java, ma la sua versione compilatafile .class). Si tratta pertanto di uno strumento di anal-isi di bytecode, cioe del “linguaggio macchina” della JavaVirtual Machine. Per questo motivo, i detector adottatida FindBugs, internamente, sfruttano la libreria BCEL [2],una libreria open source di analisi di bytecode Java. Piuprecisamente, FindBugs propone una struttura di detectorbasata sul cosiddetto Visitor design pattern di BCEL: ognidetector visita singolarmente ciascuna classe della libreria oapplicazione da analizzare ed esegue la sua analisi in manieraatomica ed indipendente da eventuali altri detector operantisullo stesso codice.

FindBugs e corredato da un numero elevato di rilevatoridi bug pattern ricorrenti (la versione 0.9.1 ne fornisce cir-ca 130), altri possono essere progettati su misura e aggiun-ti a piacere alla configurazione standard del tool. Usandotecniche di analisi statica relativamente semplici, possonoessere implementati tanti diversi rivelatori automatici, unoper ciascun pattern nuovo da riconoscere.

Indipendentemente dal fatto che un particolare detector siastato progettato per soddisfare problemi di programmazionesu misura o che faccia parte dei detector generali forniti in-sieme ad una versione particolare di FindBugs, questi pos-sono essere raggruppati in quattro classi di riconoscitori fun-zionalmente diversi. In particolare, le diverse strategie diimplementazione dei detector pongono i seguenti approccianalitici nel centro della loro attenzione:

• Struttura della classe e gerarchia di ereditarieta. Questidetector guardano solamente alla struttura delle classianalizzate e controllano se le gerarchie di ereditarietae le implementazioni di interfacce siano coerenti, sen-za tenere conto di eventuale codice sorgente all’internodelle classi.

• Scansione lineare del codice. Questi detector analiz-zano piu in dettaglio ogni singola classe ed “entrano”nei rispettivi metodi. Si basano su una lettura lin-eare del bytecode dei metodi da analizzare, in basealla quale aggiornano (se necessario) una macchina astati finiti interna, ogni qualvolta un detector richie-da il mantenimento di un certo stato durante l’analisi.Questi detector non usano eventuali informazioni di-sponibili sul flusso di controllo vero dell’esecuzione epiuttosto si basano su euristiche che ne permettonoun’approssimazione e!cace.

• flusso di controllo. I detector di questa categoria sibasano su un grafo accurato del flusso di controllo perciascun metodo da analizzare. Non usando piu ap-prossimazioni del flusso di esecuzione, l’applicazionedi questi detector risulta piu onerosa in termini divelocita.

• Flusso di dati. I detector piu complicati si basanosu un’analisi approfondita del flusso di dati, oltre chesull’analisi del flusso di controllo.

Queste tecniche di analisi statica permettono di coprire ungran numero di pattern di errori e determinano, insieme alla

scelta di limitare l’analisi al bytecode, il potere riconosciti-vo dei detector. Conseguentemente, FindBugs si presta so-prattutto per la scoperta delle seguenti classi di problemi oerrori:

• Problemi di correttezza per thread singoli.

• Problemi di correttezza nella sincronizzazione di piuthread cooperanti.

• Questioni di performance.

• Problemi di sicurezza o vulnerabilita del codice.

Generalmente, piu e complesso il pattern da riconoscere, piue complesso il suo detector. I detector basati sull’analisi delflusso di dati sono i piu complessi, mentre quelli per l’analisistrutturale delle classi sono i piu semplici. Comunque, i de-tector piu complessi solo in pochi casi superano le 1000 righedi codice Java, e quasi la meta dei detector totali occupameno di 100 righe.

Date queste premesse e per una migliore comprensione, diseguito discuteremo qualche detector tipico, gia presente inFindBugs; per motivi di spazio non approfondiremo tutti ipattern definiti.

Dropped Exception.Iniziamo con un pattern molto ricorrente e di facile compren-sione. Il detector Dropped Exception si concentra sulla ges-tione delle eccezioni in Java, e quindi sui blocchi try-catch.In particolare, questo detector individua tutti quei costrut-ti try-catch con blocco catch vuoto, cioe tutti quelli chescartano eventuali eccezioni.

Spesso durante la stesura del codice un programmatore econvito che certe eccezioni non possano mai accadere e quin-di ignora la gestione corretta delle relative eccezioni. Ma,soprattutto in base a modifiche successive al codice che al-terano anche le premesse stesse alla base di quel partico-lare frammento di codice, le eccezioni potrebbero sı esserelanciate. Questo molto probabilmente avrebbe come con-seguenze comportamenti di runtime anomali da parte del-l’applicazione. Trovare problemi connessi ad eccezioni nonpropriamente gestite risulta essere molto oneroso in praticae spesso richiede molto tempo.

Null Pointer Dereference, Redundant Comparisonto Null.Chiamare un metodo o accedere a variabili di istanza tramiteriferimenti al puntatore nullo (null) porta inevitabilmentead una NullPointerException durante l’esecuzione dell’ap-plicazione. Solitamente un programmatore e molto attento aquesto tipo di errore, perche la NullPointerException spes-so – se non gestita in maniera opportuna – causa il crash del-l’intero programma, ma quando il riferimento del puntatoree determinato per esempio dall’esecuzione precedente di unqualche metodo, il puntatore puo anche risultare nullo. Perquesto, il detector Null Pointer Dereference individua quelleistruzioni che de-referenziano un puntatore potenzialmentenullo.

Alla base dell’implementazione di questo detector c’e un’anal-isi del flusso di dati, ristretto all’interno del metodo sotto

analisi. Il pattern adottato non determina direttamente separametri passati a o ritornati da un metodo siano nulli, masfrutta eventuali condizioni if presenti in righe precedenti alpotenziale eccezione. Nel seguente frammento, per esempio,il puntatore foo e sicuramente nullo all’interno del bloccodella condizione:

if (foo == null) {... //foo e null in tutto il corpo della if

}

Analogamente, il frammento seguente mostra un esempio dide-referenziazione di un puntatore nullo tratto dal codicesorgente di Eclipse e scoperto con FindBugs [15]:

Control c = getControl();if (c == null && c.isDisposed()) {return;

Oltre a dereferenziazioni di null, il pattern di questo de-tector permette anche di individuare confronti il cui risul-tato e prefissato, perche entrambi i valori sono sicuramentenulli o uno e sicuramente nullo e l’altro sicuramente nonlo e (Redundant Comparison to Null). Data la natura delproblema, questo non deve risultare per forza in un errore aruntime, ma spesso indica una certa incertezza da parte delprogrammatore e puo addirittura rivelare errori completa-mente diversi in maniera indiretta. Il seguente frammento,preso dalla classe java.awt.MenuBar (Sun JDK 1.5, build59 ), ne riporta un esempio tipico:

if (m.parent != this) { //m non nullo!add(m);

}helpMenu = m;if (m != null){ //confronto fra m e null...

Unconditional Wait.Sincronizzare thread tramite le due istruzioni wait() e noti-fy() nei programmi multi-threaded rappresenta una sor-gente di errori frequenti. Questa tesi e nettamente confer-mata anche dalle esperienze raccolte con FindBugs da Hov-emeyer e Pugh [15] e gli innumerevoli errori di sincroniz-zazione riscontrati.

Il detector Unconditional Wait, per esempio, indirizza un ri-corrente problema collegato alla wait(). Cerca quelle partidi codice dove la wait() e eseguita in maniera incondizion-ata all’ingresso in un blocco synchronized (un monitor).Tipicamente questa configurazione indica che la condizioneassociata alla wait() che valuta se sospendere o meno ilthread in oggetto viene valutata senza detenere il lock sulmonitor. Conseguentemente, eventuali messaggi di notificada parte di altri thread potrebbero andare persi. Questo tipodi errore e particolarmente di!cile da riprodurre, percheintrinsecamente dipende anche dal tempo e dall’ordine diesecuzione dei singoli thread.

Il detector per questo pattern esegue una scansione linearedel bytecode del metodo e individua quelle chiamate a wait(),

immediatamente preceduti da un’istruzione monitorenter enon da una condizione. Il codice seguente (JBoss 4.0.ORC1 )ne dimostra un esempio reale:

if (!enabled) {try {synchronized (lock) {lock.wait();...

Questi tre esempi rappresentano solo una piccola frazionedei detector complessivi disponibili in FindBugs, ma per ilmomento ci interessa capire l’approccio di fondo. In questosenso e importante notare, che il metodo basato su bug pat-tern risulta essere abbastanza accurato in generale, ma indeterminate situazioni produce comunque cosiddetti falsepositives, cioe messaggi di warning sbagliati, e false neg-atives (fallimenti nel riconoscere errori esistenti). Inolte,una parte importante dei messaggi prodotti da FindBugssi riferisce piu a “violazioni” di regole di buona program-mazione e meno ad errori veri e propri. Comunque, secondogli autori di FindBugs [15] la percentuale di errori e"ettivisul totale dei messaggi prodotti durante l’analisi si aggiraintorno al 50%, che e una percentuale buona nel contestodell’analisi statica di codice Java [20].

2.2 Il tool in praticaFingBugs si presenta con vari front end: una semplice ap-plicazione batch (eseguita dalla riga dei comandi) che gen-era rapporti testuali in maniera online per ciascun patternriscontrato; un’applicazione batch che genera rapporti informato XML per una facile integrazione con altri tool disviluppo; e un tool interattivo con interfaccia grafica, chepermette di scorrere la lista di warnings generati durantela fase di analisi, di confrontare tali messaggi con il codicesorgente Java e di apportare eventuali annotazioni person-ali. Inoltre e stato sviluppato anche un plugin di FindBugsper l’ambiente di sviluppo Java Eclipse. Figura 2 mostrauno screenshot dell’interfaccia grafica di FindBugs al lavoro.La lista nella parte superiore della finestra rappresenta iproblemi riscontrati, mentre nella parte inferiore e possibilevisualizzare una descrizione testuale del pattern.

2.3 Definizione di detector personalizzatiIn questa sezione mostriamo con un piccolo esempio comeFindBugs puo essere esteso con detector personalizzati persoddisfare esigenze particolari, non previste dai detector didefault. In particolare, in questa sezione definiremo un de-tector per il seguente pattern di codice Java:

if (Logger.isLogging()) {new Logger().log("bob");

...

Si tratta di assicurare che tutte le chiamate al metodo log()della classe Logger siano precedute da una clausola if checontrolla se il componente di logging e"ettivamente e attivoo meno. Infatti, un programmatore potrebbe essere tenta-to di eseguire operazioni di logging senza prima controllareil corretto funzionamento del rispettivo componente. Per

Figure 2: Interfaccia grafica di FindBugs.

evitare eventuali problemi del genere, di seguito definiamoun opportuno detector.

Come gia accennato in precedenza, i detector di bug pat-tern di FindBugs si basano sulla Byte Code Engineering Li-brary (BCEL) per la lettura di bytecode Java. Tutti i detec-tor implementano il cosiddetto Visitor pattern, per il qualeFindBugs fornisce interfacce predefinite, che possono esserefacilmente estese per fronteggiare nuovi pattern. L’approc-cio generale a tale scopo puo essere riassunto come segue:Prima si scrive il frammento di codice Java che rappresenta ilpattern da controllare e lo si compila per ottenere la versionebytecode del pattern. Applicando il comando javap -c (oqualsiasi altro disassemblatore di bytecode) si ottiene unaversione “leggibile” del bytecode1. Questa rappresentazionepermette di derivare la struttura generale del detector pere"ettuare l’analisi sintattica del bytecode Java.

Applicando per esempio javap -c al pattern precedente, siottiene il bytecode disassemblato mostrato in figura 3 (permotivi di presentazione, la formattazione e stata modifi-cata leggermente). Questa rappresentazione e la base percomprendere a fondo il flusso di controllo e le “istruzionimacchina” a livello di bytecode che caratterizzano il parti-colare pattern sotto esame. La conoscenza delle istruzionibytecode del pattern permette di formulare le condizioni perl’analisi sintattica, come riportate dalla figura 4. In partico-lare, la figura mostra solo il metodo principale del detector, ilmetodo sawOpcode(), che viene chiamato iterativamente perciascuna istruzione bytecode del programma sotto analisi. Aquesto punto non descriviamo tutti i dettagli implementatividell’esempio; basta concentrarsi sulle condizioni della figura4 per vedere come queste si riferiscano alle singole istruzioni

1Il comando javap disassembla file .class di Java; fa partedi tutte le versioni JDK.

public void methodWithLogging_guarded(); Bytecode: 0: invokestatic #28; //Method cbg/app/Logger.isLogging:()Z 3: ifeq 18 6: new #16; //class Logger 9: dup 10: invokespecial #17; //Method cbg/app/Logger."<init>":()V 13: ldc #19; //String bob 15: invokevirtual #23; //Method cbg/app/Logger.log:(Ljava/lang/Object;)V 18: aload_0 19: invokespecial #31; //Method doWork:()V 22: return

Figure 3: Bytecode della Java Virtual Machine come prodotto da javap disassemblando file .class.

public void sawOpcode(int seen) { if ("cbg/app/Logger".equals(classConstant) && seen == INVOKESTATIC && "isLogging".equals(nameConstant) && "()Z".equals(sigConstant)) { seenGuardClauseAt = PC; } if (seen == IFEQ && (PC >= seenGuardClauseAt + 3 && PC < seenGuardClauseAt + 7)) { logBlockStart = branchFallThrough; logBlockEnd = branchTarget; } if (seen == INVOKEVIRTUAL && "log".equals(nameConstant)) { if (PC < logBlockStart || PC >= logBlockEnd) { bugReporter.reportBug(new BugInstance( "CBG_UNPROTECTED_LOGGING",HIGH_PRIORITY).addClassAndMethod(this).addSourceLine(this)); } }}

Figure 4: Codice Java del detector per il controllo sull’uso corretto del logging.

bytecode di figura 3, per comprendere il funzionamento deidetector di bug pattern in FindBugs.

3. PMDPMD2 [22], come FindBugs o simili strumenti di analisi stat-ica di codice Java, e"ettua un’analisi sintattica del program-ma o della libreria. Contrariamente a FindBugs, PMD anal-izza direttamente il codice sorgente in oggetto e non e"ettuaalcun tipo di controllo a livello di bytecode. Inoltre, PMDnon e dotato di meccanismi per l’analisi del flusso di con-trollo o del flusso di dati. Conseguentemente, molti degli“errori” che si trovano con PMD si riferiscono soprattutto aconvenzioni stilistiche. In generale queste rappresentano piusospetti sulla forma del codice e meno sulla sua correttezza.Infatti, in letteratura PMD e trattato piu come verificatoredi stile che come verificatore di codice sorgente [20].

Nel confronto diretto fra PMD e FindBugs, il primo nellamaggior parte dei casi rileva piu problemi del secondo (usan-do i tool nelle loro configurazioni base) [15], ma questo nonvuol dire che l’uno sia “migliore” dell’altro. Infatti, bastapensare che PMD lavora direttamente sul codice sorgente,

2L’acronimo PMD non sembra avere una forma estesa; citi-amo letteralmente gli autori: “We’ve been trying to find themeaning of the letters PMD - because frankly, we don’t re-ally know. We just think the letters sound good together.”[22]

mentre FindBugs analizza bytecode. E proprio per questomotivo che il primo strumento si presta meglio per verificareproprieta stilistiche del codice, e il secondo si rivela piu adat-to per l’analisi di potenziali errori, trascurando la forma delcodice vero e proprio (infatti, a livello di bytecode la “forma”non c’e piu). Nonostante questa diversita nell’approccio, co-munque si registra un certo livello di sovrapposizione fra imessaggio di warning prodotti da PMD e FindBugs. Infatti,basta pensare al detector Dropped Exception di FindBugs,descritto nella sezione 2.1, che tratta piu un problema stilis-tico e meno la scoperta di un errore vero e proprio. Con-seguentemente, sia PMD che FindBugs producono messaggirelativi alla gestione scorretta delle eccezioni.

In base alle considerazioni precedenti, si puo quindi a"er-mare che i due strumenti si concentrano su due aspetti di-versi della qualita del software e si completano a vicenda,pur con qualche sovrapposizione.

4. ESC/JAVA2ESC/Java2 [10] e un tool per il controllo statico esteso (Ex-tended Static Checking) del codice, ossia si prefigge di ver-ificare il codice a compile-time individuando possibili er-rori che vanno al di la dei semplici errori solitamente ripor-tati dalla verifica statica eseguita dai compilatori (i.e., typechecking). La verifica statica avviene a partire dalle anno-tazioni JML inserite all’interno del codice sorgente usando

il theorem proving. Il tool e anche in grado di individuarealcuni possibili errori anche senza l’ausilio di annotazione(i.e. index out of bounds).

ESC/Java e nato nei laboratori Compaq Research come svilup-po del tool ESC/Modula-3 [17]. Dopo la fusione di Compaqcon HP il progetto era stato abbandonato in seguito allachiusura dei laboratori Compaq Research. Questo ha fattosı che ESC/Java rimanesse indietro rispetto alle evoluzionidi Java e di JML. Recentemente Cok e Kiniry, ottenuto ilcodice sorgente di ESC/Java, hanno dato vita al progettoESC/Java2 [5] con lo scopo di: (i) rendere il tool com-pletamente compatibile con la versione 1.4 di Java;3 (ii)aggiornare le annotazione accettate dal tool in modo chesiano consistenti con la versione attuale di JML; (iii) au-mentare la sintassi JML riconosciuta dal tool in modo da,potenzialmente, coprirla interamente.

ESC/Java2, in linea con uno degli utilizzi per cui e sta-to pensato JML, si propone come un tool per supportarela tecnica design-by-contract, che enfatizza l’importanza dispecificare in modo esplicito i vincoli che devono sussistereprima e dopo l’esecuzione di un componente software.

Il progetto non ha ancora prodotto una versione definiti-va del nuovo tool, tuttavia la release attuale – alpha-9 –e quelle immediatamente precedenti hanno raggiunto unastabilita su!ciente da permettere l’applicazione del tool aproblemi reali. ESC/Java2 funziona sia da riga di comandoche tramite interfaccia grafica. Allo stato attuale, l’interfac-cia grafica e ancora molto limitata.Il tool puo essere scaricato gratuitamente dalla pagina web:http://secure.ucd.ie/products/opensource/ESCJava2/.

Il progetto ESC/Java2 prevede tra i vari obiettivi, quel-lo di aggiornare e rendere compatibili con la versione at-tuale tutta una serie di tool che erano stati sviluppati perESC/Java: Calvin un tool per la verifica di invarianti al-l’interno di programmi Java multithreaded; Race ConditionChecker per Java (RCC/Java) un tool che identifica statica-mente le potenziali condizioni di concorrenza all’interno dicodice Java multithreaded; e infine Houdini un tool in gra-do di inferire automaticamente alcune annotazioni JML dalcodice Java per assistere i programmatori nell’inserimentodell’annotazioni da testare con ESC/Java.

Accanto a questi, recentemente sono stati sviluppati alcuniprogetti che estendono ESC/Java2. CnC [7] e un tool cheusa i controesempi generati da ESC/Java2 e li compila intest case per la verifica dinamica con JUnit. Inoltre esisteun plugin per Eclipse che permette un integrazione parzialedi ESC/Java2 con l’ambiente di sviluppo di Eclipse [4].

4.1 Architettura e funzionamento del toolIl funzionamento di ESC/Java2, come accennato in prece-denza, si basa sulla tecnica di theorem proving. Ossia sicerca di dimostrare la correttezza del codice trasformandoloin un modello logico basato su predicati e verificando la lorovalidita. Di seguito sono descritti i passi fondamentali delfunzionamento di ESC/Java2.

3Gli autori non hanno ancora investigato le problematichelegate a rendere compatibile ESC/Java2 con Java 1.5.

int Absolute(int x){if(x>=0) return x;else return -x;

}

VAR int x@pre IN{

ASSUME integralGE(x, 0);RES = x;

[]ASSUME boolNot(integralGE(x, 0));RES = integralNeg(x);

};END;

...(OR

(AND (>= |x| 0) (EQ |@true| |@true|)(AND(NOT (>= |x| 0)(EQ |@true| |@true|)

)(EQ |:RES| (- 0 |x|))

...)...

Figure 5: Un semplice frammento di codice Java peril calcolo del valore assoluto di un numero, lo stessoprogramma trasformato in Guarded Command, e in-fine la sua trasformazione nelle condizioni di verificapassate al theorem prover.

1. A partire dal codice sorgente Java e dalle specificheJML incluse nel codice, viene generato un set di pred-icati da verificare.

2. I predicati, insieme ad un modello logico del funziona-mento di Java, vengono elaborati da un theorem prover,il quale verifica che le condizioni sussistano o in ca-so contrario genera un controesempio che indica unpotenziale bug.

3. I controesempi vengono elaborati e trasformati in avvisidi possibili errori con riferimento ai punti del codiceinteressati dal problema.

Il primo passo del processo di verifica, prevede piu passag-gi di semplificazione per arrivare alla generazione finale deipredicati da passare al theorem prover. Inizialmente il codiceJava/JML viene trasformato in una forma semplificata dellinguaggio Guarded Command di Dijkstra, che viene ulte-riormente ridotta passando alla versione core di GuardedCommand, in fine da questa forma viene generato l’insiemedi condizioni da passare al theorem prover. ESC/Java, comemostrato in figura 5, permette di ottenere, tramite linea dicomando, sia la trasformazione in Guarded Command (escj-pgc codice.java), che in condizioni di verifica (escj -v-ppvc codice.java).

Il theorem prover usato, Simplify, accetta come input unasequenza di formule del primo ordine e cerca di provare lavalidita di ognuna di esse. Simplify non implementa un pro-cedura di decisione per i suoi input: a volte non e in grado didimostrare che una formula valida sia e"ettivamente valida.Tuttavia e conservativo, ossia non dice mai che una formu-la non valida sia valida. Simplify per provare una formulaF , procede per assurdo, ossia cerca di dimostrare che ¬Fnon e valida. Se ¬F e valida, allora Simplify assume che Fnon lo sia e produce un controesempio, ossia un insieme diformule atomiche che ritiene rendano invalida la formula F .Purtroppo non sempre il controesempio prodotto e correttoed e, data la sua verbosita, di di!cile comprensione e quindidi scarsa utilita per individuare facilmente una soluzione alproblema riscontrato.

Questo dimostratore, gia usato per nei tool ESC/Modula-3 e ESC/Java, pur essendosi dimostrato un dimostratoredi logica del primo ordine su!cientemente robusto e puressendo disponibile per diverse piattaforme, so"re di parec-chie limitazioni dovute al fatto che e basato su un vecchiemetodologie per i dimostratori e che il suo codice non e piumantenuto da anni. Tra le limitazioni piu evidenti di Sim-plify ci sono: la sua incapacita di gestire operazioni, se nonle piu semplici, che non usino numeri interi e alcuni limitinell’uso dei quantificatori.4

L’architettura e i principi di funzionamento di ESC/Java, gliconsentono di agire modularmente su ogni metodo presentenel codice anziche sull’intero programma. Ovviamente pertrarre i maggiori vantaggi da cio e necessario che venganospecificate le precondizioni e le postcondizioni JML per imetodi chiamati da altri metodi.

La logica di verifica con cui sia ESC/Java che ESC/Java2sono stati implementati non identifica ne tutti i potenziali er-rori (e.g. perche non tutti gli aspetti di Java sono modellatidalla logica usata) ne evita tutti possibili falsi allarmi (e.g.a causa delle limitazioni del dimostratore di teoremi usato).Queste limitazioni sono giudicate nello stato dell’arte dellaverifica statica di codice, un buon ed e!cace compromessoper mantenere comunque i tool e!cienti ed usabili. Un mod-ello logico completo che rappresenti fedelmente la logica dicomportamento di Java – senza considerare alcuni problemidi indecidibilita nel suo comportamento – richiederebbe unsforzo computazionale al theorem prover tale da rendere iltool molto piu lento e quindi meno usabile dello stato attualesenza per altro aumentarne significativamente l’e!cacia.

Le considerazioni espresse prima si possono riassumere di-cendo che ESC/Java2 e unsound e incomplete: il tool potrebbenon rilevare un errore e"ettivamente presente (unsoundness)e inoltre potrebbero generare avvisi di errori che in realtanon sono presenti (incompleteness).

Una delle cause di unsoundness di ESC/Java 2 e la modalitacon cui vengono gestiti i cicli. Il comportamento predefinitodi ESC/Java per gestire i cicli semplicemente “srotola” ilciclo una sola volta. Questo semplifica il compito del pro-grammatore a cui non e richiesto di specificare alcuna in-

4Uno degli sviluppi futuri del progetto e quello di trovareun dimostratore alternativo a Simplify di concezione piumoderna e il cui codice sia ancora supportato.

while(e) c;

if(e){ c; while (e) c; }

if(e){ c; if (e) {assume false;} }

Figure 6: Un frammento semplificato di codice Ja-va contenente un ciclo while, la sua trasformazionemediante faithful unrolling e, infine, nell’e!ettivounrolling usato da ESC/Java2.

variante, ma sicuramente fa sı che molti errori possano nonessere trovati. In alternativa e possibile specificare il nu-mero di volte che si vuole “srotolare” il ciclo, questo per-mette di aumentare il numero di possibili errori trovati, macomunque non e in grado di garantire che tutti i possibilibug possano essere trovati. In figura 6 e mostrato comeESC/Java2 gestisce l’unrolling dei cicli, ossia in modo nonfaithful (fedele): il ciclo piu interno che si ottiene con il faith-ful unrolling viene sostituito con un assunzione di falsita. Equindi su quel ramo del ciclo non avviene piu alcuna verifica.

Inoltre, come altri tool5 ESC/Java permette, tramite la no-tazione JML, di specificare le invarianti di ciclo e di verifi-care automaticamente che le invarianti sussistano per tuttele possibili iterazioni del ciclo e quindi di gestire i cicli inmaniera sound, srotolando i cicli un numero di volte pari aquello massimo possibile secondo le invarianti fornite. Questooltre a richiede l’interazione del programmatore, causa ancheun costo computazionale maggiore per la verifica da partedel theorem prover.

4.2 Il tool in praticaESC/Java2 e in grado di rilevare diverse tipologie di errori:possibili eccezioni a runtime, possibili violazioni nelle speci-fiche JML delle funzioni, violazioni delle condizioni “nonnull”, errori nei cicli e nei flussi, possibili violazioni nellespecifiche delle classi, problemi legati alle eccezioni e qualcheproblema legato al multithreading.

Eccezioni a runtime (Cast, Null, NegSize, IndexTooBig,IndexNegative, ZeroDiv, ArrayStore).Il messaggio Cast viene generato quando ESC/Java2 nonpuo provare che una ClassCastException non verra gener-ata. Ad esempio, il seguente codice:

1 public class CastWarning {2 public void m(Object o) {3 String s = (String)o;4 }5 }

genera il seguente warning:

CastWarning.java:3: Warning: Possible type

5LOOP e JACK sono due tool semiautomatici per la verificastatica che, nel caso dei cicli, richiedono sempre all’utentedi specificare le invarianti.

cast error (Cast)String s = (String)o;

^

Mentre il seguente codice non produce alcun warning:

1 public class CastWarningOK {2 public void m(Object o) {3 if (o instanceof String) {4 String s = (String)o;5 }6 }7 }

Allo stesso modo, quando il tool non puo provare che nonverra lanciata una NullPointerException genera un Nullwarning:

1 public class NullWarning {2 public void m(Object o) {3 int i = o.hashCode();4 }5 }

genera il seguenta warning:

NullWarning.java:3: Warning: Possible nulldereference (Null)

int i = o.hashCode();^

Mentre il seguente non produce alcun segnale:

1 public class NullWarningOK {2 public void m(/*@ non_null */ Object o) {3 int i = o.hashCode();4 }5 }

Negli altri casi: ZeroDiv viene sollevato quando un denom-inatore di una divisione puo essere 0, NegSize quando ladimensione di un array durante la sua allocazione potrebbeessere negativa, IndexNegative quando l’indice di un arraypotrebbe essere negativo IndexTooBig quando l’indice di unarray potrebbe piu grande della dimensione e"ettiva dell’ar-ray.

Specifiche JML delle funzioni (Precondition, Postcon-dition, Modifies).Questi warning vengono generati in risposta alle precon-dizioni (requires) e alle postcondizioni (ensures, signals)annotate dagli utenti. Ad esempio il seguente codice:

1 public class PrePost {2 //@ requires i >= 0;3 //@ ensures \result == i;4 public int m(int i);

5 //@ ensures \result > 0;6 public int mm() {7 int j = m(-1);8 }9 //@ ensures \result > 0;

10 public int mmm() {11 int j = m(0);12 return j;13 }14 }

genera i seguenti messaggi:

PrePost.java:7: Warning: Precondition possiblynot established (Pre)

int j = m(-1);^

Associated declaration is "PrePost.java",line 2, col 4:

//@ requires i >= 0;^

PrePost.java:8: Warning: Postcondition possiblynot established (Post)

}^Associated declaration is "PrePost.java",

line 5, col 4://@ ensures \result > 0;

^PrePost.java:13: Warning: Postcondition possibly

not established (Post)}^

Associated declaration is "PrePost.java",line 9, col 4:

//@ ensures \result > 0;

Il primo warning indica come secondo le specifiche JML,l’argomento passato alla funzione m() debba essere maggioreo uguale a 0 mentre in questo caso e negativo. A causa diquesto errore anche le post condizioni della funzione mm()non sono rispettate. Lo stesso di scorso vale per la funzionemmm() dove la postcondizione //@ ensures \result > 0; eviolata dato che il valore ritornato dalla funzione e 0.

Il warning Modifies indica un tentativo di assegnare un val-ore a un campo di un oggetto che viola la clausola modifies.

Condizioni JML “non null” (NonNull, NonNullInit).I campi delle classi dichiarati non null devono essere inizial-izzati a valori non nulli in ogni costrutturo altrimenti vieneprodotto un messaggo NonNullInit.

1 public class NonNullInit {2 /*@ non_null */ Object o;3 public NonNullInit() { }4 }

genera i seguenti messaggi:

NonNullInit.java:4: Warning: Field declarednon_null possibly not initialized (NonNullInit)

public NonNullInit() { }^Associated declaration is "NonNullInit.java",

line 2, col 6:/*@ non_null */ Object o;^

Un messaggio NonNull viene generato dal tool ogni voltache viene vatto un assegnamento a un campo o una variabiledichiarata non null ma ESC/Java2 non puo determinare seil valore assegnato e nullo o meno.

1 public class NonNull {2 /*@ non_null */ Object o;3 public void m(Object oo) { o = oo; }4 }

genera:

NonNull.java:4: Warning: Possible assignment of nullto variable declared non_null (NonNull)

public void m(Object oo) { o = oo; }^Associated declaration is "NonNull.java",

line 2, col 6:/*@ non_null */ Object o;

^

Cicli e flussi (Assert, Reachable, LoopInv, DecreasesBound).Questi avvisi sono generati da violazioni delle specifiche con-tenute nei corpi delle routine (Assert, Reachable) o dei cicli(LoopInv, DecreasesBound). Ad esempio il warning Assertviene restituito quando una annotazione assert potrebbenon essere soddisfatta.

1 public class AssertWarning {2 //@ requires i >= 0;3 public void m(int i) {4 //@ assert i >= 0;5 --i;6 //@ assert i >= 0;7 }8 }

genera:

AssertWarning.java:6: Warning: Possibleassertion failure (Assert)

//@ assert i >= 0;^

Dato che nel caso il valore di i sia 0, dopo l’istruzione --iil nuovo valore sarebbe -1 in contraddizione con l’ultimaasserzione //@ assert i >= 0;.

Specifiche JML delle classi(Invariant, Constraint, Ini-tially).

Le clausole invariant e constraint generano postcondzioniaggiuntive per ogni funzione, mentre initially genera post-condzioni aggiuntive per ogni costruttore. Se queste con-dizioni non sussistono, i messaggi di errore appropriati ven-gono generati:

1 public class Invariant {2 public int i,j;3 //@ invariant i > 0;4 //@ constraint j > \old(j);5 public void m() {6 i = -1;7 j = j-1;8 }9 }

produce i seguenti messaggi:

Invariant.java:8: Warning: Possible violationof object constraint at exit (Constraint)}^

Associated declaration is "Invariant.java",line 4, col 6://@ constraint j > \old(j);

^Invariant.java:1: Warning: Possible violation

of object invariant (Invariant)public class Invariant {

^Associated declaration is "Invariant.java",

line 3, col 6://@ invariant i > 0;

^

Eccezioni (Exception).Non tutte le possibili eccezioni possono essere previste daESC/Java2, dato che alcune di esse sono da causate dacondizioni che non possono essere modellate. In partico-lare gli errori Java (i.e. OutOfMemoryError) possono esseregenerati in qualsiasi momento e non possono essere previstida ESC/Java2.

ESC/Java2 e piu rigoroso della semantica dei compilaroriJava e quindi genera un Exception warning se una eccezioneincontrollata puo essere esplicitamente lanciata ma non edichiarata in nelle throws. Per quanto riguarda le eccezionicontrollate, il tool si comporta pressoche come un compila-tore Java.

Multithreading (Race, RaceAllNull, Deadlock).Questo tipo di messaggi sono causati da potenziali problemicon i monitor.Problemi di multithreading causati dall’assenza di alcunasincronizzazione non sono rilevati da ESC/Java2.Il tool e in grado, per esempio, di generare un messaggiodi Deadlock quando ogni thread di un gruppo di threadha bisogno di accedere ad un monitor bloccato da un al-tro thread. La ricerca di deadlock e disabilitata di default,ma puo essere attivata usando l’opzione -warn Deadlock.

1 public class DeadlockWarning {2 /*@ non_null */3 final static Object o = new Object();4 /*@ non_null */5 final static Object oo = new Object();6 //@ axiom o < oo;7 //@ requires \max(\lockset) < o;8 public void m() {9 synchronized(o) { synchronized(oo) { }}

10 }11 //@ requires \max(\lockset) < o;12 public void mm() {13 synchronized(oo) { synchronized(o) { }}14 }15 }

genera:

DeadlockWarning.java:11: Warning: Possibledeadlock (Deadlock)

synchronized(oo) { synchronized(o) { }}^

Le funzionalita di ESC/Java2 descritte mostrano come iltool trovo facilmente alcuni errori altrimenti rilevabili soloa runtime (i.e., null pointer, division by zero, index out ofbounds), per gli altri warning molto di pende dalle anno-tazioni JML: piu il codice e annotato piu ESC/Java2 e ingrado di fare assunzioni su di esso. Questo pero implicaanche che la possibilita di cercare problemi all’interno delcodice si basa fortemente sull’assunzione che le annotazioniJML siano complete e corrette.

5. JAVA PATHFINDERJava Path Finder (JPF) [1, 18, 24] e uno strumento per laverifica, l’analisi e il testing di codice Java. Java Path Findere un model checker in grado di eseguire tutte le istruzionicontenute all’interno del bytecode e dunque e in grado dianalizzare qualsiasi programma scritto in Java.

Prima di descrivere in dettaglio lo strumento Java PathFind-er verra fatta una breve introduzione alle tecniche utilizzateper fare model checking sui linguaggi di programmazione.

5.1 Model CheckingIn letteratura e possibile ritrovare diverse definizioni di mod-el checking, ognuna delle quali pone l’accento su di un as-petto diverso del problema [8]. Qui di seguito sono ripor-tate alcune definizioni di model checking che possono essereritrovate in letteratura:

• decidere in modo e!ciente se una formula logica esoddisfacibile da un modello di macchina a stati finiti;

• il compito di definire in modo automatico se un sistemasoddisfa una formula temporale [3];

• il grafo dello stato globale di un sistema puo esserevisto come una struttura di Kripe finita e un algorit-mo e!ciente (model checker) puo essere utilizzato per

determinare se la struttura e un modello di una formu-la particolare (i.e., per determinare se un programmasoddisfa le specifiche) [9];

• supponendo che M sia una strutture di Kripe M =!S, I, R, L", dove S e un insieme di stati, I # S e l’in-sieme degli stati iniziali, R # S $ S e la relazionedi transizione e L e una funzione che etichetta glistati con preposizioni atomiche prese da un oppor-tuno linguaggio, supponendo che ! sia una formu-la di logica temporale, trovare l’insieme di tutti glistati di K che soddisfano !, cioe l’insieme degli stati{s % S|K, s |= !}.

Cio che caratterizza tutte queste definizioni e un comunedenominatore: il model checking tradizionale riguarda laverifica di proprieta temporali di sistemi a stati finiti.

Normalmente il model checking di un software viene ef-fettuato analizzando le proprieta che riguardano le speci-fiche del software stesso [9]. Le specifiche vengono dappri-ma rappresentate come una macchina a stati finiti, e solosuccessivamente, vengono analizzate con i sistemi di modelchecking.

Recentemente e stata invece introdotta una nuova metodolo-gia per l’analisi del software: il model checking non viene piue"ettuato sulle specifiche, bensı sul codice che implementail software. L’obiettivo di tale tecnica e dimostrare che l’im-plementazione del software mantiene proprieta importantie, in particolare, le stesse proprieta che erano state stabilitenelle specifiche.

E comunque importante notare che contrariamente a quan-to accadeva per il model checking tradizionale, nel caso del-l’analisi del codice non e necessario costruire il modello delsoftware poiche questo e fornito gratuitamente dal codicestesso che rappresenta un modello formale del sistema imple-mentato. Il modello e formale poiche e formale il linguaggiodi programmazione utilizzato per descriverlo.

Esistono due approcci per e"ettuare il model checking apartire dal codice [8]:

• l’approccio translation based : cerca di riutilizzare isistemi di model checking esistenti. Il codice sottoanalisi viene prima tradotto in una notazione inter-pretabile dai sistemi di model checking tradizionali equindi analizzato;

• l’approccio ad hoc: consiste nello sviluppare sistemidi model checking che accettano come notazione dispecifica il particolare linguaggio di programmazioneutilizzato per implementare il software.

Il vantaggio piu evidente dei sistemi translation based e lapossibilita di poter riutilizzare strumenti e algoritmi moltoe!cienti, gia studiati a lungo e messi a disposizione dai sis-temi di model checking tradizionali. Il difetto piu grave diquesto approccio risiede invece in una mancanza di flessibilita,causata dal fatto che spesso vi sono notevoli di"erenze se-mantiche tra i linguaggi di programmazione e i linguag-gi di modellazione utilizzati nei sistemi di model checking

tradizionali. Per esempio, i normali linguaggi di model-lazione non supportano diverse funzionalita presenti invecenei normali linguaggi di programmazione (Floating points,allocazione dinamica della memoria, passaggio di parametrimediante puntatori). Appare dunque chiaro che se si vuolee"ettuare model checking su codice e preferibile un approc-cio ad hoc piuttosto che un approccio translation based chenon puo grantire un’analisi completa ed esaustiva di tutto ilcodice.

5.1.1 L’Esplosione degli StatiGeneralmente il model checking comporta l’analisi di un in-sieme di stati molto elevato. La capacita di elaborare egestire un numero elevato di stati ha un e"etto diretto sull’-e!cienza dei sistemi di model checking e ne puo limitarela capacita di trattare sistemi con un numero elevato distati. Il punto debole di tutti i sistemi di model checking,tradizionali e non, e rappresentato dall’esplosione degli stati.Di!cilmente un sistema puo essere modellato mediante uninsieme di stati finito e questo porta ad avere problemi du-rante la fase di gestione degli stati (memorizzazione, tempi diricerca, gestione della memoria). Per limitare questo prob-lema molti sistemi di model checking utilizzano particolaritecniche chiamate di astrazione o riduzione degli stati.

5.2 Java Path FinderIn Figura 7 e rappresentata la struttura di Java Path Find-er. Il cuore della della struttura e rappresentato dalla JavaPath Finder Virtual Machine (JVMJPF) che ha il compi-to di eseguire il bytecode. Durante l’esecuzione e possibileconfigurare e guidare la JVMJPF attraverso un insieme dicomponenti (property checcker e choice generator) e librerie(library abstraction).

Per svolgere questi compiti, JPF combina tecniche di modelchecking tradizionali con tecniche che permettono di trattarespazi con un numero molto alto o infinito di stati. Questetecniche comprendono la symmetry reduction, per ridurre ilnumero degli stati trattati, la static analysis, per support-are la riduzione delle transizioni, la state abstracttion, perastrarre lo spazio degli stati e la runtime analysis utile permettere in evidenza blocchi di codice contenenti lock e corsecritiche e percio potenzialmente dannosi.

5.2.1 Linguaggio e Proprieta SupportateCome gia accennato, la JVMJPF supporta tutto il bytecodeJava e ogni programma scritto utilizzando codice Java puropuo essere analizzato. Purtroppo non tutti i programmirisultano composti da codice Java puro e spesso certi metodisono nativi rispetto al sistema operativo utilizzato. Esempidi codice nativo sono rappresentati da operazioni sul filesys-tem, comunicazioni di rete oppure creazione di codice perapplicazioni GUI. Questo significa che ogni volta che all’in-terno di un programma Java vengono chiamati metodi chenon hanno un bytecode corrispondente, JPF non e in gradodi determinare lo stato di questo codice e di conseguenzanon riesce ad e"ettuarne l’analisi. A questo proposito JPFfornisce MJI, un’interfaccia di astrazione in grado di trattarequesto problema (Sezione 5.2.3).

E’ necessario mettere in evidenza che JPF, come succedeanche per gli strumenti di testing, puo trattare solamente

sistemi chiusi. Questo significa che JPF e"ettua il modelchecking solamente sul sistema preso in esame e sull’ambi-ente all’interno del quale viene eseguito. Le analisi di sistemiesterni non sono ammissibili.

5.2.2 Le Funzionalita di JPFLa funzionalita di base di JPF, funzionalita grazie alla qualee possibile e"ettuare il model checking di codice Java, e lacapacita di simulare il non determinismo. Grazie a questacapacita, JPF funziona come una VM che non solo e in gradodi eseguire un normale programma Java ma e in grado di es-eguirlo in tutti i modi possibili. Ovviamente la simulazionedel non determinismo e qualcosa di piu di una semplice gen-erazione di stati e per gestirla sono necessarie due tecnicheparticolari:

• Backtracking: permette a JPF di ritornare in statieseguiti precedentemente per verificare se esistono per-corsi di esecuzione inesplorati. La stessa cosa potrebbeessere e"ettuata eseguendo ogni volta il programmadall’inizio. Con il backtracking si ha maggiore e!cien-za e la gestione degli stati puo essere ottimizzata;

• State Matching: permette a JPF di evitare lavoroinutile riducendo il numero di stati da controllare. Du-rante l’esecuzione di un programma, JPF controlla seogni nuovo stato generato e uguale ad uno stato prece-dentemente analizzato. Se questo accade significa chenon e necessario proseguire nuovamente lungo quel per-sorso di esecuzione e JPF puo fare backtracking e pros-eguire lungo un percorso non ancora esplorato.

Poiche anche Java Path Finder incorre nei problemi di ges-tione degli stati propri di ogni sistema di model checking,JPF dispone di un insieme di meccanismi che sono in gra-do di mantenere sotto controllo l’eslosione degli stati. JPFa"ronta questo problema:

• Riducendo il costo di memorizzazione di ognistato. Pur non essendo la tecnica principale per af-frontare l’esplosione degli stati e comunque necessariodisporre di meccanismi che permattono di utilizzarein modo e!ciente la memoria per il salvataggio deglistati. Poiche una transizione di stato solitamente com-porta piccoli combiamenti, JPF utilizza tecniche distate collapsing che permettono di ridurre lo spazionecessario alla memorizzazione degli stati;

• Utilizzando strategie di ricerca configurabili.Normalmente non e possibile limitare il numero di risorseutilizzate indirizzando la ricerca all’intero spazio deglistati. JPF permette di risolvere il problema utiliz-zando il model checker non come un dimostratore ma,bensı, come un debugger. In questo modo e possi-bile utilizzare euristiche che permettono di impostareproprieta sugli stati in modo da poterli ordinare e fil-trare durante l’analisi di un percorso di esecuzione. Ladefinizione delle euristiche e della proprieta non fannoparte del core di JPF ma devono essere costruite dagliutenti attraverso particolari classi di configurazionedescritte in Sezione 5.2.3;

verification target(Java bytecode program)

verification report

VM observerdata/scheduling

heuristics

statemgnt

Figure 7: Struttura di Java Path Finder

• Riducendo il numero degli stati che devono esserememorizzati in modo da aumentare la scalabilita delsistema. Questa riduzione e supportata da quattromeccanismi [24]:

– Symmetry Reduction: l’idea su cui poggia questomeccanismo e che la simmetria tra gli stati di unsistema produce una relazione di equivalenza eche durante l’analisi uno stato puo essere scarta-to se uno stato equivalente e gia stato analizzato.JPF utilizza tecniche di partial order reductionche attraverso l’analisi del bytecode sono in gra-do di valutare la simmetria tra gli stati. Talesimmetria puo essere calcolata sia per gli stati in-stanziati nella memoria statica che per quelli in-stanziati nella memoria dinamica. Oltre all’anal-isi del bytecode, la simmetry reduction si basa an-che sul garbage collector che permette a JPF dieliminare dalla memoria dinamica tutti gli statiche sono generati da oggetti non piu referenziati;

– State Abstraction: attraverso questo metodo,un utente puo specificare funzioni di astrazionesu una o piu parti del sistema sotto osservazione.Partendo da queste funzioni, un generico sistemadi model checking ha a disposizione due scelte: i)generare on-the-fly, durante l’esecuzione del mod-el checking, il grafo degli stati sui dati astratti;ii) generare un sistema astratto che manipola idati astratti e che a sua volta deve essere model-lato per poi essere sottoposto a model checking.Poiche le astrazioni vengono solitamente fatte supiccole parti del sistema sotto analisi, JPF uti-lizza il secondo approccio e genera un program-ma astratto il quale sara poi sottoposto a modelchecking;

– Static analysis: l’analisi statica viene e"ettua-ta analizzando i programmi senza eseguirli e sen-za fare particolare assunzioni sui dati di ingressodel programma. Per questo motivo i risultati di

tale analisi possono ritenersi validi indipendente-mente dai valori di ingresso del programma. Alfine di ridurre il numero degli stati, JPF utiliz-za tre tipi di analisi statica: i) la static slicing,che dato un programma e un insieme di criteri dislice genere un programma piu piccolo che risultafunzionalmente equivalente al programma origi-nario rispetto ai criteri di slice (JPF utilizza iltool di slicing di BANDERA); ii) la partial evalu-ation, che propaga i valori costanti e semplifica leespressioni presenti nel codice; la iii) partial ordercomputation che si occupa di identificare state-ment che possono essere incrociati in modo sicurocon statement presenti in altri thread;

– Runtime Analysis: l’analisi dinamica viene ef-fettuata eseguendo un programma una sola voltaper poi osservarne le tracce di esecuzione gener-ate in modo da riuscire ad estrarre da esse infor-mazione riguardanti il programma sotto analisi.Queste informazioni potranno poi essere utiliz-zate per predire se di"erenti esecuzioni dello stes-so programma possono violare i vincoli impostial sistema. JPF utilizza due algoritmi di anal-isi dinamica: i) il data race detection [21], chepermette di rilevare quando si verificano acces-si concorrenti ai dati che possono generare corsecritiche; ii) il deadlock detection [24] che invecepermette di rilevare le situazioni di deadlock nellequali possono incorrere thread di"erenti.

5.2.3 Estendibilita di JPFUn’ulteriore caratteristica di JPF risiede nel fatto che esso estato progettato in modo tale da favorirne l’estendibilita daparte degli utenti. Questo rende JPF un sistema di modelchecking adattabile e scalabile. L’estendibilita viene fornitaattraverso due meccanismi:

• I Search-/VMListeners. Possono essere utilizza-ti per estendere il modello interno di JPF e danno

Figure 8: Struttura generale di Bandera

agli utenti la possibilita di controllare proprieta com-plesse degli stati, configurare le strategie di ricerca oraccogliere statistiche sull’esecuzione dei programmi.L’estensione avviene attraverso il pattern degli observ-er che permette di sottoscriversi ad eventi generatiall’interno di JPF. Questo meccanismo permette, adesempio, di ricevere notifiche quando vengono eseguiteparticolari istruzioni nel bytecode o quando avviene ilpassaggio tra due diversi stati del sistema sotto osser-vazione;

• La Model Java Interface (MJI). Questo e un mec-canismo che permette di controllare la comunicazionetra il codice eseguito all’interno dell JVMJPF e quel-lo che invece e eseguito dalla virtual machine ester-na (quella che esegue JPF). MJI puo essere utilizzatoper realizzare astrazioni delle librerie Java in modo dacontenere la generazione degli stati e superare alcu-ni dei problemi di gestione del codice Java non puroevidenziati nella Sezione 5.2.2.

6. BANDERABandera [6] e un tool per la verifica di codice Java attraver-so tecniche di model checking. La Figura 8 mostra la strut-tura generale di Bandera. Molti tools per la verifica delcodice traducono un intero programma direttamente in unlinguaggio di analisi. L’approccio di Bandera e invece quellotipico del model checking cioe quello di costruire una ver-sione semplificata/astratta del codice su sui applicare le tec-niche di model checking. In particolare Bandera e"ettuauna traduzione del codice in un linguaggio intermedio con-siderando le specifiche proprieta che si vogliono verificare peril codice e quindi supporta una mappatura di questo codicesu diversi linguggi di input per model checker.

Lo scopo di Bandera e quindi quello di fornire un tool perla verifica di codice che sfrutti i modelli per model checkinggia esistenti, che fornisca un supporto automatico per l’as-

trazione del codice e che sia in grado di fornire modelli spe-cializzati secondo le proprieta che vanno verificate. Un in-teressante funzionalita o"erta da Bandera e quella di fornirecontroesempi che mostrino la violazione di una determinataproprieta.

I componenti principali di Bandera sono:

• Slicer che comprime i percorsi nei programmi rimuoven-do punti di controllo, variabili e dati che sono irrilevan-ti per la verifica di una data proprieta.

• Abstraction-Based Specializer che consente all’utentedi ridurre la cardinalita dei dati associati con le vari-abili.

• Back End che genera il BIR: un linguaggio interme-dio di basso livello basato su comandi condizionali chegenera un’astrazione dei comuni linguaggi di input permodel checker. Il Back End contiene un traduttore perogni model checker supportato

• User Interface che facilita l’interazione con le variecomponenti e mostra i controesempi all’utente in ter-mini di programma sorgente, in maniera simile ad undebugger.

La fase di astrazione del codice e caratterizzata da:

• Eliminazione di componenti irrilevanti. Molte dellecomponenti dei programmi possono essere non rilevan-ti per la proprieta che deve essere verificata.

• Astrazione dei dati. Dopo l’eliminazione delle com-ponenti non rilevanti, alcune delle restanti variabili,sebbene rilevanti, possono contenere piu dettagli delnecessario per la proprieta da verificare. E spesso pos-sibile generare una nuova variabile che e un’astrazionedella precedente e quindi piu piccola. Per esempio unapplicazione potrebbe memorizzare un insieme di itemin un vettore, ma la proprieta da verificare dipendesolo dalla presenza o meno nel vettore di un partico-lare item, in questo caso e possibile atrarre l’insiemedei possibili stati del vettore in un insieme piu piccolo{ItemInVector, ItemNotInVector}.

Bandera fornisce un supporto automatico per la costruzionedi questo modello. Inoltre il tool consente una mappatu-ra automatica dall’“error trace” espresso nel linguaggio delmodel checker sul codice sorgente java ed una visualizzazionegrafica di questa traccia.

6.1 Descrizione dettagliata del toolIn questo paragrafo verra mostrato maggiormente in det-taglio il funzionamento di Bandera. Figura 9 mostra lastruttura dettagliata di Bandera.

6.1.1 Linguaggi di rappresentazione intermediL’architettura di Bandera e simile ad un compilatore ot-timizzante. Utilizza diversi linguaggi intermedi per il pas-saggio dal codice Java a quello di input per model checker.

Figure 9: Struttura dettagliata di Bandera

I principali sono due: uno di alto livello chiamato Jimplee sviluppato in [23] ed uno di basso livello chiamato BIR(Bandera Intermediate representation).

E stato sviluppato un front-end chiamato JJJC (Java-to-Jimple-to-Java Compiler) che mantiene una corrispondenzafra il codice sorgente Java e la sua rappresentazione in Jim-ple. Analoga corrispondenza e mantenuta fra il codice inJimple ed il codice in linguaggio BIR che si pone fra il lin-guaggio Jimple e quelli di input ai model checkers e risultaparticolarmente utile nella generazione dei controesempi.

6.1.2 SlicerLe proprieta da verificare per un determinato codice possonoessere considerate i criteri in input alla fase di riduzione esono definite dall’utente attraverso ad esempio formule inlogica temporale. Bandera o"re un menu di template da cuie possibile scegliere.

Il compito del modulo Slicer e proprio quello di ridurre ilcodice Java in base alle proprieta da verificare per consen-tire delle prestazioni accettabili ai model checker. L’e"ettivariduzione del codice dipende dalla struttura del programma.In alcune situazione la riduzione e davvero notevole, in altricasi in cui i compomenti sono strettamente legati e le propri-eta da verificare interessano larga parte di codice la riduzionee molto minore. In ogni caso il costo computazionale per lariduzione e molto minore di quello per il model checkinge questa operazione e totalmente automatica, in Banderaviene sempre e"ettuata questa operazione.

Formalmente, dato un programma P e alcune espressionidi interesse C = {s1, ..., sk} che definiscono un criterio diriduzione, un Program Slicer generera una versione ridottadi P rimuovendo tutte le parti di P che non sono coinvoltenei criteri espressi da C. A seguito della riduzione e statodimostrato che una specifica # vale per P se e solo se # valeper la versione ridotta di P [12]

Costruire un tool automatico per la riduzione del codice Ja-va e piuttosto costoso, ma Bandera sfrutta i risultati giaottenuti in [11,14].

6.1.3 Bandera Abstraction Based SpecializerQuesto modulo consente la riduzione del codice attraversoun’astrazione delle variabili. Data una appropriata definizione

di un’astrazione, l’abstraction engine trasformera il codicesorgente in una versione specializzata. Riprendendoo l’e-sempio dove un vettore e astratto in due stati ItemInVectore ItemNotInVector, e chiaro che l’operazione di astrazionepuo indurre dei problemi di non determinismo (ad. es. se ecoinvolta in una decisione la lunghezza del vettore). Le situ-azioni di non determinismo che vengono gestite sono legatead informazioni non interessanti (ad esempio una scelta con-dizionale sulla lunghezza del vettore) ed e lo specializationengine che in automatico si occupa della loro gestione. Inquesta fase di astrazione e richiesta la collaborazione del-l’utente che puo scegliere da una libreria di template diastrazioni come e"ettuare l’astrazione di determinate vari-abili. La propagazione di questa scelta nel codice e compitodel sistema. Usando il Bandera Abstraction SpecificationLanguage (BASL) [13] e possibile definire nuove astrazioni.

6.1.4 Back-endQuesto modulo e simile ad un generatore di codice, in inputaccetta il codice (ridotto ed astratto) e produce un outputin un linguaggio di input per model checker. I componentidi questo modulo comunicano attraverso il BIR (BanderaIntermediate representation). Come mostrato in Figura 9 ilmodulo BIRC genera la rappresentazione BIR a partire dallarappresentazione in Jimple. Un traduttore ad-hoc poi a par-tire dal BIR genera l’input per il verificatore scelto. Lo scopodel BIR e essenzialmente quello di garantie l’estendibilita diBandera verso nuovi strumenti di verifica in quanto fornisceuna semplice interfaccia per generare nuovi traduttori. L’u-so del BIR facilita poi la generazione dei controesempi perle proprieta violate.

7. CONCLUSIONIL’articolo ha presentato un insieme di tool per l’analisi e laverifica di codice Java. La varieta degli approcci alla basedei tool presentati mette in evidenza la complessita del prob-lema a"rontato: non esistono tecniche che garantiscano unasoluzione completa al problema dell’analisi e della verifica dicodice Java al fine di scoprire potenziali errori. Per questomotivo e compito del programmatore interpretare il prob-lema da risolvere e combinare le varie tecniche in modo datrovarne una soluzione esaustiva.

Infatti, e sı vero che tutte le strategie adottate puntano a

risolvere il problema della rilevazione degli errori nel codicema non per questo portano tutte alla medesima soluzionein termini di potere riconoscitivo. In parte i risultati distrumenti diversi si sovrappongono, ma in generale questinon sono sostituibili l’uno con l’altro. Gli strumenti si com-pletano a vicenda ma purtroppo, anche applicandoli tuttiinsieme, non sono in grado di garantire l’assenza totale dierrori.

La nostra analisi ha messo in evidenza pregi e difetti dicinque tool per l’analisi e la verifica di codice Java. Partendoda questa analisi possiamo a"ermare che:

• FindBugs & PMD analizzano il bytecode (Find-Bugs) e il codice sorgente (PMD). Entrambi si prestanomolto bene all’integrazione con il processo di compi-lazione del codice e permettono un’analisi veloce diintere applicazioni e di intere librerie.

• ESC/Java2 permette di analizzare codice Java stan-dard, anche di dimensioni elevate. Il vero potere deltool viene pero raggiunto solo annotando opportuna-mente il codice con JML. Esc/Java2 si presta soprat-tutto per l’analisi di porzioni limitate di codice e per-tanto e consigliabile utilizzarlo per analizzare quelleparti di codice ritenute critiche.

• Java PathFinder e uno strumento in grado di e"et-tuare model checking su programmi Java. Java PathFind-er ricade nella categoria dei model checker ad hoc, ede utilizzabile in modo e!ciente sopratutto se ne ven-gono create delle apposite estensioni attraverso MJI elistener. Data la complessita dello strumento, l’utiliz-zo di JPF e riservato a programmatori esperti. ComeESC/Java2, anche Java PathFinder si presta per anal-isi limitate del codice (i.e., programmi con un numeromassimo di 10000 linee di codice).

• Bandera ricade nella categoria dei model checker trans-lation based e utilizza meccanismi di riduzione e as-trazione per preparare e ottimizzare codice Java inmodo da adattarlo a diversi model checker (es: SPIN eNuSMV). Bandera interpreta gli error trace dei modelchecker ed e in grado di fornire controesempi. Con-trariamente a Java PathFinder, Bandera dispone diun’ottima interfaccia grafica che ne facilita l’uso.

Concludendo, possiamo a"ermare che tutti gli strumentianalizzati sono e!cienti ed e"ettivamente sono in grado dirilevare potenziali problemi nel codice. Cio che li accomu-na in negativo e la presenza di problemi nella generazionedell’output.

Spesso producono una quantita di messaggi e indicazioni(nei tools basati su model checkers in misura minore ed in-dotti dalla necessita di costruire un’astrazione del codiceper evitare che la complessita esploda). Questo comportache l’utente medio percepisca addirittura il tool stesso comeuno strumento di bassa qualita, poiche da un lato spessonon e in grado di interpretare correttamente tutte le infor-mazioni mostrate mentre dall’altro lato bisogna ammettereche il problema della generazione di false positives e reale epuo compromettere la qualita del risultato.

La strada attualmente seguita per migliorare sia l’e!cien-za dell’analisi stessa che la generazione dell’output consistenell’inserire annotazioni all’interno del codice sotto analisi.Ovviamente questo comporta un notevole sforzo da partedell’utente e addirittura introduce una nuova dimensione dicomplessita nella manutenzione di codice e annotazioni.

Altre strade che potrebbero essere intraprese sono il miglio-ramento degli stessi algoritmi di analisi e l’introduzione ditecniche di filtraggio dell’output. La prima dovrebbe puntarealla radice del problema, ottimizzando le informazioni gen-erate, mentre la seconda dovrebbe cercare di sintetizzare ecalibrare l’output in base alle esigenze degli utenti.

8. REFERENCES[1] The JPF Runtime Verification System.

http://javapathfinder.sourceforge.net/JPF.pdf.

[2] Apache Software Foundation. The byte codeengineering library. http://jakarta.apache.org/bcel/,June 2005.

[3] R. Cleaveland and S. Smolka. Strategic directions inconcurrency research. ACM Computing Surveys,28(4):607 – 625, 1996.

[4] David Cok. Esc/java2 eclipse plugin project.http://sort.ucd.ie/projects/escjava-eclipse/.

[5] David R. Cok and Joseph Kiniry. Esc/java2: Unitingesc/java and jml. In Gilles Barthe, Lilian Burdy,Marieke Huisman, Jean-Louis Lanet, and TraianMuntean, editors, Construction and Analysis of Safe,Secure, and Interoperable Smart Devices, InternationalWorkshop, CASSIS 2004, Marseille, France, March10-14, 2004, Revised Selected Papers, volume 3362 ofLecture Notes in Computer Science, pages 108–128.Springer, 2004.

[6] J.C. Corbett, M.B. Dwyer, J. Hatcli", S. Laubach,C.S. Pasareanu, and R.H. Zheng. Bandera: extractingfinite-state models from java source code. In Proc. ofInternational Conference on on Software Engineering,(ICSE), pages 439–448, Limerick, Ireland, 2000. ACM.

[7] Christoph Csallner and Yannis Smaragdakis. Check’n’ Crash: Combining static checking and testing. InProceedings of the 27th international conference onSoftware engineering, pages 422–431, May 2005.

[8] Giovanni Denaro. A comparison between symbolicexecution based verification and model checking. Tech-nical report, Universita degli Studi di Milano - Bicocca,http://www.lta.disco.unimib.it/doc/ei/pdf/lta.2002.03.pdf,2002. Internal Report.

[9] E. Emerson E. Clarke and A. Sistla. Automaticverification of finite-state concurrent systems usingtemporal logic specifications. ACM Transactions onProgramming Languages and Systems, 8(2):244 – 263,April 1986.

[10] Cormac Flanagan, K. Rustan M. Leino, MarkLillibridge, Greg Nelson, James B. Saxe, and RaymieStata. Extended static checking for java. SIGPLANNot., 37(5):234–245, 2002.

[11] J. Hatcli", J.C. Corbett, M.B.Dwyer, S. Sokolowski,and H.Zheng. A formal study of slicing formulti-threaded programs with jvm concurrencyprimitives. In Proc. of Int. Static Analysis Symposium(SAS), 1999.

[12] J. Hatcli", M.B.Dwyer, and H.Zheng. Slicing softwarefor model construction. Higher-order and SymbolicComputation, 2000.

[13] J. Hatcli", M.B.Dwyer, and S.Laubach. Staging staticanalysis using abstraction-based programspecialization. In Proc. of Int. Symposium onProciples of Declarative Programming (PLILP), 1998.

[14] S. Horwitz, T. Reps, and D. Binkley. Interproceduralslicing using dependence graphs. ACM Transaction onProgramming Languages and systems, 12(1):26–60,1990.

[15] D. Hovemeyer and W. Pugh. Finding bugs is easy. InProceedings of the Onward! Track of the ACMConference on Object-Oriented Programming,Systems, Languages, and Applications (OOPSLA),2004.

[16] JAVA. http://java.sun.com/.

[17] K. Rustan M. Leino and Greg Nelson. An extendedstatic checker for Modula-3. In Kai Koskimies, editor,Proceedings of the 7th International Conference onCompiler Construction, CC’98, volume 1383 ofLecture Notes in Computer Science, pages 302–305.Springer, April 1998.

[18] NASA. Java™path finder.

[19] Bill Pugh and David Hovemeyer. Findbugs - find bugsin java programs.http://findbugs.sourceforge.net/index.html, May 2005.

[20] Nick Rutar, Christian B. Almazan, and Je"rey S.Foster. A comparison of bug finding tools for java. InThe 15th IEEE International Symposium on SoftwareReliability Engineering (ISSRE’04), Saint-Malo,Bretagne, France, November 2004.

[21] Stefan Savage, Michael Burrows, Greg Nelson, PatrickSobalvarro, and Thomas Anderson. Eraser: Adynamic data race detector for multithreadedprograms. ACM Transactions on Computer Systems,15(4):391–411, 1997.

[22] Sourceforge.net. Pmd. http://pmd.sourceforge.net/,June 2005.

[23] R. Valle-Rai, L. Hendren, V. Sundaresan, P. Lam,E. Gagnon, and P. Co. Soot- a java optimizationframework. In Proc. of CASCON, 1999.

[24] Willem Visser, Klaus Havelund, Guillaume Brat, andSeungJoon Park. Model checking programs. In ASE’00: Proceedings of the The Fifteenth IEEEInternational Conference on Automated SoftwareEngineering (ASE’00), page 3, Washington, DC, USA,2000. IEEE Computer Society.