Use the clap derive API for the command line arguments of kani-compiler

[JustusAdam]

Description of changes:

Ideally this doesn't change Kani's behavior at all. It only changes how kani-compiler processes its command line arguments.

This is mean as code simplification and cleanup and in anticipation of factoring out UnstableAttributes into a common crate so that they can be consistently handled by the compiler and the driver.

This change is supposed to be invisible to users

Isues

Closes #1647

Call outs

I tried to make this diff as small as possible, and in the process made some decisions that I think we can debate the efficacy of. I'm not married to these decisions and I'll happily adjust them.

1. Use QueryDb as the argument struct. I think this is the most "centralized" and "canonical" way to do things, but I'm happy to make the arguments a separate struct that gets merged onto QueryDb. Although In that case I think I'd prefer to just store that arguments struct as a field in QueryDb because the code duplication would be yikes.
2. Hand QueryDb to init_*. Maybe it doesn't need full access to the DB so we could also factor the logging arguments into a small substruct and #[clap(flatten)] it.
3. I generally ignored the help fields, because clap will just use the documentation. And for that documentation I used the doc on the argument string constants or a combination of that and the doc on QueryDb because they were more elaborate. I'm happy to use a different strategy here but I also find this less important, since no user realistically is ever going to run kani-compiler manually.

Testing:

• How is this change tested? No special test necessary

• Is this a refactor change? You might say that ...

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]

Can you link with #1647 please?

[JustusAdam]

Can you link with #1647 please?

Oh damn, I probably should have run a search on issues first. Thanks for pointing it out.

[celinval]

I don't think we should merge queries and the parser. I understand that there's a lot of redundancy, but the queries represents more than just the inputs.

You could still remove redundancy by changing the query to store the arguments that were passed inside an args field.

Edit: BTW, thank you so much for changing the compiler to use clap derived! So much nicer.

[JustusAdam]

I don't think we should merge queries and the parser. I understand that there's a lot of redundancy, but the queries represents more than just the inputs.

You could still remove redundancy by changing the query to store the arguments that were passed inside an args field.

Edit: BTW, thank you so much for changing the compiler to use clap derived! So much nicer.

No problem. That's the way I'd prefer too. I used this first because it was a smaller diff but happy to pivot.

[JustusAdam]

I'm not sure what's wrong with the CI here. @feliperodri or @celinval do you have an idea why this fails? I've rerun it multiple times but it seems to have the same failure every time.

[adpaco-aws]

It looks like GitHub is failing to download some dependencies (e.g., kissat) from itself. These failures are often intermittent and it's just a matter of trying later.

[celinval]

That's awesome! Thank you @JustusAdam.