Shape-based alias analysis for object-oriented languages

Abstract

Eine Shape Analyse ist eine statische Programmanalyse, die Eigenschaften verketteter Datenstrukturen im dynamischen Speicher untersucht. Üblicherweise wird sie zur Übersetzungszeit eingesetzt um Programmeigenschaften zu überprüfen und Fehler zu finden.<br />Ziel dieser Arbeit ist es parametrisierte Versionen von zwei Shape Analysen zu vergleichen: die SRW Analyse, wie sie in ``Solving shape-analysis problems in languages with destructive updating'' (M.<br />Sagiv, T. Reps, R. Wilhelm) beschrieben wird. Sie war die erste Shape Analyse, die für Programmknoten die Zeigerwerte ändern `strong updates' durchführen konnte. Die zweite Analyse, in Folge NNH genannt, basiert auf der vorigen Analyse, verwaltet ihre Information zu jedem Programmpunkt aber in einer Menge von Shape Graphen anstatt die Analyseinformation in einem einzelnen Zusammenfassungsgraphen zu halten.<br />Diese Analyse ist in dem Buch ``Principles of Program Analysis'' (F.<br />Nielson, H.R. Nielson, C. Hankin) beschrieben.<br />Für den Vergleich wurden beide Analysen für C++ mit dem SATIrE Programmanalyse Framework implementiert. Ein Algorithmus der eine endliche konservative Menge von May-Aliasen aus einem gegebenem Shape Graphen berechnen kann wurde entwickelt. Die Genauigkeit der beiden Analysen wird an der Qualität der May-Alias Mengen gemessen, die aus den Ergebnissen der Shape Analysen extrahiert werden, wobei kleinere Mengen ein genaueres Ergebnis der Shape Analyse anzeigen. Ergebnisse von Experimenten zeigen die relative Qualität von parametrisierten Versionen beider Shape Analysen und die Auswirkung der Parameter auf Genauigkeit und Analyselaufzeit.<br />

Shape analysis is a static code analysis technique discovering properties of linked data structures allocated in the heap. It is typically used at compile time to find software bugs or to verify high-level correctness properties.<br />Aim of this work is to evaluate merits and drawbacks of parametrized versions of two shape analyses: the SRW analysis, as described by ``Solving shape-analysis problems in languages with destructive updating'' (M. Sagiv, T. Reps, R. Wilhelm), which was the first to achieve strong update of pointer values for statements that modify pointer values. The second analysis, termed NNH, is based on the former but uses sets of shape graphs as abstraction instead of merging the analysis information into summary shape graphs. This shape analysis is described in the book ``Principles of Program Analysis'' (F. Nielson, H.R. Nielson, C. Hankin).<br />To facilitate evaluation, both analyses were implemented for C++ using the SATIrE program analysis framework. An algorithm that computes a finite conservative set of may-aliases from a given shape graph has been developed. The precision of the shape analysis algorithms is measured by the size of extracted may-alias sets, where smaller sets indicate a more precise shape analysis. Experimental results show the relative quality of parametrized versions of both shape analyses and the impact that the parameters have on precision and runtime.<br />