Unsound command line options should be documented and warnings given when used.

[jimgrundy]

The --reachability-slice option (and other slices) produce results that are unsound.

This request has two parts:
1/ All command line options that can produce unsound results should be clearly marked as such in the command's help.
2/ Any command run with an unsound command line option should produce in the output a warning indicating that the results are unsound and which option(s) are the reason for the potential unsoundness.

[martin-cs]

@jimgrundy I very much agree with the principle but none of the slices should produce unsound results, esp. --reachability-slice. If you have the time to file a bug report for what is going wrong, that would be great.

[martin-cs]

Ah, is #6394 what prompted this?

[jimgrundy]

Not directly, but yes via internal chats that led up to #6394. @kroening said that the slicers were not sound and should not be used. My feeling is that if there are command line options that we know might produce unsound results then that needs to be documented and warned. You might have to follow up with @kroening for examples of unsound slicers beyond those reported in #6349 and #260.

[martin-cs]

Perhaps it is useful to draw a distinction between:

A. Functionality that is (intentionally or unintentionally) unsound by design / choice of algorithm,
and
B. Functionality that is in-principle sound but has known or suspected issues of correctness.

A. we should definitely warn for, B. we should work towards eliminating.

As far as I know, issues with the slicers are of type B. They are just waiting on someone having time to fix them.

[martin-cs]

In the case of #260 I would be tempted to try re-running the benchmarks because I know there have been bug fixes to that code in the ... 5 years since it was first reported.

[jimgrundy]

I agree with @martin-cs on A vs B in principle, but if the time in which issues in class B lie around is measured in years rather than weeks then we risk having folks using these features and thinking they have proofs of production code when they do not. One suggestion would be to rename "--feature-X" to "--experimental-feature-X" until soundness queries are resolved. That would at least convey that feature-X is supposed to be sound, but I wouldn't bank on it just yet.

[martin-cs]

It's not unreasonable that "this should work but ... last I checked it didn't" should be somewhere other than in the heads of a few developers and implied by the bug tracker.

Renaming options is always awkward. What I wonder is whether we need a "--sound-options-only" or "--no-experimental" flag that will conflict if given with anything not on a white-list of options. Test coverage and no option bugs seem like a good criteria for adding things to the white-list.

I guess underlying this is one of Daniel's long-standing design goals which was to minimise the number of flags, esp. those that set magic constants. Over the last few years we haven't done as well at this as we should do.

[jimgrundy]

I like this last idea, but I would like to flip the sense. The tool should be presumed sound by default, so rather than having a "--forbid-stuff-we-dont-think-is-sound" option, those should be forbidden by default and the options should be "--experimental" (i.e. --allow-stuff-we-dont-think-is-sound").

[martin-cs]

Yes; you are right that's a better solution. --I-accept-this-might-give-wrong-answers?

[jimgrundy]

It looks like our desire is this:

1. Add a --unsound flag, that allows intentionally unsound options
2. Add a --experimental flag, that allows options that we want to be sound, but aren't confident in
3. Using any option that is intentionally unsound should get you a warning unless you used the --unsound flag.
4. Using any option that should be sound but we aren't confident in should get you a warning unless you used the --experimental flag
5. In a future major release those warnings should become errors

[jimgrundy]

Happy to close this and pick up the discussion over on #6480