intAbs

Readme

In diesem Repository handelt es sich um die modulare abstrakte Thread-Interpretation (unter Verwendung der Schrongbibliothek) für Interrupt-gesteuerte Programme, indem Prioritätsinformationen übernommen werden.

Der Quellcode ist eine modifizierte Version von https://github.com/markus-kusano/watts

Derzeit werden alle Dateien nicht aufgeräumt, einschließlich Testdateien.

Die Teilmenge von Ergebnistabellen kann jedoch gedruckt werden, da einige Ausgabedateien hochgeladen werden.

Unter Berufung auf 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}
}

Gebäude

Das Programm ist ein LLVM -Opt -Pass. Es wird mit CMake gebaut. Da wir CMake verwenden, erfordert dies wahrscheinlich LLVM Version 3.6.0

Ändern Sie die CMakelists Dateivariable APRON_PREFIX, um den Ort zu sein, an dem die Schürze installiert ist

Angenommen, Ihre LLVM -Bibliotheksdateien befinden sich an einem Standardort (mehr dazu unten) einfach:

 mkdir build
cd build
cmake ../
make

Das Ergebnis des Erstellungsprozesses ist eine .so -Datei, libworkListai.so

Wenn Sie CMake mitteilen müssen, wo LLVM lebt, müssen Sie die Option addieren -dllvm_dir, z.

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

Das an llvm_dir übergebene Verzeichnis sollte der Ort sein, an dem sich die LLVM-CMake-Dateien befinden (z. B. LLVM-config.cmake).

Möglicherweise müssen Sie auch -dz3_inc und -dz3_lib auf das inclupt -Verzeichnis bzw. der Bibliotheksdatei für Z3 einstellen.

Testpfad

Sie müssen den LLVM -Pfad ändern und den Pfad in der Datei src/test/export.sh erstellen, um Programm wie llvm_prefix, WorkList_so, Z3_BIN zu testen.

Nutzung geltend machen

Wenn Sie die Invarianten des Programms mit Assert überprüfen möchten, müssen Sie auf diese Weise verwenden.

Anstatt assert(a==1) zu verwenden, müssen Sie aufschreiben if (a != 1) { assert(0); } .

Aufgrund der Beziehung zwischen Post Dominator muss ich mein Tool implementieren, um nur diesen Fall zu unterstützen (Assert macht das Programm nicht erreichbar, sodass einige Post -Dominator -Beziehung verloren gehen).

Verzeichnisbeschreibung

• ICBMC: Dies ist das Verzeichnis, in dem ich die ICBMC -Binärdatei von Datum 15 mit meinen Benchmarks getestet habe.

• SRC: Es enthält die Hauptimplementierung (Worlist-AI, Utils, cmakelists.txt) und ein Testverzeichnis (Test)

• SRC/Test: Es enthält Skriptdateien zum Ausführen der Test- und Benchmark -Programme. Außerdem sind die Ergebnisdateien in jedem Verzeichnis enthalten.