Eine Entscheidungsprozedur für Separation-Logic mit Daten

Abstract

Separation Logic (zu Deutsch etwa "Trennungslogik") ist eine Erweiterung des Hoare-Kalküls, welche logische Schlussfolgerungen über imperative Computer-Programme, die dynamische Heap-Speicher verwenden, erlaubt. Es ist ein beliebter Formalismus für Programme, welche dynamische Ressourcen manipulieren und wird bereits industriell eingesetzt. Die große Ausdruckskraft der Separation Logic erlaubt es modular komplizierte Konzepte, wie dynamisch allokierte Arrays, uneingeschränkte Zeigerarithmetik und rekursive Prozeduren abzubilden. SL_data* ist ein Fragment der Separation Logic, die auf einen Kompromiss zwischen Ausdruckskraft und Komplexität abzielt und ermöglicht Aussagen über im Heap-Speicher gespeicherte Daten zu treffen. Dabei liegen das Erfüllbarkeits-Problem in NP und das Gültigkeits-Problem von Implikationen in coNP. SL_data* kann auf Theorien reduziert werden, welche in gängigen SMT-Solvern verfügbar sind, und zur Darstellung von Daten eine beliebige Theorie verwenden. Mit SLOTH existiert bereits eine Implementierung der Entscheidungsprozedur, diese ist jedoch noch eingeschränkt. SL_data* erlaubt das Auswählen einer Adress- sowie Datentheorie, was jedoch von SLOTH nicht unterstützt wird. Zusätzlich wurde SLOTH noch nicht auf Performance optimiert und die Entscheidungen für einige Probleminstanzen dauern sehr lange. Wir schlagen Optimierungen für die SL_data*-Entscheidungsprozedur vor. Zusätzlich haben wir die Entscheidungsprozedur sowie die Optimierungen implementiert und einige Einschränkungen von SLOTH überwunden. Die Prozedur wurde in Z3, einem gängigen SMT-Solver integriert. Wir zeigen, die Effektivität der Optimierungen mit einer empirischen Studie.

Separation Logic is an extension of Hoare Logic that allows reasoning about imperative programs that use dynamic data structures. It is a popular formalism for programs that manipulate the heap and on top of that has been proven on an industrial scale. Its expressive power permits modular definitions of complex concepts like dynamically allocated arrays, unrestricted pointer arithmetic and recursive procedures and data structures. SL_data* is a Separation Logic fragment with emphasis on data constraints and decidability. It aims to strike a balance between expressibility and complexity, with satisfiability being decidable in NP and entailment in coNP. SL_data* can be encoded into theories supported by off-the-shelf SMT-solvers and can be combined with arbitrary data theories. While with SLOTH a decision procedure implementation exists, it is still limited. The theory allows for configurable location and data sorts, but is not supported by SLOTH. Moreover, SLOTH has not yet been optimised for performance and the decision of some specific instances takes a long time. We propose optimisations for the decision procedure of SL_data*. In addition, have implemented the decision procedure that overcomes some of the current limits of SLOTH and integrated it within Z3, a state-of-the-art SMT solver. We show the effectiveness of the proposed optimisations with empirical benchmarks.