Prestazioni deterministiche dei compilatori C (o qualsiasi altro).

https://stackoverflow.com/questions/60547

09-06-2019
|

Domanda

Mentre lavoravo a un progetto recente, ho ricevuto la visita di un rappresentante del QA del cliente, che mi ha posto una domanda che non avevo mai considerato prima:

Come fai a sapere che il compilatore che stai utilizzando genera codice macchina che corrisponde esattamente alla funzionalità del codice c e che il compilatore è completamente deterministico?

A questa domanda non ho avuto assolutamente risposta perché ho sempre dato per scontato il compilatore.Accetta il codice ed emette codice macchina.Come posso procedere e verificare che il compilatore non stia effettivamente aggiungendo funzionalità che non ho richiesto?o ancora più pericolosamente implementare il codice in modo leggermente diverso da quello che mi aspetto?

Sono consapevole che forse questo non è un problema per tutti, e in effetti la risposta potrebbe essere semplicemente..."Sei sopra un barile e affrontalo".Tuttavia, quando lavori in un ambiente incorporato, ti fidi implicitamente del tuo compilatore.Come posso dimostrare a me stesso e al QA che ho ragione nel farlo?

Soluzione

Per le applicazioni integrate critiche per la sicurezza, gli enti di certificazione richiedono di soddisfare il requisito di "proven-in-use" per il compilatore.In genere esistono determinati requisiti (tipo "ore di funzionamento") che devono essere soddisfatti e comprovati da una documentazione dettagliata.Tuttavia, la maggior parte delle persone non può o non vuole soddisfare questi requisiti perché può essere molto difficile soprattutto nel primo progetto con un nuovo target/compilatore.

Un altro approccio consiste fondamentalmente nel NON fidarsi affatto dell'output del compilatore.Eventuali carenze del compilatore e anche dipendenti dal linguaggio (Appendice G dello standard C-90, qualcuno?) devono essere coperte da una serie rigorosa di analisi statiche, test unitari e di copertura oltre ai successivi test funzionali.

Uno standard come MISRA-C può aiutare a limitare l'input al compilatore a un sottoinsieme "sicuro" del linguaggio C.Un altro approccio consiste nel limitare l'input di un compilatore a un sottoinsieme di un linguaggio e testare quale sia l'output per l'intero sottoinsieme.Se la nostra applicazione è costituita solo da componenti del sottoinsieme, si presume che si conosca quale sarà l'output del compilatore.Di solito va per "qualifica del compilatore".

L'obiettivo di tutto ciò è essere in grado di rispondere alla domanda del rappresentante del QA con "Non ci basiamo solo sul determinismo del compilatore, ma questo è il modo in cui lo dimostriamo...".

Altri suggerimenti

Puoi applicare questo argomento a qualsiasi livello:ti fidi delle librerie di terze parti?ti fidi del sistema operativo?ti fidi del processore?

Un buon esempio del motivo per cui questa potrebbe essere una preoccupazione valida, ovviamente, è il modo in cui Ken Thompson ha inserito una backdoor nel programma di "accesso" originale...e modificato il compilatore C in modo che anche se ricompilassi il login avresti ancora la backdoor.Guarda questo pubblicazione per ulteriori dettagli.

Domande simili sono state sollevate sugli algoritmi di crittografia: come facciamo a sapere che non esiste una backdoor nel DES attraverso la quale la NSA può curiosare?

Alla fine devi decidere se ti fidi abbastanza dell'infrastruttura su cui stai costruendo da non preoccupartene, altrimenti devi iniziare a sviluppare i tuoi chip di silicio!

Lo sai testando.Quando esegui il test, stai testando sia il codice che il compilatore.

Scoprirai che le probabilità che tu o l'autore del compilatore abbiate commesso un errore sono molto inferiori alle probabilità che fareste un errore se scriveste il programma in questione in qualche linguaggio assembly.

Sono disponibili tute di convalida del compilatore.
Quello che ricordo è "Perenne".

Quando ho lavorato su un compilatore C per un processore SOC incorporato, abbiamo dovuto convalidare il compilatore rispetto a questo e ad altri due semi di convalida (di cui non ricordo il nome).Convalidare il compilatore a un certo livello di conformità a questi test faceva parte del contratto.

