eclair

Lo sviluppo di software di qualità è un lavoro duro: ECLAIR è stato progettato per assistere i team di sviluppo software e il reparto di controllo di qualità nel raggiungimento di elevati standard qualitativi e nell'ottenimento della relativa certificazione.

Cos'è ECLAIR

ECLAIR è una potente piattaforma per l'automazione dell'analisi, la verifica, il test e la trasformazione di programmi C e C++ (stiamo realizzando l'estensione a Java). [Schema di ECLAIR]

ECLAIR è molto flessibile ed estremamente configurabile. Può supportare il vostro workflow ed il vostro ambiente di sviluppo qualunque essi siano. Potete chiederci di adattarlo alle vostre specifiche necessità oppure potete farlo voi stessi.

ECLAIR si presta sia a compiti di verifica leggeri, da eseguire direttamente sul PC del singolo sviluppatore, sia ad analisi semantiche approfondite, da eseguirsi di notte.

ECLAIR è adeguato a progetti software mission-critical e safety-critical: è stato progettato dalle fondamenta in modo da escludere i falsi negativi a meno che la configurazione utente non li richieda esplicitamente.

ECLAIR viene sviluppato in modo rigoroso ed attentamente controllato anche con l'uso di testsuite interne molto estese (decine di migliaia di casi di test) nonché di suite di validazione industriali (come ACE SuperTest).

ECLAIR è basato su solidi risultati della ricerca scientifica e sulle migliori pratiche dello sviluppo software. Attenzione all'abusato luogo comune della inconciliabilità tra teoria e pratica: un sistema veramente affidabile e funzionale può solo basarsi su di un rigoroso lavoro di ricerca teorica.

ECLAIR viene sviluppato da un appassionato gruppo di esperti. Non esitate a farci avere i vostri commenti: sarete sorpresi da quanto seriamente terremo conto dei vostri suggerimenti.

Cosa ECLAIR non è

ECLAIR non è qualcosa che vi dirà quali analisi, verifiche ed attività di test siano appropriate nel vostro campo. In particolare, non vi dirà quali regole di codifica siano consigliabili per il vostro progetto. Ma gli esperti di linguaggi di programmazione di BUGSENG vi assisteranno e vi supporteranno su questi temi.

Le funzionalità di ECLAIR in breve

Applicazioni supportate

Controllo automatico di standard di codifica

ECLAIR supporta il controllo automatico di conformità rispetto a numerosi standard di codifica di largo uso, tra cui:

• CERT C;
• EC--;
• MISRA C:1998;
• MISRA C:2004;
• The Power of Ten (C);
• NASA/JPL C;
• Netrino Embedded C;
• ESA/BSSC C/C++;
• CERT C++;
• MISRA C++:2008;
• JSF C++;
• High-Integrity C++;
• Delphi C;
• Industrial Strength C++;
• Nokia Qt (C++).

BUGSENG ha sviluppato checker automatici per la verifica di conformità rispetto a vari altri standard, oltre a quelli elencati, tra i quali standard proprietari aziendali e standard specifici di singoli progetti. Il controllo delle regole di codifica è affidato a checker molto generali ed accurati, che operano sull'esatta sequenza di token e alberi di sintassi astratta che sono manipolati dal compilatore.^{1Ciò si pone in netto contrasto con i checker basati su pattern matching e parsing impreciso. Se da una parte questi possono trattare programmi non compilabili, dall'altra sono affetti da un numero elevato di falsi positivi e, soprattutto, falsi negativi, cosa che li rende inadeguati all'impiego in ambito safety-critical e mission-critical. In generale, occorre fare molta attenzione agli strumenti basati su tecnologia obsoleta: direttive come la 90/385/EEC e la 93/42/EEC, nel settore medicale, asseriscono che la conformità alla norma (compliance) può essere rivendicata solo se si è seguito lo stato dell'arte così come è generalmente riconosciuto.} Abbinato al fatto che ECLAIR controlla sempre ogni regola nel contesto appropriato (a livello di token, dichiarazione, unità di traduzione, o di intero programma o sistema), questo garantisce che i checker per le regole decidibili sono sempre esatti (ovvero senza falsi positivi né falsi negativi). Per le regole indecidibili, ECLAIR fornisce checker alternativi caratterizzati da diverse soluzioni del compromesso tra complessità computazionale, numero di falsi positivi e numero di falsi negativi. In ogni caso, quando i falsi negativi sono possibili, essi sono sempre chiaramente delimitati senza alcuna ambiguità.

