Create a playback command to make it easier to run Kani generated tests

[celinval]

Description of changes:

Introduce the unstable subcommand playback to allow users to easily compile and run their test cases that were generated using Kani's concrete playback feature.

This is the help for this subcommand (I redacted the details of options that already exist today):

Execute concrete playback testcases of a local package

Usage: cargo-kani playback [OPTIONS] --test <TEST>

Options:
      --debug
          (...)

      --test <TEST>
          Specify which test will be executed by the playback args

      --message-format <MESSAGE_FORMAT>
          Control the subcommand output
          
          [default: human]

          Possible values:
          - human: Print diagnostic messages in a user friendly format
          - json:  Print diagnostic messages in JSON format

Resolved issues:

Resolves #2440
Resolves #1441
Resolves #1581

Related RFC:

N/A

Call-outs:

1. I will update the documentation in a separate PR.
2. This PR likely fixes issue Concrete playback needs tweak for harnesses under cfg(test) #1577 but I haven't tested it yet, so I'm not claiming victory.
3. Note that we have to include a second sysroot as part of our release.

Testing:

• How is this change tested? New unit tests and end to end 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.