Обход переполнения без знака, обнаруженного CBMC
CBMC обнаруживает возможное переполнение без знака в следующих строках:
l = (t + *b)&(0xffffffffL);
c += (l < t);
Я согласен, что существует вероятность переполнения в первой строке, но я забочусь о переносе в следующей строке, который CBMC не в состоянии рассмотреть. Если в случае переполнения я устанавливаю перенос 1. Таким образом, поскольку я знаю об этом, об этом и о том, как я хочу, чтобы мой код работал, я хотел бы перейти к процессу проверки. Итак, как же я говорю CBMC пропустить эту ошибку и двигаться дальше?
1 ответ
TL;DR Это зависит от того, каковы действительные типы переменных. Во всех случаях CBMC обнаруживает фактическую ошибку, которая может привести к неопределенному поведению. Это означает, что вы должны исправить свой код, а не отключить сообщение в CBMC.
Полный ответ:
В целом: насколько мне известно, CBMC не позволяет исключать определенные свойства (с другой стороны, вы можете проверить только одно отдельное свойство, используя --property флаг). Если вы хотите получить официальный ответ / мнение или сделать запрос на добавление новых функций, я бы рекомендовал размещать их в группе поддержки CProver.
(Конечно, можно использовать __CPROVER_assume чтобы CBMC исключил следы, приводящие к ошибке, но это было бы очень, очень, очень плохой идеей, поскольку это может сделать другие проблемы недоступными.)
Вариант 1: я предполагаю, что ваш код выглядит примерно так (в связи с этим: пожалуйста, опубликуйте отдельные примеры и объясните точно, в чем проблема, эти вещи трудно угадать)
long nondet_long(void);
void main(void) {
long l = 0;
int c = 0;
long t = nondet_long();
long s = nondet_long();
long *b = &s;
l = (t + *b) & (0xffffffffL);
c += (l < t);
}
и ты бежишь
cbmc --signed-overflow-check test.c
дать вывод, похожий на следующий?
CBMC версия 5.1 64-битные макросы x86_64 Parsing test.c Преобразование теста проверки типа Генерация программы GOTO Добавление библиотеки CPROVER Функция Удаление указателя Частичное встраивание Общие инструменты Инструментарий Запуск ограниченной модели Проверка размера выражения программы: 41 шаг, простое срезание удалено 3 назначения Сгенерировано 2 VCC(s), 2 осталось после упрощения Передача задачи на пропозициональное редукцию преобразование SSA Выполнение пропозиционального редукции Постобработка Решение с помощью MiniSAT 2.2.0 с упрощающими переменными 792, 2302 предложения Проверка SAT: отрицательное утверждение является SATISFIABLE, т. е. не содержит процедуру принятия решения во время выполнения: 0.006s Трассировка ошибки построения Контрпример: Состояние 17 файла test.c строка 4 функции основной поток 0
----------------------------------------------------
l=0 (0000000000000000000000000000000000000000000000000000000000000000000000000000) Файл состояния 18 test.c строка 4, функция основной поток 0
----------------------------------------------------
l=0 (0000000000000000000000000000000000000000000000000000000000000000) Состояние 19 файла test.c строка 5 функции main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000) Файл состояния 20 test.c строка 5, функция основной поток 0 ---------------- ------------------------------------ c = 0 (00000000000000000000000000000000) Состояние 21 file test.c строка 6 функция основного потока 0
----------------------------------------------------
t=0 (0000000000000000000000000000000000000000000000000000000000000000000000000000) Файл состояния 22 test.c строка 6, функция основной поток 0
----------------------------------------------------
t=-9223372036854775808 (100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) Состояние 23 файл test.c строка 7, функция основной поток 0
----------------------------------------------------
s=0 (000000000000000000000000000000000000000000000000000000000000000000000000000000) Файл состояния 24 test.c строка 7, функция основной поток 0
----------------------------------------------------
s=-9223372036854775807 (1000000000000000000000000000000000000000000000000000000000000001) Состояние 25 файл test.c строка 8 функция основной поток 0
----------------------------------------------------
b=((long int *)NULL) (000000000000000000000000000000000000000000000000000000000000000000000000000000) Файл состояния 26 test.c строка 8 функция основной поток 0
----------------------------------------------------
b=&s!0@1 (0000001000000000000000000000000000000000000000000000000000000000) Нарушенное свойство: файл test.c Строка 10 Функция основного арифметического переполнения при знаменном + в t + *b! Переполнении ("+", знаковый длинный int, t, *b) СБОЙ ПРОВЕРКИ Я не думаю, что вы должны отключить эту проверку свойства, даже если вы могли бы. Причиной этого, как вы говорите, является то, что это дополнение может переполниться, и целочисленное переполнение является неопределенным поведением в C, или, как этот ответ на вопрос, как проверить целочисленное переполнение в C? красиво говорит:
[O] После того, как вы выполнили x + y, если он переполнен, вы уже в рукаве. Слишком поздно делать какие-либо проверки - ваша программа могла уже потерпеть крах. Думайте об этом, как о проверке деления на ноль - если вы ждете, пока разделение будет выполнено, проверить, уже слишком поздно.
См. Также Целочисленное переполнение и неопределенное поведение и Насколько губительным является целочисленное переполнение в C++?,
Таким образом, это реальная ошибка, и у CBMC есть веская причина рассказать вам об этом. Что вы на самом деле должны сделать, так это адаптировать свой код, чтобы избежать возможных переполнений! Ответ, упомянутый выше, предполагает что-то вроде (не забудьте включить limits.h):
if ((*b > 0 && t > LONG_MAX - *b)
|| (*b < 0 && LONG_MIN < *b && t < LONG_MIN - *b)
|| (*b==LONG_MIN && t < 0))
{
/* Overflow will occur, need to do maths in a more elaborate, but safe way! */
/* ... */
}
else
{
/* No overflow, addition is safe! */
l = (t + *b) & (0xffffffffL);
/* ... */
}
Вариант 2: Здесь, я предполагаю, ваш код выглядит примерно так:
unsigned int nondet_uint(void);
void main(void) {
unsigned int l = 0;
unsigned int c = 0;
unsigned int t = nondet_uint();
unsigned int s = nondet_uint();
unsigned int *b = &s;
l = (t + *b) & (0xffffffffL);
c += (l < t);
}
и ты бежишь
cbmc --unsigned-overflow-check test.c
дать вывод, похожий на следующий?
CBMC версия 5.1 64-битные макросы x86_64
Разбор test.c
преобразование
Тип проверки
Генерация программы GOTO
Добавление библиотеки CPROVER
Удаление указателя функции
Частичное встраивание
Универсальный приборостроение
Начало проверки ограниченной модели
размер выражения программы: 42 шага
простая нарезка убрано 3 задания
Создано 3 VCC, 3 осталось после упрощения
Передача задачи в пропозициональную редукцию
преобразование SSA
Запуск пропозиционального сокращения
Постобработка
Решение с помощью MiniSAT 2.2.0 с упрощением
519 переменных, 1306 предложений
SAT checker: отрицаемая заявка является УДОВЛЕТВОРЕННОЙ, т. Е. Не имеет места
Процедура принятия решения во время выполнения: 0,01 с
Трассировка ошибок здания
контрпример:
Состояние 17 файла test.c строка 4 функции основного потока 0
---------------------------------------------------
l=0 (00000000000000000000000000000000)
Состояние 18 файла test.c строка 4 функции основной поток 0
---------------------------------------------------
l=0 (00000000000000000000000000000000)
Состояние 19 файла test.c строка 5 функции основного потока 0
-------------------------------------------------- -
с = 0 (00000000000000000000000000000000)
Состояние 20 файла test.c Строка 5 Функция основного потока 0
-------------------------------------------------- -
с = 0 (00000000000000000000000000000000)
Состояние 21 файла test.c Строка 6 Функция основного потока 0
---------------------------------------------------
t=0 (00000000000000000000000000000000)
Состояние 22 файла test.c строка 6 функция основной поток 0
---------------------------------------------------
t=4187126263 (11111001100100100111100111110111)
Состояние 23 файла test.c строка 7 функция основной поток 0
---------------------------------------------------
s=0 (00000000000000000000000000000000)
Состояние 24 файла test.c строка 7 функция основной поток 0
---------------------------------------------------
s=3329066504 (11000110011011011000011000001000)
Состояние 25 файла test.c строка 8 функция основной поток 0
---------------------------------------------------
b=((unsigned int *)NULL) (000000000000000000000000000000000000000000000000000000000000000000000000000000)
Состояние 26 файла test.c строка 8 функции основного потока 0
-------------------------------------------------- -
b = & s! 0 @ 1 (0000001000000000000000000000000000000000000000000000000000000000000000000000)
Нарушенное свойство:
файл test.c строка 10 функция main
арифметическое переполнение на unsigned + в t + *b! переполнение ("+", без знака int, t, *b)
ПРОВЕРКА НЕ ПРОВЕРЕНА
Опять же, это реальная ошибка, и у CBMC есть веская причина рассказать вам об этом. Этот может быть исправлен
l = ((unsigned long)t + (unsigned long)*b) & (0xffffffffL);
c += (l < t);
который дает
CBMC версия 5.1 64-битные макросы x86_64 Разбор test.c преобразование Тип проверки Генерация программы GOTO Добавление библиотеки CPROVER Удаление указателя функции Частичное встраивание Универсальный приборостроение Начало проверки ограниченной модели размер выражения программы: 42 шага простая нарезка убрано 3 задания Создано 3 VCC, 3 осталось после упрощения Передача задачи в пропозициональную редукцию преобразование SSA Запуск пропозиционального сокращения Постобработка Решение с помощью MiniSAT 2.2.0 с упрощением 542 переменных, 1561 предложение Проверка SAT несовместима: отклоненное требование НЕ УДОВЛЕТВОРЕНО, т.е. Процедура принятия решения во время выполнения: 0,002 с ПРОВЕРКА УСПЕШНАЯ
Вариант 3: Если все как и в предыдущем случае, но у вас есть signed int вместо unsigned int все становится немного сложнее. Здесь, если вы используете (написано несколько более сложным способом, чтобы лучше увидеть, что происходит)
int nondet_int(void);
void main(void) {
int l = 0;
int c = 0;
int t = nondet_int();
int s = nondet_int();
long longt = (long)t;
long longs = (long)s;
long temp1 = longt + longs;
long temp2 = temp1 & (0xffffffffL);
l = temp2;
c += (l < t);
}
и беги
cbmc --signed-overflow-check test.c
ты получишь
CBMC версия 5.1 64-битные макросы x86_64 Разбор test.c преобразование Тип проверки Генерация программы GOTO Добавление библиотеки CPROVER Удаление указателя функции Частичное встраивание Универсальный приборостроение Начало проверки ограниченной модели размер выражения программы: 48 шагов простая нарезка убрано 3 задания Создано 3 VCC, 3 осталось после упрощения Передача задачи в пропозициональную редукцию преобразование SSA Запуск пропозиционального сокращения Постобработка Решение с помощью MiniSAT 2.2.0 с упрощением 872 переменных, 2430 предложений SAT checker: отрицаемая заявка является УДОВЛЕТВОРЕННОЙ, т. Е. Не имеет места Процедура принятия решения во время выполнения: 0,008 с Трассировка ошибок здания контрпример: Состояние 17 файла test.c строка 4 функции основного потока 0 --------------------------------------------------- l=0 (00000000000000000000000000000000) Состояние 18 файла test.c строка 4 функции основной поток 0 --------------------------------------------------- l=0 (00000000000000000000000000000000) Состояние 19 файла test.c строка 5 функции основного потока 0 -------------------------------------------------- - с = 0 (00000000000000000000000000000000) Состояние 20 файла test.c Строка 5 Функция основного потока 0 -------------------------------------------------- - с = 0 (00000000000000000000000000000000) Состояние 21 файла test.c Строка 6 Функция основного потока 0 --------------------------------------------------- t=0 (00000000000000000000000000000000) Состояние 22 файла test.c строка 6 функция основной поток 0 --------------------------------------------------- t=-2147483648 (10000000000000000000000000000000) Состояние 23 файла test.c строка 7 функция основной поток 0 --------------------------------------------------- s=0 (00000000000000000000000000000000) Состояние 24 файла test.c строка 7 функция основной поток 0 --------------------------------------------------- s=1 (00000000000000000000000000000001) Состояние 25 файла test.c строка 9 функции основного потока 0 --------------------------------------------------- longt=0 (0000000000000000000000000000000000000000000000000000000000000000000000000000) Состояние 26 файла test.c строка 9 функции основного потока 0 --------------------------------------------------- longt=-2147483648 (1111111111111111111111111111111110000000000000000000000000000000) Состояние 27 файла test.c строка 10 функции основного потока 0 --------------------------------------------------- longs=0 (0000000000000000000000000000000000000000000000000000000000000000000000000000) Состояние 28 файла test.c строка 10 функции основного потока 0 --------------------------------------------------- longs=1 (0000000000000000000000000000000000000000000000000000000000000000000000000001) Состояние 29 файла test.c строка 11 функции основного потока 0 --------------------------------------------------- temp1=0 (0000000000000000000000000000000000000000000000000000000000000000000000000000) Состояние 31 файла test.c строка 11 функции основного потока 0 --------------------------------------------------- temp1=-2147483647 (1111111111111111111111111111111110000000000000000000000000000001) Состояние 32 файла test.c строка 12 функция основной поток 0 --------------------------------------------------- temp2=0 (0000000000000000000000000000000000000000000000000000000000000000000000000000) Состояние 33 файла test.c строка 12 функции основного потока 0 --------------------------------------------------- temp2=2147483649 (0000000000000000000000000000000010000000000000000000000000000001) Нарушенное свойство: файл test.c строка 14 функция main арифметическое переполнение при преобразовании со знаком в типе (подписано int)temp2 temp2 = -2147483648l ПРОВЕРКА НЕ ПРОВЕРЕНА
Или, написано более кратко, если у вас есть
t == -2147483648 (0b10000000000000000000000000000000)
s == 1 (0b00000000000000000000000000000001)
затем
temp2 == 2147483649 (0b0000000000000000000000000000000010000000000000000000000000000001)
и попытка превратить это в signed int это проблема, потому что она выходит за пределы допустимого диапазона (см. также. Поддерживает ли приведение между подписанным и беззнаковым int сохранение точного битового шаблона переменной в памяти?).
Как видите, этот контрпример также является реальной ошибкой, и опять же, CBMC прав, когда рассказывает вам об этом. В частности, это означает, что ваша маскировка / математика не работает должным образом (ваша маскировка превращает отрицательное число в положительное число, которое выходит за пределы), и вам нужно исправить свой код, чтобы результат находился в необходимом диапазоне. (Вероятно, стоит тщательно подумать о том, что вы действительно хотите сделать, чтобы убедиться, что вы получите правильные результаты.)