introduce 'fatal assertions' #8226

kroening · 2024-03-03T23:01:16Z

This introduces a variant of ASSERT instructions that are fatal when they are refuted. Execution paths through fatal assertions that are refuted are undefined. Assertions that (otherwise) pass and that are reachable from a refuted fatal assertion are now reported as UNKNOWN.

The motivating use-case for fatal assertions is undefined behavior in languages such as C/C++ or Rust.

Each commit message has a non-empty body, explaining why the change was made.
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 · 2024-03-04T00:03:04Z

Codecov Report

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

Project coverage is 78.37%. Comparing base (41496b9) to head (3cdd832).

Files	Patch %	Lines
src/goto-checker/fatal_assertions.cpp	77.96%	13 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8226      +/-   ##
===========================================
+ Coverage    77.96%   78.37%   +0.40%     
===========================================
  Files         1720     1721       +1     
  Lines       188982   188083     -899     
  Branches     18391    18452      +61     
===========================================
+ Hits        147347   147404      +57     
+ Misses       41635    40679     -956

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

peterschrammel · 2024-03-09T16:18:09Z

Is UNKNOWN the right status here? Or should there are rather be a new status UNDEFINED?

kroening · 2024-03-09T17:02:32Z

Is UNKNOWN the right status here? Or should there are rather be a new status UNDEFINED?

I did think about revising the status outputs to increase clarity. But that should happen independently, as a separate discussion.

An issue with "UNDEFINED" is that the word "undefined behavior" is very specific to C/C++, and we may wish our status codes to be more general. Also, it may mislead a reader to believe that there is undefined behavior at the given location. There may well be, but the point is that the undefined behavior is before that assertion in program order.

zhassan-aws · 2024-03-09T19:19:42Z

In Kani, we use UNDETERMINED.

kroening · 2024-03-09T19:55:52Z

I've pulled out the question of division-by-zero for floating-point numbers into a separate PR: #8233

celinval · 2024-03-12T19:13:29Z

Are fatal assertions encoded as assert + assume? How customizable will this new assertion be? Will users also be able to instrument their code with fatal assertions?

kroening · 2024-03-12T21:08:07Z

Are fatal assertions encoded as assert + assume?

I am afraid that would yield the opposite result: you'd be more likely to get SUCCESS for the downstream properties, making the user believe that they are proven when really they are not.

How customizable will this new assertion be? Will users also be able to instrument their code with fatal assertions?

We could certainly consider a __CPROVER_fatal_assert, or the like.

celinval · 2024-03-13T03:52:01Z

Are fatal assertions encoded as assert + assume?

I am afraid that would yield the opposite result: you'd be more likely to get SUCCESS for the downstream properties, making the user believe that they are proven when really they are not.

In Kani, we over-approximate by marking all passing properties as undetermined.

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 diffblue#8226.

tautschnig · 2024-03-15T10:02:13Z

Are fatal assertions encoded as assert + assume?

I am afraid that would yield the opposite result: you'd be more likely to get SUCCESS for the downstream properties, making the user believe that they are proven when really they are not.

In Kani, we over-approximate by marking all passing properties as undetermined.

#8242 now implements the assert + assume when users request this.

kroening · 2024-03-23T23:27:50Z

This now marks refuted assertions after refuted fatal assertions as UNKNOWN.

kroening · 2024-03-25T14:27:59Z

This now marks refuted assertions after refuted fatal assertions as UNKNOWN.

This comes at a price: to identify those assertions, the trace needs to be computed. That trace computation is broken in a number of cases, now marked as KNOWNBUG. Note that these aren't regressions caused by this PR, but just exposed by this PR.

We can try to fix these beforehand, and delay this PR. I believe that the step towards reporting sound results is very important, and that we should do it for 6.0.

tautschnig · 2024-03-25T14:34:38Z

This comes at a price: to identify those assertions, the trace needs to be computed. That trace computation is broken in a number of cases, now marked as KNOWNBUG. Note that these aren't regressions caused by this PR, but just exposed by this PR.

