From 4e7f7b325938d37d08de07d7f4d4f4e08acd12c3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 25 Mar 2024 17:34:56 +0100 Subject: [PATCH 1/2] Move the field replacement out of ModuleDefinition, to avoid caching issues (#5215) ### Description Move the field replacement out of ModuleDefinition, to avoid caching issues ### How has this been tested? Refactoring, no additional tests needed. 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). --- Source/DafnyCore/AST/Modules/ModuleDefinition.cs | 8 -------- Source/DafnyCore/AST/Program.cs | 5 +++++ Source/DafnyCore/Backends/ExecutableBackend.cs | 2 +- Source/DafnyCore/Resolver/ProgramResolver.cs | 13 ++++--------- 4 files changed, 10 insertions(+), 18 deletions(-) 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/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); } } } From 52bf16e4b487f131aa7d47f16b3fbefb68838a9d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 25 Mar 2024 18:44:46 +0100 Subject: [PATCH 2/2] Add axiom warnings for functions and methods when using the new resolver (#5216) ### Description Axiom warnings for functions and method were missing when using the new resolver. This PR adds them. ### How has this been tested? Switch one test for function axioms and one for method axioms to use the new resolver instead of the old one. 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). --- Source/DafnyCore/AST/Members/MethodOrFunction.cs | 4 ++++ Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs | 4 ++++ .../TestFiles/LitTests/LitTest/ast/function.dfy | 2 +- .../TestFiles/LitTests/LitTest/ast/method.dfy | 2 +- .../LitTests/LitTest/dafny0/TypeAdjustments.dfy.expect | 2 ++ .../LitTests/LitTest/git-issues/git-issue-4939a.dfy.expect | 1 + 6 files changed, 13 insertions(+), 2 deletions(-) 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/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/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