cprover
|
Back to top Code Contracts Transformation Specification
Applying the DFCC instrumentation to a function turns it into a function that can be checked against a write set passed as parameter.
The signature of a function:
is turned into the extended version:
After this step the write_set parameter is in scope in the function and can be used to implement checks.
It is valid to pass a NULL pointer for the write_set parameter. When the write_set parameter is NULL, no checks are performed in the function.
Body instrumentation inserts additional goto instructions in the function's GOTO instruction sequence.
All instrumented checks are guarded by a null-check on the write_set pointer parameter. Hence, passing a NULL pointer results in no checks being performed in the function.
No instrumentation is performed.
No instrumentation is performed.
Assign instructions trigger a check on the LHS but also triggers an update of the write set if the RHS if it represents a dynamic allocation or deallocation.
Checks are inserted before the instruction.
If the LHS is either:
Then no check is performed, i.e. ASSERT true; is inserted:
Otherwise, we check that the LHS is found in the write set's contract_assigns set or the allocated set as shown below:
For the write set updates we consider the following cases.
If the RHS of the assignment is a side_effect_exprt(statement = ID_allocate) expression, it represents a dynamic allocation. We record it in the write set:
If the assignment is an nondeterministic update to the __CPROVER_dead_object, it in fact models a dynamic deallocation. Such instructions are generated to deallocate objects allocated with the dynamic stack allocation function __builtin_alloca and are always legal. We just record the deallocation.
If the function call is a call to the __CPROVER_deallocate function, it represents a dynamic deallocation and we check that the deallocated pointer is allowed by the write set, and then record the deallocation in the write set.
Calls to __CPROVER_was_freed or __CPROVER_is_freeable are rewritten as described in Rewriting Calls to __CPROVER_is_freeable and __CPROVER_was_freed Predicates
Calls to __CPROVER_is_fresh are rewritten as described in Rewriting Calls to the __CPROVER_is_fresh Predicate
Calls to __CPROVER_obeys_contract are rewritten as described in Rewriting Calls to the __CPROVER_obeys_contract Predicate
Calls to __CPROVER_pointer_in_range_dfcc are rewritten as described in Rewriting Calls to the __CPROVER_pointer_in_range_dfcc Predicate
Calls to __CPROVER_pointer_equals are rewritten as described in Rewriting Calls to the __CPROVER_pointer_equals Predicate
For all other function or function pointer calls, we proceed as follows.
If the function call has an LHS (i.e. its result is assigned to a return value variable), the LHS gets checked like for an assignment, and we pass the write set as an extra parameter to the function (remember that all functions of the goto models are extended with write_set parameters by the transformation).
OTHER instructions describe special built-in operations that have no explicit C or GOTO representation (they are given a semantics directly by the symex engine). From goto_symext::symex_other we see the possible operations are:
Remark: the instructions code_inputt, code_outputt and ID_nondet would also need to be instrumented as they perform side effects and introduce non-determinism, but this is not handled as of today and will trigger warnings.
For DFCC we only instrument the array_set, array_copy, array_replace and havoc_object operations.
The example below is for __CPROVER_array_set, and the dest pointer must be found in the contract_assigns set or the allocated set.
The ranges of bytes (void *lb, size_t size) updated by the different operations are:
Prev | Next |
---|---|
Dynamic Frame Condition Checking | Proof Harness Intrumentation |