Support verification logs in JSON format

[atomb]

Summary

Add support for providing JSON logs of verification results.

Background and Motivation

Verification results are naturally at least a little hierarchically structured, and a natural fit for JSON. The text and csv loggers are human-optimized and lossy, respectively. Both of these are sub-optimal for machine processing of all verification output.

Proposed Feature

It would be very useful to have a --log-format json with a machine-readable version of what shows up in --log-format text.

Alternatives

There's also a trx format (using a specific XML schema), which supports more information, and more hierarchical structuring, than the csv output format. However, it's somewhat complex and rigidly oriented toward test results (even though it's extensible enough to capture many aspects of verification results).

[hmijail]

Is there any explanation about what makes the CSV logger "lossy", and what is gained by going the JSON route?
I have existing scripts working on the CSV files, so I wonder if it'd make sense to change them to JSON.

[hmijail]

My own notes, in case it helps those googling...

JSON keeps most the information from the .text, only in a structured way.
Things that are not kept: until now I only noticed the "maximum assertion batch time / resource count".
The CSV in turn loses the hierarchical structure that is kept in the text and JSON.
So, what previously needed a CSV log for coarse detail and then a text log + manual inspection to drill down to finer detail, now can all be gathered together from a single JSON log.

What is called "Assertion Batch" in both the text and the CSV formats is called "vcNum" in the JSON. (Looks like "Assertion Batch" and "Verification Condition" are used more or less interchangeably)

[atomb]

My own notes, in case it helps those googling...

JSON keeps most the information from the .text, only in a structured way. Things that are not kept: until now I only noticed the "maximum assertion batch time / resource count". The CSV in turn loses the hierarchical structure that is kept in the text and JSON. So, what previously needed a CSV log for coarse detail and then a text log + manual inspection to drill down to finer detail, now can all be gathered together from a single JSON log.

What is called "Assertion Batch" in both the text and the CSV formats is called "vcNum" in the JSON. (Looks like "Assertion Batch" and "Verification Condition" are used more or less interchangeably)

Yes, that's all exactly right. We support CSV because it's quite convenient for a lot of statistical analysis processes, and is generally very easy to do quick queries on, import into spreadsheets, etc. But if you're building something custom, and importing JSON is easy, then it's probably the way to go.

And thanks for noting the terminology differences. I think we could make things easier to understand by making those consistent.

[hmijail]

I found another difference: verificationResult.outcome is "Correct", but verificationResult.vcResult[].outcome is "Valid".
Maybe it makes sense to have it that way, but then it'd be great to have a JSON schema to know what to expect. (Else, one has to always be on the lookout for unexpected values)

[hmijail]

Looks like in both positions the alternative is "OutOfResource"?
For comparison, in CSVs, TestResult.Outcome for the same verifications seems to be Passed/Failed.