diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs index ee2273d7d31..701c0c6b2a1 100644 --- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs +++ b/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)) { diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 1376e0e7721..7a0514e757b 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/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, IHasSymbolChildren { - - /// - /// 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. - /// - [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 diff --git a/Source/DafnyCore/AST/Program.cs b/Source/DafnyCore/AST/Program.cs index 935290cce88..b4f897463a4 100644 --- a/Source/DafnyCore/AST/Program.cs +++ b/Source/DafnyCore/AST/Program.cs @@ -17,6 +17,11 @@ void ObjectInvariant() { public bool HasParseErrors { get; set; } public readonly string FullName; + /// + /// 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. + /// + public Dictionary Replacements = new(); // Resolution essentially flattens the module hierarchy, for // purposes of translation and compilation. diff --git a/Source/DafnyCore/Backends/ExecutableBackend.cs b/Source/DafnyCore/Backends/ExecutableBackend.cs index add4996feac..cd4c50a8a1a 100644 --- a/Source/DafnyCore/Backends/ExecutableBackend.cs +++ b/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} {{ ... }}`"); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index 2956b8f13a5..cf612d72747 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/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; diff --git a/Source/DafnyCore/Resolver/ProgramResolver.cs b/Source/DafnyCore/Resolver/ProgramResolver.cs index 7b17e32b356..8f8394db6d2 100644 --- a/Source/DafnyCore/Resolver/ProgramResolver.cs +++ b/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); } } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy index a3f16c3fff1..75137a203d4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy +++ b/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" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy index 9645bedff93..bebce60ecc4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy +++ b/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" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeAdjustments.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeAdjustments.dfy.expect index 9afaa65350b..0bf0ef5cd57 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeAdjustments.dfy.expect +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy.expect index fb1f3181df7..5ec3e0aa53f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy.expect +++ b/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