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}

5 files changed, 110 insertions, 116 deletions

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 58750460..e517aa18 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -18,34 +18,34 @@ implementation Join(b: bool)
   var z: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     GlobalFlag := true;

     x := 3;

     y := 4;

     z := x + y;

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     goto Then, Else;

 

   Then:

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     assume b <==> true;

     x := x + 1;

-    assume x == 4 && y == 4 && z == 7;

+    assume {:inferred} x == 4 && y == 4 && z == 7;

     goto join;

 

   Else:

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     assume b <==> false;

     y := 4;

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     goto join;

 

   join:

-    assume y == 4 && z == 7;

+    assume {:inferred} y == 4 && z == 7;

     assert y == 4;

     assert z == 7;

     assert GlobalFlag <==> true;

-    assume y == 4 && z == 7;

+    assume {:inferred} y == 4 && z == 7;

     return;

 }

 

@@ -61,27 +61,27 @@ implementation Loop()
   var i: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     c := 0;

     i := 0;

-    assume c == 0 && i == 0;

+    assume {:inferred} c == 0 && i == 0;

     goto test;

 

   test:  // cut point

-    assume c == 0;

-    assume c == 0;

+    assume {:inferred} c == 0;

+    assume {:inferred} c == 0;

     goto Then, Else;

 

   Then:

-    assume c == 0;

+    assume {:inferred} c == 0;

     assume i < 10;

     i := i + 1;

-    assume c == 0;

+    assume {:inferred} c == 0;

     goto test;

 

   Else:

-    assume c == 0;

-    assume c == 0;

+    assume {:inferred} c == 0;

+    assume {:inferred} c == 0;

     return;

 }

 

@@ -96,16 +96,18 @@ implementation Evaluate()
   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 i == 465;

+    assume {:inferred} i == 465;

     return;

 }

 

 

 

 Boogie program verifier finished with 0 verified, 0 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
new file mode 100644
index 00000000..49d27b1c
--- /dev/null
+++ b/Test/aitest0/Intervals.bpl
@@ -0,0 +1,19 @@
+const N: int;

+axiom 0 <= N;

+

+procedure P(K: int)

+  requires 0 <= K;

+{

+  var b: bool, x, k: int;

+

+  if (!b) {

+    b := !b;

+  }

+  x := if b then 13 else 10;

+  k := K;

+  while (k != 0) {

+    x := x + k;

+    k := k - 1;

+  }

+  assert 13 <= x;

+}

diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
index a4c12d8d..1cb7a60c 100644
--- a/Test/aitest0/runtest.bat
+++ b/Test/aitest0/runtest.bat
@@ -4,3 +4,4 @@ setlocal
 set BGEXE=..\..\Binaries\Boogie.exe

 

 %BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl

+%BGEXE% %* -infer:j Intervals.bpl

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;

 }

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 15cec24f..aab1990d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -307,7 +307,6 @@ Execution trace:
     (0,0): anon0

 Definedness.dfy(105,15): Error: possible division by zero

 Execution trace:

-    (0,0): anon0

     Definedness.dfy(105,5): anon8_LoopHead

     (0,0): anon8_LoopBody

     Definedness.dfy(105,5): anon9_Else

@@ -799,13 +798,11 @@ Execution trace:
     ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

     ControlStructures.dfy(194,3): anon64_Else

-    (0,0): anon5

     ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

     ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

     ControlStructures.dfy(198,5): anon67_Else

-    (0,0): anon10

     (0,0): anon71_Then

     ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

@@ -821,20 +818,17 @@ Execution trace:
     ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

     ControlStructures.dfy(194,3): anon64_Else

-    (0,0): anon5

     ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

     ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

     ControlStructures.dfy(198,5): anon67_Else

-    (0,0): anon10

     (0,0): anon71_Then

     ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

     ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

     ControlStructures.dfy(210,9): anon74_Else

-    (0,0): anon22

     (0,0): anon75_Then

     (0,0): after_4

     ControlStructures.dfy(221,7): anon77_LoopHead

@@ -842,7 +836,6 @@ Execution trace:
     ControlStructures.dfy(221,7): anon78_Else

     (0,0): anon33

     ControlStructures.dfy(221,7): anon79_Else

-    (0,0): anon35

     (0,0): anon81_Then

     (0,0): anon38

     (0,0): after_9

@@ -856,13 +849,11 @@ Execution trace:
     ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

     ControlStructures.dfy(194,3): anon64_Else

-    (0,0): anon5

     ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

     ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

     ControlStructures.dfy(198,5): anon67_Else

-    (0,0): anon10

     (0,0): anon68_Then

     (0,0): after_5

     (0,0): anon87_Then

