36template <
typename K,
typename V>
37std::map<V, K>
swap_map(std::map<K, V>
const &map)
39 std::map<V, K> result;
40 for(
auto const &pair : map)
41 result.insert({pair.second, pair.first});
46#define CONTRACTS_PREFIX CPROVER_PREFIX "contracts_"
51 return std::map<dfcc_typet, irep_idt>{
207 return dfcc_hook.find(function_id)->second;
211std::optional<dfcc_funt>
216 return {found->second};
224 sl.
add_pragma(
"disable:pointer-primitive-check");
225 sl.
add_pragma(
"disable:pointer-overflow-check");
226 sl.
add_pragma(
"disable:signed-overflow-check");
227 sl.
add_pragma(
"disable:unsigned-overflow-check");
229 sl.
add_pragma(
"disable:undefined-shift-check");
236 auto &function =
goto_model.goto_functions.function_map[pair.second];
237 for(
auto &inst : function.body.instructions)
246 std::set<irep_idt> missing;
249 missing.insert(
"malloc");
253 missing.insert(
"free");
268 symbol_tablet::symbolst::const_iterator found =
269 goto_model.symbol_table.symbols.find(pair.second);
272 found ==
goto_model.symbol_table.symbols.end() ||
273 found->second.value.is_nil())
275 missing.insert(pair.second);
286 !
loaded,
"the cprover_contracts library can only be loaded once");
289 log.status() <<
"Adding the cprover_contracts library (" <<
config.ansi_c.arch
293 to_instrument.insert(
"malloc");
294 to_instrument.insert(
"free");
297 std::set<irep_idt> to_load;
310 to_load.insert(
"malloc");
311 to_load.insert(
"free");
322 for(
const auto &symbol_pair : tmp_symbol_table.
symbols)
324 const auto &sym = symbol_pair.first;
326 goto_model.symbol_table.insert(symbol_pair.second);
330 for(
const auto &
id : missing)
334 goto_model.symbol_table.get_writeable_ref(
id).set_compiled();
343 goto_model.goto_functions.function_map.find(pair.second);
346 found !=
goto_model.goto_functions.function_map.end() &&
347 found->second.body_available(),
348 "The body of DFCC library function " +
id2string(pair.second) +
349 " could not be found");
368 goto_model.goto_functions.function_map.at(it.second.name).make_hidden();
375 return {found->second};
439 "dfcc_libraryt::specialize_functions can only be called once");
443 std::list<std::string> loop_names;
447 const auto &function = entry.first;
448 const auto &loop_id = entry.second;
449 std::stringstream stream;
451 << contract_assigns_size + 1;
452 const auto &str = stream.str();
453 loop_names.push_back(str);
473 "dfcc_libraryt::fix_malloc_free_calls can only be called once");
482 if(ins->is_function_call())
484 const auto &function = ins->call_function();
486 if(function.id() == ID_symbol)
503 std::string options =
"assert-false";
509 const auto &function_id = it.first;
510 if(
goto_model.symbol_table.has_symbol(function_id))
512 auto &goto_function =
513 goto_model.goto_functions.function_map.at(function_id);
516 goto_function,
goto_model.symbol_table, function_id);
523 const irep_idt map_name =
"__dfcc_instrumented_functions";
525 if(
goto_model.symbol_table.has_symbol(map_name))
526 return goto_model.symbol_table.lookup_ref(map_name);
535 "__dfcc_instrumented_functions",
538 "<built-in-library>",
544 const std::set<irep_idt> &instrumented_functions,
548 auto instrumented_functions_map =
551 for(
auto &function_id : instrumented_functions)
556 auto index_expr =
index_exprt(instrumented_functions_map, object_id);
564 const exprt &address_of_write_set,
565 const exprt &max_assigns_clause_size,
566 const exprt &max_frees_clause_size,
567 const exprt &assume_requires_ctx,
568 const exprt &assert_requires_ctx,
569 const exprt &assume_ensures_ctx,
570 const exprt &assert_ensures_ctx,
571 const exprt &allow_allocate,
572 const exprt &allow_deallocate,
575 auto function_symbol =
580 arguments.emplace_back(address_of_write_set);
582 arguments.emplace_back(max_assigns_clause_size);
584 arguments.emplace_back(max_frees_clause_size);
585 arguments.push_back(assume_requires_ctx);
586 arguments.push_back(assert_requires_ctx);
587 arguments.push_back(assume_ensures_ctx);
588 arguments.push_back(assert_ensures_ctx);
589 arguments.push_back(allow_allocate);
590 arguments.push_back(allow_deallocate);
596 const exprt &address_of_write_set,
597 const exprt &max_assigns_clause_size,
601 address_of_write_set,
602 max_assigns_clause_size,
614 const exprt &write_set_ptr,
625 const exprt &write_set_ptr,
631 {write_set_ptr, ptr});
637 const exprt &write_set_ptr,
643 {write_set_ptr, ptr});
649 const exprt &write_set_ptr,
655 {write_set_ptr, ptr});
661 const exprt &write_set_ptr,
667 {write_set_ptr, ptr});
674 const exprt &check_var,
675 const exprt &write_set_ptr,
688 const exprt &check_var,
689 const exprt &write_set_ptr,
697 {write_set_ptr, ptr, size});
703 const exprt &check_var,
704 const exprt &write_set_ptr,
711 {write_set_ptr, dest});
717 const exprt &check_var,
718 const exprt &write_set_ptr,
725 {write_set_ptr, dest});
731 const exprt &check_var,
732 const exprt &write_set_ptr,
740 {write_set_ptr, dest, src});
746 const exprt &check_var,
747 const exprt &write_set_ptr,
754 {write_set_ptr, ptr});
760 const exprt &check_var,
761 const exprt &write_set_ptr,
768 {write_set_ptr, ptr});
775 const exprt &check_var,
776 const exprt &reference_write_set_ptr,
777 const exprt &candidate_write_set_ptr,
784 {reference_write_set_ptr, candidate_write_set_ptr});
791 const exprt &check_var,
792 const exprt &reference_write_set_ptr,
793 const exprt &candidate_write_set_ptr,
800 {reference_write_set_ptr, candidate_write_set_ptr});
806 const exprt &write_set_ptr,
807 const exprt &target_write_set_ptr,
812 {write_set_ptr, target_write_set_ptr});
818 const exprt &write_set_ptr,
819 const exprt &ptr_pred_ctx_ptr,
824 {write_set_ptr, ptr_pred_ctx_ptr});
830 const exprt &write_set_postconditions_ptr,
831 const exprt &write_set_to_link_ptr,
836 {write_set_postconditions_ptr, write_set_to_link_ptr});
842 const exprt &write_set_postconditions_ptr,
843 const exprt &write_set_to_link_ptr,
848 {write_set_postconditions_ptr, write_set_to_link_ptr});
856 const exprt &write_set_ptr,
862 {ptr, write_set_ptr});
869 const exprt &obj_set_ptr,
881 const exprt &obj_set_ptr,
891 const exprt &ptr_pred_ctx_ptr,
902 const exprt &ptr_pred_ctx_ptr,
void cprover_c_library_factory_force_load(const std::set< irep_idt > &functions, symbol_table_baset &symbol_table, message_handlert &message_handler)
Load the requested function symbols from the cprover library and add them to the symbol table regardl...
API to expression classes that are internal to the C frontend.
unsignedbv_typet size_type()
unsignedbv_typet unsigned_char_type()
Operator to return the address of an object.
Array constructor from single element.
goto_instruction_codet representation of a function call statement.
const code_function_callt write_set_record_dead_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_dead.
const std::map< irep_idt, dfcc_funt > havoc_hook
Maps front-end functions to library functions giving their havoc semantics.
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.
static bool inlined
True iff the library functions are inlined.
const std::map< irep_idt, dfcc_funt > dfcc_hook
Maps built-in function names to enums to use for instrumentation.
const code_function_callt write_set_check_assignment_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const exprt &size, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assignment.
static bool loaded
True iff the contracts library symbols are loaded.
dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler)
Class constructor.
void fix_malloc_free_calls()
Fixes function calls to malloc and free in library functions.
static bool malloc_free_fixed
True iff the library functions uses of malloc and free are fixed.
bool is_front_end_builtin(const irep_idt &function_id) const
Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole,...
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 std::map< irep_idt, dfcc_typet > dfcc_name_to_type
Swapped dfcc_type_to_name.
const code_function_callt write_set_record_deallocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_deallocated.
const code_function_callt write_set_add_decl_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_decl.
void inline_functions()
Inlines library functions that need to be inlined before use.
const code_function_callt write_set_check_array_copy_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_copy.
const code_function_callt link_ptr_pred_ctx_call(const exprt &write_set_ptr, const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_ptr_pred_ctx.
const code_function_callt write_set_add_allocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_allocated.
std::optional< dfcc_funt > get_dfcc_fun(const irep_idt &id) const
Returns the dfcc_funt that corresponds to the given id if any.
const std::set< irep_idt > assignable_builtin_names
All built-in function names (front-end and instrumentation hooks)
void add_instrumented_functions_map_init_instructions(const std::set< irep_idt > &instrumented_functions, const source_locationt &source_location, goto_programt &dest)
Generates instructions to initialize the instrumented function map symbol from the given set of instr...
const std::map< dfcc_typet, irep_idt > dfcc_type_to_name
Enum to type name mapping.
const symbolt & get_instrumented_functions_map_symbol()
Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.
const std::map< dfcc_funt, irep_idt > dfcc_fun_to_name
enum to function name mapping
const std::map< irep_idt, dfcc_funt > dfcc_name_to_fun
const code_function_callt write_set_check_array_set_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_set.
const code_function_callt write_set_check_array_replace_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const exprt &src, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_replace.
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 ptr_pred_ctx_init_call(const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_ptr_pred_ctx_init.
void inhibit_front_end_builtins()
Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __...
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 irep_idt & get_dfcc_fun_name(dfcc_funt fun) const
Returns the name of the given dfcc_funt.
dfcc_funt get_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given front-end function.
const code_function_callt ptr_pred_ctx_reset_call(const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_ptr_pred_ctx_init.
bool is_dfcc_library_symbol(const irep_idt &id) const
True iff the given id is one of the library symbols.
const code_function_callt write_set_check_deallocate_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_deallocate.
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.
message_handlert & message_handler
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
std::set< irep_idt > get_missing_funs()
Collects the names of all library functions currently missing from the goto_model into missing.
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_check_havoc_object_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_havoc_object.
void disable_checks()
Adds "checked" pragmas to instructions of all library functions instructions.
const code_function_callt check_replace_ensures_was_freed_preconditions_call(const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.
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 specialize(const std::size_t contract_assigns_size_hint)
Specializes the library by unwinding loops in library functions to the given assigns clause size.
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
std::optional< dfcc_funt > get_havoc_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given built-in.
void load(std::set< irep_idt > &to_instrument)
After calling this function, all library types and functions are present in the the goto_model.
static bool specialized
True iff the library functions are specialized to a particular contract.
Base class for all expressions.
typet & type()
Return the type of the expression.
source_locationt & add_source_location()
The Boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
An expression denoting infinity.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void add_pragma(const irep_idt &pragma)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
const std::map< irep_idt, dfcc_funt > create_havoc_hook()
static const std::set< dfcc_funt > to_inline
set of functions that need to be inlined
const std::map< dfcc_funt, irep_idt > create_dfcc_fun_to_name()
const std::set< irep_idt > create_assignable_builtin_names()
static void add_checked_pragmas(source_locationt &sl)
const std::map< dfcc_typet, irep_idt > create_dfcc_type_to_name()
Creates the enum to type name mapping.
std::map< V, K > swap_map(std::map< K, V > const &map)
Swaps keys and values in a map.
static const std::set< dfcc_funt > fix_malloc_free_set
Set of functions that contain calls to assignable_malloc or assignable_free.
static const std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
const std::map< irep_idt, dfcc_funt > create_dfcc_hook()
Dynamic frame condition checking library loading.
dfcc_funt
One enum value per function defined by the cprover_dfcc.c library file.
@ WRITE_SET_INSERT_OBJECT_UPTO
@ WRITE_SET_CHECK_ASSIGNMENT
@ WRITE_SET_INSERT_ASSIGNABLE
@ WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION
@ WRITE_SET_INSERT_OBJECT_WHOLE
@ WRITE_SET_DEALLOCATE_FREEABLE
@ WRITE_SET_CHECK_ARRAY_REPLACE
@ WRITE_SET_CHECK_HAVOC_OBJECT
@ OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID
@ WRITE_SET_CHECK_DEALLOCATE
@ WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY
@ WRITE_SET_CHECK_ARRAY_SET
@ WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION
@ WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET
@ WRITE_SET_CHECK_ARRAY_COPY
@ REPLACE_ENSURES_WAS_FREED_PRECONDITIONS
@ WRITE_SET_RECORD_DEALLOCATED
@ WRITE_SET_ADD_ALLOCATED
@ WRITE_SET_HAVOC_OBJECT_WHOLE
@ WRITE_SET_INSERT_OBJECT_FROM
dfcc_typet
One enum value per type defined by the cprover_dfcc.c library file.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ PTR_PRED_CTX_PTR
type of pointers to context info for pointer predicates evaluation
@ CAR_SET_PTR
type of pointers to sets of CAR
@ CAR_SET
type of sets of CAR
@ OBJ_SET_PTR
type of pointers to sets of object identifiers
@ PTR_PRED_CTX
type of context info for pointer predicates evaluation
@ OBJ_SET
type of sets of object identifiers
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
@ CAR
type of descriptors of conditionally assignable ranges of bytes
Dynamic frame condition checking utility functions.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static void inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
Inlines the given function, aborts on recursive calls during inlining.
static const symbolt & create_static_symbol(symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol ...