Реализация C ++, которая обнаруживает неопределенное поведение?

Question

Огромное количество операций в C ++ приводит к неопределенному поведению, когда спецификация полностью отключена от того, каким должно быть поведение программы, и допускает все, что происходит. Из-за этого есть все виды случаев, когда у людей есть код, который компилируется в режиме отладки, но не выпускается, или работает до тех пор, пока не будет сделано, казалось бы, несвязанное изменение, или работает на одной машине, но не на другой, и т. Д.

Мой вопрос заключается в том, существует ли утилита, которая просматривает выполнение кода C ++ и отмечает все случаи, когда программа вызывает неопределенное поведение. Хотя хорошо, что у нас есть такие инструменты, как valgrind и проверенные реализации STL, они не так сильны, как я думаю, - у valgrind могут быть ложные отрицания, если вы, например, удаляете память, выделенную вам, и проверяете реализации STL не поймет удаление через указатель базового класса.

Существует ли этот инструмент? Или вообще было бы полезно, чтобы он вообще валялся?

РЕДАКТИРОВАТЬ : я знаю, что в целом статически не удается проверить, может ли программа на C ++ когда-либо выполнять что-то, что имеет неопределенное поведение. Тем не менее, можно определить, вызвало ли специфическое выполнение C ++ неопределенное поведение. Один из способов сделать это - создать интерпретатор C ++, который будет проходить по коду в соответствии с определениями, приведенными в спецификации, в каждой точке, определяя, имеет ли код неопределенное поведение. Это не обнаружит неопределенное поведение, которое не происходит при выполнении конкретной программы, но оно обнаружит любое неопределенное поведение, которое фактически проявляется в программе. Это связано с тем, как по Тьюрингу можно определить, принимает ли ТМ какой-либо ввод, даже если он все еще неразрешим в целом.

Спасибо!

Answer 1

Это отличный вопрос, но позвольте мне дать представление о том, почему я думаю, что это может быть невозможно (или, по крайней мере, очень сложно) в целом.

Предположительно, такая реализация была бы почти интерпретатором C ++ или, по крайней мере, компилятором для чего-то более похожего на Lisp или Java. Потребуется сохранить дополнительные данные для каждого указателя, чтобы гарантировать, что вы не выполняете арифметику вне массива или разыменовываете что-то, что уже было освобождено или что-то еще.

Теперь рассмотрим следующий код:

int *p = new int;
delete p;
int *q = new int;

if (p == q)
    *p = 17;

Является ли *p = 17 неопределенным поведением? С одной стороны, он разыменовывает p после того, как он был освобожден. С другой стороны, разыменование q хорошо и p == q ...

Но дело не в этом. Дело в том, что оценка if как истинная вообще зависит от деталей реализации кучи, которая может варьироваться от реализации к реализации. Поэтому замените *p = 17 на какое-то фактическое неопределенное поведение, и у вас есть программа, которая может очень хорошо взорваться на обычном компиляторе, но нормально работать на вашем гипотетическом «UB детекторе». (Типичная реализация C ++ будет использовать свободный список LIFO, так что у указателей есть хорошие шансы быть равными. Гипотетический «детектор UB» может работать больше как язык для сборки мусора для обнаружения проблем использования после освобождения.)

Другими словами, существование просто поведения , определяемого реализацией , делает невозможным написание «детектора UB», который работает для всех программ, я подозреваю.

Тем не менее, проект по созданию "строгого компилятора C ++" будет очень интересным. Дайте мне знать, если хотите начать. : -)

Answer 2

Джон Регер в Поиск неопределенных ошибок поведения путем поиска мертвого кода указывает на инструмент под названием STACK , и я цитирую с сайта ( emphasis mine):

Нестабильный код для оптимизации (нестабильный код для краткости) - это новый класс программных ошибок: код, который неожиданно устраняется оптимизацией компилятора из-за неопределенного поведения в программе. Нестабильный код присутствует во многих системах, включая ядро ​​Linux и сервер базы данных Postgres.Последствия нестабильного кода варьируются от неправильной функциональности до отсутствующих проверок безопасности.

