Add unit tests for concrete playback, refactor util functions for easier testing

[jaisnan]

Description of changes:

This PR adds

1. Unit tests related to concrete playback outside of the existing regression tests.
2. Removes randomized layout and metadata as a parameter to generate the unit tests
3. Changes hash to use the pretty_name instead of the mangled_name.

Resolved issues:

Partly resolves #1502

Call-outs:

1. Thanks to @sanjit-bhat for the work in PR refactor(kani-driver, concrete_playback): process unit tests line by line, modularize functions, and add unit tests #1625
2. It changes the string that is to be hashed and added as a hash to the function. The naming schema hasn't yet changed to the user by this PR but will be in the coming few PR's.
3. The refactoring (removing dependency on metadata and randomized_layout) allows the functions to be tested and in the future, will allow the unit tests to be generated line by line.

Testing:

• How is this change tested? Unit and regression tests

• Is this a refactor change? Yes

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.

[adpaco-aws]

I've read the code but I'm still confused about the change in the function names of the tests. Are the generated unit tests runnable using these names without any modifications?

[jaisnan]

I've read the code but I'm still confused about the change in the function names of the tests. Are the generated unit tests runnable using these names without any modifications?

No, those generated unit tests are not runnable. I can make another revision fixing the names as well (will just need one more layer of formatting the names of the functions).

[celinval]

I've read the code but I'm still confused about the change in the function names of the tests. Are the generated unit tests runnable using these names without any modifications?

No, those generated unit tests are not runnable. I can make another revision fixing the names as well (will just need one more layer of formatting the names of the functions).

I love the idea of adding the name of the original harness. However, I think this new name schema will break the --inplace UX though, wouldn't it?

[jaisnan]

I've read the code but I'm still confused about the change in the function names of the tests. Are the generated unit tests runnable using these names without any modifications?

No, those generated unit tests are not runnable. I can make another revision fixing the names as well (will just need one more layer of formatting the names of the functions).

I love the idea of adding the name of the original harness. However, I think this new name schema will break the --inplace UX though, wouldn't it?

Yes, I am trying to find a way to make the UX work, but if not, I'll just go back to the old naming scheme.

[celinval]

Can you remove all the modules and only keep the function name?

[celinval]

That's awesome. Thanks @jaisnan

Once you merge this, can you please update our documentation as well to reflect the new convention please?

[zhassan-aws]

Since the PR changes the name of concrete playback tests, the PR title should mention that.

[celinval]

BTW, can you please either extend an existing test or add a new test for the new name schema? Thanks

[zhassan-aws]

I'm a bit confused about the description in the PR:

Functions weren't given their scope prefixes before which lead to multiple generated unit tests in the same file being called "kani_concrete_playback_harness", which is confusing to the user. This change renames them to use their scope as prefixes if available (using the "pretty name"). For example - "kani_concrete_playback_second::harness".

Can you clarify with an example?