Added side-effects and control-flow checks in hints.

3 files changed, 180 insertions, 18 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 716b3f51..bc8b6c27 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3880,9 +3880,19 @@ namespace Microsoft.Dafny
             }

             e0 = e1;

           }

+                  

+          // clear the labels for the duration of checking the hints, because break statements are not allowed to leave a parallel statement

+          var prevLblStmts = labeledStatements;

+          var prevLoopStack = loopStack;

+          labeledStatements = new Scope<Statement>();

+          loopStack = new List<Statement>();

           foreach (var h in s.Hints) {

             ResolveStatement(h, true, codeContext);

+            CheckHintRestrictions(h);

           }

+          labeledStatements = prevLblStmts;

+          loopStack = prevLoopStack;          

+

           if (prevErrorCount == ErrorCount && s.Steps.Count > 0) {

             // do not build Result if there were errors, as it might be ill-typed and produce unnecessary resolution errors

             s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());

@@ -4518,6 +4528,124 @@ namespace Microsoft.Dafny
       }

     }

 

+    /// <summary>

+    /// Check that a statment is a valid hint for a calculation.

+    /// ToDo: generalize the part for compound statements to take a delegate?

+    /// </summary>

+    public void CheckHintRestrictions(Statement stmt) {

+      Contract.Requires(stmt != null);

+      if (stmt is PredicateStmt) {

+        // cool

+      } else if (stmt is PrintStmt) {

+        // not allowed in ghost context

+      } else if (stmt is BreakStmt) {

+        // already checked while resolving hints

+      } else if (stmt is ReturnStmt) {

+        Error(stmt, "return statement is not allowed inside a hint");

+      } else if (stmt is YieldStmt) {

+        Error(stmt, "yield statement is not allowed inside a hint");

+      } else if (stmt is AssignSuchThatStmt) {

+        var s = (AssignSuchThatStmt)stmt;

+        foreach (var lhs in s.Lhss) {

+          CheckHintLhs(s.Tok, lhs.Resolved);

+        }

+      } else if (stmt is AssignStmt) {

+        var s = (AssignStmt)stmt;

+        CheckHintLhs(s.Tok, s.Lhs.Resolved);

+      } else if (stmt is VarDecl) {

+        // cool

+      } else if (stmt is CallStmt) {

+        var s = (CallStmt)stmt;

+        if (s.Method.Mod.Expressions.Count != 0) {

+          Error(stmt, "calls to methods with side-effects are not allowed inside a hint");

+        }

+      } else if (stmt is ConcreteSyntaxStatement) {

+        var s = (ConcreteSyntaxStatement)stmt;

+        foreach (var ss in s.ResolvedStatements) {

+          CheckHintRestrictions(ss);

+        }

+      } else if (stmt is BlockStmt) {

+        var s = (BlockStmt)stmt;

+        scope.PushMarker();

+        foreach (var ss in s.Body) {

+          CheckHintRestrictions(ss);

+        }

+        scope.PopMarker();

+

+      } else if (stmt is IfStmt) {

+        var s = (IfStmt)stmt;

+        CheckHintRestrictions(s.Thn);

+        if (s.Els != null) {

+          CheckHintRestrictions(s.Els);

+        }

+

+      } else if (stmt is AlternativeStmt) {

+        var s = (AlternativeStmt)stmt;

+        foreach (var alt in s.Alternatives) {

+          foreach (var ss in alt.Body) {

+            CheckHintRestrictions(ss);

+          }

+        }

+

+      } else if (stmt is WhileStmt) {

+        WhileStmt s = (WhileStmt)stmt;

+        CheckHintRestrictions(s.Body);

+

+      } else if (stmt is AlternativeLoopStmt) {

+        var s = (AlternativeLoopStmt)stmt;

+        foreach (var alt in s.Alternatives) {

+          foreach (var ss in alt.Body) {

+            CheckHintRestrictions(ss);

+          }

+        }

+

+      } else if (stmt is ParallelStmt) {

+        var s = (ParallelStmt)stmt;

+        switch (s.Kind) {

+          case ParallelStmt.ParBodyKind.Assign:

+            Error(stmt, "a parallel statement with heap updates is not allowed inside a hint");

+            break;

+          case ParallelStmt.ParBodyKind.Call:

+          case ParallelStmt.ParBodyKind.Proof:

+            // these are fine, since they don't update any non-local state

+            break;

+          default:

+            Contract.Assert(false);  // unexpected kind

+            break;

+        }

+		

+      } else if (stmt is CalcStmt) {

+        var s = (CalcStmt)stmt;

+        foreach (var h in s.Hints) {

+          CheckHintRestrictions(h);

+        }

+

+      } else if (stmt is MatchStmt) {

+        var s = (MatchStmt)stmt;

+        foreach (var kase in s.Cases) {

+          foreach (var ss in kase.Body) {

+            CheckHintRestrictions(ss);

+          }

+        }

+

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();

+      }

+    }

