Merge

9 files changed, 236 insertions, 17 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index b9f5e7e6..54a3de3b 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -2809,15 +2809,17 @@ namespace Microsoft.Dafny {
 

       } else if (expr is FunctionCallExpr) {

         var e = (FunctionCallExpr)expr;

-        if (e.Function != null && e.Function.IsGhost) {

-          Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");

-          return;

-        }

-        // function is okay, so check all NON-ghost arguments

-        CheckIsNonGhost(e.Receiver);

-        for (int i = 0; i < e.Function.Formals.Count; i++) {

-          if (!e.Function.Formals[i].IsGhost) {

-            CheckIsNonGhost(e.Args[i]);

+        if (e.Function != null) {

+          if (e.Function.IsGhost) {

+            Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");

+            return;

+          }

+          // function is okay, so check all NON-ghost arguments

+          CheckIsNonGhost(e.Receiver);

+          for (int i = 0; i < e.Function.Formals.Count; i++) {

+            if (!e.Function.Formals[i].IsGhost) {

+              CheckIsNonGhost(e.Args[i]);

+            }

           }

         }

         return;

@@ -2885,9 +2887,13 @@ namespace Microsoft.Dafny {
 #endif

       if (member == null) {

         // error has already been reported by ResolveMember

-      } else if (allowMethodCall && member is Method) {

-        // it's a method

-        return new CallRhs(e.tok, e.Receiver, e.Name, e.Args);

+      } else if (member is Method) {

+        if (allowMethodCall) {

+          // it's a method

+          return new CallRhs(e.tok, e.Receiver, e.Name, e.Args);

+        } else {

+          Error(e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, cce.NonNull(ctype).Name);

+        }

       } else if (!(member is Function)) {

         Error(e, "member {0} in type {1} does not refer to a function", e.Name, cce.NonNull(ctype).Name);

       } else {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 3ec3c291..1e400599 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3652,7 +3652,22 @@ namespace Microsoft.Dafny {
       }

       ProcessCallStmt(s.Tok, s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran);

       for (int i = 0; i < lhsBuilders.Count; i++) {

-        lhsBuilders[i](bLhss[i], builder, etran);

+        var lhs = s.Lhs[i];

+        Type lhsType = null;

+        if (lhs is IdentifierExpr) {

+          lhsType = lhs.Type;

+        } else if (lhs is FieldSelectExpr) {

+          var fse = (FieldSelectExpr)lhs;

+          lhsType = fse.Field.Type;

+        }

+

+        Bpl.Expr bRhs = bLhss[i];  // the RHS (bRhs) of the assignment to the actual call-LHS (lhs) was a LHS (bLhss[i]) in the Boogie call statement

+        if (lhsType != null) {

+          CheckSubrange(lhs.tok, bRhs, lhsType, builder);

+        }

+        bRhs = etran.CondApplyBox(lhs.tok, bRhs, lhs.Type, lhsType);

+

+        lhsBuilders[i](bRhs, builder, etran);

       }

       builder.Add(CaptureState(s.Tok));

     }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0c2e487a..a3e5e11f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -541,8 +541,20 @@ Array.dfy(183,1): Error BP5003: A postcondition might not hold on this return pa
 Array.dfy(182,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

+Array.dfy(198,10): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

+Array.dfy(199,5): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

 

-Dafny program verifier finished with 30 verified, 13 errors

+Dafny program verifier finished with 31 verified, 15 errors

 

 -------------------- MultiDimArray.dfy --------------------

 MultiDimArray.dfy(53,21): Error: assertion violation

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 6699e648..613cdd83 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -182,3 +182,24 @@ ghost method Fill_None(s: seq<int>)
   ensures forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j];

 {  // error: cannot prove postcondition

 }

+

+// -------------- some regression tests; there was a time when array-element LHSs of calls were not translated correctly

+

+method Test_ArrayElementLhsOfCall(a: array<int>, i: int, c: Cdefg<int>) returns (x: int)

+  requires a != null && c != null;

+  modifies a, c;

+{

+  if (0 <= i < a.Length) {

+    a[i] := x;

+    a[i] := Test_ArrayElementLhsOfCall(a, i-1, c);  // this line used to crash Dafny

+    c.t := x;

+    c.t := Test_ArrayElementLhsOfCall(a, i-1, c);  // this line used to crash Dafny

+    var n: nat;

+    n := x;  // error: subrange check is applied and it cannot be verified

+    n := Test_ArrayElementLhsOfCall(a, i-1, c);  // error: subrange check is applied and it cannot be verified

+  }

+}

+

+class Cdefg<T> {

+  var t: T;

+}

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 2dc49cd9..405f3e15 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -34,7 +34,7 @@ class ExtensibleArray<T> {
     (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M])

   }

 

-  method Init()

+  constructor Init()

     modifies this;

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

     ensures Contents == [];

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 3eb32da8..d052c463 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -2,3 +2,7 @@
 -------------------- SnapshotableTrees.dfy --------------------

 

 Dafny program verifier finished with 37 verified, 0 errors

+

+-------------------- TreeBarrier.dfy --------------------

+

+Dafny program verifier finished with 8 verified, 0 errors

diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy
index 0c31d8f3..3386b123 100644
--- a/Test/dafny2/SnapshotableTrees.dfy
+++ b/Test/dafny2/SnapshotableTrees.dfy
@@ -147,7 +147,7 @@ class Tree
   }

 

   method CreateIterator() returns (iter: Iterator)

-    requires Valid() && IsReadonly;

+    requires Valid(); // && IsReadonly;

     ensures iter != null && iter.Valid() && fresh(iter.IterRepr);

     ensures iter.T == this && iter.Contents == Contents && iter.N == -1;

   {

@@ -459,3 +459,21 @@ class Iterator
 }

 

 datatype List = Nil | Cons(Node, List);

+

+/*  The following method shows the problem of concurrent modifications and shows that the

+ *  design of the snapshotable trees herein handle this correctly.  That is, after inserting

+ *  into a tree that is being iterated, use of the associated iterator can no longer be

+ *  proved to be correct.

+ *

+method TestConcurrentModification(t: Tree)

+  requires t != null && t.Valid() && !t.IsReadonly;

+  modifies t.MutableRepr;

+{

+  var it := t.CreateIterator();

+  var more := it.MoveNext();

+  if (more) {

+    var pos := t.Insert(52);  // this modification of the collection renders all associated iterators invalid

+    more := it.MoveNext();  // error: operation t.Insert may have made this iterator invalid

+  }

+}

+*/

diff --git a/Test/dafny2/TreeBarrier.dfy b/Test/dafny2/TreeBarrier.dfy
new file mode 100644
index 00000000..f4cc25d2
--- /dev/null
+++ b/Test/dafny2/TreeBarrier.dfy
@@ -0,0 +1,143 @@
+class Node {

+  var left: Node;

+  var right: Node;

+  var parent: Node;

+  var anc: set<Node>;

+  var desc: set<Node>;

+  var sense: bool;

+  var pc: int;

+

+

+  function validDown(): bool

+    reads this, desc;    

+  {

+    this !in desc &&

+    null !in desc &&

+    left != right &&  // not needed, but speeds up verification

+

+    (right != null ==> right in desc && left !in right.desc) &&

+

+    (left != null ==> 

+      left in desc && 

+      (right != null ==> desc == {left,right} + left.desc + right.desc)  &&

+      (right == null ==> desc == {left} + left.desc)  &&

+      left.validDown()) &&

+    (left == null ==> 

+      (right != null ==> desc == {right} + right.desc)  &&

+      (right == null ==> desc == {})) &&

+

+    (right != null ==> right.validDown()) &&

+

+    (blocked() ==> forall m :: m in desc ==> m.blocked()) &&

+    (after() ==> forall m :: m in desc ==> m.blocked() || m.after())

+//    (left != null && right != null ==> left.desc !! right.desc)  // not needed

+  }

+

+

+

+

+  function  validUp(): bool

+    reads this, anc;    

+  {

+    this !in anc &&

+    null !in anc &&

+    (parent != null ==> parent in anc && anc == { parent } + parent.anc && parent.validUp()) &&

+    (parent == null ==> anc == {}) &&

+    (after() ==> forall m :: m in anc ==> m.after())

+  }

+

+  function valid(): bool

+    reads this, desc, anc;

+  { validUp() && validDown() && desc !! anc }

+

+  function before(): bool

+    reads this;

+  { !sense && pc <= 2 }

+

+  function blocked(): bool

+    reads this;

+  { sense }

+

+  function after(): bool

+    reads this;

+  { !sense && 3 <= pc }

+

+

+  method barrier()

+    requires valid();

+    requires before();

+    modifies this, left, right;

+  {

+

+//A

+    pc := 1;

+    if(left != null) {

+      while(!left.sense) 

+        modifies left;

+        invariant validDown(); // this seems necessary to get the necessary unfolding of functions

+        invariant valid();

+        decreases *;  // to by-pass termination checking for this loop

+      {

+        // this loop body is supposed to model what the "left" thread

+        // might do to its node. This body models a transition from

+        // "before" to "blocked" by setting sense to true. A transition

+        // all the way to "after" is not permitted; this would require

+        // a change of pc.

+        // We assume that "left" preserves the validity of its subtree,

+        // which means in particular that it goes to "blocked" only if

+        // all its descendants are already blocked.

+        left.sense := *; 

+        assume left.blocked() ==> forall m :: m in left.desc ==> m.blocked();

+      }  

+    }

+    if(right != null) {

+      while(!right.sense) 

+        modifies right;

+        invariant validDown(); // this seems necessary to get the necessary unfolding of functions

+        invariant valid();

+        decreases *;  // to by-pass termination checking for this loop

+      {

+        // analogous to the previous loop

+        right.sense := *; 

+        assume right.blocked() ==> forall m :: m in right.desc ==> m.blocked();

+      }  

+    }

+

+//B

+    pc := 2;

+    if(parent != null) {

+      sense := true; 

+    }

+//C

+    pc := 3;

+    while(sense)

+        modifies this;

+        invariant validUp(); // this seems necessary to get the necessary unfolding of functions

+        invariant valid();

+        invariant left == old(left);

+        invariant right == old(right);

+        invariant sense ==> parent != null;

+        decreases *;  // to by-pass termination checking for this loop

+    {

+      // this loop body is supposed to model what the "parent" thread

+      // might do to its node. The body models a transition from

+      // "blocked" to "after" by setting sense to false.

+      // We assume that "parent" initiates this transition only

+      // after it went to state "after" itself.

+      sense := *;

+      assume !sense ==> parent.after();

+    }

+//D

+    pc := 4;

+    if(left != null) {

+      left.sense := false;

+    }

+//E

+    pc := 5;

+    if(right != null) {

+      right.sense := false;

+    }

+//F

+    pc := 6;

+  }

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index a58b03c6..62b0b6fe 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

-for %%f in (SnapshotableTrees.dfy) do (

+for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy) do (

   echo.

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