Enable -Z stubbing and error out instead of ignore stub

[celinval]

Description of changes:

Enable -Z stubbing, deprecate --enable-stubbing, and emit an error if the user tries to verify a harness that has stubs without explicitly enabling stubs. This used to be a warning before which was easy to miss. It was also hard to debug when the harness would take a while to run.

Resolved issues:

Resolves #ISSUE-NUMBER

Related RFC:

Optional #ISSUE-NUMBER.

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.

[tautschnig]

There are a number of tests that have enable-stubbing in their Cargo.toml files. Will these tests still work (without issuing a warning)?

[celinval]

There are a number of tests that have enable-stubbing in their Cargo.toml files. Will these tests still work (without issuing a warning)?

They will emit a warning but the test shouldn't fail because of that. I can modify them in this PR If you prefer

[tautschnig]

There are a number of tests that have enable-stubbing in their Cargo.toml files. Will these tests still work (without issuing a warning)?

They will emit a warning but the test shouldn't fail because of that. I can modify them in this PR If you prefer

If we are deprecating a feature then, yes, I think we should completely remove its use from our repository.

[celinval]

@tautschnig just checking if you are planning on reviewing this PR or should I ping anyone else? Thanks!

[JustusAdam]

We should probably do a similar thing for the compiler. It also tracks stubbing differently from unstable features for some reason and it's quite confusing.

Also we could consider factoring the whole "unstable features" stuff out into a crate that is common between driver and compiler so we don't have to reimplement it twice for every feature.

[celinval]

We should probably do a similar thing for the compiler. It also tracks stubbing differently from unstable features for some reason and it's quite confusing.

Ah, do you mean replace the --enable-stubbing from the compiler as well and just use the unstable flag that is already passed? I can do that. The reason is legacy code. The stubbing RFC came before the unstable API RFC. =)

Also we could consider factoring the whole "unstable features" stuff out into a crate that is common between driver and compiler so we don't have to reimplement it twice for every feature.

I do think having a crate just for the "unstable features" stuff is a bit overkill, but we have been talking about creating a kani_common crate. Just didn't have the time to do that.

[JustusAdam]

We should probably do a similar thing for the compiler. It also tracks stubbing differently from unstable features for some reason and it's quite confusing.

Ah, do you mean replace the --enable-stubbing from the compiler as well and just use the unstable flag that is already passed? I can do that. The reason is legacy code. The stubbing RFC came before the unstable API RFC. =)

Also we could consider factoring the whole "unstable features" stuff out into a crate that is common between driver and compiler so we don't have to reimplement it twice for every feature.

I do think having a crate just for the "unstable features" stuff is a bit overkill, but we have been talking about creating a kani_common crate. Just didn't have the time to do that.

I actually already wrote the code for that and then realized it'd work best if we refactored the compiler args to use clap deriving also so I opened #2689

[celinval]

We should probably do a similar thing for the compiler. It also tracks stubbing differently from unstable features for some reason and it's quite confusing.

Ah, do you mean replace the --enable-stubbing from the compiler as well and just use the unstable flag that is already passed? I can do that. The reason is legacy code. The stubbing RFC came before the unstable API RFC. =)

Also we could consider factoring the whole "unstable features" stuff out into a crate that is common between driver and compiler so we don't have to reimplement it twice for every feature.

I do think having a crate just for the "unstable features" stuff is a bit overkill, but we have been talking about creating a kani_common crate. Just didn't have the time to do that.

I actually already wrote the code for that and then realized it'd work best if we refactored the compiler args to use clap deriving also so I opened #2689

Ok. So I won't do that in this PR. Thanks @JustusAdam

[JustusAdam]

Ok. So I won't do that in this PR. Thanks @JustusAdam

Thanks. I work fast when I get annoyed by something 😂

Looks good to me otherwise

[adpaco-aws]

This makes sense to me, thanks @celinval !

One question: Are we tracking the removal of this feature somewhere? I don't think we have a mechanism in place to keep track of deprecated feature and when their removal is estimated to occur.