Move common arguments to their own structure

[celinval]

Description of changes:

This is a pre-work needed for implementing #2440 as a subcommand. Today, the only other subcommand we have is assess and the way it takes arguments is rather broken as explained in #1831.

For the playback sub-command, I expect that we will need at least CargoArgs and CommonArgs to control the build process and to control the process verbosity.

We would probably benefit from properly isolating the build arguments, and not allowing arguments when subcommands are provided, but that will be a problem for another day since it will require changes to assess logic and Kani sesssion. I am hoping this will be enough for a first working version of the playback subcommand (famous last words... 🙂).

Resolved issues:

Related to #2440

Related RFC:

Call-outs:

I created an args/ folder for all argument related logic because I believe it will be easier to maintain and it creates a better separation of responsibility and cleaner dependency tree (i.e.: args module no longer depends on assess module).

Update: I'll probably need to create one more PR that enables args_conflicts_with_subcommands to fix the issue with the argument position.

Testing:

• How is this change tested?

• Is this a refactor change?

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.

[jaisnan]

Question 1: This change is a simple refactor to put all the args into two structures, one for common ones (Which will be used by the subcommands) and one structure for the verification related arguments, am i understanding that correct?

Question 2: The plan to have two subcommands (assess and concrete-playback) and one default one for verify after this PR, is that correct? That makes sense. Does this also mean that running concrete-playback, will block the verification flow and just print the unit test after the coming PR?

Question 3: I didn't understand the motivation behind removing --dry-run in the test case. Is it because you moved it into the ValidateArgs and so dry-run doesn't work now as expected, but it will with the upcoming PR?

[jaisnan]

Looks like a re organization, so I'm approving with a few questions. Thanks!

[celinval]

I have just one comment, which is about the regression test that was changed. I didn't understand the motivation behind removing --dry-run. Is it because you moved it into the ValidateArgs and so dry-run doesn't work now as expected, but it will with the upcoming PR?

Great question! The test at hand had two errors:

1. Conflicting unwinding arguments (which is what we want to test).
2. Use of --dry-run which has been removed already.

Before this change, we checked # 1 first, then we checked # 2. With this change, the order has changed, and the test was failing now because of # 2. So I removed the --dry-run argument so it still tests # 1.

[celinval]

Question 1: This change is a simple refactor to put all the args into two structures, one for common ones (Which will be used by the subcommands) and one structure for the verification related arguments, am i understanding that correct?

Yes! I was thinking that we could even add a subcommand verify, which is the default one when no subcommand is given.

Question 2: The plan to have two subcommands (assess and concrete-playback) and one default one for verify after this PR, is that correct? That makes sense. Does this also mean that running concrete-playback, will block the verification flow and just print the unit test after the coming PR?

Oh, I guess you already answered the first question here. 😉 So the testcase generation won't change, and it will still be part of the "verify" subcommand. The new playback subcommand will compile and run this testcase.

Question 3: I didn't understand the motivation behind removing --dry-run in the test case. Is it because you moved it into the ValidateArgs and so dry-run doesn't work now as expected, but it will with the upcoming PR?

Per my previous answer, --dry-run doesn't work today. We should really just remove it completely, but I didn't want to make that change as part of this PR.