intAbs

Réadmettre

Ce référentiel concerne l'interprétation abstraite modulaire de threads (en utilisant la bibliothèque de tabliers) pour les programmes axés sur l'interruption en adoptant des informations prioritaires.

Le code source est une version modifiée de https://github.com/markus-kusano/watts

À l'heure actuelle, tous les fichiers ne sont pas nettoyés, y compris les fichiers de test.

Cependant, le sous-ensemble des tables de résultats peut être imprimé car certains fichiers de sortie sont téléchargés.

Citant des 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}
}

Bâtiment

Le programme est un Pass LLVM OPT. Il est construit à l'aide de cmake. Puisque nous utilisons CMake, cela nécessite probablement la version 3.6.0 de LLVM

Modifiez la variable de fichier CMAKELIST APRON_PREFIX pour être l'emplacement où le tablier est installé

En supposant que vos fichiers de bibliothèque LLVM sont dans un emplacement standard (plus à ce sujet ci-dessous), simplement:

 mkdir build
cd build
cmake ../
make

Le résultat du processus de construction est un fichier .so, libworkListai.so

Si vous devez dire à Cmake où vit LLVM, vous devez ajouter l'option -dllvm_dir, par exemple,

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

Le répertoire transmis à LLVM_DIR devrait être l'emplacement où se trouvent les fichiers LLVM CMake (par exemple, llvm-config.cmake).

Vous devrez peut-être également définir -dz3_inc et -dz3_lib dans le répertoire inclué et le fichier de bibliothèque pour Z3, respectivement.

Chemin d'essai

Vous devez modifier le chemin LLVM et la construction du chemin du chemin dans le fichier SRC / test / export.sh pour tester le programme tel que LLVM_PREFIX, Worklist_So, Z3_Bin.

Affirmer l'utilisation

Si vous souhaitez vérifier les invariants du programme à l'aide d'Assert, vous devez l'utiliser de cette manière.

Au lieu d'utiliser assert(a==1) , vous devez noter if (a != 1) { assert(0); } .

En raison de la relation post-dominatrice, je dois implémenter mon outil pour prendre en charge uniquement ce cas (Assert rend le programme inaccessible, donc une relation post-dominatrice est perdue).

Description du répertoire

• ICBMC: Il s'agit du répertoire où j'ai testé le fichier binaire ICBMC à partir du papier Date15 avec mes repères.

• SRC: Il contient une implémentation principale (Worlist-AI, Utils, cMakelistis.Txt) et un répertoire de test (test)

• SRC / Test: il contient des fichiers de script pour exécuter les programmes de test et de référence. De plus, les fichiers de résultats sont inclus dans chaque répertoire.