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

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

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

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

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

Answer 1

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

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

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

Джесси имеет:

#pragma JessieIntegerModel(modulo)

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

Во фторе RTE не предупреждает о a + 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);