Abort after failing C assert #5866

tautschnig · 2021-02-25T00:36:05Z

The C standard specifies behaviour of the "assert" macro as resulting in
an abort when the condition does not evaluate to true. Implement this
behaviour by inserting assume(0) after assert(0).

Fixes: #5505

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 · 2021-02-25T09:55:51Z

Codecov Report

Merging #5866 (9940fd9) into develop (e021eef) will decrease coverage by 2.43%.
The diff coverage is 62.50%.

❗ Current head 9940fd9 differs from pull request most recent head 76491eb. Consider uploading reports for the commit 76491eb to get more accurate results

@@             Coverage Diff             @@
##           develop    #5866      +/-   ##
===========================================
- Coverage    76.74%   74.30%   -2.44%     
===========================================
  Files         1579     1447     -132     
  Lines       182171   157796   -24375     
===========================================
- Hits        139802   117257   -22545     
+ Misses       42369    40539    -1830

Impacted Files	Coverage Δ
src/goto-programs/builtin_functions.cpp	`55.32% <55.55%> (-1.55%)`	⬇️
src/goto-instrument/goto_program2code.cpp	`69.15% <71.42%> (+0.37%)`	⬆️
unit/unit_tests.cpp	`0.00% <0.00%> (-100.00%)`	⬇️
src/goto-checker/goto_verifier.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/goto-cc/linker_script_merge.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/goto-instrument/wmm/shared_buffers.h	`0.00% <0.00%> (-95.46%)`	⬇️
src/goto-instrument/document_properties.cpp	`0.00% <0.00%> (-89.35%)`	⬇️
src/goto-instrument/uninitialized.cpp	`0.00% <0.00%> (-87.76%)`	⬇️
src/goto-programs/link_goto_model.cpp	`0.00% <0.00%> (-85.51%)`	⬇️
src/analyses/uninitialized_domain.cpp	`0.00% <0.00%> (-81.09%)`	⬇️
... and 1310 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update e08c77d...76491eb. Read the comment docs.

peterschrammel

I think this requires a thorough documentation review since __CPROVER_assert is now the default way to specify non-aborting properties. Some downstream CBMC users might not operate with abort-semantics in mind.

Side note: JBMC does something similar (in one of its modes)

cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines 2444 to 2446 in f4edb72

    
           // we translate athrow into 
        
           // ASSERT false; 
        
           // ASSUME false:

peterschrammel · 2021-02-25T12:59:08Z

regression/cbmc-incr-oneloop/multiple-asserts/test.c

