Added test cases and fixes for overrides termination checks

Removed syntactic presence checks for specifications--these will be checked semantically by the verifier

2 files changed, 66 insertions, 64 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bf417de7..727011e8 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2952,25 +2952,6 @@ namespace Microsoft.Dafny
                             classMethod.OverriddenMethod = traitMethod;

                             //adding a call graph edge from the trait method to that of class

                             cl.Module.CallGraph.AddEdge(traitMethod, classMethod);

-

-                            //checking specifications

-                            //class method must provide its own specifications in case the overriden method has provided any

-                            if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0))  //it means m.OverriddenMethod.Req =>  m.Req

-                            {

-                                Error(classMethod, "Method must provide its own Requires clauses anew");

-                            }

-                            if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0))  //it means m.OverriddenMethod.Ens =>  m.Ens

-                            {

-                                Error(classMethod, "Method must provide its own Ensures clauses anew");

-                            }

-                            if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0))  //it means m.OverriddenMethod.Mod =>  m.Mod

-                            {

-                                Error(classMethod, "Method must provide its own Modifies clauses anew");

-                            }

-                            if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0))  //it means m.OverriddenMethod.Decreases =>  m.Decreases

-                            {

-                                Error(classMethod, "Method must provide its own Decreases clauses anew");

-                            }

                         }

                     }

                     else if (traitMem.Value is Function)

@@ -2985,25 +2966,6 @@ namespace Microsoft.Dafny
                             classFunction.OverriddenFunction = traitFunction;

                             //adding a call graph edge from the trait function to that of class

                             cl.Module.CallGraph.AddEdge(traitFunction, classFunction);

-

-                            //checking specifications

-                            //class function must provide its own specifications in case the overriden function has provided any

-                            if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0))  //it means m.OverriddenMethod.Req =>  m.Req

-                            {

-                                Error(classFunction, "Function must provide its own Requires clauses anew");

-                            }

-                            if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0))  //it means m.OverriddenMethod.Ens =>  m.Ens

-                            {

-                                Error(classFunction, "Function must provide its own Ensures clauses anew");

-                            }

-                            if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0))  //it means m.OverriddenMethod.Mod =>  m.Mod

-                            {

-                                Error(classFunction, "Function must provide its own Reads clauses anew");

-                            }

-                            if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0))  //it means m.OverriddenMethod.Decreases =>  m.Decreases

-                            {

-                                Error(classFunction, "Function must provide its own Decreases clauses anew");

-                            }

                         }

                     }

                     else if (traitMem.Value is Field)

@@ -3058,6 +3020,11 @@ namespace Microsoft.Dafny
                         {

                             Method classMethod = (Method)classMem;

                             refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);

+                            var traitMethodAllowsNonTermination = Contract.Exists(traitMethod.Decreases.Expressions, e => e is WildcardExpr);

+                            var classMethodAllowsNonTermination = Contract.Exists(classMethod.Decreases.Expressions, e => e is WildcardExpr);

+                            if (classMethodAllowsNonTermination && !traitMethodAllowsNonTermination) {

+                              Error(classMethod.tok, "not allowed to override a terminating method with a possibly non-terminating method ('{0}')", classMethod.Name);

+                            }

                         }

                         if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)

                             Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 96405daf..8678e2c3 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3405,33 +3405,68 @@ namespace Microsoft.Dafny {
         }

     }

 

-    private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)

-    {

-        var decrToks = new List<IToken>();

-        var decrTypes1 = new List<Type>();

-        var decrTypes2 = new List<Type>();

-        var decrClass = new List<Expr>();

-        var decrTrait = new List<Expr>();

-        if (m.Decreases != null)

-        {

-            foreach (var decC in m.Decreases.Expressions)

-            {

-                decrToks.Add(decC.tok);

-                decrTypes1.Add(decC.Type);

-                decrClass.Add(etran.TrExpr(decC));

-            }

-        }

-        if (m.OverriddenMethod.Decreases != null)

-        {

-            foreach (var decT in m.OverriddenMethod.Decreases.Expressions)

-            {

-                var decCNew = Substitute(decT, null, substMap);

-                decrTypes2.Add(decCNew.Type);

-                decrTrait.Add(etran.TrExpr(decCNew));

-            }

+    private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap) {

+      Contract.Requires(m != null);

+      Contract.Requires(builder != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(substMap != null);

+      // Note, it is as if the trait's method is calling the class's method.

+      var contextDecreases = m.OverriddenMethod.Decreases.Expressions;

+      var calleeDecreases = m.Decreases.Expressions;

+      // We want to check:  calleeDecreases <= contextDecreases (note, we can allow equality, since there is a bounded, namely 1, number of dynamic dispatches)

+      if (Contract.Exists(contextDecreases, e => e is WildcardExpr)) {

+        // no check needed

+        return;

+      }

+

+      int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);

+      var toks = new List<IToken>();

+      var types0 = new List<Type>();

+      var types1 = new List<Type>();

+      var callee = new List<Expr>();

+      var caller = new List<Expr>();

+

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

+        Expression e0 = calleeDecreases[i];

+        Expression e1 = Substitute(contextDecreases[i], null, substMap);

+        if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {

+          N = i;

+          break;

         }

-        var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false);

-        builder.Add(new Bpl.AssertCmd(m.tok, decrChk));

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

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

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

+        callee.Add(etran.TrExpr(e0));

+        caller.Add(etran.TrExpr(e1));

+      }

+

+      var decrCountT = contextDecreases.Count;

+      var decrCountC = calleeDecreases.Count;

+      // Generally, we want to produce a check "decrClass <= decrTrait", allowing (the common case where) they are equal.

+      // * If N < decrCountC && N < decrCountT, then "decrClass <= decrTrait" if the comparison ever gets beyond the

+      //   parts that survived truncation.  Thus, we compare with "allowNoChange" set to "false".

+      // Otherwise:

+      // * If decrCountC == decrCountT, then the truncation we did above had no effect and we pass in "allowNoChange" as "true".

+      // * If decrCountC > decrCountT, then we will have truncated decrClass above.  Let x,y and x' denote decrClass and

+      //   decrTrait, respectively, where x and x' have the same length.  Considering how Dafny in effect pads the end of

+      //   decreases tuples with a \top, we were supposed to evaluate (x,(y,\top)) <= (x',\top), which by lexicographic pairs

+      //   we can expand to:

+      //       x <= x' && (x == x' ==> (y,\top) <= \top)

+      //   which is equivalent to just x <= x'.  Thus, we called DecreasesCheck to compare x and x' and we pass in "allowNoChange"

+      //   as "true".

+      // * If decrCountC < decrCountT, then we will have truncated decrTrait above.  Let x and x',y' denote decrClass and

+      //   decrTrait, respectively, where x and x' have the same length.  We then want to check (x,\top) <= (x',(y',\top)), which

+      //   expands to:

+      //       x <= x' && (x == x' ==> \top <= (y',\top))

+      //    =      { \top is strictly larger than a pair }

+      //       x <= x' && (x == x' ==> false)

+      //    =

+      //       x < x'

+      //   So we perform our desired check by calling DecreasesCheck to strictly compare x and x', so we pass in "allowNoChange"

+      //   as "false".

+      bool allowNoChange = N == decrCountT && decrCountT <= decrCountC;

+      var decrChk = DecreasesCheck(toks, types0, types1, callee, caller, null, null, allowNoChange, false);

+      builder.Add(Assert(m.tok, decrChk, "method's decreases clause must be below or equal to that in the trait"));

     }

 

     private void AddMethodOverrideSubsetChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables, Dictionary<IVariable, Expression> substMap)