Доказательства для кода, основанного на переполнении целых чисел без знака?

Question

Как я должен подходить к доказательству правильности кода, как показано ниже, что, во избежание некоторой неэффективности, зависит от модульной арифметики?

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

Я экспериментировал с моделью РГ «ИНТ», но, если я правильно понимаю, что модель настраивает семантику логических чисел в ДДУ, а не формальные модели коды C. Например, плагины WP и RTE по-прежнему требуют и вводят PO-запросы подтверждения переполнения для беззнакового добавления выше при использовании модели «int».

В таких случаях можно добавить аннотации, содержащие логическую модель для оператора или базового блока, поэтому я мог бы рассказать Frama-C, как конкретный компилятор действительно интерпретирует инструкцию? Если это так, я мог бы использовать другие методы проверки для таких вещей, как поведение, связанное с определенным, но часто вызывающим дефекты, такое как неподписанное обертывание, поведение, определяемое компилятором, нестандартное поведение (встроенный assy?) И т. Д., А затем доказать правильность окружающий код. Я представляю нечто похожее (но более мощное, чем) «assert fix», используемое для информирования некоторых статических анализаторов о том, что некоторые свойства сохраняются, когда они не могут получить свойства для себя.

Я работаю с Frama-C Fluorine-20130601, для справки, с alt-ergo 95.1.

Answer 1

Я работаю с Frama-C Фтор-20130601

Рад видеть, что вы нашли способ использовать последнюю версию.

Вот некоторые случайные биты информации, что, хотя они и не полностью ответить на ваш вопрос, не поместился в StackOverflow комментарий:

Jessie имеет:

#pragma JessieIntegerModel(modulo) 

выше Прагма делает его рассмотреть что все переполнения (как неопределенные подписанные, так и определенные беззнаковые) обертываются (в том же знаке переполнения, в арифметике дополнений 2). Сгенерированные обязательства по доказательству намного сложнее, потому что они содержат дополнительные модульные операции во всем мире. Из автоматизированных инструкторов теорем, как правило, только Simplify способен что-то с ними делать.

В фтором, RTE не предупреждает о + B по умолчанию:

$ 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 можно сделать, чтобы предупредить о неподписанных дополнительно с опцией -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; 
    … 

Но это точно напротив того, чего вы хотите, поэтому я не понимаю, почему вы это сделаете.

Answer 2

Вы не указали точную командную строку, которую используете. Я думаю, это frama-c -wp -wp-rte file.c -pp-annot. В этом случае, действительно, генерируются все утверждения, которые RTE может испускать. Тем не менее, вы можете более точно контролировать это, инструктируя frama-c сначала генерировать только интересующие вас категории RTE (будьте осторожны, чтобы они контролировались двумя типами опций: frama-c -rte-help и -warn-{signed,unsigned}-{overflow,downcast} в ядре), а затем запустите wp на результат.Это делается с помощью frama-c -rte -pp-annot file.c -then -wp По умолчанию, RTE не считает неподписанного переполнения ошибки, так что с помощью данной командной строки, я могу доказать, что функция уважает следующие характеристики:

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