Avoid backward goto during applying loop contracts

[qinheping]

CBMC version: 5.69.1
Operating system: n/a

Problem description

Currently, the loop contract transformation will insert a backward jump (https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/contracts.cpp#L110) into the result goto program. So after applying loop contracts, there will be loops that execute only one iteration in the place of the original annotated loops, which require users to correctly specify the unwinding number of them: either not unwinding them, or unwind them for at least twice. It is an unnecessary usability pain point for users. So backward goto should be avoided during loop contract transformation.

Example

A smaller example to illustrate the problem.

int main()
{
  int i;
  for(i = 0; i < 1; i++)
    __CPROVER_loop_invariant(1 > 1)
    {
      i++;
    }
}

Note that the invariant 1 > 1 is invalid. So that a correct run of CBMC should report loop invariant doesn’t hold before entry of the loop.
Run goto-cc main.c goto-instrument --apply-loop-contracts a.out b.out to apply loop contracts and get the result goto program b.goto. Then with command cbmc b.out (or cbmc --unwind 2 b.out) CBMC will correctly report the failure

[main.1] line 5 Check loop invariant before entry: FAILURE

However, running cbmc --unwind 1 b.out will report no failure.
Running cbmc --unwind 1 --unwinding-assertions b.out will report

[main.unwind.0] line 5 unwinding assertion loop 0: FAILURE

[remi-delmas-3000]

The backjump is introduced to separate the base case and the step case of the loop in the transformed program, and analyse the loop step only if the loop can run at least once.

The structure of the transformed loop is roughly this:

base_case = true;
ran_once = false;
I_base = I; // loop invariant in the base case

A = snapshot_assigns_clause();
goto LOOP_HEAD;

// we will back jump to this label if the loop can run once
STEP_CASE:
base_case = false; 
havoc(A);
assume(I);
D_init = D; // decreases clause

// All user-specified writes, including those in the guard,
// will be instrumented with assigns clause checks.

LOOP_HEAD:

// The evaluation of guard G could be split and have early exits
// due to Boolean short circuiting, and/or code with side effects,
// e.g. while (G1 && G2 && G3 && ...)
// 1. If the guard is falsified and we are in the base the base case,
//    we jump past the loop and continue execution from  a non-havoced state.
// 2. If the guard is falsified and we are in the step case,
//    then we reached a loop termination state, we jump past the loop
//    and execution continues from a havoced state that satisfies the invariant.                                       

... eval_side_effects_1 ...
IF (!G1) goto LOOP_EXIT;
... eval_side_effects_2 ...
IF (!G2) goto LOOP_EXIT;
... eval_side_effects_3 ...
IF (!G3) goto LOOP_EXIT;

... loop body instructions are here ...

// The jump target for `continue` statements in `body`.

LOOP_END:
// if we reach this lable then the loop ran once,
// and the step case needs to be checked
ran_once = true;

// If in the base case, then check the invariant in the base case.
// This location is after side effects in the control flow,
// but we are using a snapshot of the invariant expression 
// taken in the initial state before side effects happen.
ASSERT base_case ==> I_base;

// If control reaches this location,
// then the loop runs at least once from the base case
// and we jump back to analyse the step case

IF (base_case) goto STEP_CASE; // this back jump might not get unrolled if `--unwind 1` is set on the CLI

// When control reaches this location, we are necessarily in the step case,
// and are checking these assertions after taking a step from a havoced state.

assert(I) // check invariant
D_end = D;
assert(D_end < D_init);
assume(false); // was GOTO LOOP_HEAD in the original untransformed program

// The jump target for `break` and false loop guard (skips invariant and decreases clauses)

LOOP_EXIT:
// extra assertion : check that if the loop ran in the base case, 
// then the step case was also checked
assert(ran_once ==> !base_case);

// When control reaches this point, there are only two possibilities:
// 1. Either the loop guard was false in the base case,
//    and so we did not abstract the loop (no havocing and contract checks), or
// 2. We abstracted the loop, instrumented all contract checks,
//    and are  continuing execution from an arbitrary havoc state that satisfies
//    (I && ~G) || <possible states at `break`s>

I see at least two ways to address this unrolling issue:

• add a loop unwinding assertion in the transformed program at instrumentation time so that the analysis would fail if the loop could have run once and the loop step has not been analysed: assert(ran_once ==> !base_case);
  This would turn cbmc --unwind 1 b.out into a FAILED run;
• unwind the transformed loop at instrumentation time using the unwindsett class so that it disappears and the user does not have to worry about it

[qinheping]

Thank you @remi-delmas-3000. I will create a PR to unwind the transformed loop at instrumentation time.