Burgstaller, B. (2005). Symbolic evaluation of imperative programming languages [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-11235
Symbolische Analyse ist eine statische Programmanalysemethode, die Daten- und Kontrollflussinformation an wohldefinierten Programmpunkten beschreibt. Information dieser Art ist von großer Bedeutung für Test und Verifikation von Programmen, sowie für Laufzeitabschätzungen und Programmparallelisierung. Weiters ist symbolische Analyse für optimierende Compiler sowie für Codegeneratoren von Bedeutung.<br />Gegenstand dieser Dissertation ist ein neuer Ansatz in der symbolischen Analyse, der auf Pfadausdrücken beruht. Pfadausdrücke werden bei diesem Ansatz dazu verwendet, die Kontrollflusseigenschaften eines Programms zu erfassen. Einen wesentlichen Teil der Arbeit stellt jene algebraische Struktur dar, in der die symbolische Analyse stattfindet.<br />Wir beschreiben Syntax und Semantik einer einfachen Turing-äquivalenten Fluss-Sprache, die uns als Basis für die Definition dieser Struktur dient. In ihrem Mittelpunkt steht der Superkontext, mit dessen Hilfe wir die möglichen Variablenbindungen an einem wohldefinierten Programmpunkt beschreiben.<br />Um den Seiteneffekt eines Eingabeprogramms zu beschreiben, bilden wir seine einzelnen Programmanweisungen auf Funktionen ab, die ihrerseits einen Superkontext auf einen Superkontext abbilden.<br />Pfadausdrücke werden sodann im Kontext dieser Funktionen interpretiert, womit wir eine funktionale Beschreibung des Eingabeprogramms erhalten. Ein Korrektheitsbeweis sichert die Richtigkeit dieser funktionalen Beschreibung im Hinblick auf die konkrete Semantik der Fluss-Sprache ab.<br />Die beschriebene Methode der symbolischen Analyse ist weniger komplex als existierende Methoden, da sie im Wesentlichen aus der Anwendung der funktionalen Programmbeschreibung auf einen Superkontext besteht. Das Ergebnis dieser Funktionsanwendung ist wiederum ein Superkontext, der die Variablenbindungen nach Ausführung des jeweiligen Eingabeprogramms beschreibt.<br />Die beschriebene Methode kann weiters Lösungen für beliebige Programmpunkte reduzibler sowie irreduzibler Kontrollflussgraphen berechnen und ist damit mächtiger als existierende Methoden.<br />
de
Symbolic analysis is a static program analysis technique that captures data and control flow information at well-defined program points. This information is useful in the areas of program verification, program testing, worst case execution time analysis, and parallelization. Optimizing compilers and code generators can also benefit from the type of information provided by symbolic analysis.<br />In this thesis we take a novel approach to symbolic analysis that is based on path expressions.<br />Path expressions allow us to capture the control flow information that is inherent in a program.<br />By reinterpreting path expressions we obtain a mapping from the path expression algebra into the symbolic analysis domain.<br />A major topic of this thesis is therefore the symbolic analysis domain itself. We describe syntax and semantics of a simple yet Turing-equivalent flow language which serves as the basis for the definition of this domain. At the heart of it is the supercontext, an algebraic structure capable of describing all possible variable bindings valid at a well-defined program point.<br />To describe the computational effects of the input program, we map single statements to functions from supercontexts to supercontexts.<br />The reinterpretation of path expressions takes place in the context of these functions, thus obtaining a functional description of the input program.<br />We develop a proof that establishes the correctness of these functional descriptions with respect to the concrete semantics of the flow language.<br />Our method is less complex than existing methods in the sense that it reduces to the application of the functional description to a given supercontext, yielding a supercontext describing the variable bindings valid after execution of the corresponding input program.<br />It is more general than existing methods because it can derive solutions for arbitrary graph nodes of reducible and irreducible flow graphs.
