Проверка отсутствия целочисленных циклов без знака - PullRequest
Новая
       30

Проверка отсутствия целочисленных циклов без знака

1 голос
/ 04 мая 2020

Frama- c, по-видимому, разрешает циклическое вычисление беззнакового целочисленного значения, в то время как предполагается, что целочисленное целое число со знаком не будет переполнено, и это необходимо позже доказать с помощью флага -wp-rte. (Я лично использую Frama- C 20.0 Calcium.) Я хотел бы как-то создать гарантию / требование, чтобы некоторые расчеты / свойства не переполнялись. Упрощенная версия проблемы, которую я пытаюсь решить, такова: 

#include <stdint.h>

struct example_struct {
  unsigned int a;
  unsigned int b;
};

/*@
  predicate valid_example_struct_one{L}(struct example_struct ex_struct) =
    ex_struct.a * ex_struct.b <= UINT_MAX;
*/

Очевидно, что приведенный выше предикат всегда верен из-за циклического преобразования в целочисленной математике без знака. Я хотел бы иметь возможность приводить a и b к целочисленному типу, который не будет переполнен, или как-то указать, что он не может переполниться, используя другой метод. Следующее, кажется, несколько работает: 

/*@
  predicate valid_example_struct_two{L}(struct example_struct ex_struct) =
    1 <= UINT_MAX / ex_struct.a / ex_struct.b;
*/

Однако я не уверен, что вышесказанное действительно эквивалентно, так как оно пытается доказать (обратите внимание на поменявшиеся местами a и b): 

  1 <= UINT_MAX / ex_struct.b / ex_struct.a;

, если я попрошу это с введенным сообщением, удерживайте до предиката valid_example_struct_two. У кого-нибудь есть предложения сказать, что a * b меньше, чем UINT_MAX (без выполнения циклического изменения)?

1 Ответ

2 голосов
/ 04 мая 2020

Ваш предикат 

/*@
  predicate valid_example_struct_one{L}(struct example_struct ex_struct) =
    ex_struct.a * ex_struct.b <= UINT_MAX;
*/

не "всегда верен из-за циклического преобразования целой математики без знака". Как упомянуто в руководстве ACSL, все арифметические операции c в ACSL выполняются в типе integer (или real), т.е. без циклического переноса. Таким образом, это канонический способ express отсутствия арифметического c переполнения и тот, который используется RTE и Eva при излучении связанных аварийных сигналов.

При этом RTE вполне способен выдать утверждение для переполнения без знака, но это должно быть активировано явно с опцией ядра -warn-unsigned-overflow (см. Frama- C руководство пользователя , раздел 6.3. Причина, по которой эта опция не активирована по умолчанию, заключается в том, что наоборот например, со знаком переполнения, без знака переполнения имеют совершенно определенную семантику в C.

...