Implemented block coalescing invoked right after type checking.

Controlled by the option /coalesceBlocks (default is to perform the optimization).

3 files changed, 23 insertions, 79 deletions

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index 4e5c8f27..ca9ff22a 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -121,29 +121,9 @@ implementation FooTooStepByStep()
   L0:

     assume true;

     i := 5;

-    assume i == 5;

-    goto L1;

-

-  L1:

-    assume i == 5;

     i := 3 * i + 1;

-    assume i == 16;

-    goto L2;

-

-  L2:

-    assume i == 16;

     i := 3 * (i + 1);

-    assume 1 / 3 * i == 17;

-    goto L3;

-

-  L3:

-    assume 1 / 3 * i == 17;

     i := 1 + 3 * i;

-    assume i == 154;

-    goto L4;

-

-  L4:

-    assume i == 154;

     i := (i + 1) * 3;

     assume 1 / 3 * i == 155;

     return;

@@ -256,13 +236,18 @@ implementation p()
     assume true;

     assume x < y;

     assume x + 1 <= y;

-    goto B;

+    goto B, C;

 

   B:

     assume x + 1 <= y;

     x := x * x;

     assume true;

     return;

+

+  C:

+    assume x + 1 <= y;

+    assume x + 1 <= y;

+    return;

 }

 

 

@@ -285,25 +270,30 @@ implementation p()
     assume true;

     assume 0 - 1 <= x;

     assume -1 <= x;

-    goto B;

+    goto B, E;

 

   B:

     assume -1 <= x;

     assume x < y;

     assume x + 1 <= y && -1 <= x;

-    goto C;

+    goto C, E;

 

   C:

     assume x + 1 <= y && -1 <= x;

     x := x * x;

     assume 0 <= y;

-    goto D;

+    goto D, E;

 

   D:

     assume 0 <= y;

     x := y;

     assume x == y && 0 <= y;

     return;

+

+  E:

+    assume true;

+    assume true;

+    return;

 }

 

 

@@ -405,54 +395,14 @@ implementation foo()
   A:

     assume true;

     n := 0;

-    assume n == 0;

-    goto B;

-

-  B:

-    assume n == 0;

     j := 0;

-    assume j == 0 && n == 0;

-    goto C;

-

-  C:

-    assume j == 0 && n == 0;

     i := j + 1;

-    assume i == j + 1 && j == 0 && n == 0;

-    goto D;

-

-  D:

-    assume i == j + 1 && j == 0 && n == 0;

     i := i + 1;

-    assume i == j + 2 && j == 0 && n == 0;

-    goto E;

-

-  E:

-    assume i == j + 2 && j == 0 && n == 0;

     i := i + 1;

-    assume i == j + 3 && j == 0 && n == 0;

-    goto F;

-

-  F:

-    assume i == j + 3 && j == 0 && n == 0;

     i := i + 1;

-    assume i == j + 4 && j == 0 && n == 0;

-    goto G;

-

-  G:

-    assume i == j + 4 && j == 0 && n == 0;

     i := i + 1;

-    assume i == j + 5 && j == 0 && n == 0;

-    goto H;

-

-  H:

-    assume i == j + 5 && j == 0 && n == 0;

     j := j + 1;

     assume i == j + 4 && j == 1 && n == 0;

-    goto I;

-

-  I:

-    assume i == j + 4 && j == 1 && n == 0;

-    assume i == j + 4 && j == 1 && n == 0;

     return;

 }

 

@@ -481,19 +431,9 @@ implementation foo()
   loop0:  // cut point

     assume 4 <= n && 0 <= i && j == i + 1;

     assume j <= n;

-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;

-    goto loop1;

-

-  loop1:

-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;

     i := i + 1;

-    assume 1 <= i && j == i && j <= n && 4 <= n;

-    goto loop2;

-

-  loop2:

-    assume j <= n && 4 <= n && 1 <= i && j == i;

     j := j + 1;

-    assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i;

+    assume j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;

     goto loop0, exit;

 

   exit:

diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl
index c8c4605c..2207debe 100644
--- a/Test/aitest1/Linear4.bpl
+++ b/Test/aitest1/Linear4.bpl
@@ -8,8 +8,10 @@ procedure p()
 {

   A:

     assume x < y;

-    goto B;

+    goto B, C;

   B:

     x := x*x;

     return;

+  C:

+    return;

 }

diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
index 4f04999c..199cb6f2 100644
--- a/Test/aitest1/Linear5.bpl
+++ b/Test/aitest1/Linear5.bpl
@@ -8,14 +8,16 @@ procedure p()
 {

   A:

     assume -1 <= x;

-    goto B;

+    goto B, E;

   B:

     assume x < y;

-    goto C;

+    goto C, E;

   C:

     x := x*x;

-    goto D;

+    goto D, E;

   D:

     x := y;

     return;

+  E:

+    return;

 }