Установка Frama-C с последней версией плагина дедуктивной верификации Jessie (AstraVer)

Здесь я расскажу о том, как установить актуальный стек инструментов дедуктивной верификации AstraVer. По сравнению с официальной инструкцией я подробнее распишу что к чему, и приведу команды для установки дополнительных инструментов, которые я так или иначе буду стараться затрагивать в других постах. Процесс установки описывается для Linux систем. Инструменты также работают и на других операционных системах. Здесь я дам небольшие комментарии по поводу установки инструментов на Windows и Mac OS X, касающиеся отличий в процессе установки от Linux систем.

Для начала о самих инструментах. Будут использоваться форк плагина дедуктивной верификации Jessie от команды AstraVer, фреймворк для анализа кода на языке Си Frama-C, среда для работы с солверами Why3.
Разработчики оригинального плагина Jessie перестали его развивать и переключились на инструменты для языка Ada. В нынешнем виде его трудно установить и запустить, приходится это делать вручную с кучей старых зависимостей. Astraver - это отдельный форк Jessie. В форке были исправлены многие проблемы его родителя, существенно упрощён процесс установки и введены дополнительные возможности.
Как следует из последней ссылки, на текущий момент в синтаксис языка ACSL внесены небольшие изменения для того, чтобы было возможно смоделировать на уровне спецификаций некоторые операции в коде. Это привело к тому, что потребовалось менять код парсера спецификаций. Так как этим занимается фронтенд Frama-C, то было сделано ответвление от него с ограниченным набором изменений. Инструментарий от AstraVer не способен работать с официальной версией Frama-C и использует свою версию, которая, не ломая обратной совместимости, поддерживает парсинг расширенных конструкций ACSL.
Модифицированная версия Frama-C с некоторым запозданием синхронизируется с официальной версией Frama-C. Тем не менее, возможно держать две версии Frama-C в системе, о чем я расскажу в данном посте.

Установка всех инструментов будет осуществляться через opam. Это пакетный менеджер языка ocaml.


Оглавление

  1. Готовая ВМ с инструментами
  2. Установка OPAM
  3. Настройка OPAM
  4. Установка инструментов
  5. Windows
  6. MAC OS X
  7. Обновление инструментов
  8. Две версии Frama-C в системе

Виртуальная машина с инструментами

По ссылке можно загрузить образ виртуальной машины VirtualBox в формате ova с уже с предустановленными и настроенными инструментами. Размер образа ~3.6 гигабайт. Ос - Ubuntu. Логин - user. Пароль - 1. Виртуальная машина время от времени обновляется.
В директории workspace находятся два репозитория для того, чтобы можно было сразу запустить инструменты на каком-то коде. Один репозиторий содержит спецификации к реальным функциям, а второй - к обучающим примерам.

Установка opam

Как установить opam рассказывается на странице его документации. Если вкратце, то:

# Debian/Ubuntu
$ apt-get install opam

# Arch Linux
$ yaourt -S opam

# From source
$ wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh
$ chmod +x opam_installer.sh
$ sudo ./opam_installer.sh /usr/local/bin

Opam может использовать солвер aspcud для разрешения пакетных зависимостей. Основываясь на собственном опыте, могу твёрдо сказать что без него opam может очень криво выполнять обновления установленных пакетов.
При установке opam в Debian/Ubuntu aspcud будет автоматически устанавливаться. К сожалению, в других системах это не так. Как установить aspcud на Fedora Linux можно посмотреть по ссылке. В принципе, действия аналогичны на любой системе. Посмотреть всё же рекомендую, потому что там есть одна неприятная особенность, связанная с запуском из текущей рабочей директорией (относительными путями к солверу).

Настройка opam

Нужно установить компилятор ocaml. Также нужно добавить репозиторий пакетов от astraver.
Лучше не использовать системный компилятор, потому что часть инструментов и библиотек ocaml собираются не всеми версиями компилятора. К тому же, ситуация, когда часть пакетов установлены системой, а другая часть через opam, ведёт к рассинхронизации. Из моего опыта, у Ocaml есть большие проблемы с бинарной совместимостью и чуть-что, сразу нужно пересобирать пакеты.

# версия компилятора
$ opam init --comp 4.04.2
# локальные пути для установки пакетов для текущей сессии терминала
$ eval `opam config env`
# добавить репозиторий под именем astraver
$ opam repo add astraver https://forge.ispras.ru/git/astraver.opam-repository.git

Установка инструментов

У opam есть хороший плагин depext. Рекомендую сразу установить его. Он автоматически выявляется системные зависимости для установки ocaml пакетов и сильно облегчает жизнь.

# Установка depext
opam depext

Далее нам понадобятся:

  • frama-c - собственно, фреймворк для анализа кода на на языке Си.
  • jessie2 - плагин дедуктивной верификации для Frama-C от AstraVer.
  • why3 - среда для запуска солверов и интеграции результатов их работы.
  • alt-ergo - солвер, его удобно установить через opam.
  • altgr-ergo - графический интерфейс к солверу alt-ergo. Помогает посмотреть, какие утверждения солвер использует при доказательстве условий верификации.
  • satML-plugin - пакет содержит файл подсветки для ACSL синтаксиса.

