Abstract Maintaining software is cumbersome when method argument constraints are undocumented. To reveal them, previous work learned preconditions from exemplary valid and invalid method arguments. In practice, it would be highly beneficial to know class invariants, too, because functionality added during software maintenance must not break them. Even more so than method preconditions, class invariants are rarely documented and often cannot completely be inferred automatically, especially for objects exhibiting complex state such as dynamic data structures. This paper presents a novel dynamic approach to learning class invariants, thereby complementing related work on learning method preconditions. We automatically synthesize assertions from an adjustable assertion grammar to distinguish valid and invalid objects. While random walks generate valid objects, a combination of bounded-exhaustive testing techniques and behavioral oracles yield invalid objects. The utility of our approach for code comprehension and software maintenance is demonstrated by comparing our learned invariants to documented invariant validation methods found in real-world Java classes and to the invariants detected by the Daikon tool.

Understanding complex software components is crucial for software evolution and maintenance. While documentation on software behavior is often available and sufficient for software reusability, maintenance requires additional information such as internal state constraints. While, these constraints, typically encoded as class invariants in object-oriented programming, are rarely documented, dynamic class invariant learning approaches can be used to extract candidate invariants from concrete object states. Recent approaches leverage negative training data to assess invariant completeness; however, a diverse set of invalid object states is particularly challenging to obtain. This paper proposes a novel approach for the automatic creation of invalid objects by combining program mutation with object state space exploration, thereby reaching invalid objects that cannot be constructed using the original class definition. Evaluating our approach on data structures, including those from the java.util package, revealed that it achieves a high object state space coverage. This demonstrates its potential for generating a diverse set of invalid objects suitable for class invariant learning.

Analyzing heap dumps containing complex dynamic data structures is essential when debugging modern software systems. However, existing tools for visualizing memory graphs can neither deal with corrupt structures such as binary trees exhibiting cycles, nor do they offer adequate abstractions when being confronted with large heaps. This paper presents MGE (Memory Graph Explorer), a memory analyzer and visualizer that combines a novel memory graph abstraction with an interactive visualization. MGE borrows ideas from separation logic and shape analysis to reveal relationships between memory nodes, name recognized structures such as doubly-linked lists and binary trees, and summarize complex structures. This summarization works for corrupt data structures, too, and is particularly powerful for large, nested structures due to its support for interactive (un)folding. MGE's utility for aiding program comprehension is illustrated by real-world and textbook examples and contrasted with existing debuggers.

Visualizing large memory graphs containing dynamic data structures and nested payload data is crucial when debugging legacy and modern software. However, existing visualization tools primarily focus on aggregating data structures and either rely on hard-coded patterns, generic heuristics, or predicates written in expressive logics. We present a novel heap pattern language for concisely and intuitively describing structural aspects of dynamic data structures and nested payload data. Evaluating a heap pattern on a memory graph yields a set of matching groups of interconnected objects, and analyzing these groups enables the construction of a multi-level hierarchy for memory graph visualization, where groups can individually be (un)folded to the desired level of detail. We have prototypically implemented our heap pattern language in the Memory Graph Explorer tool and illustrate its use for visualizing large memory graphs on real-world and textbook examples. Unlike existing tools, developers can now control the construction of hierarchies using heap patterns to flexibly and locally adjust the level of memory graph abstraction in an interactive graph visualization to highlight the areas demanding attention during debugging.

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.

Reverse engineering binary code is notoriously difficult and, especially, understanding a binary's dynamic data structures. Existing data structure analyzers are limited wrt. program comprehension: they do not detect complex structures such as skip lists, or lists running through nodes of different types such as in the Linux kernel's cyclic doubly-linked list. They also do not reveal complex parent-child relationships between structures. The tool DSI remedies these shortcomings but requires source code, where type information on heap nodes is available. We present DSIbin, a combination of DSI and the type excavator Howard for the inspection of C/C++ binaries. While a naive combination already improves upon related work, its precision is limited because Howard's inferred types are often too coarse. To address this we auto-generate candidates of refined types based on speculative nested-struct detection and type merging; the plausibility of these hypotheses is then validated by DSI. We demonstrate via benchmarking that DSIbin detects data structures with high precision.