STACK - это статическая проверка , которая обнаруживает нестабильный код в программах на C / C ++ .Применение STACK к широко используемым системам выявило 160 новых ошибок, которые были подтверждены и исправлены разработчиками.

Также в C ++ 11 для случая constexpr переменных и функций неопределенное поведение должны быть пойманы ввремя компиляции .

У нас также есть gcc ubsan :

GCC недавно (версия 4.9) получила Undefined Behavior Sanitizer (ubsan), запускпроверка времени для языков C и C ++.Чтобы проверить вашу программу с помощью ubsan, скомпилируйте и свяжите программу с опцией -fsanitize = undefined.Такие инструментальные двоичные файлы должны быть выполнены;если ubsan обнаруживает какую-либо проблему, он выводит сообщение «ошибка времени выполнения:» и в большинстве случаев продолжает выполнение программы.

и Clang Static Analyzer , который включает в себя manyпроверяет на неопределенное поведение.Например, clangs -fsanitize проверяет, что включает -fsanitize=undefined:

-fsanitize = undefined: Быстрая и совместимая неопределенная проверка поведения.Включает неопределенные проверки поведения, которые имеют небольшие затраты времени выполнения и не влияют на структуру адресного пространства или ABI.Это включает в себя все перечисленные ниже проверки, кроме unsigned-integer-overflow.

и для C мы можем взглянуть на его статью Пора серьезно отнестись к эксплуатацииНеопределенное поведение , которое гласит:

[..] Я признаюсь, что лично у меня не было смысла, необходимого для заполнения GCC или LLVM через лучших доступных динамических неопределенных средств проверки поведения: KCC и Frama-C . [...]

Вот ссылка на kcc , и я цитирую:

[...]Если вы попытаетесь запустить программу, которая не определена (или программу, для которой нам не хватает семантики), программа застрянет.Сообщение должно сказать вам, где оно застряло и может дать подсказку, почему.Если вам нужна помощь в расшифровке вывода или в понимании того, почему программа не определена, отправьте нам свой файл .kdump. [...]

и вот ссылка на Frama-C , статья , где описано первое использование Frama-C в качестве интерпретатора C и приложение к статье.

Answer 3

Использование g++

-Wall -Werror -pedantic-error

(желательно с соответствующим аргументом -std) подхватит довольно много случаев U.B.

---

Вещи, которые -Wall получает, включают:

-pedantic
Выпускать все предупреждения, требуемые строгими стандартами ISO C и ISO C ++; отклонять все программы, использующие запрещенные расширения, и некоторые другие программы которые не соответствуют ISO C и ISO C ++. Для ISO C следует версия стандарта ISO C, указанная в любой используемой опции -std.

-Winit-self (только C, C ++, Objective-C и Objective-C ++)
Предупреждать о неинициализированных переменных, которые инициализируются с самих себя. Обратите внимание, что эта опция может использоваться только с Опция -Wuninitialized, которая, в свою очередь, работает только с -O1 и выше. * * тысяча двадцать-одна

-Wuninitialized
Предупредить, если автоматическая переменная используется без предварительного инициализируется или если переменная может быть захвачена вызовом "setjmp".

и различные запрещенные действия, которые вы можете делать со спецификаторами функций семейства printf и scanf.

Answer 4

Clang имеет набор дезинфицирующих средств , которые улавливают различные формы неопределенного поведения. Их конечная цель - уловить неопределенное поведение всего основного языка C ++, но проверки на несколько хитрых форм неопределенного поведения сейчас отсутствуют.

Для достойного набора дезинфицирующих средств попробуйте:

clang++ -fsanitize=undefined,address

-fsanitize=address проверяет использование неверных указателей (не указывая на действительную память), а -fsanitize=undefined включает набор облегченных UB-проверок (целочисленное переполнение, неправильные сдвиги, смещенные указатели, ...).