Дополнительно:

  • coq - интерактивный доказатель теорем. Может вызываться из Why3 для ручного доказательства/анализа условий верификации. Устанавливается довольно долго. Если вы только знакомитесь со средствами, то он вам, определённо, не нужен. При установке требует пересборки jessie2 и why3.
  • coqide - интерактивная среда к Coq.

Итак:

# depext --install устанавливает системные зависимости,
#  а затем пакеты через opam

# Если нужен Coq, то сначала:
#opam depext --install coq coqide

# Установка основных пакетов
$ opam depext --install jessie2 frama-c why3

# установка солвера alt-ergo с плагином подсветки и интерактивной оболочки
$ opam depext --install alt-ergo altgr-ergo satML-plugin

Из системных пакетов рекомендуется установить солверы:

  • CVC4 - доказывает многое из того, с чем не справляется Alt-Ergo.
  • Z3 - в отдельных случаях может доказать условие верификации, с которым не справились остальные солверы. В остальных случаях работает хуже.
  • Eprover - пару раз его эвристики находили противоречия в спецификациях, где остальные солверы ничего не доказывали. Строго говоря, этот солвер не нужен. И я бы не стал заморачиваться с его установкой, если он не входит в пакетную базу дистрибутива.

Важно понимать, что характеристики, которые я дал солверам, применимы только к моделям и условиями верификации, генерируемым Jessie2.

# Fedora Linux
$ dnf install z3 cvc4
# Arch Linux
$ yaourt -S z3 cvc4 eprover
# Debian/Ubuntu
$ apt install z3 cvc4
...

Последним шагом, нужно сконфигурировать Why3. Он должен найти солверы в системе и определить их версии:

$ why3 config --detect-provers --detect-plugins

Теперь можно протестировать, что все инструменты установились и работают корректно:

# Однострочная функция
$ echo -e '/*@ assigns \\nothing;*/\nint avg(int a, int b) { return (a + b) / 2; }' > test.c
# Запуск инструментов дедуктивной верификации
$ frama-c -jessie test.c

Результат может быть увиден на картинке:

Windows

Отличия в процессе установки на Windows затрагивают только установку opam и системных солверов.

Нужно установить opam c этого сайта. Он одновременно установит CygWin. Далее нужно запустить Cygwin64 Terminal из меню Пуск.

Далее инициализация opam:

$ opam init --comp 4.04.2+mingw64
$ opam depext
# Бекенд для opam для установки системных пакетов через Cygwin
$ opam install depext-cygwinports

Последняя команда скорее всего выведет сообщение о том, что нужно добавить в переменную PATH путь к компилятору. Что-то вроде такого: /usr/i686-w64-mingw32/sys-root/mingw/bin Соответственно, это нужно сделать.

Также нужно не забыть добавить репозиторий astraver:

$ opam repo add astraver https://forge.ispras.ru/git/astraver.opam-repository.git

Установка же самих инструментов происходит так же, как и на Linux системах (через opam depext --install).

Солверы, кроме Alt-Ergo, надо устанавливать вручную. Скачивать бинарники с сайтов (Z3, CVC4), устанавливать, добавлять путь к ним в PATH. Последним шагом делать why3 --detect.

Mac OS X

Отличия в процессе установки на OS X затрагивают только установку opam и системных солверов.

Установить opam на OSX можно следующим образом:

$ brew install opam
$ eval `opam config env` # Нужно добавить в .bashrc
$ opam init --comp 4.04.2
# добавить репозиторий под именем astraver
$ opam repo add astraver https://forge.ispras.ru/git/astraver.opam-repository.git

Установка самих инструментов происходит так же, как и на Linux системах (через opam depext --install).

Установка системных солверов перед (why3 config):

$ brew tap homebrew/boneyard
$ brew install cvc4
$ brew install z3

Обновление инструментов

Обновлять пакеты через opam довольно легко. Для этого требуются две стандартные команды:

$ opam update
$ opam upgrade

Если обновились версии солверов, то необходимо перезапустить конфигурацию why3:

$ why3 config --detect-provers --detect-plugins

Две версии Frama-C в системе

Как уже упомяналось в начале, frama-c AstraVer версии отстаёт от официальной. Стандартная версия frama-c находится в пакете frama-c-base. Нельзя одновременно установить два пакета frama-c и frama-c-base. Однако, у opam есть возможность создавать несколько "окружений" и переключаться между ними.
Соответственно, можно создать новое окружение таким образом:

# Создать окружение orig с компилятором версии 4.04.2
$ opam switch orig -A 4.04.2
# Обновить переменные окружения
$ eval `opam config env`
# Установить оригинальную версию frama-c
$ opam install frama-c-base

Переключаться между окружениями можно через команду switch:

# назад к jessie
$ opam switch 4.04.2
$ eval `opam config env`

# обратно к оригинальной frama-c
$ opam switch orig
$ eval `opam config env`

Comments

comments powered by Disqus