Add benchcomp parser for kani perf tests

[karkhaz]

This commit adds a parser that emits CBMC-generated metrics to benchcomp. It is intended to be run in a kani checkout after running kani-perf.sh. A minimal working example would be to run benchcomp in a directory containing the following benchcomp.yaml:

variants:
  kani_0.17:
    config:
      directory: ~/src/kani
      command_line: git checkout .; git checkout kani-0.17.0 && rm -rf target && cargo build-dev && ./scripts/kani-perf.sh ; true
  kani_0.24:
    config:
      directory: ~/src/kani
      command_line: git checkout .; git checkout main; rm -rf target && cargo build-dev && ./scripts/kani-perf.sh ; true
run:
  suites:
    kani_perf:
      parser:
        module: kani_perf
      variants:
        - kani_0.17
        - kani_0.24

This commit also contains minor fixes to ensure that the test suite runs to completion even if it exited with a non-zero return code.

Testing:

• How is this change tested?

Running as indicated in the commit message should write a result.yaml file to the current directory.

• Is this a refactor change?

No

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.

[qinheping]

Can we add a test in CI to make sure the parser will not be broken by future PRs that modify Kani's output?

[karkhaz]

@qinheping I've added a unit test. Regression test has the following problems:

• Actually running kani-perf.sh seems like overkill for this regression. Is there a way to run just a single test from that suite?
• Even if we run one test, the actual metrics will be different on different machines. So we can't check the values of the metrics, we can only check that the metrics were found in the log.

If there's an easy way to write a regression test so that it passes fairly quickly, I'd be happy to do that.

[qinheping]

@karkhaz thank you for the unit test!

Actually running kani-perf.sh seems like overkill for this regression. Is there a way to run just a single test from that suite?

The current unit test check that the parser works correctly on the output given by the current Kani. I suggest to run Kani on two benchmarks (one success and one fail) and dump the output before testing the parser. For example, add the following commands in https://github.com/karkhaz/kani/blob/kk-wip-benchcomp/tools/benchcomp/test/run

kani ../../tests/kani/Unwind-Attribute/fixme_lib.rs > test/unit/kani_unwind-attribute_fixme_lib_out
kani ../../tests/kani/Arbitrary/arbitrary_impls.rs > test/unit/kani_Arbitrary_arbitrary_impls_out  

And then run the parser on kani_unwind-attribute_fixme_lib_out and test/unit/kani_Arbitrary_arbitrary_impls_out. As we can't predict the running time. Let's just check that verification_time, solver_runtime, symex_runtime are correctly parsed as numbers; and "success" is True for the kani_unwind-attribute_fixme_lib_out and is False for kani_Arbitrary_arbitrary_impls_out. We can remove the two output files after the test.

Also, do we have a plan to integrate all benchcomp tests in CI?

[zhassan-aws]

LGTM modulo @qinheping's comments.

[karkhaz]

@qinheping Thank you, I removed the unit test as it's not as useful as the regression test.

[karkhaz]

@qinheping I'll post an Action that uses this feature as soon as this is merged, blocking CI required this and the error_on_regression patch.

[qinheping]

Sounds great! Thank you @karkhaz