Dafny: implemented thresholds for the new interval domain (/infer:j)

5 files changed, 136 insertions, 2 deletions

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index e517aa18..73a9509c 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -109,5 +109,15 @@ implementation Evaluate()
 

 

 Boogie program verifier finished with 0 verified, 0 errors

-

-Boogie program verifier finished with 1 verified, 0 errors

+Intervals.bpl(62,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(57,5): anon0

+    Intervals.bpl(58,3): anon3_LoopHead

+    Intervals.bpl(58,3): anon3_LoopDone

+Intervals.bpl(73,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(68,5): anon0

+    Intervals.bpl(69,3): anon3_LoopHead

+    Intervals.bpl(69,3): anon3_LoopDone

+

+Boogie program verifier finished with 4 verified, 2 errors

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 49d27b1c..7ed2c3d2 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -17,3 +17,59 @@ procedure P(K: int)
   }

   assert 13 <= x;

 }

+

+procedure Thresholds0()

+{

+  var i: int;

+  i := 0;

+  while (i < 200)

+  {

+    i := i + 1;

+  }

+  assert i == 200;

+}

+

+procedure Thresholds1()

+{

+  var i: int;

+  i := 0;

+  while (i <= 199)

+  {

+    i := i + 1;

+  }

+  assert i == 200;

+}

+

+procedure Thresholds2()

+{

+  var i: int;

+  i := 100;

+  while (0 < i)

+  {

+    i := i - 1;

+  }

+  assert i == 0;

+}

+

+procedure Thresholds3()

+{

+  var i: int;

+  i := 0;

+  while (i < 200)

+  {

+    i := i + 1;

+  }

+  assert i == 199;  // error

+}

+

+procedure Thresholds4()

+{

+  var i: int;

+  i := 0;

+  while (i + 3 < 203)

+  {

+    i := i + 1;

+  }

+  assert i * 2 == 400;  // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200

+}

+

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 9cb94f69..ea481dae 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -26,3 +26,7 @@ Dafny program verifier finished with 4 verified, 0 errors
 -------------------- COST-verif-comp-2011-4-FloydCycleDetect.dfy --------------------

 

 Dafny program verifier finished with 23 verified, 0 errors

+

+-------------------- Intervals.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny2/Intervals.dfy b/Test/dafny2/Intervals.dfy
new file mode 100644
index 00000000..f04f6411
--- /dev/null
+++ b/Test/dafny2/Intervals.dfy
@@ -0,0 +1,63 @@
+// The RoundDown and RoundUp methods in this file are the ones in the Boogie

+// implementation Source/AbsInt/IntervalDomain.cs.

+

+var thresholds: array<int>;

+

+function Valid(): bool

+  reads this, thresholds;

+{

+  thresholds != null &&

+  forall m,n :: 0 <= m < n < thresholds.Length ==> thresholds[m] <= thresholds[n]

+}

+

+method RoundDown(k: int) returns (r: int)

+  requires Valid();

+  ensures -1 <= r < thresholds.Length;

+  ensures forall m :: r < m < thresholds.Length ==> k < thresholds[m];

+  ensures 0 <= r ==> thresholds[r] <= k;

+{

+  if (thresholds.Length == 0 || k < thresholds[0]) {

+    return -1;

+  }

+  var i, j := 0, thresholds.Length - 1;

+  while (i < j)

+    invariant 0 <= i <= j < thresholds.Length;

+    invariant thresholds[i] <= k;

+    invariant forall m :: j < m < thresholds.Length ==> k < thresholds[m];

+  {

+    var mid := i + (j - i + 1) / 2;

+    assert i < mid <= j;

+    if (thresholds[mid] <= k) {

+      i := mid;

+    } else {

+      j := mid - 1;

+    }

+  }

+  return i;

+}

+

+method RoundUp(k: int) returns (r: int)

+  requires Valid();

+  ensures 0 <= r <= thresholds.Length;

+  ensures forall m :: 0 <= m < r ==> thresholds[m] < k;

+  ensures r < thresholds.Length ==> k <= thresholds[r];

+{

+  if (thresholds.Length == 0 || thresholds[thresholds.Length-1] < k) {

+    return thresholds.Length;

+  }

+  var i, j := 0, thresholds.Length - 1;

+  while (i < j)

+    invariant 0 <= i <= j < thresholds.Length;

+    invariant k <= thresholds[j];

+    invariant forall m :: 0 <= m < i ==> thresholds[m] < k;

+  {

+    var mid := i + (j - i) / 2;

+    assert i <= mid < j;

+    if (thresholds[mid] < k) {

+      i := mid + 1;

+    } else {

+      j := mid;

+    }

+  }

+  return i;

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index d7c0dc79..79ee0f89 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -14,6 +14,7 @@ for %%f in (
     COST-verif-comp-2011-2-MaxTree-datatype.dfy

     COST-verif-comp-2011-3-TwoDuplicates.dfy

     COST-verif-comp-2011-4-FloydCycleDetect.dfy

+    Intervals.dfy

   ) do (

   echo.

   echo -------------------- %%f --------------------