bug fix for interaction between inlining and loops

3 files changed, 75 insertions, 22 deletions

diff --git a/Test/inline/Answer b/Test/inline/Answer
index eddeb64f..ff2a5e71 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -101,6 +101,7 @@ implementation Main()
   inline$inc$0$Entry:

     inline$inc$0$x := x;

     inline$inc$0$i := 5;

+    havoc inline$inc$0$y;

     goto inline$inc$0$anon0;

 

   inline$inc$0$anon0:

@@ -119,6 +120,7 @@ implementation Main()
   inline$incdec$0$Entry:

     inline$incdec$0$x := x;

     inline$incdec$0$y := 2;

+    havoc inline$incdec$0$z;

     goto inline$incdec$0$anon0;

 

   inline$incdec$0$anon0:

@@ -129,6 +131,7 @@ implementation Main()
   inline$dec$0$Entry:

     inline$dec$0$x := inline$incdec$0$z;

     inline$dec$0$i := inline$incdec$0$y;

+    havoc inline$dec$0$y;

     goto inline$dec$0$anon0;

 

   inline$dec$0$anon0:

@@ -174,6 +177,7 @@ implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
   inline$dec$0$Entry:

     inline$dec$0$x := z;

     inline$dec$0$i := y;

+    havoc inline$dec$0$y;

     goto inline$dec$0$anon0;

 

   inline$dec$0$anon0:

@@ -253,6 +257,7 @@ implementation calculate()
 

   inline$increase$0$Entry:

     inline$increase$0$i := y;

+    havoc inline$increase$0$j, inline$increase$0$k;

     inline$increase$0$glb := glb;

     goto inline$increase$0$anon0;

 

@@ -344,6 +349,7 @@ implementation recursivetest()
 

   inline$recursive$0$Entry:

     inline$recursive$0$x := glb;

+    havoc inline$recursive$0$k, inline$recursive$0$y;

     goto inline$recursive$0$anon0;

 

   inline$recursive$0$anon0:

@@ -360,6 +366,7 @@ implementation recursivetest()
 

   inline$recursive$1$Entry:

     inline$recursive$1$x := inline$recursive$0$x - 1;

+    havoc inline$recursive$1$k, inline$recursive$1$y;

     goto inline$recursive$1$anon0;

 

   inline$recursive$1$anon0:

@@ -376,6 +383,7 @@ implementation recursivetest()
 

   inline$recursive$2$Entry:

     inline$recursive$2$x := inline$recursive$1$x - 1;

+    havoc inline$recursive$2$k, inline$recursive$2$y;

     goto inline$recursive$2$anon0;

 

   inline$recursive$2$anon0:

@@ -448,6 +456,7 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
 

   inline$recursive$0$Entry:

     inline$recursive$0$x := x - 1;

+    havoc inline$recursive$0$k, inline$recursive$0$y;

     goto inline$recursive$0$anon0;

 

   inline$recursive$0$anon0:

@@ -464,6 +473,7 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
 

   inline$recursive$1$Entry:

     inline$recursive$1$x := inline$recursive$0$x - 1;

+    havoc inline$recursive$1$k, inline$recursive$1$y;

     goto inline$recursive$1$anon0;

 

   inline$recursive$1$anon0:

@@ -480,6 +490,7 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
 

   inline$recursive$2$Entry:

     inline$recursive$2$x := inline$recursive$1$x - 1;

+    havoc inline$recursive$2$k, inline$recursive$2$y;

     goto inline$recursive$2$anon0;

 

   inline$recursive$2$anon0:

@@ -656,6 +667,7 @@ implementation main(x: int)
     inline$find$0$A := A;

     inline$find$0$size := size;

     inline$find$0$x := x;

+    havoc inline$find$0$i, inline$find$0$b, inline$find$0$ret, inline$find$0$found;

     goto inline$find$0$anon0;

 

   inline$find$0$anon0:

@@ -677,6 +689,7 @@ implementation main(x: int)
     inline$check$0$i := inline$find$0$i;

     inline$check$0$c := inline$find$0$x;

     assert inline$check$0$i >= 0;

+    havoc inline$check$0$ret;

     goto inline$check$0$anon0;

 

   inline$check$0$anon0:

@@ -774,6 +787,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
     inline$check$0$i := i;

     inline$check$0$c := x;

     assert inline$check$0$i >= 0;

+    havoc inline$check$0$ret;

     goto inline$check$0$anon0;

 

   inline$check$0$anon0:

@@ -819,38 +833,38 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
 }

 

 

-<console>(68,4): Error BP5003: A postcondition might not hold on this return path.

+<console>(70,4): Error BP5003: A postcondition might not hold on this return path.

 <console>(78,2): Related location: This is the postcondition that might not hold.

 Execution trace:

     <console>(19,0): anon0

-    <console>(28,0): inline$find$0$anon0

-    <console>(38,0): inline$find$0$anon4_LoopBody

-    <console>(42,0): inline$check$0$Entry

