CBMC
dfcc_wrapper_program.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 \*******************************************************************/
8 
12 
13 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_WRAPPER_PROGRAM_H
14 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_WRAPPER_PROGRAM_H
15 
17 
18 #include <util/message.h>
19 #include <util/namespace.h>
20 #include <util/std_expr.h>
21 
23 #include "dfcc_contract_mode.h"
24 
25 #include <set>
26 
27 class goto_modelt;
28 class messaget;
29 class message_handlert;
30 class dfcc_instrumentt;
31 class dfcc_libraryt;
35 
96 {
97 public:
114  const symbolt &wrapper_symbol,
115  const symbolt &wrapped_symbol,
117  const symbolt &caller_write_set_symbol,
123 
126  void add_to_dest(goto_programt &dest, std::set<irep_idt> &dest_fp_contracts);
127 
128 protected:
136 
139 
141  std::optional<symbol_exprt> return_value_opt;
142 
145 
148 
151 
154 
157 
160 
163 
166 
169  std::set<irep_idt> function_pointer_contracts;
170 
179 
183 
184  // The body of a wrapper function is decomposed in different sections.
185  // Each type of contract clause may add instructions to multiple sections.
186  // The sections then get added to the target program by \ref add_to_dest
187  // in the declaration order below.
188 
199 
202  void add_to_dest(goto_programt &dest);
203 
210 
217 
226 
231  void encode_is_fresh_set();
232 
235 
237  void encode_ensures_clauses();
238 
240  void encode_function_call();
241 
245 
250 };
251 
252 #endif
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition: c_expr.h:233
Generates GOTO functions modelling a contract assigns and frees clauses.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
Generates the body of a wrapper function from a contract specified using requires,...
const source_locationt wrapper_sl
Source location with wrapper function name as function name.
void encode_ensures_clauses()
Encodes postconditions, instruments them to check for side effects.
const symbol_exprt contract_write_set
Symbol for the write set object derived from the contract.
void encode_havoced_function_call()
Creates instructions that havoc the contract write set, create a nondet return value,...
const symbol_exprt caller_write_set
void encode_requires_write_set()
Encodes the empty write set used to check for side effects in requires.
void encode_requires_clauses()
Encodes preconditions, instruments them to check for side effects.
void encode_is_fresh_set()
Encodes the object set used to evaluate is fresh predicates,.
const symbol_exprt addr_of_requires_write_set
Symbol for the pointer to the write set used to check requires clauses.
void encode_contract_write_set()
Encodes the write set of the contract being checked/replaced (populated by calling functions provided...
const dfcc_contract_functionst & contract_functions
goto_programt link_allocated_caller
message_handlert & message_handler
const code_with_contract_typet & contract_code_type
const symbolt & contract_symbol
const symbol_exprt requires_write_set
Symbol for the write set used to check requires clauses for side effects.
exprt::operandst contract_lambda_parameters
Vector of arguments to use to instantiate the lambdas wrapping the contract clauses.
const symbol_exprt addr_of_ensures_write_set
Symbol for the pointer to the write set used to check ensures clauses.
const dfcc_contract_modet contract_mode
void encode_checked_function_call()
Creates a checked function call to the wrapped function, passing it the contract-derived write set as...
std::set< irep_idt > function_pointer_contracts
Set of required or ensured contracts for function pointers discovered when processing the contract of...
const symbol_exprt addr_of_is_fresh_set
Symbol for the pointer to the is_fresh object set.
dfcc_lift_memory_predicatest & memory_predicates
const symbolt & wrapper_symbol
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.
void encode_function_call()
Encodes the function call section of the wrapper program.
const symbolt & wrapped_symbol
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)
const symbol_exprt addr_of_contract_write_set
Symbol for the pointer to the write set object derived from the contract.
const symbol_exprt ensures_write_set
Symbol for the write set used to check ensures clauses for side effects.
std::optional< symbol_exprt > return_value_opt
Symbol for the return value of the wrapped function.
dfcc_instrumentt & instrument
void encode_ensures_write_set()
Encodes the empty write set used to check for side effects in ensures.
goto_programt link_deallocated_contract
const symbol_exprt is_fresh_set
Symbol for the object set used to evaluate is_fresh predicates.
std::vector< exprt > operandst
Definition: expr.h:58
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Expression to hold a symbol (variable)
Definition: std_expr.h:131
Symbol table entry.
Definition: symbol.h:28
Translates assigns and frees clauses of a function contract into goto functions that allow to build a...
Enum type representing the contract checking and replacement modes.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Program Transformation.
API to expression classes.