Boogie: Added new abstract interpretation harness, which uses native Boogie Expr's, not the more abstract AIExpr's.

Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false.
Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals
Boogie: Mark all inferred conditions with attribute {:inferred}

1 files changed, 70 insertions, 70 deletions

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index ca9ff22a..718e7171 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -8,27 +8,27 @@ implementation SimpleLoop()
   var i: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     i := 0;

-    assume i == 0;

+    assume {:inferred} i == 0;

     goto test;

 

   test:  // cut point

-    assume 0 <= i;

-    assume 0 <= i;

+    assume {:inferred} 0 <= i;

+    assume {:inferred} 0 <= i;

     goto Then, Else;

 

   Then:

-    assume 0 <= i;

+    assume {:inferred} 0 <= i;

     assume i < 10;

     i := i + 1;

-    assume i <= 10 && 1 <= i;

+    assume {:inferred} i <= 10 && 1 <= i;

     goto test;

 

   Else:

-    assume 0 <= i;

+    assume {:inferred} 0 <= i;

     assume !(i < 10);

-    assume 10 <= i;

+    assume {:inferred} 10 <= i;

     return;

 }

 

@@ -43,27 +43,27 @@ implementation VariableBoundLoop(n: int)
   var i: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     i := 0;

-    assume i == 0;

+    assume {:inferred} i == 0;

     goto test;

 

   test:  // cut point

-    assume 0 <= i;

-    assume 0 <= i;

+    assume {:inferred} 0 <= i;

+    assume {:inferred} 0 <= i;

     goto Then, Else;

 

   Then:

-    assume 0 <= i;

+    assume {:inferred} 0 <= i;

     assume i < n;

     i := i + 1;

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

+    assume {:inferred} i <= n && 1 <= i;

     goto test;

 

   Else:

-    assume 0 <= i;

+    assume {:inferred} 0 <= i;

     assume !(i < n);

-    assume n <= i && 0 <= i;

+    assume {:inferred} n <= i && 0 <= i;

     return;

 }

 

@@ -78,12 +78,12 @@ implementation Foo()
   var i: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     i := 3 * i + 1;

     i := 3 * (i + 1);

     i := 1 + 3 * i;

     i := (i + 1) * 3;

-    assume true;

+    assume {:inferred} true;

     return;

 }

 

@@ -98,13 +98,13 @@ implementation FooToo()
   var i: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     i := 5;

     i := 3 * i + 1;

     i := 3 * (i + 1);

     i := 1 + 3 * i;

     i := (i + 1) * 3;

-    assume 1 / 3 * i == 155;

+    assume {:inferred} 1 / 3 * i == 155;

     return;

 }

 

@@ -119,13 +119,13 @@ implementation FooTooStepByStep()
   var i: int;

 

   L0:

-    assume true;

+    assume {:inferred} true;

     i := 5;

     i := 3 * i + 1;

     i := 3 * (i + 1);

     i := 1 + 3 * i;

     i := (i + 1) * 3;

-    assume 1 / 3 * i == 155;

+    assume {:inferred} 1 / 3 * i == 155;

     return;

 }

 

@@ -145,8 +145,8 @@ implementation p()
 {

 

   start:

-    assume true;

-    assume true;

+    assume {:inferred} true;

+    assume {:inferred} true;

     return;

 }

 

@@ -166,9 +166,9 @@ implementation p()
 {

 

   start:

-    assume true;

+    assume {:inferred} true;

     assume x * x == y;

-    assume true;

+    assume {:inferred} true;

     return;

 }

 

@@ -188,9 +188,9 @@ implementation p()
 {

 

   start:

-    assume true;

-    assume x == 8;

+    assume {:inferred} true;

     assume x == 8;

+    assume {:inferred} x == 8;

     return;

 }

 

@@ -210,9 +210,9 @@ implementation p()
 {

 

   start:

-    assume true;

+    assume {:inferred} true;

     assume x < y;

-    assume x + 1 <= y;

+    assume {:inferred} x + 1 <= y;

     return;

 }

 

