crab

CRAB: Eine C ++ - Bibliothek zum Erstellen von statischen Analysen für Programme

Crab ist eine C ++ - Bibliothek zum Erstellen von statischen Analysen für Programme, die auf abstrakter Interpretation basieren. CRAB bietet eine Menge abstrakter Domänen, Fixpoint-Löser auf Kleene-basierten und unterschiedlichen Analysen wie Datenflow, inter-procedural und rückwärts. Das Design von Krabben ist ziemlich modular, so dass es einfach ist, neue abstrakte Domänen und Löser zu platzieren oder neue Analysen zu erstellen.

Krabben abstrakte Domänen können über Speicherinhalte, c-ähnliche Arrays und numerische Eigenschaften argumentieren. Crab verwendet effiziente Implementierungen populärer numerischer Domänen wie Zonen und Octagons und neuartige Domänen, um beispielsweise über symbolische Begriffe (auch nicht interpretierte Funktionen) zu begründen. Crab implementiert auch populäre nicht-relationale Domänen wie Intervall oder Kongruenzen unter Verwendung effizienter Umgebungskarten und ermöglicht die Kombination von willkürlichen Domänen über standardmäßige reduzierte Produktkonstruktionen. Crab bietet auch nicht konvexe Domänen wie spezialisierte disjunktive Intervalle, die als Kästchen bezeichnete, die auf linearen Entscheidungsdiagrammen basieren, und eine allgemeinere Wertungsstrategie für die Wertschöpfung, die eine willkürliche Domäne auf eine Überaberzeugung seiner Abschlusspflicht ansteigt. Zusätzlich zu diesen Domänen, die alle von Crab -Autoren entwickelt wurden, integriert die Crab Library beliebte abstrakte Domänenbibliotheken wie Schürze, Elina und PPLite.

Crab liefert den modernsten Löser mit verschachtelten Fixed Fixpoint, der die schwache topologische Reihenfolge von Bourdoncle verwendet, um den Satz der Erweiterungspunkte auszuwählen. Um Präzisionsverluste während der Verbreiterung zu mildern, implementiert Crab einige beliebte Techniken wie die Erweiterung mit Schwellenwerten und Aussehen aus der Auseinandersetzung.

Crab bietet zwei verschiedene Implementierungen interprozeduraler Analysen: eine Top-Down-Analyse mit Memoisierung inter-proceduraler Analyse mit Unterstützung rekursiver Aufrufe und einer Hybrid von Bottom-Up + Top-Down-Analyse. Last but not least implementiert Crab auch eine experimentellere Rückwärtsanalyse, mit der die erforderlichen Voraussetzungen berechnet und/oder die Anzahl der Fehlalarme reduziert werden können.

Crab analysiert nicht direkt eine Mainstream-Programmiersprache, sondern analysiert stattdessen seine eigene CFG-basierte Zwischendarstellung, die als Crabir bezeichnet wird. Crabir ist ein Dreiadress-Code und wird stark tippt. In Crabir wird der Kontrollfluss durch nicht deterministische GOTO-Anweisungen definiert. Abgesehen von Standard -Booleschen und arithmetischen Operationen bietet Crabir besondere Annahmen und Erklärungen. Ersteres kann verwendet werden, um den Kontrollfluss zu verfeinern, und letzteres bietet einen einfachen Mechanism, um auf benutzerdefinierte Eigenschaften zu überprüfen. Trotz seines einfachen Designs ist Crabir reich genug, um Sprachen wie LLVM darzustellen.

Krabben befindet sich aktiv in der Entwicklung. Wenn Sie einen Fehler finden, öffnen Sie bitte ein Github -Problem. Anfragen mit neuen Funktionen sind sehr willkommen. Die verfügbare Dokumentation finden Sie in unserem Wiki. Wenn Sie diese Bibliothek verwenden, zitieren Sie bitte dieses Papier.

Fenster	Ubuntu	Os x	Berichterstattung
TBD		TBD

Docker

Eine (nächtliche) vorgefertigte Version von Krabben, die alle Tests ausführt, können mit Docker erhalten werden:

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

