Merge branch 'master' into issue-2064

Source/DafnyCore/AST/Members/MethodOrFunction.cs

@@ -34,6 +34,10 @@ protected MethodOrFunction(Cloner cloner, MethodOrFunction original) : base(clon
   public bool IsAbstract => EnclosingClass.EnclosingModuleDefinition.ModuleKind != ModuleKindEnum.Concrete;
 
   public virtual void Resolve(ModuleResolver resolver) {
+    ResolveMethodOrFunction(resolver);
+  }
+
+  public void ResolveMethodOrFunction(INewOrOldResolver resolver) {
     if (Bodyless && !IsVirtual && !IsAbstract && !this.IsExtern(resolver.Options) && !this.IsExplicitAxiom()) {
       foreach (var ensures in Ens) {
         if (!ensures.IsExplicitAxiom() && !resolver.Options.Get(CommonOptionBag.AllowAxioms)) {

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -24,14 +24,6 @@ public enum ImplementationKind {
 public record Implements(ImplementationKind Kind, ModuleQualifiedId Target);
 
 public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
-
-  /// <summary>
-  /// If this is a placeholder module, code generation will look for a unique module that replaces this one,
-  /// and use it to set this field. 
-  /// </summary>
-  [FilledInDuringResolution]
-  public ModuleDefinition Replacement { get; set; }
-
   public IToken BodyStartTok = Token.NoToken;
   public IToken TokenWithTrailingDocString = Token.NoToken;
   public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code

Source/DafnyCore/AST/Program.cs

@@ -17,6 +17,11 @@ void ObjectInvariant() {
 
   public bool HasParseErrors { get; set; }
   public readonly string FullName;
+  /// <summary>
+  /// If this is a placeholder module, code generation will look for a unique module that replaces this one,
+  /// and use it to set this field. 
+  /// </summary>
+  public Dictionary<ModuleDefinition, ModuleDefinition> Replacements = new();
 
   // Resolution essentially flattens the module hierarchy, for
   // purposes of translation and compilation.

Source/DafnyCore/Backends/ExecutableBackend.cs

@@ -40,7 +40,7 @@ protected void CheckInstantiationReplaceableModules(Program dafnyProgram) {
         }
       }
 
-      if (compiledModule.ModuleKind == ModuleKindEnum.Replaceable && compiledModule.Replacement == null) {
+      if (compiledModule.ModuleKind == ModuleKindEnum.Replaceable && dafnyProgram.Replacements.GetValueOrDefault(compiledModule) == null) {
         if (compiledModule.ShouldCompile(dafnyProgram.Compilation)) {
           Reporter!.Error(MessageSource.Compiler, compiledModule.Tok,
             $"when producing executable code, replaceable modules must be replaced somewhere in the program. For example, `module {compiledModule.Name}Impl replaces {compiledModule.Name} {{ ... }}`");

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -1240,6 +1240,8 @@ void ResolveIterator(IteratorDecl iter) {
     void ResolveFunction(Function f) {
       Contract.Requires(f != null);
 
+      f.ResolveMethodOrFunction(this);
+
       // make note of the warnShadowing attribute
       bool warnShadowingOption = resolver.Options.WarnShadowing;  // save the original warnShadowing value
       bool warnShadowing = true;
@@ -1322,6 +1324,8 @@ void ResolveFunction(Function f) {
     void ResolveMethod(Method m) {
       Contract.Requires(m != null);
 
+      m.ResolveMethodOrFunction(this);
+
       try {
         currentMethod = m;
 

Source/DafnyCore/Resolver/ProgramResolver.cs

@@ -215,21 +215,16 @@ private void CheckDuplicateModuleNames(Program program) {
   }
 
   protected void InstantiateReplaceableModules(Program dafnyProgram) {
-    foreach (var compiledModule in dafnyProgram.Modules()) {
-      // This is a workaround for the problem that the IDE caches resolved modules,
-      // So this field might still be set from a previous compilation.
-      // Better solution is described here: https://github.com/dafny-lang/dafny/issues/5188
-      compiledModule.Replacement = null;
-    }
     foreach (var compiledModule in dafnyProgram.Modules().OrderByDescending(m => m.Height)) {
       if (compiledModule.Implements is { Kind: ImplementationKind.Replacement }) {
         var target = compiledModule.Implements.Target.Def;
-        if (target.Replacement != null) {
-          Reporter!.Error(MessageSource.Resolver, new NestedToken(compiledModule.Tok, target.Replacement.Tok,
+        var replacement = Program.Replacements.GetValueOrDefault(target);
+        if (replacement != null) {
+          Reporter!.Error(MessageSource.Resolver, new NestedToken(compiledModule.Tok, replacement.Tok,
               $"other replacing module"),
             "a replaceable module may only be replaced once");
         } else {
-          target.Replacement = compiledModule.Replacement ?? compiledModule;
+          Program.Replacements[target] = Program.Replacements.GetValueOrDefault(compiledModule, compiledModule);
         }
       }
     }

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --allow-axioms:false "%s" > "%t"
+// RUN: %verify --allow-axioms:false --type-system-refresh "%s" > "%t"
 // NONUNIFORM: warning will be the same for all back-end
 // RUN: ! %run --allow-axioms:false "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --allow-axioms:false "%s" > "%t"
+// RUN: %verify --allow-axioms:false --type-system-refresh "%s" > "%t"
 // NONUNIFORM: warning will be the same for all back-ends
 // RUN: ! %run --allow-axioms:false "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeAdjustments.dfy.expect

@@ -1,3 +1,5 @@
+TypeAdjustments.dfy(588,14): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
+TypeAdjustments.dfy(616,14): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 TypeAdjustments.dfy(23,13): Error: assertion might not hold
 TypeAdjustments.dfy(25,17): Error: assertion might not hold
 TypeAdjustments.dfy(27,13): Error: assertion might not hold

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

@@ -1,3 +1,4 @@
+git-issue-4939a.dfy(99,19): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 git-issue-4939a.dfy(142,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'T' can be constructed
 git-issue-4939a.dfy(144,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'Mutual' can be constructed
 git-issue-4939a.dfy(145,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nutual' can be constructed