Skip to content

Commit

Permalink
Fix 4287 gutter highlight before project pr (#4308)
Browse files Browse the repository at this point in the history 
Fixes #4287

Co-authored-by: Robin Salkeld <[email protected]>
  • Loading branch information
@MikaelMayer @robin-aws
MikaelMayer and robin-aws committed Jul 20, 2023
1 parent 89eed61 commit d4ba007
Show file tree
Hide file tree
Showing 9 changed files with 166 additions and 75 deletions.
6 changes: 3 additions & 3 deletions Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs
View file
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
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
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
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
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

0 comments on commit d4ba007

Please sign in to comment.