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 4287 gutter highlight before project pr #4308

Merged
merged 4 commits into from
Jul 20, 2023
Merged

Fix 4287 gutter highlight before project pr #4308

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3bbabae
Fix: 4287 - Made gutter icons more robust
MikaelMayer Jul 19, 2023
46abd6e
Poke CI
robin-aws Jul 19, 2023
bbbabc3
Whitespace
robin-aws Jul 19, 2023
18257ce
PR feedback
robin-aws Jul 20, 2023
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
6 changes: 3 additions & 3 deletions Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ public class CachedLinearVerificationGutterStatusTester : LinearVerificationGutt

// To add a new test, just call VerifyTrace on a given program,
// the test will fail and give the correct output that can be use for the test
// Add '//Next<n>:' to edit a line multiple times
// Add '//Replace<n>:' to edit a line multiple times

[Fact(Timeout = MaxTestExecutionTimeMs)]
public async Task EnsureCachingDoesNotMakeSquigglyLinesToRemain() {
Expand All @@ -24,7 +24,7 @@ await SetUp(options => {
await VerifyTrace(@"
. S S | I $ | :method test() {
. S | | I $ | : assert true;
. S S | I $ | : //Next:
. S S | I $ | : //Replace:
. S S | I $ | :}");
}

Expand All @@ -38,7 +38,7 @@ await VerifyTrace(@"
. S [S][ ][I][S][S][ ]:method test() {
. S [O][O][o][Q][O][O]: assert true;
. S [=][=][-][~][=][=]: assert false;
. S [S][ ][I][S][S][ ]: //Next:
. S [S][ ][I][S][S][ ]: //Replace:
. S [S][ ][I][S][S][ ]:}");
}

Expand Down
2 changes: 1 addition & 1 deletion ...e/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ public async Task EnsuresManyDocumentsCanBeVerifiedAtOnce() {
| | | I | | :
. S [S][ ][I][S][ ]:method H()
. S [=][=][-][~][O]: ensures F(1)
. S [=][=][-][~][=]:{//Next: { assert false;
. S [=][=][-][~][=]:{//Replace: { assert false;
. S [S][ ][I][S][ ]:}", $"testfile{i}.dfy", true, true, verificationStatusGutterReceivers[i]));
}

Expand Down
104 changes: 74 additions & 30 deletions Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,21 +67,37 @@ private static bool IsNotIndicatingProgress(LineVerificationStatus status) {
status != LineVerificationStatus.AssertionVerifiedInErrorContextObsolete &&
status != LineVerificationStatus.AssertionVerifiedInErrorContextVerifying;
}
public static string RenderTrace(List<LineVerificationStatus[]> statusesTrace, string code) {
public static string RenderTrace(List<LineVerificationStatus[]> statusesTrace, List<string> codes) {
var code = codes[0];
var codeLines = new Regex("\r?\n").Split(code);
var maxLines = codeLines.Length;
foreach (var trace in statusesTrace) {
if (maxLines < trace.Length) {
maxLines = trace.Length;
}
}
foreach (var intermediateCode in codes) {
var intermediateCodeLines = new Regex("\r?\n").Split(intermediateCode).Length;
if (maxLines < intermediateCodeLines) {
maxLines = intermediateCodeLines;
}
}
var renderedCode = "";
for (var line = 0; line < codeLines.Length; line++) {
for (var line = 0; line < maxLines; line++) {
if (line != 0) {
renderedCode += "\n";
}
foreach (var statusTrace in statusesTrace) {
renderedCode += LineVerificationStatusToString[statusTrace[line]];
if (line >= statusTrace.Length) {
renderedCode += "###";
} else {
renderedCode += LineVerificationStatusToString[statusTrace[line]];
}
}

renderedCode += ":";
renderedCode += codeLines[line];
renderedCode += line < codeLines.Length ? codeLines[line] : "";
}
Assert.All(statusesTrace, trace => Assert.Equal(codeLines.Length, trace.Length));

return renderedCode;
}
Expand Down Expand Up @@ -165,26 +181,30 @@ private static bool NoMoreNotificationsToAwaitFrom(VerificationStatusGutter veri
/// <summary>
/// Given some code, will emit the edit like this:
/// ```
/// sentence //Next1:sentence2 //Next2:sentence3
/// ^^^^^^^^^^^^^^^^^ remove
/// sentence //Replace1:This is a \nsentence2 //Replace2:sentence3 with \\n character
/// ^^^remove^^^^^^^^^^^ ^^ replace with newline ^^ replace with \
/// ```
/// ```
/// sentence //Next1:\nsentence2 //Next2:sentence3
/// ^^^^^^^^^^^^^^^^^^^ replace with newline
/// sentence //Insert1:This is a \nsentence2 //Replace2:sentence3 with \\n character
/// ^^^remove^ ^^ replace with newline ^^ replace with \
/// ```
/// ```
/// sentence //Remove1:sentence2 //Next2:sentence3
/// ^^^^^^^^^^^^^^^^^^^ remove, including the newline before sentence if any
/// sentence //Remove1:sentence2 //Replace2:sentence3
/// ^^^^^^^^^^^^^^^^^^^ Same as Replace, but will remove also the newline before
/// ```
/// </summary>
/// <param name="code">The original code with the //Next: comments or //NextN:</param>
/// <param name="code">The original code with the //Replace: comments or //ReplaceN:</param>
/// <returns></returns>
public (string code, List<(Range changeRange, string changeValue)> changes) ExtractCodeAndChanges(string code) {
public (string code, List<string> codes, List<List<Change>> changes) ExtractCodeAndChanges(string code) {
var lineMatcher = new Regex(@"\r?\n");
var matcher = new Regex(@"(?<previousNewline>^|\r?\n)(?<toRemove>.*?//(?<newtOrRemove>Next|Remove)(?<id>\d*):(?<newline>\\n)?)");
var newLineOrDoubleBackslashMatcher = new Regex(@"\\\\|\\n");
var matcher = new Regex(@"(?<previousNewline>^|\r?\n)(?<toRemove>.*?(?<commentStart>//)(?<keyword>Replace|Remove|Insert)(?<id>\d*):)(?<toInsert>.*)");
code = code.Trim();
var codes = new List<string>();
codes.Add(code);
var originalCode = code;
var matches = matcher.Matches(code);
var changes = new List<(Range, string)>();
var changes = new List<List<Change>>();
while (matches.Count > 0) {
var firstChange = 0;
Match firstChangeMatch = null;
Expand All @@ -205,12 +225,20 @@ private static bool NoMoreNotificationsToAwaitFrom(VerificationStatusGutter veri
break;
}

var startRemove =
firstChangeMatch.Groups["newtOrRemove"].Value == "Next" ?
firstChangeMatch.Groups["toRemove"].Index :
firstChangeMatch.Groups["previousNewline"].Index;
var keyword = firstChangeMatch.Groups["keyword"].Value;
var startRemove = keyword switch {
"Replace" => firstChangeMatch.Groups["toRemove"].Index,
"Remove" => firstChangeMatch.Groups["previousNewline"].Index,
"Insert" => firstChangeMatch.Groups["commentStart"].Index,
_ => throw new Exception("Unexpected keyword: " + keyword + ", expected Replace, Remove or Insert")
};
var endRemove = firstChangeMatch.Groups["toRemove"].Index + firstChangeMatch.Groups["toRemove"].Value.Length;

var toInsert = firstChangeMatch.Groups["toInsert"].Value;
var toInsertIndex = firstChangeMatch.Groups["toInsert"].Index;
var allNewlinesOrDoubleBackslashes = newLineOrDoubleBackslashMatcher.Matches(toInsert);


Position IndexToPosition(int index) {
var before = code.Substring(0, index);
var newlines = lineMatcher.Matches(before);
Expand All @@ -224,15 +252,31 @@ Position IndexToPosition(int index) {
return new Position(line, character);
}

var optionalNewLine = firstChangeMatch.Groups["newline"].Success ? "\n" : "";
// For now, simple: Remove the line
changes.Add(new(
new Range(IndexToPosition(startRemove), IndexToPosition(endRemove)), optionalNewLine));
code = code.Substring(0, startRemove) + optionalNewLine + code.Substring(endRemove);
// If there are \n characters in the comments, we replace them by newlines
// If there are \\ characters in the comments, we replace them by single slashes
var resultingChange = new List<Change>();
for (var i = allNewlinesOrDoubleBackslashes.Count - 1; i >= 0; i--) {
var newlineOrDoubleBackslash = allNewlinesOrDoubleBackslashes[i];
var isNewline = newlineOrDoubleBackslash.Value == @"\n";
var index = newlineOrDoubleBackslash.Index;
var absoluteIndex = toInsertIndex + index;
var absoluteIndexEnd = absoluteIndex + newlineOrDoubleBackslash.Value.Length;
var replacement = isNewline ? "\n" : @"\";
resultingChange.Add(new(
new Range(IndexToPosition(absoluteIndex), IndexToPosition(absoluteIndexEnd)), replacement
));
code = code.Substring(0, absoluteIndex) + replacement + code.Substring(absoluteIndexEnd);
}

resultingChange.Add(new(
new Range(IndexToPosition(startRemove), IndexToPosition(endRemove)), ""));
code = code.Substring(0, startRemove) + code.Substring(endRemove);
matches = matcher.Matches(code);
changes.Add(resultingChange);
codes.Add(code);
}

return (originalCode, changes);
return (originalCode, codes, changes);
}

// If testTrace is false, codeAndTree should not contain a trace to test.
Expand All @@ -245,18 +289,18 @@ public async Task VerifyTrace(string codeAndTrace, string fileName = null, bool
codeAndTrace.Substring(0, 2) == "\r\n" ? codeAndTrace.Substring(2) :
codeAndTrace;
var codeAndChanges = testTrace ? ExtractCode(codeAndTrace) : codeAndTrace;
var (code, changes) = ExtractCodeAndChanges(codeAndChanges);
var documentItem = CreateTestDocument(code, fileName);
var (code, codes, changesList) = ExtractCodeAndChanges(codeAndChanges);
var documentItem = CreateTestDocument(code.Trim(), fileName);
client.OpenDocument(documentItem);
var traces = new List<LineVerificationStatus[]>();
traces.AddRange(await GetAllLineVerificationStatuses(documentItem, verificationStatusGutterReceiver, intermediates: intermediates));
foreach (var (range, inserted) in changes) {
ApplyChange(ref documentItem, range, inserted);
foreach (var changes in changesList) {
ApplyChanges(ref documentItem, changes);
traces.AddRange(await GetAllLineVerificationStatuses(documentItem, verificationStatusGutterReceiver, intermediates: intermediates));
}

if (testTrace) {
var traceObtained = RenderTrace(traces, code);
var traceObtained = RenderTrace(traces, codes);
var ignoreQuestionMarks = AcceptQuestionMarks(traceObtained, codeAndTrace);
var expected = "\n" + codeAndTrace + "\n";
var actual = "\n" + ignoreQuestionMarks + "\n";
Expand Down
30 changes: 15 additions & 15 deletions Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,10 @@ public class ReorderingVerificationGutterStatusTester : LinearVerificationGutter
public async Task EnsuresPriorityDependsOnEditing() {
await TestPriorities(@"
method m1() {
assert false;//Next2: assert true;
assert false;//Replace2: assert true;
}
method m2() {
assert false;//Next1: assert true;
assert false;//Replace1: assert true;
}
",
"m1 m2\n" +
Expand All @@ -42,19 +42,19 @@ method m2() {
public async Task EnsuresPriorityDependsOnEditingWhileEditingSameMethod() {
await TestPriorities(@"
method m1() {
assert false;//Next7: assert true;//Next8: assert false;
assert false;//Replace7: assert true;//Replace8: assert false;
}
method m2() {
assert false;//Next5: assert true;
assert false;//Replace5: assert true;
}
method m3() {
assert false;//Next2: assert true;//Next9: assert false;
assert false;//Replace2: assert true;//Replace9: assert false;
}
method m4() {
assert false;//Next3: assert true;//Next4: assert false;
assert false;//Replace3: assert true;//Replace4: assert false;
}
method m5() {
assert false;//Next1: assert true;//Next6: assert false;//Next10: assert true;
assert false;//Replace1: assert true;//Replace6: assert false;//Replace10: assert true;
}
", "m1 m2 m3 m4 m5\n" +
"m5 m1 m2 m3 m4\n" +
Expand All @@ -76,10 +76,10 @@ await TestPriorities(@"
method m1() { assert false; }
method m2() { assert false; }
method m3() {
assert false;//Next1: assert true;
assert false;//Replace1: assert true;
}
method m4() {
assert false;//Next2: assert true;
assert false;//Replace2: assert true;
}
method m5() { assert false; } //Remove3:
",
Expand All @@ -94,13 +94,13 @@ public async Task EnsuresPriorityWorksEvenIfRemovingMethodsWhileTypo() {
await TestPriorities(@"
method m1() { assert false; }
method m2() {
assert false;//Next3: typo//Next5: assert true;
assert false;//Replace3: typo//Replace5: assert true;
}
method m3() {
assert false;//Next1: assert true;
assert false;//Replace1: assert true;
}
method m4() {
assert false;//Next2: assert true;
assert false;//Replace2: assert true;
}
method m5() { assert false; } //Remove4:
",
Expand All @@ -123,7 +123,7 @@ await SetUp(options => {
});
var symbols = ExtractSymbols(symbolsString);

var (code, changes) = ExtractCodeAndChanges(codeAndChanges.TrimStart());
var (code, codes, changesList) = ExtractCodeAndChanges(codeAndChanges.TrimStart());
var documentItem = CreateTestDocument(code);
client.OpenDocument(documentItem);

Expand All @@ -147,9 +147,9 @@ async Task CompareWithExpectation(List<string> expectedSymbols) {
}

await CompareWithExpectation(symbols.First());
foreach (var (change, expectedSymbols) in changes.Zip(symbols.Skip(1))) {
foreach (var (changes, expectedSymbols) in changesList.Zip(symbols.Skip(1))) {
index++;
ApplyChange(ref documentItem, change.changeRange, change.changeValue);
ApplyChanges(ref documentItem, changes);
if (expectedSymbols != null) {
var migrated = expectedSymbols.Count == 0;
if (migrated) {
Expand Down
35 changes: 21 additions & 14 deletions Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,15 @@ public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutt

// To add a new test, just call VerifyTrace on a given program,
// the test will fail and give the correct output that can be use for the test
// Add '//Next<n>:' to edit a line multiple times
// Add '//Replace<n>:' to edit a line multiple times

[Fact]
public async Task GitIssue4287GutterHighlightingBroken() {
await VerifyTrace(@"
| | [ ]://Insert1:method Test() {//Insert2:\\n assert false;\n}
### | [=]:
######[ ]:", intermediates: false);
}

[Fact]
public async Task GitIssue3821GutterIgnoredProblem() {
Expand Down Expand Up @@ -62,7 +70,7 @@ await VerifyTrace(@"
. S [S][ ][I][I][S] | : if x {
. S [S][ ][I][I][S] | : i := 2;
. S [=][=][-][-][~] | : } else {
. S [S][ ]/!\[I][S] | : i := 1; //Next1: i := /; //Next2: i := 2;
. S [S][ ]/!\[I][S] | : i := 1; //Replace1: i := /; //Replace2: i := 2;
. S [S][ ][I][I][S] | : }
. S [S][ ][I][I][S] | :}
| | | I I | | :
Expand All @@ -73,15 +81,15 @@ await VerifyTrace(@"
[Fact(Timeout = MaxTestExecutionTimeMs)]
public async Task EnsuresItWorksForSubsetTypes() {
await VerifyTrace(@"
| | | I I | | | I I | | | :
| | | I I | | | I I | | | :// The maximum Id
. | | | I I | | | I I | | | :ghost const maxId := 200;
| | | I I | | | I I | | | :
. | | | I I | | | I I | | | :ghost predicate isIssueIdValid(issueId: int) {
. | | | I I | | | I I | | | : 101 <= issueId < maxId
. | | | I I | | | I I | | | :}
| | | I I | | | I I | | | :
. S S | I . S S [=] I . S S | :type IssueId = i : int | isIssueIdValid(i)
. S | | I . S | [=] I . S | | : witness 101 //Next1: witness 99 //Next2: witness 101 ");
. S | | I . S | [=] I . S | | : witness 101 //Replace1: witness 99 //Replace2: witness 101 ");
}

[Fact(Timeout = MaxTestExecutionTimeMs)]
Expand All @@ -104,9 +112,9 @@ await VerifyTrace(@"
. | | | I | :predicate P(x: int)
| | | I | :
. S [S][ ][I] | :method Main() {
. S [=][=][I] | : ghost var x :| P(x); //Next: ghost var x := 1;
. S [=][=][I] | : ghost var x :| P(x); //Replace: ghost var x := 1;
. S [S][ ][I] | :}
| :");
| :// Comment to not trim this line");
}
}

Expand All @@ -115,16 +123,15 @@ public async Task EnsureEmptyDocumentIsVerified() {
await VerifyTrace(@"
| :class A {
| :}
| :");
| :// Comment so test does not trim this line");
}


[Fact/*, Timeout(MaxTestExecutionTimeMs)*/]
public async Task EnsuresEmptyDocumentWithParseErrorShowsError() {
await VerifyTrace(@"
/!\:class A {/
:}
:");
:}");
}

[Fact/*(Timeout = MaxTestExecutionTimeMs)*/]
Expand All @@ -146,10 +153,10 @@ await VerifyTrace(@"
public async Task EnsuresAddingNewlinesMigratesPositions() {
await VerifyTrace(@"
. S [S][ ][I][S][ ][I][S][ ]:method f(x: int) {
. S [S][ ][I][S][ ][I][S][ ]: //Next1:\n //Next2:\n
. S [S][ ][I][S][ ][I][S][ ]: //Replace1:\n //Replace2:\\n
. S [=][=][I][S][ ][I][S][ ]: assert x == 2; }
[-][~][=][I][S][ ]:
[-][~][=]:");
############[-][~][=][I][S][ ]:
#####################[-][~][=]:");
}

[Fact/*(Timeout = MaxTestExecutionTimeMs)*/]
Expand All @@ -159,12 +166,12 @@ await VerifyTrace(@"
. S [S][ ][I][S][S][ ]:method f(x: int) returns (y: int)
. S [S][ ][I][S][S][ ]:ensures
. S [=][=][-][~][=][=]: x > 3 { y := x;
. S [S][ ][I][S][S][ ]: //Next1:\n
. S [S][ ][I][S][S][ ]: //Replace1:\n
. S [=][=][-][~][=][ ]: while(y <= 1) invariant y >= 2 {
. S [S][ ][-][~][~][=]: y := y + 1;
. S [S][ ][I][S][S][ ]: }
. S [S][ ][I][S][S][ ]:}
[I][S][S][ ]:");
############[I][S][S][ ]:");
}

[Fact]
Expand Down
Loading
Loading