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](#4918 (comment)),
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
dafny-lang/ide-vscode#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

@@ -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>();

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

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

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,

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;