Java program analysis by symbolic execution

Otto, Carsten; Giesl, Jürgen; Spoto, Fausto

doi:34599

Java program analysis by symbolic execution = Java-Programmanalyse durch symbolische Auswertung

Otto, Carsten

2015 & 2015

VerantwortlichkeitsangabeCarsten Otto

ImpressumAachen : Fachgruppe Informatik, RWTH Aachen University 2015

Umfang223 S. : graph. Darst.

ReiheAachener Informatik-Berichte Technical report / Department of Computer Science, RWTH Aachen ; 2013,16

Zugl.: Aachen, Techn. Hochsch., Diss., 2015

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor) ; Spoto, Fausto (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2015-03-03

Online
URN: urn:nbn:de:hbz:82-rwth-2015-013732
URL: https://publications.rwth-aachen.de/record/464568/files/464568.pdf
URL: https://publications.rwth-aachen.de/record/464568/files/464568.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
In der Informatik hat die Programmanalyse eine lange Geschichte. Selbst wenn man nur den wichtigen Bereich der Terminierungsanalyse betrachtet, wurde in den letzten Jahrzehten eine überwältigende Anzahl von neuen Techniken erforscht.Während die meisten dieser Ansätze ursprünglich mehr von theoretischem als praktischem Nutzen waren, wurden in der letzten Zeit auch automatische Analysenfür imperative Programmiersprachen wie C oder Java entwickelt. Dabei ist der Umgang mit Sprachkonstrukten und -konzepten, die in einfacheren Sprachen nicht existieren, eine große Herausforderung. Beispielsweise verwendet man in Java dynamische Bindung, komplexe Objekthierarchien oder Seiteneffekte mit weitreichenden Konsequenzen im gesamten Speicher. In dieser Arbeit präsentieren wir einen Vorverarbeitungsschritt für JBC-Programme, in dem alle komplizierten Sprachkonstrukte behandelt werden. Dadurch ist es in nachfolgenden Analyseschritten nicht mehr erforderlich sich damit zu beschäftigen, und die Anwendung bereits existierender Techniken wird vereinfacht. Insbesondere zeigen wir, wie symbolische Auswertungsgraphen konstruiert werden können, welche eine Überabschätzung aller möglichen Programmabläufe enthalten. Dadurch, dass diese Abschätzung möglichst präzise ist, können die in den konstruierten Graphen enthaltene Informationen beispielsweise verwendet werden, um über das Terminierungsverhalten des ursprünglichen Programms zu argumentieren. Zusätzlich zur Konstruktion solcher Graphen stellen wir in dieser Arbeit eine neue Analysetechnik vor, die es dem Endbenutzer ermöglicht Teile des analysierten Codes zu identifizieren, die für das gewünschte Ergebnis irrelevant sind. Dadurch können Programmierfehler, die sonst zu nicht ausgeführtem Code führen, identifiziert und schließlich auch vom Benutzer korrigiert werden. Damit diese Technik praktisch verwendbar ist, müssen die in den vorher erzeugten Graphen vorhandenen Informationen präzise sein. Wir werden demonstrieren, dass dies der Fall ist. Für die in dieser Arbeit vorgestellten Techniken wird eine rigorose Formalisierung gezeigt. Um das übergreifende Ziel von beispielsweise automatischer Terminierungsanalyse zu erreichen, müssen die Techniken und theoretischen Ergebnisse implementiert werden. In dieser Arbeit zeigen wir, wie bestimmte schwer zu automatisierende Aspekte angegangen werden können, und zeigen, dass diese Ansätze zu wettbewerbsfähigen Resultaten führen. Die in dieser Arbeit präsentierten Techniken sind im Software-Tool AProVE implementiert. Da auch verwandte Techniken, die auf symbolischen Auswertungsgraphen arbeiten, in AProVE implementiert sind, kann der Benutzer durch Drücken eines Knopfes JBC-Programme analysieren und auf (Nicht-)Terminierung untersuchen und irrelevanten Code finden. Im jährlichen internationalen Terminierungs-Wettbewerb wird gezeigt, dass AProVE aktuell das stärkste Tool zur Terminierungs-Analyse von JBC-Programmen ist.

Program analysis has a long history in computer science. Even when only considering the important aspect of termination analysis, in the past decades an overwhelming number of different techniques has been developed. While the programming languages considered by these approaches initially were more of theoretical importance than of practical use, recently also automated analysesfor imperative programming languages like C or Java have been developed. Here, a major challenge is to deal with language constructs and concepts which do not exist in simpler languages. For example, in Java one often uses dynamic dispatch, complex object hierarchies, or side-effects with far-reaching consequences involving the global heap. In this thesis, we present a preprocessing step for JBC programs in which all such complicated language constructs are handled. This way, subsequent analyses do not need to be concerned with these, and making use of existing techniques is easy. In particular, we show how Symbolic Execution Graphs can be constructed which contain an over-approximation of all possible program runs. This way, and by taking care of having a precise approximation, the information contained in the constructed graphs can, for example, be used to reason about the termination behavior of the original program. Additionally to the construction of such graphs, in this thesis we present a new analysis technique which helps end users identify parts of the analyzed code which are irrelevant for the desired outcome. This way, programming errors causing code to be not executed can be identified and, consequently, fixed by the user. For this technique to be useful, the information containedin the previously constructed graph needs to be precise. We will demonstrate that this is the case. For the techniques presented in this thesis, a rigorous formalization is shown. To comply with the overall goal of, for example, automated termination analysis, we also need to implement the techniques and theoretical results. In this thesis we show how certain hard to automate aspects can be approached, leading to a competitive implementation. The techniques presented in this thesis are implemented in the AProVE tool. As also related techniques working on Symbolic Execution Graphs are implemented in AProVE, with the click of a button users can analyze JBC programs for (non)termination and find irrelevant code. In the annual International Termination Competition, it is demonstrated that currently AProVE is the most powerful termination analyzer for JBC programs.

OpenAccess:
PDF PDF (PDFA)
(additional files)