Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix: Formatting on VSCode for multi-file projects with project file #4918

Merged
merged 7 commits into from
Jan 8, 2024
Merged

Fix: Formatting on VSCode for multi-file projects with project file #4918

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
274f26e
Fix: Formatting on VSCode and CLI
MikaelMayer Dec 27, 2023
8b95924
Formatting fix 2
MikaelMayer Dec 27, 2023
3fbe6d1
Needed to updated GeneratedFromDafny apparently
MikaelMayer Dec 27, 2023
733030c
Removed useless close
MikaelMayer Jan 8, 2024
39cbb3b
Split the PR
MikaelMayer Jan 8, 2024
b669fa1
Review comments
MikaelMayer Jan 8, 2024
fff8129
Merge branch 'master' into fixed-formatter
MikaelMayer Jan 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion Source/DafnyCore/AST/Grammar/IFileSystem.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,10 @@ private OnDiskFileSystem() {
}

public TextReader ReadFile(Uri uri) {
return new StreamReader(uri.LocalPath);
var reader = new StreamReader(uri.LocalPath);
var str = reader.ReadToEnd();
reader.Close();
return new StringReader(str);
Copy link
Member

@keyboardDrummer keyboardDrummer Jan 2, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not OK for performance reasons. We need to design our code towards parsing in a streaming fashion. Could you take this part out for now so we can fix #4836 ASAP?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I usually worry more about correctness than performance, but I think I might find something that suits both of our needs and I'll put it up in a separate PR.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was about to write a StreamReader that auto-closes the file it reads when done, since I haven't found any. However, after analzying the code further, I don't think it is necessary.

Here is an analysis to consider:

  • IFileSystem.cs:50 public TextReader ReadFile(Uri uri) { is called by
    • DafnyProject.cs:53 which has a ReadToEndAsync but does not closes the stream
    • IFileSystem.cs:25 public TextReader ReadFile(Uri uri) { which has the same usage as its parents
    • LanguageServerFileSystem.cs:41 existingText = OnDiskFileSystem.Instance.ReadFile(uri).ReadToEnd(); which reads to the end but does not closes the stream
    • LanguageServerFileSystem:92 which has the same usage as its parents
    • DafnyFile.cs:96 store the call as a closure in the GetContent of a field of a DafnyFile. This field is read in different places:
      • DafnyConsolePrinter.cs:72 var reader = file.GetContent(); lines = Util.Lines(reader).ToList();`. Similarly, we read to the end to get all the lines but it does not close the stream
      • ProgramParser.cs:269 var text = SourcePreprocessor.ProcessDirectives(getReader(), new List<string>()); which returns a source file after preprocessing. as a single string, but does not close the stream
      • CoverageReporter.cs:321 var source = dafnyFile.GetContent().ReadToEnd(); reads to the end but does not close the stream
      • FormatCommand.cs:75 using var content = dafnyFile.GetContent(); var originalText = await content.ReadToEndAsync(); This one also reads to the end and close the stream appropriately (I don't remember doing that, probably you did when you migrate to the new file system, so thanks)

In short, we currently never rely on streaming files and just forget to close it in almost every place. C# does perform auto-closing but is lazy and for big files it won't do it fast enough, which crashes the formatter on the command-line randomly.
So my recommandation is just to do this read and close it immediately so that it becomes possible to write after read. I'll create a separate PR for that.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#4950

Copy link
Member

@keyboardDrummer keyboardDrummer Jan 8, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

DafnyProject.cs:53 which has a ReadToEndAsync but does not closes the stream

What makes you say it does not close the stream? It uses a using directive:

using var textReader = fileSystem.ReadFile(uri);

Regarding the rest of the list, good finds! Let's fix them.

}

public bool Exists(Uri path) {
Expand Down
7 changes: 5 additions & 2 deletions Source/DafnyCore/AST/Grammar/IndentationFormatter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,11 +23,14 @@ public IndentationFormatter(TokenNewIndentCollector formatter) {
/// Creates an IndentationFormatter for the given program,
/// by immediately processing all nodes and assigning indentations to most structural tokens
/// </summary>
public static IndentationFormatter ForProgram(Program program, bool reduceBlockiness = true) {
var tokenNewIndentCollector = new TokenNewIndentCollector(program) {
public static IndentationFormatter ForProgram(Program program, Uri uri, bool reduceBlockiness = true) {
var tokenNewIndentCollector = new TokenNewIndentCollector(program, uri) {
ReduceBlockiness = reduceBlockiness
};
foreach (var child in program.DefaultModuleDef.PreResolveChildren) {
if (child.Tok.line != 0 && child.Tok.Uri != uri) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

child.Tok.line != 0 what is the meaning of this check? Could you assign the expression to a variable to clarify?

continue;
}
if (child is TopLevelDecl topLevelDecl) {
tokenNewIndentCollector.SetDeclIndentation(topLevelDecl, 0);
} else if (child is Include include) {
Expand Down
6 changes: 4 additions & 2 deletions Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,8 +83,9 @@ private Indentations PosToIndentations(int pos) {
public int binOpIndent = -1;
public int binOpArgIndent = -1;

internal TokenNewIndentCollector(Program program) {
internal TokenNewIndentCollector(Program program, Uri uri) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What uri is this? My impression is that you want to format one file at a time, which is fine, but let's make that explicit by renaming uri to fileToFormat

this.program = program;
this.uri = uri;
preResolve = true;
}

Expand Down Expand Up @@ -222,6 +223,7 @@ public int GetRightAlignIndentAfter(IToken token, int indentFallback) {
}

private static readonly Regex FollowedByNewlineRegex = new Regex("^[ \t]*([\r\n]|//)");
private readonly Uri uri;

public static bool IsFollowedByNewline(IToken token) {
return FollowedByNewlineRegex.IsMatch(token.TrailingTrivia);
Expand All @@ -231,7 +233,7 @@ public static bool IsFollowedByNewline(IToken token) {
// 'inline' is the hypothetical indentation of this token if it was on its own line
// 'below' is the hypothetical indentation of a comment after that token, and of the next token if it does not have a set indentation
public void SetIndentations(IToken token, int above = -1, int inline = -1, int below = -1) {
if (token.FromIncludeDirective(program) || (token.line == 0 && token.col == 0)) {
if (token.Uri != uri || (token.line == 0 && token.col == 0)) {
// Just ignore this token.
return;
}
Expand Down
15 changes: 6 additions & 9 deletions Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,12 @@ module {:extern "DCOMP"} DCOMP {
}

function replaceDots(i: string): string {
if |i| == 0 then (
""
) else (
if i[0] == '.' then (
"_" + replaceDots(i[1..])
) else (
[i[0]] + replaceDots(i[1..])
)
)
if |i| == 0 then
""
else if i[0] == '.' then
"_" + replaceDots(i[1..])
else
[i[0]] + replaceDots(i[1..])
}

function escapeIdent(i: string): string {
Expand Down
24 changes: 11 additions & 13 deletions Source/DafnyCore/GeneratedFromDafny.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5471,18 +5471,16 @@ public partial class __default {
TAIL_CALL_START:;
if ((new BigInteger((i).Count)).Sign == 0) {
return Dafny.Sequence<Dafny.Rune>.Concat(__accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
} else if (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('.'))) {
__accumulator = Dafny.Sequence<Dafny.Rune>.Concat(__accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_"));
Dafny.ISequence<Dafny.Rune> _in0 = (i).Drop(BigInteger.One);
i = _in0;
goto TAIL_CALL_START;
} else {
if (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('.'))) {
__accumulator = Dafny.Sequence<Dafny.Rune>.Concat(__accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_"));
Dafny.ISequence<Dafny.Rune> _in0 = (i).Drop(BigInteger.One);
i = _in0;
goto TAIL_CALL_START;
} else {
__accumulator = Dafny.Sequence<Dafny.Rune>.Concat(__accumulator, Dafny.Sequence<Dafny.Rune>.FromElements((i).Select(BigInteger.Zero)));
Dafny.ISequence<Dafny.Rune> _in1 = (i).Drop(BigInteger.One);
i = _in1;
goto TAIL_CALL_START;
}
__accumulator = Dafny.Sequence<Dafny.Rune>.Concat(__accumulator, Dafny.Sequence<Dafny.Rune>.FromElements((i).Select(BigInteger.Zero)));
Dafny.ISequence<Dafny.Rune> _in1 = (i).Drop(BigInteger.One);
i = _in1;
goto TAIL_CALL_START;
}
}
public static Dafny.ISequence<Dafny.Rune> escapeIdent(Dafny.ISequence<Dafny.Rune> i) {
Expand Down Expand Up @@ -7978,7 +7976,7 @@ public static void GenExpr(DAST._IExpression e, DAST._IOptional<Dafny.ISequence<
goto after__ASSIGN_SUCH_THAT_0;
}
}
throw new System.Exception("assign-such-that search produced no value (line 1242)");
throw new System.Exception("assign-such-that search produced no value (line 1239)");
after__ASSIGN_SUCH_THAT_0:;
_648_allReadCloned = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(_648_allReadCloned, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("let ")), DCOMP.__default.escapeIdent(_649_next)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" = ")), DCOMP.__default.escapeIdent(_649_next)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(".clone();\n"));
_647_recIdents = Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Difference(_647_recIdents, Dafny.Set<Dafny.ISequence<Dafny.Rune>>.FromElements(_649_next));
Expand Down Expand Up @@ -17385,7 +17383,7 @@ public static void GenExpr(DAST._IExpression e, DAST._IOptional<Dafny.ISequence<
goto after__ASSIGN_SUCH_THAT_1;
}
}
throw new System.Exception("assign-such-that search produced no value (line 1933)");
throw new System.Exception("assign-such-that search produced no value (line 1930)");
after__ASSIGN_SUCH_THAT_1:;
if ((!object.Equals(selfIdent, DAST.Optional<Dafny.ISequence<Dafny.Rune>>.create_None())) && ((_2912_next).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_this")))) {
if (!object.Equals(selfIdent, DAST.Optional<Dafny.ISequence<Dafny.Rune>>.create_None())) {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyDriver/Commands/FormatCommand.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ public static async Task<ExitValue> DoFormatting(DafnyOptions options) {
var result = originalText;
if (firstToken != null) {
result = Formatting.__default.ReindentProgramFromFirstToken(firstToken,
IndentationFormatter.ForProgram(dafnyProgram));
IndentationFormatter.ForProgram(dafnyProgram, file.Uri));
if (result != originalText) {
neededFormatting += 1;
if (doCheck) {
Expand Down
1 change: 1 addition & 0 deletions Source/DafnyDriver/CompilerDriver.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -596,6 +596,7 @@ public static void WriteFile(string filename, string text, string moreText = nul
if (moreText != null) {
target.Write(moreText);
}
target.Close();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does the above using directive not already guarantee that target is closed? This line seems obsolete.

}

private static void CheckFilenameIsLegal(string filename) {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyLanguageServer/Workspace/Compilation.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -428,7 +428,7 @@ public void CancelPendingUpdates() {
firstToken = firstToken.Prev;
}
var result = Formatting.__default.ReindentProgramFromFirstToken(firstToken,
IndentationFormatter.ForProgram(program));
IndentationFormatter.ForProgram(program, firstToken.Uri));

var lastToken = firstToken;
while (lastToken.Next != null) {
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyPipeline.Test/FormatterBaseTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString

var reprinted = firstToken != null && firstToken.line > 0
? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
: programString;
EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram);
if (expectedProgram != reprinted) {
Expand All @@ -100,7 +100,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
});
var reprintedCloned = firstToken != null && firstToken.line > 0
? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
: programString;
EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram);
if (expectedProgram != reprintedCloned) {
Expand All @@ -112,7 +112,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
DafnyMain.Resolve(dafnyProgram);
reprinted = firstToken != null && firstToken.line > 0
? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
: programString;
if (expectedProgram != reprinted) {
options.ErrorWriter.WriteLine("Formatting after resolution generates an error:");
Expand All @@ -131,7 +131,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString
firstToken = dafnyProgram.GetFirstTokenForUri(uri);
var reprinted2 = firstToken != null && firstToken.line > 0
? Formatting.__default.ReindentProgramFromFirstToken(firstToken,
IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness))
IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness))
: reprinted;
if (reprinted != reprinted2) {
Console.Write("Double formatting is not stable:\n");
Expand Down
Loading