CONTRACTS: Dynamic frame condition checking #6887
Closed
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
remi-delmas-3000
added
do not merge
dependent - do not merge
aws
remi-delmas-3000
requested review from
SaswatPadhi,
martin-cs,
chris-ryder,
peterschrammel and
kroening
as code owners
remi-delmas-3000
force-pushed
the
contracts-dfcc
branch
from
7fe0e6d to
4d368ae
Compare
Codecov ReportBase: 77.87% // Head: 77.90% // Increases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #6887 +/- ##
===========================================
+ Coverage 77.87% 77.90% +0.03%
===========================================
Files 1576 1593 +17
Lines 181824 184380 +2556
===========================================
+ Hits 141598 143649 +2051
- Misses 40226 40731 +505
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report at Codecov. |
remi-delmas-3000
force-pushed
the
contracts-dfcc
branch
from
61748d2 to
1a24104
Compare
remi-delmas-3000
force-pushed
the
contracts-dfcc
branch
4 times, most recently
from
3183180 to
f6e22e9
Compare
remi-delmas-3000
force-pushed
the
contracts-dfcc
branch
5 times, most recently
from
0190a5a to
102d2b2
Compare
remi-delmas-3000
force-pushed
the
contracts-dfcc
branch
3 times, most recently
from
4f373d7 to
7d98112
Compare
added 18 commits
September 22, 2022 11:36
`__CPROVER_is_freshr` works like `__CPROVER_is_fresh` but takes pointers by reference instead of by value. This willallow using the predicate from within user-defined functions. Only type-checking in the front-end is implemented, support in the back-end will come with dynamic frames.
The `dfcc_utilst` class provides methods to manipulate function symbols in the symbol table: - create fresh symbols - clone and rename function parameter lists, - clone and rename function symbols, - add parameters to functions symbols and goto functions These transformations will help us implement dynamic frames.
`cprover_contracts.c` defines C types representing dynamic frames: - `__CPROVER_contract_car_t` - `__CPROVER_contract_car_set_t` - `__CPROVER_contract_obj_set_t` - `__CPROVER_contract_write_set_t` It also defines functions that build and check frame conditions in various situations: - allocations/deallocations, - assignments, - array operations, - havoc operations, - assigns clause inclusion checks for contract replacement, - frees clause inclusion checks for contract replacement, - etc. It also provides C implementations for built-in predicates: - `__CPROVER_contracts_is_freeable` for `__CPROVER_is_freeable` - `__CPROVER_contracts_is_freed` for `__CPROVER_is_freed` - `__CPROVER_contracts_is_freshr` for `__CPROVER_is_fresh` and `__CPROVER_is_freshr` The class `dfcc_libraryt` provides a programmatic interface to load and use the library types and functions and perform some optimisations like inlining or unwinding loops in library functions. dfcc_libraryt fixes
- `dfcc_contract_modet` is an enum representing the CHECK and REPLACE modes for contracts, - `dfcc_contract_handlert` is an abstract interface for generating GOTO instructions from contracts for CHECK or REPLACE modes.
Rewrite calls to - `is_fresh` to `__CPROVER_contracts_is_freshr` - `is_freshr` to `__CPROVER_contracts_is_freshr` - `is_freeable` to `__CPROVER_contracts_is_freeable` - `is_freed` to `__CPROVER_contracts_is_freed`
This class extends `cfg_infot` and computes locals and dirty locals directly from a goto program's instruction sequence. Contary to `function_cfg_infot` it does not consider function parameters as locals.
programs with checks against a dynamic frame.
This class rewrites `__CPROVER_assignable_t` and `__CPROVER_freeable_t` functions into functions that accept two extra write set parameters. Targets specified by the function are added to the first write set. The second write set is used to check that any other the side effect performed by the function is allowed. This second write set will usually be the empty write set, or a write set that allows only writing to history variables.
The class translates the assigns and frees clauses of a contract expressed in DSL style into goto functions returning `__CPROVER_assignable_t` and `__CPROVER_freeable_t` types and describing the same set of targets as the clause. Internally it uses the `dfcc_spec_functiontst` class to translate the functions generated from the clauses into functions that dynamically build write sets at runtime. A havoc function is also generated for the assigns clause, that havocs the locations described by the clause in a type-directed way, taking snapshots of start addresses from a write set instance.
The class generates a sequence of GOTO instruction from a contract expressed in the DSL syntax. These instructions are meant to be added to the GOTO function that serves as a wrapper for the function under verification or being replaced by the contract. It first uses `dfcc_dsl_contract_functionst` to generate goto functions from the contract's assigns and frees clauses. In contract checking mode, it generates GOTO instructions that assume preconditions, snapshots history variables, creates a write set instance, call the function under verification asserts the postconditions, and returns the call's return value. In contract replacement mode, it generates GOTO instructions encoding the nondeterministic abstraction defined by the contract: assert preconditions, create and havoc assigns clause targets, create a nondet return value for the call, nondeterministically free frees clause targets, assume postconditions, return a value that satisfies the post conditions.
This class implements the abstract `dfcc_contract_handlert` interfance for DSL-style contracts using the class `dfcc_dsl_wrapper_programt`.
Given a `function_id`, a `contract_id`, a contract `mode`, and a `dfcc_contract_handlert` for the contract, this class swaps the body of the function to a function with a mangled name, instruments the mangled function for dynamic frame condition checking using `dfcc_instrument`. The body of the original function is then replaced with instructions generated by the contract handler for the required contract mode. To handle recursive functions in contract checking mode, the body of the wrapper function is generated in such a way the first invocation results in checking the contract against the mangled function and recursive invocations of the wrapper behave like the contract abstraction (modelling that the contract holds).
function contracts with dynamic frames. The class receives the proof harness function, the map of functions and contracts to check and the map of functions to replace with contracts. It instruments the proof harness, performs swap-and-wrap operations for each of the checked and replaced functions. It then instruments all other functions for DFCC.
The switch expects the harness function name as parameter, and accepts any number of `--enforce-contract` and `--replace-call-with-contract` switches.
Updated tests - update assigns-enforce-malloc-zero - update assigns-local-composite - update assigns-replace-ignored-return-value - update assigns-replace-malloc-zero - update assigns-slice-targets - update assigns-slice-targets - update assigns_enforce_01 - update assigns_enforce_02 - update assigns_enforce_03 - update assigns_enforce_04 - update assigns_enforce_05 - update assigns_enforce_06 - update assigns_enforce_07
remi-delmas-3000
force-pushed
the
contracts-dfcc
branch
from
7bf890c to
29ef0b0
Compare
6 tasks
6 tasks
|
Fixes #7197 |
|
Fixes #7198 |
|
Fixes #7206 |
This was referenced Oct 5, 2022
7 tasks
7 tasks
|
Superseded by #7242 |
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.
Dependencies
The first 6 commits are from these other PRs (do not read)
function_pointer_obeys_contract_exprt#7082inlining_decoratort#7083contracts.hmethods public. #7084OTHERinstructions. #7085The build fails with ubuntu 18.04 and I am not sure why, since no error is visible on the output.
Implement the functionality described below.
Dynamic frame condition checking (DFCC) for function contracts
Motivation
This new implementation proposes front-end extensions and a new dynamic method for checking assigns and frees clauses addressing all of the above:
Current limitations:
Frame condition checking
Let’s call
f_top the top-level function against which the contract is being checked.We assume
f_top is itself called from aharnessfunction, which may call other functions besidesf_top.Let’s consider a function
fthat is eitherf_topor one of the functions called (directly or indirectly) byf_top. The goal is to verify thatfwrites only to memory locations that are part of the frame of the call tof_topbut allowed by the contract or that were allocated after enteringf_top and are hence not part of the frame of the call. To do that, we add ghost code to the program to build representations the following sets of memory locations as the program runs:contract_assigns,contract_frees,allocated,deallocated)where:
contract_assignsis the set of memory locations specified in the assigns clause of the contract being checkedcontract_freesis the set of pointers specified in the frees clause of the contract being checkedallocatedis the set objects identifiers allocated on the stack or the heap since enteringf_topdeallocatedis the set of heap objects identifiers deallocated since enteringf_top (allows verification that an object was freed as a post-condition of the contract)The instrumentation transforms all user-defined goto functions and library functions:
Into functions accepting an extra parameter that is a pointer to a dynamic representation of the sets introduced above:
Function bodies is instrumented so that
contract_assignsorallocated,allocatedallocated__CPROVER_dead_objectare removed fromallocated__CPROVER_deallocateare checked for inclusion incontract_freesorallocated, and recorded indeallocated(so that if needed we can check in post conditions that the function indeed deallocated the expected memory).Since the write set is dynamically updated, a same function called at different call sites can see a different write set.
Write sets are initialised from contracts descriptions and injected in function calls that are checked against contracts, or used to perform inclusion checks against write sets obtained from callers for functions that are replaced by a contract.