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

…mentations

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) (overryd is Function f1 ? f1.EnclosingClass : ((Method)overryd).EnclosingClass);
+ var I = (TopLevelDeclWithMembers) (original is Function f2 ? f2.EnclosingClass : ((Method)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
@@ -1474,9 +1477,12 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
  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 +1492,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;
  }

docs/dev/news/5087.fix

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