ECLAIR può essere configurato per produrre ogni sorta di rapporto sulle violazioni riscontrate:

• per un esame immediato o differito usando IDE molto diffusi come Eclipse, Microsoft Visual Studio, IAR Embedded Workbench®, ed ogni altro editor funzionalmente adeguato (un potente browser web-based delle violazioni e del codice che le riguarda è al momento in beta-test);
• per l'inserimento automatico in sistemi di issue-tracking ed ogni altro database;
• per la produzione automatica delle matrici di conformità necessarie per soddisfare i requisiti di standard e direttive industriali come IEC 61508, ISO 26262 (settore automotive), CENELEC EN 50128 (ferroviario), DO-178B/C (aerospaziale), IEC 62304 e norme FDA (medicale).

Analisi semantica

Stiamo equipaggiando ECLAIR con potenti motori di propagazione di vincoli, model checking simbolico e interpretazione astratta. Il loro uso combinato consente la realizzazione di differenti compromessi tra complessità computazionale e precisione, così che ogni utente possa scegliere la combinazione costi-benefici che meglio si adatta ai propri obiettivi. Sul PC del programmatore, le analisi semplici e veloci sono le più appropriate; ma quando l'alternativa è tra dimostrare, ad esempio, l'assenza di errori a run-time manualmente o meccanicamente, 12 ore di calcolo sono meglio di un mese-uomo di lavoro: ECLAIR è stato progettato per supportare l'intero spettro tra questi due estremi.

Generazione automatica di casi di test

ECLAIR può sintetizzare automaticamente insiemi minimi di input per test funzionali che raggiungono un criterio di copertura specificato (ove questo non sia possibile, ECLAIR dimostra che tale copertura non è ottenibile a causa di condizioni insoddisfacibili nel programma). Se è a disposizione un "oracolo", umano o meccanico, per predire l'output atteso, i test di unità completi possono essere prodotti in una frazione del tempo necessario per la generazione manuale.

Matching e patching semantico

ECLAIR può eseguire complesse trasformazioni di programmi trovando automaticamente nel sorgente aree del programma identificate da criteri sintattici e semantici. I frammenti interessati possono essere rimpiazzati con una sostituzione parametrica.

Altre applicazioni

Semplificatori, offuscatori, traduttori, ... questi sono solo pochi esempi della quantità di applicazioni che, grazie alla modularità del progetto di ECLAIR, possono essere sviluppate con relativa facilità lavorando al giusto livello di astrazione. Ad esempio, ECLAIR comprende un semplificatore C che legge un qualunque sorgente di programma e (tenendo in conto gli aspetti implementation-defined dell'implementazione considerata) scrive codice C equivalente ma molto semplificato (dove, tra l'altro, gli effetti collaterali sono stati rimossi dalle espressioni).

Piena integrazione con la toolchain

ECLAIR intercetta ogni invocazione dei componenti della toolchain (compilatori, linker, assembler, gestore degli archivi) estraendo ed interpretando automaticamente le opzioni che il build system gli ha passato. Questo consente la perfetta integrazione con ogni build system. Inoltre, l'utente non deve esporsi ad attività caratterizzate da elevata probabilità di errore, quali:

• la specifica di quali file compongano l'applicazione e dove siano collocati gli header file giusti;
• la configurazione dell'analizzatore statico in modo che i parametri dell'analisi corrispondano alle opzioni passate al compilatore (molte delle quali influenzano la semantica del programma).

