Merge

6 files changed, 61 insertions, 30 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index e136a3de..d3fad9e6 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -656,7 +656,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   | "constructor"                   (. if (allowConstructor) {

                                          isConstructor = true;

                                        } else {

-                                         SemErr(t, "constructors are only allowed in classes");

+                                         SemErr(t, "constructors are allowed only in classes");

                                        }

                                     .)

   )                                 (. keywordToken = t; .)

@@ -1424,13 +1424,13 @@ Invariant<out MaybeFreeExpression/*!*/ invariant>
 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

 = (. Expression/*!*/ e; .)

   PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {

-                                              SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+                                              SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

                                             } else {

                                               decreases.Add(e);

                                             }

                                          .)

   { "," PossiblyWildExpression<out e>    (. if (!allowWildcard && e is WildcardExpr) {

-                                              SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+                                              SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

                                             } else {

                                               decreases.Add(e);

                                             }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 005dbc44..35a70869 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1838,6 +1838,7 @@ namespace Microsoft.Dafny {
     ModuleDefinition EnclosingModule { get; }  // to be called only after signature-resolution is complete

     bool MustReverify { get; }

     string FullSanitizedName { get; }

+    bool AllowsNontermination { get; }

   }

   /// <summary>

   /// An ICallable is a Function, Method, or IteratorDecl.

@@ -1880,6 +1881,7 @@ namespace Microsoft.Dafny {
     ModuleDefinition ICodeContext.EnclosingModule { get { return Module; } }

     bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

     public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

+    public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

   }

 

   public class IteratorDecl : ClassDecl, IMethodCodeContext

@@ -1981,6 +1983,11 @@ namespace Microsoft.Dafny {
     }

     ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }

     bool ICodeContext.MustReverify { get { return false; } }

+    public bool AllowsNontermination {

+      get {

+        return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

+      }

+    }

   }

 

   public abstract class MemberDecl : Declaration {

@@ -2496,6 +2503,12 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public bool AllowsNontermination {

+      get {

+        return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

+      }

+    }

+

     /// <summary>

     /// The "AllCalls" field is used for non-CoPredicate, non-PrefixPredicate functions only (so its value should not be relied upon for CoPredicate and PrefixPredicate functions).

     /// It records all function calls made by the Function, including calls made in the body as well as in the specification.

@@ -2728,6 +2741,11 @@ namespace Microsoft.Dafny {
       }

     }

     bool ICodeContext.MustReverify { get { return this.MustReverify; } }

+    public bool AllowsNontermination {

+      get {

+        return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

+      }

+    }

   }

 

   public class Lemma : Method

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 3eff2f87..cfa18e56 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -991,7 +991,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			if (allowConstructor) {

 			 isConstructor = true;

 			} else {

-			 SemErr(t, "constructors are only allowed in classes");

+			 SemErr(t, "constructors are allowed only in classes");

 			}

 			

 		} else SynErr(151);

@@ -1546,7 +1546,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ e; 

 		PossiblyWildExpression(out e);

 		if (!allowWildcard && e is WildcardExpr) {

-		 SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+		 SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

 		} else {

 		 decreases.Add(e);

 		}

