Trace Generalization via Loop Compression
Joxan Jaffar and Vijayaraghavan Murali
We present a new method to generalize execution traces by compressing loop
iterations in them using loop invariants. The invariants discovered are ``safe''
such that the resulting compressed trace also satisfies certain target
properties which the original trace satisfied (e.g., an assertion at the end).
This results in a concise trace that captures the semantics of the original
trace w.r.t. the target but without needing to unroll the loops fully. A central
feature is the use of a canonical loop invariant discovery algorithm which
preserves all atomic formulas in the representation of a symbolic state which
can be shown to be invariant. If this fails to provide a safe invariant, then
the algorithm dynamically unrolls the loop and attempts the discovery at the
next iteration, where it is more likely to succeed as the loop stabilizes
towards an invariant. We show using realistic benchmarks that the end result,
a generalization of the original trace, is significantly more succinct.