klaas' Contracts work #3769
Closed
klaas' Contracts work #3769
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 --expand-pointer-predicates pass resolves pointer predicates
(util/pointer_predicates.{cpp, h}) which have side effects and
so require expanding into multiple instructions.
Currently, the only such predicate that needs to be expanded is
__CPROVER_points_to_valid_memory (name subject to change).
The __CPROVER_points_to_valid_memory predicates takes two parameters,
a pointer and a size. Semantically,
__CPROVER_points_to_valid_memory(p, size) should be true if and only
if p points to a memory object which is valid to read/write for at
least size bytes past p. When used in assertions, this will be checked
in a similar manner to how --pointer-check checks validity of a
dereference. When used in assumptions, this predicate creates (if none
exists already) an object for p to refer to, using
local_bitvector_analysis to make that determination, and then makes
assumptions (again corresponding to the assertions made by
--pointer-check) about that object.
This commit adds support for a one-argument form of __CPROVER_points_to_valid_memory, taking only a pointer, with no size. If ptr has type T*, then __CPROVER_points_to_valid_memory(ptr) is equivalent to __CPROVER_points_to_valid_memory(ptr, sizeof(T)).
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, and adds code contracts help text to goto-instrument
karkhaz
requested review from
allredj,
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli,
romainbrenguier,
smowton,
tautschnig and
thk123
as code owners
|
A quick question: is the new __CPROVER_points_to_valid_memory() basically the same as __CPROVER_r_ok()? |
|
Another small one: The tweak to .gitignore should be a separate PR, it's very unrelated. |
|
The tests go into three different directories -- focus on regression/contracts? |
|
Commits such as 724ed52 could also be separate PRs. |
7 tasks
owen-mc-diffblue
pushed a commit
to owen-mc-diffblue/cbmc
that referenced
this pull request
Feb 28, 2019
This branch is not taken by symex but it is taken by the slicer. The code I've removed has no effect, as far as I can tell, and may have been left over from an old implementation from before the beginning of the git history. Note, there is a commit that splits ID_dynamic_object into two different ids. See diffblue#2646 and diffblue#3769 for more details.
|
Closing, but please don't delete. I'm going to post separate and more manageable PRs for this a little at a time. |
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 is a squash of the memory predicate patch (#2706) and the code contracts patch (#2677) by Klaas. Klaas has agreed for me to take ownership of these patches and work to get them merged.
At the moment, I haven't made many changes. I plan to clean them up over the next few weeks, but please chime in: I would be grateful for any guidance on what changes need to be made in order to get these patches merged. I'll be reading the comments on the old PRs, but please let's continue the discussion here.