Enable --list-harnesses flag

[jaisnan]

Description of changes:

Kani contains the harness metadata in a JSON file but it is only read temporarily before being deleted. The only way to retain this information was through the --keep-temps flag which stores these temporary files but is a bulky operation. The flag now however, does not start the verification process. The --list-harnesses flag returns a JSON string which can be consumed as an API by any receiver.

The output with the flag looks like this -
$cargo kani --enable-unstable --list-harnesses

[
  {
    "pretty_name": "check_estimate_size_2",
    "mangled_name": "check_estimate_size_2",
    "original_file": "../src/lib.rs",
    "original_start_line": 39,
    "original_end_line": 42,
    "unwind_value": null
  },
  {
    "pretty_name": "check_estimate_size",
    "mangled_name": "check_estimate_size",
    "original_file": "..src/lib.rs",
    "original_start_line": 30,
    "original_end_line": 33,
    "unwind_value": null
  }
]

Resolved issues:

Resolves #1612

Call-outs:

The flag only runs with cargo kani and not the single script kani because the cargo kani output would always be a superset of the kani output. i.e running the flag with just kani -

kani --list-harnesses test.rs

would return the regular verification output as if kani test.rs were run.

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.

[celinval]

I would expect --list-harnesses to be formatted as a user friendly output though. I would suggest to rename it to be --print-metadata or something like that if you want to keep that output.

[celinval]

Call-outs:

The flag only runs with cargo kani and not the single script kani because the cargo kani output would always be a superset of the kani output.

I don't understand what you mean here? What will happen if the user invokes:

kani --list-harnesses test.rs

You should also clarify that this will not run the verification.

[jaisnan]

Call-outs:

The flag only runs with cargo kani and not the single script kani because the cargo kani output would always be a superset of the kani output.

I don't understand what you mean here? What will happen if the user invokes:

kani --list-harnesses test.rs

You should also clarify that this will not run the verification.

Makes sense. Will clarify these in the PR.

[jaisnan]

PR came directly from a local branch by mistake.