sea dsa
1.0.0
SeaDsa ist eine von DSA inspirierte LLVM-Bitcode, die von DSA inspiriert ist. SeaDsa ist eine Größenordnung skalierbarer und präziser als Dsa und eine frühere Implementierung von SeaDsa dank einer verbesserten Handhabung der Kontextempfindlichkeit, der Zugabe der partiellen Flussempfindlichkeit und der Typ-Wahrnehmung.
Obwohl SeaDsa beliebige LLVM -Bitcode analysieren kann, wurde es auf die Programmüberprüfung von C/C ++ - Programmen zugeschnitten. Es kann als eigenständiges Werkzeug oder zusammen mit dem Seahorn-Verifizierungsrahmen und seinen Analysen verwendet werden.
Dieser Zweig unterstützt LLVM 14.
SeaDsa ist in C ++ geschrieben und verwendet die Boost -Bibliothek. Die Hauptanforderungen sind:
Um Tests auszuführen, installieren Sie die folgenden Pakete:
sudo pip install lit OutputChecksudo easy_install networkxsudo apt-get install libgraphviz-devsudo easy_install pygraphvizGraph , Cell und Node , sind include/Graph.hh und src/Graph.cc definiert.include/Local.hh und src/DsaLocal.cc .include/BottomUp.hh und src/DsaBottomUp.cc .include/TopDown.hh und src/DsaTopDown.cc .include/Cloner.hh und src/Clonner.cc .include/FieldType.hh , include/TypeUtils.hh , src/FieldType.cc und src/TypeUtils.cc .include/AllocWrapInfo.hh und src/AllocWrapInfo.cc . Anweisungen zum Ausführen von Programmüberprüfungsbenchmarks sowie Rezepte zum Aufbau realer Projekte und unseren Ergebnissen finden Sie in Tea-Dsa-Extras.
SeaDsa enthält zwei Verzeichnisse: include und src . Da SeaDsa LLVM Bitcode analysiert, müssen LLVM -Header -Dateien und -Bibliotheken beim Erstellen mit SeaDsa zugänglich sein.
Wenn Ihr Projekt cmake verwendet, müssen Sie nur CMakeLists.txt Ihres Projekts hinzufügen.
include_directories(seadsa/include)
add_subdirectory(seadsa)
Wenn Sie llvm-14 bereits auf Ihrem Computer installiert haben:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake ..
cmake --build . --target install
Ansonsten:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install
Tests ausführen:
cmake --build . --target test-sea-dsa
Betrachten Sie ein C -Programm namens tests/c/simple.c :
#include <stdlib.h>
typedef struct S {
int * * x ;
int * * y ;
} S ;
int g ;
int main ( int argc , char * * argv ){
S s1 , s2 ;
int * p1 = ( int * ) malloc ( sizeof ( int ));
int * q1 = ( int * ) malloc ( sizeof ( int ));
s1 . x = & p1 ;
s1 . y = & q1 ;
* ( s1 . x ) = & g ;
return 0 ;
} Bitcode generieren:
clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll
Die Option -O0 wird verwendet, um die Optimierungen von Klirpern zu deaktivieren. Im Allgemeinen ist es eine gute Idee, Krallenoptimierungen zu ermöglichen. Für triviale Beispiele wie simple.c vereinfacht Clang jedoch zu sehr, so dass nichts Nützliches beobachtet wird. Die Optionen -c -emit-llvm -S erzeugen Bitcode im menschlich -lesbaren Format.
Führen Sie sea-dsa auf dem Bitcode aus und drucken Sie Speicherdiagramme zum DOT-Format:
seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot simple.ll
Die Optionen -sea-dsa=butd-cs -sea-dsa-type-aware werden die in unserem FMCAD'19-Artikel implementierte Analyse (siehe Referenzen). Dieser Befehl generiert für jeden FUN im Bitcode -Programm eine FUN.mem.dot -Datei. In unserem Fall ist die einzige Funktion main , und daher gibt es eine Datei namens main.mem.dot . Die Datei wird im aktuellen Verzeichnis generiert. Wenn Sie die .dot Dateien in einem anderen Verzeichnisspeicher speichern möchten DIR fügen Sie die Option -sea-dsa-dot-outdir=DIR hinzu
Visualisieren Sie main.mem.dot , indem Sie sie in eine pdf -Datei umwandeln:
dot -Tpdf main.mem.dot -o main.mem.pdf
open main.mem.pdf // replace with you favorite pdf viewer
In unserem Speichermodell wird ein Zeigerwert durch eine Zelle dargestellt, die ein Paar eines Speicherobjekts und Offset ist. Speicherobjekte werden im Speicherdiagramm als Knoten dargestellt. Kanten sind zwischen Zellen.
Jedes Knotenfeld repräsentiert eine Zelle (dh einen Versatz im Knoten). Zum Beispiel sind die Knotenfelder <0,i32**> und <8,i32**> die von %6 bzw. %15 gezeigt werden, zwei verschiedene Zellen aus demselben Speicherobjekt. Das Feld <8,i32**> repräsentiert die Zelle bei Offset 8 im entsprechenden Speicherobjekt und sein Typ ist i32** . Schwarze Kanten repräsentieren Punkte zu Beziehungen zwischen Zellen. Sie sind mit einer Zahl gekennzeichnet, die den Offset im Zielknoten darstellt. Blaue Kanten verbinden formale Parameter der Funktion mit einer Zelle. Lila Kanten verbinden LLVM -Zeigervariablen mit Zellen. Knoten können Marker wie S (Stack -zugewiesener Speicher), H (HEAP -Zuordnungsspeicher), M (modifiziertem Speicher), R (Lesespeicher), E (extern zugewiesener Speicher) usw. haben, usw. Wenn ein Knoten rot ist, bedeutet dies, dass die Analyse die Feldempfindlichkeit für diesen Knoten verloren hat. Mit dem Etikett {void} wird bezeichnet, dass der Knoten zugewiesen wurde, aber nicht vom Programm verwendet wurde.
sea-dsa kann auch indirekte Anrufe lösen. Ein indirekter Anruf ist ein Anruf, bei dem die Callee statisch nicht bekannt ist. sea-dsa identifiziert alle möglichen Kallees eines indirekten Aufrufs und generiert ein LLVM-Anrufdiagramm als Ausgabe.
Betrachten Sie dieses Beispiel in tests/c/complete_callgraph_5.c :
struct class_t ;
typedef int ( * FN_PTR )( struct class_t * , int );
typedef struct class_t {
FN_PTR m_foo ;
FN_PTR m_bar ;
} class_t ;
int foo ( class_t * self , int x )
{
if ( x > 10 ) {
return self -> m_bar ( self , x + 1 );
} else
return x ;
}
int bar ( class_t * self , int y ) {
if ( y < 100 ) {
return y + self -> m_foo ( self , 10 );
} else
return y - 5 ;
}
int main ( void ) {
class_t obj ;
obj . m_foo = & foo ;
obj . m_bar = & bar ;
int res ;
res = obj . m_foo ( & obj , 42 );
return 0 ;
}Geben Sie die Befehle ein:
clang -c -emit-llvm -S tests/c/complete_callgraph_5.c -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll
Es generiert eine .dot -Datei namens callgraph.dot im aktuellen Verzeichnis. Auch hier kann die .dot -Datei in eine .pdf -Datei konvertiert und mit den Befehlen geöffnet werden:
dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf
sea-dsa kann auch einige Statistiken zum Aufruf -Graph -Auflösungsprozess ausdrucken (beachten Sie, dass Sie clang mit -g anrufen müssen, um Datei-, Zeilen- und Spalteninformationen zu drucken):
sea-dsa --sea-dsa-callgraph-stats ex.ll
=== Sea-Dsa CallGraph Statistics ===
** Total number of indirect calls 0
** Total number of resolved indirect calls 3
%16 = call i32 %12(%struct.class_t* %13, i32 %15) at tests/c/complete_callgraph_5.c:14:12
RESOLVED
Callees:
i32 bar(%struct.class_t*,i32)
%15 = call i32 %13(%struct.class_t* %14, i32 10) at tests/c/complete_callgraph_5.c:23:16
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
%11 = call i32 %10(%struct.class_t* %2, i32 42) at tests/c/complete_callgraph_5.c:36:9
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
Die Zeigersemantik externer Anrufe kann definiert werden, indem ein Wrapper geschrieben wird, der eine dieser Funktionen aufruft, die in seadsa/seadsa.h definiert sind.
extern void seadsa_alias(const void *p, ...);extern void seadsa_collapse(const void *p);extern void seadsa_mk_seq(const void *p, unsigned sz); seadsa_alias vereint alle p , seadsa_collapse p seadsa_mk_seq dass sea-dsa sea-dsa (dh Verlust der Feldempfindlichkeit) sz
Betrachten Sie beispielsweise einen externen Anruf foo der wie folgt definiert ist:
extern void* foo(const void*p1, void *p2, void *p3);
Nehmen wir an, dass der zurückgegebene Zeiger zu p2 jedoch nicht zu p1 einheitlich sein sollte. Zusätzlich möchten wir die Zelle, p3 entspricht, zusammenbrechen. Anschließend können wir den obigen Prototyp von foo durch die folgende Definition ersetzen:
#include "seadsa/seadsa.h"
void* foo(const void*p1, void *p2, void*p3) {
void* r = seadsa_new();
seadsa_alias(r,p2);
seadsa_collapse(p3);
return r;
}
"Ein kontextempfindliches Gedächtnismodell zur Überprüfung von C/C ++-Programmen" von A. Gurfinkel und JA Navas. In Sas'17. (Papier) | (Folien)
"Einheitliche Zeigeranalyse ohne Überschreibung" von J. Kuderski, Ja Navas und A. Gurfinkel. In fmcad'19. (Papier)
