Random Testing via Runtime Abstract Interpretation

Abstract

Property-based testing of C programs can be automated by synthesizing random input generators from separation-logic specifications. Existing work in this space, such as the Bennet testing tool, uses randomized backtracking search, generating random values and checking them against constraints, backtracking on failure. Although this approach performs well on simple recursive heap structures, it struggles as constraints grow more complex, particularly when they involve pointer arithmetic—as, for example, in the many forms of specialized storage allocators that arise in low-level systems software. Existing work uses targeted optimizations and heuristics to satisfy specific classes of constraints, but this requires continual expansion as new special cases arise, resulting in complex tools. We reframe generation as the iterative refinement of abstract domain elements, where sampling a concrete value is the final refinement. By applying abstract interpretation at runtime to obtain an abstract element, we obtain a lightweight form of constraint solving and propagation that enables randomized testing of programs with complex preconditions. We identify three strategies for applying abstract interpretation: (1) speculative refinement, refining abstract elements before sampling based on immediately following constraints, (2) corrective refinement, calculating “desired” abstract elements from information gleaned from failed constraints, and (3) cascading propagation, propagating information from failures to components of compound expressions. We formalize these ideas in a generator DSL whose monadic semantics are parametric over abstract domains. We implement this DSL in a new tool called Lucas and evaluate it on sixteen workloads: the six original case studies from the Bennet paper, six position-independent data structures, and four free-list allocators. Comparing configurations with and without refinement, we find that refinement finds bugs in all four allocators and in two of the position-independent data structures that Bennet-style random backtracking fails to find.