Add a __CPROVER_postcondition builtin #4921

angelhof · 2019-07-17T16:42:00Z

Add a builtin __CPROVER_postcondition builtin function that internally becomes an assert (like __CPROVER_precondition).

This will be used (by a later PR) to turn function preconditions, and postconditions to code contracts.

smowton · 2019-07-17T20:56:57Z

Please add a regression test exercising the new code. There actually don't appear to be any exercising __CPROVER_precondition either, so if you're feeling generous add that too!

angelhof · 2019-07-17T21:01:50Z

Please add a regression test exercising the new code. There actually don't appear to be any exercising __CPROVER_precondition either, so if you're feeling generous add that too!

@smowton Thanks, I will add a regression test for both. On a different note, why is CPP-LINT in travis complaining only for the newly added line and not for the ones above that use __CPROVER_?

owen-mc-diffblue · 2019-07-18T11:56:43Z

I think CPP-LINT in travis only checks newly added lines. This is so that things can be slowly fixed as we go, rather than having to fix them all at once so that we can see if we add any new ones.

angelhof · 2019-07-18T15:02:04Z

I think CPP-LINT in travis only checks newly added lines. This is so that things can be slowly fixed as we go, rather than having to fix them all at once so that we can see if we add any new ones.

Thanks. Shouldn't this check in cpplint.py only check for uses of __CPROVER_ in strings? I am not aware of any way to define a function using a string literal (CPROVER_PREFIX).

owen-mc-diffblue · 2019-07-19T06:45:42Z

@tautschnig, you wrote that check in cpplint.py (last October), can you help @angelhof?

smowton · 2019-07-22T14:48:13Z

Here's the check: https://github.com/diffblue/cbmc/blob/develop/scripts/cpplint.py#L4607

I would suggest simply whitelisting paths beginning with regession/ or src/ansi-c/library/` for that particular check. Hard-coding that should be fine given the check itself is our own custom invention.

angelhof · 2019-07-22T15:15:08Z

Here's the check: https://github.com/diffblue/cbmc/blob/develop/scripts/cpplint.py#L4607

I would suggest simply whitelisting paths beginning with regession/ or src/ansi-c/library/` for that particular check. Hard-coding that should be fine given the check itself is our own custom invention.

Wouldn't something like r'\".*__CPROVER_.*\"' make more sense? Since (from what I understand) this check suggests using CPROVER_PREFIX in string literals and not in general (e.g. function names).

smowton · 2019-07-23T11:30:26Z

That precise regex would misfire for f("Hello", __CPROVER_blah(y, z), "world"), but looking for precisely "__CPROVER_ would probably do the trick 90% of the time. I'd be happy with either solution.

angelhof · 2019-07-23T11:44:07Z

@smowton I don't have any preference between the two. I could implement any of them in a separate PR. Is this PR blocked until the lint check succeeds?

smowton · 2019-07-23T12:47:42Z

Yes without administrative intervention. I'd recommend making the change as a second commit in this PR.

codecov-io · 2019-07-26T12:46:51Z

Codecov Report

Merging #4921 into develop will increase coverage by <.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #4921      +/-   ##
===========================================
+ Coverage    69.27%   69.28%   +<.01%     
===========================================
  Files         1307     1307              
  Lines       108145   108148       +3     
===========================================
+ Hits         74918    74926       +8     
+ Misses       33227    33222       -5

Impacted Files	Coverage Δ
src/goto-programs/builtin_functions.cpp	`45.76% <100%> (+0.31%)`	⬆️
src/solvers/flattening/boolbv_get.cpp	`78.66% <0%> (+3.33%)`	⬆️

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 103b2dc...44197bb. Read the comment docs.

angelhof · 2019-07-26T12:52:12Z

Could someone review this?

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 44197bb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120852254
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

angelhof · 2019-07-29T18:28:24Z

@peterschrammel could you review this?

angelhof · 2019-08-01T17:26:29Z

@peterschrammel @thk123 could you review this PR?

thk123

Approving the changes to cpplint only - seems like there has been more than enough eyes on the rest!

tautschnig

The empty commit bodies plus the absence of other documentation make this hard for anyone to use effectively. Otherwise looks good to me.

tautschnig · 2019-08-04T16:26:26Z

src/ansi-c/cprover_builtin_headers.h

@@ -2,6 +2,7 @@ void __CPROVER_assume(__CPROVER_bool assumption);
 void __VERIFIER_assume(__CPROVER_bool assumption);
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
 void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);
+void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);


