Dowody kodu, który opiera się na niepodpisanym całkowitym przepełnieniu?

Question

Jak mam podejść do udowodnienia poprawności kodu, jak poniżej, który, aby uniknąć jakiejś nieefektywności, opiera się na modułowej arytmetyki?

#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; 
} 

Mam eksperymentował z modelu „int” WP, ale, jeśli dobrze rozumiem, że wzór konfiguruje semantykę całkowitymi logicznych w OP, a nie formalne modele kod C. Na przykład, wtyczki WP i RTE wciąż wymagają i wstrzykują przepełnienie asercji PO dla niepodpisanego dodania powyżej podczas korzystania z modelu "int".

W takich przypadkach, czy mogę dodać adnotacje określające model logiczny dla instrukcji lub bloku podstawowego, więc mógłbym powiedzieć Frama-C, jak dany kompilator faktycznie interpretuje instrukcję? Jeśli tak, to czy mogę użyć innych technik weryfikacji w przypadku takich rzeczy, jak zdefiniowane, ale często wywołujące defekty zachowania, takie jak niepodpisane otoczenie, zachowania zdefiniowane przez kompilator, niestandardowe zachowania (wbudowane assy?) Itp., A następnie udowodnienie poprawności dla otaczający kod. Wyobrażam sobie coś podobnego do (ale silniejszego niż) "poprawki assert", używanej do informowania niektórych analizatorów statycznych, że pewne właściwości utrzymują się, gdy nie mogą samodzielnie wyprowadzić właściwości.

Pracuję z Frama-C Fluor-20130601, dla odniesienia, z alt-ergo 95.1.

Answer 1

pracuję z Frama-C fluor 20130601

Cieszę się, że znalazł sposób na korzystanie z najnowszej wersji.

Oto kilka losowych bitów informacji, które, choć nie w pełni odpowiedzieć na to pytanie, nie pasują komentarz StackOverflow:

Jessie posiada:

#pragma JessieIntegerModel(modulo) 

Powyższy Pragma czyni go rozważyć wszystkie przepełnienia (zarówno undefined, jak i unsigned one unsigned) zawijają się (w tym samym podpisanym przepełnieniu, w arytmetyce uzupełnień 2). Wytworzone zobowiązania dowodowe są znacznie trudniejsze, ponieważ zawierają dodatkowe operacje modulo na całym świecie. Z zautomatyzowanych dowodów twierdzeń, zazwyczaj tylko Simplify jest w stanie coś z nimi zrobić.

W fluor, RTE nie ostrzega o A + B domyślnie:

$ 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 mogą być wykonane, aby ostrzec o unsigned Ponadto z opcją -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; 
    … 

Ale to właśnie przeciwieństwo tego, czego chcesz, więc nie rozumiem, dlaczego to zrobiłeś.

Answer 2

Nie podano dokładnej linii poleceń, której używasz. Chyba to jest frama-c -wp -wp-rte file.c -pp-annot. W takim przypadku generowane są wszystkie twierdzenia, że ​​RTE może emitować. Możesz jednak uzyskać lepszą kontrolę nad tym, polecając frama-c, aby najpierw wygenerował tylko kategorie RTE, które Cię interesują (zachowaj ostrożność, aby były kontrolowane przez dwa rodzaje opcji: zdefiniowane są frama-c -rte-help i -warn-{signed,unsigned}-{overflow,downcast} w jądrze), a następnie uruchomić wp na wynik.Odbywa się to poprzez frama-c -rte -pp-annot file.c -then -wp Domyślnie RTE nie uważa niepodpisany przepełnienie być błąd, tak że z powyższej linii komend, jestem w stanie udowodnić, że funkcja jest zgodny z następującą specyfikację:

/*@ 
    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);