diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 5e0fa12d746..933c86c1f6c 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -205,8 +205,8 @@ public string GetCompileName(DafnyOptions options) { return compileName; } - if (Replacement != null) { - return Replacement.GetCompileName(options); + if (Implements is { Kind: ImplementationKind.Replacement }) { + return Implements.Target.Def.GetCompileName(options); } var externArgs = options.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern"); diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index 0c6cc8e00db..9ce454af73d 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs @@ -115,38 +115,13 @@ public bool IsVisibleInScope(VisibilityScope scope) { public virtual string GetCompileName(DafnyOptions options) { if (compileName == null) { - IsExtern(options, out _, out compileName); + this.IsExtern(options, out _, out compileName); compileName ??= SanitizedName; } return compileName; } - public bool IsExtern(DafnyOptions options, out string/*?*/ qualification, out string/*?*/ name) { - // ensures result==false ==> qualification == null && name == null - Contract.Ensures(Contract.Result() || (Contract.ValueAtReturn(out qualification) == null && Contract.ValueAtReturn(out name) == null)); - // ensures result==true ==> qualification != null ==> name != null - Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out qualification) == null || Contract.ValueAtReturn(out name) != null); - - qualification = null; - name = null; - if (!options.DisallowExterns) { - var externArgs = Attributes.FindExpressions(this.Attributes, "extern"); - if (externArgs != null) { - if (externArgs.Count == 0) { - return true; - } else if (externArgs.Count == 1 && externArgs[0] is StringLiteralExpr) { - name = externArgs[0].AsStringLiteral(); - return true; - } else if (externArgs.Count == 2 && externArgs[0] is StringLiteralExpr && externArgs[1] is StringLiteralExpr) { - qualification = externArgs[0].AsStringLiteral(); - name = externArgs[1].AsStringLiteral(); - return true; - } - } - } - return false; - } public Attributes Attributes; // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict Attributes IAttributeBearingDeclaration.Attributes => Attributes; diff --git a/Source/DafnyCore/Compilers/DafnyExecutableBackend.cs b/Source/DafnyCore/Compilers/DafnyExecutableBackend.cs index d3eabeb6d9a..7791fee87ac 100644 --- a/Source/DafnyCore/Compilers/DafnyExecutableBackend.cs +++ b/Source/DafnyCore/Compilers/DafnyExecutableBackend.cs @@ -29,7 +29,7 @@ public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection Compiler.ModuleSeparator; public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) { - InstantiateReplaceableModules(dafnyProgram); + CheckInstantiationReplaceableModules(dafnyProgram); ProcessOuterModules(dafnyProgram); Compiler.Compile(dafnyProgram, output); } - protected void InstantiateReplaceableModules(Program dafnyProgram) { - foreach (var compiledModule in dafnyProgram.Modules().OrderByDescending(m => m.Height)) { + protected void CheckInstantiationReplaceableModules(Program dafnyProgram) { + foreach (var compiledModule in dafnyProgram.Modules()) { if (compiledModule.Implements is { Kind: ImplementationKind.Replacement }) { - var target = compiledModule.Implements.Target.Def; - if (target.Replacement != null) { - Reporter!.Error(MessageSource.Compiler, new NestedToken(compiledModule.Tok, target.Replacement.Tok, "Other replacing module:"), - "a replaceable module may only be replaced once"); - } else { - target.Replacement = compiledModule.Replacement ?? compiledModule; + if (compiledModule.IsExtern(Options, out _, out var name) && name != null) { + Reporter!.Error(MessageSource.Compiler, compiledModule.Tok, + "inside a module that replaces another, {:extern} attributes may only be used without arguments"); } } if (compiledModule.ModuleKind == ModuleKindEnum.Replaceable && compiledModule.Replacement == null) { - 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} {{ ... }}`"); + 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/Compilers/ExternExtensions.cs b/Source/DafnyCore/Compilers/ExternExtensions.cs new file mode 100644 index 00000000000..c13e7ba9461 --- /dev/null +++ b/Source/DafnyCore/Compilers/ExternExtensions.cs @@ -0,0 +1,32 @@ +using System.Diagnostics.Contracts; + +namespace Microsoft.Dafny; + +public static class ExternExtensions { + + public static bool IsExtern(this IAttributeBearingDeclaration declaration, DafnyOptions options, out string/*?*/ qualification, out string/*?*/ name) { + // ensures result==false ==> qualification == null && name == null + Contract.Ensures(Contract.Result() || (Contract.ValueAtReturn(out qualification) == null && Contract.ValueAtReturn(out name) == null)); + // ensures result==true ==> qualification != null ==> name != null + Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out qualification) == null || Contract.ValueAtReturn(out name) != null); + + qualification = null; + name = null; + if (!options.DisallowExterns) { + var externArgs = Attributes.FindExpressions(declaration.Attributes, "extern"); + if (externArgs != null) { + if (externArgs.Count == 0) { + return true; + } else if (externArgs.Count == 1 && externArgs[0] is StringLiteralExpr) { + name = externArgs[0].AsStringLiteral(); + return true; + } else if (externArgs.Count == 2 && externArgs[0] is StringLiteralExpr && externArgs[1] is StringLiteralExpr) { + qualification = externArgs[0].AsStringLiteral(); + name = externArgs[1].AsStringLiteral(); + return true; + } + } + } + return false; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/ProgramResolver.cs b/Source/DafnyCore/Resolver/ProgramResolver.cs index 08c1553df8d..82c3aa2aa27 100644 --- a/Source/DafnyCore/Resolver/ProgramResolver.cs +++ b/Source/DafnyCore/Resolver/ProgramResolver.cs @@ -76,6 +76,7 @@ public virtual void Resolve(CancellationToken cancellationToken) { Type.DisableScopes(); + InstantiateReplaceableModules(Program); CheckDuplicateModuleNames(Program); foreach (var rewriter in rewriters) { @@ -213,6 +214,20 @@ private void CheckDuplicateModuleNames(Program program) { } } + protected void InstantiateReplaceableModules(Program dafnyProgram) { + 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.Compiler, new NestedToken(compiledModule.Tok, target.Replacement.Tok, "Other replacing module:"), + "a replaceable module may only be replaced once"); + } else { + target.Replacement = compiledModule.Replacement ?? compiledModule; + } + } + } + } + public static string ModuleNotFoundErrorMessage(int i, List path, string tail = "") { Contract.Requires(path != null); Contract.Requires(0 <= i && i < path.Count); diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs index 5a945cf6b45..c5fb9f530a3 100644 --- a/Source/DafnyDriver/CompilerDriver.cs +++ b/Source/DafnyDriver/CompilerDriver.cs @@ -500,7 +500,7 @@ public static async Task CompileDafnyProgram(Program dafnyProgram, string var compiler = options.Backend; - var hasMain = Compilers.SinglePassCompiler.HasMain(dafnyProgram, out var mainMethod); + var hasMain = SinglePassCompiler.HasMain(dafnyProgram, out var mainMethod); if (hasMain) { mainMethod.IsEntryPoint = true; dafnyProgram.MainMethod = mainMethod; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy index f684d7b8847..8db03749686 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy @@ -1,5 +1,7 @@ -// RUN: %baredafny run %args %s --target=java --build=%S/Build/build --input %S/Inputs/wrappers.dfy --input %S/Inputs/random.dfy --input %S/Inputs/randomJava.dfy --input %S/Inputs/Interop/__default.java > "%t" -// RUN: %baredafny run %args %s --build=%S/Build/build --input %S/Inputs/wrappers.dfy --input %S/Inputs/random.dfy --input %S/Inputs/randomCSharp.dfy --input %S/Inputs/Interop.cs >> "%t" +// RUN: %build --target=lib --output=%S/Build1/build %S/Inputs/wrappers.dfy %S/Inputs/random.dfy > "%t" +// RUN: %build --target=cs --output=%S/Build1/build %S/Build1/build.doo %S/Inputs/randomCSharp.dfy %S/Inputs/Interop.cs >> "%t" +// RUN: %run %s --input %S/Build1/build.dll --target=cs --build=%S/Build2 --library=%S/Build1/build.doo >> "%t" +// RUN: %baredafny run %args %s --target=java --build=%S/Build/build --input %S/Inputs/wrappers.dfy --input %S/Inputs/random.dfy --input %S/Inputs/randomJava.dfy --input %S/Inputs/Interop/__default.java >> "%t" // RUN: %diff "%s.expect" "%t" // Test can fail non-deterministically by design, but the chance is ~10^-30 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy.expect index e6bbead8def..de552a546bc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/user.dfy.expect @@ -1,4 +1,8 @@ -Dafny program verifier finished with 10 verified, 0 errors +Dafny program verifier finished with 4 verified, 0 errors + +Dafny program verifier finished with 5 verified, 0 errors + +Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier finished with 10 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/externErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/externErrors.dfy new file mode 100644 index 00000000000..d8d42c17871 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/externErrors.dfy @@ -0,0 +1,23 @@ +// RUN: ! %run %s > %t +// RUN: %diff "%s.expect" "%t" + +replaceable module {:extern "FooNameOverride"} Foo { + method {:extern "ZazOverride1"} Zaz() returns (i: int) + ensures i >= 2 +} + +module {:extern "BarNameOverride1"} TwoErrors replaces Foo { + // missing error on BarNameOverride2 + method {:extern "BarNameOverride2", "ZazOverride2"} Zaz() returns (i: int) + ensures i >= 2 +} + +replaceable module {:extern "FaaNameOverride"} Faa { + method {:extern "ZazOverride1"} Zaz() returns (i: int) + ensures i >= 2 +} + +module {:extern} NoErrors replaces Faa { + method {:extern "ZazOverride2"} Zaz() returns (i: int) + ensures i >= 2 +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/externErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/externErrors.dfy.expect new file mode 100644 index 00000000000..112e598c5f9 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/externErrors.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 0 verified, 0 errors +externErrors.dfy(9,36): Error: inside a module that replaces another, {:extern} attributes may only be used without arguments diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy index e1f310ab044..0b78faade28 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy @@ -6,32 +6,7 @@ replaceable module NeverReplaced { ensures i >= 2 } -replaceable module ReplacedThrice { - method Foo() returns (i: int) - ensures i >= 2 -} - -module Replace1 replaces ReplacedThrice { - method Foo() returns (i: int) { - return 3; - } -} - -module Replace2 replaces ReplacedThrice { - method Foo() returns (i: int) { - return 3; - } -} - -module Replace3 replaces ReplacedThrice { - method Foo() returns (i: int) { - return 3; - } -} - method Main() { var x := NeverReplaced.Foo(); print x, "\n"; - var y := ReplacedThrice.Foo(); - print y, "\n"; } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy.expect index e87a90f1898..54dedfe1ab8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableExecutionErrors.dfy.expect @@ -1,5 +1,3 @@ -Dafny program verifier finished with 4 verified, 0 errors -replaceableExecutionErrors.dfy(20,7): Error: a replaceable module may only be replaced once Other replacing module: replaceableExecutionErrors.dfy(26,7) -replaceableExecutionErrors.dfy(14,7): Error: a replaceable module may only be replaced once Other replacing module: replaceableExecutionErrors.dfy(26,7) +Dafny program verifier finished with 1 verified, 0 errors replaceableExecutionErrors.dfy(4,19): Error: when producing executable code, replaceable modules must be replaced somewhere in the program. For example, `module NeverReplacedImpl replaces NeverReplaced { ... }` diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/resolveManyReplacement.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/resolveManyReplacement.dfy index 083bb28573b..5e8d4e1de0b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/resolveManyReplacement.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/resolveManyReplacement.dfy @@ -1,5 +1,7 @@ -// RUN: %resolve %s +// RUN: ! %resolve %s > %t +// RUN: %diff "%s.expect" "%t" +// Currently this creates a resolution error. replaceable module FooModule { method Foo() returns (i: int) ensures i >= 2 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/resolveManyReplacement.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/resolveManyReplacement.dfy.expect new file mode 100644 index 00000000000..16efd7c4e31 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/resolveManyReplacement.dfy.expect @@ -0,0 +1,3 @@ +resolveManyReplacement.dfy(10,7): Error: a replaceable module may only be replaced once Other replacing module: resolveManyReplacement.dfy(15,7) +resolveManyReplacement.dfy(15,7): Error: modules 'Replacement1' and 'Replacement2' both have CompileName 'FooModule' +2 resolution/type errors detected in resolveManyReplacement.dfy