JSON log inaccuracies

[hmijail]

Dafny version

4.7.0+ebbec43ec8bab9e081f739c2742de185107df208

Code to produce this issue

module test {
    method a() 
    {
        assert true;
        assert true;
        assert false;
    }
}

Command to run and resulting output

$ dafny measure-complexity src/test2.dfy --log-format json\;LogFileName=test.json
Starting verification of iteration 1/1 with seed 0
src/test2.dfy(6,15): Error: assertion might not hold
  |
6 |         assert false;
  |                ^^^^^

The total consumed resources are 3641
The most demanding 10 verification tasks consumed these resources:
src/test2.dfy(2,11): 3641

What happened?

The JSON log entry for the failing assert is: ...{"filename":"test2.dfy","line":6,"col":16,"description":"assertion always holds"}...

1. Dafny's stdout says that this assertion failed. But the log doesn't give any hint about this, only that the containing verification result failed. This makes the log much less useful than it could be.

2. The JSON log gives a different location for that assertion: col 16 in the log, col 15 in stdout. So even parsing stdout would be problematic.

3. Sometimes the discrepancy between log and stdout is larger, and stdout even shows a spurious underlining for the failing assertion, so it's impossible to know where actually is the problem. I have tried to create an example showing this, but I didn't manage; so this is a real example I just got from a bigger project:

   
   file.dfy(525,61): Error: assertion might not hold
   |
   525 |       assert (st.Peek(0) == 0x44 && st.Peek(2) == dst as u256 && st.Peek(3) == src as u256 && st.Peek(4) == 0x229);
   |                                                              ^^^^^^^^^^^^^^^^^^^^^^^^^

In this case, the log reports many asserts in this line, but none is in col 61. The closest ones are -8 and +5 cols away. It's impossible to know which one is the correct one.

4. The JSON log's assertions' descriptions are always positive; that is, even if verification fails, the failing assertion has a description like "assertion always holds". This is confusing. Looks like the description is the _goal_ of the assertion, while stdout gives the _actual result_ for the assertion. Is that correct?

### What type of operating system are you experiencing the problem on?

Mac

[hmijail]

Just found the reason for point 3: if the source line is indented with tabs, then "col" counts the char offset, which doesn't correspond with the printed offset.

[atomb]

Thanks for pointing these issues out!

On (1), we should definitely update the log output to identify which assertion failed when running in the default "verify each definition in one goal" mode. If you use --isolate-assertions, the log will identify which one failed, but it really should do so in both cases.

On (2), I think there may be some differences in 0-based or 1-based column numbers. I've seen some discrepancies about that in the past.

Thanks for diagnosing (3)! That should be easily fixable.

And on (4), yes, that's intentional. The idea is that, in the log, we list all assertions, and for consistency those are presented as descriptions of the goal along with the result. When presented as an error message, however, the idea is to more clearly communicate what went wrong. One reason for this is that we aim for error messages to be as immediately understandable as possible to someone with little verification background. The log format we expect to be used by at least slightly more experienced folks for whom the idea of a goal to be proved, and that goal either succeeding or failing, has become natural. It's possible there's a better approach than what we have, though.

[hmijail]

I'll throw in a Feature Request: obviously Dafny knows the source code range to underline in stdout, while the JSON log only shows a line:col. It would be helpful if the log also contained the range.