sys
1.0.0
Wenn Sie interessiert sind, lesen Sie die (sehr sehr) neue Neuauflagen hier!
Wenn Sie SYS lokal installieren möchten:
--shared Option. Sehen Sie sich die Funktionen build() und package() in dieser Datei als Beispiel für die Installation von Boolector nach dem Klonen an. Unter Arch Linux können Sie nur boolector-git von AUR installieren.Alternativ können Sie die Dockerfile von Ralf-Philipp Weinmann verwenden.
Sobald Sie alle Abhängigkeiten installiert haben, sollten Sie einfach das Tool erstellen können:
stack build
Sobald Sie das Werkzeug erstellt haben, können Sie unsere Tests erstellen und durchführen:
stack test
Dies führt zu einer mehr oder weniger Vollversion unserer Testsuite sowie Regressionstests für jeden Fehler, den wir in der Zeitung auflisten. Die Suite dauert etwas mehr als zwei Minuten auf dem Laptop mit 64 GB RAM und 8 Fäden. Alle Tests mit einer Ausnahme-ein Fehler, dessen Quelle wir Probleme haben, sollte bestehen. Wenn etwas anderes fehlschlägt, versuchen Sie, die Tests erneut zu fahren. Der Löser hat vielleicht zeitlich festgelegt (dies ist nicht auf unseren Maschinen passiert, aber da wir Ihnen keine Anmeldung für Annonymität geben können, ist es eine Möglichkeit, dass er auf Ihrer Maschine passieren wird).
Wenn Sie nur die Papierergebnisse reproduzieren möchten und sonst nichts, rennen Sie:
stack test --ta '-p End-to-end'
Sobald Sie das Tool erstellt haben, können Sie es jetzt verwenden, um Fehler zu finden!
stack exec sys
Das Tool nimmt mehrere Optionen aus:
-d DIR --libdir=DIR directory (or file) to analyze
-e EXTN --extn=EXTN file extension
-c CHECK --check=CHECK checker to run
-d wird verwendet, um das Verzeichnis (mit den LLVM -Dateien) oder eine einzelne LLVM -Datei anzugeben.-e wird verwendet, um die Erweiterung der zu prüfenden Dateien anzugeben. Dies ist nützlich, wenn Sie Ihr Projekt mit unterschiedlichen Optimierungsstufen erstellen (z. B. .ll-O0 für Debugg Build mit -O0 und .ll-O0_p für die Produktion).ll entspricht allen *.ll -DateienO0 entspricht allen *.ll-O0 und *.ll-O0_p DateienO1 entspricht allen *.ll-O1 und *.ll-O1_p DateienO2 entspricht allen *.ll-O2 und *.ll-O2_p DateienO3 entspricht allen *.ll-O3 und *.ll-O3_p DateienOg entspricht den Dateien mit allen *.ll-Og und *.ll-Og_pOs entspricht allen *.ll-Os und *.ll-Os_p DateienOz entspricht allen *.ll-Oz und *.ll-Os_z Dateienprod entspricht allen *_p -Dateienany Dateien entsprechen allen Dateien-c wird verwendet, um den für die ausgeführten Prüfer anzugeben, einer von::uninit : nicht initialisierte Speicherprüfungheapoob : Malloc OOB Checkerconcroob : Negativer Index -OOB -Checkeruserinput : Benutzereingangsprüfung Um den nicht initialisierten Speicherzugriffsfehler zu finden, den unser Tool in der PRIO -Bibliothek von Firefox gefunden hat:
$ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p
Das Werkzeug ändert zwei Fehler. Schauen wir uns den ersten an:
Stack uninit bug
Name "serial_read_mp_array_73"
in
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]
Wenn Sie die Funktion serial_read_mp_array () inspizieren, beträgt der Buggy -Block -Pfad %4 (der erste Block) auf %71 , wo wir [ %73 ] verwenden.
Wir haben Sys als Arch Linux nicht getestet (und werden wahrscheinlich nicht testen). Gerne integrieren wir Patches, die Unterstützung für andere OSS und Build -Systeme hinzufügen!
├── app -- Executable used to run the checkers
├── src
│ ├── Checkers -- Static and symbolic checkers
│ ├── Control -- Logging helpers
│ ├── LLVMAST -- LLVM AST interface
│ ├── InternalIR -- Internal IR used to represent paths for both static and symex
│ ├── Static -- Static checker DSL
│ └── Symex -- Symbolic DSL and execution engine
├── community -- Community files
└── test -- Tests
