1
Vote

Procedure extraction for nested loops looks buggy

description

The recent fix creates another bug. For example,
procedure Main() returns(r:int)
{
  var i,j:int;
  i := 0;
  while(i < 10) {
    j := 0;
    while(j < 10) {
      j := j + 1;
    }
    i := i + 1;
  }
Its outer loop got translated to,
implementation Main_loop_anon4_LoopHead(in_i: int, in_j: int) returns (out_i: int, out_j: int)
{

  entry:
    out_i, out_j := in_i, in_j;
    goto anon4_LoopHead;

  anon4_LoopHead:
    goto anon4_LoopDone, anon4_LoopBody;

  anon4_LoopDone:
    assume {:partition} 10 <= out_i;
    out_i, out_j := in_i, in_j;
    return;

  anon5_LoopDone:
    assume {:partition} 10 <= out_j;
    out_i := out_i + 1;
    goto anon5_LoopDone_dummy;

  anon5_LoopHead:
    call out_i, out_j := Main_loop_anon5_LoopHead(out_i, out_j);
    goto anon5_LoopHead_last;

  anon5_LoopHead_last:
    goto anon5_LoopDone, anon5_LoopBody;

  anon4_LoopBody:
    assume {:partition} out_i < 10;
    out_j := 0;
    goto anon5_LoopHead;

  anon5_LoopBody:
    assume {:partition} out_j < 10;
    out_j := out_j + 1;
    //assume false;
    return;

  anon5_LoopDone_dummy:
    call {:si_unique_call 1} out_i, out_j := Main_loop_anon4_LoopHead(out_i, out_j);
    return;

  exit:
    return;
}
Note that inlining of the last iteration of inner loop (anon5_LoopBody) has a return command which instead should be assume false.

It breaks the proof of relative termination because there is path of v1 in which the next recursive procedure is not called.

To show its effect in a single program. We can add ensures to Main_loop_anon4_LoopHead,
free ensures R(in_i, out_i);
ensures in_i < 10 ==> R(in_i + 1, out_i); 
in which R is function R(x:int, y:int) returns(bool);

If unrolling the last iteration of inner loop leads to an unreachable path, then the second ensure should be proved (you might want to constraint the effect of inner loop, like it doesn't modify i).

file attachments

comments

shuvendu wrote Aug 18, 2015 at 9:49 PM

Adding repro


I'm writing to report a potential bug of SymDiff/Boogie when nested loops are extracted to tail-recursion procedures. To be more specific, global variables (possibly local variables as well) are incorrectly restored in the procedure extracted from the outer loop right after the procedure extracted from the inner loop is called. For example, consider this simple Boogie program which contains nested loops,
var t: int;
procedure NestedLoops()
modifies t;
ensures t == 200;
{
   var i:int, j:int;
   i, j, t := 0, 0, 0;
   while(i < 10) {
     j := 0;
     while (j < 20) {
       t := t + 1;
       j := j + 1;
     }
     i := i + 1;
   }
}
Part of the translated Boogie program (with the command shown in the DAC paper, which generates almost the same transformation with SymDiff) is (and I highlight the interesting part),
implementation NestedLoops_loop_anon4_LoopHead[w](in_i: int, in_j: int) returns (out_i: int, out_j: int) {

   entry:
     out_i, out_j := in_i, in_j;
     goto anon4_LoopHead;

   anon4_LoopHead:
     assume {:inferred} 0 <= t && 0 <= out_i && out_i < 11 && 0 <= out_j && out_j < 21;
     goto anon4_LoopDone, anon4_LoopBody;

   anon4_LoopDone:
     assume {:partition} 10 <= out_i;
     out_i, out_j := in_i, in_j;
     t := old(t);
     return;

   anon5_LoopDone:
     assume {:partition} 20 <= out_j;
     out_i := out_i + 1;
     goto anon5_LoopDone_dummy;

   anon5_LoopHead:
     call out_j := NestedLoops_loop_anon5_LoopHead[w](out_i, out_j);
     goto anon5_LoopHead_last;

   anon5_LoopHead_last:
     assume {:inferred} 0 <= t && 0 <= out_i && out_i < 10 && 0 <= out_j && out_j < 21;
>   out_i, out_j := in_i, in_j;
>   t := old(t);

     goto anon5_LoopDone, anon5_LoopBody;

   anon4_LoopBody:
     assume {:partition} out_i < 10;
     out_j := 0;
     goto anon5_LoopHead;

   anon5_LoopBody:
     assume {:partition} out_j < 20;
     t := t + 1;
     out_j := out_j + 1;
     goto anon5_LoopBody_dummy;

   anon5_LoopBody_dummy:
     assume false;
     out_i, out_j := in_i, in_j;
     t := old(t);
     return;

   anon5_LoopDone_dummy:
     call {:si_unique_call 1} out_i, out_j := NestedLoops_loop_anon4_LoopHead[w](out_i, out_j);
     return;

   exit:
     return;
}
The two statements highlighted restore the local variables and the global variable after the extracted-inner-loop procedure is called. It seems that the inlined inner-loop body is blocked by assume false under the anon5_LoopBody_dummy flag, which means the inlined inner-loop body has no impact on the execution of outer-loop. So the global is not modified in the extracted outer-loop procedure. I wrote a program to verify it (I have to modify the program above because it couldn't be parsed by Boogie),
var t:int;
procedure NestedLoops_loop_anon4_LoopHead(in_i: int, in_j: int) returns
(out_i: int, out_j: int)
modifies t;
ensures old(t) == t;
{

   entry:
     out_i, out_j := in_i, in_j;
     goto anon4_LoopHead;

   anon4_LoopHead:
     assume {:inferred} 0 <= t && 0 <= out_i && out_i < 11 && 0 <= out_j && out_j < 21;
     goto anon4_LoopDone, anon4_LoopBody;

   anon4_LoopDone:
     assume {:partition} 10 <= out_i;
     out_i, out_j := in_i, in_j;
     t := old(t);
     return;

   anon5_LoopDone:
     assume {:partition} 20 <= out_j;
     out_i := out_i + 1;
     goto anon5_LoopDone_dummy;

   anon5_LoopHead:
     //call out_j := NestedLoops_loop_anon5_LoopHead[w](out_i, out_j);
     out_j, t := 20, t + 20;
     goto anon5_LoopHead_last;

   anon5_LoopHead_last:
     assume {:inferred} 0 <= t && 0 <= out_i && out_i < 10 && 0 <= out_j && out_j < 21;
     out_i, out_j := in_i, in_j;
     t := old(t);
     goto anon5_LoopDone, anon5_LoopBody;

   anon4_LoopBody:
     assume {:partition} out_i < 10;
     out_j := 0;
     goto anon5_LoopHead;

   anon5_LoopBody:
     assume {:partition} out_j < 20;
     t := t + 1;
     out_j := out_j + 1;
     goto anon5_LoopBody_dummy;

   anon5_LoopBody_dummy:
     assume false;
     out_i, out_j := in_i, in_j;
     t := old(t);
     return;

   anon5_LoopDone_dummy:
     call {:si_unique_call 1} out_i, out_j := NestedLoops_loop_anon4_LoopHead(out_i, out_j);
     return;

   exit:
     return;
}
Please point it out if I mess up something. The related files are attached. v5.bpl is the original program and v5_extracted.bpl is the translated one.

Best,
Shaobo

shuvendu wrote Oct 28, 2015 at 12:44 AM