Fixed crashes in overrides checking of function decreases clauses, and improved the error message reported to users

4 files changed, 76 insertions, 38 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 134fb4c1..d14d82a3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2223,6 +2223,7 @@ namespace Microsoft.Dafny {
   public interface ICallable : ICodeContext

   {

     IToken Tok { get; }

+    string WhatKind { get; }

     string NameRelativeToModule { get; }

     Specification<Expression> Decreases { get; }

     /// <summary>

@@ -2234,6 +2235,7 @@ namespace Microsoft.Dafny {
   }

   public class DontUseICallable : ICallable

   {

+    public string WhatKind { get { throw new cce.UnreachableException(); } }

     public bool IsGhost { get { throw new cce.UnreachableException(); } }

     public List<TypeParameter> TypeArgs { get { throw new cce.UnreachableException(); } }

     public List<Formal> Ins { get { throw new cce.UnreachableException(); } }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index cefce6b6..a4cf3700 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3018,7 +3018,7 @@ namespace Microsoft.Dafny {
         AddFunctionOverrideReqsChk(f, builder, etran, substMap);

 

         //adding assert R <= Rank’;

-        AddFunctionOverrideTerminationChk(f, builder, etran, substMap);

+        AddOverrideTerminationChk(f, f.OverriddenFunction, builder, etran, substMap);

 

         //adding assert W <= Frame’

         AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap);

@@ -3181,35 +3181,6 @@ namespace Microsoft.Dafny {
         builder.Add(Assert(tok, q, "expression may read an object not in the parent trait context's reads clause", kv));

     }

 

-    private void AddFunctionOverrideTerminationChk(Function f, 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 (f.Decreases != null)

-        {

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

-            {

-                decrToks.Add(decC.tok);

-                decrTypes1.Add(decC.Type);

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

-            }

-        }

-        if (f.OverriddenFunction.Decreases != null)

-        {

-            foreach (var decT in f.OverriddenFunction.Decreases.Expressions)

-            {

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

-                decrTypes2.Add(decCNew.Type);

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

-            }

-        }

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

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

-    }

-

     private void AddFunctionOverrideReqsChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)

     {

         //generating trait pre-conditions with class variables

@@ -3277,7 +3248,7 @@ namespace Microsoft.Dafny {
         AddMethodOverrideReqsChk(m, builder, etran, substMap);

 

         //adding assert R <= Rank’;

-        AddMethodOverrideTerminationChk(m, builder, etran, substMap);

+        AddOverrideTerminationChk(m, m.OverriddenMethod, builder, etran, substMap);

 

         //adding assert W <= Frame’

         AddMethodOverrideSubsetChk(m, builder, etran, localVariables, substMap);

@@ -3364,14 +3335,15 @@ namespace Microsoft.Dafny {
         }

     }

 

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

-      Contract.Requires(m != null);

+    private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap) {

+      Contract.Requires(original != null);

+      Contract.Requires(overryd != 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;

+      var contextDecreases = overryd.Decreases.Expressions;

+      var calleeDecreases = original.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

@@ -3392,7 +3364,7 @@ namespace Microsoft.Dafny {
           N = i;

           break;

         }

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

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

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

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

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

@@ -3425,7 +3397,7 @@ namespace Microsoft.Dafny {
       //   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"));

+      builder.Add(Assert(original.Tok, decrChk, string.Format("{0}'s decreases clause must be below or equal to that in the trait", original.WhatKind)));

     }

 

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

diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy b/Test/dafny0/Trait/TraitsDecreases.dfy
index 53ce28be..8ab3672a 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy
@@ -106,3 +106,49 @@ class CC extends TT {
     decreases *

   { }

 }

+

+

+// The following module contains various regression tests

+module More {

+  trait A0 {

+    predicate P() decreases 5

+  }

+  class B0 extends A0 {

+    predicate P()  // error: rank is not lower

+  }

+

+  trait A1 {

+    predicate P() decreases 5

+  }

+  class B1 extends A1 {

+    predicate P() reads this  // error: rank is not lower

+  }

+

+  trait A2 {

+    predicate P(x: int)

+  }

+  class B2 extends A2 {

+    predicate P(x: int) reads this  // error: rank is not lower

+  }

+

+  trait A3 {

+    predicate P() reads this

+  }

+  class B3 extends A3 {

+    predicate P()  // error: rank is not lower

+  }

+

+  trait A4 {

+    predicate P(x: int) decreases 5

+  }

+  class B4 extends A4 {

+    predicate P(x: int)  // error: rank is not lower

+  }

+

+  trait A5 {

+    method M(x: int) decreases 5

+  }

+  class B5 extends A5 {

+    method M(x: int)  // error: rank is not lower

+  }

+}

diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
index 6c76f9a8..2607a0c6 100644
--- a/Test/dafny0/Trait/TraitsDecreases.dfy.expect
+++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect
@@ -1,3 +1,21 @@
+TraitsDecreases.dfy(117,15): Error: predicate's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(124,15): Error: predicate's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(131,15): Error: predicate's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(138,15): Error: predicate's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(145,15): Error: predicate's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

+TraitsDecreases.dfy(152,12): Error: method's decreases clause must be below or equal to that in the trait

+Execution trace:

+    (0,0): anon0

 TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait

 Execution trace:

     (0,0): anon0

@@ -14,4 +32,4 @@ TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or eq
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 63 verified, 5 errors

+Dafny program verifier finished with 75 verified, 11 errors