Dafny: for refinements, don't consider a newly provided predicate body to be an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be

7 files changed, 78 insertions, 59 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index b1b8828a..4b588289 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -452,7 +452,6 @@ namespace Microsoft.Dafny
     }

 

     public Function CloneFunction(Function f) {

-

       var tps = f.TypeArgs.ConvertAll(CloneTypeParam);

       var formals = f.Formals.ConvertAll(CloneFormal);

       var req = f.Req.ConvertAll(CloneExpr);

@@ -463,7 +462,7 @@ namespace Microsoft.Dafny
 

       if (f is Predicate) {

         return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals,

-          req, reads, ens, decreases, body, false, null, false);

+          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, null, false);

       } else if (f is CoPredicate) {

         return new CoPredicate(Tok(f.tok), f.Name, f.IsStatic, tps, f.OpenParen, formals,

           req, reads, ens, body, null, false);

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index c558dd14..a4d0eba1 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -660,7 +660,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   ]

   (. if (isPredicate) {

         f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

-                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);

+                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);

      } else if (isCoPredicate) {

         f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,

                           reqs, reads, ens, body, attrs, signatureOmitted);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 021a0ba7..46c15cf9 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1558,14 +1558,20 @@ namespace Microsoft.Dafny {
 

   public class Predicate : Function

   {

-    public readonly bool BodyIsExtended;  // says that this predicate definition is a refinement extension of a predicate definition is a refining module

+    public enum BodyOriginKind

+    {

+      OriginalOrInherited,  // this predicate definition is new (and the predicate may or may not have a body), or the predicate's body (whether or not it exists) is being inherited unmodified (from the previous refinement--it may be that the inherited body was itself an extension, for example)

+      DelayedDefinition,  // this predicate declaration provides, for the first time, a body--the declaration refines a previously declared predicate, but the previous one had no body

+      Extension  // this predicate extends the definition of a predicate with a body in a module being refined

+    }

+    public readonly BodyOriginKind BodyOrigin;

     public Predicate(IToken tok, string name, bool isStatic, bool isGhost,

                      List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,

                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

-                     Expression body, bool bodyIsExtended, Attributes attributes, bool signatureOmitted)

+                     Expression body, BodyOriginKind bodyOrigin, Attributes attributes, bool signatureOmitted)

       : base(tok, name, isStatic, isGhost, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureOmitted) {

-      Contract.Requires(!bodyIsExtended || body != null);

-      BodyIsExtended = bodyIsExtended;

+      Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);

+      BodyOrigin = bodyOrigin;

     }

   }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 46e17f7e..bd5ba6dc 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -633,7 +633,7 @@ bool IsAttribute() {
 		}

 		if (isPredicate) {

 		  f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

-		                    reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);

+		                    reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);

 		} else if (isCoPredicate) {

 		  f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,

 		                    reqs, reads, ens, body, attrs, signatureOmitted);

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index e0f12246..28387f16 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -473,21 +473,26 @@ namespace Microsoft.Dafny
       }

 

       Expression body;

+      Predicate.BodyOriginKind bodyOrigin;

       if (replacementBody != null) {

         body = replacementBody;

+        bodyOrigin = Predicate.BodyOriginKind.DelayedDefinition;

       } else if (moreBody != null) {

         if (f.Body == null) {

           body = moreBody;

+          bodyOrigin = Predicate.BodyOriginKind.DelayedDefinition;

         } else {

           body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, refinementCloner.CloneExpr(f.Body), moreBody);

+          bodyOrigin = Predicate.BodyOriginKind.Extension;

         }

       } else {

         body = refinementCloner.CloneExpr(f.Body);

+        bodyOrigin = Predicate.BodyOriginKind.OriginalOrInherited;

       }

 

       if (f is Predicate) {

         return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

-          req, reads, ens, decreases, body, moreBody != null, null, false);

+          req, reads, ens, decreases, body, bodyOrigin, null, false);

       } else if (f is CoPredicate) {

         return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,

           req, reads, ens, body, null, false);

@@ -592,10 +597,10 @@ namespace Microsoft.Dafny
 

               Expression moreBody = null;

               Expression replacementBody = null;

