From d29e2349cd280e7920249df9f2a38dd6aa421c69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <MikaelMayer@users.noreply.github.com>
Date: Mon, 8 Jan 2024 10:26:58 -0600
Subject: [PATCH] Fix: Formatting on the command line works again (#4950)

This PR makes sure StreamReaders are closed after use, which prevented
formatting from overwriting the files randomly. The reason why to do
this despite an obvious memory increase is that in [all places where we
use this
StreamReader](https://github.com/dafny-lang/dafny/pull/4918#discussion_r1444530522),
we actually already read to the end and don't make use of the streaming.

Before, the "dafny format" command was throwing exceptions on large
files, and now it no longer throws an exception (test added for that)

Even better, this solved the issue that when I create a blank Dafny file
and try to save it, it used to complain with "Failed to save
'todelete.dfy': Unable to write file". (Fixes
https://github.com/dafny-lang/ide-vscode/issues/452)

<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/DafnyConsolePrinter.cs       |  2 +-
 .../DafnyDriver.Test/FormatterCommandTest.cs  | 65 +++++++++++++++++++
 Source/DafnyDriver/Commands/FormatCommand.cs  |  5 +-
 .../Workspace/LanguageServerFilesystem.cs     |  3 +-
 Source/DafnyPipeline.Test/FormatterIssues.cs  |  4 +-
 5 files changed, 74 insertions(+), 5 deletions(-)
 create mode 100644 Source/DafnyDriver.Test/FormatterCommandTest.cs

diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs
index 36bb9f2151..8a22e60103 100644
--- a/Source/DafnyCore/DafnyConsolePrinter.cs
+++ b/Source/DafnyCore/DafnyConsolePrinter.cs
@@ -69,7 +69,7 @@ private string GetFileLine(Uri uri, int lineIndex) {
         // Note: This is not guaranteed to be the same file that Dafny parsed. To ensure that, Dafny should keep
         // an in-memory version of each file it parses.
         var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken);
-        var reader = file.GetContent();
+        using var reader = file.GetContent();
         lines = Util.Lines(reader).ToList();
       } catch (Exception) {
         lines = new List<string>();
diff --git a/Source/DafnyDriver.Test/FormatterCommandTest.cs b/Source/DafnyDriver.Test/FormatterCommandTest.cs
new file mode 100644
index 0000000000..cd3ae0260a
--- /dev/null
+++ b/Source/DafnyDriver.Test/FormatterCommandTest.cs
@@ -0,0 +1,65 @@
+using System.Diagnostics;
+using System.IO.Pipelines;
+using System.Reactive.Concurrency;
+using System.Reflection;
+using System.Text;
+using Microsoft.Dafny;
+using Microsoft.Extensions.Logging.Abstractions;
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.JsonRpc.Client;
+using OmniSharp.Extensions.JsonRpc.Serialization;
+using OmniSharp.Extensions.LanguageServer.Protocol.Client.Capabilities;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+
+namespace DafnyDriver.Test;
+
+public class FormatterCommandTest {
+  [Fact]
+  public async Task GitIssueVSCode452FormattingWorksOnBigFiles() {
+    // We write to a temporary file
+    var oneSource = (int i) => $@"function Test{i}(x: int): int
+// This returns {i} if x is greater than 20
+{{
+  if x < 10 then
+                  0
+                  else if x < 20 then
+                                       1
+                                          else {i}
+}}
+
+";
+
+    var oneSourceFormatted = (int i) => $@"function Test{i}(x: int): int
+  // This returns {i} if x is greater than 20
+{{
+  if x < 10 then
+    0
+  else if x < 20 then
+    1
+  else {i}
+}}
+
+";
+    var source = "";
+    var sourceFormatted = "";
+    for (var i = 0; i < 1000; i++) {
+      source += oneSource(i);
+      sourceFormatted += oneSourceFormatted(i);
+    }
+
+    var file = Path.GetTempFileName() + ".dfy";
+
+    await File.WriteAllTextAsync(file, source);
+    StringWriter strWriter = new StringWriter();
+    var options = DafnyOptions.Create(strWriter, null,
+      file
+      );
+
+    var exitValue = await FormatCommand.DoFormatting(options);
+    Assert.Equal(0, (int)exitValue);
+
+    var result = await File.ReadAllTextAsync(file);
+    Assert.Equal(sourceFormatted, result);
+    File.Delete(file);
+  }
+}
diff --git a/Source/DafnyDriver/Commands/FormatCommand.cs b/Source/DafnyDriver/Commands/FormatCommand.cs
index 7782a1aa78..62ba02ef9e 100644
--- a/Source/DafnyDriver/Commands/FormatCommand.cs
+++ b/Source/DafnyDriver/Commands/FormatCommand.cs
@@ -9,7 +9,7 @@
 
 namespace Microsoft.Dafny;
 
-static class FormatCommand {
+public static class FormatCommand {
 
   public static IEnumerable<Option> Options => DafnyCommands.FormatOptions;
 
@@ -72,8 +72,9 @@ public static async Task<ExitValue> DoFormatting(DafnyOptions options) {
           OnDiskFileSystem.Instance, options, new Uri(tempFileName), Token.NoToken);
       }
 
-      using var content = dafnyFile.GetContent();
+      var content = dafnyFile.GetContent();
       var originalText = await content.ReadToEndAsync();
+      content.Close(); // Manual closing because we want to overwrite
       dafnyFile.GetContent = () => new StringReader(originalText);
       // Might not be totally optimized but let's do that for now
       var err = DafnyMain.Parse(new List<DafnyFile> { dafnyFile }, programName, options, out var dafnyProgram);
diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs
index 03fdcab515..a545ba4197 100644
--- a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs
+++ b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs
@@ -38,7 +38,8 @@ public bool OpenDocument(TextDocumentItem document) {
     string existingText = "";
     try {
       if (OnDiskFileSystem.Instance.Exists(uri)) {
-        existingText = OnDiskFileSystem.Instance.ReadFile(uri).ReadToEnd();
+        using var fileStream = OnDiskFileSystem.Instance.ReadFile(uri);
+        existingText = fileStream.ReadToEnd();
       }
     } catch (IOException) {
       // If we don't manage to detect whether this document already existed ond disc,
diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs
index 7cfd8e3a5f..18bad05f7c 100644
--- a/Source/DafnyPipeline.Test/FormatterIssues.cs
+++ b/Source/DafnyPipeline.Test/FormatterIssues.cs
@@ -1,4 +1,6 @@
-using JetBrains.Annotations;
+using System;
+using System.IO;
+using JetBrains.Annotations;
 using Xunit;
 using Xunit.Abstractions;