From b144df247ef09915ac7407cd1880df9a87915a86 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 13 Mar 2024 22:18:06 +0100
Subject: [PATCH] Fix bug that occurred when using resolution caching and
 replaceable modules (#5189)

Fixes https://github.com/dafny-lang/dafny/issues/5187

### Description
Fix bug that occurred when using resolution caching in combination with
replaceable modules

### How has this been tested?
Added a language server test

<small>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).</small>
---
 .../AST/Modules/ModuleQualifiedId.cs          |  4 ++-
 Source/DafnyCore/Resolver/ProgramResolver.cs  |  6 ++++
 .../ProjectFiles/StandardLibrary.cs           | 34 +++++++++++++++++++
 .../DafnyLanguageServer.cs                    |  6 ++--
 4 files changed, 46 insertions(+), 4 deletions(-)
 create mode 100644 Source/DafnyLanguageServer.Test/ProjectFiles/StandardLibrary.cs

diff --git a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs
index dbda0218a5f..e71f8955e01 100644
--- a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs
+++ b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs
@@ -28,7 +28,9 @@ public ModuleQualifiedId(List<Name> path) {
 
   public ModuleQualifiedId(Cloner cloner, ModuleQualifiedId original) {
     Path = original.Path.Select(n => n.Clone(cloner)).ToList();
-    Root = original.Root;
+    if (cloner.CloneResolvedFields) {
+      Root = original.Root;
+    }
   }
 
   public string RootName() {
diff --git a/Source/DafnyCore/Resolver/ProgramResolver.cs b/Source/DafnyCore/Resolver/ProgramResolver.cs
index 171beffdbfe..7b17e32b356 100644
--- a/Source/DafnyCore/Resolver/ProgramResolver.cs
+++ b/Source/DafnyCore/Resolver/ProgramResolver.cs
@@ -215,6 +215,12 @@ 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;
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/StandardLibrary.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/StandardLibrary.cs
new file mode 100644
index 00000000000..77bddd23f08
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/StandardLibrary.cs
@@ -0,0 +1,34 @@
+using System.IO;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles;
+
+public class StandardLibrary : ClientBasedLanguageServerTest {
+
+  [Fact]
+  public async Task EditWhenUsingStandardLibrary() {
+    var projectFile = @"
+[options]
+standard-libraries=true
+";
+    var program = @"
+method Foo() ensures false { }
+".TrimStart();
+    var path = Path.GetRandomFileName();
+    var project = CreateAndOpenTestDocument(projectFile, Path.Combine(path, DafnyProject.FileName));
+    var document = CreateAndOpenTestDocument(program, Path.Combine(path, "EditWhenUsingStandardLibrary.dfy"));
+    var diagnostics1 = await GetLastDiagnostics(document);
+    Assert.Single(diagnostics1);
+    ApplyChange(ref document, new Range(0, 0, 1, 0), "method Bar() ensures true { }");
+    var diagnostics2 = await GetLastDiagnostics(document);
+    Assert.Empty(diagnostics2);
+  }
+
+  public StandardLibrary(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) {
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
index 0ef3ba91dff..0753c9cfcec 100644
--- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs
+++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
@@ -57,7 +57,7 @@ private static void PublishSolverPath(ILanguageServer server) {
         var proverOptions = new SMTLibSolverOptions(options);
         proverOptions.Parse(options.ProverOptions);
         solverPath = proverOptions.ExecutablePath();
-        HandleZ3Version(telemetryPublisher, proverOptions);
+        HandleZ3Version(telemetryPublisher, solverPath);
       } catch (Exception e) {
         solverPath = $"Error while determining solver path: {e}";
       }
@@ -65,8 +65,8 @@ private static void PublishSolverPath(ILanguageServer server) {
       telemetryPublisher.PublishSolverPath(solverPath);
     }
 
-    private static void HandleZ3Version(TelemetryPublisherBase telemetryPublisher, SMTLibSolverOptions proverOptions) {
-      var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
+    private static void HandleZ3Version(TelemetryPublisherBase telemetryPublisher, string solverPath) {
+      var z3Version = DafnyOptions.GetZ3Version(solverPath);
       if (z3Version is null) {
         return;
       }