Executable trace feature

[sanjit-bhat]

Description of changes:

This PR adds the executable trace feature for improving users' debugging experience after verification failures. With the --gen-exe-trace flag, Kani will print out a Rust unit test that contains 1) concrete values for all calls to kani::any and 2) a call to the failed proof harness. The user can then debug their failing proof harness like they would with any normal Rust unit test. With an optional --add-exe-trace-to-src flag, Kani will even add the unit test directly to the user's source code.

To use this feature on a test crate:

1. Add this to your Cargo.toml:

[dev-dependencies]
kani = { path = "{path_to_kani}/library/kani", features = ["exe_trace"] }

2. Make sure your code isn't hidden under a cfg(kani) feature flag.

Resolved issues:

Implements recommended approach in #1388. Closes #1253. Closes #1317. Closes #1392. Closes #1443. Closes #1444. Closes #1445.

Call-outs:

1. New any_raw: After Deprecate any_raw and Invariant #1415, any_raw_internal will only be called on primitive types. These show up nicely in the CBMC output trace, removing the need for a complicated parser or changing the lowest level non-determinism to a byte array.
2. Performance: On the verification side, performance should stay the exact same. On the post-processing side, we only add the --trace flag to CBMC when the user runs with --gen-exe-trace. This flag adds a bit more overhead to CBMC post-processing, which scales with the length of the trace. We have been able to run this feature on fairly large traces (100s of states) without much of a noticeable performance difference.
3. slice-formula: Currently, if a variable uses a kani::any assignment, but that variable isn't present in the verification conditions, CBMC doesn't have a concrete value for it in the output trace. To fix this, we would likely need to disable --slice-formula when we run CBMC with --trace. See Enable CBMC's equation-level slicer #1252.
4. generic_const_expr: We needed this incomplete feature to take the size_of a generic type. However, after Deprecate any_raw and Invariant #1415, if we only call any_raw_internal using macros on primitive types, we could remove this and add the size as a type parameter to any_raw_internal.

Testing:

This change has an end-to-end UI test that checks to see if the correct concrete values are parsed and placed into a test case. We also manually tested this feature on a few different test harnesses. In the future, we plan to add the following tests:

1. A custom test that uses the --add-exe-trace-to-src feature and runs the unit test to verify that assertions actually fail. For now, we manually test this.
2. Unit tests for the exe_trace module in the kani-driver.

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]

First pass. Thanks for doing this! :)

[celinval]

Sorry, I know this is not ready yet for review, but I just have two comments that hopefully will help you refine this.

1. I think you still need to add implementation for some of our library functions, e.g., the kani::assert() is empty today.
2. Improve the interface to initialize the test values. See comment below.

[celinval]

Looking good. It's almost there.

I tried to only post comments on things that are user visible. I created #1481 to track the outstanding work.

Thank you!

[sanjit-bhat]

@adpaco-aws can you take a look at the changes to kani-driver/src/cbmc_output_parser.rs?

[celinval]

Awesome! We should create a section in our documentation about this feature and how to try it out. Thanks

[adpaco-aws]

You've kept the changes to the parser to a minimum. Great work!