Dafny: reverify if the refining method modifies the heap.

3 files changed, 17 insertions, 12 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0dcbcf11..8ea17a52 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1545,6 +1545,7 @@ namespace Microsoft.Dafny {
   public class Method : MemberDecl, TypeParameter.ParentType

   {

     public readonly bool SignatureIsOmitted;

+    public bool MustReverify;

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly List<Formal/*!*/>/*!*/ Ins;

     public readonly List<Formal/*!*/>/*!*/ Outs;

@@ -1593,6 +1594,7 @@ namespace Microsoft.Dafny {
       this.Decreases = decreases;

       this.Body = body;

       this.SignatureIsOmitted = signatureOmitted;

+      MustReverify = false;

     }

   }

 

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index c2fc57c5..3ba26dbf 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -66,6 +66,7 @@ namespace Microsoft.Dafny
     private ModuleDefinition moduleUnderConstruction;  // non-null for the duration of Construct calls

     private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction

     public Queue<Tuple<Method, Method>> translationMethodChecks = new Queue<Tuple<Method, Method>>();  // contains all the methods that need to be checked for structural refinement.

+    private Method currentMethod;

 

     public void PreResolve(ModuleDefinition m) {

 

@@ -634,7 +635,7 @@ namespace Microsoft.Dafny
                 CheckAgreement_Parameters(m.tok, prevMethod.Ins, m.Ins, m.Name, "method", "in-parameter");

                 CheckAgreement_Parameters(m.tok, prevMethod.Outs, m.Outs, m.Name, "method", "out-parameter");

               }

-

+              currentMethod = m;

               var replacementBody = m.Body;

               if (replacementBody != null) {

                 if (prevMethod.Body == null) {

@@ -1201,7 +1202,8 @@ namespace Microsoft.Dafny
       } else if (s is ConcreteUpdateStatement) {

         postTasks.Enqueue(() =>

         {

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

+          if (!CheckIsOkayUpdateStmt((ConcreteUpdateStatement)s, moduleUnderConstruction))

+            currentMethod.MustReverify = true;

         });

       } else if (s is CallStmt) {

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

@@ -1223,7 +1225,7 @@ 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) {

+    private bool CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m) {

       foreach (var lhs in stmt.Lhss) {

         var l = lhs.Resolved;

         if (l is IdentifierExpr) {

@@ -1231,24 +1233,25 @@ namespace Microsoft.Dafny
           Contract.Assert(ident.Var is VarDecl || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals)

           if ((ident.Var is VarDecl && RefinementToken.IsInherited(((VarDecl)ident.Var).Tok, m)) || ident.Var is Formal) {

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

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

+            return false;

           }

         } else if (l is FieldSelectExpr) {

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

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

+            return false;

           }

         } else {

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

+          return false;

         }

       }

       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");

+            return false;

           }

         }

       }

+      return true;

     }

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

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a8541293..2e322029 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3595,7 +3595,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(errorMessage != null);

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

 

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

+      if (RefinementToken.IsInherited(refinesToken, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition);

       } else {

@@ -3614,7 +3614,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(condition != null);

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

 

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

+      if (RefinementToken.IsInherited(refinesTok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         // produce a "skip" instead

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

       } else {

@@ -3634,7 +3634,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(condition != null);

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

 

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

+      if (RefinementToken.IsInherited(tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition, kv);

       } else {

@@ -4762,7 +4762,7 @@ namespace Microsoft.Dafny {
 

       // Make the call

       string name;

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

+      if (RefinementToken.IsInherited(method.tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify)) {

         name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName);

       } else {

         name = method.FullCompileName;

@@ -7479,7 +7479,7 @@ namespace Microsoft.Dafny {
         translatedExpression = etran.TrExpr(expr);

         splitHappened = etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

       }

-      if (RefinementToken.IsInherited(expr.tok, currentModule) && RefinementTransformer.ContainsChange(expr, currentModule)) {

+      if (RefinementToken.IsInherited(expr.tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule)) {

         // If "expr" contains a subexpression that has changed from the inherited expression, we'll destructively

         // change the token of the translated expression to make it look like it's not inherited.  This will cause "e" to

         // be verified again in the refining module.