Dafny: restored soundness for refinement by disallowing certain updates and method calls

3 files changed, 134 insertions, 25 deletions

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index a5fab242..09e17fe1 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -1134,10 +1134,11 @@ namespace Microsoft.Dafny {
            *   

            *   var x := E;                 var x;                       var x := E;

            *   var x := E;                 var x := *;                  var x := E;

-           *   var x := E1;                var x :| E0;                 var x := E1; assert E0;

+           *   var x := E1;                var x :| P;                  var x := E1; assert P;

            *   var VarProduction;                                       var VarProduction;

            *   

            *   x := E;                     x := *;                      x := E;

+           *   x := E;                     x :| P;                      x := E; assert P;

            *   

            *   if ... Then else Else       if (G) Then' else Else'      if (G) Merge(Then,Then') else Merge(Else,Else')

            *   if (G) Then else Else       if (*) Then' else Else'      if (G) Merge(Then,Then') else Merge(Else,Else')

@@ -1272,22 +1273,26 @@ namespace Microsoft.Dafny {
 

           } else if (cur is VarDeclStmt) {

             var cNew = (VarDeclStmt)cur;

-            var cOld = oldS as VarDeclStmt;

             bool doMerge = false;

             Expression addedAssert = null;

-            if (cOld != null && cNew.Lhss.Count == 1 && cOld.Lhss.Count == 1 && cNew.Lhss[0].Name == cOld.Lhss[0].Name) {

-              var update = cNew.Update as UpdateStmt;

-              if (update != null && update.Rhss.Count == 1 && update.Rhss[0] is ExprRhs) {

-                // Note, we allow switching between ghost and non-ghost, since that seems unproblematic.

-                if (cOld.Update == null) {

-                  doMerge = true;

-                } else if (cOld.Update is AssignSuchThatStmt) {

-                  doMerge = true;

-                  addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Expr);

-                } else {

-                  var updateOld = (UpdateStmt)cOld.Update;  // if cast fails, there are more ConcreteUpdateStatement subclasses than expected

-                  if (updateOld.Rhss.Count == 1 && updateOld.Rhss[0] is HavocRhs) {

+            if (oldS is VarDeclStmt) {

+              var cOld = (VarDeclStmt)oldS;

+              if (VarDeclAgree(cOld.Lhss, cNew.Lhss)) {

+                var update = cNew.Update as UpdateStmt;

+                if (update != null && update.Rhss.TrueForAll(rhs => !rhs.CanAffectPreviouslyKnownExpressions)) {

+                  // Note, we allow switching between ghost and non-ghost, since that seems unproblematic.

+                  if (cOld.Update == null) {

+                    doMerge = true;

+                  } else if (cOld.Update is AssignSuchThatStmt) {

+                    doMerge = true;

+                    addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Expr);

+                  } else {

+                    var updateOld = (UpdateStmt)cOld.Update;  // if cast fails, there are more ConcreteUpdateStatement subclasses than expected

                     doMerge = true;

+                    foreach (var rhs in updateOld.Rhss) {

+                      if (!(rhs is HavocRhs))

+                        doMerge = false;

+                    }

                   }

                 }

               }

@@ -1297,7 +1302,7 @@ namespace Microsoft.Dafny {
               body.Add(cNew);

               i++; j++;

               if (addedAssert != null) {

-                body.Add(new AssertStmt(addedAssert.tok, addedAssert, null));

+                body.Add(new AssertStmt(new Translator.ForceCheckToken(addedAssert.tok), addedAssert, null));

               }

             } else {

               MergeAddStatement(cur, body);

@@ -1330,6 +1335,38 @@ namespace Microsoft.Dafny {
               i++;

             }

 

+          } else if (cur is UpdateStmt) {

+            var nw = (UpdateStmt)cur;

+            List<Statement> stmtGenerated = new List<Statement>();

+            bool doMerge = false;

+            if (oldS is UpdateStmt) {

+              var s = (UpdateStmt)oldS;

+              if (LeftHandSidesAgree(s.Lhss, nw.Lhss)) {

+                doMerge = true;

+                stmtGenerated.Add(nw);

+                foreach(var rhs in s.Rhss) {

+                  if (!(rhs is HavocRhs))

+                    doMerge = false;

+                }

+              }

+            } else if (oldS is AssignSuchThatStmt) {

+              var s = (AssignSuchThatStmt)oldS;

+              if (LeftHandSidesAgree(s.Lhss, nw.Lhss)) {

+                doMerge = true;

+                stmtGenerated.Add(nw);

+                var addedAssert = CloneExpr(s.Expr);

+                stmtGenerated.Add(new AssertStmt(new Translator.ForceCheckToken(addedAssert.tok), addedAssert, null));

+              }

+            }

+            if (doMerge) {

+              // Go ahead with the merge:

+              Contract.Assert(cce.NonNullElements(stmtGenerated));

+              body.AddRange(stmtGenerated);

+              i++; j++;

+            } else {

+              MergeAddStatement(cur, body);

+              i++;

+            }

           } else if (cur is IfStmt) {

             var cNew = (IfStmt)cur;

             var cOld = oldS as IfStmt;

@@ -1367,6 +1404,30 @@ namespace Microsoft.Dafny {
       return new BlockStmt(skeleton.Tok, body);

     }

 

+    private bool LeftHandSidesAgree(List<Expression> old, List<Expression> nw) {

+      if (old.Count != nw.Count)

+        return false;

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

+        var a = old[i].Resolved as IdentifierExpr;

+        var b = nw[i] as IdentifierSequence;

+        if (a != null && b != null)

+          if (b.Tokens.Count == 1 && b.Arguments == null)

+            if (a.Name == b.Tokens[0].val)

+              continue;

+        return false;

+      }

+      return true;

+    }

+    private bool VarDeclAgree(List<VarDecl> old, List<VarDecl> nw) {

+      if (old.Count != nw.Count)

+        return false;

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

+        if (old[i].Name != nw[i].Name)

+          return false;

+      }

+      return true;

+    }

+

     bool PotentialMatch(Statement nxt, Statement other) {

       Contract.Requires(!(nxt is SkeletonStatement) || ((SkeletonStatement)nxt).S != null);  // nxt is not "...;"

       Contract.Requires(other != null);

@@ -1391,6 +1452,9 @@ namespace Microsoft.Dafny {
       } else if (nxt is WhileStmt) {

         var oth = other as WhileStmt;

         return oth != null && oth.Guard == null;

+      } else if (nxt is VarDeclStmt) {

+        var oth = other as VarDeclStmt;

+        return oth != null && VarDeclAgree(((VarDeclStmt)nxt).Lhss, oth.Lhss);

       }

 

       // not a potential match

@@ -1474,7 +1538,6 @@ namespace Microsoft.Dafny {
       for (LList<Label> n = s.Labels; n != null; n = n.Next) {

         labels.Push(n.Data.Name);

       }

-

       if (s is SkeletonStatement) {

         reporter.Error(s, "skeleton statement may not be used here; it does not have a matching statement in what is being replaced");

       } else if (s is ReturnStmt) {

@@ -1488,6 +1551,18 @@ namespace Microsoft.Dafny {
         // TODO: To be a refinement automatically (that is, without any further verification), only variables and fields defined

         // in this module are allowed.  This needs to be checked.  If the LHS refers to an l-value that was not declared within

         // this module, then either an error should be reported or the Translator needs to know to translate new proof obligations.

+        var a = (AssignStmt)s;

+        reporter.Error(a.Tok, "cannot have assignment statement");

+      } else if (s is ConcreteUpdateStatement) {

+        postTasks.Enqueue(() =>

+        {

+          CheckIsOkayUpdateStmt((ConcreteUpdateStatement)s, moduleUnderConstruction, reporter);

+        });

+      } else if (s is CallStmt) {

+        reporter.Error(s.Tok, "cannot have call statement");

+      } else if (s is ParallelStmt) {

+        if (((ParallelStmt)s).Kind == ParallelStmt.ParBodyKind.Assign) // allow Proof and Call (as neither touch any existing state)

+          reporter.Error(s.Tok, "cannot have parallel statement");

       } else {

         if (s is WhileStmt || s is AlternativeLoopStmt) {

           loopLevels++;

@@ -1502,6 +1577,32 @@ namespace Microsoft.Dafny {
       }

     }

 

+    // Checks that statement stmt, defined in the constructed module m, is a refinement of skip in the parent module

+    private void CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m, ResolutionErrorReporter reporter) {

+      foreach (var lhs in stmt.Lhss) {

+        var l = lhs.Resolved;

+        if (l is IdentifierExpr) {

+          if (RefinementToken.IsInherited(l.tok, m) || ((IdentifierExpr)l).Var is Formal) {

+            // for some reason, formals are not considered to be inherited.

+            reporter.Error(l.tok, "cannot assign to variable defined previously");

+          }

+        } else if (l is FieldSelectExpr) {

+          if (RefinementToken.IsInherited(((FieldSelectExpr)l).Field.tok, m)) {

+            reporter.Error(l.tok, "cannot assign to field defined previously");

+          }

+        } else {

+          reporter.Error(lhs.tok, "cannot assign to something which could exist in the previous refinement");

+        }

+      }

+      if (stmt is UpdateStmt) {

+        var s = (UpdateStmt)stmt;

+        foreach (var rhs in s.Rhss) {

+          if (s.Rhss[0].CanAffectPreviouslyKnownExpressions) {

+            reporter.Error(s.Rhss[0].Tok, "cannot have method call which can affect the heap");

+          }

+        }

+      }

+    }

     // ---------------------- additional methods -----------------------------------------------------------------------------

 

     public static bool ContainsChange(Expression expr, ModuleDefinition m) {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index bff09734..7839c5ad 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3303,14 +3303,17 @@ namespace Microsoft.Dafny {
       }

     }

 

-    Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)

-    {

+    Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage) {

+      return Assert(tok, condition, errorMessage, tok);

+    }

+

+    Bpl.PredicateCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesToken) {

       Contract.Requires(tok != null);

       Contract.Requires(condition != null);

       Contract.Requires(errorMessage != null);

       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

 

-      if (RefinementToken.IsInherited(tok, currentModule)) {

+      if (RefinementToken.IsInherited(refinesToken, currentModule)) {

         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition);

       } else {

@@ -3319,15 +3322,17 @@ namespace Microsoft.Dafny {
         return cmd;

       }

     }

-

-    Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)

+    Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage) {

+      return AssertNS(tok, condition, errorMessage, tok);

+    }

+    Bpl.PredicateCmd AssertNS(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.IToken refinesTok)

     {

       Contract.Requires(tok != null);

       Contract.Requires(errorMessage != null);

       Contract.Requires(condition != null);

       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

 

-      if (RefinementToken.IsInherited(tok, currentModule)) {

+      if (RefinementToken.IsInherited(refinesTok, currentModule)) {

         // produce a "skip" instead

         return new Bpl.AssumeCmd(tok, Bpl.Expr.True);

       } else {

@@ -3425,12 +3430,12 @@ namespace Microsoft.Dafny {
           var ss = TrSplitExpr(s.Expr, etran, out splitHappened);

           if (!splitHappened) {

             var tok = enclosingToken == null ? s.Expr.tok : new NestedToken(enclosingToken, s.Expr.tok);

-            builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation"));

+            builder.Add(Assert(tok, etran.TrExpr(s.Expr), "assertion violation", stmt.Tok));

           } else {

             foreach (var split in ss) {

               if (!split.IsFree) {

                 var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.E.tok);

-                builder.Add(AssertNS(tok, split.E, "assertion violation"));

+                builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok));

               }

             }

             builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 9ea7a3ff..dce9795b 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -51,6 +51,9 @@ module B refines A {
         i := i + 1;

       }

       var k := arr[i];

+      ...;

+      var a :| Contents == set x | x in a;

+      arr := a;

     }

   }

 }

@@ -60,7 +63,7 @@ module C refines B {
     method Retrieve...

     {

       ...;

-      arr := [thing] + arr[..i] + arr[i+1..];  // LRU behavior

+      var a := [thing] + arr[..i] + arr[i+1..];  // LRU behavior

     }

   }

 }