intAbs

Ридме

Этот репозиторий посвящена потоке модульной абстрактной интерпретации (с использованием библиотеки фартука) для программ, управляемых прерыванием путем принятия приоритетной информации.

Исходный код-это модифицированная версия от https://github.com/markus-kusano/watts

Прямо сейчас все файлы не очищаются, включая тестовые файлы.

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

Цитируя интаб

 @inproceedings{DBLP:conf/kbse/SungKW17,
  author    = {Chungha Sung and
               Markus Kusano and
               Chao Wang},
  title     = {Modular verification of interrupt-driven software},
  booktitle = {Proceedings of the 32nd {IEEE/ACM} International Conference on Automated
               Software Engineering, {ASE} 2017, Urbana, IL, USA, October 30 - November
               03, 2017},
  pages     = {206--216},
  year      = {2017},
  crossref  = {DBLP:conf/kbse/2017},
  url       = {https://doi.org/10.1109/ASE.2017.8115634},
  doi       = {10.1109/ASE.2017.8115634},
  timestamp = {Fri, 01 Dec 2017 22:44:10 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/kbse/SungKW17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

Здание

Программа - это проход LLVM Opt. Он построен с использованием Cmake. Поскольку мы используем CMAKE, это, вероятно, требует LLVM версии 3.6.0

Измените файл cmakelists переменную apron_prefix, чтобы быть местом, где установлен фартук

Предполагая, что ваши файлы библиотеки LLVM находятся в стандартном месте (подробнее об этом ниже), просто:

 mkdir build
cd build
cmake ../
make

Результатом процесса сборки является файл .so, libworklistai.so

Если вам нужно сообщить Cmake, где живет LLVM, вам нужно добавить опцию -dllvm_dir, например,

cmake -dllvm_dir =/home/Chungha/src/share/llvm/cmake ../

Каталог, переданный в LLVM_DIR, должен быть местом, где представлены файлы CMAKE LLVM (например, LLVM-config.cmake).

Вам также может потребоваться установить -dz3_inc и -dz3_lib в каталог включения и файл библиотеки для Z3 соответственно.

Тестовый путь

Вам необходимо изменить путь LLVM и путь построения в файле src/test/export.sh для тестирования программы, такой как LLVM_PREFIX, WorkList_SO, Z3_BIN.

Утверждают использование

Если вы хотите проверить инварианты программы, используя Assert, вы должны использовать таким образом.

Вместо использования assert(a==1) вы должны записать if (a != 1) { assert(0); } .

Из -за отношения после доминатора мне нужно реализовать свой инструмент для поддержки только этого случая (Assert делает программу недоступной, чтобы некоторые отношения после доминирования были потеряны).

Описание каталога

• ICBMC: Это каталог, в котором я тестировал двоичный файл ICBMC с бумаги Date15 с моими тестами.

• SRC: он содержит основную реализацию (Worlist-AI, Utils, Cmakelists.txt) и тестовый каталог (тест)

• SRC/TEST: он содержит файлы скриптов для запуска программ теста и эталон. Кроме того, файлы результатов включены в каждый каталог.