Merge branch 'fix-4823-general-traits-bug-extends' of https://github.…

…com/dafny-lang/dafny into fix-4823-general-traits-bug-extends

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");

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<bool>() || (Contract.ValueAtReturn(out qualification) == null && Contract.ValueAtReturn(out name) == null));
-    // ensures result==true ==> qualification != null ==> name != null
-    Contract.Ensures(!Contract.Result<bool>() || 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;
 

Source/DafnyCore/Compilers/DafnyExecutableBackend.cs

@@ -29,7 +29,7 @@ public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<str
   }
 
   public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
-    InstantiateReplaceableModules(dafnyProgram);
+    CheckInstantiationReplaceableModules(dafnyProgram);
     ProcessOuterModules(dafnyProgram);
     ((DafnyCompiler)compiler).Start();
     compiler.Compile(dafnyProgram, new ConcreteSyntaxTree());

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -30,26 +30,25 @@ protected ExecutableBackend(DafnyOptions options) : base(options) {
   public override string ModuleSeparator => 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} {{ ... }}`");
+        }
       }
     }
   }

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<bool>() || (Contract.ValueAtReturn(out qualification) == null && Contract.ValueAtReturn(out name) == null));
+    // ensures result==true ==> qualification != null ==> name != null
+    Contract.Ensures(!Contract.Result<bool>() || 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;
+  }
+}

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<Name> path, string tail = "") {
     Contract.Requires(path != null);
     Contract.Requires(0 <= i && i < path.Count);

Source/DafnyDriver/CompilerDriver.cs

@@ -500,7 +500,7 @@ public static async Task<bool> 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;

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

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

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
+}

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

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";
 }

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 { ... }`

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

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