-    <console>(57,0): inline$check$0$anon4_Else

-    <console>(62,0): inline$check$0$anon3

-    <console>(65,0): inline$check$0$Return

-<console>(100,4): Error BP5001: This assertion might not hold.

+    <console>(29,0): inline$find$0$anon0

+    <console>(39,0): inline$find$0$anon4_LoopBody

+    <console>(43,0): inline$check$0$Entry

+    <console>(59,0): inline$check$0$anon4_Else

+    <console>(64,0): inline$check$0$anon3

+    <console>(67,0): inline$check$0$Return

+<console>(102,4): Error BP5001: This assertion might not hold.

 Execution trace:

     <console>(19,0): anon0

-    <console>(28,0): inline$find$0$anon0

-    <console>(38,0): inline$find$0$anon4_LoopBody

-    <console>(42,0): inline$check$0$Entry

-    <console>(52,0): inline$check$0$anon4_Then

-    <console>(65,0): inline$check$0$Return

-    <console>(73,0): inline$find$0$anon5_Then

-    <console>(87,0): inline$find$0$anon3

-    <console>(90,0): inline$find$0$Return

-    <console>(95,0): anon0$1

-    <console>(98,0): anon3_Then

-<console>(50,4): Error BP5003: A postcondition might not hold on this return path.

+    <console>(29,0): inline$find$0$anon0

+    <console>(39,0): inline$find$0$anon4_LoopBody

+    <console>(43,0): inline$check$0$Entry

+    <console>(54,0): inline$check$0$anon4_Then

+    <console>(67,0): inline$check$0$Return

+    <console>(75,0): inline$find$0$anon5_Then

+    <console>(89,0): inline$find$0$anon3

+    <console>(92,0): inline$find$0$Return

+    <console>(97,0): anon0$1

+    <console>(100,0): anon3_Then

+<console>(51,4): Error BP5003: A postcondition might not hold on this return path.

 <console>(78,2): Related location: This is the postcondition that might not hold.

 Execution trace:

     <console>(10,0): anon0

     <console>(20,0): anon4_LoopBody

     <console>(24,0): inline$check$0$Entry

-    <console>(39,0): inline$check$0$anon4_Else

-    <console>(44,0): inline$check$0$anon3

-    <console>(47,0): inline$check$0$Return

+    <console>(40,0): inline$check$0$anon4_Else

+    <console>(45,0): inline$check$0$anon3

+    <console>(48,0): inline$check$0$Return

 <console>(99,0): Error BP5003: A postcondition might not hold on this return path.

 <console>(78,2): Related location: This is the postcondition that might not hold.

 Execution trace:

@@ -1540,3 +1554,18 @@ Execution trace:
     polyInline.bpl(27,3): anon0

 

 Boogie program verifier finished with 0 verified, 2 errors

+-------------------- InliningAndLoops.bpl --------------------

+InliningAndLoops.bpl(12,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    InliningAndLoops.bpl(5,10): anon0#3

+    InliningAndLoops.bpl(6,3): anon4_LoopHead#3

+    InliningAndLoops.bpl(8,5): anon4_LoopBody#3

+    InliningAndLoops.bpl(8,5): anon4_LoopBody$1#3

+    InliningAndLoops.bpl(6,3): anon4_LoopHead#2

+    InliningAndLoops.bpl(8,5): anon4_LoopBody#2

+    InliningAndLoops.bpl(8,5): anon4_LoopBody$1#2

+    InliningAndLoops.bpl(6,3): anon4_LoopHead#1

+    InliningAndLoops.bpl(6,3): anon4_LoopDone#3

+    InliningAndLoops.bpl(12,5): anon5_Then#3

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/inline/InliningAndLoops.bpl b/Test/inline/InliningAndLoops.bpl
new file mode 100644
index 00000000..970591a5
--- /dev/null
+++ b/Test/inline/InliningAndLoops.bpl
@@ -0,0 +1,20 @@
+procedure foo(N: int)

+  requires N == 2;

+{

+  var n, sum, recent: int;

+  n, sum := 0, 0;

+  while (n < N)

+  {

+    call recent := bar();

+    sum, n := sum + recent, n + 1;

+  }

+  if (n == 2) {

+    assert sum == recent + recent;  // no reason to believe this always to be true

+  }

+}

+

+procedure {:inline 1} bar() returns (r: int)

+{

+  var x: int;

+  r := x;

+}

diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index f56d55a0..cd404bfa 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -37,3 +37,7 @@ echo -------------------- fundef.bpl --------------------
 echo -------------------- polyInline.bpl --------------------

 %BGEXE% %* /typeEncoding:predicates /logPrefix:p polyInline.bpl

 %BGEXE% %* /typeEncoding:arguments /logPrefix:a polyInline.bpl

+

+echo -------------------- InliningAndLoops.bpl --------------------

+%BGEXE% %* /loopUnroll:3 /soundLoopUnrolling InliningAndLoops.bpl

+