Feat: Added ranges to expression #1985

MikaelMayer · 2022-04-07T21:19:07Z

Before (possibly failing assertions are barely visible):

After (assertions are clearly visible)

Although it cannot be seen yet, related positions on postconditions also now cover an entire expression instead of just a token.

This PR:

Adds a way for expression to expose their start token and their end token
Offers a way to create a "RangeToken" from any expression that represents the entire range of an expression
Also changes the tokens we use for Boogie so that they use RangeToken if an translator option ``ReportRange` is activated
activates this option for the language server only for now.

In the translator, the method GetTok replaces .tok to perform the switch.

After searching for 30 minutes, I didn't find what else to change to get an entire function or method call to be entirely highlighted, any hint @RustanLeino ?

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

…or now

…token.

cpitclaudel

👍 lovely

keyboardDrummer · 2022-04-08T13:23:06Z

Source/Dafny/AST/DafnyAst.cs

+ private void RecomputeStartEnd() {
+ startTok = tok;
+ endTok = tok;
+ foreach (var e in SubExpressions) {


Possibly out of scope: it would help if SubExpressions was a IReadOnlyList so you could retrieve the first and last element without having to iterate.

You mean, we could cache the SubExpressions? That's a good point, but yes, let's leave it out of scope for this PR.

keyboardDrummer · 2022-04-08T13:26:17Z

Source/Dafny/AST/DafnyAst.cs

+ endTok = tok;
+ foreach (var e in SubExpressions) {
+ if (e.tok.pos < startTok.pos) {
+ startTok = e.tok;


Shouldn't this be e.StartTok ?

Yes that would be even better, thanks. I'm also adding a check that the filename should be the same.

keyboardDrummer · 2022-04-08T13:29:24Z

Source/Dafny/AST/DafnyAst.cs

+ public IToken RangeToken => new RangeToken(StartTok, EndTok);
+
+ // Computes the start and end token of this expression
+ private void RecomputeStartEnd() {


Why is this called Re compute, isn't it only called once?

I imagine it could be called multiple times if we modify the AST, e.g. by adding elements in a set comprehension. But we can always clone and expression, modify it and then access the new range so that's not useful. Will remove this method.

keyboardDrummer · 2022-04-08T13:30:00Z

Source/Dafny/AST/DafnyAst.cs

+ if (e.tok.pos < startTok.pos) {
+ startTok = e.tok;
+ } else if (e.tok.pos > endTok.pos) {
+ endTok = e.tok;


Shouldn't this be e.EndTok ?

keyboardDrummer · 2022-04-08T13:30:54Z

Source/Dafny/AST/DafnyAst.cs

@@ -9070,6 +9086,48 @@ public abstract class Expression {
 get { yield break; }
 }

+ private IToken startTok;


Why not store the RangeToken instead of two ITokens?

keyboardDrummer · 2022-04-08T13:36:09Z

Source/Dafny/AST/DafnyAst.cs

+
+ // Creates a token on the entire range of the expression.
+ // Used only for error reporting.
+ public IToken RangeToken => new RangeToken(StartTok, EndTok);


Do you think we could move all the new code to a class

class SyntaxNode { public readonly IToken tok; public abstract IEnumerable<SyntaxNode> ChildNodes {get;} public IToken RangeToken => .. }

and then have

class Expression : SyntaxNode { public IEnumerable<SyntaxNode> ChildNodes => SubExpressions; }

Or do you feel that's too early for this PR ?

We could as well use the bounded polymorphism pattern:

class SyntaxNode<T> where T: SyntaxNode { public readonly IToken tok; public abstract IEnumerable<T> Children{get;} public IToken RangeToken => .. } class Expression : SyntaxNode<Expression> { }

However, we should do this refactoring later, when I see a compelling reason to do so. We might as well replace the "tok" by a Format or trait to keep track of concrete syntax tree elements.

However, we should do this refactoring later

Alright. Indeed, I think it only makes sense to do this if we have multiple subclasses of SyntaxNode.

keyboardDrummer · 2022-04-08T13:36:55Z

Source/Dafny/Verifier/Translator.ExpressionTranslator.cs

@@ -110,6 +111,10 @@ public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)
 Contract.Requires(modifiesFrame != null);
 }

+ internal IToken GetTok(Expression e) {


Why not name it GetToken ? Also, I'm not a fan of e even though this is such as short method ^^

keyboardDrummer · 2022-04-08T13:40:17Z

Source/Dafny/Verifier/Translator.cs

@@ -44,6 +44,7 @@ public partial class Translator {
 public class TranslatorFlags {
 public bool InsertChecksums = 0 < DafnyOptions.O.VerifySnapshots;
 public string UniqueIdPrefix = null;
+ public bool ReportRanges = false;


When do we not want to report ranges? Looks like it's turned on for the IDE but not the CLI. Why the difference?

Yes, because the IDE will highlight ranges. However, in the CLI, there is a format to report positions only, so that would mean 1) to change that format to support ranges of positions, which would be cluttering 2) or we could also decide so activate this option when -showSnipptes is enabled, but it's not the option by default yet and it will require to change the way we display errors anyway.

I though we should first add these ranges in the Dafny Language Server, where they are the most useful, and then we can always do this later.

keyboardDrummer · 2022-04-08T13:42:00Z

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -582,7 +582,7 @@ modifies this
 Assert.AreEqual("This is the postcondition that might not hold.", relatedInformation[0].Message);
 Assert.AreEqual(new Range((14, 16), (14, 21)), relatedInformation[0].Location.Range);
 Assert.AreEqual("Related location", relatedInformation[1].Message);
- Assert.AreEqual(new Range((9, 13), (9, 14)), relatedInformation[1].Location.Range);
+ Assert.AreEqual(new Range((9, 11), (9, 16)), relatedInformation[1].Location.Range);


Could we have tests with more nested expressions as well?

tests added

keyboardDrummer · 2022-04-08T13:46:05Z

Nice change!

Failed function call highlight Other cases of extended range highlighting

keyboardDrummer · 2022-04-11T19:41:09Z

Source/Dafny/AST/DafnyAst.cs

@@ -8997,6 +9026,38 @@ public abstract class Expression {
 get { yield break; }
 }

+ private RangeToken rangeToken;
+
+ // Creates a token on the entire range of the expression.


Nitpick: I'd prefer documentation comments /// above members.

Source/Dafny/AST/DafnyAst.cs

Added ranges to expression. Report them only in the language server f…

70db78c

…or now

MikaelMayer requested review from cpitclaudel, RustanLeino and robin-aws April 7, 2022 21:19

MikaelMayer self-assigned this Apr 7, 2022

MikaelMayer added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny area: error-reporting Clarity of the error reporting labels Apr 7, 2022

Release notes and more changes in accessing the range instead of the …

24d3250

…token.

cpitclaudel previously approved these changes Apr 7, 2022

View reviewed changes

keyboardDrummer reviewed Apr 8, 2022

View reviewed changes

Review comments

414877a

MikaelMayer dismissed cpitclaudel’s stale review via 414877a April 8, 2022 21:44

MikaelMayer and others added 2 commits April 11, 2022 11:47

Statement RangeToken for call statements

b2a5997

Failed function call highlight Other cases of extended range highlighting

Merge branch 'master' into feat-ranges

4ed2e1e

MikaelMayer enabled auto-merge (squash) April 11, 2022 18:49

MikaelMayer requested a review from keyboardDrummer April 11, 2022 18:49

keyboardDrummer previously approved these changes Apr 11, 2022

View reviewed changes

Merge branch 'master' into feat-ranges

c4711b3

MikaelMayer commented Apr 11, 2022

View reviewed changes

Source/Dafny/AST/DafnyAst.cs Outdated Show resolved Hide resolved

Update Source/Dafny/AST/DafnyAst.cs

0ae47af

MikaelMayer dismissed keyboardDrummer’s stale review via 0ae47af April 11, 2022 19:59

MikaelMayer requested a review from keyboardDrummer April 11, 2022 19:59

keyboardDrummer approved these changes Apr 11, 2022

View reviewed changes

MikaelMayer merged commit 7918c70 into master Apr 12, 2022

MikaelMayer deleted the feat-ranges branch April 12, 2022 00:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: Added ranges to expression #1985

Feat: Added ranges to expression #1985

MikaelMayer commented Apr 7, 2022

cpitclaudel left a comment

keyboardDrummer Apr 8, 2022

MikaelMayer Apr 8, 2022

keyboardDrummer Apr 8, 2022

MikaelMayer Apr 8, 2022

keyboardDrummer Apr 8, 2022

MikaelMayer Apr 8, 2022 •

edited

Loading

keyboardDrummer Apr 8, 2022

keyboardDrummer Apr 8, 2022

keyboardDrummer Apr 8, 2022

MikaelMayer Apr 8, 2022

keyboardDrummer Apr 11, 2022

keyboardDrummer Apr 8, 2022

keyboardDrummer Apr 8, 2022

MikaelMayer Apr 8, 2022

keyboardDrummer Apr 11, 2022

keyboardDrummer Apr 8, 2022

MikaelMayer Apr 11, 2022

keyboardDrummer commented Apr 8, 2022

keyboardDrummer Apr 11, 2022

Feat: Added ranges to expression #1985

Feat: Added ranges to expression #1985

Conversation

MikaelMayer commented Apr 7, 2022

cpitclaudel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer Apr 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented Apr 8, 2022

Choose a reason for hiding this comment

MikaelMayer Apr 8, 2022 •

edited

Loading