Closed
Description
Currently, to apply loop contracts, we instrument
... preamble ...
... eval guard ...
if (!guard)
goto EXIT;
... loop body ...
goto HEAD;
EXIT:
... postamble ...
to
... preamble ...
PREHEAD:
skip;
/// loop begin
loop_entry_vars = ...;
entered_loop = false;
I_base = <I>;
in_base_case = true;
goto HEAD;
STEP:
assert(I_base);
in_base_case = false;
in_loop_havoc_block = true;
loop_i_havoc_write_set(&w_loop_i);
in_loop_havoc_block = false;
assume (invariant_expr);
D_before = <D>;
HEAD:
... eval guard ... // instrument against w_loop_i
if(!guard)
GOTO EXIT;
... body ... // instrument against w_loop_i
entered_loop = true;
if(in_base_case)
goto STEP;
assert(I);
D_after = <D>;
assert(D_after < D_before);
DEAD D_after, D_before;
assume(false);
EXIT:
// did we actually do the step
assert(entered_loop ==> !in_base_case);
DEAD w_loop_i
... postamble ...
The havocing, all initialization of temporary variables, the snapshotting of the loop invariants all happends in the PREHEAD block or the STEP block. If there are some jumps from out side of the loop into the loop body, they will skip the PREHEAD block and the STEP block; and hence fail the loop contracts.
For example, after the instrumentation, the jump GOTO 2 in the following GOTO program will skip the PREHEAD and the STEP of the loop.
GOTO 2;
... preamble ...
1: IF x == 0 THEN GOTO 3;
2: ASSIGN x := x - 1;
GOTO 1;
3:
... postamble ...
After instrumentation
GOTO 2;
... preamble ...
PREHEAD:
... pre-head block ...
STEP:
... step block ...
HEAD:
1: IF x == 0 THEN GOTO EXIT;
2: ASSIGN x := x - 1;
assert(loop_invariants);
... remaining part of the head block ...
assume(false);
EXIT:
ASSERT(entered_loop ==> !in_base_case);
... postamble ...
So, we should apply loop contracts only when there is no jumps from outside into the body of the loop, and error out otherwise.