Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs
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.