Tutto si riduce alla fiducia.Il tuo cliente si fida di qualche compilatore?Usalo o almeno confronta il codice di output tra il tuo e il loro.

Se non si fidano di nessuno, esiste un'implementazione di riferimento per la lingua?Potresti convincerli a fidarsi?Quindi confronta il tuo con il riferimento o usa il riferimento.

Tutto questo presupponendo che tu verifichi effettivamente il codice effettivo che ricevi dal venditore/provider e che controlli che il compilatore non sia stato manomesso, che dovrebbe essere il primo passo.

In ogni caso questo lascia ancora la domanda su come verificare, senza avere riferimenti, un compilatore, da zero.Sembra sicuramente un sacco di lavoro e richiede una definizione del linguaggio, che non sempre è disponibile, a volte la definizione è il compilatore.

Come fai a sapere che il compilatore che stai utilizzando genera codice macchina che corrisponde esattamente alla funzionalità del codice c e che il compilatore è completamente deterministico?

Non lo fai, ecco perché testi il codice binario risultante e perché ti assicuri di spedire lo stesso codice binario con cui hai testato.E perché quando si apportano modifiche "minori" al software, si esegue un test di regressione per assicurarsi che nessuna delle vecchie funzionalità si sia interrotta.

L'unico software che ho certificato è l'avionica.La certificazione FAA non è abbastanza rigorosa per dimostrare che il software funziona correttamente, ma allo stesso tempo ti costringe a fare un certo numero di passaggi.Il trucco sta nel strutturare il tuo "processo" in modo che migliori il più possibile la qualità, con il minor numero possibile di salti estranei.Quindi tutto ciò che sai è inutile e in realtà non troverà bug, probabilmente puoi scappare.E tutto ciò che sai dovresti fare perché lo sia Volere trova bug che non sono esplicitamente richiesti dalla FAA, la soluzione migliore è distorcere le parole finché non sembra che tu stia dando alla FAA / al tuo personale del QA ciò che hanno chiesto.

In realtà questo non è così disonesto come ho fatto sembrare, in generale la FAA si preoccupa di più che tu sia coscienzioso e fiducioso di essere provando fare un buon lavoro, piuttosto che quello che fai esattamente.

Alcuni argomenti intellettuali potrebbero essere trovati in Crosstalk, una rivista per ingegneri di software per la difesa.Questa domanda è il tipo di cosa su cui trascorrono molte ore da svegli. http://www.stsc.hill.af.mil/crosstalk/2006/08/index.html (Se riesco a trovare i miei vecchi appunti da un vecchio progetto, torno qui...)

Non puoi mai fidarti completamente del compilatore, anche di quelli altamente raccomandati.Potrebbero rilasciare un aggiornamento che presenta un bug e il tuo codice viene compilato allo stesso modo.Questo problema si aggrava quando si aggiorna il vecchio codice con il compilatore difettoso, si eseguono test e si spedisce la merce solo per farsi chiamare dal cliente 3 mesi dopo per un problema.

Tutto si basa sui test e, se c'è una cosa che ho imparato, è eseguire test approfonditi dopo ogni modifica non banale.Se il problema sembra impossibile da trovare, dai un'occhiata all'assembler compilato e verifica che stia facendo quello che dovrebbe fare.

In diverse occasioni ho riscontrato bug nel compilatore.Una volta si è verificato un bug in cui le variabili a 16 bit venivano incrementate ma senza riporto e solo se la variabile a 16 bit faceva parte di una struttura esterna definita in un file di intestazione.

... ti fidi implicitamente del tuo compilatore

Smetterai di farlo la prima volta che incontri un bug del compilatore.;-)

Ma alla fine è a questo che servono i test.Non importa per il tuo regime di test come il bug sia entrato nel tuo prodotto, tutto ciò che conta è che non abbia superato il tuo vasto regime di test.

