feat: Add `-diagnosticsFormat` command-line flag #2363

cpitclaudel · 2022-07-05T17:22:46Z

This PR adds -diagnosticsFormat:json to the CLI. The output looks like this:

{"range":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":8,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}
{"range":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":9,"character":17}}},"severity":1,"message":"Error: result of operation might violate newtype constraint for \u0027byte\u0027","source":"Verifier","relatedInformation":[]}
{"range":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":12,"character":16}}},"severity":1,"message":"Error: A precondition for this call might not hold.","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":11,"character":35}}},"message":"Related location: This is the precondition that might not hold."}]}

Dafny program verifier finished with 1 verified, 2 errors

This format is consistent with a bunch of other tools (see below). The intent is that client can look for { in column 0 and parse one object per such line.

Design notes:

Many compilers have this option, but it's not named consistently. Other tools
use -fdiagnostics-format=json, --json, --outputjson, --formatter=json,
--format=json, --error-format=json, --output-format=json,
--message-format=json, etc.
Output format is one message per line. This makes it easy to parse output
even if it's mixed with other non-JSON output. This is a common
approach (e.g. rustc does this), but it's not universal (GCC groups all
messages into an array). Streaming results allows clients to consume them as
they come.

Implementation:

Source/Dafny/DafnyOptions.cs
(DiagnosticsFormats): New enum.
(DiagnosticsFormat): Default to PlainText.
(ParseOption): Recognize new -diagnosticsFormat flag.
(HelpBody): Document it.
Source/DafnyDriver/DafnyDriver.cs
(ThreadMain): Delay initialization of ErrorReporter.
Source/Dafny/JsonDiagnostics.cs: New file. Capture Dafny and boogie message
and print them as single-line JSON objects.
Test/cli/diagnosticsFormats.dfy: New test.
docs/DafnyRef/UserGuide.md: Document -diagnosticsFormat.

Closes #2084 (by adressing the underlying use case), closes #2229 (by superseding it). CC @mschlaipfer

Design notes: - Many compilers have this option, but it's not named consistently. Other tools use `-fdiagnostics-format=json`, `--json`, `--outputjson`, `--formatter=json`, `--format=json`, `--error-format=json`, `--output-format=json`, `--message-format=json`, etc. - Output format is one message per line. This makes it easy to parse output even if it's mixed with other non-JSON output. This is a common approach (e.g. `rustc` does this), but it's not universal (GCC groups all messages into an array). Streaming results allows clients to consume them as they come. Implementation: * `Source/Dafny/DafnyOptions.cs` (`DiagnosticsFormats`): New enum. (`DiagnosticsFormat`): Default to `PlainText`. (`ParseOption`): Recognize new `-diagnosticsFormat` flag. (`HelpBody`): Document it. * `Source/DafnyDriver/DafnyDriver.cs` (`ThreadMain`): Delay initialization of `ErrorReporter`. * `Source/Dafny/JsonDiagnostics.cs`: New file. Capture Dafny and boogie message and print them as single-line JSON objects. * `Test/cli/diagnosticsFormats.dfy`: New test. * `docs/DafnyRef/UserGuide.md`: Document `-diagnosticsFormat`.

MikaelMayer · 2022-07-18T14:24:55Z

This is a great addition to the Dafny ecosystem which will surely make Dafny more modular.
A few remarks before I dive in the PR review:

I would like you to detect if the token is a RangeToken, and in this case add an "end" field to the range above, so that the range has both "start" and "end"
Since it's API, I think we should also offer
*. The absolute offset of the position. Necessary so that programmatic API consumers don't need to think of lines/column when parsing our error messages.
*. The file name. There might be several files and just the position is not enough. There are also included files, and related errors.

Related positions should be, as for the Language Server, nested under the main error, not a top-level error. In your example, the message containing "Related location: " is a top-level one... Look at how LSP does it:

dafny/Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

Lines 55 to 77 in 8792af1

    
           public void ReportBoogieError(ErrorInformation error) { 
        
             var relatedInformation = new List<DiagnosticRelatedInformation>(); 
        
             foreach (var auxiliaryInformation in error.Aux) { 
        
               if (auxiliaryInformation.Category == RelatedLocationCategory) { 
        
                 relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(auxiliaryInformation.Tok, auxiliaryInformation.Msg)); 
        
               } else { 
        
                 // The execution trace is an additional auxiliary which identifies itself with 
        
                 // line=0 and character=0. These positions cause errors when exposing them, Furthermore, 
        
                 // the execution trace message appears to not have any interesting information. 
        
                 if (auxiliaryInformation.Tok.line > 0) { 
        
                   Info(VerifierMessageSource, auxiliaryInformation.Tok, auxiliaryInformation.Msg); 
        
                 } 
        
               } 
        
             } 
        
             var uri = GetDocumentUriOrDefault(error.Tok); 
        
             var diagnostic = new Diagnostic { 
        
               Severity = DiagnosticSeverity.Error, 
        
               Message = error.Msg, 
        
               Range = error.Tok.GetLspRange(), 
        
               RelatedInformation = relatedInformation, 
        
               Source = VerifierMessageSource.ToString() 
        
             };

cpitclaudel · 2022-07-18T16:36:52Z

I would like you to detect if the token is a RangeToken, and in this case add an "end" field to the range above, so that the range has both "start" and "end"

Done, can you give me an example of code with a RangeToken so I can test the code?

Since it's API, I think we should also offer. The absolute offset of the position.

I don't think we should deviate from LSP here, but I can do it if you want.

The file name.

Yep, good catch. Done.

Related positions should be, as for the Language Server, nested under the main error, not a top-level error.

I will look into that.

cpitclaudel · 2022-07-18T17:36:51Z

 I will look into that.

Done.

MikaelMayer · 2022-07-18T19:20:25Z

Can you update the PR description?

cpitclaudel · 2022-07-19T16:20:56Z

Since it's API, I think we should also offer. The absolute offset of the position.

I don't think we should deviate from LSP here, but I can do it if you want.

I changed my mind. I'd love to do that, but we don't have the data. Tokens have a UTF-16 offset, which is not very usable by clients. Until we move away from that, I don't think we should include that info in the output.

cpitclaudel · 2022-07-19T16:21:23Z

Can you update the PR description?

With the example output? I can! It's also in the diff of the PR (there's a test)

…gnostics

cpitclaudel · 2022-07-19T16:35:01Z

Ready for review, I think

MikaelMayer · 2022-07-19T17:07:01Z

I changed my mind. I'd love to do that, but we don't have the data. Tokens have a UTF-16 offset, which is not very usable by clients. Until we move away from that, I don't think we should include that info in the output.

An UTF-16 offset? I don't think so. I have been consistently using pos to extract strings from program and it works well, either reading a buffer or the C# string. See #2434

MikaelMayer

A few items, otherwise, great start to make Dafny become more library-friendly.

RELEASE_NOTES.md

Source/Dafny/DafnyOptions.cs

Source/Dafny/JsonDiagnostics.cs

MikaelMayer · 2022-07-19T17:11:15Z

Test/cli/diagnosticsFormats.dfy.expect

+diagnosticsFormats.dfy(11,35): Related location: This is the precondition that might not hold.
+
+Dafny program verifier finished with 1 verified, 2 errors
+{"range":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":8,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}


To test for the "end", you have to provide the argument name /showSnippets:1

I don't understand: /showSnippets is for showing the error in context, and we don't want to do that in JSON mode, right?

/showSnippets enables Dafny to create RangeTokens instead of just Tokens.
For the JSON mode, if /showSnippets is activated, it would be reasonable to me that we don't add the snippet as part of the error message (but we could... that could be useful), but that way we can report error using ranges.

Cool, I understand now :) Is there a strong reason to not create RangeTokens all the time? This way we could report ranges on the command line even when /showSnippets isn't specified, not just line-column pairs.

Well the only reason was that I'm too lazy (or don't think it's worth it?) to change the 1200+ files of our integration tests And it could be a breaking change (however, I don't think this would be a big deal)

Oh, good point regarding the test files.

I've added -showSnippets:1 to the test and documented it in UserGuide.md

MikaelMayer · 2022-07-19T17:12:08Z

Test/cli/diagnosticsFormats.dfy.expect

+diagnosticsFormats.dfy(11,35): Related location: This is the precondition that might not hold.
+
+Dafny program verifier finished with 1 verified, 2 errors
+{"range":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":8,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}


Suggested change

{"range":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":8,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}

{"location":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":8,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}

I suggest we use "range" only for the start and the end, and "location" for something that holds a file name and a range, like LSP is doing.

Good catch, will fix, that was the intended thing and I got it wrong :'(

cpitclaudel · 2022-07-19T18:02:33Z

An UTF-16 offset? I don't think so. I have been consistently using pos to extract strings from program and it works well, either reading a buffer or the C# string. See #2434

Yep, strings are UTF-16 in C#, so if you use these offsets into strings in C# it will work, but it wouldn't work in other languages that use bytes or utf-8. It would be weird to leak that.

Co-authored-by: Mikaël Mayer <[email protected]>

MikaelMayer · 2022-07-19T19:23:33Z

Yep, strings are UTF-16 in C#, so if you use these offsets into strings in C# it will work, but it wouldn't work in other languages that use bytes or utf-8. It would be weird to leak that.

But isn't "col" already leaking this information?

cpitclaudel · 2022-07-19T20:42:13Z

But isn't "col" already leaking this information?

😱 you're right :'(
I will add pos then, it doesn't make things worse.

cpitclaudel · 2022-07-21T00:08:33Z

I will add pos then, it doesn't make things worse.

Done

MikaelMayer

Looks good, almost there.

RELEASE_NOTES.md

Source/Dafny/JsonDiagnostics.cs

MikaelMayer · 2022-07-21T03:05:06Z

Source/Dafny/JsonDiagnostics.cs

@@ -74,7 +75,7 @@ record DiagnosticMessageData(MessageSource source, ErrorLevel level, IToken tok,
    var auxRelated = related?.SelectMany(SerializeAuxInfo) ?? Enumerable.Empty<JsonNode>();
    var innerRelated = SerializeInnerTokens(tok);
    return new JsonObject {
-      ["range"] = SerializeToken(tok),
+      ["location"] = SerializeToken(tok),


A few CI failures line 93?

MikaelMayer

Great job

cpitclaudel requested review from mschlaipfer and MikaelMayer July 5, 2022 17:22

cpitclaudel force-pushed the cpitclaudel_jsonDiagnostics branch from 5d8b142 to c9b8564 Compare July 5, 2022 21:50

cpitclaudel self-assigned this Jul 8, 2022

cpitclaudel force-pushed the cpitclaudel_jsonDiagnostics branch from 6147c97 to 6f0b6e9 Compare July 14, 2022 23:32

cpitclaudel force-pushed the cpitclaudel_jsonDiagnostics branch from 6f0b6e9 to 1bed89b Compare July 14, 2022 23:33

Merge branch 'master' into cpitclaudel_jsonDiagnostics

c2f22e1

Add file name and end token

2ddb4a7

cpitclaudel force-pushed the cpitclaudel_jsonDiagnostics branch from 7ba16a1 to 2ddb4a7 Compare July 18, 2022 16:43

Group related messages

656e136

Merge remote-tracking branch 'origin/master' into cpitclaudel_jsonDia…

71f94b3

…gnostics

MikaelMayer requested changes Jul 19, 2022

View reviewed changes

cpitclaudel and others added 2 commits July 19, 2022 14:04

Update Source/Dafny/DafnyOptions.cs

00f1cd2

Co-authored-by: Mikaël Mayer <[email protected]>

Update RELEASE_NOTES.md

83d6f20

Co-authored-by: Mikaël Mayer <[email protected]>

cpitclaudel added 2 commits July 20, 2022 16:51

Rename "range" to "location"

d5ca1e7

Add absolute offsets

ec86eab

Merge branch 'master' into cpitclaudel_jsonDiagnostics

aae95a0

Add test for end positions

5bbb8a2

cpitclaudel requested a review from MikaelMayer July 21, 2022 01:10

MikaelMayer requested changes Jul 21, 2022

View reviewed changes

cpitclaudel and others added 3 commits July 21, 2022 11:28

Disambiguate Dafny.IToken and Boogie.IToken

44e9bb4

Update release notes

db6c91d

Merge branch 'master' into cpitclaudel_jsonDiagnostics

9b220ac

MikaelMayer previously approved these changes Jul 21, 2022

View reviewed changes

cpitclaudel enabled auto-merge (squash) July 21, 2022 19:01

Check in auto-generated file

68903cd

cpitclaudel dismissed MikaelMayer’s stale review via 68903cd July 21, 2022 19:03

Merge branch 'master' into cpitclaudel_jsonDiagnostics

324fc70

cpitclaudel requested a review from MikaelMayer July 21, 2022 19:09

MikaelMayer approved these changes Jul 21, 2022

View reviewed changes

cpitclaudel merged commit 9253265 into master Jul 21, 2022

cpitclaudel deleted the cpitclaudel_jsonDiagnostics branch July 21, 2022 20:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Add `-diagnosticsFormat` command-line flag #2363

feat: Add `-diagnosticsFormat` command-line flag #2363

cpitclaudel commented Jul 5, 2022 •

edited

Loading

MikaelMayer commented Jul 18, 2022

cpitclaudel commented Jul 18, 2022 •

edited

Loading

cpitclaudel commented Jul 18, 2022

MikaelMayer commented Jul 18, 2022

cpitclaudel commented Jul 19, 2022

cpitclaudel commented Jul 19, 2022

cpitclaudel commented Jul 19, 2022

MikaelMayer commented Jul 19, 2022

MikaelMayer left a comment

MikaelMayer Jul 19, 2022

cpitclaudel Jul 19, 2022

MikaelMayer Jul 19, 2022

cpitclaudel Jul 19, 2022

MikaelMayer Jul 19, 2022

cpitclaudel Jul 21, 2022

cpitclaudel Jul 21, 2022

MikaelMayer Jul 19, 2022

cpitclaudel Jul 19, 2022

cpitclaudel Jul 21, 2022

cpitclaudel commented Jul 19, 2022

MikaelMayer commented Jul 19, 2022

cpitclaudel commented Jul 19, 2022

cpitclaudel commented Jul 21, 2022

MikaelMayer left a comment

MikaelMayer Jul 21, 2022

MikaelMayer left a comment

	{"range":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":8,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}
	{"location":{"filename":"diagnosticsFormats.dfy","range":{"start":{"line":8,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}

feat: Add -diagnosticsFormat command-line flag #2363

feat: Add -diagnosticsFormat command-line flag #2363

Conversation

cpitclaudel commented Jul 5, 2022 • edited Loading

MikaelMayer commented Jul 18, 2022

cpitclaudel commented Jul 18, 2022 • edited Loading

cpitclaudel commented Jul 18, 2022

MikaelMayer commented Jul 18, 2022

cpitclaudel commented Jul 19, 2022

cpitclaudel commented Jul 19, 2022

cpitclaudel commented Jul 19, 2022

MikaelMayer commented Jul 19, 2022

MikaelMayer 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

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

cpitclaudel commented Jul 19, 2022

MikaelMayer commented Jul 19, 2022

cpitclaudel commented Jul 19, 2022

cpitclaudel commented Jul 21, 2022

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

feat: Add `-diagnosticsFormat` command-line flag #2363

feat: Add `-diagnosticsFormat` command-line flag #2363

cpitclaudel commented Jul 5, 2022 •

edited

Loading

cpitclaudel commented Jul 18, 2022 •

edited

Loading