Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25838
Titel: Programmanalyse des XRTL Zwischencodes
Verfasser: Backes, Werner
Sprache: Deutsch
Erscheinungsjahr: 2004
SWD-Schlagwörter: Theoretische Informatik
Freie Schlagwörter: XRTL Zwischencode
xGCC
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: In dieser Arbeit stellen wir das Analysetool xGCC vor. Dieses Tool analysiert den XRTL Zwischencode, um Sicherheitseigenschaften, z.B. Speicherüberlauf, die Division durch Null und die Verwendung von uninitialisierten Variablen oder Speicherstücken, zu verifizieren. XRTL ist eine von uns entwickelte Erweiterung der Register Transfer Language (RTL). Dieser sprachunabh ängige Zwischencode wird von Frontends der GNU Compiler Collection (GCC) für verschiedene Programmiersprachen, wie z.B. C, C++, Java und Fortran 77, erzeugt. xGCC unterstützt diese Programmiersprachen, da sich unsere Compilermodifikationen auf den sprachunabhängigen Teil des Compilers beschränken. Für die Analyse von XRTL setzen wir die abstrakte Interpretation ein. Wir verwenden Listen von gültigen Intervallen, um Mengen von benötigten Registern und Speicherstücken darzustellen. Gültige Intervalle sind Intervalle für die zusätzlichen Bedingungen gelten, um die Implementierung der XRTL Operationen zu erleichtern. Die Präzision der Approximation ist durch die Listenlänge einstellbar. Wir zeigen, wie einfache und parallele XRTL Anweisungen abgearbeitet werden.Wir leiten Constraints aus der Bedingung von Verzweigungen ab, um den Suchraum einzuschränken. Wir verwenden das Widening/Narrowing, um die Fixpunktberechnung für XRTL Scheifen zu beschleunigen. Wir stellen die Implementierung von xGCC vor und erläutern die getroffenen Designentscheidungen. Mit Hilfe ausgewählter Beispiele demonstrieren wir verschiedene Klassen von Fehlern, die das Analysetool xGCC entdeckt. Wir untersuchen das Laufzeitverhalten der Analyse mit Beispielen aus den Numerical Recipes in C und stellen verschiedene Optimierungen vor.
We present the xGCC analysis tool for the verification of safety properties of the XRTL intermediate code. These properties include the absence of buffer overow, division by zero and the use of uninitialized variables and memory. XRTL is our extension of the Register Transfer Language (RTL). This language independent intermediate code is generated by frontends of the GNU Compiler Collection (GCC) for the programming languages C, C++, Java and Fortran 77. These programming languages are supported by xGCC since we have modified only the language independent part of the compiler. We apply abstract interpretation for the analysis of XRTL. Lists of valid intervals are used for the abstraction of sets of registers and memory blocks. Valid intervals are intervals with additional contraints that simplify the implementation of the XRTL operations. The precision of the abstraction is parameterized by the list length. We describe the interpretation of sequential and parallel XRTL instructions.We take branching conditions into account for restricting the search space, and apply the Widening/Narrowing techniques to speed up the fixpoint computation for XRTL loops. We present the implementation of xGCC and explain the tool design.We demonstrate xGCC analysis tool on a collection of examples.We analyse the tool performance on examples from the Numerical Recipes in C, and introduce several optimizations.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-4566
hdl:20.500.11880/25894
http://dx.doi.org/10.22028/D291-25838
Erstgutachter: Andreas Podelski
Tag der mündlichen Prüfung: 7-Jan-2004
SciDok-Publikation: 23-Jun-2005
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Dissertation_2522_Backes_Werner_2004.pdf536,35 kBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.