Built-in checks can optionally be fatal

[tautschnig]

With a new option --assert-then-assume each built-in check (assertion) is followed by an assumption. For Kani, this will enable more consistent behaviour, and it may give us an additional way to produce "fatal assertions" as proposed in #8226.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 88.88889% with 1 lines in your changes are missing coverage. Please review.

Project coverage is 79.66%. Comparing base (689c552) to head (eb48d8b).

Files	Patch %	Lines
src/ansi-c/goto_check_c.cpp	88.88%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8242   +/-   ##
========================================
  Coverage    79.66%   79.66%           
========================================
  Files         1682     1682           
  Lines       195544   195547    +3     
========================================
+ Hits        155771   155776    +5     
+ Misses       39773    39771    -2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[kroening]

I strongly advise against this. As mentioned in the comments to #8226, this is a significant soundness risk, and I'd much rather like to work towards soundness.

[celinval]

I strongly advise against this. As mentioned in the comments to #8226, this is a significant soundness risk, and I'd much rather like to work towards soundness.

What if this option flips all passing assertions to undetermined? One of the reasons we decided to follow this design opposed to what is proposed in #8226 in Kani is to reduce the amount of noise that a failing assertion can cause. The idea is to fail fast to help the user to debug their code.

[kroening]

What if this option flips all passing assertions to undetermined? One of the reasons we decided to follow this design opposed to what is proposed in #8226 in Kani is to reduce the amount of noise that a failing assertion can cause. The idea is to fail fast to help the user to debug their code.

If the goal is to reduce noise from downstream assertions that are failing, I'd recommend making those "undetermined" via the mechanism in #8226. The reason why I didn't is subtle, and as follows. You can have two assertions that are downstream of each other. The problem is then that it's arbitrary which one you mark as failing, and which one you mark as undetermined.

[celinval]

What if this option flips all passing assertions to undetermined? One of the reasons we decided to follow this design opposed to what is proposed in #8226 in Kani is to reduce the amount of noise that a failing assertion can cause. The idea is to fail fast to help the user to debug their code.

BTW, I was wrong, we haven't actually implemented this yet in Kani, and only in a few cases, but not UB, we modify the status of a passing assertion. So this issue was a good reminder for us to do that. :)

If the goal is to reduce noise from downstream assertions that are failing, I'd recommend making those "undetermined" via the mechanism in #8226. The reason why I didn't is subtle, and as follows. You can have two assertions that are downstream of each other. The problem is then that it's arbitrary which one you mark as failing, and which one you mark as undetermined.

Totally. In that case you would have to inspect the trace to know which one failed first.

[kroening]

Totally. In that case you would have to inspect the trace to know which one failed first.

I am considering this.

[kroening]

On this PR self: please also remember that the assertions that we generate can't be assumed; they use nondeterminism. As a consequence, you may still receive counterexamples that are spurious.

[tautschnig]

Closing given points raised in the discussion in here.