Tutto questo è ottenuto automaticamente, in modo da supportare anche processi di costruzione dell'applicazione che comportano la generazione automatica di sorgenti dipendenti dalla configurazione, senza richiedere lo sviluppo e la maintenance di una procedura di analisi separata: con ECLAIR la procedura di compilazione esistente può essere utilizzata invariata.

Una delle proprietà chiave di ECLAIR è la sua "comprensione" di tutte le opzioni dei compilatori supportati che sono rilevanti per l'analisi. Il linguaggio usato per realizzare un modello astratto di tali opzioni è così potente che aggiungere il supporto per un nuovo compilatore non è più un problema.

Interfaccia di configurazione web-based

Tutti i compiti di verifica supportati da ECLAIR possono essere specificati e rivisti incrementalmente per mezzo di una comoda interfaccia di configurazione web-based. Mediante l'utilizzo di un normale web browser è possibile, ad esempio: trovare le regole di codifica di interesse, utilizzando una potente logica di selezione basata su tag; attivare e personalizzare le regole di codifica, opzionalmente restringendo il loro impiego a parti specifiche del progetto; selezionare e personalizzare il tipo di rapporti e matrici di conformità da produrre; mettere a punto il trattamento semantico di ogni operazione elementare (in particolare per ciò che concerne i comportamenti indefiniti o definiti dall'implementazione) per il model-checking e la generazione automatica di casi di test; scegliere se eseguire immediatamente il task di verifica o se salvarlo per usarlo in seguito.

Parsing preciso dei sorgenti

ECLAIR include un parser per i linguaggi C e C++ conforme allo stato dell'arte. In particolare, per:

• il dialetto C pre-standardizzazione (K&R);
• i linguaggi C standard (C90, C99 e C11);
• i linguaggi C++ standard (C++98, C++03 e C++11);
• le estensioni dei dialetti GNU C/C++ (eccetto qualche estensione deprecata);
• le estensioni dei dialetti Microsoft C/C++.

Stiamo lavorando per supportare altre estensioni (come OpenCL e CUDA) nonché il linguaggio Java.

Il parser produce un albero di sintassi astratta (AST) molto accurato, il quale rappresenta tutte le informazioni disponibili, direttamente ed indirettamente, nel codice analizzato. Accuratezza significa, in particolare, che:

• l'AST rappresenta non solo i costrutti esplicitamente presenti nel codice, ma anche quelli impliciti: conversioni di tipo implicite, funzioni generate dal compilatore (ad esempio i costruttori non definiti esplicitamente), istanze di funzioni e classi templatiche, ecc.;
• tutti i costrutti del linguaggio sono corredati da informazioni precise riguardo alla loro collocazione nei sorgenti, consentendo la generazione di rapporti che identificano esattamente l'esatta origine di ogni violazione.

L'informazione sulla collocazione nei sorgenti non è solo precisa, ma anche esaustiva:

• sono disponibili informazioni complete sulla catena di inclusioni e, ortogonalmente, sulla catena di espansioni di macro che hanno portato un token lessicale a far parte del codice analizzato;
• la ben nota difficoltà di tracciare i problemi in istanze implicite di template è risolta presentando all'utente informazioni complete e, al tempo stesso, facilmente leggibili circa l'intera catena di istanziazione.

Piattaforme e ambienti di sviluppo supportati

ECLAIR è disponibile su tutte le moderne varianti di Unix®, Linux, Mac OS X® e Windows®, inclusi Cygwin e MinGW, e può essere usato in abbinamento con ogni ambiente di sviluppo. Grazie alla sua abilità di intercettare le invocazioni dei componenti della toolchain, supporta ogni tipo di build system, sia esso basato su makefile, su script, o ibrido. ECLAIR può trarre vantaggio dalla disponibilità di risorse di calcolo supportando analisi parallele e distribuite. I più diffusi compilatori e cross-compilatori C/C++ sono supportati, inclusi quelli Code Warrior™, GCC, Green Hills®, IAR, Intel®, Microsoft®, MPLAB®, Renesas Electronics, clang/LLVM.