Add an --assert-ensures check #4976
Conversation
angelhof
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
martin-cs,
peterschrammel and
smowton
as code owners
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 497b740).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121669324
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.
Codecov Report
@@ Coverage Diff @@
## develop #4976 +/- ##
===========================================
+ Coverage 69.24% 69.25% +0.01%
===========================================
Files 1309 1309
Lines 108453 108497 +44
===========================================
+ Hits 75096 75138 +42
- Misses 33357 33359 +2
Continue to review full report at Codecov.
|
|
@chrisr-diffblue @martin-cs could you review this PR? |
|
Seems sensible overall -- perhaps call it |
| @@ -1643,6 +1659,7 @@ void goto_instrument_parse_optionst::help() | |||
| " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*) | |||
| " (use multiple times if required)\n" | |||
| " --check-invariant function instruments invariant checking function\n" | |||
| " --assert-ensures function checks that function satisfies its contract ensures after each call\n" // NOLINT(*) | |||
| " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) | |||
There was a problem hiding this comment.
What does "after each call" mean?
So this is really checking the post-conditions in particular calling contexts?
There was a problem hiding this comment.
Seems sensible overall -- perhaps call it
--check-postconditions?
I agree that this is a much better name.
What does "after each call" mean?
So this is really checking the post-conditions in particular calling contexts?
It asserts the postcondition after all calls to the function. So it checks the postcondition if the function is reachable, and is called with its name (i.e. it wouldn't work for function pointers). If this is a problem, I could re-implement this as a check before each return point in the function body. I didn't do that initially for simplicity. What do you think?
There was a problem hiding this comment.
Or maybe --check-ensures (because they are written in the source code as __CPROVER_ensures) or --check-contracts ?
There was a problem hiding this comment.
What about --check-contract-postconditions or --check-contract-ensures?
There was a problem hiding this comment.
My personal opinion is that I like these --check-blah options to mirror whatever is in the source code - so I'd lean towards --check-ensures or --check-contract-ensures - others may have different opinions :-)
|
Would it also make sense to add an |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 167e36d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122308767
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.
| --assert-ensures min | ||
| ^EXIT=10$ | ||
| ^SIGNAL=0$ | ||
| ^VERIFICATION FAILED$ |
There was a problem hiding this comment.
Could fail for other reasons -- suggest checking the particular failure line you're expecting, and/or comparing against a companion test that doesn't use --assert-ensures and for which verification succeeds
| @@ -0,0 +1,7 @@ | |||
| CORE | |||
| main.c | |||
| --assert-ensures min | |||
| goto_functionst &_goto_functions): | ||
| ns(_symbol_table), | ||
| goto_functionst &_goto_functions, | ||
| std::list<std::string> _functions_to_assert_ensures) |
There was a problem hiding this comment.
Take by const ref, or std::move into the local variable
| assert_ensures_after_calls(goto_functionst::goto_functiont &goto_function); | ||
|
|
||
| void | ||
| assert_ensures(goto_programt &goto_program, goto_programt::targett target); |
There was a problem hiding this comment.
_after_call for consistency with function above?
|
|
||
| // is there a contract? | ||
| if(ensures.is_nil()) | ||
| return goto_assertion; |
There was a problem hiding this comment.
This intends return None, but is vulnerable to accidentally returning a partial program if someone moves some prep work to the top of the function, e.g. allocating a temporary, or labelled SKIP or whatever. Suggest instead this function should return optionalt<goto_programt> so you can use return {} when you intend to report failure / no-action.
| // replace formal parameters by arguments, replace return | ||
| replace_symbolt replace; | ||
|
|
||
| // TODO: return value could be nil |
There was a problem hiding this comment.
? As it just not set at all? I don't think that's valid
| code_function_callt::argumentst::const_iterator a_it = | ||
| call.arguments().begin(); | ||
| for(code_typet::parameterst::const_iterator p_it = type.parameters().begin(); | ||
| p_it != type.parameters().end() && a_it != call.arguments().end(); |
There was a problem hiding this comment.
arguments ending before parameters would be a static error AFAIK -- should probably just INVARIANT that you have at least enough arguments (and decide what you want to do for varargs?)
| if(mode_assert_ensures) | ||
| { | ||
| Forall_goto_functions(it, goto_functions) | ||
| assert_ensures_after_calls(it->second); |
There was a problem hiding this comment.
Does this share any code with code_contracts? If so perhaps it should be a different pass rather than two modes of the same one
Add an --assert-ensures check that asserts the ensures part of a function's contract. Many function names can be given as arguments to the check.