@@ -2,8 +2,8 @@ int main()
 {
  for(int i = 0; i < 10; ++i)
  {
-    assert(i != 5);
-    assert(i != 8);
+    __CPROVER_assert(i != 5, "");


❓ Do we need a convenienve overload without the comment argument since __CPROVER_assert is now the default way to specify non-aborting properties?

Sounds like a good idea to me

hannes-steffenhagen-diffblue · 2021-02-25T16:03:45Z

IMHO this sounds like the right way to go forward with this. I do also agree with @peterschrammel though that this requires us going through documentation and making sure we don't say anything wrong now, and for the other I think this should result in a major version bump.

TGWDB · 2021-02-25T16:54:38Z

regression/goto-harness/do-not-use-nondet-for-selecting-pointers-to-treat-as-equal/test.desc

+\[test.assertion.1\] line 3 assertion: SUCCESS
+\[test.assertion.2\] line 4 assertion: SUCCESS
+\[test.assertion.3\] line 5 assertion: FAILURE
+\[test.assertion.4\] line 6 assertion: FAILURE
+\[test.assertion.5\] line 7 assertion: FAILURE


Have we lost something useful and helpful here by not showing any detail of the assertion that failed? (I realise the empty messages may contribute to this, but with the comment of @peterschrammel above perhaps we should consider having the same behaviour in our override?)

+1 these should give a message...

martin-cs · 2021-02-25T21:27:05Z

We are doing a similar assert/assume thing for Ada.

As regards updating -- this always used to be how assert() worked. I guess it must have been removed at some point? There were a few years where there was ... ambiguity over the semantics of assert.

martin-cs

A good and useful thing to do. I won't block this but I do agree with others that this needs to be clearly communicated (or, at least, "If you want a non-terminating check, use __CPROVER_assert()").

One thought : it feels like assert should be implementable in the C library (possibly with a macro to copy the expression into the string so that we don't have the problem with loss of messages that @TGWDB flagged). I am generally in favour of modelling going in the library in C where possible.

SaswatPadhi · 2021-02-26T00:26:05Z

I have one small comment that I had mentioned to @tautschnig this morning:

The semantics for ASSUME statement currently is stated (in src/goto-programs/goto_program.h) as:

This thread of execution waits for guard to evaluate to true.
Assume does not "retro-actively" affect the thread or any ASSERTs.

This means, if the guard evaluates to false, it would keep waiting forever as opposed to aborting (as mandated by C assert semantics).

It seems to me that THROW might be the closest we have to an aborting goto primitive, but I'm not sure.

martin-cs · 2021-02-26T11:13:33Z

@SaswatPadhi This is a sensible and a valid concern but I think that assume is the right thing to do. Our (informal) model of execution has nothing happen after termination, so in the single threaded case, an abrupt termination and an infinite loop are indistinguishable. The multi-threaded case is a little more complex and I haven't worked on it so I am probably not the best person to ask but I don't think we have a way of distinguishing a "hung" thread from one that terminates early, so, again, this is not an issue.

THROWand CATCH... TBH their semantics are even less clear to me. I think the clearest explanation is the code that removes them. This is different for C++ and Java. In practice they are removed early on so I don't think we should be introducing them, esp. in things like C that don't have an exception model at all.

tautschnig · 2021-05-13T21:20:08Z

Marking do-not-merge as this likely wants a major-version bump. Otherwise it should be ready for (re-)review.

C's assert() should result in an abort() when the asserted condition evaluates to false. If we want to test multiple properties, including some failing ones, use __CPROVER_assert to not rely on any modelling of assert() that does not result in an abort().

The C standard specifies behaviour of the "assert" macro as resulting in an abort when the condition does not evaluate to true. Implement this behaviour by inserting assume(0) after assert(0). Fixes: diffblue#5505

esteffin · 2023-11-08T15:41:36Z

We are considering to include this PR into version 6.

However we should make sure that we do add the documentation specifying that assert is blocking as opposed to __CPROVER_assert that is not.

tautschnig · 2023-11-16T16:35:06Z

This is a major undertaking with limited added value. Users could choose to add their own assert macro that exhibits this behaviour. Closing as we are unlikely to find time to work on this anytime soon.

tautschnig requested review from kroening, peterschrammel and smowton as code owners February 25, 2021 00:36

tautschnig mentioned this pull request Feb 25, 2021

Fixed weakest precondition for code_assertt #5847

Closed

7 tasks

tautschnig force-pushed the c-assert branch from 887755c to f75988e Compare February 25, 2021 08:51

tautschnig self-assigned this Feb 25, 2021

peterschrammel reviewed Feb 25, 2021

View reviewed changes

TGWDB reviewed Feb 25, 2021

View reviewed changes

martin-cs approved these changes Feb 25, 2021

View reviewed changes

tautschnig force-pushed the c-assert branch from f75988e to da42233 Compare March 19, 2021 15:55

tautschnig force-pushed the c-assert branch from da42233 to 6273c92 Compare March 31, 2021 19:39

tautschnig requested a review from romainbrenguier as a code owner March 31, 2021 19:39

tautschnig force-pushed the c-assert branch 3 times, most recently from c324b9a to 9b215f7 Compare April 2, 2021 21:14

tautschnig added the dependent - do not merge label Apr 2, 2021

tautschnig changed the title ~~Abort after failing C assert~~ Abort after failing C assert [depends-on: #6001, #6002] Apr 2, 2021

tautschnig marked this pull request as draft April 2, 2021 21:18

tautschnig force-pushed the c-assert branch 4 times, most recently from 37b5112 to 0e2eb40 Compare April 7, 2021 16:29

tautschnig changed the title ~~Abort after failing C assert [depends-on: #6001, #6002]~~ Abort after failing C assert [depends-on: #6001] Apr 7, 2021

tautschnig changed the title ~~Abort after failing C assert [depends-on: #6001]~~ Abort after failing C assert Apr 30, 2021

tautschnig removed the dependent - do not merge label Apr 30, 2021

tautschnig force-pushed the c-assert branch from 0e2eb40 to b7158df Compare April 30, 2021 19:46

tautschnig removed their assignment Apr 30, 2021

tautschnig marked this pull request as ready for review April 30, 2021 19:47

tautschnig requested a review from chrisr-diffblue as a code owner April 30, 2021 19:47

tautschnig force-pushed the c-assert branch from b7158df to 9940fd9 Compare May 7, 2021 06:19

tautschnig self-assigned this May 11, 2021

tautschnig added the do not merge label May 13, 2021

martin-cs approved these changes May 19, 2021

View reviewed changes

tautschnig mentioned this pull request Dec 3, 2021

Prevent multiple instrumentation of a same check and instrumentation of instrumentation assertions #6471

Merged

5 tasks

tautschnig added 2 commits February 10, 2022 10:53

Abort after failing C assert

76491eb

The C standard specifies behaviour of the "assert" macro as resulting in an abort when the condition does not evaluate to true. Implement this behaviour by inserting assume(0) after assert(0). Fixes: diffblue#5505

tautschnig force-pushed the c-assert branch from 9940fd9 to 76491eb Compare February 10, 2022 10:54

tautschnig requested a review from chris-ryder as a code owner February 10, 2022 10:54

feliperodri added the aws Bugs or features of importance to AWS CBMC users label Oct 6, 2022

feliperodri mentioned this pull request Oct 6, 2022

Propagating information from assertions that hold to subsequent lines of code using __CPROVER_assume #5505

Open

feliperodri added the aws-medium label Nov 2, 2022

tautschnig added the Version 6 Pull requests and issues requiring a major version bump label Nov 8, 2022

feliperodri removed the aws-medium label Nov 9, 2022

esteffin added the Needs rebase label Nov 8, 2023

TGWDB added Version 7 and removed Version 6 Pull requests and issues requiring a major version bump labels Nov 16, 2023

tautschnig closed this Nov 16, 2023

tautschnig mentioned this pull request Feb 27, 2024

Semantics of assert statements #8223

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Abort after failing C assert #5866

Abort after failing C assert #5866

tautschnig commented Feb 25, 2021 •

edited by feliperodri

Loading

codecov bot commented Feb 25, 2021 •

edited

Loading

peterschrammel left a comment •

edited

Loading

peterschrammel Feb 25, 2021

hannes-steffenhagen-diffblue Feb 25, 2021

hannes-steffenhagen-diffblue commented Feb 25, 2021

TGWDB Feb 25, 2021

martin-cs Feb 25, 2021

martin-cs commented Feb 25, 2021

martin-cs left a comment

SaswatPadhi commented Feb 26, 2021 •

edited

Loading

martin-cs commented Feb 26, 2021

tautschnig commented May 13, 2021

esteffin commented Nov 8, 2023

tautschnig commented Nov 16, 2023

Abort after failing C assert #5866

Abort after failing C assert #5866

Conversation

tautschnig commented Feb 25, 2021 • edited by feliperodri Loading

codecov bot commented Feb 25, 2021 • edited Loading

Codecov Report

peterschrammel left a comment • edited Loading

Choose a reason for hiding this comment

peterschrammel Feb 25, 2021

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue Feb 25, 2021

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented Feb 25, 2021

TGWDB Feb 25, 2021

Choose a reason for hiding this comment

martin-cs Feb 25, 2021

Choose a reason for hiding this comment

martin-cs commented Feb 25, 2021

martin-cs left a comment

Choose a reason for hiding this comment

SaswatPadhi commented Feb 26, 2021 • edited Loading

martin-cs commented Feb 26, 2021

tautschnig commented May 13, 2021

esteffin commented Nov 8, 2023

tautschnig commented Nov 16, 2023

tautschnig commented Feb 25, 2021 •

edited by feliperodri

Loading

codecov bot commented Feb 25, 2021 •

edited

Loading

peterschrammel left a comment •

edited

Loading

SaswatPadhi commented Feb 26, 2021 •

edited

Loading