BENE..non puoi semplicemente dire che ti fidi dell'output del tuo compilatore, in particolare se lavori con codice incorporato.Non è difficile trovare discrepanze tra il codice generato durante la compilazione dello stesso codice con compilatori diversi.Questo avviene perché lo standard C stesso è troppo vago.Molti dettagli possono essere implementati in modo diverso da compilatori diversi senza infrangere lo standard.Come affrontiamo queste cose?Evitiamo costrutti dipendenti dal compilatore quando possibile.Possiamo affrontarlo scegliendo un sottoinsieme più sicuro di C like Misra-C come accennato in precedenza dall'utente cschol.Raramente devo controllare il codice generato dal compilatore, ma a volte è successo anche a me.Ma, alla fine, ti affidi ai tuoi test per assicurarti che il codice si comporti come previsto.

C'è un'opzione migliore là fuori?Alcuni sostengono che esista.L'altra opzione è scrivere il codice SCINTILLA/Ada.Non ho mai scritto codice in SPARK ma da quanto ho capito dovresti comunque collegarlo alle routine scritte in C che si occuperebbero del materiale "bare metal".La bellezza di SPARK/Ada è che hai la garanzia assoluta che il codice generato da qualsiasi compilatore sarà sempre lo stesso.Nessuna ambiguità di sorta.Oltre a ciò, il linguaggio consente di annotare il codice con spiegazioni su come si prevede che il codice si comporti.Il set di strumenti SPARK utilizzerà queste annotazioni per dimostrare formalmente che il codice scritto fa effettivamente ciò che le annotazioni hanno descritto.Quindi mi è stato detto che per i sistemi critici, SPARK/Ada è una buona scommessa.Non l'ho mai provato personalmente però.

Non sai per certo che il compilatore farà esattamente quello che ti aspetti.Il motivo è, ovviamente, quello un compilatore è un pezzo di software, ed è quindi suscettibile ai bug.

Gli autori di compilatori hanno il vantaggio di lavorare con specifiche di alta qualità, mentre il resto di noi deve capire cosa stiamo facendo man mano che procediamo.Tuttavia, le specifiche del compilatore Anche hanno bug e parti complesse con interazioni sottili.Quindi, non è esattamente banale capire cosa dovrebbe fare il compilatore.

Tuttavia, una volta deciso cosa pensi che significhino le specifiche della lingua, puoi scrivere un test valido, veloce e automatizzato per ogni sfumatura.È qui che la scrittura del compilatore ha un enorme vantaggio rispetto alla scrittura di altri tipi di software:nei test.Ogni bug diventa un caso di test automatizzato e la suite di test può essere molto approfondita.I fornitori di compilatori hanno molto più budget da investire nella verifica della correttezza del compilatore rispetto a te (hai già un lavoro quotidiano, giusto?).

Che cosa significa questo per te?Significa che devi essere aperto alle possibilità di bug nel tuo compilatore, ma è probabile che non ne troverai nessuno tu stesso.

Sceglierei un fornitore di compilatori che difficilmente cesserà l'attività a breve, che ha una storia di alta qualità nei propri compilatori e che ha dimostrato la propria capacità di fornire assistenza (patch) ai propri prodotti.I compilatori sembrano diventare più corretti nel tempo, quindi ne sceglierei uno che esiste da circa un decennio o due.

Concentra la tua attenzione su come ottenere il codice corretto. Se è chiaro e semplice, poi quando tu Fare si verifica un bug del compilatore, non dovrai pensare molto per decidere dove si trova il problema. Scrivi buoni test unitari, che garantirà che il tuo codice faccia ciò che ti aspetti.

Prova il test unitario.

Se ciò non bastasse, utilizza compilatori diversi e confronta i risultati dei tuoi test unitari.Confronta gli output strace, esegui i test in una VM, conserva un registro degli I/O del disco e della rete, quindi confrontali.

Oppure proponi di scrivere il tuo compilatore e di dire loro quanto costerà.

Il massimo che puoi facilmente certificare è che stai utilizzando un compilatore non manomesso dal provider X.Se non si fidano del fornitore X, il problema è loro (se X è ragionevolmente affidabile).Se non si fidano di alcun fornitore di compilatori, sono totalmente irragionevoli.

Rispondendo alla loro domanda:Mi assicuro di utilizzare un compilatore non manomesso da X attraverso questi mezzi.X ha una buona reputazione, inoltre ho una bella serie di test che mostrano che la nostra applicazione si comporta come previsto.

