Fix bug that occurred when using resolution caching and replaceable m…

…odules (#5189)

Fixes #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>

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() {

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;

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

Source/DafnyLanguageServer/DafnyLanguageServer.cs

@@ -57,16 +57,16 @@ 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}";
  }
 
  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;
  }