Random place for a comment: I think this strictly requires documentation. When should users make use of this? I note that the commit message doesn't have a body either, so it's really hard to see when that should be used.

Thanks. Where is a good place to add documentation for this?

As discussed elsewhere: doc/cprover-manual/cbmc-assertions.md is likely the best place for this. @kroening Would you be able to contribute some documentation of __CPROVER_precondition, which AFAIK never got documented?

I would structure this differently.
__CPROVER_precondition was introduced as a means to add preconditions to library functions, i.e., it was never meant to be used by anyone but CBMC developers.

The new feature, which is contract checking, is a different use-case, and externalises this to users of CBMC. My experience is that users like manuals that are structured by use-case. Thus, I would suggest to add a new chapter, say titled "Modular Verification using Code Contracts", or the like, to discuss this use-case separately.

[...] never meant to be used by anyone but CBMC developers.

While this is a good intention, I don't think it will remain as constrained if people find it useful in other places as well. Anything that can be used will be used at some point...

scripts/cpplint.py

The added builtin function, is transformed into an assert (like __CPROVER_precondition) by the goto-cc pass. The reason why it was added, is to allow an analysis on the AST to extract the postconditions from function bodies, to extend their function contracts.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 59ab9e9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122362598
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

angelhof · 2019-08-08T21:10:38Z

The lint error is fixed in #5000.

doc/cprover-manual/cbmc-assertions.md

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 119ce60).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122640419
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

angelhof requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners July 17, 2019 16:42

angelhof force-pushed the cprover-postcondition branch from 6ad9a09 to 44197bb Compare July 26, 2019 11:38

angelhof requested a review from thk123 as a code owner July 26, 2019 11:38

allredj reviewed Jul 26, 2019

View reviewed changes

smowton approved these changes Jul 26, 2019

View reviewed changes

owen-mc-diffblue approved these changes Jul 26, 2019

View reviewed changes

kroening approved these changes Jul 29, 2019

View reviewed changes

thk123 approved these changes Aug 2, 2019

View reviewed changes

tautschnig requested changes Aug 4, 2019

View reviewed changes

tautschnig assigned angelhof Aug 4, 2019

angelhof added 2 commits August 7, 2019 17:37

Clang-format

8f445f9

Add regression tests for pre and postconditions

f4a6f43

angelhof force-pushed the cprover-postcondition branch from 44197bb to 59ab9e9 Compare August 7, 2019 22:16

allredj reviewed Aug 7, 2019

View reviewed changes

angelhof force-pushed the cprover-postcondition branch from 59ab9e9 to f4a6f43 Compare August 8, 2019 21:07

angelhof requested a review from chrisr-diffblue as a code owner August 8, 2019 21:48

tautschnig approved these changes Aug 8, 2019

View reviewed changes

doc/cprover-manual/cbmc-assertions.md Outdated Show resolved Hide resolved

doc/cprover-manual/cbmc-assertions.md Show resolved Hide resolved

angelhof force-pushed the cprover-postcondition branch from 8746b52 to 3811798 Compare August 8, 2019 22:01

Add a description of the new feature in the manual

119ce60

angelhof force-pushed the cprover-postcondition branch from 3811798 to 119ce60 Compare August 9, 2019 17:58

allredj reviewed Aug 9, 2019

View reviewed changes

karkhaz merged commit d263955 into diffblue:develop Aug 11, 2019

Add a __CPROVER_postcondition builtin #4921

Add a __CPROVER_postcondition builtin #4921

Uh oh!

Conversation

angelhof commented Jul 17, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton commented Jul 17, 2019

Uh oh!

angelhof commented Jul 17, 2019

Uh oh!

owen-mc-diffblue commented Jul 18, 2019

Uh oh!

angelhof commented Jul 18, 2019

Uh oh!

owen-mc-diffblue commented Jul 19, 2019

Uh oh!

smowton commented Jul 22, 2019

Uh oh!

angelhof commented Jul 22, 2019

Uh oh!

smowton commented Jul 23, 2019

Uh oh!

angelhof commented Jul 23, 2019

Uh oh!

smowton commented Jul 23, 2019

Uh oh!

codecov-io commented Jul 26, 2019

Codecov Report

Uh oh!

angelhof commented Jul 26, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

angelhof commented Jul 29, 2019

Uh oh!

angelhof commented Aug 1, 2019

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig Aug 4, 2019

Choose a reason for hiding this comment

Uh oh!

angelhof Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Aug 5, 2019

Choose a reason for hiding this comment

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

angelhof commented Aug 8, 2019

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

angelhof commented Jul 17, 2019 •

edited

Loading