AIB 2014-08: Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs

[Thomas Ströder]

The following technical report is available from
http://aib.informatik.rwth-aachen.de:

Generating Inductive Predicates for Symbolic Execution of
Pointer-Manipulating Programs
Christina Jansen, Florian Gï¿œbe, and Thomas Noll
AIB 2014-08

Separation Logic (SL) is an extension of Hoare Logic that supports
reasoning about pointer-manipulating programs. It employs
inductively-defined predicates for specifying the (dynamic) data
structures maintained at runtime, such as lists or trees. To support
symbolic execution, SL introduces abstraction rules that yield symbolic
representations of concrete heap states. Whenever concrete program
instructions are to be applied, so-called unrolling rules are used to
locally concretise the symbolic heap. To enable automatic generation of
a complete set of unrolling rules, however, predicate definitions have
to meet certain requirements, which are currently only implicitly
specified and manually established.

To tackle this problem, we exploit the relationship between SL and
hyperedge replacement grammars (HRGs). The latter represent (abstracted)
heaps by hypergraphs containing placeholders whose interpretation is
specified by grammar rules. Earlier work has shown that the correctness
of heap abstraction using HRGs requires certain structural properties,
such as increasingness, which can automatically be established. We show
that it is exactly the Separation Logic counterparts of those properties
that enable a direct generation of abstraction and unrolling rules from
predicate definitions for symbolic execution.

Technically, this result is achieved by first providing formalisations
of the structural properties in SL. We then extend an existing
translation between SL and HRGs such that it covers all HRGs describing
data structures, and show that it preserves these structural properties.