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

7 files changed, 361 insertions, 87 deletions

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 457bc894..7d964061 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -17,7 +17,7 @@ class Benchmark2 {
     var high := a.Length();

 

     while (low < high)

-      invariant 0 <= low && high <= a.Length();

+      invariant 0 <= low && low <= high && high <= a.Length();

       invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);

       invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));

       decreases high - low;

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index d45db684..37b73cba 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -61,10 +61,10 @@ class Benchmark3 {
     

     var n := 0;

 	while (n < |q.contents|)

-		invariant n <=|q.contents| ;

-		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

+		invariant n <= |q.contents|;

 		invariant n == |p|;

-		decreases |q.contents| -n;

+		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

+		decreases |q.contents| - n;

    {

 		p := p + [n];

 		n := n + 1;

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index d320f9e9..90f484bd 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -6,22 +6,22 @@ class Collection<T> {
   function Valid():bool

   reads this, footprint;

   {

-		this in footprint

+    this in footprint

   }

   

   method GetCount() returns (c:int)

   requires Valid();

   ensures 0<=c;

   {

-		c:=|elements|;

+    c:=|elements|;

   }

   

   method Init()

   modifies this;

   ensures Valid() && fresh(footprint -{this});

   {

-		elements := [];

-		footprint := {this}; 

+    elements := [];

+    footprint := {this}; 

   }

   

   method GetItem(i:int ) returns (x:T)

@@ -29,7 +29,7 @@ class Collection<T> {
   requires 0<=i && i<|elements|;

   ensures elements[i] ==x;

   {

-		x:=elements[i];

+    x:=elements[i];

   }

   

   method Add(x:T )

@@ -38,7 +38,7 @@ class Collection<T> {
   ensures Valid() && fresh(footprint - old(footprint));

   ensures elements == old(elements) + [x];

   {

-		elements:= elements + [x];

+    elements:= elements + [x];

   }

   

   method GetIterator() returns (iter:Iterator<T>)

@@ -63,7 +63,7 @@ class Iterator<T> {
   function Valid():bool

   reads this, footprint;

   {

-		this in footprint && c!= null && -1<= pos && null !in footprint

+    this in footprint && c!= null && -1<= pos && null !in footprint

   }

   

   method Init(coll:Collection<T>)

@@ -72,9 +72,9 @@ class Iterator<T> {
   ensures Valid() && fresh(footprint -{this}) && pos ==-1;

   ensures c == coll;

   {

-		c:= coll;

-		pos:=-1;

-		footprint := {this}; 

+    c:= coll;

+    pos:=-1;

+    footprint := {this}; 

   }

   

   method MoveNext() returns (b:bool)

@@ -83,22 +83,22 @@ class Iterator<T> {
   ensures fresh(footprint - old(footprint)) &&  Valid()  && pos == old(pos) + 1;

   ensures b == HasCurrent() && c == old(c);

   {

-	pos:= pos+1;

-	b:= pos < |c.elements|;

+  pos:= pos+1;

+  b:= pos < |c.elements|;

   }

   

  function HasCurrent():bool //???

- requires Valid();

- reads this, c;

+   requires Valid();

+   reads this, c;

  {

-	0<= pos && pos < |c.elements|

+  0<= pos && pos < |c.elements|

  }

  

  method GetCurrent() returns (x:T)

  requires Valid() && HasCurrent();

  ensures c.elements[pos] == x;

   {

-		x:=c.elements[pos];

+    x:=c.elements[pos];

   }

  

 } 

@@ -106,34 +106,34 @@ class Iterator<T> {
 class Client

 {

 

-	method Main()

-	{

-		var c:= new Collection<int>;

-		call c.Init();

-		call c.Add(33);

-		call c.Add(45);

-		call c.Add(78);

-		

-		var s:= [ ];

-		

-		call iter:=c.GetIterator();

-		call b:= iter.MoveNext();

-		

-		while (b)

-		invariant b == iter.HasCurrent() && fresh(iter.footprint) && iter.Valid();

-		invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints

-		invariant 0<= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;

-		invariant iter.c == c;

-		decreases |c.elements| - iter.pos;

-		{   

-			call x:= iter.GetCurrent();

-			s:= s + [x];

-			call b:= iter.MoveNext();

-		}

-		

-		assert s == c.elements; //verifies that the iterator returns the correct things

-		call c.Add(100);

-	}

-	

+  method Main()

+  {

+    var c:= new Collection<int>;

+    call c.Init();

+    call c.Add(33);

+    call c.Add(45);

+    call c.Add(78);

+    

+    var s:= [ ];

+    

+    call iter := c.GetIterator();

+    call b := iter.MoveNext();

+    

+    while (b)

+      invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);

+      invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints

+      invariant 0 <= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;

+      invariant iter.c == c;

+      decreases |c.elements| - iter.pos;

+    {   

+      call x:= iter.GetCurrent();

+      s:= s + [x];

+      call b:= iter.MoveNext();

+    }

+    

+    assert s == c.elements; //verifies that the iterator returns the correct things

+    call c.Add(100);

+  }

+  

 }

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a364d4e9..3186ae01 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -98,6 +98,12 @@ Execution trace:
     (0,0): anon3

     (0,0): anon11_Then

     (0,0): anon6

+SmallTests.dfy(82,20): Error: decreases expression must be well defined at top of each loop iteration

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(81,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    (0,0): anon8_Then

 SmallTests.dfy(95,5): Error: call may violate caller's modifies clause

 Execution trace:

     (0,0): anon0

@@ -141,103 +147,214 @@ Execution trace:
 SmallTests.dfy(209,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

+SmallTests.dfy(231,9): Error: LHS expression must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(232,12): Error: LHS expression must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(233,7): Error: RHS expression must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(238,18): Error: assert condition must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(239,5): Error: assume condition must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(244,16): Error: if guard must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(251,19): Error: loop guard must be well defined

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(251,5): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    SmallTests.dfy(251,5): anon9_Else

+    (0,0): anon3

+SmallTests.dfy(260,23): Error: decreases expression must be well defined at top of each loop iteration

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(259,5): anon13_LoopHead

+    (0,0): anon13_LoopBody

+    (0,0): anon14_Then

+SmallTests.dfy(266,17): Error: decreases expression must be well defined at top of each loop iteration

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(259,5): anon13_LoopHead

+    (0,0): anon13_LoopBody

+    SmallTests.dfy(259,5): anon14_Else

+    (0,0): anon3

+    (0,0): anon15_Then

+    (0,0): anon6

+    SmallTests.dfy(265,5): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    (0,0): anon17_Then

+SmallTests.dfy(276,22): Error: loop invariant must be well defined

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(275,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    (0,0): anon8_Then

+SmallTests.dfy(276,22): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(277,17): Error: decreases expression must be well defined at top of each loop iteration

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(275,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    (0,0): anon8_Then

+SmallTests.dfy(286,24): Error: loop guard must be well defined

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(286,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    SmallTests.dfy(286,5): anon8_Else

+    (0,0): anon3

+SmallTests.dfy(305,24): Error: loop guard must be well defined

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(299,5): anon13_LoopHead

+    (0,0): anon13_LoopBody

+    SmallTests.dfy(299,5): anon14_Else

+    (0,0): anon3

+    (0,0): anon15_Then

+    (0,0): anon6

+    SmallTests.dfy(305,5): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    SmallTests.dfy(305,5): anon17_Else

+    (0,0): anon9

+SmallTests.dfy(326,44): Error: loop invariant must be well defined

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(316,5): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    SmallTests.dfy(316,5): anon17_Else

+    (0,0): anon3

+    (0,0): anon18_Then

+    (0,0): anon6

+    SmallTests.dfy(324,5): anon19_LoopHead

+    (0,0): anon19_LoopBody

+    (0,0): anon20_Then

+SmallTests.dfy(347,21): Error: collection expression must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(349,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(351,33): Error: range expression must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(357,18): Error: RHS of assignment must be well defined

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(366,23): Error: loop invariant must be well defined

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(364,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    (0,0): anon8_Then

+SmallTests.dfy(366,23): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 30 verified, 16 errors

+Dafny program verifier finished with 43 verified, 38 errors

 

 -------------------- Queue.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 22 verified, 0 errors

 

 -------------------- ListCopy.dfy --------------------

 

-Dafny program verifier finished with 2 verified, 0 errors

+Dafny program verifier finished with 4 verified, 0 errors

 

 -------------------- BinaryTree.dfy --------------------

 

-Dafny program verifier finished with 13 verified, 0 errors

+Dafny program verifier finished with 24 verified, 0 errors

 

 -------------------- ListReverse.dfy --------------------

 

-Dafny program verifier finished with 1 verified, 0 errors

+Dafny program verifier finished with 2 verified, 0 errors

 

 -------------------- ListContents.dfy --------------------

 

-Dafny program verifier finished with 5 verified, 0 errors

+Dafny program verifier finished with 9 verified, 0 errors

 

 -------------------- SchorrWaite.dfy --------------------

 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 10 verified, 0 errors

 

 -------------------- Termination.dfy --------------------

 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 13 verified, 0 errors

 

 -------------------- Use.dfy --------------------

-Use.dfy(15,5): Error: assertion violation

+Use.dfy(15,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(26,5): Error: assertion violation

+Use.dfy(26,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(35,5): Error: assertion violation

+Use.dfy(35,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(56,5): Error: assertion violation

+Use.dfy(56,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(88,5): Error: assertion violation

+Use.dfy(88,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(130,5): Error: assertion violation

+Use.dfy(130,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(152,5): Error: assertion violation

+Use.dfy(144,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(170,5): Error: assertion violation

+Use.dfy(144,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(215,5): Error: assertion violation

+Use.dfy(215,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 20 verified, 9 errors

+Dafny program verifier finished with 38 verified, 9 errors

 

 -------------------- DTypes.dfy --------------------

-DTypes.dfy(15,5): Error: assertion violation

+DTypes.dfy(15,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-DTypes.dfy(28,5): Error: assertion violation

+DTypes.dfy(28,13): Error: assertion violation

 Execution trace:

     (0,0): anon0

-DTypes.dfy(54,5): Error: assertion violation

+DTypes.dfy(54,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 5 verified, 3 errors

+Dafny program verifier finished with 13 verified, 3 errors

 

 -------------------- TypeParameters.dfy --------------------

-TypeParameters.dfy(41,5): Error: assertion violation

+TypeParameters.dfy(41,22): Error: assertion violation

 Execution trace:

     (0,0): anon0

-TypeParameters.dfy(63,5): Error: assertion violation

+TypeParameters.dfy(63,27): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 10 verified, 2 errors

+Dafny program verifier finished with 20 verified, 2 errors

 

 -------------------- Datatypes.dfy --------------------

 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 10 verified, 0 errors

 

 -------------------- UnboundedStack.dfy --------------------

 

-Dafny program verifier finished with 7 verified, 0 errors

+Dafny program verifier finished with 12 verified, 0 errors

 

 -------------------- SumOfCubes.dfy --------------------

 

-Dafny program verifier finished with 10 verified, 0 errors

+Dafny program verifier finished with 17 verified, 0 errors

 

 -------------------- TerminationDemos.dfy --------------------

 

-Dafny program verifier finished with 7 verified, 0 errors

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 07dc2f7e..62636ce5 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -75,7 +75,7 @@ class Node<T> {
         (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);

       invariant

         (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);

-      decreases current, |current.list|;

+      decreases if current != null then |current.list| else -1;

     {

       var nx := current.next;

       assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma

diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index fb06d211..f429b9ed 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -115,7 +115,7 @@ class Main {
                   (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

       invariant (forall n :: n in S && n !in stackNodes && n != t ==>

                 n.childrenVisited == old(n.childrenVisited));

-      invariant (forall n: Node :: n.children == old(n.children));

+      invariant (forall n: Node :: n in S ==> n.children == old(n.children));

       invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);

       decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;

     {

@@ -205,7 +205,7 @@ class Main {
                   (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

       invariant (forall n :: n in S && n !in stackNodes && n != t ==>

                 n.childrenVisited == old(n.childrenVisited));

-      invariant (forall n :: n in stackNodes || n.children == old(n.children));

+      invariant (forall n :: n in S ==> n in stackNodes || n.children == old(n.children));

       invariant (forall n :: n in stackNodes ==>

                   |n.children| == old(|n.children|) &&

                   (forall j :: 0 <= j && j < |n.children| ==>

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;

+    }

+  }

+}