seahorn
v0.1.0 Release (SV-COMP'16)
Seahorn ist ein automatisiertes Analyse-Framework für LLVM-basierte Sprachen. Diese Version erstellt gegen LLVM 14.
Einige der unterstützten Funktionen sind
Seahorn wird hauptsächlich als Rahmen für die Durchführung von Forschungsforschung zur automatisierten Überprüfung entwickelt. Die Frameworks bieten viele Komponenten, die auf verschiedene Weise zusammengestellt werden können. Es handelt sich jedoch nicht um ein "Out-of-the-Box" -Stoly.
Viele Analysetools und Beispiele werden mit dem Framework bereitgestellt. Wir suchen ständig nach neuen Anwendungen und unterstützen neue Benutzer. Weitere Informationen darüber, was passiert, finden Sie in unserem (selten aktualisierten) Blog.
Seahorn wird unter einer modifizierten BSD -Lizenz verteilt. Einzelheiten siehe Lizenz.txt.
Seahorn bietet ein Python -Skript namens sea , um mit Benutzern zu interagieren. Angesichts eines mit Behauptungen kommentierten C -Programms müssen Benutzer nur eingeben: sea pf file.c
Das Ergebnis von sea-pf ist unsat wenn alle Behauptungen ausfallen, ein sat wenn eine der Behauptungen verletzt wird.
Die Option pf fordert Seahorn an, file.c in LLVM -Bitcode zu übersetzen, eine Reihe von Verifizierungsbedingungen (VCs) zu generieren und schließlich zu lösen. Der Hauptlöser für Back-End-Löser ist Abstandhalter.
Der Befehl pf bietet unter anderem die folgenden Optionen:
--show-invars : Anzeige berechnete Invarianten, wenn die Antwort unsat .
--cex=FILE : Speichert ein Gegenbeispiel in FILE , wenn die Antwort sat wurde.
-g : Kompiliert mit Debug -Informationen für verfolgbare Gegenbeispiele.
--step=large : Großstufe Codierung. Jede Übergangsbeziehung entspricht einen schleifenfreien Fragmente.
--step=small : Small-Step-Codierung. Jede Übergangsbeziehung entspricht einem Grundblock.
--track=reg : Modell (Ganzzahl) nur Register.
--track=ptr : Modellregister und Zeiger (aber nicht Speicherinhalt)
--track=mem : Modell sowohl Skalare, Zeiger als auch Gedächtnisinhalte modellieren
--inline : Einbezogen das Programm vor der Überprüfung
--crab : Inject Inject Inject Inject Inject Inject Inject Injects in spacer , die vom Crab-Abstract-Interpretations-basierten Tool erzeugt werden. Hier finden Sie Details zu allen Krabbenoptionen (Präfix --crab ). Sie können sehen, welche Invarianten durch die Tippoption --log=crab durch die Krabbe abgeleitet werden.
--bmc : Verwenden Sie den BMC-Motor.
sea pf ist eine Pipeline, die mehrere Befehle ausführt. Einzelne Teile der Pipeline können auch separat ausgeführt werden:
sea fe file.c -o file.bc : Seahorn Frontend übersetzt ein C -Programm in optimierte LLVM -Bitcode einschließlich der Transformation mit gemischter Semantik.
sea horn file.bc -o file.smt2 : Seahorn generiert die Überprüfungsbedingungen aus file.bc und gibt sie in SMT -Lib V2 -Format aus. Benutzer können zwischen verschiedenen Codierungsstilen mit mehreren Genauigkeitsebenen wählen, indem sie hinzufügen:
--step={small,large,fsmall,flarge} Wo small ist, kleiner Schritt codieren, large ist Block-Large-Codierung, fsmall ist kleiner Stufencodieren, der flache Horn-Klauseln erzeugt (dh ein Übergangssystem mit nur einer Prädiktion) und flarge : blocklarge Codierung flacher Horn-Clauss.
--track={reg,ptr,mem} wobei reg nur Integer Scalarars, ptr Modelle reg und Zeigeradressen sowie mem Modelle ptr und Speicherinhalte.
sea smt file.c -o file.smt2 : Generiert CHC im SMT -LIB2 -Format. Ist ein Alias für sea fe gefolgt von sea horn . Das Kommando sea pf ist ein Alias für sea smt --prove .
sea clp file.c -o file.clp : generiert CHC im CLP -Format.
sea lfe file.c -o file.ll : Läuft das Legacy Front -End
Um alle Befehle zu sehen, geben Sie sea --help . Um Optionen für jeden einzelnen Befehl CMD (z. B. horn ) zu sehen, geben Sie sea CMD --help (z. sea horn --help ) an.
Seahorn verwendet standardmäßig keine Krabbe. Um Crab zu aktivieren, fügen Sie die Option --crab dem sea -Befehl.
Der abstrakte Dolmetscher ist standardmäßig intra-procedural und verwendet die Zonendomäne als numerische abstrakte Domäne. Diese Standardoptionen sollten für normale Benutzer ausreichen. Wenn Sie für Entwickler andere abstrakte Domänen verwenden möchten, müssen Sie:
cmake -Optionen -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea mit Option --crab-dom=DOM wobei DOM sein kann:int für Intervalleterm-int für Intervalle mit nicht interpretierten Funktionenboxes : Für disjunktive Intervalleoct für Octagonspk für Polyeder Um die inter-procedurale Krabbenanalyse zu verwenden, müssen Sie mit Option sea durchführen --crab-inter
Standardmäßig ist der abstrakte Dolmetscher nur Gründe für Skalarvariablen (dh LLVM -Register). Führen Sie sea mit den Optionen --crab-track=mem --crab-singleton-aliases=true für den Speicherinhalt.
Krabbe ist größtenteils unempfindlich, während der Abstandshalter, unser Horn-Klausel-Solver, Pfadempfindlichkeit ist. Obwohl Pfad-unempfindliche Analysen effizienter sind, ist die Pfadempfindlichkeit in der Regel erforderlich, um die Eigenschaft von Interesse nachzuweisen. Dies motiviert unsere Entscheidung, zuerst die Krabbe zu führen (falls Option --crab ) und dann die generierten Invarianten an den Abstandshalter übergeben. Derzeit gibt es zwei Möglichkeiten für Spacer, die von Crab erzeugten Invarianten zu verwenden. Die sea -Option --horn-use-invs=VAL sagt spacer , wie man diese Invarianten verwendet:
VAL gleich bg ist, werden Invarianten nur verwendet, um spacer zu helfen, zu beweisen, dass ein Lemma induktiv ist.VAL always gleich ist, ist das Verhalten dem bg ähnlich, aber zusätzlich werden Invarianten auch verwendet, um spacer beim Blockieren eines Gegenbeispiels zu helfen. Der Standardwert ist bg . Wenn die Krabbe beweisen kann, dass das Programm sicher ist, entspricht der Spacer natürlich keine zusätzlichen Kosten.
Es wird angenommen, dass Eigenschaften Behauptungen sind. Seahorn liefert ein statisches Behandlungsbefehl sassert , wie im folgenden Beispiel dargestellt
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();
int main ( void ) {
int k = 1 ;
int i = 1 ;
int j = 0 ;
int n = nd ();
while ( i < n ) {
j = 0 ;
while ( j < i ) {
k += ( i - j );
j ++ ;
}
i ++ ;
}
sassert ( k >= n );
} Innen folgt Seahorn die SV-Comp-Konvention von Codierungsfehlern durch einen Aufruf der angegebenen Fehlerfunktion __VERIFIER_error() . Seahorn kehrt unsat zurück, wenn __VERIFIER_error() nicht erreichbar ist und das Programm als sicher angesehen wird. Seahorn kehrt sat wenn __VERIFIER_error() erreichbar ist und das Programm unsicher ist. sassert() -Methode ist in seahorn/seahorn.h definiert.
Abgesehen davon, dass Eigenschaften nachgewiesen oder Gegenbeispiele erzeugt werden, ist es manchmal nützlich, den in Analyse befindlichen Code zu inspizieren, um eine Vorstellung von seiner Komplexität zu erhalten. Dazu bietet Seahorn eine Kommando sea inspect an. Zum Beispiel bei einem C -Programm ex.c -Typ:
sea inspect ex.c --sea-dsa=cs+t --mem-dot
Die Option --sea-dsa=cs+t ermöglicht die neue Kontext-sensitive Sea-DSA-Analyse, die in FMCAD19 beschrieben wird. Dieser Befehl generiert für jeden FUN im Eingabeprogramm eine FUN.mem.dot -Datei. Verwenden Sie um die Grafik der Hauptfunktion zu visualisieren, verwenden Sie Web Graphivz -Schnittstelle oder die folgenden Befehle:
$ dot -Tpdf main.mem.dot -o main.mem.pdfWeitere Details zu den Speichergraphen finden Sie im Seadsa -Repository: hier.
Verwenden Sie sea inspect --help um alle Optionen zu sehen. Derzeit sind die verfügbaren Optionen:
sea inspect --profiler druckt die Anzahl der Funktionen, Basisblöcke, Schleifen usw. aus.sea inspect --mem-callgraph-dot DRUCKEN DES dot -Formates Die von Seadsa konstruierte Anrufdiagramm.sea inspect --mem-callgraph-stats FÜR STATSTICS über die von Seadsa durchgeführte Call-Graph-Konstruktion.sea inspect --mem-smc-stats druckt die Anzahl der Speicherzugriffe, die von Seadsa als sicher erwiesen werden können.Der einfachste Weg, um mit Seahorn zu beginnen, ist eine Docker -Verteilung.
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly Beginnen Sie mit der Erforschung, was der sea -Befehl kann:
$ sea --help
$ sea pf --help Das nightly Tag wird automatisch täglich aktualisiert und enthält die neueste Entwicklungsversion. Wir verwalten alle anderen Tags (für die manuelle Aktualisierung erfordern) selten. Überprüfen Sie die Daten auf DockerHub und protokollieren Sie ein Problem auf GitHub, wenn sie zu abgestanden sind.
Weitere Beispiele und Konfigurationsoptionen finden Sie im Blog. Der Blog ist selten aktualisiert. Insbesondere die Optionen ändern sich, die Funktionen werden ausgeschaltet, neue Dinge werden hinzugefügt. Wenn Sie Probleme im Blog finden, lassen Sie es uns wissen. Wir werden den Blog -Beitrag zumindest aktualisieren, um anzuzeigen, dass nicht erwartet wird, dass er mit der neuesten Version des Codes funktioniert.
Sie können auch manuell installieren von:
Befolgen Sie die Anweisungen in der Docker-Datei Dockerfile: docker/seahorn-builder.Dockerfile .
Wenn dies nicht funktioniert, laufen Sie:
$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *Die ersten 3 Befehle werden LLVM 14 installiert, der 4. wird libpolly installieren, das fälschlicherweise von LLVM 14 weggelassen wird (aber in nachfolgenden Versionen enthalten ist).
Befolgen Sie als nächstes die Anweisung in der obigen Docker -Datei
Die Informationen von diesem Punkt an sind nur für Entwickler. Wenn Sie zu Seahorn beitragen möchten, bauen Sie Ihre eigenen Werkzeuge basierend darauf oder interessieren Sie sich einfach daran, wie es im Inneren funktioniert, und lesen Sie weiter.
Seahorn benötigt LLVM, Z3 und Boost. Die genauen Versionen der Bibliotheken ändern sich weiter, aber CMake Craft wird verwendet, um zu überprüfen, ob die richtige Version verfügbar ist.
Um eine bestimmte Version einer der Abhängigkeiten anzugeben, verwenden Sie den üblichen <PackageName>_ROOT und/oder <PackageName>_DIR (siehe find_package () für Details) cmake -Variablen.
Seahorn ist in mehrere Komponenten unterteilt, die in verschiedenen Repositories (unter Seahornorganisation) leben. Der Build -Prozess überprüft automatisch alles bei Bedarf. Für aktuelle Build -Anweisungen überprüfen Sie die CI -Skripte.
Dies sind die generischen Schritte. Benutze sie nicht . Lesen Sie einen besseren Weg weiter:
cd seahorn ; mkdir build ; cd build (das Build -Verzeichnis kann sich auch außerhalb des Quellverzeichnisses befinden.)cmake -DCMAKE_INSTALL_PREFIX=run ../ (Install ist erforderlich! )cmake --build . --target extra && cmake .. (Klonekomponenten, die anderswo leben)cmake --build . --target crab && cmake .. (Klonekrabbenbibliothek)cmake --build . --target install (bauen und installieren Sie alles unter run )cmake --build . --target test-all (Ausführen von Tests)HINWEIS : Das Installieren von Target ist erforderlich, damit die Tests funktionieren!
Für eine verbesserte Entwicklungserfahrung:
clanglld -Linkercompile_commands.json Unter Linux schlagen wir die folgende cmake -Konfiguration vor:
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run
-DCMAKE_BUILD_TYPE=RelWithDebInfo
-DCMAKE_CXX_COMPILER="clang++-14"
-DCMAKE_C_COMPILER="clang-14"
-DSEA_ENABLE_LLD=ON
-DCMAKE_EXPORT_COMPILE_COMMANDS=1
../
-DZ3_ROOT=<Z3_ROOT>
-DLLVM_DIR=<LLMV_CMAKE_DIR>
-GNinja
$ (cd .. && ln -sf build/compile_commands.json .)
wobei <Z3_ROOT ein Verzeichnis ist, das Z3 -Binärverteilung enthält, und LLMV_CMAKE_DIR ist ein Verzeichnis, das LLVMConfig.cmake enthält.
Weitere rechtliche Optionen für CMAKE_BUILD_TYPE sind Debug und Coverage . Beachten Sie, dass die CMAKE_BUILD_TYPE mit dem zur kompilierten LLVM kompatibel sein muss. Insbesondere benötigen Sie einen Debug -Build von LLVM, um SeaHorn im "Debug ** -Modus" zusammenzustellen. Stellen Sie sicher, dass Sie viel Geduld, Speicherplatz und Zeit haben, wenn Sie sich für diesen Weg entscheiden.
Alternativ kann das Projekt mit CMAKE -Voreinstellungen konfiguriert werden. Führen Sie dazu einfach den folgenden Befehl aus:
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > So konfigurieren Sie CMake, wobei <BUILD_TYPE> einer von: Debug , RelWithDebInfo oder Coverage und <PRESET_NAME> ist, ist die voreingestellte, die Sie verwenden möchten. Die derzeit verfügbaren Voreinstellungen sind: jammy . Diese Voreinstellungen gehen davon aus, dass Sie Z3 in /opt/z3-4.8.9 und Yices in /opt/yices-2.6.1 installiert haben.
Auf diese Weise kann das Projekt auch in VS -Code mit der CMAKE -Tools -Erweiterung konfiguriert und kompiliert werden.
Wenn Sie verschiedene Kompilierungseinstellungen verwenden möchten oder Z3 oder YICES in einem anderen Verzeichnis installiert sind, müssen Sie Ihre eigene CMakeUserPresets.json -Datei mit Ihren eigenen Voreinstellungen erstellen.
Fügen Sie nicht -DSEA_ENABLE_LLD=ON . Der Standard -Compiler ist Clang, sodass Sie ihn möglicherweise nicht explizit festlegen müssen.
Seahorn bietet mehrere Komponenten, die automatisch über das extra Ziel geklont und installiert werden. Diese Komponenten können von anderen Projekten außerhalb von Seahorn verwendet werden.
Sea-Ssa: git clone https://github.com/seahorn/sea-dsa.git
sea-dsa ist eine neue DSA-basierte Heap-Analyse. Im Gegensatz zu llvm-dsa ist sea-dsa kontextsensitiv und daher kann eine feiner körnige Aufteilung des Haufens in Gegenwart von Funktionsaufrufen erzeugt werden.
Clam: git clone https://github.com/seahorn/crab-llvm.git
clam bietet induktiven Invarianten mit abstrakten Interpretationstechniken für den Rest der Backends von Seahorn.
llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn bietet maßgeschneiderte Versionen von InstCombine und IndVarSimplify -LLVM-Pässen sowie einen LLVM-Pass, um undefinierte Werte unter anderem in nichtministische Anrufe umzuwandeln.
Seahorn kommt nicht mit einer eigenen Version von Clang und erwartet, dass er es entweder im Build -Verzeichnis ( run/bin ) oder im Pfad finden wird. Stellen Sie sicher, dass die Version von Clang mit der Version von LLVM übereinstimmt, mit der Seahorn zusammengestellt wurde (derzeit LLVM14). Der einfachste Weg, um die richtige Version von Clang bereitzustellen, besteht darin, sie von llvm.org herunterzuladen, irgendwo auszubilden und einen symbolischen Link zu clang und clang++ in run/bin zu erstellen.
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ Wo <CLANG_ROOT> ist der Ort, an dem Clang ausgepackt wurde.
Die Testinfrastruktur hängt von mehreren Python -Paketen ab. Diese haben ihre eigenen Abhängigkeiten. Wenn Sie sie nicht herausfinden können, verwenden Sie stattdessen Docker.
$ pip install lit OutputCheck networkx pygraphviz Wir können gcov und lcov verwenden, um Informationen zur Testabdeckung für Seahorn zu generieren. Um mit aktivierter Deckung zu erstellen, müssen wir Build unter einem anderen Verzeichnis ausführen und festlegen, dass CMAKE_BUILD_TYPE während der CMAKE -Konfiguration die Coverage abgibt.
Beispielschritte zum Erstellen von Deckungsbericht für das test-opsem Ziel:
mkdir coverage; cd coverage erstellen und gebencmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem Opsem-Tests, jetzt .gcda und .gcno -Dateien sollten in den entsprechenden CMakeFiles -Verzeichnissen erstellt werdenlcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info Sammeln Sie Deckungsdaten aus dem gewünschten Modul, wenn clang als Compiler anstelle von gcc verwendet wird, erstellen Sie eine Bash -Skript llvm-gcov.sh : #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh Anschließend append --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh zum Befehl lcov -c ... 6. Daten aus gewünschten Verzeichnissen extrahieren und HTML -Bericht erstellen:
lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report Öffnen Sie dann im Browser coverage_report/index.html um den Berichterstattungsbericht anzuzeigen
Siehe auch scripts/coverage für Skripte, die vom CI verwendet werden. Der Berichterstattungsbericht für nächtliche Builds ist bei Codecov erhältlich
Die Kompilierungsdatenbank für das Seahorn -Projekt und alle ihre Unterprojekte werden mit -DCMAKE_EXPORT_COMPILE_COMMANDS=ON option for cmake generiert.
Eine einfache Möglichkeit, die Code -Indexierung mit der Unterstützung der Kompilierungsdatenbank zu erhalten, besteht darin, die Datei compilation_database.json in das Hauptprojektverzeichnis zu verknüpfen und Anweisungen zu befolgen, die für Ihren Editor spezifisch sind.
lsp-ui mit clangd , die in Spacemacs entwickeln können, Branchen Für einen detaillierten Leitfaden für einen Remote-Workflow mit Clion Check Clion-Konfiguration.
Verwenden Sie unsere Gabel von Mainframer. Verpassen Sie nicht die Beispielkonfiguration.