Anforderungen

Die Krabbe ist in C ++ geschrieben und basiert auf der Boost -Bibliothek. Die Hauptanforderungen sind:

• C ++ 11 Compiler
• Boost> = 1,65
• GMP
• MPFR (if -DCRAB_USE_APRON=ON oder -DCRAB_USE_ELINA=ON )
• Flint (nur wenn -DCRAB_USE_PPLITE=ON )

In Linux können Sie die Anforderungen installieren, die die Befehle eingeben:

 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

Zusammenstellung und Installation

Zum Installieren von Krabben:

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

Das tests enthält viele Beispiele für das Erstellen von Programmen, die in Crabir geschrieben werden und Invarianten unter Verwendung verschiedener Analysen und abstrakter Domänen berechnen. Um diese Tests zu kompilieren, fügen Sie Option hinzu -DCRAB_ENABLE_TESTS=ON zu Zeile 2.

und dann zum Beispiel zum Ausführen test1 :

 build/test-bin/test1

Fügen Sie abstrakte Domänenbibliotheken von Drittanbietern ein

Die Kästchen/Schürze/Elina/PPLite-Domänen erfordern Bibliotheken von Drittanbietern. Um die Belastung für Benutzer zu vermeiden, die sich nicht für diese Domänen interessieren, ist die Installation der Bibliotheken optional.

• Wenn Sie die Kästchen -Domäne verwenden möchten, fügen Sie die Option -DCRAB_USE_LDD=ON .

• Wenn Sie die Domänen der Apron -Bibliothek verwenden möchten, fügen Sie die Option -DCRAB_USE_APRON=ON .

• Wenn Sie die Elina -Bibliotheksdomänen verwenden möchten, fügen Sie -DCRAB_USE_ELINA=ON .

• Wenn Sie die PPLite -Bibliotheksdomänen verwenden möchten, fügen Sie -DCRAB_USE_PPLITE=ON .

Wichtig: Schürze und Elina sind derzeit nicht kompatibel, sodass Sie nicht gleichzeitig -DCRAB_USE_APRON=ON und -DCRAB_USE_ELINA=ON aktivieren können.

Zum Beispiel zum Installieren von Krabben mit Kästchen und Schürze eingeben:

 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 	

Die Zeilen 3 und 4 werden die Kästchen bzw. Schürze -Domänen herunterladen, kompilieren und installieren. Ersetzen Sie apron in Zeile 4 durch elina oder pplite , wenn Sie stattdessen Elina oder Pplite verwenden möchten. Wenn Sie diese Bibliotheken bereits in Ihrem Computer kompiliert und installiert haben, überspringen Sie die Befehle in Zeile 3 und 4 und fügen Sie die folgenden Optionen in Zeile 2 hinzu.

• Für Schürze: -DAPRON_ROOT=$APRON_INSTALL_DIR
• Für Elina: -DELINA_ROOT=$ELINA_INSTALL_DIR
• Für Kästchen: -DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR
• Für pplite: -DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR

Verwenden der Krabbenbibliothek in anderen C ++ - Projekten

Um Krabben in Ihre C ++ - Anwendung aufzunehmen, müssen Sie:

• Fügen Sie die C ++ - Header -Dateien bei $INSTALL_DIR/crab/include und ein hinzu und

• Verknüpfen Sie Ihre Anwendung mit den in $INSTALL_DIR/crab/lib installierten Krabbenbibliotheken.

Wenn Sie mit Boxen/Apron/Elina/PPLite kompilieren EXT=apron|elina|ldd|pplite müssen Sie auch $INSTALL_DIR/EXT/include und verknüpfen und mit $INSTALL_DIR/EXT/lib

Cmake

Wenn Ihr Projekt cmake verwendet, müssen Sie nur CMakeLists.txt Ihres Projekts hinzufügen.

 add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})

Und dann Ihre ausführbare Datei mit ${CRAB_LIBS} verknüpfen

Machen

Wenn Ihr Projekt make wird, lesen Sie dieses Beispiel Makefile.