Fixed bug in the cutting of back edges (that manifested itself whenever the first block in a procedure was the target of a back edge)

5 files changed, 51 insertions, 13 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 988d80fd..6a0891b8 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1789,13 +1789,15 @@ namespace VC {
       }

       #endregion

 

+      // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges

+      // below assumes that the start node has no predecessor)

+      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new CmdSeq(), new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))));

       ResetPredecessors(impl.Blocks);

       

       #region Convert program CFG into a DAG

 

       #region Use the graph library to figure out where the (natural) loops are

 

-      

       #region Create the graph by adding the source node and each edge

       Graph<Block> g = Program.GraphFromImpl(impl);

       #endregion

diff --git a/Test/smoke/Answer b/Test/smoke/Answer
index 98cff8d2..e2390446 100644
--- a/Test/smoke/Answer
+++ b/Test/smoke/Answer
@@ -5,6 +5,9 @@ implementation b(x: int)
   var y: int;

 

 

+  0:

+    goto anon0;

+

   anon0:

     goto anon3_Then;

 

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 915f63e8..159b3579 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -1,9 +1,9 @@
 

 -------------------- NullInModel --------------------

 *** MODEL

-%lbl%@45 -> false

+%lbl%@47 -> false

 %lbl%+24 -> true

-%lbl%+35 -> true

+%lbl%+37 -> true

 boolType -> T@T!val!2

 intType -> T@T!val!0

 null -> T@U!val!0

@@ -35,9 +35,9 @@ Boogie program verifier finished with 0 verified, 1 error
 

 -------------------- IntInModel --------------------

 *** MODEL

-%lbl%@37 -> false

+%lbl%@39 -> false

 %lbl%+23 -> true

-%lbl%+27 -> true

+%lbl%+29 -> true

 boolType -> T@T!val!2

 i -> 0

 intType -> T@T!val!0

@@ -62,9 +62,9 @@ Boogie program verifier finished with 0 verified, 1 error
 

 -------------------- ModelTest --------------------

 *** MODEL

-%lbl%@145 -> false

+%lbl%@147 -> false

 %lbl%+64 -> true

-%lbl%+82 -> true

+%lbl%+84 -> true

 boolType -> T@T!val!2

 i@0 -> 1

 intType -> T@T!val!0

@@ -120,11 +120,11 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

 *** MODEL

-%lbl%@291 -> false

+%lbl%@293 -> false

 %lbl%+112 -> true

 %lbl%+114 -> true

 %lbl%+118 -> true

-%lbl%+146 -> true

+%lbl%+148 -> true

 @MV_state_const -> 6

 boolType -> T@T!val!2

 F -> T@U!val!2

@@ -133,7 +133,7 @@ Heap -> T@U!val!0
 intType -> T@T!val!0

 m -> **m

 m@0 -> -451

-m@2 -> -450

+m@1 -> -450

 m@3 -> -450

 r -> **r

 r@0 -> -900

@@ -155,8 +155,8 @@ type -> {
 }

 @MV_state -> {

   6 0 -> true

-  6 3 -> true

-  6 4 -> true

+  6 1 -> true

+  6 2 -> true

   6 5 -> true

   else -> true

 }

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 4a7fd32f..b936ef87 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -153,8 +153,15 @@ CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained
 Execution trace:

     CutBackEdge.bpl(5,3): entry

     CutBackEdge.bpl(9,3): block850

+CutBackEdge.bpl(20,5): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+CutBackEdge.bpl(26,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    CutBackEdge.bpl(25,3): L

+CutBackEdge.bpl(38,5): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

 

-Boogie program verifier finished with 0 verified, 1 error

+Boogie program verifier finished with 1 verified, 4 errors

 

 -------------------- False.bpl --------------------

 

diff --git a/Test/test2/CutBackEdge.bpl b/Test/test2/CutBackEdge.bpl
index 934974aa..7294d0f9 100644
--- a/Test/test2/CutBackEdge.bpl
+++ b/Test/test2/CutBackEdge.bpl
@@ -12,3 +12,29 @@ procedure Test()
     goto block850;

 

 }

+

+// The following procedure once exhibited a bug in Boogie's DAG manipulations

+procedure TightLoop0()

+{

+  L:

+    assert !true;  // error

+    goto L;

+}

+procedure TightLoop1()

+{

+  L:

+    assert false;  // error

+    goto L;

+}

+procedure TightLoop2()

+{

+  L:

+    assert true;  // cool

+    goto L;

+}

+procedure TightLoop3(b: bool)

+{

+  L:

+    assert b;  // error

+    goto L;

+}