fix: Forbid recursive function uses in decreases clauses (#6045)

Fixes #6043 

This PR changes two verification checks into resolution checks:

* use of a function in a `decreases` clause in the function's SCC
* use of naked functions inside an SCC

The first of these was omitted in the recent `CanCall` PR. Hence, this
PR fixes that regression.

<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/AST/Expressions/Applications/ThisExpr.cs

@@ -66,16 +66,16 @@ public override bool IsImplicit {
 /// gives a way to distinguish this receiver from other receivers, which
 /// plays a role in checking the restrictions on divided block statements.
 /// </summary>
-public class ImplicitThisExpr_ConstructorCall : ImplicitThisExpr, ICloneable<ImplicitThisExpr_ConstructorCall> {
-  public ImplicitThisExpr_ConstructorCall(Cloner cloner, ImplicitThisExpr_ConstructorCall original) : base(cloner, original) {
+public class ImplicitThisExprConstructorCall : ImplicitThisExpr, ICloneable<ImplicitThisExprConstructorCall> {
+  public ImplicitThisExprConstructorCall(Cloner cloner, ImplicitThisExprConstructorCall original) : base(cloner, original) {
   }
 
-  public ImplicitThisExpr_ConstructorCall(IOrigin tok)
+  public ImplicitThisExprConstructorCall(IOrigin tok)
     : base(tok) {
     Contract.Requires(tok != null);
   }
 
-  public new ImplicitThisExpr_ConstructorCall Clone(Cloner cloner) {
-    return new ImplicitThisExpr_ConstructorCall(cloner, this);
+  public new ImplicitThisExprConstructorCall Clone(Cloner cloner) {
+    return new ImplicitThisExprConstructorCall(cloner, this);
   }
 }

Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs → Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs

@@ -8,18 +8,18 @@ namespace Microsoft.Dafny;
 /// <summary>
 /// This class is used only inside the resolver itself. It gets hung in the AST in uncompleted name segments.
 /// </summary>
-class Resolver_IdentifierExpr : Expression, IHasReferences, ICloneable<Resolver_IdentifierExpr> {
+class ResolverIdentifierExpr : Expression, IHasReferences, ICloneable<ResolverIdentifierExpr> {
   public readonly TopLevelDecl Decl;
   public readonly List<Type> TypeArgs;
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Decl != null);
     Contract.Invariant(TypeArgs != null);
     Contract.Invariant(TypeArgs.Count == Decl.TypeArgs.Count);
-    Contract.Invariant(Type is ResolverType_Module || Type is ResolverType_Type);
+    Contract.Invariant(Type is ResolverTypeModule or ResolverTypeType);
   }
 
-  public Resolver_IdentifierExpr(Cloner cloner, Resolver_IdentifierExpr original) : base(cloner, original) {
+  public ResolverIdentifierExpr(Cloner cloner, ResolverIdentifierExpr original) : base(cloner, original) {
     Decl = original.Decl;
     TypeArgs = original.TypeArgs;
   }
@@ -38,38 +38,38 @@ public override Type ReplaceTypeArguments(List<Type> arguments) {
       throw new NotSupportedException();
     }
   }
-  public class ResolverType_Module : ResolverType {
+  public class ResolverTypeModule : ResolverType {
     [System.Diagnostics.Contracts.Pure]
     public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) {
       Contract.Assert(parseAble == false);
       return "#module";
     }
     public override bool Equals(Type that, bool keepConstraints = false) {
-      return that.NormalizeExpand(keepConstraints) is ResolverType_Module;
+      return that.NormalizeExpand(keepConstraints) is ResolverTypeModule;
     }
   }
-  public class ResolverType_Type : ResolverType {
+  public class ResolverTypeType : ResolverType {
     [System.Diagnostics.Contracts.Pure]
     public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) {
       Contract.Assert(parseAble == false);
       return "#type";
     }
     public override bool Equals(Type that, bool keepConstraints = false) {
-      return that.NormalizeExpand(keepConstraints) is ResolverType_Type;
+      return that.NormalizeExpand(keepConstraints) is ResolverTypeType;
     }
   }
 
-  public Resolver_IdentifierExpr(IOrigin origin, TopLevelDecl decl, List<Type> typeArgs)
+  public ResolverIdentifierExpr(IOrigin origin, TopLevelDecl decl, List<Type> typeArgs)
     : base(origin) {
     Contract.Requires(origin != null);
     Contract.Requires(decl != null);
     Contract.Requires(typeArgs != null && typeArgs.Count == decl.TypeArgs.Count);
     Decl = decl;
     TypeArgs = typeArgs;
-    Type = decl is ModuleDecl ? (Type)new ResolverType_Module() : new ResolverType_Type();
+    Type = decl is ModuleDecl ? (Type)new ResolverTypeModule() : new ResolverTypeType();
     PreType = decl is ModuleDecl ? new PreTypePlaceholderModule() : new PreTypePlaceholderType();
   }
-  public Resolver_IdentifierExpr(IOrigin origin, TypeParameter tp)
+  public ResolverIdentifierExpr(IOrigin origin, TypeParameter tp)
     : this(origin, tp, new List<Type>()) {
     Contract.Requires(origin != null);
     Contract.Requires(tp != null);
@@ -79,7 +79,7 @@ public IEnumerable<Reference> GetReferences() {
     return new[] { new Reference(Center, Decl) };
   }
 
-  public Resolver_IdentifierExpr Clone(Cloner cloner) {
-    return new Resolver_IdentifierExpr(cloner, this);
+  public ResolverIdentifierExpr Clone(Cloner cloner) {
+    return new ResolverIdentifierExpr(cloner, this);
   }
 }

Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs

@@ -571,12 +571,12 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
         if (parensNeeded) { wr.Write("("); }
         if (!e.Lhs.IsImplicit) {
           PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword);
-          if (e.Lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+          if (e.Lhs.Type is ResolverIdentifierExpr.ResolverTypeType) {
             Contract.Assert(e.Lhs is NameSegment || e.Lhs is ExprDotName);  // these are the only expressions whose .Type can be ResolverType_Type
             if (options.DafnyPrintResolvedFile != null && options.PrintMode == PrintModes.Everything) {
               // The printing of e.Lhs printed the type arguments only if they were given explicitly in the input.
               var optionalTypeArgs = e.Lhs is NameSegment ns ? ns.OptTypeArguments : ((ExprDotName)e.Lhs).OptTypeArguments;
-              if (optionalTypeArgs == null && e.Lhs.Resolved is Resolver_IdentifierExpr ri) {
+              if (optionalTypeArgs == null && e.Lhs.Resolved is ResolverIdentifierExpr ri) {
                 PrintTypeInstantiation(ri.TypeArgs);
               }
             }
@@ -1228,7 +1228,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
         wr.Write("[BoogieWrapper]");  // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here
       } else if (expr is BoogieGenerator.BoogieFunctionCall) {
         wr.Write("[BoogieFunctionCall]");  // this prevents debugger watch window crash
-      } else if (expr is Resolver_IdentifierExpr) {
+      } else if (expr is ResolverIdentifierExpr) {
         wr.Write("[Resolver_IdentifierExpr]");  // we can get here in the middle of a debugging session
       } else if (expr is DecreasesToExpr decreasesToExpr) {
         var opBindingStrength = BindingStrengthDecreasesTo;

Source/DafnyCore/AST/Types/Types.cs

@@ -1145,10 +1145,10 @@ public static bool Equal_Improved(Type a, Type b) {
           return true;
         }
       }
-    } else if (a is Resolver_IdentifierExpr.ResolverType_Module) {
-      return b is Resolver_IdentifierExpr.ResolverType_Module;
-    } else if (a is Resolver_IdentifierExpr.ResolverType_Type) {
-      return b is Resolver_IdentifierExpr.ResolverType_Type;
+    } else if (a is ResolverIdentifierExpr.ResolverTypeModule) {
+      return b is ResolverIdentifierExpr.ResolverTypeModule;
+    } else if (a is ResolverIdentifierExpr.ResolverTypeType) {
+      return b is ResolverIdentifierExpr.ResolverTypeType;
     } else {
       // this is an unexpected type; however, it may be that we get here during the resolution of an erroneous
       // program, so we'll just return false
@@ -2232,7 +2232,7 @@ public void AddSubtype(TypeConstraint c) {
   public enum Family { Unknown, Bool, Char, IntLike, RealLike, Ordinal, BitVector, ValueType, Ref, Opaque }
   public Family family = Family.Unknown;
   public static Family GetFamily(Type t) {
-    Contract.Ensures(Contract.Result<Family>() != Family.Unknown || t is TypeProxy || t is Resolver_IdentifierExpr.ResolverType);  // return Unknown ==> t is TypeProxy || t is ResolverType
+    Contract.Ensures(Contract.Result<Family>() != Family.Unknown || t is TypeProxy || t is ResolverIdentifierExpr.ResolverType);  // return Unknown ==> t is TypeProxy || t is ResolverType
     if (t.IsBoolType) {
       return Family.Bool;
     } else if (t.IsCharType) {

Source/DafnyCore/AST/Types/UserDefinedType.cs

@@ -165,7 +165,7 @@ public UserDefinedType(IOrigin origin, string name, TopLevelDecl cd, [Captured]
     this.TypeArgs = typeArgs;
     if (namePath == null) {
       var ns = new NameSegment(origin, name, typeArgs.Count == 0 ? null : typeArgs);
-      var r = new Resolver_IdentifierExpr(origin, cd, typeArgs);
+      var r = new ResolverIdentifierExpr(origin, cd, typeArgs);
       ns.ResolvedExpression = r;
       ns.Type = r.Type;
       this.NamePath = ns;
@@ -218,7 +218,7 @@ public UserDefinedType(IOrigin origin, TypeParameter tp) : base(origin) {
     this.TypeArgs = new List<Type>();
     this.ResolvedClass = tp;
     var ns = new NameSegment(origin, tp.Name, null);
-    var r = new Resolver_IdentifierExpr(origin, tp);
+    var r = new ResolverIdentifierExpr(origin, tp);
     ns.ResolvedExpression = r;
     ns.Type = r.Type;
     this.NamePath = ns;

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -1606,7 +1606,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
       Contract.Assert(enclosingModule == null);
       enclosingModule = module;
       var wr = CreateModule(module, module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode);
-      var v = new CheckHasNoAssumes_Visitor(this, wr);
+      var v = new CheckHasNoAssumesVisitor(this, wr);
       foreach (TopLevelDecl d in module.TopLevelDecls) {
         if (!ProgramResolver.ShouldCompile(d)) {
           continue;
@@ -2151,7 +2151,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite
       Contract.Ensures(thisContext == null);
 
       var errorWr = classWriter.ErrorWriter();
-      var v = new CheckHasNoAssumes_Visitor(this, errorWr);
+      var v = new CheckHasNoAssumesVisitor(this, errorWr);
 
       var inheritedMembers = c.InheritedMembers;
       OrderedBySCC(inheritedMembers, c);
@@ -3263,10 +3263,10 @@ protected string DefaultValueCoercedIfNecessary(Type type, ConcreteSyntaxTree wr
 
     // ----- Stmt ---------------------------------------------------------------------------------
 
-    public class CheckHasNoAssumes_Visitor : BottomUpVisitor {
+    public class CheckHasNoAssumesVisitor : BottomUpVisitor {
       readonly SinglePassCodeGenerator codeGenerator;
       ConcreteSyntaxTree wr;
-      public CheckHasNoAssumes_Visitor(SinglePassCodeGenerator c, ConcreteSyntaxTree wr) {
+      public CheckHasNoAssumesVisitor(SinglePassCodeGenerator c, ConcreteSyntaxTree wr) {
         Contract.Requires(c != null);
         codeGenerator = c;
         this.wr = wr;

Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs → Source/DafnyCore/Resolver/CheckDividedConstructorInitVisitor.cs

@@ -4,8 +4,8 @@
 
 namespace Microsoft.Dafny;
 
-class CheckDividedConstructorInit_Visitor : ResolverTopDownVisitor<int> {
-  public CheckDividedConstructorInit_Visitor(ErrorReporter reporter)
+class CheckDividedConstructorInitVisitor : ResolverTopDownVisitor<int> {
+  public CheckDividedConstructorInitVisitor(ErrorReporter reporter)
     : base(reporter) {
     Contract.Requires(reporter != null);
   }
@@ -65,7 +65,7 @@ protected override bool VisitOneExpr(Expression expr, ref int unused) {
       }
     } else if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Assigned }) {
       return false;  // don't continue the recursion
-    } else if (expr is ThisExpr && !(expr is ImplicitThisExpr_ConstructorCall)) {
+    } else if (expr is ThisExpr && !(expr is ImplicitThisExprConstructorCall)) {
       reporter.Error(MessageSource.Resolver, expr.Origin, "in the first division of the constructor body (before 'new;'), 'this' can only be used to assign to its fields");
     }
     return base.VisitOneExpr(expr, ref unused);

Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs → Source/DafnyCore/Resolver/CheckTypeCharacteristicsVisitor.cs

@@ -9,8 +9,8 @@ namespace Microsoft.Dafny;
 /// In addition, this visitor checks that operations that require equality are applied to
 /// types that really do support equality; this, too, is checked only in compiled contexts.
 /// </summary>
-class CheckTypeCharacteristics_Visitor : ResolverTopDownVisitor<bool> {
-  public CheckTypeCharacteristics_Visitor(ErrorReporter reporter)
+class CheckTypeCharacteristicsVisitor : ResolverTopDownVisitor<bool> {
+  public CheckTypeCharacteristicsVisitor(ErrorReporter reporter)
     : base(reporter) {
     Contract.Requires(reporter != null);
   }

Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs → Source/DafnyCore/Resolver/CollectFriendlyCallsInSpecVisitor.cs

@@ -3,10 +3,10 @@
 
 namespace Microsoft.Dafny;
 
-class CollectFriendlyCallsInSpec_Visitor : FindFriendlyCalls_Visitor {
+class CollectFriendlyCallsInSpecVisitor : FindFriendlyCallsVisitor {
   readonly ISet<Expression> friendlyCalls;
   readonly ExtremeLemma Context;
-  public CollectFriendlyCallsInSpec_Visitor(ErrorReporter reporter, ISet<Expression> friendlyCalls, bool co, ExtremeLemma context)
+  public CollectFriendlyCallsInSpecVisitor(ErrorReporter reporter, ISet<Expression> friendlyCalls, bool co, ExtremeLemma context)
     : base(reporter, co, context.KNat) {
     Contract.Requires(reporter != null);
     Contract.Requires(friendlyCalls != null);

Source/DafnyCore/Resolver/DetectUnsoundFunctionReferencesVisitor.cs

@@ -0,0 +1,41 @@
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny;
+
+class DetectUnsoundFunctionReferencesVisitor : ResolverBottomUpVisitor {
+  private readonly ICallable context;
+  private bool doDecreasesChecks;
+  private DetectUnsoundFunctionReferencesVisitor(ModuleResolver resolver, ICallable context)
+    : base(resolver) {
+    Contract.Requires(resolver != null);
+    Contract.Requires(context != null);
+    this.context = context;
+  }
+
+  public static void Check(Function function, ModuleResolver resolver) {
+    var visitor = new DetectUnsoundFunctionReferencesVisitor(resolver, function);
+    visitor.doDecreasesChecks = false;
+    visitor.Visit(function);
+    visitor.doDecreasesChecks = true;
+    visitor.Visit(function.Decreases.Expressions);
+  }
+
+  protected override void VisitOneExpr(Expression expr) {
+    if (!doDecreasesChecks && expr is MemberSelectExpr { Member: Function fn } && ModuleDefinition.InSameSCC(context, fn)) {
+      resolver.reporter.Error(MessageSource.Resolver, expr.Origin,
+        "cannot use naked function in recursive setting. Possible solution: eta expansion.");
+    }
+
+    if (doDecreasesChecks && expr is FunctionCallExpr callExpr && ModuleDefinition.InSameSCC(context, callExpr.Function)) {
+      string msg;
+      if (context == callExpr.Function) {
+        msg = "a decreases clause is not allowed to call the enclosing function";
+      } else {
+        msg = $"the decreases clause of {context.WhatKind} '{context.NameRelativeToModule}' is not allowed to call '{callExpr.Function}', " +
+              "because they are mutually recursive";
+      }
+
+      resolver.reporter.Error(MessageSource.Resolver, callExpr.Origin, msg);
+    }
+  }
+}

Source/DafnyCore/Resolver/ExtremeLemmaChecksVisitor.cs

@@ -0,0 +1,35 @@
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny;
+
+class ExtremeLemmaChecksVisitor : ResolverBottomUpVisitor {
+  ExtremeLemma context;
+  public ExtremeLemmaChecksVisitor(ModuleResolver resolver, ExtremeLemma context)
+    : base(resolver) {
+    Contract.Requires(resolver != null);
+    Contract.Requires(context != null);
+    this.context = context;
+  }
+  protected override void VisitOneStmt(Statement stmt) {
+    if (stmt is CallStmt callStmt) {
+      if (callStmt.Method is ExtremeLemma or PrefixLemma) {
+        // all is cool
+      } else {
+        // the call goes from an extreme lemma context to a non-extreme-lemma callee
+        if (ModuleDefinition.InSameSCC(context, callStmt.Method)) {
+          // we're looking at a recursive call (to a non-extreme-lemma)
+          resolver.reporter.Error(MessageSource.Resolver, callStmt.Origin, "a recursive call from a {0} can go only to other {0}s and prefix lemmas", context.WhatKind);
+        }
+      }
+    }
+  }
+  protected override void VisitOneExpr(Expression expr) {
+    if (expr is FunctionCallExpr callExpr) {
+      // the call goes from a greatest lemma context to a non-greatest-lemma callee
+      if (ModuleDefinition.InSameSCC(context, callExpr.Function)) {
+        // we're looking at a recursive call (to a non-greatest-lemma)
+        resolver.reporter.Error(MessageSource.Resolver, callExpr.Origin, "a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas");
+      }
+    }
+  }
+}

Source/DafnyCore/Resolver/ExtremePredicateChecks_Visitor.cs → Source/DafnyCore/Resolver/ExtremePredicateChecksVisitor.cs

@@ -2,9 +2,9 @@
 
 namespace Microsoft.Dafny;
 
-class ExtremePredicateChecks_Visitor : FindFriendlyCalls_Visitor {
+class ExtremePredicateChecksVisitor : FindFriendlyCallsVisitor {
   readonly ExtremePredicate context;
-  public ExtremePredicateChecks_Visitor(ErrorReporter reporter, ExtremePredicate context)
+  public ExtremePredicateChecksVisitor(ErrorReporter reporter, ExtremePredicate context)
     : base(reporter, context is GreatestPredicate, context.KNat) {
     Contract.Requires(reporter != null);
     Contract.Requires(context != null);

Source/DafnyCore/Resolver/FillInDefaultLoopDecreases_Visitor.cs → Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs

@@ -3,9 +3,9 @@
 
 namespace Microsoft.Dafny;
 
-class FillInDefaultLoopDecreases_Visitor : ResolverBottomUpVisitor {
+class FillInDefaultLoopDecreasesVisitor : ResolverBottomUpVisitor {
   readonly ICallable EnclosingMethod;
-  public FillInDefaultLoopDecreases_Visitor(ModuleResolver resolver, ICallable enclosingMethod)
+  public FillInDefaultLoopDecreasesVisitor(ModuleResolver resolver, ICallable enclosingMethod)
     : base(resolver) {
     Contract.Requires(resolver != null);
     Contract.Requires(enclosingMethod != null);

Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs → Source/DafnyCore/Resolver/FindFriendlyCallsVisitor.cs

@@ -4,10 +4,10 @@ namespace Microsoft.Dafny;
 
 public enum CallingPosition { Positive, Negative, Neither }
 
-class FindFriendlyCalls_Visitor : ResolverTopDownVisitor<CallingPosition> {
+class FindFriendlyCallsVisitor : ResolverTopDownVisitor<CallingPosition> {
   public readonly bool IsCoContext;
   public readonly bool ContinuityIsImportant;
-  public FindFriendlyCalls_Visitor(ErrorReporter reporter, bool co, bool continuityIsImportant)
+  public FindFriendlyCallsVisitor(ErrorReporter reporter, bool co, bool continuityIsImportant)
     : base(reporter) {
     Contract.Requires(reporter != null);
     this.IsCoContext = co;