Loop unrolling: formal definition and application to testing

TL;DR

The paper questions the adequacy of branch coverage for loops due to unpredictable iterations and introduces loop unrolling up to a finite depth $n$ as a rigorous, practical alternative. It provides a machine-checked formal framework based on trace-set semantics and a power-operator construction to define loop unrolling, along with equivalent representations proven in Isabelle. The authors implement this approach in a seeding-contradiction driven test-generation pipeline (SCU) and empirically evaluate it on 12 loop-containing examples, showing that unrolling uncovers substantially more bugs with only modest increases in generation and execution time for small depths. The findings argue for integrating loop unrolling into test-generation strategies and coverage metrics to achieve higher fault-detection effectiveness beyond standard branch coverage.

Abstract

Testing processes usually aim at high coverage, but loops severely limit coverage ambitions since the number of iterations is generally not predictable. Most testing teams address this issue by adopting the extreme solution of limiting themselves to branch coverage, which only considers loop executions that iterate the body either once or not at all. This approach misses any bug that only arises after two or more iterations. To achieve more meaningful coverage, testing strategies may unroll loops, in the sense of using executions that iterate loops up to n times for some n greater than one, chosen pragmatically in consideration of the available computational power. While loop unrolling is a standard part of compiler optimization techniques, its use in testing is far less common. Part of the reason is that the concept, while seemingly intuitive, lacks a generally accepted and precise specification. The present article provides a formal definition and a set of formal properties of unrolling. All the properties have mechanically been proved correct (through the Isabelle proof assistant). Using this definition as the conceptual basis, we have applied an unrolling strategy to an existing automated testing framework and report the results: how many more bugs get detected once we unroll loops more than once? These results provide a first assessment of whether unrolling should become a standard part of test generation and test coverage measurement.

Figures (6)

• Figure 1: Control flow for a loop
• Figure 2: Seeding contradictions for a loop
• Figure 3: SCU for plain loop body
• Figure 4: SCU for conditionals inside loop body
• Figure 5: $P (N_p)$: the percentage of faults detected per run at different unrolling levels.