crab

Краб: библиотека C ++ для строительных программ Статический анализ

Crab - это библиотека C ++ для строительных программ статического анализа, основанного на абстрактной интерпретации. Crab предоставляет богатый набор абстрактных доменов, решателей Fixpoint на основе Kleene, а также различные анализы, такие как DataFlow, межпроцедуральный и обратный. Дизайн краба довольно модульный, так что легко подключать новые абстрактные домены и решатели или создавать новые анализы.

Абстрактные домены краба могут рассуждать о содержании памяти, C-подобных массивах и числовых свойствах. Crab использует эффективные реализации популярных численных доменов, таких как зоны и октагоны и новые области, для разумного, например, о символических терминах (он же неинтерпретированные функции). Crab также реализует популярные нереляционные домены, такие как интервал или согласованности с использованием эффективных карт окружающей среды, и позволяет комбинацию произвольных доменов посредством стандартных построенных конструкций продукта. Crab также предоставляет невыпуктные домены, такие как специализированные дизъюнктивные интервалы, называемые коробками, основанными на линейных диаграммах принятия решений, и более общая стратегия разделения стоимости, которая поднимает произвольную область до чрезмерного приспособления его завершения дизъюнкции. В дополнение к этим областям, все разработанные авторами крабов, библиотека крабов объединяет популярные библиотеки абстрактных доменов, такие как Apron, Elina и Pplite.

Crab обеспечивает современный решатель Fixpoint, который использует слабый топологический порядок Bourdoncle, чтобы выбрать набор точек расширения. Чтобы смягчить точные потери во время расширения, краб реализует некоторые популярные методы, такие как расширение с порогами и расширение Lookahead.

Crab предоставляет две различные реализации межпроцедурного анализа: нисходящий вниз с межпроцедурным анализом Memoization с поддержкой рекурсивных вызовов и гибридом анализа снизу вверх + сверху вниз. И последнее, но не менее важное, Краб также реализует более экспериментальный обратный анализ, который можно использовать для вычисления необходимых предварительных условий и/или уменьшения количества ложных тревог.

Crab не анализирует непосредственно основной язык программирования, но вместо этого он анализирует свое собственное промежуточное представление на основе CFG под названием Crabir. Crabir-это код с тремя адресами, и он сильно напечатан. В Crabir управляющий поток определяется нетерминированными инструкциями GOTO. Помимо стандартных логических и арифметических операций, Crabir предоставляет особые заявления и утверждение. Первый может использоваться для уточнения потока управления, а последний предоставляет простой механишм для проверки пользовательских свойств. Несмотря на свой простой дизайн, Crabir достаточно богат, чтобы представлять такие языки, как LLVM.

Краб активно находится в стадии разработки. Если вы найдете ошибку, откройте проблему GitHub. Запросы на вытягивание с новыми функциями очень приветствуются. Доступную документацию можно найти в нашей вики. Если вы используете эту библиотеку, пожалуйста, укажите эту статью.

Окна	Ubuntu	OS X.	Покрытие
TBD		TBD

Докер

(Ночная) предварительно построенная версия краба, которая запускает все тесты, можно получить с помощью Docker:

docker pull seahorn/crab:bionic
docker run -v ` pwd ` :/host -it seahorn/crab:bionic

Требования

Краб написан в C ++ и полагается на библиотеку Boost. Основные требования:

• C ++ 11 компилятор
• Boost> = 1,65
• GMP
• Mpfr (if -DCRAB_USE_APRON=ON или -DCRAB_USE_ELINA=ON )
• Flint (только если -DCRAB_USE_PPLITE=ON )

В Linux вы можете установить требования, набирающие команды:

 sudo apt-get install libboost-all-dev libboost-program-options-dev
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev	
sudo apt-get install libflint-dev

Компиляция и установка

Чтобы установить краб, введите:

 1. mkdir build && cd build
 2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
 3. cmake --build . --target install 

Каталог tests содержит много примеров того, как создавать программы, написанные в Crabir, и вычислить инварианты с использованием различных анализов и абстрактных областей. Чтобы скомпилировать эти тесты добавить опцию -DCRAB_ENABLE_TESTS=ON Line 2.

и затем, например, запустить test1 :

 build/test-bin/test1

Включите сторонние библиотеки абстрактных доменов

Домены коробок/фартук/Elina/pplite требуют сторонних библиотек. Чтобы избежать бремени для пользователей, которые не заинтересованы в этих доменах, установка библиотек не является обязательной.

• Если вы хотите использовать домен полетов, добавьте -DCRAB_USE_LDD=ON option.

• Если вы хотите использовать домены библиотеки фартука, добавьте -DCRAB_USE_APRON=ON опция.

• Если вы хотите использовать домены библиотеки Elina, добавьте -DCRAB_USE_ELINA=ON опцию.

• Если вы хотите использовать домены библиотеки Pplite, добавьте -DCRAB_USE_PPLITE=ON option.

ВАЖНО: Фартук и Элина в настоящее время не совместимы, поэтому вы не можете включить -DCRAB_USE_APRON=ON и -DCRAB_USE_ELINA=ON в то же время.

Например, чтобы установить краб с коробками и фартуком, тип:

 1. mkdir build && cd build
 2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
 3. cmake --build . --target ldd && cmake ..
 4. cmake --build . --target apron && cmake ..	
 5. cmake --build . --target install 	

Строки 3 и 4 будут загружать, компилировать и установить коробки и домены фартука соответственно. Замените apron в строке 4 на elina или pplite , если вы хотите использовать Elina или Pplite. Если вы уже собрали и установили эти библиотеки в своем компьютере, пропустите команды в строке 3 и 4 и добавьте следующие параметры в строке 2.

• Для фартука: -DAPRON_ROOT=$APRON_INSTALL_DIR
• Для Elina: -DELINA_ROOT=$ELINA_INSTALL_DIR
• Для коробок: -DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR
• Для pplite: -DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR

Использование Crab Library в других проектах C ++

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

• Включите файлы заголовков C ++, расположенные на $INSTALL_DIR/crab/include , и

• Свяжите свое приложение с библиотеками крабов, установленными в $INSTALL_DIR/crab/lib .

Если вы компилируете с коробками/Apron/Elina/Pplite, вам также необходимо включить $INSTALL_DIR/EXT/include и ссылка с $INSTALL_DIR/EXT/lib , где EXT=apron|elina|ldd|pplite .

Cmake

Если ваш проект использует cmake , вам просто нужно добавить в CMakeLists.txt вашего проекта.txt:

 add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})

А затем свяжите свой исполняемый файл с ${CRAB_LIBS}

Делать

Если ваш проект использует make , прочитайте этот пример Makefile.