Dafny: Added definedness checks for all statements (previously, some were missing)

Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting

1 files changed, 163 insertions, 6 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 3e626f25..3bf5ed3f 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -58,9 +58,9 @@ class Node {
   }

 

   function PoorlyDefined(x: int): int

-    requires if next == null then 5/x < 20 else true;  // ill-defined then branch

-    requires if next == null then true else 0 <= 5/x;  // ill-defined then branch

-    requires if next.next == null then true else true;  // ill-defined guard

+    requires if next == null then 5/x < 20 else true;  // error: ill-defined then branch

+    requires if next == null then true else 0 <= 5/x;  // error: ill-defined then branch

+    requires if next.next == null then true else true;  // error: ill-defined guard

     requires 10/x != 8;  // this is well-defined, because we get here only if x is non-0

     reads this;

   {

@@ -79,9 +79,9 @@ class Modifies {
   {

     x := x + 1;

     while (p != null && p.x < 75)

-      decreases 75 - p.x;

-    {

-      p.x := p.x + 1;

+      decreases 75 - p.x;  // error: not defined at top of each iteration (there's good reason to

+    {                      // insist on this; for example, the decrement check could not be performed

+      p.x := p.x + 1;      // at the end of the loop body if p were set to null in the loop body)

     }

   }

 

@@ -213,3 +213,160 @@ class SoWellformed {
     modifies s;

     ensures next.xyz < 100;  // fine

 }

+

+// ---------------------- welldefinedness checks for statements -------------------

+

+class StatementTwoShoes {

+  var x: int;

+

+  function method F(b: int): StatementTwoShoes

+    requires 0 <= b;

+  {

+    this

+  }

+

+  method M(p: StatementTwoShoes, a: int)

+    modifies this, p;

+  {

+    p.x := a;  // error: receiver may be null

+    F(a).x := a;  // error: LHS may not be well defined

+    x := F(a-10).x;  // error: RHS may not be well defined

+  }

+

+  method N(a: int, b: int)

+  {

+    assert 5 / a == 5 / a;  // error: expression may not be well defined

+    assume 20 / b == 5;  // error: expression may not be well defined

+  }

+

+  method O(a: int) returns (b: int)

+  {

+    if (20 / a == 5) {  // error: expression may not be well defined

+      b := a;

+    }

+  }

+

+  method P(a: int)

+  {

+    while (20 / a == 5) {  // error: expression may not be well defined

+      break;

+    }

+  }

+

+  method Q(a: int, b: int)

+  {

+    var i := 1;

+    while (i < a)

+      decreases F(i), F(a), a - i;  // error: component 1 may not be well defined

+    {

+      i := i + 1;

+    }

+    i := 1;

+    while (i < a)

+      decreases F(b), a - i;  // error: component 0 may not be well defined

+    {

+      i := i + 1;

+    }

+  }

+

+  method R(a: int)

+  {

+    var i := 0;

+    while (i < 100)  // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption

+      invariant F(a) != null;  // error: expression may not be well defined, and error: loop invariant may not hold

+      decreases F(a), 100 - i;  // error: component 0 not well defined

+    {

+      i := i + 1;

+    }

+  }

+

+  method S(a: int)

+  {

+    var j := 0;

+    while (20 / a == 5 && j < 100)  // error: guard may not be well defined

+      invariant j <= 100;

+      decreases F(101 - j), 100 - j;

+    {

+      j := j + 1;

+    }

+  }

+

+  method T(a: int)

+    requires a != 0 && 20 / a == 5;

+  {

+    var k := a;

+    var j := 0;

+    while (20 / k == 5 && j < 100)  // fine

+      decreases 100 - j;

+    {

+      j := j + 1;

+    }

+    j := 0;

+    while (20 / k == 5 && j < 100)  // error: guard may not be well defined

+      decreases 100 - j;

+    {

+      havoc k;

+      j := j + 1;

+    }

+  }

+

+  method U()

+  {

+    var i := 0;

+    while (i < 100)

+      invariant i <= 100;

+      decreases 100 - i;

+      invariant F(123 - i) == this;

+    {

+      i := i + 1;

+    }

+    i := 0;

+    while (i < 100)

+      decreases 100 - i;

+      invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined

+    {

+      i := i + 1;

+      if (i == 77) { i := i + 1; }

+    }

+  }

+

+  use function G(w: int): int { 5 }

+  function method H(x: int): int;

+

+  method V(s: set<StatementTwoShoes>, a: int, b: int)

+    modifies s;

+  {

+    use G(12 / b);  // fine, because there are no welldefinedness checks on use statements

+    foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null

+    {

+      assume 0 <= m.x;

+      assert m.x < 1000;

+      use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements

+      m.x := m.x + 1;

+    }

+    foreach (m in s + {F(a)})  // error: collection expression may not be well defined

+    {

+      m.x := 5;  // error: possible modifies clause violation

+    }

+    foreach (m in s | F(H(m.x)) == this)  // error: range expression may not be well defined

+    {

+      m.x := H(m.x);

+    }

+    foreach (m in s)

+    {

+      m.x := 100 / m.x;  // error: RhS may not be well defined

+    }

+  }

+

+  method W(x: int)

+  {

+    var i := 0;

+    while (i < 100)

+      // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking

+      invariant 5 / x != 5 / x;  // error: not well-defined, and error: loop invariant does not hold initially

+      decreases 100 - i;

+    {

+      i := i + 1;

+    }

+  }

+}