Clean up benchmark directories after building

[karkhaz]

Description of changes:

This commit makes benchcomp delete fresh copies of benchmark directories after running the benchmark suite, by default. This is to save disk space, especially on CI machines which do not have enough disk space to run the perf suite. The new behavior can be turned off with the new --no-cleanup-run-dirs flag.

Resolved issues:

N/A

Related RFC:

N/A

Call-outs:

Here is a run where the benchcomp job succeeds after deleting the stale benchmark repos.

Testing:

• How is this change tested?

Ran in CI

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

[celinval]

Sorry, it's not clear to me what this is actually cleaning and when. Can you please clarify?

In order to test this, I think we need to compare two versions of Kani that use a different toolchain. I think that is the main problem, probably because each toolchain takes around 2GB of disk.

[karkhaz]

Sorry, it's not clear to me what this is actually cleaning and when. Can you please clarify?

If you have a benchmark directory foo and configure benchcomp to run it twice with two different toolchains, benchcomp does not actually run the command inside foo. Instead it copies foo to a temporary location for each toolchain, and runs the command inside there. Previously benchcomp was not deleting these copies.

So for the kani-perf suite, in the CI machine, kani gets cloned, and then benchcomp makes two more copies of it to run with the old and new toolchain... and each of those copies of kani contain the whole git history and object files etc.

(I had previously considered making benchcomp ignore .git, but it turns out that for some repositories, the benchmark suite uses git for various reasons like finding the root of the repository etc).