Allow users to select a subset of harness to run

[celinval]

Description of changes:

Users can now select a subset of harnesses to run using --harness multiple times. Previously users could either run a single harness or they had to run them all.

For the example provided in #1778:

// example.rs
#[kani::proof]
fn a() {}
#[kani::proof] 
fn b() {}
#[kani::proof] 
fn c() {std::unimplemented!();}

Users can select harnesses a and b by running:

$ kani example.rs --harness a --harness b

In case of multiple matches, Kani will run all harnesses that matches at least one of the --harness argument.

Resolved issues:

Resolves #1778

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Testing:

• How is this change tested? New 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.

[jaisnan]

Awesome change! this will come in really handy for the kani extension. Could you add an example invocation of the change to the description as well?

[jaisnan]

I have a couple of non-blocking questions -

1. Does this change anything about cargo kani? It doesn't seem that way. Afaik cargo kani has the option to run multiple harnesses using cargo kani --harness ['a', 'b'] or is that not the case? (and if not, Why add this change to single file kani as opposed to cargo kani?)
2. This doesn't add the --filter [FILTER_STR] option yet, is that still coming in a future PR? That is something that could be very useful for the kani extension as well.

[celinval]

I have a couple of non-blocking questions -

1. Does this change anything about `cargo kani`? It doesn't seem that way. Afaik `cargo kani` has the option to run multiple harnesses using `cargo kani --harness ['a', 'b']` or is that not the case? (and if not, Why add this change to single file `kani` as opposed to `cargo kani`?)

2. This doesn't add the `--filter [FILTER_STR]` option yet, is that still coming in a future PR? That is something that could be very useful for the kani extension as well.

Great questions! I need to check how this argument configuration will work for configuration via Cargo.toml.

1. All the changes here should apply to cargo kani as well. I don't believe cargo kani allows you to specify multiple harnesses today.
2. Since we changed to match against substring, I don't think we need the --filter option. What do you think?

[jaisnan]

I have a couple of non-blocking questions -

1. Does this change anything about `cargo kani`? It doesn't seem that way. Afaik `cargo kani` has the option to run multiple harnesses using `cargo kani --harness ['a', 'b']` or is that not the case? (and if not, Why add this change to single file `kani` as opposed to `cargo kani`?)

2. This doesn't add the `--filter [FILTER_STR]` option yet, is that still coming in a future PR? That is something that could be very useful for the kani extension as well.

Great questions! I need to check how this argument configuration will work for configuration via Cargo.toml.

1. All the changes here should apply to `cargo kani` as well. I don't believe `cargo kani` allows you to specify multiple harnesses today.

2. Since we changed to match against substring, I don't think we need the `--filter` option. What do you think?

Substrings work great as well. Would it be possible to change the invokation to use the form --harness ['a' 'b'] format instead of --harness 'a' --harness 'b'? Seems more ergonomic but just something to maybe add in the future, not too important for now.

[adpaco-aws]

Would it be possible to change the invokation to use the form --harness ['a' 'b'] format instead of --harness 'a' --harness 'b'? Seems more ergonomic but just something to maybe add in the future, not too important for now.

I'd recommend against this.

Allowing multiple --harness arguments gives more flexibility to the user. The other problem is that characters ' and [ often need to be escaped depending on the context (the current proposal doesn't use ' as far as I know).

[celinval]

@jaisnan I totally understand your point, and I totally agree that it is painful to pass multiple --harness arguments, but I think this is more robust, as @adpaco-aws mentioned. It is also not the recommended to accept multiple values if you have positional arguments (see this doc on why). To go around this, we could consider doing one of the following:

• Create a short version of --harness, I don't know which letter to use though, since -h is help. 🙂
• We could consider using , delimiter to allow users to provide multiple arguments to --harness. So users could use --harness first,second.

[jaisnan]

I see, makes sense to me. Yeah, the second idea would be ergonomic as well, but honestly what we have works too.

[adpaco-aws]

How does this impact the features that are supposed to only work for a single harness (e.g., stubbing)? I couldn't find the code that deals with that case, apologies if I missed it.

[celinval]

How does this impact the features that are supposed to only work for a single harness (e.g., stubbing)? I couldn't find the code that deals with that case, apologies if I missed it.

It's there, but it's not pretty. I'm currently working on removing that restriction, so I didn't want to spend too much time with this.

Let me improve this to at least throw an error if more than one filter is given and if more than one harness matches the filter. Is that OK?

Also, is there any other feature besides stubbing that relies on a single harness? I remember that we used to have that restriction for concrete playback, but that's no longer the case.

[adpaco-aws]

It's there, but it's not pretty. I'm currently working on removing that restriction, so I didn't want to spend too much time with this.

Let me improve this to at least throw an error if more than one filter is given and if more than one harness matches the filter. Is that OK?

Sounds good. I don't think you need to check both conditions though, just the latter.

Also, is there any other feature besides stubbing that relies on a single harness? I remember that we used to have that restriction for concrete playback, but that's no longer the case.

I wasn't sure about concrete playback, but that's the only two that I had mind. Sorry about that.

[zhassan-aws]

Thanks for implementing this @celinval! A couple of minor comments.