18.02.2015: Первый публичный выпуск Astraver Toolset

Опубликовано Mikhail Mandrykin в Втр, 10/03/2015 - 09:00

Состоялся первый публичный выпуск системы верификации Astraver Toolset 1.0, построенной на базе набора инструментов дедуктивной верификации 'Frama-C + Jessie + Why3 IDE'. Инструменты были адаптированы для спецификации и доказательства свойств в коде ядра ОС Linux. Большинство наших изменений затронули встраиваемый модуль Jessie, в то время как во внешний интерфейс Frama-C и платформу Why3 были внесены лишь небольшие исправления и улучшения. Некоторые из наших изменений уже интегрированы в официальную версию инструментов, в то время как остальные доступны в наших публичных репозиториях.

Основные изменения описаны ниже.

Поддержка языка Си

  • Поддержка низкоуровневых приведений типов указателей на целочисленные типы данных. Добавление этой возможности потребовало модификации модели памяти Jessie в соответствии с описанием в статье "Расширенная высокоуровневая Си-совместимая модель памяти для промежуточного языка Jessie с ограниченной поддержкой низкоуровневого приведения типов указателей". Основная идея заключается в предоставлении пользователю возможности производить некоторые теневые перевыделения блоков памяти в явно указанных точках с целью преобразования выделенных массивов одного типа в другой.
    ВНИМАНИЕ. Поддержка различаемых объединений (union) пока еще не была полностью адаптирована для новой модели памяти.
  • Префиксное приведение типов между объемлющими структурами и структурами, вложенными в них в качестве первых полей. Реализовано при помощи встраивания полей и установление отношения наследования между структурами.
  • Поддержка функций выделения/освобождения памяти в адресном пространстве ядра (kmalloc()/kzalloc(), kfree()).
  • Встроенный в C99 тип __Bool.
  • Функции memcpy(), memmove(), memcmp() and memset() из стандартной библиотеки. Поддержка основана на использовании нескольких предопределенных шаблонных спецификаций, в которые подставляются различные конкретные типы данных.(*)
  • Указатели на функции (через полный перебор возможных алиасов). (*)
  • Функции с переменным числом параметров (через дополнительный параметр-массив). (*)
  • Ассемблерные вставки (через вызовы неопределенных функций). (*)

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

  • Функция memset() может использоваться только для инициализации памяти нулями, причем инициализация некоторых структур может быть не полной (в частности, значения массивов переменной длины после инициализации могут оставаться недетерминированными);
  • Существенно используется предположение о том, что значениями функциональных указателей могут быть только адреса каких-либо функций из анализируемого кода (как, например, в правильно зарегистрированном модуле ядра Linux). Если это предположение не выполняется, что некоторые из сгенерированных условий верификации становятся недоказуемыми.
  • Поддержка функций с переменным числом параметров может быть не полна или неудобна для их верификации (в нашем целевом коде такие функции используются только для отладочной печати и логирования и на данный момент времени по сути игнорируются).
  • Ассемблерные вставки могут либо встречаться только в недостижимом коде, либо использоваться только в целях реализации возможностей, не подлежащих верификации на текущем этапе (таких как барьеры синхронизации или атомарные блоки).

Расширения языка ACSL

  • Поддержка специфичных для Jessie конструкций \offset_min() и \offset_max().
  • Прокси-переменные для строковых литералов (с генерацией соответствующих инвариантов на содержимое).
  • Аннотация-прагма Jessie для явного указания точек переинтерпретации указателей.

Для реализации этих небольших расширений языка спецификаций ACSL были внесены изменения как во внешний интерфейс Frama-C, так и во встраиваемый модуль Jessie.

Улучшения инструмента Jessie

  • Разворачивание термов составных типов в конструкции \assigns, то есть /*@ assigns s;*/, где s имеет составной тип (структура или объединение), разворачивается в /*@ assigns s.a, s.b, s.c; */, где a, b и c -- члены составного типа. Аналогичное расширение также применяется к массивам фиксированной длины.
  • Ослабление предусловия безопасной операции сравнения указателей на равенство: теперь для обоих указателей требуется либо принадлежность к одному блоку памяти, либо валидность.
  • Усиление предусловия функции освобождения памяти (free): теперь для аргумента требуется выполнение условия \offset_min == 0.
  • Реализация функций отладочной печати для объектов, используемых во внутреннем представлении транслятора Jessie (для работы с отладчиком OCaml). Обычные функции не могут быть использованы в силу ограничения на вызовы отлаживаемого кода (по функциональным указателям), происходящие при вызовах методов объектов и приводящие к падению отладчика с ошибками сегментирования.

