42 "__contract_write_set",
56 "__address_of_contract_write_set",
70 "__requires_write_set",
84 "__address_of_requires_write_set",
98 "__ensures_write_set",
112 "__address_of_ensures_write_set",
140 "__address_of_is_fresh_set",
149 const symbolt &caller_write_set_symbol,
155 : contract_mode(contract_mode),
156 wrapper_symbol(wrapper_symbol),
157 wrapped_symbol(wrapped_symbol),
158 contract_functions(contract_functions),
159 contract_symbol(contract_functions.pure_contract_symbol),
161 caller_write_set(caller_write_set_symbol.symbol_expr()),
162 wrapper_sl(wrapper_symbol.location),
165 goto_model.symbol_table,
169 goto_model.symbol_table,
173 goto_model.symbol_table,
177 goto_model.symbol_table,
181 goto_model.symbol_table,
185 goto_model.symbol_table,
191 goto_model.symbol_table,
194 function_pointer_contracts(),
195 goto_model(goto_model),
196 message_handler(message_handler),
197 log(message_handler),
199 instrument(instrument),
200 memory_predicates(memory_predicates),
201 ns(goto_model.symbol_table),
202 converter(goto_model.symbol_table,
log.get_message_handler())
211 "__contract_return_value",
219 for(
const auto ¶m_id :
237 std::set<irep_idt> &dest_fp_contracts)
240 dest_fp_contracts.insert(
306 "__no_alloc_dealloc_in_requires",
320 "Check that requires do not allocate or deallocate memory");
386 "__no_alloc_dealloc_in_ensures_clauses",
400 "Check that ensures do not allocate or deallocate memory");
449 for(
const auto ¶meter : wrapper_code_type.parameter_identifiers())
452 wrapper_arguments.push_back(parameter_symbol.
symbol_expr());
463 for(
const auto &arg : wrapper_arguments)
464 arguments.push_back(arg);
482 for(
const auto &arg : wrapper_arguments)
483 arguments.push_back(arg);
542 const auto &language_mode =
547 const auto &statement_type =
556 exprt requires_lmbd =
559 if(statement_type == ID_assert)
564 " for function " +
id2string(wrapper_id));
566 codet requires_statement(statement_type, {std::move(requires_lmbd)}, sl);
592 const auto &statement_type =
610 if(statement_type == ID_assert)
615 " for function " +
id2string(wrapper_id));
618 codet ensures_statement(statement_type, {std::move(ensures)}, sl);
666 call.
lhs() = return_value;
679 for(
const auto ¶meter : wrapper_code_type.parameter_identifiers())
696 for(
const auto ¶meter :
701 write_set_arguments.push_back(parameter_symbol.
symbol_expr());
716 auto goto_instruction =
726 "__check_assigns_clause_incl",
741 " is included in the caller's assigns clause");
752 "__check_frees_clause_incl",
767 " is included in the caller's frees clause");
772 auto label_instruction =
774 goto_instruction->complete_goto(label_instruction);
778 {addr_of_contract_write_set});
API to expression classes that are internal to the C frontend.
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Operator to return the address of an object.
goto_instruction_codet representation of a function call statement.
const typet & return_type() const
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
const exprt::operandst & c_requires() const
const exprt::operandst & c_ensures() const
Data structure for representing an arbitrary statement in a program.
Generates GOTO functions modelling a contract assigns and frees clauses.
const symbolt & get_spec_frees_function_symbol() const
Returns the contract::frees function symbol.
const symbolt & get_spec_assigns_function_symbol() const
Returns the contract::c_assigns function symbol.
const std::size_t get_nof_assigns_targets() const
Returns the maximum number of targets in the assigns clause.
const symbolt & get_spec_assigns_havoc_function_symbol() const
Returns the contract::c_assigns::havoc function symbol.
const std::size_t get_nof_frees_targets() const
Returns the maximum number of targets in the frees clause.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
void instrument_goto_program(const irep_idt &function_id, goto_programt &goto_program, const exprt &write_set, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO program against a given write set variable.
Class interface to library types and functions defined in cprover_contracts.c.
const code_function_callt write_set_check_allocated_deallocated_is_empty_call(const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.
const code_function_callt obj_set_create_indexed_by_object_id_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.
const code_function_callt link_allocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_allocated.
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
const code_function_callt obj_set_release_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_release.
const code_function_callt link_deallocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_deallocated.
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt link_is_fresh_call(const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_is_fresh.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
const code_function_callt write_set_check_frees_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.
const code_function_callt write_set_deallocate_freeable_call(const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_deallocate_freeable.
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
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
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.
goto_programt postconditions
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...
goto_programt write_set_checks
goto_programt link_is_fresh
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.
goto_programt function_call
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)
goto_programt preconditions
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.
Base class for all expressions.
std::vector< exprt > operandst
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
typet & type()
Return the type of the expression.
The Boolean constant false.
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
symbol_tablet symbol_table
Symbol table.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
exprt application(const operandst &arguments) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A side_effect_exprt that returns a non-deterministically chosen value.
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
The symbol table base class interface.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
The Boolean constant true.
Translates assigns and frees clauses of a function contract into goto functions that allow to build a...
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ OBJ_SET_PTR
type of pointers to sets of object identifiers
@ OBJ_SET
type of sets of object identifiers
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Dynamic frame condition checking utility functions.
static symbol_exprt create_requires_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
static symbol_exprt create_addr_of_contract_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the contract write set pointer.
static symbol_exprt create_addr_of_ensures_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set pointer to check side effects in ensures clauses.
static symbol_exprt create_addr_of_is_fresh_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate object set pointer used to support is_fresh predicates.
static symbol_exprt create_addr_of_requires_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set pointer to check side effects in requires clauses.
static symbol_exprt create_ensures_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set to check side effects in ensures clauses.
static symbol_exprt create_contract_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the contract write set.
static symbol_exprt create_is_fresh_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate object set used to support is_fresh predicates.
Generates the body of a wrapper function from a contract for contract checking or contract replacemen...
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
#define PRECONDITION(CONDITION)
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.