Add tooltip on assertions that shows which functions are hidden #5929
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,3 @@ | ||
| [submodule "boogie"] | ||
| path = boogie | ||
| url = git@github.com:keyboardDrummer/boogie.git |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,97 @@ | ||
| using System; | ||
| using System.Text; | ||
|
|
||
| namespace Microsoft.Dafny; | ||
|
|
||
| public class RangeToken : TokenWrapper { | ||
| public IToken StartToken => WrappedToken; | ||
|
|
||
| public IToken EndToken => endToken ?? StartToken; | ||
|
|
||
| public bool InclusiveEnd => endToken != null; | ||
|
|
||
| public override bool Equals(object obj) { | ||
| if (obj is RangeToken other) { | ||
| return StartToken.Equals(other.StartToken) && EndToken.Equals(other.EndToken); | ||
| } | ||
| return false; | ||
| } | ||
|
|
||
| public override int GetHashCode() { | ||
| return HashCode.Combine(StartToken.GetHashCode(), EndToken.GetHashCode()); | ||
| } | ||
|
|
||
| public DafnyRange ToDafnyRange(bool includeTrailingWhitespace = false) { | ||
| var startLine = StartToken.line - 1; | ||
| var startColumn = StartToken.col - 1; | ||
| var endLine = EndToken.line - 1; | ||
| int whitespaceOffset = 0; | ||
| if (includeTrailingWhitespace) { | ||
| string trivia = EndToken.TrailingTrivia; | ||
| // Don't want to remove newlines or comments -- just spaces and tabs | ||
| while (whitespaceOffset < trivia.Length && (trivia[whitespaceOffset] == ' ' || trivia[whitespaceOffset] == '\t')) { | ||
| whitespaceOffset++; | ||
| } | ||
| } | ||
|
|
||
| var endColumn = EndToken.col + (InclusiveEnd ? EndToken.val.Length : 0) + whitespaceOffset - 1; | ||
| return new DafnyRange( | ||
| new DafnyPosition(startLine, startColumn), | ||
| new DafnyPosition(endLine, endColumn)); | ||
| } | ||
|
|
||
| public RangeToken(IToken startToken, IToken endToken) : base(startToken) { | ||
| this.endToken = endToken; | ||
| } | ||
|
|
||
| public string PrintOriginal() { | ||
| var token = StartToken; | ||
| var originalString = new StringBuilder(); | ||
| originalString.Append(token.val); | ||
| while (token.Next != null && token.pos < EndToken.pos) { | ||
| originalString.Append(token.TrailingTrivia); | ||
| token = token.Next; | ||
| originalString.Append(token.LeadingTrivia); | ||
| originalString.Append(token.val); | ||
| } | ||
|
|
||
| return originalString.ToString(); | ||
| } | ||
|
|
||
| public int Length() { | ||
| return EndToken.pos - StartToken.pos; | ||
| } | ||
|
|
||
| public RangeToken MakeAutoGenerated() { | ||
| return new RangeToken(new AutoGeneratedToken(StartToken), EndToken); | ||
| } | ||
|
|
||
| public RangeToken MakeRefined(ModuleDefinition module) { | ||
| return new RangeToken(new RefinementToken(StartToken, module), EndToken); | ||
| } | ||
|
|
||
| // TODO rename to Generated, and Token.NoToken to Token.Generated, and remove AutoGeneratedToken. | ||
| public static RangeToken NoToken = new(Token.NoToken, Token.NoToken); | ||
| private readonly IToken endToken; | ||
|
|
||
| public override IToken WithVal(string newVal) { | ||
| throw new NotImplementedException(); | ||
| } | ||
|
|
||
| public override bool IsSourceToken => this != NoToken; | ||
|
|
||
| public BoogieRangeToken ToToken() { | ||
| return new BoogieRangeToken(StartToken, EndToken, null); | ||
| } | ||
|
|
||
| public bool Contains(IToken otherToken) { | ||
| return StartToken.Uri == otherToken.Uri && | ||
| StartToken.pos <= otherToken.pos && | ||
| (EndToken == null || otherToken.pos <= EndToken.pos); | ||
| } | ||
|
|
||
| public bool Intersects(RangeToken other) { | ||
| return !(other.EndToken.pos + other.EndToken.val.Length <= StartToken.pos | ||
| || EndToken.pos + EndToken.val.Length <= other.StartToken.pos); | ||
| } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -356,15 +356,29 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT | |
| return result; | ||
| }); | ||
| if (updated || randomSeed != null) { | ||
| updates.OnNext(new CanVerifyPartsIdentified(canVerify, tasks)); | ||
| } | ||
|
|
||
| // When multiple calls to VerifyUnverifiedSymbol are made, the order in which they pass this await matches the call order. | ||
| await ticket; | ||
|
|
||
| if (!onlyPrepareVerificationForGutterTests) { | ||
| var groups = tasks.GroupBy(t => | ||
| // We unwrap so that we group on tokens as they are displayed to the user by Reporter.Info | ||
| TokenWrapper.Unwrap(BoogieGenerator.ToDafnyToken(true, t.Token))). | ||
| OrderBy(g => g.Key); | ||
| foreach (var tokenTasks in groups) { | ||
| var functions = tokenTasks.SelectMany(t => t.Split.HiddenFunctions.Select(f => f.tok). | ||
| OfType<FromDafnyNode>().Select(n => n.Node). | ||
|
There was a problem hiding this comment. Wrapping tokens to filter functions is not ideal. There are multi competing token wrapping strategies that will end up failing this test in the future. For example, refinement tokens will wrap your FromDafnyNode token making them not pass this test. There are other wrapped tokens types, like auto-generated tokens, nested tokens, override tokens for traits, etc. I'm not expecting you to do this refactoring, so in the meantime, please use something like There was a problem hiding this comment. Here the wrapping happens right before handing the token to Boogie, so Dafny won't do any further wrapper, and Boogie might do some wrapping on tokens but only use that for nodes that it creates, so not on the nodes that I'm interested in. I don't think there's a potential issue here. If there is one, how can we test for it? There was a problem hiding this comment. Ok, good to know that the risk is mitigated. I think that we still have the risk that later, someone will wrap your token after your own wrapping and their test cases will be orthogonal to yours, so both won't be tested together. |
||
| OfType<Function>()).Distinct().OrderBy(f => f.tok); | ||
| var hiddenFunctions = string.Join(", ", functions.Select(f => f.FullDafnyName)); | ||
| if (!string.IsNullOrEmpty(hiddenFunctions)) { | ||
| Reporter.Info(MessageSource.Verifier, tokenTasks.Key, $"hidden functions: {hiddenFunctions}"); | ||
| } | ||
| } | ||
|
|
||
| foreach (var task in tasks.Where(taskFilter)) { | ||
|
|
||
|
|
||
| var seededTask = randomSeed == null ? task : task.FromSeed(randomSeed.Value); | ||
| VerifyTask(canVerify, seededTask); | ||
| } | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.