Contracts dependence on remove_returns [depends-on: #2677] #2712
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.
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.
This changes the code-contracts passes (both apply and check) to rely on the remove_function_pointers and remove_returns passes. This avoids problems that arose beforehand wherein those passes interfered with the code-contracts passes.
qaphla
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli,
smowton,
tautschnig and
thk123
as code owners
kroening
requested changes
Aug 10, 2018
tautschnig
changed the title
|
Closing due to age. If you believe this is erroneous please reopen and update the PR. |
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.
Only the last commit of this is new. The rest are from #2676 and #2677.
It was pointed out that contracts fail to behave correctly if
--remove-returnsis invoked before--[check/apply]-code-contracts. This change makes it so that--remove-returnsis always invoked beforehand. However, under some circumstances, invoking--remove-returnstwice can still lead to issues (I believe due to some interaction of--remove-returnswith one of the other simplifying passes) wherein (some) function calls are removed altogether.This should be ignored until its predecessors are more settled, but may yield useful discussion after that point.