lart

LART: LLVM -Abstraktions- und Verfeinerungswerkzeug

LART = LLVM Abstraktions- und Verfeinerungswerkzeug. Ziel dieses Tools ist es, LLVM-zu-LLVM-Transformationen bereitzustellen, die verschiedene Programmabstraktionen implementieren. In Bezug auf den Anweisungssatz sind die resultierenden Programme normal, konkrete LLVM -Programme, die ausgeführt und analysiert werden können. Zusätzliche Informationen über die Abstraktion (en) über ein (Fragment) -Programm werden unter Verwendung von speziellen LLVM -intrinsischen Funktionen und LLVM -Metadatenknoten eingefügt. LART bietet sowohl ein eigenständiges Tool, das Bitcode-Dateien auf disk verarbeitet, als auch ein Framework, das in komplexe LLVM-basierte Tools integriert werden kann. Die Hauptmotivation für LART besteht darin, einen "Präprozessor" für LLVM-basierte Modellprüfer und andere Analyse-Tools bereitzustellen, wodurch deren Auftrag die Problemgröße verringert wird, ohne die Klang der Analysen zu beeinträchtigen. Die von LART implementierten Abstraktionen können normalerweise auf der Grundlage spezifischer Anweisungen, welcher "Teil" der Abstraktion zu rau ist (eine zu raue Abstraktion, die für nachfolgende Analysen sichtbar ist, aber im ursprünglichen Programm nicht vorhanden ist).

Abstraktionen für LLVM -Bitcode

Der Zweck der gesamten Übung besteht darin, Informationen von LLVM Bitcode abstrahieren und nachfolgende Analysen effizienter zu machen (auf Kosten einiger Präzision). Zu diesem Zweck müssen wir hauptsächlich in LLVM-Programmen nicht deterministische Auswahl kodieren können, die einfach durch eine Spezialfunktion (ähnlich wie LLVM-Intrinsics) durchgeführt werden können. Die Funktion heißt @lart.choice , nimmt ein Paar Grenzen als Argumente und gibt nicht deterministisch einen Wert zurück, der zwischen diesen Grenzen fällt.

Diese Erweiterung der LLVM -Semantik muss vom nachgeschalteten Tool erkannt werden. Dies ist auch die einzige entscheidende Abweichung vom Standard -LLVM -Bitcode. Viele Analysetools implementieren bereits einen ähnlichen Mechanismus, entweder intern oder sogar mit einer externen Schnittstelle. Die Anpassung von Tools ohne Unterstützung für @lart.choice um mit Lart zu arbeiten, ist normalerweise sehr einfach.

Es gibt andere Spezialfunktionen von Lart, nämlich die Familie @lart.meta.* @llvm.dbg.* Es wird erwartet, dass Programmtransformationen diese Aufrufe beibehalten, wenn LART eine Abstraktion verfeinert wird (jede von Lart bereitgestellte Abstraktion wird mit einem entsprechenden Verfeinerungsverfahren geliefert, das häufig die von der Abstraktion eingefügten @lart.meta -Aufrufe ermitteln muss).

Während die meisten traditionellen Abstraktionsmotoren als Dolmetscher funktionieren, können Abstraktionen auch in Programme "zusammengestellt" werden. Anstatt (neu) Anweisungen symbolisch zu interpretieren, können die symbolischen Anweisungen kompiliert werden. Bei Prädikatabstraktion manipuliert und verwendet die resultierende Bitcode Prädikatbewertungen anstelle von konkreten Variablen. Wie oben erläutert, besteht der wichtige Unterschied darin, dass der Bitcode nicht deterministische Entscheidungen treffen muss, da einige Prädikate möglicherweise unbestimmte Bewertungen haben (sowohl wahr als auch falsch). Einige Variablen könnten sogar vollständig abstrahiert werden, und alle Tests an solchen Variablen liefern sowohl Ja- als auch Nein -Antworten.

Bauen

Verwenden oder wiederholen Sie das Setup vorerst von ./devcontainer/Dockerfile .

Dann verwenden Sie:

 ./scripts/build.sh

Compiler ausführen

 ./build/bin/lartcc <domain> <compiler arguments> in.c

Opt

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

Prüfen

 lit -v build/test

Hinweis: build/lartcc/lartcc müssen übergreifende Permisionen haben.