@@ -233,20 +233,20 @@ implementation p()
 {

 

   A:

-    assume true;

+    assume {:inferred} true;

     assume x < y;

-    assume x + 1 <= y;

+    assume {:inferred} x + 1 <= y;

     goto B, C;

 

   B:

-    assume x + 1 <= y;

+    assume {:inferred} x + 1 <= y;

     x := x * x;

-    assume true;

+    assume {:inferred} true;

     return;

 

   C:

-    assume x + 1 <= y;

-    assume x + 1 <= y;

+    assume {:inferred} x + 1 <= y;

+    assume {:inferred} x + 1 <= y;

     return;

 }

 

@@ -267,32 +267,32 @@ implementation p()
 {

 

   A:

-    assume true;

+    assume {:inferred} true;

     assume 0 - 1 <= x;

-    assume -1 <= x;

+    assume {:inferred} -1 <= x;

     goto B, E;

 

   B:

-    assume -1 <= x;

+    assume {:inferred} -1 <= x;

     assume x < y;

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

+    assume {:inferred} x + 1 <= y && -1 <= x;

     goto C, E;

 

   C:

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

+    assume {:inferred} x + 1 <= y && -1 <= x;

     x := x * x;

-    assume 0 <= y;

+    assume {:inferred} 0 <= y;

     goto D, E;

 

   D:

-    assume 0 <= y;

+    assume {:inferred} 0 <= y;

     x := y;

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

+    assume {:inferred} x == y && 0 <= y;

     return;

 

   E:

-    assume true;

-    assume true;

+    assume {:inferred} true;

+    assume {:inferred} true;

     return;

 }

 

@@ -315,26 +315,26 @@ implementation p()
 {

 

   A:

-    assume true;

+    assume {:inferred} true;

     x := 8;

-    assume x == 8;

+    assume {:inferred} x == 8;

     goto B, C;

 

   B:

-    assume x == 8;

+    assume {:inferred} x == 8;

     x := 9;

-    assume x == 9;

+    assume {:inferred} x == 9;

     goto D;

 

   C:

-    assume x == 8;

+    assume {:inferred} x == 8;

     x := 10;

-    assume x == 10;

+    assume {:inferred} x == 10;

     goto D;

 

   D:

-    assume 9 <= x && x <= 10;

-    assume 9 <= x && x <= 10;

+    assume {:inferred} 9 <= x && x <= 10;

+    assume {:inferred} 9 <= x && x <= 10;

     return;

 }

 

@@ -356,25 +356,25 @@ implementation p()
 {

 

   A:

-    assume true;

-    assume true;

+    assume {:inferred} true;

+    assume {:inferred} true;

     goto B, C;

 

   B:

-    assume true;

-    assume x <= 0;

+    assume {:inferred} true;

     assume x <= 0;

+    assume {:inferred} x <= 0;

     goto D;

 

   C:

-    assume true;

-    assume y <= 0;

+    assume {:inferred} true;

     assume y <= 0;

+    assume {:inferred} y <= 0;

     goto D;

 

   D:

-    assume true;

-    assume true;

+    assume {:inferred} true;

+    assume {:inferred} true;

     return;

 }

 

@@ -393,7 +393,7 @@ implementation foo()
   var n: int;

 

   A:

-    assume true;

+    assume {:inferred} true;

     n := 0;

     j := 0;

     i := j + 1;

@@ -402,7 +402,7 @@ implementation foo()
     i := i + 1;

     i := i + 1;

     j := j + 1;

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

+    assume {:inferred} i == j + 4 && j == 1 && n == 0;

     return;

 }

 

@@ -421,24 +421,24 @@ implementation foo()
   var n: int;

 

   entry:

-    assume true;

+    assume {:inferred} true;

     assume n >= 4;

     i := 0;

     j := i + 1;

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

+    assume {:inferred} j == i + 1 && i == 0 && 4 <= n;

     goto exit, loop0;

 

   loop0:  // cut point

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

+    assume {:inferred} 4 <= n && 0 <= i && j == i + 1;

     assume j <= n;

     i := i + 1;

     j := j + 1;

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

+    assume {:inferred} j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;

     goto loop0, exit;

 

   exit:

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

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

+    assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;

+    assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;

     return;

 }