@@ -876,20 +867,17 @@ Execution trace:
     ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

     ControlStructures.dfy(194,3): anon64_Else

-    (0,0): anon5

     ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

     ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

     ControlStructures.dfy(198,5): anon67_Else

-    (0,0): anon10

     (0,0): anon71_Then

     ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

     ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

     ControlStructures.dfy(210,9): anon74_Else

-    (0,0): anon22

     (0,0): anon75_Then

     (0,0): after_4

     ControlStructures.dfy(221,7): anon77_LoopHead

@@ -897,7 +885,6 @@ Execution trace:
     ControlStructures.dfy(221,7): anon78_Else

     (0,0): anon33

     ControlStructures.dfy(221,7): anon79_Else

-    (0,0): anon35

     (0,0): anon82_Then

     (0,0): anon85_Then

     (0,0): after_8

@@ -915,7 +902,6 @@ Execution trace:
     Termination.dfy(105,3): anon8_Else

     (0,0): anon3

     Termination.dfy(105,3): anon9_Else

-    (0,0): anon5

 Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

@@ -925,7 +911,6 @@ Execution trace:
     (0,0): anon11_Then

     (0,0): anon5

     Termination.dfy(113,3): anon12_Else

-    (0,0): anon7

 Termination.dfy(122,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

@@ -935,7 +920,6 @@ Execution trace:
     (0,0): anon11_Then

     (0,0): anon5

     Termination.dfy(122,3): anon12_Else

-    (0,0): anon7

 Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

 Execution trace:

     (0,0): anon0

@@ -945,7 +929,6 @@ Execution trace:
     (0,0): anon11_Then

     (0,0): anon5

     Termination.dfy(122,3): anon12_Else

-    (0,0): anon7

 Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon6_Else

@@ -959,7 +942,6 @@ Execution trace:
     Termination.dfy(291,3): anon11_Else

     Termination.dfy(291,3): anon12_Else

     (0,0): anon13_Else

-    (0,0): anon8

 

 Dafny program verifier finished with 45 verified, 6 errors

 

@@ -1131,7 +1113,6 @@ Execution trace:
     TypeParameters.dfy(153,3): anon22_Else

     (0,0): anon13

     TypeParameters.dfy(153,3): anon24_Else

-    (0,0): anon15

 

 Dafny program verifier finished with 35 verified, 5 errors

 

@@ -1224,7 +1205,6 @@ Execution trace:
     LoopModifies.dfy(14,4): anon10_Else

     (0,0): anon5

     LoopModifies.dfy(14,4): anon12_Else

-    (0,0): anon7

 LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -1233,7 +1213,6 @@ Execution trace:
     LoopModifies.dfy(42,4): anon10_Else

     (0,0): anon5

     LoopModifies.dfy(42,4): anon12_Else

-    (0,0): anon7

 LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -1242,7 +1221,6 @@ Execution trace:
     LoopModifies.dfy(57,4): anon10_Else

     (0,0): anon5

     LoopModifies.dfy(57,4): anon12_Else

-    (0,0): anon7

 LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -1254,7 +1232,6 @@ Execution trace:
     LoopModifies.dfy(90,4): anon10_Else

     (0,0): anon5

     LoopModifies.dfy(90,4): anon12_Else

-    (0,0): anon7

 LoopModifies.dfy(146,11): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -1263,13 +1240,11 @@ Execution trace:
     LoopModifies.dfy(134,4): anon18_Else

     (0,0): anon5

     LoopModifies.dfy(134,4): anon20_Else

-    (0,0): anon7

     LoopModifies.dfy(139,7): anon21_LoopHead

     (0,0): anon21_LoopBody

     LoopModifies.dfy(139,7): anon22_Else

     (0,0): anon12

     LoopModifies.dfy(139,7): anon24_Else

-    (0,0): anon14

 LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -1278,7 +1253,6 @@ Execution trace:
     LoopModifies.dfy(193,4): anon10_Else

     (0,0): anon5

     LoopModifies.dfy(193,4): anon12_Else

-    (0,0): anon7

 LoopModifies.dfy(285,13): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -1287,13 +1261,11 @@ Execution trace:
     LoopModifies.dfy(273,4): anon18_Else

     (0,0): anon5

     LoopModifies.dfy(273,4): anon20_Else

-    (0,0): anon7

     LoopModifies.dfy(281,7): anon21_LoopHead

     (0,0): anon21_LoopBody

     LoopModifies.dfy(281,7): anon22_Else

     (0,0): anon12

     LoopModifies.dfy(281,7): anon24_Else

-    (0,0): anon14

 

 Dafny program verifier finished with 23 verified, 9 errors