Fix output parsing when using debugger

[jaisnan]

Description of changes:

The first object returned is now a non-JSON version string line from Kani. This is a result of the change from model-checking/kani#2619.

This PR adds a fix to the output parsing when parsing the JSON objects in debugger mode.

Call-outs:

1. This is a temporary patch while Kani concrete-playback --json-ui gives a non-json response kani#2649 is fixed from Kani's side.

Testing:

• How is this change tested?

• Is this a refactor change?

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

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

[adpaco-aws]

What makes it non-JSON? I don't understand why this is needed, can you show an example?

[jaisnan]

What makes it non-JSON? I don't understand why this is needed, can you show an example?

Here is a sample array of objects that is returned from Kani

0:
'Kani Rust Verifier 0.33.0 (cargo plugin)'
1:
{"reason":"compiler-message","package_id":"sample-coverage 0.1.0 )","manifest_path":"...","target":{"kind":["bin"],"crate_types":["bin"],"name":"sample-coverage","src_path":"/Users/jaisnan/Desktop/temp/sample-coverage/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: unused variable: `y`\\n  --> src/main.rs:44:9\\n   |\\n44 |     let y = est…hlight_start":9,"text":"    let y = estimate_size(x);"}]}]}],"code":{"code":"unused_variables","explanation":null},"level":"warning","message":"unused variable: `y`","spans":[{"byte_end":776,"byte_start":775,"column_end":10,"column_start":9,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":44,"line_start":44,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":10,"highlight_start":9,"text":"    let y = estimate_size(x);"}]}]}}
2:
{"reason":"compiler-message","package_id":"sample-coverage 0.1.0 ","manifest_path":"...","target":{"kind":["bin"],"crate_types":["bin"],"name":"sample-coverage","src_path":"/Users/jaisnan/Desktop/temp/sample-coverage/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: 1 warning emitted\\n\\n","children":[],"code":null,"level":"warning","message":"1 warning emitted","spans":[]}}'
3:
{"reason":"compiler-artifact","package_id":"sample-coverage 0.1.0 ","manifest_path":".../Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"sample-coverage","src_path":"/Users/jaisnan/Desktop/temp/sample-coverage/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":true},"features":[],"filenames":[".../sample_coverage-e06b8dc25d1abcec"],"executable":"../sample_coverage-e06b8dc25d1abcec","fresh":true}'
4:
{"reason":"build-finished","success":true}

as you can see, the first object is always a string showing Kani's version number in a non-JSON format. Even with --message-format=JSON, we get a non-JSON string, so to avoid parsing it and causing errors, I am simply discarding the first element away since we know that the first element is always the Kani-version string.

If needed, I could make the handling more robust but I think the hack is sufficient for fixing the issue.

[adpaco-aws]

But we don't have a minimum version check in the VS Code extension, right? Some users may have a previous version and then they'll miss the first object because of this hack.

[adpaco-aws]

Or maybe you can fix this on Kani's end?

[jaisnan]

In this particular case, this should be backwards compatible as well since we only use the last but one JSON blob from Kani. That blob contains the path for the debugger executable. So, missing the first object is not a problem.

I think we can and should fix it on Kani's end, but till then, this hack allows users of Kani 0.33 as well to use the debugger.

[adpaco-aws]

Please check that this works for previous versions of Kani and create an issue to get it fixed on Kani's end to remove this change. Link the issue above it.