Prova del codice che si basa sull'overflow di numeri interi senza segno?

Question

Come dovrei avvicinarmi a dimostrare la correttezza del codice come il seguente, che, per evitare qualche inefficienza, si basa sull'aritmetica modulare?

#include <stdint.h> 

uint32_t my_add(uint32_t a, uint32_t b) { 
    uint32_t r = a + b; 
    if (r < a) 
     return UINT32_MAX; 
    return r; 
} 

Ho sperimentato con il modello "int" di WP, ma, se ho capito bene, quel modello configura la semantica di interi logiche OP, non i modelli formali di codice C. Ad esempio, i plug-in WP e RTE richiedono ancora e iniettano PO di asserzione di overflow per l'aggiunta senza segno sopra quando si utilizza il modello "int".

In casi come questo, posso aggiungere annotazioni che stabiliscono un modello logico per un'istruzione o un blocco di base, così ho potuto dire a Frama-C come un particolare compilatore interpreta effettivamente un'istruzione? In tal caso, potrei usare altre tecniche di verifica per cose come comportamenti definiti, ma spesso causa di difetti come involontari involontari, comportamenti definiti dal compilatore, comportamenti non standard (in linea assy?), Ecc., E quindi provare la correttezza per codice circostante. Sto immaginando qualcosa di simile a (ma più potente di) la "assert fix" usata per informare alcuni analizzatori statici che certe proprietà mantengono quando non possono derivare le proprietà da sole.

Sto lavorando con Frama-C Fluorine-20130601, per riferimento, con alt-ergo 95.1.

Answer 1

sto lavorando con Frama-C Fluoro-20130601

Mi fa piacere vedere che hai trovato un modo per utilizzare la versione più recente.

Ecco alcuni bit casuali di informazione che, anche se non rispondono completamente alla tua domanda, non rientrano in un commento StackOverflow:

Jessie ha:

#pragma JessieIntegerModel(modulo) 

È possibile che questo pragma rende considerare che tutti gli overflow (sia quelli firmati non definiti sia quelli definiti senza segno) si avvolgono (nello stesso modo degli overflow firmati, nell'aritmetica del complemento a 2). Gli obblighi di prova generati sono molto più difficili, perché contengono operazioni modulo aggiuntive ovunque. Dei dimostratori di teoremi automatici, in genere solo Simplify è in grado di fare qualcosa con loro.

In Fluoro, RTE non avvisa di un B + per impostazione predefinita:

$ frama-c -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    r = a + b; 
    if (r < a) { 
    __retres = 4294967295U; 
    goto return_label; 
    } 
    __retres = r; 
    return_label: return __retres; 
} 

RTE può essere fatto per mettere in guardia circa l'aggiunta non firmato con l'opzione -warn-unsigned-overflow:

$ frama-c -warn-unsigned-overflow -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    /*@ assert rte: unsigned_overflow: 0 ≤ a+b; */ 
    /*@ assert rte: unsigned_overflow: a+b ≤ 4294967295; */ 
    r = a + b; 
    … 

Ma è proprio questo il di fronte a ciò che vuoi quindi non vedo perché lo faresti.

Answer 2

Non hai fornito la riga di comando esatta che hai utilizzato. Immagino che questo sia frama-c -wp -wp-rte file.c -pp-annot. In tal caso, infatti, vengono generate tutte le asserzioni che RTE può eventualmente emettere. Puoi comunque avere un controllo più preciso, istruendo frama-c in primo luogo a generare solo le categorie di RTE a cui sei interessato (fai attenzione che siano controllate da due tipi di opzioni: quelle di frama-c -rte-help e di -warn-{signed,unsigned}-{overflow,downcast} definite nel kernel), quindi lanciare wp sul risultato.Questo viene fatto frama-c -rte -pp-annot file.c -then -wp Per impostazione predefinita, rte non considera senza segno troppo pieno per essere un errore, in modo che con la linea di comando di cui sopra, sono in grado di dimostrare che la vostra funzione rispetti le seguenti specifiche:

/*@ 
    behavior no_overflow: 
    assumes a + b <= UINT32_MAX; 
    ensures \result == a+b; 
    behavior saturate: 
    assumes a+b > UINT32_MAX; 
    ensures \result == UINT32_MAX; 
*/ 
uint32_t my_add(uint32_t a,uint32_t b);