Debug-Localize-Repair: A Symbiotic Construction for Heap Manipulations

TL;DR

Wolverine2 is an integrated environment that combines debugging, localization, and repair for heap-manipulating programs, enabling quick bug fixes with visual aids and proof-directed algorithms.

Contribution

It introduces a novel, integrated debugging environment with proof-directed repair and bug localization algorithms, supporting hot-patching and new repair strategies.

Findings

Successfully repaired all buggy instances within 5 seconds on average.

Repaired over 80% of student submissions with reasonable attempts.

Effective on various complex data structures like AVL and Red-Black trees.

Abstract

We present Wolverine2, an integrated Debug-Localize-Repair environment for heap manipulating programs. Wolverine2 provides an interactive debugging environment: while concretely executing a program via on an interactive shell supporting common debugging facilities, Wolverine2 displays the abstract program states (as box-and-arrow diagrams) as a visual aid to the programmer, packages a novel, proof-directed repair algorithm to quickly synthesize the repair patches and a new bug localization algorithm to reduce the search space of repairs. Wolverine2 supports "hot-patching" of the generated patches to provide a seamless debugging environment, and also facilitates new debug-localize-repair possibilities: \textit{specification refinement} and \textit{checkpoint-based hopping}. We evaluate Wolverine2 on 6400 buggy programs (generated using automated fault injection) on a variety of data-structures like singly, doubly, and circular linked lists, AVL trees, Red-Black trees, Splay Trees and Binary Search Trees; Wolverine2 could repair all the buggy instances within realistic programmer wait-time (less than 5 sec in most cases). Wolverine2 could also repair more than 80\% of the 247 (buggy) student submissions where a reasonable attempt was made.