ПРОГРАММИРОВАНИЕ, 2015, No 4, с. 23-39
ЯЗЫКИ И СИСТЕМЫ ПРОГРАММИРОВАНИЯ
У V 004.45
ВЫСОКОУРОВНЕВАЯ МОДЕЛЬ ПАМЯТИ ПРОМЕЖУТОЧНОГО ЯЗЫКА JESSIE С ПОДДЕРЖКОЙ ПРОИЗВОЛЬНОГО ПРИВЕДЕНИЯ ТИПОВ УКАЗАТЕЛЕЙ
© 2015 г. М.У. Мандрыкин, A.B. Хорошилов
Институт системного программирования РАН
109004 Москва, ул. А. Солженицына, 25 E-mail: khoroshilov@ispras.ru, mandrykin@ispras.ru Поступила в редакцию 25.11.2014
В статье представлен промежуточный язык, предназначенный для использования в качестве целевого анализируемого языка при верификации промышленного кода на языке GNU С (в частности, модулей ядра Linux). Язык представляет собой расширение существующего промежуточного языка, используемого подключаемым модулем jessie в системе статического анализа Frama-c. Он имеет семантику, совместимую с семантикой языка Си (в частности, для массивов), изначально поддерживает различаемые объединения и префиксные (иерархические) приведения типов указателей на структуры, и расширен ограниченной поддержкой низкоуровневого приведения типов указателей. Подходы к трансляции исходного Си-кода в промежуточный язык, а также трансляции промежуточного языка во входной язык платформы дедуктивной верификации Why3 рассматриваются на примерах. Эти примеры иллюстрируют выразительность расширенного промежуточного языка и эффективность получаемых аксиоматических спецификаций.
1. ВВЕДЕНИЕ
Существует множество подходов к статической верификации Си-программ. Среди них есть дедуктивная верификация, которая основана на переводе исходного кода на языке Си, аннотированного спецификациями проверяемых свойств, во множество логических формул, общезначимость (или невыполнимость) которых эквивалентна корректности (в смысле отсутствия нарушений спецификации) исходной программы в соответствии с заданными свойствами. Эти логические формулы, также известные как условия верификации (УВ, англ. vérification conditions (VCs), а также proof obligations) могут быть проверены на выполнимость (разрешены) с помощью различных инструментов. Эти инструменты могут быть автоматическими, такими как
* Исследование проводилось при финансовой поддержке Министерства образования и науки Российской федерации (уникальный идентификатор проекта — RFMEFI60414X0051).
SAT- и SMT-решатели [1, 2| (Z3, CVC3, CVC4, Alt-Ergo и др.), а также доказатели теорем на основе обобщенного резолютивного вывода (Vampire, E-Prover и др.), или требующими участия со стороны пользователя, такими как интерактивные средства доказательства теорем Coq и pvs.
Таким образом, любой инструмент дедуктивной верификации для языка Си, целью которого служит максимальная автоматизация проверки заданных спецификаций, должен каким-либо образом преобразовывать семантику исходного аннотированного кода во множество УВ, которые способны разрешать современные автоматические инструменты проверки выполнимости.
В то же время основные свойства языка Си существенно усложняют подобное преобразование. Во-первых, Си — это императивный язык программирования, и, как следствие, неявное состояние Си-программы должно каким-либо образом моделироваться в получаемых логических
формулах. Его можно моделировать несколькими способами, которые обычно так или иначе предполагают использование теории массивов для представления состояния памяти программы. Во-вторых, Си предполагает ручное управление памятью, что требует генерации дополнительных проверок условий корректности, связанных с возможными ошибками управления памятью (преждевременное очищение, мусор, обращение за пределы выделенной памяти). В третьих, Си это низкоуровневый язык программирования, имеющий в общем случае нетипи-зированную семантику, что может существенно влиять на выбор подходящей модели памяти.
Рассмотрим очень простой пример аннотированного фрагмента Си-ирограммы (рис. 1):
с11 4 I , с I 4 I ;
1 1 Г11 *а , *Ь
2 с Наг с | 4 | ;
3 1 Г11 п, 111;
4
5 а ^ е ;
6 ь - а ;
7 ЬМ - 1;
8 с1 ш - 2; _
9 с[1] ^ ' а '
10 аззсгЧ
а[п] =
Рис. 1. Пример аннотированного фрагмента Си-программы.
Предположим, что требуется получить УВ для проверки условия а[п] = 1 в строке 10. Наиболее прямолинейным и одновременно точным решением будет использование для построения соответствующей логической формулы низкоуровневой модели, в которой каждая ячейка памяти программы представлена некоторым количеством последовательных индексов в одном общем логическом байтовом (8-битном) массиве М, индексированном, например, 32-битными адресами. Логические массивы [2| (те, с которыми работают БЫТ-решатели) это тотальные отображения из значений типа индекса массива в значения типа элемента массива, для которых определена тернарная операция обновления ■ [■ <— ] без побочных эффектов для троек (массив, индекс, значение), которая для указанного массива возвращает новый логический массив того же типа, отличающийся от исходного тем и только тем, что он отображает указанный
индекс в указанное новое значение (то есть для остальных индексов значения остаются без изменения). В логических формулах задаются только ограничения на значения массивов по некоторым индексам, изначально значения элементов массивов считаются неопределенными (недетерминированными). Взятие значения элемента массива М по индексу г будем обозначать через М [г]. Для обозначения изменений массива М в результате выполнения операций записи в память будем использовать (конечную) последовательность логических массивов М1, М2,..., Мп. Пусть адреса неременных а, Ь, с, с1, е, 11 и ш, представлены неинтерпретируемыми константами 32-битными векторами а, Ь С а е, п и ш. Тогда соответствующее УВ в низкоуровневой модели памяти запишется в виде:
М1 = М0[а ^ М0[е]]л М2 = М1[Ь ^ М1[а]]л
М3 = М2 [М2 [6] +32 М2 [п] ^ 08] л М4 = Мз[Мз[6] +32 Мз[п] +32 132 ^ 08] л М5 = М4 [М4 [6] +32 М4[п] +32 232 ^ 08] л Мб = М5 [М5[6] +32 М5[п] +32 332 ^ 18] л
М7 = М2 [Мб И +32 Мб[ш] ^ 08] л ... л М10 = М5 [М9 [¿] +32 М9 [ш] + 332 ^ 28] л
М11 = М1о[Мю[е] ^ 97] л
(6 < а — 4 v 6 > а + 4) л ... л "i
(е < а — 16 v е > а + 4) л ... л>42 неравенства
(е < а — 16 v е > а +16)
Низкоуровневая модель позволяет моделировать семантику Си-программ с очень высокой побитовой точностью, в перспективе (при еще более точном моделировании памяти, например с учетом регистров и кэшей) достигая практически полного соответствия модели реальному выполнению программы на какой-либо физической машине. Логические формулы, использующие одновременно теории массивов и битовых векторов, в значительном числе случаев поддаются разрешению с помощью современных автоматических инструментов проверки выполнимости (БЫТ-решателей), хотя существующие алгоритмы для теории массивов в общем случае не полны [2| (то есть соответствующие инструменты могут завершаться, не выдавая вердикт
выполни,мо / невыполнимо или вовсе не завершаться). Однако даже на приведенном простейшем примере видно, что логические формулы, построенные в низкоуровневой модели памяти, весьма избыточны и неоптимальны. На практике такая модель памяти плохо масштабируется и не используется в инструментах дедуктивной верификации в изначальном виде — при построении формул всегда применяются некоторые существенные оптимизации.
1.1. Существующая модель памяти Jessie
Здесь следует упомянуть, что в данной статье речь идет только о построении логических формул в классической логике первого порядка с равенством и с использованием некоторых теорий (таких как теории массивов, неинтер-претируемых функций, битовых векторов и линейной вещественной или целочисленной арифметики), то есть так называемых SMT-формул (от англ. Satisfiability Modulo Theories). Альтернативные техники, в первую очередь, основанные на использовании различных модификаций логики разделения (англ. separation logic) [3], отличаются, в целом, менее развитой поддержкой со стороны инструментов автоматического разрешения задач выполнимости соответствующих формул и, соответственно, обычно требуют существенно большего участия со стороны пользователя при проверке получаемых УВ. В области автоматизированной дедуктивной верификации техники, основанные на построении SMT-формул, остаются наиболее часто используемыми на практике, в частности, в инструментах ESC/Java [4], Spec# [5], VCC [6], Frama-С/Jessie [7, 8], Frama-C/WP [71 и др.
Первая, наиболее распространенная и очевидная оптимизация, используемая при построении SMT-формул — это выделение в исходной Си-программе так называемых чистых переменных, то есть переменных простых (не составных) типов данных, обращение к которым может происходить только по их именам, в отличие от общего случая, когда обращение к переменной может происходить также, например, по указателю, содержащему адрес этой переменной. В частности, в качестве чистых переменных часто рассматриваются переменные, для которых в
исходном коде отсутствуют операции взятия адреса (&). Такое предположение является надежным при условии того, что для исходной программы каким-либо образом доказана корректность работы с памятью (в частности, отсутствие обращений за границы выделенных областей). Так как обращение к чистым переменным может происходить только по их именам, обращения к каждой чистой переменной можно легко статически отделить от обращений как к другим чистым переменным, так и к другим объектам в памяти программы. Поэтому для каждой чистой переменной вместо индекса (адреса) в последовательности массивов M1,..., Mn можно использовать отдельную последовательность переменных vi,v2,.. .Vk- Одна только эта оптимизация позволяет уменьшить число неравенств (задающих непересечение (разделение) различных объектов в памяти) в приведенном примере формулы с 42 до 6, а также уменьшить число переменных в по-
M1 , . . . , Mn
с 11 до 9.
Идею отделения некоторых индексов из обще-M
менных, можно обобщить на произвольные априорно (с точностью до некоторой статической аппроксимации) разделенные области памяти. Для этого можно выделить набор непересекающихся множеств объектов в памяти, таких, что для любого указателя в любой точке программы гарантированно можно указать то единственное множество об
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.