seahorn
v0.1.0 Release (SV-COMP'16)
Seahorn-это автоматизированная структура анализа для языков на основе LLVM. Эта версия собирает против LLVM 14.
Некоторые из поддерживаемых функций
Seahorn разрабатывается в основном как основа для проведения исследований в области автоматической проверки. Фреймворки предоставляют много компонентов, которые можно собрать вместе различными способами. Тем не менее, это не «вне коробки» статический инструмент анализа.
Многие инструменты анализа и примеры предоставляются в рамках. Мы постоянно ищем новые приложения и оказываем поддержку новым пользователям. Для получения дополнительной информации о том, что происходит, проверьте наш (редко обновленный) блог.
Seahorn распространяется по модифицированной лицензии BSD. См. License.txt для деталей.
Seahorn предоставляет сценарий Python под названием sea для взаимодействия с пользователями. Учитывая программу C, аннотированную с утверждениями, пользователям просто нужно ввести: sea pf file.c
Результат sea-pf является unsat если все утверждения проходят, sat , если какое-либо из утверждений нарушено.
Опция pf сообщает Seahorn для перевода file.c в биткод LLVM, генерировать набор условий проверки (VCS) и, наконец, решить их. Основным мощным решателем является проставка.
Команда pf предоставляет, среди прочего, следующие варианты:
--show-invars : отображать вычисленные инварианты, если ответ был unsat .
--cex=FILE : хранит контр-пример в FILE , если ответ был sat .
-g : компилируется с информацией отладки для более отслеживаемых контрпримеров.
--step=large : большой шаг кодирование. Каждое соотношение перехода соответствует фрагментам без петли.
--step=small : Кодирование мелкого шага. Каждое отношение перехода соответствует основному блоку.
--track=reg : model (целое число) только регистры.
--track=ptr : модель регистров и указателей (но не содержание памяти)
--track=mem : моделировать как скаляры, указатели и содержимое памяти
--inline : внедрять программу перед проверкой
--crab : инварианты инъекции в spacer , генерируемый инструментом, основанным на крабе, на основе абстрактной интерпретации. Прочитайте здесь для получения подробной информации обо всех вариантах краба (Prefix --crab ). Вы можете увидеть, какие инварианты выводятся Crab путем ввода опции --log=crab .
--bmc : используйте двигатель BMC.
sea pf - это трубопровод, который запускает несколько команд. Отдельные части трубопровода могут также работать отдельно:
sea fe file.c -o file.bc : Seahorn Frontend переводит программу C в оптимизированный бит -код LLVM, включая преобразование смешанного соэлемы.
sea horn file.bc -o file.smt2 : Seahorn генерирует условия проверки из file.bc и выводит их в формат smt -lib v2. Пользователи могут выбирать между различными стилями кодирования с несколькими уровнями точности, добавив:
--step={small,large,fsmall,flarge} , где small кодирование маленького шага, large кодирование с большим блоком, fsmall -это маленький шаг, кодирующий, производящие положения плоского рога (то есть он генерирует переходную систему только с одним предикатом), и flarge : кодирование с плоским рогом, производящим плоского рога.
--track={reg,ptr,mem} , где модели reg только для моделей Scalars, модели ptr reg и адреса указателя и модели mem ptr и содержимое памяти.
sea smt file.c -o file.smt2 : генерирует CHC в формате SMT -LIB2. Это псевдоним для sea fe за которым следует sea horn . Командование sea pf -псевдоним для sea smt --prove .
sea clp file.c -o file.clp : генерирует CHC в формате CLP.
sea lfe file.c -o file.ll : Запуск Legacy Front -End
Чтобы увидеть все команды, введите sea --help . Чтобы увидеть параметры для каждой отдельной команды cmd (например, horn ), типа sea CMD --help (например, sea horn --help ).
Seahorn не использует краб по умолчанию. Чтобы включить крабов, добавьте опцию --crab в команду sea .
Абстрактный интерпретатор по умолчанию внутрипроцедурально и использует зоны домена в качестве численной абстрактной области. Этих параметров по умолчанию должны быть достаточно для обычных пользователей. Для разработчиков, если вы хотите использовать другие абстрактные домены, которые вам нужно:
cmake -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea с опцией --crab-dom=DOM , где DOM может быть:int для интерваловterm-int для интервалов с неинтерпретированными функциямиboxes : для дизъюнктивных интерваловoct для октябряpk для Polyehdra Для использования межпроцедурного анализа краба вам нужно запустить sea с опцией --crab-inter
По умолчанию абстрактный интерпретатор только причинах скалярных переменных (т.е. регистры LLVM). Запустите sea с опциями --crab-track=mem --crab-singleton-aliases=true для разума о содержании памяти.
Крб в основном нечувствителен к пути, в то время как Spacer, наш решатель оговорки, чувствителен к пути. Хотя нечувствительные к пути анализы более эффективны, чувствительность пути обычно требуется для доказывания интересующего свойства. Это мотивирует наше решение о запуске первого краба (if Option --crab ), а затем передает сгенерированные инварианты Spacer. В настоящее время есть два способа для Spacer использовать инварианты, сгенерированные Crab. Опция sea --horn-use-invs=VAL сообщает spacer , как использовать эти инварианты:
VAL равен bg , то инварианты используются только для того, чтобы помочь spacer в доказательстве, что лемма индуктивна.VAL always равен, то поведение похоже на bg , но, кроме того, инварианты также используются, чтобы помочь spacer блокировать контрпример. Значение по умолчанию - bg . Конечно, если краб может доказать, что программа безопасна, то Spacer не несет никакой дополнительной стоимости.
Предполагается, что свойства являются утверждениями. Seahorn предоставляет статическую команду утверждения sassert , как показано в следующем примере
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();
int main ( void ) {
int k = 1 ;
int i = 1 ;
int j = 0 ;
int n = nd ();
while ( i < n ) {
j = 0 ;
while ( j < i ) {
k += ( i - j );
j ++ ;
}
i ++ ;
}
sassert ( k >= n );
} Внутренне, Seahorn следует за SV-Comp Comply, посредством расположения ошибок кодирования при вызове обозначенной функции ошибки __VERIFIER_error() . Seahorn возвращается unsat , когда __VERIFIER_error() недоступен, и программа считается безопасной. Seahorn возвращает sat , когда __VERIFIER_error() доступна, а программа небезопасна. Метод sassert() определен в seahorn/seahorn.h .
Помимо доказывания свойств или создания контрприменов, иногда полезно осмотреть анализ кода, чтобы получить представление о его сложности. Для этого Seahorn обеспечивает командование sea inspect . Например, с учетом программы C ex.c тип:
sea inspect ex.c --sea-dsa=cs+t --mem-dot
Опция --sea-dsa=cs+t позволяет новый анализ контекста, чувствительного к типу SEA-DSA, описанный в FMCAD19. Эта команда генерирует файл FUN.mem.dot для каждой функции FUN в программе ввода. Чтобы визуализировать график основной функции, используйте интерфейс Web Graphivz или следующие команды:
$ dot -Tpdf main.mem.dot -o main.mem.pdfБолее подробная информация о графах памяти находится в репозитории Seadsa: здесь.
Используйте sea inspect --help чтобы увидеть все варианты. В настоящее время доступные варианты:
sea inspect --profiler печатает количество функций, основных блоков, петлей и т. Д.sea inspect --mem-callgraph-dot Prints для dot формата графа вызовов, построенного Seadsa.sea inspect --mem-callgraph-stats отпечатывает для стандартного вывода.sea inspect --mem-smc-stats печатает количество доступа к памяти, которое может быть оказано безопасным Seadsa.Самый простой способ начать работу с Сихорном - это распределение Docker.
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly Начните с изучения того, что может сделать команда sea :
$ sea --help
$ sea pf --help nightly тег автоматически обновляется ежедневно и содержит новейшую версию разработки. Мы поддерживаем все остальные теги (которые требуют ручного обновления) редко. Проверьте даты на Dockerhub и зарегистрируйте проблему на GitHub, если они слишком устарели.
Дополнительные примеры и параметры конфигурации находятся в блоге. Блог обновляется нечасто. В частности, изменение опций, функции вытекают, добавляются новые вещи. Если вы находите проблемы в блоге, сообщите нам. Мы, по крайней мере, обновим сообщение в блоге, чтобы указать, что он не будет работать с последней версией кода.
Вы также можете вручную установить по:
Следуя инструкциям в файле Docker DockerFile: docker/seahorn-builder.Dockerfile .
Если это не работает, беги:
$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *Первые 3 команды установит LLVM 14, 4th установит Libpolly, которая ошибочно опущена из LLVM 14 (но включена в последующие версии)
Далее следуйте инструкции в файле Docker выше
Информация с этого момента предназначена только для разработчиков. Если вы хотите внести свой вклад в Seahorn, создайте свои собственные инструменты на основе его или просто заинтересованы в том, как он работает внутри, продолжайте читать.
Seahorn требует LLVM, Z3 и Boost. Точные версии библиотек продолжают меняться, но Cmake Craft используется для проверки этой правильной версии.
Чтобы указать конкретную версию любой из зависимостей, используйте обычную <PackageName>_ROOT и/или <PackageName>_DIR (для подробностей find_package ()).
Seahorn разбит на несколько компонентов, которые живут в разных репозиториях (под организацией Seahorn). Процесс сборки автоматически проверяет все по мере необходимости. Для текущих инструкций по сборке проверьте сценарии CI.
Это общие шаги. Не используйте их. Читайте дальше для лучшего способа:
cd seahorn ; mkdir build ; cd build (каталог сборки также может быть за пределами исходного каталога.)cmake -DCMAKE_INSTALL_PREFIX=run ../ (установка требуется! )cmake --build . --target extra && cmake .. (Клоны, которые живут в другом месте)cmake --build . --target crab && cmake .. (Clones Crab Library)cmake --build . --target install (создайте и установите все под run )cmake --build . --target test-all (Run Tests)Примечание . Установка Target требуется для работы тестов!
Для улучшенного опыта разработки:
clanglld -линкерcompile_commands.json На Linux мы предлагаем следующую конфигурацию cmake :
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run
-DCMAKE_BUILD_TYPE=RelWithDebInfo
-DCMAKE_CXX_COMPILER="clang++-14"
-DCMAKE_C_COMPILER="clang-14"
-DSEA_ENABLE_LLD=ON
-DCMAKE_EXPORT_COMPILE_COMMANDS=1
../
-DZ3_ROOT=<Z3_ROOT>
-DLLVM_DIR=<LLMV_CMAKE_DIR>
-GNinja
$ (cd .. && ln -sf build/compile_commands.json .)
где <Z3_ROOT - это каталог, содержащий двоичное распределение Z3, а LLMV_CMAKE_DIR - это каталог, содержащий LLVMConfig.cmake .
Другими юридическими вариантами для CMAKE_BUILD_TYPE являются Debug и Coverage . Обратите внимание, что CMAKE_BUILD_TYPE должен быть совместим с тем, что используется для компиляции LLVM . В частности, вам понадобится Debug сборка LLVM для компиляции SeaHorn в режиме отладки **. Убедитесь, что у вас достаточно терпения, дискового пространства и времени, если вы решите пойти по этому пути.
В качестве альтернативы, проект может быть настроен с использованием пресетов Cmake. Для этого просто запустите следующую команду:
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > Для настройки Cmake, где <BUILD_TYPE> - это один из: Debug , RelWithDebInfo или Coverage и <PRESET_NAME> - это предустановка, которую вы хотели бы использовать. Предузатели, которые в настоящее время доступны: jammy . Эти предустановки предполагают, что у вас установлен Z3 в /opt/z3-4.8.9 , а YIES установлен в /opt/yices-2.6.1 .
Это также позволит конфигурировать и составить проект в коде VS, используя расширение инструментов Cmake.
Если вы хотите использовать различные настройки компиляции или если у вас установлен Z3 или Yeces в любом другом каталоге, вам нужно будет сделать свой собственный файл CMakeUserPresets.json с собственными пресетами.
Не включайте -DSEA_ENABLE_LLD=ON . Компилятор по умолчанию - Clang, поэтому вам может не понадобиться его явно.
Seahorn предоставляет несколько компонентов, которые автоматически клонируются и установлены через extra цель. Эти компоненты могут использоваться другими проектами за пределами Сихорна.
SEA-DSA: git clone https://github.com/seahorn/sea-dsa.git
sea-dsa -это новый анализ кучи на основе DSA. В отличие от llvm-dsa , sea-dsa зависит от контекста, и, следовательно, более тонкозернистого разделения кучи может быть получено при наличии функциональных вызовов.
Clam: git clone https://github.com/seahorn/crab-llvm.git
clam обеспечивает индуктивные инварианты, используя методы абстрактной интерпретации для остальных бэкэндов Сихорна.
llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn обеспечивает адаптированные версии InstCombine и IndVarSimplify LLVM, а также проход LLVM для преобразования неопределенных значений в непермерминированные вызовы, среди прочего.
Seahorn не поставляется со своей собственной версией Clang и рассчитывает найти его либо в каталоге сборки ( run/bin ), либо по пути. Убедитесь, что версия Clang соответствует версии LLVM, которая использовалась для компиляции Seahorn (в настоящее время LLVM14). Самый простой способ предоставить правильную версию Clang - это загрузить его с LLVM.org, не считать его где -то и создать символическую ссылку на clang и clang++ в run/bin .
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ где <CLANG_ROOT> это место, в котором Кланг был распакован.
Инфраструктура тестирования зависит от нескольких пакетов Python. У них есть свои зависимости. Если вы не можете их выяснить, вместо этого используйте Docker.
$ pip install lit OutputCheck networkx pygraphviz Мы можем использовать gcov и lcov , чтобы генерировать информацию о покрытии тестирования для Seahorn. Чтобы построить с включенным покрытием, нам нужно запустить сборку под другим каталогом и установить CMAKE_BUILD_TYPE для Coverage во время конфигурации CMAKE.
Примеры шагов для создания отчета о покрытии для цели test-opsem :
mkdir coverage; cd coverage Каталог mkdir coverage; cd coverage Создайте и введите охват.cmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem запустить тесты Opsem, теперь файлы .gcda и .gcno должны быть созданы в соответствующих каталогах CMakeFileslcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info Соберите данные покрытия из желаемого модуля, если clang используется в качестве компилятора вместо gcc , создайте Bash Script llvm-gcov.sh : #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh Затем приложение --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh в команду lcov -c ... 6. Извлеките данные из желаемых каталогов и генерируйте отчет HTML:
lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report Затем Open coverage_report/index.html в браузере, чтобы просмотреть отчет о покрытии
Также см. scripts/coverage для сценариев, используемых CI. Отчет о покрытии для ночных сборок доступен в Codecov
База данных компиляции для проекта Seahorn и всех его субпроектов генерируется с использованием -DCMAKE_EXPORT_COMPILE_COMMANDS=ON опция для cmake .
Простой способ получить индексацию кода для работы с поддержкой базы данных компиляции - это связать файл compilation_database.json в основной каталог проекта и следить за инструкциями, специфичными для вашего редактора.
lsp-ui с clangd , которые доступны в Spacemacs Разработка филиала Для подробного руководства для удаленного рабочего процесса с Clion Check Clion-конфигурацией.
Используйте нашу вилку мейнфрамера. Не пропустите пример конфигурации.