Tutto il resto sta iniziando ad aprire il vaso dei vermi.Devi fermarti da qualche parte, come dice Rob.

A volte si ottengono cambiamenti comportamentali quando si richiedono livelli aggressivi di ottimizzazione.

E l'ottimizzazione e i numeri in virgola mobile?Lasci perdere!

Per la maggior parte dello sviluppo software (si pensi alle applicazioni desktop) la risposta è probabilmente che non lo sai e non ti interessa.

Nei sistemi critici per la sicurezza (pensa alle centrali nucleari e all'avionica commerciale) tu Fare le agenzie di cura e di regolamentazione ti chiederanno di dimostrarlo.Secondo la mia esperienza, puoi farlo in due modi:

Utilizzare un compilatore qualificato, dove "qualificato" significa che è stato verificato secondo gli standard stabiliti dall'agenzia di regolamentazione.
Eseguire l'analisi del codice oggetto.In sostanza, si compila una parte di codice di riferimento e quindi si analizza manualmente l'output per dimostrare che il compilatore non ha inserito alcuna istruzione che non possa essere ricondotta al codice sorgente.

Ottieni quello che ha scritto Dijkstra.

Seleziona un compilatore formalmente verificato, come il compilatore Compcert C.

La modifica del livello di ottimizzazione del compilatore modificherà l'output.
Piccole modifiche a una funzione potrebbero rendere il compilatore inline o non più inline una funzione.
Le modifiche al compilatore (ad esempio le versioni gcc) possono modificare l'output
Alcune funzioni della libreria possono essere instriniche (cioè emettere un assembly ottimizzato) mentre altre non lo sono.

La buona notizia è che per la maggior parte delle cose non ha molta importanza.In tal caso, potresti prendere in considerazione l'assemblaggio se è davvero importante (ad esempio, in un ISR).

Se sei preoccupato per un codice macchina imprevisto che non produce risultati visibili, l'unico modo è probabilmente contattare il fornitore del compilatore per una certificazione di qualche tipo che soddisfi il tuo cliente.

Altrimenti lo saprai nello stesso modo in cui conosci i bug nel tuo codice: i test.

Il codice macchina dei compilatori moderni può essere molto diverso e totalmente incomprensibile per gli umani deboli.

Penso che sia possibile ridurre questo problema a Problema di arresto in qualche modo.

Il problema più ovvio è che se usi qualche tipo di programma per analizzare il compilatore e il suo determinismo, come fai a saperlo tuo il programma viene compilato correttamente e produce il risultato corretto?

Se stai usando un altro compilatore "sicuro", non ne sono sicuro.Quello di cui sono sicuro è che scrivere un compilatore da zero sarebbe probabilmente un lavoro più semplice.

Anche un compilatore qualificato o certificato può produrre risultati indesiderati.Mantieni il tuo codice semplice e prova, prova, prova.Oppure esegui manualmente il codice macchina senza consentire alcun errore umano.Inoltre il sistema operativo o qualunque ambiente su cui sei in esecuzione (preferibilmente nessun sistema operativo, solo il tuo programma).

Questo problema è stato risolto in ambienti mission-critical sin dall'inizio del software e dei compilatori.Come sanno anche molti altri che hanno risposto.Ogni settore ha le proprie regole, dai compilatori certificati allo stile di programmazione (devi sempre programmare in questo modo, non usare mai questo o quello o l'altro), molti test e revisioni tra pari.Verifica di ogni percorso di esecuzione, ecc.

Se non lavori in uno di questi settori, ottieni ciò che ottieni.Un programma commerciale su un sistema operativo COTS su hardware COTS.Fallirà, questa è una garanzia.

Se sei preoccupato per dannoso bug nel compilatore, una raccomandazione (IIRC, un requisito NSA per alcuni progetti) è che il binario del compilatore sia anteriore alla scrittura del codice.Almeno allora sai che nessuno lo ha fatto aggiunto bug presi di mira tuo programma.

Autorizzato sotto: CC-BY-SA insieme a attribuzione

Non affiliato a StackOverflow