CBMC
|
Class interface to library types and functions defined in cprover_contracts.c
.
More...
#include <dfcc_library.h>
Public Member Functions | |
dfcc_libraryt (goto_modelt &goto_model, message_handlert &lmessage_handler) | |
Class constructor. More... | |
void | load (std::set< irep_idt > &to_instrument) |
After calling this function, all library types and functions are present in the the goto_model. More... | |
std::optional< dfcc_funt > | get_dfcc_fun (const irep_idt &id) const |
Returns the dfcc_funt that corresponds to the given id if any. More... | |
const irep_idt & | get_dfcc_fun_name (dfcc_funt fun) const |
Returns the name of the given dfcc_funt. More... | |
bool | is_dfcc_library_symbol (const irep_idt &id) const |
True iff the given id is one of the library symbols. More... | |
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. More... | |
void | inhibit_front_end_builtins () |
Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __CPROVER_object_from __CPROVER_assignable __CPROVER_freeable An error will be triggered in case calls to these functions occur outside of a contrat clause and were hence not mapped to their library implementation. More... | |
void | disable_checks () |
Adds "checked" pragmas to instructions of all library functions instructions. More... | |
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 , __CPROVER_object_from , __CPROVER_object_upto , __CPROVER_freeable More... | |
dfcc_funt | get_hook (const irep_idt &function_id) const |
Returns the library instrumentation hook for the given front-end function. More... | |
std::optional< dfcc_funt > | get_havoc_hook (const irep_idt &function_id) const |
Returns the library instrumentation hook for the given built-in. More... | |
const symbolt & | get_instrumented_functions_map_symbol () |
Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already. More... | |
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 instrumented function. More... | |
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. More... | |
const code_function_callt | write_set_create_call (const exprt &write_set_ptr, const exprt &contract_assigns_size, const source_locationt &source_location) |
Builds call to __CPROVER_contracts_write_set_create. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
Public Attributes | |
std::map< dfcc_typet, typet > | dfcc_type |
Maps enum values to the actual types (dynamically loaded) More... | |
std::map< dfcc_funt, symbolt > | dfcc_fun_symbol |
Maps enum values to the actual function symbols (dynamically loaded) More... | |
Protected Member Functions | |
std::set< irep_idt > | get_missing_funs () |
Collects the names of all library functions currently missing from the goto_model into missing . More... | |
void | inline_functions () |
Inlines library functions that need to be inlined before use. More... | |
void | fix_malloc_free_calls () |
Fixes function calls to malloc and free in library functions. More... | |
Protected Attributes | |
goto_modelt & | goto_model |
message_handlert & | message_handler |
messaget | log |
Static Protected Attributes | |
static bool | loaded = false |
True iff the contracts library symbols are loaded. More... | |
static bool | inlined = false |
True iff the library functions are inlined. More... | |
static bool | specialized = false |
True iff the library functions are specialized to a particular contract. More... | |
static bool | malloc_free_fixed = false |
True iff the library functions uses of malloc and free are fixed. More... | |
Private Attributes | |
const std::map< dfcc_typet, irep_idt > | dfcc_type_to_name |
Enum to type name mapping. More... | |
const std::map< irep_idt, dfcc_typet > | dfcc_name_to_type |
Swapped dfcc_type_to_name. More... | |
const std::map< dfcc_funt, irep_idt > | dfcc_fun_to_name |
enum to function name mapping More... | |
const std::map< irep_idt, dfcc_funt > | dfcc_name_to_fun |
const std::map< irep_idt, dfcc_funt > | dfcc_hook |
Maps built-in function names to enums to use for instrumentation. More... | |
const std::map< irep_idt, dfcc_funt > | havoc_hook |
Maps front-end functions to library functions giving their havoc semantics. More... | |
const std::set< irep_idt > | assignable_builtin_names |
All built-in function names (front-end and instrumentation hooks) More... | |
Class interface to library types and functions defined in cprover_contracts.c
.
Definition at line 153 of file dfcc_library.h.
dfcc_libraryt::dfcc_libraryt | ( | goto_modelt & | goto_model, |
message_handlert & | lmessage_handler | ||
) |
Class constructor.
Definition at line 174 of file dfcc_library.cpp.
void dfcc_libraryt::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 instrumented function.
Definition at line 538 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 849 of file dfcc_library.cpp.
void dfcc_libraryt::disable_checks | ( | ) |
Adds "checked" pragmas to instructions of all library functions instructions.
By default checks are not disabled.
Definition at line 227 of file dfcc_library.cpp.
|
protected |
Fixes function calls to malloc and free in library functions.
Change calls to __CPROVER_contracts_malloc
into calls to malloc
Change calls to __CPROVER_contracts_free
into calls to free
Definition at line 464 of file dfcc_library.cpp.
Returns the dfcc_funt that corresponds to the given id if any.
Definition at line 366 of file dfcc_library.cpp.
Returns the name of the given dfcc_funt.
Definition at line 380 of file dfcc_library.cpp.
Returns the library instrumentation hook for the given built-in.
function_id must be one of __CPROVER_assignable
, __CPROVER_object_whole
, __CPROVER_object_from
, __CPROVER_object_upto
Definition at line 207 of file dfcc_library.cpp.
Returns the library instrumentation hook for the given front-end function.
Returns the instrumentation function to use for a given front-end function.
function_id
is a front end built-in as defined by is_front_end_builtin. Definition at line 199 of file dfcc_library.cpp.
const symbolt & dfcc_libraryt::get_instrumented_functions_map_symbol | ( | ) |
Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.
This symbol is an unbounded map of booleans indexed by function pointer ID, meant to have value true for instrumented functions and false for non-instrumented functions. Initialisation instructions for this map are generated by add_instrumented_functions_map_init_instructions
Definition at line 516 of file dfcc_library.cpp.
|
protected |
Collects the names of all library functions currently missing from the goto_model into missing
.
Definition at line 239 of file dfcc_library.cpp.
void dfcc_libraryt::inhibit_front_end_builtins | ( | ) |
Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __CPROVER_object_from __CPROVER_assignable __CPROVER_freeable An error will be triggered in case calls to these functions occur outside of a contrat clause and were hence not mapped to their library implementation.
Definition at line 495 of file dfcc_library.cpp.
|
protected |
Inlines library functions that need to be inlined before use.
Definition at line 407 of file dfcc_library.cpp.
bool dfcc_libraryt::is_dfcc_library_symbol | ( | const irep_idt & | id | ) | const |
True iff the given id is one of the library symbols.
Definition at line 375 of file dfcc_library.cpp.
bool dfcc_libraryt::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
, __CPROVER_object_from
, __CPROVER_object_upto
, __CPROVER_freeable
Returns the instrumentation function to use for a given front-end function.
Definition at line 193 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 824 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 836 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 812 of file dfcc_library.cpp.
void dfcc_libraryt::load | ( | std::set< irep_idt > & | to_instrument | ) |
After calling this function, all library types and functions are present in the the goto_model.
Any other functions that the DFCC functions rely on and need to be instrumented will be added to to_instrument
Definition at line 278 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 863 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::obj_set_release_call | ( | const exprt & | obj_set_ptr, |
const source_locationt & | source_location | ||
) |
Builds call to __CPROVER_contracts_obj_set_release.
Definition at line 875 of file dfcc_library.cpp.
void dfcc_libraryt::specialize | ( | const std::size_t | contract_assigns_size_hint | ) |
Specializes the library by unwinding loops in library functions to the given assigns clause size.
contract_assigns_size_hint | size of the assigns clause being checked |
Definition at line 430 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 619 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 631 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 668 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 711 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 725 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 697 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 682 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 769 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 754 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 785 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 740 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 558 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::write_set_create_call | ( | const exprt & | write_set_ptr, |
const exprt & | contract_assigns_size, | ||
const source_locationt & | source_location | ||
) |
Builds call to __CPROVER_contracts_write_set_create.
Definition at line 590 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 800 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 643 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::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.
Definition at line 655 of file dfcc_library.cpp.
const code_function_callt dfcc_libraryt::write_set_release_call | ( | const exprt & | write_set_ptr, |
const source_locationt & | source_location | ||
) |
Builds call to __CPROVER_contracts_write_set_release.
Definition at line 608 of file dfcc_library.cpp.
|
private |
All built-in function names (front-end and instrumentation hooks)
Definition at line 210 of file dfcc_library.h.
Maps enum values to the actual function symbols (dynamically loaded)
Definition at line 217 of file dfcc_library.h.
enum to function name mapping
Definition at line 198 of file dfcc_library.h.
Maps built-in function names to enums to use for instrumentation.
Definition at line 204 of file dfcc_library.h.
Definition at line 201 of file dfcc_library.h.
|
private |
Swapped dfcc_type_to_name.
Definition at line 195 of file dfcc_library.h.
std::map<dfcc_typet, typet> dfcc_libraryt::dfcc_type |
Maps enum values to the actual types (dynamically loaded)
Definition at line 214 of file dfcc_library.h.
|
private |
Enum to type name mapping.
Definition at line 192 of file dfcc_library.h.
|
protected |
Definition at line 174 of file dfcc_library.h.
Maps front-end functions to library functions giving their havoc semantics.
Definition at line 207 of file dfcc_library.h.
|
staticprotected |
True iff the library functions are inlined.
Definition at line 165 of file dfcc_library.h.
|
staticprotected |
True iff the contracts library symbols are loaded.
Definition at line 162 of file dfcc_library.h.
|
protected |
Definition at line 176 of file dfcc_library.h.
|
staticprotected |
True iff the library functions uses of malloc and free are fixed.
True iff the library functions have already been fixed.
Definition at line 172 of file dfcc_library.h.
|
protected |
Definition at line 175 of file dfcc_library.h.
|
staticprotected |
True iff the library functions are specialized to a particular contract.
Definition at line 169 of file dfcc_library.h.