-              if (isPredicate) {

-                moreBody = f.Body;

-              } else if (prevFunction.Body == null) {

+              if (prevFunction.Body == null) {

                 replacementBody = f.Body;

+              } else if (isPredicate) {

+                moreBody = f.Body;

               } else if (f.Body != null) {

                 reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");

               }

@@ -1263,7 +1268,7 @@ namespace Microsoft.Dafny
         var e = (FunctionCallExpr)expr;

         if (e.Function.EnclosingClass.Module == m) {

           var p = e.Function as Predicate;

-          if (p != null && p.BodyIsExtended) {

+          if (p != null && p.BodyOrigin == Predicate.BodyOriginKind.Extension) {

             return true;

           }

         }

@@ -1283,7 +1288,7 @@ namespace Microsoft.Dafny
     public RefinementCloner(ModuleDefinition m) {

       moduleUnderConstruction = m;

     }

-    override public IToken Tok(IToken tok) {

+    public override IToken Tok(IToken tok) {

       return new RefinementToken(tok, moduleUnderConstruction);

     }

   }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5879995a..363eb4e0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -705,7 +705,7 @@ namespace Microsoft.Dafny
 

       if (f is Predicate) {

         return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

-          req, reads, ens, decreases, body, false, null, false);

+          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, null, false);

       } else if (f is CoPredicate) {

         return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,

           req, reads, ens, body, null, false);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c8cc11f6..5ce0e1a1 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7456,51 +7456,58 @@ namespace Microsoft.Dafny {
 

           if (module == currentModule && functionHeight < heightLimit) {

             if (f.Body != null && !(f.Body.Resolved is MatchExpr)) {

-              // inline this body

-              Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

-              Contract.Assert(fexp.Args.Count == f.Formals.Count);

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

-                Formal p = f.Formals[i];

-                Expression arg = fexp.Args[i];

-                arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);

-                arg.Type = p.Type;  // resolve here

-                substMap.Add(p, arg);

-              }

-              Expression body = Substitute(f.Body, fexp.Receiver, substMap);

-

-              // Produce, for a "body" split into b0, b1, b2:

-              //     free F#canCall(args) && F(args) && (b0 && b1 && b2)

-              //     checked F#canCall(args) ==> F(args) || b0

-              //     checked F#canCall(args) ==> F(args) || b1

-              //     checked F#canCall(args) ==> F(args) || b2

-              // Note that "body" does not contain limited calls.

-

-              // F#canCall(args)

-              Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);

-              ExprSeq args = etran.FunctionInvocationArguments(fexp);

-              Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

-

-              // F(args)

-              Bpl.Expr fargs = etran.TrExpr(fexp);

-

-              // body

-              Bpl.Expr trBody = etran.TrExpr(body);

-              trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);

-

-              // here goes the free piece:

-              splits.Add(new SplitExprInfo(true, Bpl.Expr.Binary(trBody.tok, BinaryOperator.Opcode.And, canCall, BplAnd(fargs, trBody))));

-

-              // recurse on body

-              var ss = new List<SplitExprInfo>();

-              TrSplitExpr(body, ss, position, functionHeight, etran);

-              foreach (var s in ss) {

-                var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);

-                var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);

-                var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

-                splits.Add(new SplitExprInfo(s.IsFree, p));

-              }

+              if (RefinementToken.IsInherited(fexp.tok, currentModule) &&

+                  f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition &&

+                  (currentMethod == null || !currentMethod.MustReverify)) {

+                // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything

+                // that needed to be proved about the function was proved already in the previous module, even without the body definition).

+              } else {

+                // inline this body

+                Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

+                Contract.Assert(fexp.Args.Count == f.Formals.Count);

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

+                  Formal p = f.Formals[i];

+                  Expression arg = fexp.Args[i];

+                  arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);

+                  arg.Type = p.Type;  // resolve here

+                  substMap.Add(p, arg);

+                }

+                Expression body = Substitute(f.Body, fexp.Receiver, substMap);

+

+                // Produce, for a "body" split into b0, b1, b2:

+                //     free F#canCall(args) && F(args) && (b0 && b1 && b2)

+                //     checked F#canCall(args) ==> F(args) || b0

+                //     checked F#canCall(args) ==> F(args) || b1

+                //     checked F#canCall(args) ==> F(args) || b2

+                // Note that "body" does not contain limited calls.

+

+                // F#canCall(args)

+                Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);

+                ExprSeq args = etran.FunctionInvocationArguments(fexp);

+                Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

+

+                // F(args)

+                Bpl.Expr fargs = etran.TrExpr(fexp);

+

+                // body

+                Bpl.Expr trBody = etran.TrExpr(body);

+                trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);

+

+                // here goes the free piece:

+                splits.Add(new SplitExprInfo(true, Bpl.Expr.Binary(trBody.tok, BinaryOperator.Opcode.And, canCall, BplAnd(fargs, trBody))));

+

+                // recurse on body

+                var ss = new List<SplitExprInfo>();

+                TrSplitExpr(body, ss, position, functionHeight, etran);

+                foreach (var s in ss) {

+                  var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);

+                  var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);

+                  var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

+                  splits.Add(new SplitExprInfo(s.IsFree, p));

+                }

 

-              return true;

+                return true;

+              }

             }

           }

         }

@@ -7600,6 +7607,8 @@ namespace Microsoft.Dafny {
         translatedExpression = etran.TrExpr(expr);

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

       }

+      // TODO: Is the the following call to ContainsChange expensive?  It's linear in the size of "expr", but we get here many times in TrSpliExpr, so wouldn't the total

+      // time in the size of the expression passed to the first TrSpliExpr be quadratic?

       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