What kind of brokenness is this? I have previously only seen that computing traces can be very expensive (see #5714).

kroening · 2024-03-25T15:22:55Z

What kind of brokenness is this? I have previously only seen that computing traces can be very expensive (see #5714).

It seems to be a miscellaneous set of issues that get triggered by calling get(...); some of them in the contract code, and also one in the interface to cprover_smt.

I didn't see a case of things getting very slow, but I'd say that's just as bad as throwing an error. This ought to be linear.

tautschnig · 2024-04-22T13:14:24Z

regression/symtab2gb/multiple_symtabs/test.desc

@@ -7,4 +7,3 @@ user.json_symtab library.json_symtab
 ^\[2\] file library.adb line \d+ assertion: FAILURE$
 ^VERIFICATION FAILED$
 --
-error


Why did this line get removed?

The test triggered on "error trace", i.e., fails when --trace is added.

But ... this PR no longer adds a need to compute traces?

Yes, but our future selves still want this. But could pull over into separate PR.

I'm sorry, I had to convince myself of the problem... Done and now PR'ed as #8270.

tautschnig · 2024-04-22T13:14:31Z

regression/symtab2gb/single_symtab/test.desc

@@ -7,4 +7,3 @@ entry_point.json_symtab
 ^\[2\] file entry_point.adb line \d+ assertion: SUCCESS$
 ^VERIFICATION FAILED$
 --
-error


Same here: Why did this line get removed?

remi-delmas-3000

Maybe add tests with mutually recursive functions containing fatal assertions

remi-delmas-3000 · 2024-04-22T13:52:12Z

src/goto-checker/fatal_assertions.cpp

+    if(!insertion_result.second)
+      continue; // seen already
+
+    if(loc.target->is_function_call())


does this assume that function pointer calls have been eliminated ?

remi-delmas-3000 · 2024-04-22T13:54:35Z

src/goto-checker/fatal_assertions.cpp

+
+/// Proven assertions after refuted fatal assertions
+/// are marked as UNKNOWN.
+void propagate_fatal_to_proven(


why keep refuted assertions after refuted fatal assertions intact ? The counter example could also be spurious or not worth investigating.

Note the discussion on the PR. The problem is that enabling the computation of counterexamples is expensive and doesn't work. Hence I've taken that out again.

remi-delmas-3000 · 2024-04-22T13:57:57Z

src/goto-checker/fatal_assertions.cpp

+{
+  // Iterate to find refuted fatal assertions. Anything reachalble
+  // from there is a 'fatal loc'.
+  loc_sett fatal_locs;


Is there a risk to flip the status of a fatal assertion from FAIL to UNKOWN if the goto model contains mutually recursive functions ? (a fatal assertion could appear to be after itself ?)

No, assertions that are failed simply stay failed.

remi-delmas-3000

Is there a documentation update for fatal assertions ?

Are there ways to invoke CBMC which would result in the propagation not happening ?
i.e. is all_properties_verifier_with_trace_storaget the only verifier that users can invoke through the CLI ?

kroening · 2024-04-22T21:22:28Z

Is there a documentation update for fatal assertions ?

This is a bigger job. It will need to be done eventually, but I'd do it as part of a bigger doc overhaul. It requires explaining what UB is, why it's bad, and why it's not locally contained.

Are there ways to invoke CBMC which would result in the propagation not happening ?

Not that I know of.

tautschnig

Approving, but would appreciate if #8270 could be merged first to have a proper separation of concerns.

This introduces a variant of ASSERT instructions that are fatal when they are refuted. Execution paths through fatal assertions that are refuted are undefined. Assertions that (otherwise) pass and that are reachable from a refuted fatal assertion are now reported as UNKNOWN. The motivating use-case for fatal assertions is undefined behavior in languages such as C/C++ or Rust. Noi attempt is made to modify the outcome of ASSERT instructions that are refuted owing to a trace through a refuted fatal assertion. The computation of the trace is not robust enough.

kroening force-pushed the fatal-assertions branch 3 times, most recently from fa9256f to 8f8e599 Compare March 3, 2024 23:32

kroening force-pushed the fatal-assertions branch from 8f8e599 to f24b721 Compare March 8, 2024 23:54

kroening mentioned this pull request Mar 9, 2024

CBMC 5.84 unsound in presence of undefined behaviour #7732

Closed

kroening force-pushed the fatal-assertions branch 5 times, most recently from 58bdc8c to 2a08484 Compare March 9, 2024 15:57

kroening marked this pull request as ready for review March 9, 2024 19:55

kroening requested review from tautschnig, peterschrammel and remi-delmas-3000 as code owners March 9, 2024 19:55

kroening force-pushed the fatal-assertions branch from 2a08484 to a393868 Compare March 10, 2024 00:13

kroening requested review from jimgrundy and TGWDB as code owners March 10, 2024 00:13

kroening force-pushed the fatal-assertions branch from a393868 to 66e5329 Compare March 10, 2024 00:35

kroening force-pushed the fatal-assertions branch from 66e5329 to e9622b3 Compare March 15, 2024 01:41

tautschnig mentioned this pull request Mar 15, 2024

Built-in checks can optionally be fatal #8242

Closed

4 tasks

kroening force-pushed the fatal-assertions branch from c1c781b to c8c61ca Compare March 23, 2024 23:25

kroening force-pushed the fatal-assertions branch 7 times, most recently from 4d88965 to f6e0d9f Compare March 24, 2024 21:19

kroening force-pushed the fatal-assertions branch 2 times, most recently from 5cc78c4 to 0ad525c Compare April 3, 2024 20:01

kroening force-pushed the fatal-assertions branch 2 times, most recently from be78e8c to eb9ccc9 Compare April 19, 2024 15:16

tautschnig reviewed Apr 22, 2024

View reviewed changes

remi-delmas-3000 reviewed Apr 22, 2024

View reviewed changes

tautschnig approved these changes Apr 30, 2024

View reviewed changes

tautschnig assigned kroening and tautschnig Apr 30, 2024

tautschnig added the dependent - do not merge label Apr 30, 2024

kroening force-pushed the fatal-assertions branch from eb9ccc9 to 3cdd832 Compare April 30, 2024 11:47

kroening enabled auto-merge April 30, 2024 11:49

kroening removed the dependent - do not merge label Apr 30, 2024

kroening merged commit 69169d1 into develop Apr 30, 2024
41 checks passed

tautschnig deleted the fatal-assertions branch April 30, 2024 13:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

introduce 'fatal assertions' #8226

introduce 'fatal assertions' #8226

kroening commented Mar 3, 2024

codecov bot commented Mar 4, 2024 •

edited

Loading

peterschrammel commented Mar 9, 2024

kroening commented Mar 9, 2024

zhassan-aws commented Mar 9, 2024

kroening commented Mar 9, 2024

celinval commented Mar 12, 2024

kroening commented Mar 12, 2024

celinval commented Mar 13, 2024

tautschnig commented Mar 15, 2024

kroening commented Mar 23, 2024

kroening commented Mar 25, 2024

tautschnig commented Mar 25, 2024

kroening commented Mar 25, 2024

tautschnig Apr 22, 2024

kroening Apr 22, 2024

tautschnig Apr 23, 2024

kroening Apr 23, 2024

tautschnig Apr 30, 2024

tautschnig Apr 22, 2024

remi-delmas-3000 left a comment

remi-delmas-3000 Apr 22, 2024

kroening Apr 22, 2024

remi-delmas-3000 Apr 22, 2024

kroening Apr 22, 2024

remi-delmas-3000 Apr 22, 2024 •

edited

Loading

kroening Apr 22, 2024

remi-delmas-3000 left a comment

kroening commented Apr 22, 2024

tautschnig left a comment

introduce 'fatal assertions' #8226

introduce 'fatal assertions' #8226

Conversation

kroening commented Mar 3, 2024

codecov bot commented Mar 4, 2024 • edited Loading

Codecov Report

peterschrammel commented Mar 9, 2024

kroening commented Mar 9, 2024

zhassan-aws commented Mar 9, 2024

kroening commented Mar 9, 2024

celinval commented Mar 12, 2024

kroening commented Mar 12, 2024

celinval commented Mar 13, 2024

tautschnig commented Mar 15, 2024

kroening commented Mar 23, 2024

kroening commented Mar 25, 2024

tautschnig commented Mar 25, 2024

kroening commented Mar 25, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

remi-delmas-3000 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

remi-delmas-3000 Apr 22, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

remi-delmas-3000 left a comment

Choose a reason for hiding this comment

kroening commented Apr 22, 2024

tautschnig left a comment

Choose a reason for hiding this comment

codecov bot commented Mar 4, 2024 •

edited

Loading

remi-delmas-3000 Apr 22, 2024 •

edited

Loading