Please use this identifier to cite or link to this item:
doi:10.22028/D291-25716
Title: | Generating program analyzers |
Other Titles: | Generierung von Programmanalysatoren |
Author(s): | Martin, Florian |
Language: | English |
Year of Publication: | 1999 |
SWD key words: | Programmanalyse ; Generator <Informatik> ; Implementierung |
DDC notations: | 004 Computer science, internet |
Publikation type: | Dissertation |
Abstract: | In this work the automatic generation of program analyzers from
concise specifications is presented. It focuses on provably correct
and complex interprocedural analyses for real world sized imperative
programs. Thus, a powerful and flexible specification mechanism
is required, enabling both correctness proofs and efficient
implementations. The generation process relies on the theory of
data flow analysis and on abstract interpretation. The theory of
data flow analysis provides methods to efficiently implement analyses.
Abstract interpretation provides the relation to the semantics
of the programming language. This allows the systematic derivation
of efficient provably correct, and terminating analyses. The
approach has been implemented in the program analyzer generator
PAG. It addresses analyses ranging from "simple'; intraprocedural
bit vector frameworks to complex interprocedural alias
analyses. A high level specialized functional language is used as
specification mechanism enabling elegant and concise specifications
even for complex analyses. Additionally, it allows the automatic
selection of efficient implementations for the underlying
abstract datatypes, such as balanced binary trees, binary decision
diagrams, bit vectors, and arrays. For the interprocedural analysis
the functional approach, the call string approach, and a novel
approach especially targeting on the precise analysis of loops can
be chosen. In this work the implementation of PAG as well as a
large number of applications of PAG are presented. Diese Arbeit befaßt sich mit der automatischen Generierung von Programmanalysatoren aus prägnanten Spezifikationen. Dabei wird besonderer Wert auf die Generierung von beweisbar korrekten und komplexen interprozeduralen Analysen für imperative Programme realer Größe gelegt. Um dies zu erreichen, ist ein leistungsfähiger und flexibler Spezifikationsmechanismus erforderlich, der sowohl Korrektheitsbeweise, als auch effiziente Implementierungen ermöglicht. Die Generierung basiert auf den Theorien der Datenflußanalyse und der abstrakten Interpretation. Die Datenflußanalyse liefert Methoden zur effizienten Implementierung von Analysen. Die abstrakte Interpretation stellt den Bezug zur Semantik der Programmiersprache her und ermöglicht dadurch die systematische Ableitung beweisbar korrekter und terminierender Analysen. Dieser Ansatz wurde im Programmanalysatorgenerator PAG implementiert, der sowohl für einfache intraprozedurale Bitvektor- Analysen, als auch für komplexe interprozedurale Alias-Analysen geeignet ist. Als Spezifikationsmechanismus wird dabei eine spezialisierte funktionale Sprache verwendet, die es ermöglicht, auch komplexe Analysen kurz und prägnant zu spezifizieren. Darüberhinaus ist es möglich, für die zugrunde liegenden abstrakten Bereiche automatisch effiziente Implementierungen auszuwählen, z.B. balancierte binäre Bäume, Binary Decision Diagrams, Bitvektoren oder Felder. Für die interprozedurale Analyse stehen folgende Möglichkeiten zur Auswahl: der funktionale Ansatz, der Call-String-Ansatz und ein neuer Ansatz, der besonders auf die präzise Analyse von Schleifen abzielt. Diese Arbeit beschreibt sowohl die Implementierung von PAG, als auch eine große Anzahl von Anwendungen. |
Link to this record: | urn:nbn:de:bsz:291-scidok-2039 hdl:20.500.11880/25772 http://dx.doi.org/10.22028/D291-25716 |
Advisor: | Reinhard Wilhelm |
Date of oral examination: | 22-Oct-1999 |
Date of registration: | 26-Apr-2004 |
Faculty: | MI - Fakultät für Mathematik und Informatik |
Department: | MI - Informatik |
Collections: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Files for this record:
File | Description | Size | Format | |
---|---|---|---|---|
FlorianMartin_ProfDrReinhardWilhelm.pdf | 1,4 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.