Dynamically Discovering Pointer-Based Program Invariants

Abstract

Explicitly stated program invariants can help programmers by characterizing aspects of program execution and identifying program properties that must be preserved when modifying code; invariants can also be of assistance to automated tools. Unfortunately, these invariants are usually absent from code. Previous work showed how to dynamically invariants from program traces by looking for patterns in and relationships among variable values. Although the original prototype recovered invariants from formally-specified programs, and the invariants it detected assisted programmers in a software evolution task, it was not effective for pointerbased programs. This paper closes that gap by showing that two key techniques are adequate to detect pointer-related invariants. First, we linearize data structures to present them whole to our invariant detector and to express values for expressions not present in the source code. Second, we discuss several policies and a mechanism for computing disjunct...