Add run_command benchcomp visualization

[karkhaz]

This allows users to write their own custom visualization script to run after running the benchmarks. Prior to this commit, visualizations had to be checked into the Kani repository.

When run_command is specified as a visualization, benchcomp runs the specified command and passes the result of the run as a JSON file on stdin. The command can then process the result however it likes.

This resolves #2518.

Testing:

• How is this change tested?

2 new regression tests

• 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.

[karkhaz]

(Note that the doc text for run_command will automatically get rendered into the visualizations section of the Kani book.)

[celinval]

(Note that the doc text for run_command will automatically get rendered into the visualizations section of the Kani book.)

That's a neat idea. Do you have an example from your repo on how that would look like?

[karkhaz]

That's a neat idea. Do you have an example from your repo on how that would look like?

In this file (the same file as in this PR, you can also just expand the diff downwards) there are three classes. Each of them has a doc text, and those three doc texts are what get rendered into the three visualization documentations in the kani book

[celinval]

That's a neat idea. Do you have an example from your repo on how that would look like?

In this file (the same file as in this PR, you can also just expand the diff downwards) there are three classes. Each of them has a doc text, and those three doc texts are what get rendered into the three visualization documentations in the kani book

I was wondering if you have the link to the rendered version that includes your PR changes. You can enable the documentation to be built in your fork, so it is easy to review documentation changes. For example, here is the link for my fork's documentation: https://celinval.github.io/kani-dev/

The only thing is that those changes have to be made to your fork's main branch.

[karkhaz]

You can enable the documentation to be built in your fork

Awesome, thank you! I'll do that from now on. Here's how it looks:

https://karkhaz.github.io/kani/benchcomp-conf.html#run_command