Fixed weakest precondition for code_assertt

[SaswatPadhi]

The existing wp function treated an assert statement the same way as a skip statement. This commit fixes this behavior as per standard Hoare logic rules.

• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[NlightNFotis]

LGTM, with the caveat of the clang-format issued fixed.

[martin-cs]

Can we discuss what your understanding of the semantics of assert is?

This is not well documented but I think that assert is just a check; it does not alter the flow of control in any way (there are a number of reasons why I think this is the useful semantics). Thus your patch is correct for the original Floyd-Hoare logic rules but I don't think that is what we have.

[martin-cs]

It seems that there is actually some documentation! And I wrote it :-\ and then forgot :-|

#2031

is the original discussion and

92b92d6

is the resultant documentation.

[SaswatPadhi]

Hi @martin-cs,

I am not sure about the semantics of assert within CBMC, but we had a discussion with @kroening on our Slack channel and he agreed that this should be changed.

It seems kind of strange that assert(cond) doesn't behave like if(!cond) abort.
I am working on generating VCs (in form of CHCs) for C programs, and the postcondition was simply being ignored during WP computation.

[SaswatPadhi]

Or may be I misunderstood @kroening. Probably he was pointing to a broader change -- changing the semantics of assert and then changing this wp computation.

[martin-cs]

I would strongly oppose changing the semantics of assert because it will be a lot of work and there are current bits of functionality that cannot be replicated with the strong assert-terminates-execution semantics.

If you want this semantics, may I suggest you name it "assert-free-WP" or similar. I can see that it is a useful thing to have but I think it should be separate to the normal WP.

PS If you are working on CHC, have you seen https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/horn_encoding.h ? Maybe Daniel has the patch that fills this in?

[SaswatPadhi]

This patch also seems consistent with the C/C++ semantics for assert -- it does terminate the program on assertion failure.

[SaswatPadhi]

If you are working on CHC, have you seen https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/horn_encoding.h? Maybe Daniel has the patch that fills this in?

Thanks, yes I am extending this file and I have handled many of the constructs that are currently not handled by the wp.cpp file, for example conditionals, code blocks, and loops.

[SaswatPadhi]

If you want this semantics, may I suggest you name it "assert-free-WP" or similar. I can see that it is a useful thing to have but I think it should be separate to the normal WP.

Thanks. Yes, currently for assert and decl I override the WP computation, but I thought of making this PR since this change was agreed upon in the Slack channel. If it's a major change then I'd keep the overriding logic within my horn_encoding.cpp for now.

I read the documentation @ #2301 and understand the rationale behind the current semantics, although it's somewhat unsettling that it differs from the C semantics. The PR discusses goto statements though. So the same applies to codet as well?

[tautschnig]

[...]

I read the documentation @ #2301 and understand the rationale behind the current semantics, although it's somewhat unsettling that it differs from the C semantics. The PR discusses goto statements though. So the same applies to codet as well?

I don't think anyone ever claimed that GOTO programs should have the same semantics as C programs? codet is a rather different story in that these are ASTs. A code_assertt generated by the Java front-end, for example, might have a different semantics than a code_assertt produced by the C front-end.

[codecov]

Codecov Report

Merging #5847 (37440ac) into develop (dbbe1da) will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5847   +/-   ##
========================================
  Coverage    72.86%   72.86%           
========================================
  Files         1421     1421           
  Lines       154173   154173           
========================================
  Hits        112337   112337           
  Misses       41836    41836           

---

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 751c986...37440ac. Read the comment docs.

[SaswatPadhi]

I don't think anyone ever claimed that GOTO programs should have the same semantics as C programs?

But isn't this claim implicit, when we say it's a bounded model checker for C? I mean if we model programs differently, then our check might have totally different guarantees that may not hold over actual execution of the program.

Although this particular case might be a non-issue, so please feel free to close this PR.

[hannes-steffenhagen-diffblue]

Sorry, I must've misunderstood what this change was about during the meeting. I would agree with Martin that changing the meaning of assert would be a major breaking change that's likely to have a lot of unintended consequence elsewhere in the codebase as well as downstream. Whether or not we should change the meaning of assert is a discussion for another time, but it's certainly not something that should happen without prior discussion.

[martin-cs]

On Fri, 2021-02-19 at 10:05 -0800, Saswat Padhi wrote: > I don't think anyone ever claimed that GOTO programs should have > the same semantics as C programs? But isn't this claim implicit, when we say it's a bounded model checker for C? I mean if we model programs differently, then our check might have totally different guarantees that may not hold over actual execution of the program.

I fear there may be a subtle miscommunication here. I think the point @tautschnig was making was that the /primitives/ of GOTO don't have to have the same semantics as C. However the over-all goal is to express the semantics of C /using/ those primitives. Thus the results are accurate w.r.t. ISO-9899+implementation defined behaviour but the /means/ of computing those aren't necessarily a subset of C. Cheers, - Martin

[SaswatPadhi]

That makes sense. Thanks @martin-cs!

[SaswatPadhi]

@martin-cs, @tautschnig:
The ISO C standard mandates that a program must abort on assertion failure: https://en.cppreference.com/w/c/error/assert. So a C program with assert would behave very differently than a goto program with goto's assert primitive.

To preserve behavior, goto-cc might compile C assert to some terminating primitive in goto (may be some assume + assert combination? not sure), but it doesn't appear to be doing so currently.

[tautschnig]

@martin-cs, @tautschnig:
The ISO C standard mandates that a program must abort on assertion failure: https://en.cppreference.com/w/c/error/assert. So a C program with assert would behave very differently than a goto program with goto's assert primitive.

To preserve behavior, goto-cc might compile C assert to some terminating primitive in goto (may be some assume + assert combination? not sure), but it doesn't appear to be doing so currently.

Indeed - I've now implemented this in #5866.

[SaswatPadhi]

Thanks, @tautschnig.

There is still some issue with the WP computation -- I am thinking more about it and would bring it up during our meeting tomorrow / next DiffBlue meeting.

Basically, the C statement assert(A) is compiled to __CPROVER_assert(A); __CPROVER_assume(A); and since __CPROVER_assert is just skip during WP computation currently, a C assert is effectively seen as a goto assume (i.e. __CPROVER_assume) during WP.

[tautschnig]

[...]

Basically, the C statement assert(A) is compiled to __CPROVER_assert(A); __CPROVER_assume(A); and since __CPROVER_assert is just skip during WP computation currently, a C assert is effectively seen as a goto assume (i.e. __CPROVER_assume) during WP.

Yes, that's what WP computation will need to deal with. It's the "ASSUME" that you should be able to derive preconditions from.

[hannes-steffenhagen-diffblue]

To preserve behavior, goto-cc might compile C assert to some terminating primitive in goto (may be some assume + assert combination? not sure), but it doesn't appear to be doing so currently.

This is, in fact, what jbmc is doing. I think changing the frontend to that may make sense, this'll change coverage results but probably not in a way anyone's going to complain about.

[martin-cs]

@hannes-steffenhagen-diffblue agreed. There is a long-standing question / concern / issue with the correctness of traces / model checking after any undefined behaviour in C.

[SaswatPadhi]

Closing this PR for now. The WP seems consistent with the non-aborting assert and the C assert will now be compiled to ASSERT + ASSUME in goto. I'll rethink the WP and open another PR.

Thanks everyone!