fix: Correct cast of EnclosingClass (#4954)

This PR causes 5 kinds of crashes that could happen when a
function/method (with a specification) of a trait was overridden in an
abstract type.

Fixes #4952

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1094,7 +1094,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
       //generating trait post-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var en in f.OverriddenFunction.Ens) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassLikeDecl)f.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
         foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
           builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
         }
@@ -1135,7 +1135,7 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b
       List<FrameExpression> traitFrameExps = new List<FrameExpression>();
       FunctionCallSubstituter sub = null;
       foreach (var e in func.OverriddenFunction.Reads.Expressions) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)func.OverriddenFunction.EnclosingClass, (ClassLikeDecl)func.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)func.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)func.EnclosingClass);
         var newE = sub.Substitute(e.E);
         FrameExpression fe = new FrameExpression(e.tok, newE, e.FieldName);
         traitFrameExps.Add(fe);
@@ -1182,7 +1182,7 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde
       //generating trait pre-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var req in f.OverriddenFunction.Req) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassLikeDecl)f.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
         builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, sub.Substitute(req.E), "overridden function requires clause"));
       }
       //generating class pre-conditions
@@ -1425,7 +1425,7 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex
       //generating trait post-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var en in m.OverriddenMethod.Ens) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassLikeDecl)m.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
         foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
           builder.Add(Assert(m.RangeToken, s.E, new PODesc.EnsuresStronger()));
         }
@@ -1442,7 +1442,7 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E
       //generating trait pre-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var req in m.OverriddenMethod.Req) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassLikeDecl)m.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
         builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, sub.Substitute(req.E), "overridden requires clause"));
       }
       //generating class pre-conditions

Source/DafnyCore/Verifier/FunctionCallSubstituter.cs

@@ -4,13 +4,13 @@
 namespace Microsoft.Dafny {
   public class FunctionCallSubstituter : Substituter {
     public readonly TraitDecl Tr;
-    public readonly ClassLikeDecl Cl;
+    public readonly TopLevelDeclWithMembers Cl;
 
     // 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, ClassLikeDecl cl)
+      TraitDecl parentTrait, TopLevelDeclWithMembers cl)
       : base(new ThisExpr(cl.tok) { Type = UserDefinedType.FromTopLevelDecl(cl.tok, cl) }, substMap, typeMap) {
       this.Tr = parentTrait;
       this.Cl = cl;

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

@@ -0,0 +1,29 @@
+// RUN: %testDafnyForEachResolver "%s" -- --general-traits=datatype
+
+trait A<K> {
+  function FunctionRequires(): bool
+    requires true
+  function FunctionReads(): bool
+    reads {}
+    decreases 2
+  function FunctionEnsures(): bool
+    ensures true
+
+  method MethodRequires()
+    requires true
+  method MethodEnsures()
+    ensures true
+}
+
+type B extends A<string> {
+  // Each of the following 5 override checks once caused a crash, because those checks
+  // were not expecting the overrides to be found in an abstract type.
+
+  function FunctionRequires(): bool
+  function FunctionReads(): bool
+    decreases 2
+  function FunctionEnsures(): bool
+
+  method MethodRequires()
+  method MethodEnsures()
+}

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

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

docs/dev/news/4954.fix

@@ -0,0 +1 @@
+Fix crash when a function/method with a specification is overridden in an abstract type.