Parse log file of multi-threaded Kani run (terse output) into JSON

[tautschnig]

Given a run of Kani on the standard library with --jobs=<N> --output-format=terse (and, typically, autoharness) enabled this produces a machine-processable JSON result via

python3 log_parser.py \
  --kani-list-file kani-list.json \
  --analysis-results-dir std_lib_analysis/results/ \
  verification.log -o results.json

where each entry in the resulting JSON array is of the form

{
  "thread_id": int,
  "result": {
    "harness": string,
    "is_autoharness": bool,
    "autoharness_result": string,
    "with_contract": bool,
    "crate": string,
    "function": string,
    "function_safeness": string,
    "file_name": string,
    "n_failed_properties": int,
    "n_total_properties": int,
    "result": string,
    "time": string,
    "output": array
  }
}

With the help of jq one can then conveniently compute various metrics, e.g.,

jq 'map(select(.result.result == "SUCCESSFUL" and
               .result.is_autoharness == true and
               .result.crate == "core" and
               .result.function_safeness == "unsafe" and
               .result.with_contract == true)) | length' results.json

to find the number of successfully-verified contracts of unsafe functions in crate core that were verified using automatically generated harnesses.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[carolynzech]

Thanks Michael! It looks like these results will be very useful. My comments can be summarized as:

1. asking for a bit more inline documentation, especially where we're doing some hardcoding to get around edge cases, and
2. whether we should try to avoid duplicate dictionary keys

[qinheping]

Can we have some unit tests for this Parser? Or is it tested with any existing test?

[tautschnig]

Requires a more recent Kani version for CI to pass.