Исправления ошибок

  • Различные значения размера типа в коде и в спецификациях, возникающие из-за встраивания полей
  • Неполные постусловия и ограничения, соответствующие следам операций выделения/освобождения памяти.
  • Неполная трансляция конструкции allocates.
  • Трансляция assigns для глобальных переменных.
  • Лишние разыменования локальных констант.
  • Трансляция \valid(p+(a..b)), не совместимая с соответствующей ACSL-спецификацией.
  • [Frama-C] Разбор "void (*) (void)" в логических выражениях.
  • [Frama-C] typeof в применении к выражениям функционального типа (всегда давал результат типа указатель на функцию, но должен быть также совместим и с непосредственно функциональным типом, например, при объявлении функции).
  • [Frama-C] Операторы goto в сложных составных инициализаторах приводили к падениям в отладочном выводе, включенном по умолчанию (исправлено в версии Neon, но, вероятно, все равно приводит к падениям в режиме отладки).
  • [Frama-C] Позиции в исходном коде для выражений приведения типа (отсутствовали в силу функции CIL mkCast без соответствующего аргумента).
  • [Frama-C] В модифицированной версии массивы нулевого размера обрабатываются как массивы переменной длины (без указания размера), в то время как текущая реализация Cabs2Cil рассматривает нулевую длину как ошибку (не фатальную) и восстанавливается после этой ошибки, устанавливая длину массива в единицу.
  • Множество других небольших исправлений.

Масштабируемость

  • Мы также приложили некоторые усилия для улучшения применимости инструментария к очень большим программам (> 10 000 строк кода), где лишь небольшая часть кода существенно необходима для анализа (например, если объем исходного кода сильно увеличивается после раскрытия включаемых заголовочных файлов). Масштабируемость достигается за счет удаления несущественных глобальных объявлений и определений перед началом основных существенных преобразований кода, производимых встраиваемым модулем Jessie.

Рефакторинг Jessie2

  • Был сделан также некоторый рефакторинг как во встраиваемом модуле, так и в трансляторе Jessie. Больше всего были затронуты модуль Common во встраиваемом модуле Jessie и модули вывода в форматы Why/Why3 (теперь это два отдельных модуля) в трансляторе. Модифицированный инструмент Jessie использует для сборки систему Ocamlbuild, а также использует модульный алиасинг на уровне типов, реализованный в OCaml 4.02 (вместо механизма упаковки) для сборки транслятора Jessie в виде одного библиотечного модуля (Jc).

Улучшения Why3

  • Подсветка условий (различные цвета используются для подсветки условий, которые предполагаются выполненными или, соответственно, не выполненными) упрощает использование инструмента. Мы используем простую эвристическую реализацию, основанную на информации о местоположении условия в исходном коде (когда выражение логического отрицания не имеет связанной с ним информации о местоположении, но его соответствующее подвыражение под символом отрицания имеет, оно считается невыполненным условием и подсвечивается красным (или другим настраиваемым цветом),-- это позволяет лучше подсвечивать условия в операторах if, while и др.).
  • Другим относительно значительным изменением в платформе Why3 является новый критерий установления соответствия меток термов и пояснений к генерируемым условиям верификации.
    Проблема заключалась в том, что Why3 всегда использовал самую последнюю в некотором порядке метку с пояснением среди (упорядоченного) множества всех меток, поставленных в соответствие некоторому терму условия верификации. В одном из примеров для вызываемой функции было выбрано пояснение, соответствующее самой внешней конструкции let внутри этой функции, а вызывающая функция получила в итоге малоинформативное пояснение по умолчанию, которое оказалось в соответствующем ей множестве меток последним. В нашей модификации, содержимое всех меток пояснений объединяется через точку, причем самое последнее пояснение во множестве ставится на первое место (для обратной совместимости). Кроме того, предотвращается продвижение пояснений к внутренним термам функции на верхний уровень в качестве пояснений к самой функции. Также предотвращается добавление меток с пояснениями по умолчанию к множествам, в которых уже есть метки, заданные пользователем. Сделанные изменения особенно полезны для автоматически генерируемых *.mlw-файлов с множеством функций, целевых утверждений и соответствующих им пояснений.

Текущий выпуск системы верификации Astraver Toolset можно установить либо через OPAM, либо вручную собрав его из исходного кода, доступного в наших публичных репозиториях. Все изменения публикуются под теми же лицензиями, что и оригинальный код соответствующих инструментов.