@@ -1555,7 +1555,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			PossiblyWildExpression(out e);

 			if (!allowWildcard && e is WildcardExpr) {

-			 SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");

+			 SemErr(e.tok, "'decreases *' is allowed only on loops and tail-recursive methods");

 			} else {

 			 decreases.Add(e);

 			}

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 88d3fd24..69dfb03d 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -749,14 +749,20 @@ namespace Microsoft.Dafny
               if (m.Mod.Expressions.Count != 0) {

                 reporter.Error(m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause");

               }

+              // If the previous method was not specified with "decreases *", then the new method is not allowed to provide any "decreases" clause.

+              // Any "decreases *" clause is not inherited, so if the previous method was specified with "decreases *", then the new method needs

+              // to either redeclare "decreases *", provided a termination-checking "decreases" clause, or give no "decreases" clause and thus

+              // get a default "decreases" loop.

               Specification<Expression> decreases;

-              if (Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) {

-                decreases = m.Decreases;

+              if (m.Decreases.Expressions.Count == 0) {

+                // inherited whatever the previous loop used

+                decreases = refinementCloner.CloneSpecExpr(prevMethod.Decreases);

               } else {

-                if (m.Decreases.Expressions.Count != 0) {

+                if (!Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) {

+                  // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause.

                   reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported, unless the refined method was specified with 'decreases *'");

                 }

-                decreases = refinementCloner.CloneSpecExpr(prevMethod.Decreases);

+                decreases = m.Decreases;

               }

               if (prevMethod.IsStatic != m.IsStatic) {

                 reporter.Error(m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name);

@@ -1407,18 +1413,16 @@ namespace Microsoft.Dafny
       // the Specification structures with a null list).

       Contract.Assume(cNew.Mod.Expressions == null);

 

-      // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause.

-      // Any "decreases *" clause is not inherited, so if the previous loop was specified with "decreases *", then the new loop needs

-      // to either redeclare "decreases *", provided a termination-checking "decreases" clause, or give no "decreases" clause and thus

-      // get a default "decreases" loop.

       Specification<Expression> decr;

-      if (Contract.Exists(cOld.Decreases.Expressions, e => e is WildcardExpr)) {

-        decr = cNew.Decreases;  // take the new decreases clauses, whatever they may be (including nothing at all)

+      if (cNew.Decreases.Expressions.Count == 0) {

+        // inherited whatever the previous loop used

+        decr = refinementCloner.CloneSpecExpr(cOld.Decreases);

       } else {

-        if (cNew.Decreases.Expressions.Count != 0) {

+        if (!Contract.Exists(cOld.Decreases.Expressions, e => e is WildcardExpr)) {

+          // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause.

           reporter.Error(cNew.Decreases.Expressions[0].tok, "a refining loop can provide a decreases clause only if the loop being refined was declared with 'decreases *'");

         }

-        decr = refinementCloner.CloneSpecExpr(cOld.Decreases);

+        decr = cNew.Decreases;

       }

 

       var invs = cOld.Invariants.ConvertAll(refinementCloner.CloneMayBeFreeExpr);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 52bc87ac..320a096a 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1961,9 +1961,6 @@ namespace Microsoft.Dafny
             }

           }

         }

-        if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {

-          Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");

-        }

       } else if (member is Function) {

         var f = (Function)member;

         var errorCount = ErrorCount;

@@ -4843,8 +4840,12 @@ namespace Microsoft.Dafny
         ResolveAttributes(s.Decreases.Attributes, new ResolveOpts(codeContext, true));

         foreach (Expression e in s.Decreases.Expressions) {

           ResolveExpression(e, new ResolveOpts(codeContext, true));

-          if (bodyMustBeSpecOnly && e is WildcardExpr) {

-            Error(e, "'decreases *' is not allowed on ghost loops");

+          if (e is WildcardExpr) {

+            if (bodyMustBeSpecOnly) {

+              Error(e, "'decreases *' is not allowed on ghost loops");

+            } else if (!codeContext.AllowsNontermination) {

+              Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");

+            }

           }

           // any type is fine

         }

@@ -4877,8 +4878,12 @@ namespace Microsoft.Dafny
 

         foreach (Expression e in s.Decreases.Expressions) {

           ResolveExpression(e, new ResolveOpts(codeContext, true));

-          if (s.IsGhost && e is WildcardExpr) {

-            Error(e, "'decreases *' is not allowed on ghost loops");

+          if (e is WildcardExpr) {

+            if (s.IsGhost) {

+              Error(e, "'decreases *' is not allowed on ghost loops");

+            } else if (!codeContext.AllowsNontermination) {

+              Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");

+            }

           }

           // any type is fine

         }

@@ -5454,7 +5459,7 @@ namespace Microsoft.Dafny
         s.Method = (Method)member;

         callee = s.Method;

         if (!isInitCall && callee is Constructor) {

-          Error(s, "a constructor is only allowed to be called when an object is being allocated");

+          Error(s, "a constructor is allowed to be called only when an object is being allocated");

         }

         s.IsGhost = callee.IsGhost;

         if (specContextOnly && !callee.IsGhost) {

@@ -5579,6 +5584,9 @@ namespace Microsoft.Dafny
           }

         }

       }

+      if (callee != null && Contract.Exists(callee.Decreases.Expressions, e => e is WildcardExpr) && !codeContext.AllowsNontermination) {

+        Error(s.Tok, "a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating");

+      }

     }

 

     /// <summary>

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index de160637..4f834793 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7970,9 +7970,6 @@ namespace Microsoft.Dafny {
         string msg;

         if (s.InferredDecreases) {

           msg = "cannot prove termination; try supplying a decreases clause for the loop";

-          if (s is RefinedWhileStmt) {

-            msg += " (note that a refined loop does not inherit 'decreases *' from the refined loop)";

-          }

         } else {

           msg = "decreases expression might not decrease";

         }

@@ -8370,6 +8367,10 @@ namespace Microsoft.Dafny {
       var types1 = new List<Type>();

       var callee = new List<Expr>();

       var caller = new List<Expr>();

+      if (RefinementToken.IsInherited(tok, currentModule) && contextDecreases.All(e => !RefinementToken.IsInherited(e.tok, currentModule))) {

+        // the call site is inherited but all the context decreases expressions are new

+        tok = new ForceCheckToken(tok);

+      }

       for (int i = 0; i < N; i++) {

         Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);

         Expression e1 = contextDecreases[i];

@@ -8377,7 +8378,7 @@ namespace Microsoft.Dafny {
           N = i;

           break;

         }

-        toks.Add(tok);

+        toks.Add(new NestedToken(tok, e1.tok));

         types0.Add(e0.Type.NormalizeExpand());

         types1.Add(e1.Type.NormalizeExpand());

         callee.Add(etranCurrent.TrExpr(e0));