+

+    void CheckHintLhs(IToken tok, Expression lhs) {

+      var idExpr = lhs as IdentifierExpr;

+      if (idExpr != null) {

+        if (scope.ContainsDecl(idExpr.Var)) {

+          Error(tok, "a hint is not allowed to update a variable declared outside the hint");

+        }

+      } else {

+        Error(tok, "a hint is not allowed to update heap locations");

+      }

+    }

+

+

+

     Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) {

       Contract.Requires(rr != null);

       Contract.Requires(stmt != null);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 72ae7ad4..6e775b43 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -505,12 +505,12 @@ Execution trace:
 Dafny program verifier finished with 8 verified, 4 errors

 

 -------------------- ResolutionErrors.dfy --------------------

-ResolutionErrors.dfy(466,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

-ResolutionErrors.dfy(471,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

-ResolutionErrors.dfy(485,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

-ResolutionErrors.dfy(497,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

-ResolutionErrors.dfy(532,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly

-ResolutionErrors.dfy(396,2): Error: More than one default constructor

+ResolutionErrors.dfy(497,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

+ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

+ResolutionErrors.dfy(516,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

+ResolutionErrors.dfy(528,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

+ResolutionErrors.dfy(563,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly

+ResolutionErrors.dfy(427,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

@@ -528,10 +528,10 @@ ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowe
 ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

 ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

 ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)

-ResolutionErrors.dfy(402,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

-ResolutionErrors.dfy(407,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(408,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(410,9): Error: class Lamb does not have a default constructor

+ResolutionErrors.dfy(433,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

+ResolutionErrors.dfy(438,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(439,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(441,9): Error: class Lamb does not have a default constructor

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)

@@ -572,14 +572,17 @@ ResolutionErrors.dfy(372,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(377,10): Error: first argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(382,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ResolutionErrors.dfy(434,7): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(440,12): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(508,7): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(510,7): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(510,20): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(512,7): Error: let-such-that expressions are allowed only in ghost contexts

-ResolutionErrors.dfy(513,18): Error: unresolved identifier: w

-74 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(404,6): Error: calls to methods with side-effects are not allowed inside a hint

+ResolutionErrors.dfy(406,12): Error: a hint is not allowed to update heap locations

+ResolutionErrors.dfy(408,8): Error: a hint is not allowed to update a variable declared outside the hint

+ResolutionErrors.dfy(465,7): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(471,12): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(539,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

+77 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 6c86e7a8..5ad6d1fe 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -384,6 +384,37 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
   }

 }

 

+/* Side-effect checks */

+ghost var ycalc: int;

+

+ghost method Mod(a: int)

+  modifies this;

+  ensures ycalc == a;

+{

+  ycalc := a;

+}  

+  

+ghost method Bad()

+  modifies this;

+  ensures 0 == 1;

+{

+  var x: int;

+  calc {

+    0;

+    { Mod(0); }     // methods with side-effects are not allowed

+    ycalc;

+    { ycalc := 1; } // heap updates are not allowed

+    1;

+    { x := 1; }     // updates to locals defined outside of the hint are not allowed

+    x;

+    {

+      var x: int;

+      x := 1;       // this is OK

+    }

+    1;

+  }

+}

+

 // ------------------- nameless constructors ------------------------------

 

 class YHWH {