Dafny: Fixed bug in call statements where mutability of out parameters was not checked.

Added regression test.

4 files changed, 61 insertions, 20 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 780e04d9..197a603e 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1806,7 +1806,7 @@ namespace Microsoft.Dafny {
 

     /// <summary>

     /// Resolves the given call statement.

-    /// Assumes all LHSs have already been resolved.

+    /// Assumes all LHSs have already been resolved (and checked for mutability).

     /// </summary>

     void ResolveCallStmt(CallStmt s, bool specContextOnly, Method method, Type receiverType) {

       Contract.Requires(s != null);

@@ -1906,27 +1906,41 @@ namespace Microsoft.Dafny {
           var lhs = s.Lhs[i];

           if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {

             Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);

-          } else if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {

-            // LHS must denote a ghost

-            lhs = lhs.Resolved;

-            if (lhs is IdentifierExpr) {

-              var ll = (IdentifierExpr)lhs;

-              if (!ll.Var.IsGhost) {

-                if (ll is AutoGhostIdentifierExpr && ll.Var is VarDecl) {

-                  // the variable was actually declared in this statement, so auto-declare it as ghost

-                  ((VarDecl)ll.Var).MakeGhost();

-                } else {

-                  Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

+          } else {

+            var resolvedLhs = lhs.Resolved;

+            if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {

+              // LHS must denote a ghost

+              if (resolvedLhs is IdentifierExpr) {

+                var ll = (IdentifierExpr)resolvedLhs;

+                if (!ll.Var.IsGhost) {

+                  if (ll is AutoGhostIdentifierExpr && ll.Var is VarDecl) {

+                    // the variable was actually declared in this statement, so auto-declare it as ghost

+                    ((VarDecl)ll.Var).MakeGhost();

+                  } else {

+                    Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

+                  }

                 }

+              } else if (resolvedLhs is FieldSelectExpr) {

+                var ll = (FieldSelectExpr)resolvedLhs;

+                if (!ll.Field.IsGhost) {

+                  Error(s, "actual out-parameter {0} is required to be a ghost field", i);

+                }

+              } else {

+                // this is an array update, and arrays are always non-ghost

+                Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

               }

-            } else if (lhs is FieldSelectExpr) {

-              var ll = (FieldSelectExpr)lhs;

-              if (!ll.Field.IsGhost) {

-                Error(s, "actual out-parameter {0} is required to be a ghost field", i);

+            }

+            // LHS must denote a mutable field.

+            if (resolvedLhs is IdentifierExpr) {

+              var ll = (IdentifierExpr)resolvedLhs;

+              if (!ll.Var.IsMutable) {

+                Error(resolvedLhs, "LHS of assignment must denote a mutable variable");

+              }

+            } else if (resolvedLhs is FieldSelectExpr) {

+              var ll = (FieldSelectExpr)resolvedLhs;

+              if (!ll.Field.IsMutable) {

+                Error(resolvedLhs, "LHS of assignment must denote a mutable field");

               }

-            } else {

-              // this is an array update, and arrays are always non-ghost

-              Error(s, "actual out-parameter {0} is required to be a ghost variable", i);

             }

           }

         }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e5621773..a29c64fa 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1103,3 +1103,8 @@ Dafny program verifier finished with 16 verified, 0 errors
 -------------------- ChainingDisjointTests.dfy --------------------

 

 Dafny program verifier finished with 6 verified, 0 errors

+

+-------------------- CallStmtTests.dfy --------------------

+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable

+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable

+2 resolution/type errors detected in CallStmtTests.dfy

diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy
new file mode 100644
index 00000000..735efe81
--- /dev/null
+++ b/Test/dafny0/CallStmtTests.dfy
@@ -0,0 +1,21 @@
+

+method testing1(t: int)

+{

+   t := m(); // error: should be checked at the Dafny level, not fall to Boogie.

+}

+

+method m() returns (r: int)

+{

+   return 3;

+}

+

+method testing2()

+{

+   var v;

+   v := m2(); // error: v needs to be ghost because r is.

+}

+

+method m2() returns (ghost r: int)

+{

+   r := 23;

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 143a0dc5..7aa1b38e 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -19,7 +19,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Termination.dfy DTypes.dfy

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

             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy

-            ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy) do (

+            ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

+            CallStmtTests.dfy) do (

   echo.

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

   %DAFNY_EXE% /compile:0 %* %%f