Add --exact flag

[jaisnan]

Description of changes:

When the user calls kani with a command cargo kani --harness module::check_blah --exact and they want to specify which harness to match, using --exact, they can prevent multiple harnesses from being run. The user will need to specify the harness name by using the fully qualified name as well.

Resolved issues:

Resolves #2285

Call-outs:

If the user adds --exact and they want to run kani on multiple harnesses, they will need to provide the specific name for every harness.

Testing:

• How is this change tested? Unit and regression change

• 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.

[zhassan-aws]

Thanks @jaisnan! I was expecting to see at least one test with two or more harnesses where the name of one harness is a substring of the other, and --exact --harness is used for selecting the one that is a substring while making sure the other one is not selected.

[celinval]

It looks good. Just a few minor comments.

I do wonder if we should fail in the case where an exact match was not found. I don't think rust tests fail, but they also don't fail when a filter has no match.

@adpaco-aws might have an opinion about this one. @jaisnan do you have any preference?

[celinval]

Thanks @jaisnan! I was expecting to see at least one test with two or more harnesses where the name of one harness is a substring of the other, and --exact --harness is used for selecting the one that is a substring while making sure the other one is not selected.

I think the test tests/ui/exact-harness/some_matching_harnesses/subset.rs was design to test that, but I don't think it is quite testing it yet.

[adpaco-aws]

I do wonder if we should fail in the case where an exact match was not found. I don't think rust tests fail, but they also don't fail when a filter has no match.

@adpaco-aws might have an opinion about this one.

Yes, I do. We should fail in that case. In addition to "catch" mistakes from users, it'll also be helpful to detect issues with target selection on the VSCode extension.

[celinval]

We should consider adding the number of ignored harnesses to the summary. But that's out of the scope of this change. Thanks Jai

Actually, we're still missing the failure when an exact match was not found.

[jaisnan]

@celinval I've added the error when an exact match is not found.

[zhassan-aws]

Thanks @jaisnan!