CBMC
|
Generates the body of a wrapper function from a contract specified using requires, assigns, frees, ensures, clauses attached to a function symbol. More...
#include <dfcc_wrapper_program.h>
Public Member Functions | |
dfcc_wrapper_programt (const dfcc_contract_modet contract_mode, const symbolt &wrapper_symbol, const symbolt &wrapped_symbol, const dfcc_contract_functionst &contract_functions, const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates) | |
void | add_to_dest (goto_programt &dest, std::set< irep_idt > &dest_fp_contracts) |
Adds the whole program to dest and the discovered function pointer contracts dest_fp_contracts . More... | |
Protected Member Functions | |
void | add_to_dest (goto_programt &dest) |
Adds the whole generated program to dest , which is meant to be a part of the body of the wrapper_symbol . More... | |
void | encode_requires_write_set () |
Encodes the empty write set used to check for side effects in requires. More... | |
void | encode_ensures_write_set () |
Encodes the empty write set used to check for side effects in ensures. More... | |
void | encode_contract_write_set () |
Encodes the write set of the contract being checked/replaced (populated by calling functions provided in contract_functions) More... | |
void | encode_is_fresh_set () |
Encodes the object set used to evaluate is fresh predicates,. More... | |
void | encode_requires_clauses () |
Encodes preconditions, instruments them to check for side effects. More... | |
void | encode_ensures_clauses () |
Encodes postconditions, instruments them to check for side effects. More... | |
void | encode_function_call () |
Encodes the function call section of the wrapper program. More... | |
void | encode_checked_function_call () |
Creates a checked function call to the wrapped function, passing it the contract-derived write set as parameter. More... | |
void | encode_havoced_function_call () |
Creates instructions that havoc the contract write set, create a nondet return value, nondeterministically free the freeable part of the write set. More... | |
Generates the body of a wrapper function from a contract specified using requires, assigns, frees, ensures, clauses attached to a function symbol.
The desired mode CHECK or REPLACE is given to the constructor of the class.
The body of the wrapper is divided into a number of sections represented as separate goto_programs:
There a private method per type of contract clause, which adds contents encoding the semantics of the clause to the appropriate section when called.
The public method add_to_dest calls the private methods to populate the sections, and then adds the contents of these sections in order to the given destination program.
Definition at line 95 of file dfcc_wrapper_program.h.
dfcc_wrapper_programt::dfcc_wrapper_programt | ( | const dfcc_contract_modet | contract_mode, |
const symbolt & | wrapper_symbol, | ||
const symbolt & | wrapped_symbol, | ||
const dfcc_contract_functionst & | contract_functions, | ||
const symbolt & | caller_write_set_symbol, | ||
goto_modelt & | goto_model, | ||
message_handlert & | message_handler, | ||
dfcc_libraryt & | library, | ||
dfcc_instrumentt & | instrument, | ||
dfcc_lift_memory_predicatest & | memory_predicates | ||
) |
contract_mode | checking or replacement mode for the contract |
wrapper_symbol | function symbol receiving the generated instructions |
wrapped_symbol | function symbol being checked or replaced |
contract_functions | contains the contract expressions and the assigns/frees/havoc functions symbols derived from the contract |
caller_write_set_symbol | symbol representing the write set passed to the wrapper function by its caller. |
goto_model | the goto model being transformed |
message_handler | used for debug/warning/error messages |
library | the contracts instrumentation library |
instrument | the instrumenter class for goto functions/goto programs |
memory_predicates | handler for user-defed memory predicates, used to adjust call parameters for user defined predicates used in requires and ensures clauses. |
Definition at line 144 of file dfcc_wrapper_program.cpp.
|
protected |
Adds the whole generated program to dest
, which is meant to be a part of the body of the wrapper_symbol
.
Definition at line 244 of file dfcc_wrapper_program.cpp.
void dfcc_wrapper_programt::add_to_dest | ( | goto_programt & | dest, |
std::set< irep_idt > & | dest_fp_contracts | ||
) |
Adds the whole program to dest
and the discovered function pointer contracts dest_fp_contracts
.
Definition at line 235 of file dfcc_wrapper_program.cpp.
|
protected |
Creates a checked function call to the wrapped function, passing it the contract-derived write set as parameter.
Definition at line 656 of file dfcc_wrapper_program.cpp.
|
protected |
Encodes the write set of the contract being checked/replaced (populated by calling functions provided in contract_functions)
Definition at line 414 of file dfcc_wrapper_program.cpp.
|
protected |
Encodes postconditions, instruments them to check for side effects.
Definition at line 588 of file dfcc_wrapper_program.cpp.
|
protected |
Encodes the empty write set used to check for side effects in ensures.
Definition at line 331 of file dfcc_wrapper_program.cpp.
|
protected |
Encodes the function call section of the wrapper program.
Definition at line 648 of file dfcc_wrapper_program.cpp.
|
protected |
Creates instructions that havoc the contract write set, create a nondet return value, nondeterministically free the freeable part of the write set.
Definition at line 692 of file dfcc_wrapper_program.cpp.
|
protected |
Encodes the object set used to evaluate is fresh predicates,.
Definition at line 502 of file dfcc_wrapper_program.cpp.
|
protected |
Encodes preconditions, instruments them to check for side effects.
Definition at line 537 of file dfcc_wrapper_program.cpp.
|
protected |
Encodes the empty write set used to check for side effects in requires.
Definition at line 259 of file dfcc_wrapper_program.cpp.
|
protected |
Symbol for the pointer to the write set object derived from the contract.
Definition at line 147 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the pointer to the write set used to check ensures clauses.
Definition at line 159 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the pointer to the is_fresh object set.
Definition at line 165 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the pointer to the write set used to check requires clauses.
Definition at line 153 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 135 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 134 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 132 of file dfcc_wrapper_program.h.
|
protected |
Vector of arguments to use to instantiate the lambdas wrapping the contract clauses.
Definition at line 182 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 129 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 133 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the write set object derived from the contract.
Definition at line 144 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 178 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the write set used to check ensures clauses for side effects.
Definition at line 156 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 194 of file dfcc_wrapper_program.h.
|
protected |
Set of required or ensured contracts for function pointers discovered when processing the contract of interest.
Definition at line 169 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 171 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 192 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 175 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the object set used to evaluate is_fresh predicates.
Definition at line 162 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 174 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 195 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 196 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 190 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 173 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 176 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 172 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 177 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 198 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 197 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 189 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 191 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the write set used to check requires clauses for side effects.
Definition at line 150 of file dfcc_wrapper_program.h.
|
protected |
Symbol for the return value of the wrapped function.
Definition at line 141 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 131 of file dfcc_wrapper_program.h.
|
protected |
Source location with wrapper function name as function name.
Definition at line 138 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 130 of file dfcc_wrapper_program.h.
|
protected |
Definition at line 193 of file dfcc_wrapper_program.h.