intAbs

Readme

Este repositório é sobre interpretação abstrata modular de threads (usando a biblioteca de avental) para programas orientados a interrupções, adotando informações prioritárias.

O código-fonte é uma versão modificada de https://github.com/markus-kusano/watts

No momento, todos os arquivos não são limpos, incluindo arquivos de teste.

No entanto, o subconjunto de tabelas de resultado pode ser impresso, pois alguns arquivos de saída são enviados.

Citando intabs

 @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}
}

Prédio

O programa é um passe Opt LLVM. É construído usando cmake. Como estamos usando o CMake, isso provavelmente requer LLVM versão 3.6.0

Modifique o arquivo cmakelists variável apron_prefix para ser o local onde o avental está instalado

Supondo que seus arquivos de biblioteca LLVM estejam em um local padrão (mais sobre isso abaixo), simplesmente:

 mkdir build
cd build
cmake ../
make

O resultado do processo de construção é um arquivo .SO, libworklistai.so

Se você precisar dizer ao cmake onde o LLVM mora, você precisa adicionar a opção -dllvm_dir, por exemplo,

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

O diretório passou para LLVM_DIR deve ser o local onde os arquivos CMake LLVM são (por exemplo, llvm-config.cmake).

Você também pode precisar definir -dz3_inc e -dz3_lib para o diretório incluir e o arquivo da biblioteca para Z3, respectivamente.

Caminho de teste

Você precisa modificar o caminho LLVM e criar o caminho no arquivo SRC/Test/Export.sh para testar o programa como LLVM_Prefix, Worklist_SO, Z3_BIN.

Afirmar uso

Se você deseja verificar os invariantes do programa usando as afirmações, precisa usar dessa maneira.

Em vez de usar assert(a==1) , você deve escrever if (a != 1) { assert(0); } .

Devido à relação pós -dominador, preciso implementar minha ferramenta para suportar apenas este caso (assert torna o programa inacessível para que algum relacionamento pós -dominador seja perdido).

Descrição do diretório

• ICBMC: Este é o diretório em que testei o arquivo binário ICBMC do documento Date15 com meus benchmarks.

• SRC: Contém a implementação principal (Worlist-AI, UTILS, Cmakelists.txt) e um diretório de teste (teste)

• SRC/teste: ele contém arquivos de script para executar os programas de teste e referência. Além disso, os arquivos de resultado estão incluídos em cada diretório.