cprover
Loading...
Searching...
No Matches
dfcc_wrapper_program.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: 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/optional.h>
21#include <util/std_expr.h>
22
24#include "dfcc_contract_mode.h"
25
26#include <set>
27
28class goto_modelt;
29class messaget;
32class dfcc_libraryt;
36
97{
98public:
115 const symbolt &wrapper_symbol,
116 const symbolt &wrapped_symbol,
118 const symbolt &caller_write_set_symbol,
124
127 void add_to_dest(goto_programt &dest, std::set<irep_idt> &dest_fp_contracts);
128
129protected:
137
140
143
146
149
152
155
158
161
164
167
170 std::set<irep_idt> function_pointer_contracts;
171
180
184
185 // The body of a wrapper function is decomposed in different sections.
186 // Each type of contract clause may add instructions to multiple sections.
187 // The sections then get added to the target program by \ref add_to_dest
188 // in the declaration order below.
189
200
203 void add_to_dest(goto_programt &dest);
204
211
218
227
232 void encode_is_fresh_set();
233
236
239
242
246
251};
252
253#endif
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:232
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.
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
message_handlert & message_handler
const code_with_contract_typet & contract_code_type
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
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.
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.
dfcc_instrumentt & instrument
void encode_ensures_write_set()
Encodes the empty write set used to check for side effects in ensures.
optionalt< symbol_exprt > return_value_opt
Symbol for the return value of the wrapped function.
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.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:113
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.
nonstd::optional< T > optionalt
Definition optional.h:35
API to expression classes.