refactor(kani-driver, concrete_playback): process unit tests line by line, modularize functions, and add unit tests

[sanjit-bhat]

Description of changes:

This PR does the following:

1. It refactors the kani-driver concrete playback code to generate/process unit tests line by line. As discussed with @celinval, this is a more intuitive/clean way to do things.
2. It moves the following functionality out of the KaniSession functions: 1) generating rustfmt args, 2) writing the new src code to a tmp file, 3) extracting the parent directory and source file from a file path.
3. It adds unit tests for kani-driver concrete playback functions that live outside KaniSession.

Note: I'm about to start PhD research next week, so trying to finish up some Kani PRs before then:)

Call-outs

1. This should probably be reviewed by at least @celinval.
2. @adpaco-aws, you might want to look at the unit test for the concrete vals extractor. Maybe we can generalize that by making mock initializations for some of the CBMC output parser structs?

Resolved issues:

Resolves #1502.

Testing:

• How is this change tested? Added kani-driver unit tests for 1) the formatting functions that generate the concrete playback unit test, 2) a file path helper function, 3) the concrete vals extractor.

• Is this a refactor change? Yes

Checklist

• [x] Each commit message has a non-empty body, explaining why the change was made
• [x] Methods or procedures are documented
• [x] Regression or unit tests are included, or existing tests cover the modified code
• [x] 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.

[sanjit-bhat]

@celinval did you get a chance to look at this PR?

[celinval]

Sorry @sanjit-bhat, I was out of the office. I'll take a look at it tomorrow!

[rahulku]

@celinval @sanjit-bhat - is this still active?

[sanjit-bhat]

Not currently, but I think it's fairly close to being ready to go. @celinval how close do you think it is?

I can take a look at the comments tomorrow, but there may be parts of the code that've changed since I last looked.

[sanjit-bhat]

Update: will only be able to get to this over the upcoming weekend.

[celinval]

Let me take a look at it tomorrow. But I think @sanjit-bhat is right, this should be close. I don't think the changes were that bad, so hopefully merging with main will be ok

[jaisnan]

The changes suggested here have been merged in other PR's referred above with modifications. I think this issue can be closed. Thanks @sanjit-bhat for your work!