CONTRACTS: Error-out on unknown functions (replace/enforce). #6733
Conversation
remi-delmas-3000
requested review from
tautschnig,
feliperodri,
SaswatPadhi,
martin-cs,
chris-ryder and
peterschrammel
as code owners
remi-delmas-3000
force-pushed
the
contracts-replace-unknown-fix
branch
from
84feaf2 to
73fc478
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6733 +/- ##
========================================
Coverage 76.86% 76.86%
========================================
Files 1589 1589
Lines 183813 183809 -4
========================================
+ Hits 141289 141293 +4
+ Misses 42524 42516 -8
Continue to review full report at Codecov.
|
| @@ -0,0 +1,5 @@ | |||
|
|
|||
There was a problem hiding this comment.
[minor] empty line
| @@ -0,0 +1,12 @@ | |||
| CORE | |||
There was a problem hiding this comment.
[minor] just to reduce code duplication, we can place this .desc file in enforce-unknown-function as well.
Concretely, we could:
- rename
enforce-unknown-function->function-contracts-unknown-function - rename
function-contracts-unknown-function/test.desc->test_enforce.desc - move this
test.desc->function-contracts-unknown-function/test_replace.desc
| --enforce-contract goo | ||
| ^Invariant check failed$ | ||
| ^Condition: Precondition$ | ||
| ^Reason: all_functions_found\(to_enforce\)$ |
There was a problem hiding this comment.
Should we also test for the message from PRECONDITION_WITH_DIAGNOSTICS?
There was a problem hiding this comment.
Now throwing an exception instead of using a precondition. The guidelines for error handling are: handle incorrect user input gracefully, throwing informative exceptions from util/exception_utils.h, use INVARIANT and PRECONDITION for internal checks that shall never fail.
| @@ -1150,8 +1150,18 @@ void goto_instrument_parse_optionst::instrument_goto_program() | |||
| // first replacement then enforcement. We rely on contract replacement | |||
| // and inlining of sub-function calls to properly annotate all | |||
| // assignments. | |||
| contracts.replace_calls(to_replace); | |||
| contracts.enforce_contracts(to_enforce); | |||
| if(contracts.replace_calls(to_replace)) | |||
There was a problem hiding this comment.
Do we need to keep these if statements here or just modify replace_calls and enforce methods to throw 0 whenever the precondition fail? Is there any case where we actually return false from these methods and use these if statement here? In any case, we could move them.
There was a problem hiding this comment.
Since we are now throwing exceptions for incorrect user input I changed the signatures to return void, and got rid of these checks.
remi-delmas-3000
force-pushed
the
contracts-replace-unknown-fix
branch
2 times, most recently
from
2372e1e to
d411e97
Compare
We dropped the pattern of returning boolean error flags and accumulating errors in `replace_calls` and `enforce_contracts`. We are now checking that all functions exist upfront and throwing exceptions from `util/exception_utils.h` as soon as the first unknown function is found. Subsequent checks of the same conditions are now INVARIANTS.
remi-delmas-3000
force-pushed
the
contracts-replace-unknown-fix
branch
from
d411e97 to
e6402ec
Compare
feliperodri
added
bugfix
aws
goto-instrument now errors out when attempting to enforce or replace the contract of an unknown function.
replace_callsandenforce_contractsare now checking that functions exist upfront and are failing fast by throwing exceptions fromutil/exception_utils.h, and are now returning void instead of a boolean error flag.