User Tools

Site Tools


how_to_use_incremental_unwinding

How to use incremental unwinding

CBMC with incremental loop unwinding is currently in http://www.cprover.org/svn/cbmc/branches/peter-incremental-unwinding

Incremental unwinding is useful for bounded model checking a program with an unbounded loop, as e.g. found in control software where the program is actually one big loop. With incremental unwinding, the generated SSA formula is checked after each unwinding. If a bug was found, CBMC terminates with a counterexample. Otherwise, the SSA formula is extended by another unwinding and checked again, a.s.o.

Command line options

There are 3 options to control incremental unwinding:

--incremental-check loopid enables incremental unwinding for one specific loop

--incremental enables incremental unwinding for all loops and recursions

--unwind-min nr start incremental unwinding after nr iterations (default 1)

--unwind-max nr stop incremental unwinding after nr iterations (default UINT_MAX)

The options --partial-loops and --no-unwinding-assertions can be used as usual.

--unwind: If used with --incremental-check loopid it acts only on loops other than loopid. Cannot be used together with --incremental.

--unwindset: Loops specified in the unwindset will not be unrolled incrementally if used with --incremental.

Examples

http://www.cprover.org/svn/cbmc/branches/peter-incremental-unwinding/regression/cbmc-incr/simpleloop1

extern int nondet_int();
int main() {
  int x = nondet_int();
  __CPROVER_assume(0<=x && x<=1);
  while(x<4) {
    x=x+1;
    assert(x<4);
  }
}

cbmc main.c unwinds the loop forever.

cbmc main.c --incremental-check c::main.0 returns a counterexample after 3 unwindings, as expected.

Remark: Note that, if the loop is not trivially bounded and contains no bug, e.g. change to assert(x<=4) or move the assertion after the loop, then also --incremental-check loopid will keep unwinding forever if no --unwind-max is given. Yet --incremental will terminate if the loop is indeed bounded.

Further options

--ignore-assertions-before-unwind-min ignore assertions for unwindings before the unwind-min bound

--earliest-loop-exit stop unwinding a loop as soon as we can exit loop (to be used with --incremental)

--no-sat-preprocessor use MiniSAT2 without simplifier

--slice-formula slice SSA formula

--refine do bitvector refinement

Currently, only MiniSAT2 is supported at the backend.

K-Induction

Incremental CBMC can also be used to perform k-induction proofs (at least for one-loop programs).

Base case: just use incremental CBMC with --incremental-check loopid --no-unwinding-assertions. This will terminate as soon as the base case fails.

Step case: use incremental CBMC with --incremental-check loopid --stop-when-unsat --no-unwinding-assertions. This will terminate as soon as the step case holds.

You can run both in parallel and, as soon as one of the processes terminates, you stop the other process.

The input programs are assumed to be instrumented as follows:

Base case:

initialize();
while(...) {
  body();
  assert(property);
}

Step case:

initialize();
havoc_variables_modified_in_the_loop();
while(...) {
  __CPROVER_assume(property);
  body();
  assert(property);
}

(see example: http://www.cprover.org/svn/cbmc/branches/peter-incremental-unwinding/regression/cbmc-incr/induction1)

how_to_use_incremental_unwinding.txt · Last modified: 2014/09/30 22:36 by schram