This paper presents a novel algorithm for automatically learning recursive shape pred- icates from memory graphs, so as to formally describe the pointer-based data structures contained in a program. These predicates are expressed in separation logic and can be used, e.g., to construct efficient secure wrappers that validate the shape of data structures exchanged between trust boundaries at runtime. Our approach first decomposes memory graph(s) into sub-graphs, each of which exhibits a single data structure, and generates candidate shape predicates of increasing complexity, which are expressed as rule sets in Prolog. Under separation logic semantics, a meta-interpreter then performs a systematic search for a subset of rules that form a shape predicate that non-trivially and concisely captures the data structure. Our algorithm is implemented in the prototype tool ShaPE and evaluated on examples from the real-world and the literature. It is shown that our approach indeed learns concise predicates for many standard data structures and their implementation variations, and thus alleviates software engineers from what has been a time-consuming manual task.
Integrating program and algorithm visualisation for learning data structure implementation
