Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic

Jansen, Christina; Huisman, Marieke; Noll, Thomas; Katoen, Joost-Pieter

doi:36624

Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic = Statische Analyse von Zeigerprogrammen - Integration von Graphgrammatiken und Separation Logic

Jansen, Christina^RWTH*

2017

Verantwortlichkeitsangabevorgelegt von Diplom-Informatikerin Christina Maria Jansen

ImpressumAachen 2017

Umfang1 Online-Ressource (xi, 286 Seiten) : Diagramme

Dissertation, RWTH Aachen University, 2017

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor) ; Huisman, Marieke (Thesis advisor) ; Noll, Thomas (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2017-10-19

Online
DOI: 10.18154/RWTH-2017-09657
URL: http://publications.rwth-aachen.de/record/708116/files/708116.pdf
URL: http://publications.rwth-aachen.de/record/708116/files/708116.pdf?subformat=pdfa

Einrichtungen

Projekte

CARP - Correct and Efficient Accelerator Programming (287767) (287767)

Inhaltliche Beschreibung (Schlagwörter)
heap abstraction (frei) ; heap manipulation (frei) ; hyperedge replacement grammar (frei) ; separation logic (frei) ; static analysis (frei)

Thematische Einordnung (Klassifikation)
DDC: 530

Kurzfassung
In dieser Dissertation wird ein Framework zur abstrakten Analyse von Zeigerprogrammen vorgestellt, dessen Einsatzgebiet prozedurale, rekursive und nebenläufige Programme umfasst. Den Grundstein des Frameworks bildet eine auf Hypergraphen basierende Repräsentation des Heaps. Hypergraphen stellen eine Verallgemeinerung von herkömmlichen Graphen dar, in der Kanten beliebig viele Knoten verbinden können und eine Beschriftung tragen. Durch diese Generalisierung bringen Hypergraphen alle notwendigen Voraussetzungen zur Heapabstraktion mit: Während Kanten zwischen zwei Knoten als Zeiger aufgefasst werden, fungieren alle übrigen Kanten als Platzhalter. Diese Platzhalter können durch Heapteile ersetzt werden, deren Struktur von sogenannten Hyperedge Replacement-Grammatiken formal beschrieben wird. Konkretisierung und Abstraktion der Heaprepräsentation entspricht der Anwendung von Produktionsregeln der Grammatik: eine Rückwärtsanwendung abstrahiert den Heap, während eine Vorwärtsanwendung einer Konkretisierung entspricht. Im ersten Teil der Dissertation werden die formalen Voraussetzungen für die Heaprepräsentation sowie ihrer Konkretisierung und Abstraktion geschaffen. Auf dieser Grundlage wird ein Ansatz zur Analyse von nicht-prozeduralen Zeigerprogrammen vorgestellt. Dazu werden alle Anforderungen an Hyperedge Replacement-Grammatiken erarbeitet, die für eine korrekte und terminierende Konkretisierung und Abstraktion nötig sind. Weiterhin wird die Konstruktion einer äquivalenten, diese Eigenschaften erfüllenden Grammatik adressiert. Der zweite Teil der Dissertation schlägt eine Brücke in Form eines beidseitigen Übersetzungsalgorithmus zwischen Hyperedge Replacement-Grammatiken und dem symbolic heap-Fragment der Separation Logic. Neben dem Korrektheitsbeweis der Übersetzung werden die Gegenstücke der Anforderungen an Hyperedge Replacement-Grammatiken aus dem ersten Teil für die Separation Logic definiert und ihre Erhaltung während der Übersetzung bewiesen. Die hergestellte Beziehung zwischen Separation Logic und Hyperedge Replacement-Grammatiken bildet den Grundstein für die Erweiterung des Analyseframeworks. Im letzten Teil dieser Dissertation wird das Spektrum der analysierbaren Zeigerprogramme auf prozedurale sowie nebenläufige Programme ausgedehnt. Dazu bedienen wir uns des Konzepts der Contracts, die bereits im Bereich der Zeigerprogrammanalyse mithilfe von Separation Logic erfolgreich eingesetzt werden. Ein Contract bildet ein Paar aus Vor- und Nachbedingung, wobei die Nachbedingung den Effekt einer Prozedur oder eines Threads auf die Vorbedingung erfasst. Damit erlaubt er eine modulare Analyse von Programmen auf Prozedur- bzw. Threadebene. Um auch im Fall von nebenläufigen Programmen Threads unabhängig voneinander untersuchen zu können, werden zusätzlich so genannte Permissions, d.h. Berechtigungen zum Lesen oder Schreiben von Teilen des Heaps, eingeführt. Auch hier handelt es sich um ein Konzept, das für die Separation Logic etabliert ist. Das Hauptresultat des letzten Dissertationsteils besteht in der Erarbeitung eines neuartigen Ansatzes, der zu einem Zeigerprogramm sowohl Prozedur- als auch (Permission-annotierte) Threadcontracts automatisiert generiert.

This thesis presents a sound abstraction framework for the static analysis of pointer programs, which is able to handle (recursive) procedures as well as concurrency. The framework builds on a graph representation of the heap using so-called hypergraphs. In these graphs edges are labelled and can be connected to arbitrarily many vertices. Understanding edges between two vertices as pointers and the remaining edges as placeholders for parts of the heap, hypergraphs feature the necessary concepts for heap abstraction. More concretely, edge labels are used to specify the shape of the heap that is abstracted. Hyperedge replacement grammars formalise this mapping. That is, they define the data structures each of the labels represents. Concretisation and abstraction of heaps then directly correspond to forward and backward application of production rules of the hyperedge replacement grammar, respectively. The first part of the thesis lays the formal foundation for hypergraph-based heap representation and its concretisation and abstraction. Utilising this, an analysis approach for non-procedural pointer programs is presented. Additionally, we make requirements of hyperedge replacement grammars that are crucial for the soundness and termination of concretisation and abstraction. It is shown that each hyperedge replacement grammar can be transformed such that it satisfies these requirements. In the second part of the thesis, a bridge between hyperedge replacement grammars and the symbolic heap fragment of Separation Logic is built. In particular, a translation procedure between both formalisms is given and proven correct. Additionally, we provide the Separation Logic counterparts of the requirements determined in the preceding part and show that they are preserved by the translation. The relationship between Separation Logic and hyperedge replacement grammars inspired the extension to a framework that modularly handles procedures and fork-join-concurrency. That is, in the last part of the thesis we adopt the concept of contracts, i.e. pairs consisting of a pre- and a postcondition that capture the effect of a procedure or thread execution, to obtain procedure and thread modular analyses, respectively. In the latter case, we additionally introduce permissions to hypergraphs. They constitute a concept which is, similarly to contracts, well-understood for Separation Logic. Permissions provide transferable access grants to heap parts and enable the analysis of threads independently of each other. As a main contribution of the procedural and concurrent program analysis, a novel approach for automated derivation of procedure and (permission-enriched) thread contracts is presented.

OpenAccess:
PDF PDF (PDFA)
(additional files)