Add --manifest-path and --features #2085

tedinski · 2023-01-06T00:12:39Z

Description of changes:

Add the two flags, resolving the feature requests below.
Clap's parse_from calls exit on failure, so fix all tests to use try_parse_from().unwrap() (to panic instead of exit), otherwise the test suite runner can't handle failure properly.
Use clap's derive more precisely: not everything is a Parser, some are just Subcommand or Args
Refactor the cargo args together into a separate structure
The test for --manifest-path requires more scripty tests. Compiletest mode for executing arbitrary commands #2059 continues to be a need :(

Resolved issues:

Resolves #1420
Resolves #1979

Call-outs:

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.

scripts/kani-regression.sh

…-path

celinval

Thanks for fixing the issue with the manifest flags.

kani-driver/src/args.rs

celinval · 2023-01-10T22:15:27Z

kani-driver/src/args.rs

@@ -273,6 +266,51 @@ impl KaniArgs {
    }
 }

+/// Arguments that Kani pass down into Cargo essentially uninterpreted.
+/// These generally have to do with selection of packages or activation of features.
+/// These do not (currently) include cargo args that kani pays special attention to:


maybe say "these should not include"

Should it? I wasn't sure. I didn't want to make too strong of a statement if we decide otherwise later except someone sees this comment and wonders "well, why not?"...

I think if we decide the other way around, we can always update the comments. I don't think writing it here is a one-way door. But I do think that this leaves space for inconsistency.

I do think it would be odd to have a cargo argument being called as part of standalone kani flow. If we want to move stuff here, I would expect a counter part StandaloneArgs that basically duplicate the things that are relevant to both.

I think you misunderstood the comment? It's not about kani vs cargo-kani, it's about cargo args that kani is interpreting (hence the examples like --target-dir) versus those that we just kinda pass down.

ok, I literally just said "kani is interpreting" again, which was maybe the confusion (between kani-the-project, and kani-the-binary)

"It's about cargo args that we are interpreting... versus those that we just pass down"

I was actually wondering if this should be part of CargoKaniArgs instead of KaniArgs? None of these flags make sense in the standalone version, right?

Correct, but this PR doesn't change that yet. There's more extensive work needed (e.g. in how arguments get plumbed through the session) to do that.

celinval · 2023-01-10T22:17:57Z

kani-driver/src/args.rs

+    /// Do not activate the `default` feature
+    #[arg(long)]
+    pub no_default_features: bool,
+    // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach...


why can't we use: https://docs.rs/clap/4.0.32/clap/struct.Arg.html#method.value_delimiter?

I don't think that supports multiple delimiters?

But why do you want to support multiple delimeters? Don't we want to only support comma or multiple usage of the same argument?

well, cargo says it does?

cargo build --help ... -F, --features <FEATURES> Space or comma separated list of features to activate

I see. You want to keep the same format as cargo. We should probably document the exact behavior in this case. Maybe say that comma is preferred.

Note that clap mentions that we shouldn't really be accepting options with multiple arguments and positional arguments:

A common mistake is to define an option which allows multiple values and a positional argument.

from: https://docs.rs/clap/4.0.32/clap/builder/struct.Arg.html#examples-20

I was wondering if explicitly setting the separator to ',' would fix this issue, but clap seems to just join all the space separated arguments into one. 🤦‍♀️

Maybe say that comma is preferred

I already set our help text to just say comma, since I thought spaces was an odd choice.

BTW, if you want to match the cargo behavior, I believe you should set the action to append.

?? There's a test below showing it behaving how I expect?

Cool. From reading the docs I thought that Set was the default

celinval · 2023-01-10T22:24:12Z

kani-driver/src/call_cargo.rs

@@ -66,9 +60,20 @@ impl KaniSession {
        let rustc_args = self.kani_rustc_flags();

        let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
-        if self.args.all_features {
+        if let Some(path) = &self.args.cargo.manifest_path {


Any chance this can be auto generated? So we don't need to change two files whenever we just want to pass down the arguments?

I didn't see any way to reverse the parsed args back into a vector, if that's what you mean. (I agree it'd be nice.)

I think at least creating a method that converts them might be nice. Not a blocker though.

kani-driver/src/args.rs

celinval · 2023-01-10T22:28:12Z

kani-driver/src/call_cbmc.rs


        let harness_none = mock_proof_harness("check_one", None, None);
        let harness_some = mock_proof_harness("check_one", Some(3), None);

+        fn resolve(args: &[&str], harness: &HarnessMetadata) -> Option<u32> {


Not for this PR, but I was wondering if we could stop calling the parser as part of these unit tests.

scripts/kani-regression.sh

celinval

My other comments are nice to have, not blockers.

Add --manifest-path and --features

43e2c1c

tedinski requested a review from a team as a code owner January 6, 2023 00:12

celinval reviewed Jan 6, 2023

View reviewed changes

scripts/kani-regression.sh Outdated Show resolved Hide resolved

tedinski added 3 commits January 9, 2023 18:28

Merge remote-tracking branch 'origin/main' into manifest-features

bae5504

Fix cargo_locate_project to account for the possibility of --manifest…

c3e3c40

…-path

clippy fix

19eddf0

celinval reviewed Jan 10, 2023

View reviewed changes

tedinski added 2 commits January 11, 2023 16:35

put path in variable

5c8cd71

Merge remote-tracking branch 'origin/main' into manifest-features

42929fd

tedinski force-pushed the manifest-features branch from 6a1dfe8 to 42929fd Compare January 11, 2023 16:36

celinval approved these changes Jan 11, 2023

View reviewed changes

tedinski added 2 commits January 11, 2023 18:16

Merge branch 'main' into manifest-features

a68d4c3

Merge branch 'main' into manifest-features

37af95e

tedinski merged commit 29dd214 into model-checking:main Jan 12, 2023

tedinski deleted the manifest-features branch January 12, 2023 16:37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add --manifest-path and --features #2085

Add --manifest-path and --features #2085

tedinski commented Jan 6, 2023

celinval left a comment

celinval Jan 10, 2023

tedinski Jan 11, 2023

celinval Jan 11, 2023

tedinski Jan 11, 2023

tedinski Jan 11, 2023

celinval Jan 11, 2023

tedinski Jan 11, 2023

celinval Jan 10, 2023 •

edited

Loading

tedinski Jan 11, 2023

celinval Jan 11, 2023

tedinski Jan 11, 2023

celinval Jan 11, 2023

tedinski Jan 11, 2023

celinval Jan 11, 2023

tedinski Jan 11, 2023

celinval Jan 12, 2023

celinval Jan 10, 2023

tedinski Jan 11, 2023

celinval Jan 11, 2023

celinval Jan 10, 2023

celinval left a comment

Add --manifest-path and --features #2085

Add --manifest-path and --features #2085

Conversation

tedinski commented Jan 6, 2023

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval Jan 10, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

celinval Jan 10, 2023 •

edited

Loading