FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Shape Neutral Analysis of Graph-based Data-structures

Authors: Gregory Duck, Joxan Jaffar and Roland Yap

Paper Information

Title:Shape Neutral Analysis of Graph-based Data-structures
Authors:Gregory Duck, Joxan Jaffar and Roland Yap
Proceedings:ICLP Proceedings of ICLP 2018
Editors: Paul Tarau and Alessandro Dal Palu'
Keywords:Constraint Handling Rules, Satisfiability Modulo Constraint Handling Rules, Satisfiability Modulo Theories, Program Analysis, Data-structures, Memory Errors
Abstract:

ABSTRACT. Malformed data-structures can lead to runtime errors such as arbitrary memory access or corruption. Despite this, reasoning over data-structure properties for low-level heap manipulating programs remains challenging. In this paper we present a constraint-based program analysis that checks data-structure integrity, w.r.t. given target data-structure properties, as the heap is manipulated by the program. Our approach is to automatically generate a solver for properties using the type definitions from the target program. The generated solver is implemented in Constraint Handling Rules (CHR) extending builtin heap, integer and equality solvers. A key property of our program analysis is that the target data-structure properties are shape neutral, i.e. the analysis does not check for properties relating to a given data-structure graph shape, such as doubly-linked-lists versus trees. Nevertheless, the analysis can detect errors in wide range of datastructure manipulating programs, including those that use lists, trees, DAGs, graphs, etc. We present an implementation based on a specialized shape neutral constraint solver implemented in the Satisfiability Modulo Constraint Handling Rules (SMCHR) system. Experimental results show that our approach works well for real-world C programs.

Pages:14
Talk:Jul 17 14:00 (Session 121D: Probabilistic and Constraint LP)
Paper: