Стандарт ISO C - официальная спецификация языка C - оставляет многие части семантики языка C неопределенными. В случае неопределённого поведения программа может сделать буквально всё что угодно, (например, может попасть в аварию, или может привести к произвольному результату и побочным эффектам). Поэтому, чтобы установить корректность программы на языке Си, необходимо убедиться, что программа не имеет неопределенного поведения для всех возможных вариантов недетерминированности из-за неустановленного поведения.
В этой статье мы сосредоточимся на неопределенном поведении, связанном с семантикой выражения С, которое было проигнорировано большинством существующих инструментов верификации, но имеет решающее значение для установления правильности реалистичных программ на С. Стандарт языка Си не требует, чтобы подвыражения вычислялись в определенном порядке, а скорее позволяет их вычислять в любом порядке. Более того, выражение имеет неопределенное поведение, когда между двумя точками следования(так называемое "нарушение точки следования") имеется конфликтующий доступ на запись или чтение-запись в одном и том же месте. Точки последовательности возникают, в конце полного выражения (;), до и после каждого вызова функции, а также после первого операнда условного выражения(-?-:-)
Давайте посмотрим это на рисунке 1 :
Из-за неопределенного порядка оценки можно было бы наивно ожидать, что эта программа напечатает либо « 3 7 », либо « 4 7 », в зависимости от того, какое назначение для "х " было оценено первым. Но эта программа демонстрирует неопределенное поведение из-за нарушения точки последовательности: есть две конфликтующие записи в переменную Open image в новом окне. Действительно, при компиляции с GCC (версия 8.2.0) программа фактически выводит « 4 8 », что не соответствует ожидаемым результатам ни одного из заказов на оценку.
Можно ожидать, что эти программы можно легко статически исключить, используя некоторую форму статического анализа, но это не так. В отличие от простой программы, описанной выше, можно получить доступ к значениям произвольных указателей, что делает невозможным статическое установление отсутствия конфликтов записи или чтения-записи. Кроме того, необходимо не только установить отсутствие неопределённого поведения из-за противоречивого доступа к одним и тем же локациям, но и установить отсутствие других форм неопределённого поведения (например, отсутствие разыменованных NULL указателей) для любого порядка оценки.
Для решения этой проблемы, Кребберс разработал программную логику, основанную на логике параллельного разделения (CSL) для установления отсутствия неопределенного поведения в программах на языке Си при наличии недетерминизма. Чтобы получить представление о том, как работает его логика, рассмотрим правило для оператора сложения:
Это правило очень похоже на правило для параллельной композиции в CSL - предварительное условие должно быть разделено на две части P1 и P2, описывающие ресурсы, необходимые для доказательства тройственности Хоара обоих операндов. Принципиально важно, поскольку P1 и P2 описывают разобщенные ресурсы, выраженные разделительной связью, то гарантируется, что Открытое изображение в новом окне и Открытое изображение в новом окне не будут мешать друг другу, а значит не вызовут нарушения точек следования.
Целью последнего помещения правила является обеспечение того, чтобы для всех возможных возвращаемых значений и постусловия, а так же двух операндов можно объединить в постусловие, всего выражение.
Логика Кребберса имеет ряд ограничений, влияющих на его практичность:
-Правила не являются алгоритмическими, и поэтому непонятно, как они могут быть реализованы в рамках автоматизированного или интерактивного инструмента.
-Трудно расширить логику новыми особенностями. Обоснованность монолитной и специальной модели логики разделения была доказана.
Рассмотрим обе эти проблемы.
Представлен новый алгоритм символического исполнения в логике разделения. В отличие от обычного символического исполнения в логике разделения, наш символический исполнитель принимает в качестве своего ввода выражение и предусловие и вычисляет не только постусловие, но и одновременно вычисляет кадр, описывающий ресурсы, которые не были использованы для доказательства постусловия. Рамка используется для вывода предпосылок и постусловий смежных подвыражений.
Для полуавтоматического рассуждения о программах на языке Си мы интегрируем наш символический исполнитель в генератор верификационных условий (vcgen). Наш vcgen не просто превращает программы в доказательственные цели, но и конструирует доказательственные цели только при условии, что он может автоматически выполнять их с помощью нашего символического исполнителя. Если попытка использования символического исполнителя не удастся, наш vcgen вернет новую цель, с которой vcgen может быть вызван снова после того, как пользователь помог. Такой подход полезен при интеграции в интерактивную испытатель теорем.
Доказана правильность символического исполнителя и генератора условий верификации в отношении уточненной версии логики разделения по Кребберам. Наша новая логика была разработана поверх Iris framework и наследует таким образом все расширенные возможности Iris (такие как экспрессивная поддержка призрачного состояния и инвариантов), без необходимости моделировать их явно. Чтобы наша новая логика лучше соответствовала доказательству корректности символического исполнителя и генератора условий верификации, вместо изначальной логики Кребберса в три раза слабее, чем изначальная логика Хоара, наша новая логика поставляется со слабейшей связью предварительного условия.
Чтобы упростить доказательство правильности нашей новой программной логики, мы предоставляем новый монодифференциальный перевод подмножества Си, относящегося к недетерминизму и точкам следования, на функциональный язык в стиле ML с параллелизмом. В отличие от прямого стиля оперативной семантики для подмножества языка Си, предложенного Кребберами, наш подход приводит к более простой для понимания семантике и расширению с помощью дополнительных языковых возможностей.
Механизировали все наши разработки в интерактивной теоретической поговорке Coq. Символический исполнитель и генератор условий верификации определены в Coq как вычислимые функции и интегрированы в тактику в рамках Iris Proof Mode/MoSeL. Для получения сквозной корректности мы механизировали доказательства правильности работы нашего символического исполнителя и генератора условий проверки в соответствии с нашей новой логикой разделения и новой монадической семантикой определения для подмножества C. Разработка Coq доступна для пользования.
Мы описываем подход к полуавтоматическому доказательству отсутствия неопределенного поведения в данной программе на языке Си для любого порядка оценки. При этом мы вносим следующий вклад:
Мы определяем MC небольшой язык Си-стиля с семантикой путем моноадного перевода на функциональный язык ML с параллельностью;
Представлена разделительная логика с наиболее слабыми предпосылками для MC, основанная на разделительной логике для недетерминизма Кребберса в С;
Доказываем правильность нашей логики разделения с самыми слабыми предпосылками, давая модульную модель с использованием Iris-структуры;
Представляем нового символического исполнителя, который вычисляет не только постусловие выражения Си, но и кадр, используемый для определения того, как ресурсы должны распределяться между подвыражениями;
В дополнение к нашему символическому исполнителю мы определяем генератор условий верификации, который позволяет полуавтоматизировать доказательства с помощью интерактивной;
Демонстрируем, что наш подход может быть реализован и доказан с помощью Coq для сверхнабора языка MC, рассмотренного в данной статье.
Модель памяти, которую представили в этой статье, была преднамеренно упрощена. В Coq модель памяти для M C дополнительно поддерживает изменяемые локальные переменные, массивы и арифметику указателей. Добавление поддержки этих функций было относительно простым и требовало только локальных изменений в семантике определения и логике разделения.