-fsanitize=memory (для обнаружения неинициализированных операций чтения из памяти) и -fsanitize=thread (для обнаружения скачек данных) также полезны, но ни один из них не может быть объединен ни с -fsanitize=address, ни друг с другом, поскольку все три имеют агрессивное влияние на адресное пространство программы.

Answer 5

Возможно, вы захотите прочитать о SAFECode .

Это исследовательский проект Университета Иллинойса, цель которого указана на первой странице (ссылка выше):

Цель проекта SAFECode - обеспечить безопасность программы без сбора мусора и с минимальными проверками во время выполнения, используя статический анализ, когда это возможно, и проверки во время выполнения, когда это необходимо.SAFECode определяет представление кода с минимальными семантическими ограничениями, разработанными для обеспечения статического обеспечения безопасности, используя агрессивные методы компиляции, разработанные в этом проекте.

Что меня действительно интересует, так это устранение проверок во время выполнения всякий раз, когда программа может быть подтверждена статически корректно, например:

int array[N];
for (i = 0; i != N; ++i) { array[i] = 0; }

Больше не должно возникатьнакладные расходы, чем обычная версия.

Более легким образом, Clang , насколько я помню, тоже имеет некоторые гарантии относительно неопределенного поведения, но я не могу достать его ...

Answer 6

К сожалению, я не знаю ни одного такого инструмента.Обычно UB определяется как таковой именно потому, что компилятору будет трудно или невозможно диагностировать его во всех случаях.

На самом деле ваш лучший инструмент - это, вероятно, предупреждения компилятора: они часто предупреждают об элементах типа UB (например,не виртуальный деструктор в базовых классах, злоупотребление правилами строгого наложения имен и т. д.).

Проверка кода также может помочь выявить случаи, в которых используется UB.

Тогда вы должны полагаться наvalgrind захватывает остальные случаи.

Answer 7

Компилятор clang может обнаруживать некоторые неопределенные поведения и предупреждать их. Возможно, не так полно, как хотелось бы, но это определенно хорошее начало.

Answer 8

Так же, как побочное наблюдение, согласно теории вычислимости, вы не можете иметь программу, которая обнаруживает все возможные неопределенные поведения.

У вас могут быть только инструменты, которые используют эвристику и обнаруживаютнекоторые конкретные случаи, которые следуют определенным моделям.Или вы можете в некоторых случаях доказать, что программа ведет себя так, как вы хотите.Но вы не можете обнаружить неопределенное поведение в целом.

Редактировать

Если программа не завершает работу (зависает, зацикливается навсегда) на данном входе, то ее вывод не определен.

Если вы согласны с этим определением, то определение того, завершается ли программа, является общеизвестной «проблемой остановки», которая, как было доказано, неразрешима, т. Е. Не существует программы (Turing Machine, программа C,Программа на C ++, программа на языке Pascal на любом языке), которая может решить эту проблему в общем.

Проще говоря: не существует программы P, которая может принимать в качестве входных данных любую программу Q и вводить данные I и печатать в качестве выходных данных TRUE, еслиQ (I) завершается, или выведите FALSE, если Q (I) не завершается.

Для получения дополнительной информации вы можете посмотреть http://en.wikipedia.org/wiki/Halting_problem.

Answer 9

Взгляните на PCLint , он довольно неплох при обнаружении множества плохих вещей в C ++.

Здесь это подмножество того, что он ловит

Answer 10

Неопределенное поведение: undefined . Лучшее, что вы можете сделать, это педантично соответствовать стандарту, как предлагали другие, однако вы не можете проверить, что не определено, потому что вы не знаете, что это такое. Если бы вы знали, что это было, и стандарты указали это, это не было бы неопределенным.

Однако, если вы по какой-то причине действительно полагаетесь на то, что в стандарте написано undefined , и это приводит к определенному результату, то вы можете определить его и написать несколько модульных тестов для подтвердите, что для вашей конкретной сборки это определено. Однако гораздо лучше избегать неопределенного поведения, когда это возможно.