fix: Termination override check for certain non-reference trait imple…

…mentations (#5087)

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1461,6 +1461,9 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
  // Note, it is as if the trait's method is calling the class's method.
  var contextDecreases = overryd.Decreases.Expressions;
  var calleeDecreases = original.Decreases.Expressions;
+ var T = (TraitDecl)((MemberDecl)overryd).EnclosingClass;
+ var I = (TopLevelDeclWithMembers)((MemberDecl)original).EnclosingClass;
+
  // 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
@@ -1473,10 +1476,12 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
  var types1 = new List<Type>();
  var callee = new List<Expr>();
  var caller = new List<Expr>();
+ FunctionCallSubstituter sub = null;
 
  for (int i = 0; i < N; i++) {
  Expression e0 = calleeDecreases[i];
- Expression e1 = Substitute(contextDecreases[i], null, substMap, typeMap);
+ sub ??= new FunctionCallSubstituter(substMap, typeMap, T, I);
+ Expression e1 = sub.Substitute(contextDecreases[i]);
  if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {
  N = i;
  break;
@@ -1486,6 +1491,10 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
  types1.Add(e1.Type.NormalizeExpand());
  callee.Add(etran.TrExpr(e0));
  caller.Add(etran.TrExpr(e1));
+ var canCall = etran.CanCallAssumption(e1);
+ if (canCall != Bpl.Expr.True) {
+ builder.Add(new Bpl.AssumeCmd(e1.tok, canCall));
+ }
  }
 
  var decrCountT = contextDecreases.Count;

Source/DafnyCore/Verifier/FunctionCallSubstituter.cs

@@ -4,16 +4,16 @@
 namespace Microsoft.Dafny {
  public class FunctionCallSubstituter : Substituter {
  public readonly TraitDecl Tr;
- public readonly TopLevelDeclWithMembers Cl;
+ public readonly TopLevelDeclWithMembers Impl;
 
  // We replace all occurrences of the trait version of the function with the class version. This is only allowed if
  // the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex
  // expressions that evaluate to one.
  public FunctionCallSubstituter(Dictionary<IVariable, Expression /*!*/> /*!*/ substMap, Dictionary<TypeParameter, Type> typeMap,
- TraitDecl parentTrait, TopLevelDeclWithMembers cl)
- : base(new ThisExpr(cl.tok) { Type = UserDefinedType.FromTopLevelDecl(cl.tok, cl) }, substMap, typeMap) {
- this.Tr = parentTrait;
- this.Cl = cl;
+ TraitDecl parentTrait, TopLevelDeclWithMembers impl)
+ : base(new ThisExpr(impl.tok) { Type = UserDefinedType.FromTopLevelDecl(impl.tok, impl) }, substMap, typeMap) {
+ Tr = parentTrait;
+ Impl = impl;
  }
 
  public override Expression Substitute(Expression expr) {
@@ -24,10 +24,10 @@ public override Expression Substitute(Expression expr) {
  Function function;
  if ((e.Function.EnclosingClass == Tr || Tr.InheritedMembers.Contains(e.Function)) &&
  e.Receiver.Resolved is ThisExpr && receiver.Resolved is ThisExpr &&
- Cl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) {
+ Impl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) {
  receiver = new ThisExpr((TopLevelDeclWithMembers)f.EnclosingClass);
  function = (Function)f;
- typeApplicationAtEnclosingClass = receiver.Type.AsParentType(Cl).TypeArgs.ToList();
+ typeApplicationAtEnclosingClass = receiver.Type.AsParentType(Impl).TypeArgs.ToList();
  } else {
  function = e.Function;
  }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy

@@ -0,0 +1,55 @@
+// RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype
+
+trait Tr1 {
+ function Decrease(): nat {
+ 0
+ }
+
+ function F(): nat
+ decreases Decrease()
+}
+
+datatype Dt1 extends Tr1 = Dt {
+ function F(): nat
+ decreases 0
+ {
+ 0
+ }
+}
+
+trait Tr2<A> {
+ function Decrease(): nat {
+ 0
+ }
+
+ function F(): A
+ decreases Decrease()
+}
+
+datatype Dt2 extends Tr2<nat> = Dt {
+ function F(): nat
+ decreases 0
+ {
+ 0
+ }
+}
+
+trait ProgramTrait {
+ function Rank(): nat
+
+ method Compute() returns (r: Result)
+ decreases Rank()
+}
+
+datatype Result = Bounce(next: ProgramTrait) | Done
+
+datatype Trivial extends ProgramTrait = Trivial
+{
+ function Rank(): nat { 0 }
+
+ method Compute() returns (r: Result)
+ decreases Rank()
+ {
+ return Done();
+ }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 10 verified, 0 errors

docs/dev/news/5087.fix

@@ -0,0 +1 @@
+Termination override check for certain non-reference trait implementations