Improvements to code contracts [depends-on: #2646, #2676, blocks: #2712] #2677
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The previous implementation of code-contracts has a single flag --apply-code-contracts, which created checks to verify that the contracts are satisfied and also used the contracts to abstract out the portions of code which had contracts provided. This commit splits that process into two parts, one of which only uses the contracts, without checking that they hold (--apply-code-contracts) and the other of which (incomplete as of this commit) both checks and applies, in a similar manner to the existing method. While it is clear that applying contracts without checking them is unsound, it is nevertheless useful in verifying large pieces of software in a modular fashion. If we verify a function to satisfy its specification from an arbitrary environment, then we can avoid needing to check that function again by using --apply-code-contracts.
This commit completes the work started in the previous commit by revising the existing contract-handling code into the new pass --check-code-contracts, which first applies all contracts and then checks them. By applying the contracts before checking begins, this checks the relative correctness of each function/loop with respect to the functions called by/loops contained in it. Since there can be no infinite sequence of nested functions/loops, these relative correctness results together imply the correctness of the overall program. We take this approach rather than checking entirely without using contracts because it allows significant reuse of results --- a function that is called many times only needs to be checked once, and all of its invocations will be abstracted out by the contract application.
Several functions from the old implementation of code-contracts that were made dead by the previous commits are removed by this commit. Additionally, some variables which were formerly in use are no longer needed, and so are removed.
This commit resolves an issue where ID_dynamic_object was used to label two semantically distinct exprts. One, with a single operand, was a boolean expression meaning that the operand is a pointer to a dynamic object. This has been renamed to ID_is_dynamic_object. The second, with two operands, is an exprt representing a dynamic object itself. This has stayed ID_dynamic_object. Disambiguating which meaning was intended in each case was relatively easy, as uses of these exprts frequently come with assertions about the number of operands, and so this was used to inform which instances of ID_dynamic_object should be changed and which should be left the same.
When handling the case of pointers, goto_rw would mark both the object pointed to and the pointer itself as written. For example, if x = &i, the line `*x = 1' would yield a write set containing both x and i, instead of just i. This resolves that issue by ensuring that value_set_dereference always gives at least one object that the dereference can refer to. This also resolves a bug wherein &a is marked as reading from a by removing the ID_symbol special case from get_objects_address_of.A
…ions Code contracts that introduce local declarations result in nested typecheck_declaration calls. The artificial __CPROVER_return_value symbol must then be added/removed by a single call only.
This commit changes the behaviour of --apply-code-contracts on function calls. Previously, when applying contracts, a function call would be replaced by an assertion that the precondition holds, followed by an assumption that the postcondition holds. This change inserts between that assert/assume pair code that sets all variables that could be modified by the function being called to be nondeterministic.
Because code contracts should be checked in an environment constrained only by the preconditions, we want to check contracts before initializing the dead and deallocated objects --- otherwise, we fail to check the cases where a pointer argument to a function points to a dead or deallocated object but is not NULL. This commit resolves these issues by temporarily initializing dead and deallocated objects to be the same fixed object before checking contracts, and then performing the standard initialization to NULL.
qaphla
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli,
smowton,
tautschnig and
thk123
as code owners
added 2 commits
August 3, 2018 13:41
This change replaces the use of local_may_alias analysis in code contracts with the more accurate goto_rw analysis. These analyses are used to find the set of variables written to by a loop or function so that we know which variables to make nondeterministic when abstracting out those pieces of code.
This commit adds some documentation to code-contracts, as well as fixing up small errors or confusing wording in existing comments.
allredj
reviewed
Aug 3, 2018
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 522c765).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80904637
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- 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).
kroening
requested changes
Aug 4, 2018
| @@ -65,6 +67,8 @@ jbmc/regression/**/tests-symex-driven-loading.log | |||
|
|
|||
| # files stored by editors | |||
| *~ | |||
| .*.swp | |||
| .*.swo | |||
|
|
|||
There was a problem hiding this comment.
Is this not redundant with the above?
| @@ -184,6 +186,8 @@ void dep_graph_domaint::data_dependencies( | |||
| data_deps.insert(w_range.first); | |||
| found=true; | |||
| } | |||
| } | |||
| } | |||
| } | |||
There was a problem hiding this comment.
The change to this file appears unrelated.
| @@ -414,16 +412,19 @@ void rw_range_sett::get_objects_typecast( | |||
|
|
|||
| void rw_range_sett::get_objects_address_of(const exprt &object) | |||
| { | |||
| if(object.id() == ID_string_constant || | |||
| if(object.id() == ID_symbol || | |||
| object.id() == ID_string_constant || | |||
| object.id() == ID_label || | |||
There was a problem hiding this comment.
The ID_symbol case overrides the case below.
| @@ -2141,7 +2141,7 @@ exprt c_typecheck_baset::do_special_functions( | |||
| throw 0; | |||
| } | |||
|
|
|||
| exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type()); | |||
| exprt dynamic_object_expr=exprt(ID_is_dynamic_object, expr.type()); | |||
| dynamic_object_expr.operands()=expr.arguments(); | |||
There was a problem hiding this comment.
Use is_dynamic_object_exprt, which you are adding.
|
Given that new syntax is proposed here, did you consider ACSL? |
martin-cs
reviewed
Aug 6, 2018
There was a problem hiding this comment.
Although I appreciate it is a pain, could we get the supporting PRs merged first and then look at this? I'm also very much with @kroening on the idea of annotation languages : the world may need another annotation language for C but it won't be one that is a partial subset of the features of an existing one. Interoperability is good and being able to compare wih / share benchmarks with tools like Frama-C would be great.
This was referenced Aug 6, 2018
tautschnig
changed the title
Closed
tautschnig
changed the title
tautschnig
changed the title
|
Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This provides a few changes which together serve to improve the havocking of variables when dealing with function calls (as well as a patch [02eb459] which doesn't really seem to fit anywhere else).
63b2af3 fixes a soundness issue with contract application by havocking the variables which could be touched by the function call being abstracted out.
2ec8f88 resolves an issue wherein function contracts were checked before initializing the dead and deallocated objects, and so any check that a pointer was not dead or deallocated would fail.
c3fcb36 switches contracts from using the local_may_alias analysis to the goto_rw analysis for finding the write sets of functions or loops.
a9354ac improves the documentation of the contracts feature.
This builds on #2646 because the changes in c3fcb36 benefit greatly from a less conservative approximation in goto_rw.
Only the commits mentioned by name in this are new. The others either come from #2646 or #2676.