Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression

11 files changed, 97 insertions, 27 deletions

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index cf109c1a..df8cb1b7 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -30,10 +30,8 @@ class AmortizedQueue<T> {
     modifies this;

     ensures Valid() && List == [];

   {

-    var tmp := new LinkedList<T>.Init();

-    front := tmp;

-    tmp := new LinkedList<T>.Init();

-    rear := tmp;

+    front := new LinkedList<T>.Init();

+    rear := new LinkedList<T>.Init();

     Repr := {this};

     Repr := Repr + front.Repr + rear.Repr;

     List := [];

@@ -52,8 +50,7 @@ class AmortizedQueue<T> {
       call ff := f.Concat(rr);

       front := ff;

 

-      var tmp := new LinkedList<T>.Init();

-      rear := tmp;

+      rear := new LinkedList<T>.Init();

     }

     Repr := {this};

     Repr := Repr + front.Repr + rear.Repr;

@@ -79,8 +76,7 @@ class AmortizedQueue<T> {
     ensures r != null && r.Valid() && r.List == List + [item];

   {

     call rr := rear.Cons(item);

-    var tmp := new AmortizedQueue<T>.InitFromPieces(front, rr);

-    r := tmp;

+    r := new AmortizedQueue<T>.InitFromPieces(front, rr);

   }

 }

 

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 02c1a63a..3438d6e0 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -48,7 +48,7 @@ class Glossary {
     var rs:= new ReaderStream;

     call rs.Open();

     var glossary := new Map<Word,seq<Word>>.Init();

-    var q:= new Queue<Word>.Init();

+    var q := new Queue<Word>.Init();

     

     while (true)

       invariant rs.Valid() && fresh(rs.footprint);

diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy
new file mode 100644
index 00000000..b73af758
--- /dev/null
+++ b/Test/dafny0/AdvancedLHS.dfy
@@ -0,0 +1,59 @@
+class C {

+  var x: C;

+

+  method M(S: set<C>, a: array<C>, b: array2<C>)

+    requires S != {};

+    modifies this, a, b;

+  {

+    x := new C;

+    x := new C.Init();

+    havoc x;

+    x := choose(S);

+

+    // test evaluation order

+    var c := x;

+    x := null;

+    x := new C.InitOther(x);  // since the parameter is evaluated before the LHS is set, the precondition is met

+    assert x != c;

+

+    // test evaluation order and modification

+    if (*) {

+      var k := this.x;

+      var kx := this.x.x;

+      this.x.x := new C.InitAndMutate(this);

+      assert this.x == null;

+      assert this.x != k;

+      assert k.x != kx;  // because it was set to a new object

+      assert fresh(k.x);

+    } else {

+      var k := this.x;

+      var kx := this.x.x;

+      this.x.x := new C.InitAndMutate(this);

+      var t := this.x.x;  // error: null dereference (because InitAndMutate set this.x to null)

+    }

+

+    if (a != null && 10 <= a.Length) {

+      a[2] := new C;

+      a[4..8] := null;

+      havoc a[3];

+    }

+    if (b != null && 10 <= b.Length0 && 20 <= b.Length1) {

+      b[2,14] := new C;

+      havoc b[3,11];

+    }

+  }

+

+  method Init() { }

+  method InitOther(c: C)

+    requires c == null;

+  {

+    var d := new int[if c == null then 10 else -3];  // run-time error if c were non-null, but it ain't

+  }

+  method InitAndMutate(c: C)

+    requires c != null;

+    modifies c;

+    ensures c.x == null;

+  {

+    c.x := null;

+  }

+}

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index f57c6ead..eb85403e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -81,7 +81,9 @@ TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
 TypeTests.dfy(72,6): Error: Duplicate local-variable name: y

 TypeTests.dfy(79,17): Error: member F in class C does not refer to a method

 TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments

-16 resolution/type errors detected in TypeTests.dfy

+TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+18 resolution/type errors detected in TypeTests.dfy

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

@@ -418,6 +420,14 @@ NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be
 NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 8 resolution/type errors detected in NonGhostQuantifiers.dfy

 

+-------------------- AdvancedLHS.dfy --------------------

+AdvancedLHS.dfy(32,23): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon15_Else

+

+Dafny program verifier finished with 7 verified, 1 error

+

 -------------------- Modules0.dfy --------------------

 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

 Modules0.dfy(13,7): Error: module T named among imports does not exist

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 048ecd7a..60854f63 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -37,10 +37,10 @@ class A {
   method O() {

     var zz2 := new A[25];

     assert zz2 != zz0;  // holds because zz2 is newly allocated

-    /******  These would be good things to be able to verify, but the current encoding is not up to the task

     var o: object := zz0;

     assert this != o;  // holds because zz0 has a different type

-    if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) {

+    /******  This would be a good thing to be able to verify, but the current encoding is not up to the task

+    if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) {

       o := zz1[1];

       assert zz0[1] == o ==> o == null;  // holds because zz0 and zz1 have different element types

     }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index cbab53bf..93c4aec4 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -80,3 +80,12 @@ method InitCalls() {
   var d := new C.M(8);  // error: M has out parameters

   var e := new C.Caller();

 }

+

+// ---------------------

+

+method ArrayRangeAssignments(a: array<C>)

+  requires a != null && 10 <= a.Length;

+{

+  a[0..5] := new C;  // this is not allowed

+  havoc a[1..4];  // this is not allowed

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 2c55a6b9..6a2f2cb5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -12,7 +12,7 @@ for %%f in (Simple.dfy) do (
 )

 

 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy

-            Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy

+            Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index b790eea5..4ceca552 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -39,7 +39,7 @@ class ExtensibleArray<T> {
     ensures Valid() && fresh(Repr - {this});

     ensures Contents == [];

   {

-    var arr := new T[256];  elements := arr;

+    elements := new T[256];

     more := null;

     length := 0;

     M := 0;

@@ -90,15 +90,14 @@ class ExtensibleArray<T> {
       elements[length - M] := t;

     } else {

       if (more == null) {

-        var mr := new ExtensibleArray<array<T>>.Init();

-        more := mr;

-        Repr := Repr + {mr} + mr.Repr;

+        more := new ExtensibleArray<array<T>>.Init();

+        Repr := Repr + {more} + more.Repr;

       }

       // "elements" is full, so move it into "more" and allocate a new array

       call more.Append(elements);

       Repr := Repr + more.Repr;

       M := M + 256;

-      var arr := new T[256];  elements := arr;

+      elements := new T[256];

       Repr := Repr + {elements};

       elements[0] := t;

     }

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 957eb7cb..db1c60fa 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -27,8 +27,7 @@ class PriorityQueue {
     ensures N == capacity;

   {

     N := capacity;

-    var arr := new int[N+1];

-    a := arr;

+    a := new int[N+1];

     n := 0;

     Repr := {this};

     Repr := Repr + {a};

@@ -143,8 +142,7 @@ class PriorityQueue_Alternative {
     ensures N == capacity;

   {

     N := capacity;

-    var arr := new int[N+1];

-    a := arr;

+    a := new int[N+1];

     n := 0;

     Repr := {this};

     Repr := Repr + {a};

diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 940e1a0a..dfc10327 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -31,8 +31,7 @@ class UnboundedStack<T> {
     ensures IsUnboundedStack();

     ensures content == [val] + old(content);

   {

-    var tmp := new Node<T>.InitNode(val,top);

-    top := tmp;

+    top := new Node<T>.InitNode(val,top);

     representation := representation + top.footprint;

     content := [val] + content;

   }

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index fc4d687d..e56a8317 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -41,9 +41,9 @@ class LazyInitArray<T> {
     ensures |Contents| == N && Zero == zero;

     ensures (forall x :: x in Contents ==> x == zero);

   {

-    var aa := new T[N+1];  a := aa;

-    var ii := new int[N];  b := ii;

-    ii := new int[N];      c := ii;

+    a := new T[N+1];

+    b := new int[N];

+    c := new int[N];

     n := 0;

 

     // initialize ghost variable Contents to a sequence of length N containing only zero's,