32 std::string correct_format)
34 correct_format(
std::move(correct_format))
42 res +=
"Invalid function-contract mapping";
53static std::pair<irep_idt, irep_idt>
57 "the format for function and contract pairs is "
58 "`<function_name>[/<contract_name>]`";
68 else if(
split.size() == 2)
70 auto function_name =
split[0];
71 if(function_name.empty())
74 "couldn't find function name before '/' in '" +
cli_flag_str +
"'",
81 "couldn't find contract name after '/' in '" +
cli_flag_str +
"'",
97 const std::optional<irep_idt> &to_check,
98 const bool allow_recursive_calls,
99 const std::set<irep_idt> &to_replace,
101 const std::set<std::string> &to_exclude_from_nondet_static,
105 for(
const auto &
cli_flag : to_replace)
113 : std::optional<std::pair<irep_idt, irep_idt>>{},
114 allow_recursive_calls,
116 loop_contract_config,
118 to_exclude_from_nondet_static);
125 const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
126 const bool allow_recursive_calls,
127 const std::map<irep_idt, irep_idt> &to_replace,
130 const std::set<std::string> &to_exclude_from_nondet_static)
132 goto_model(goto_model),
133 harness_id(harness_id),
135 allow_recursive_calls(allow_recursive_calls),
136 to_replace(to_replace),
137 loop_contract_config(loop_contract_config),
138 to_exclude_from_nondet_static(to_exclude_from_nondet_static),
139 message_handler(message_handler),
140 log(message_handler),
141 library(goto_model, message_handler),
142 ns(goto_model.symbol_table),
143 spec_functions(goto_model, message_handler, library),
144 contract_clauses_codegen(goto_model, message_handler, library),
150 contract_clauses_codegen),
151 memory_predicates(goto_model, library, instrument, message_handler),
159 contract_clauses_codegen),
167 max_assigns_clause_size(0)
178 "' either not found or has no body");
186 "' either not found or has no body");
194 "' cannot be both be checked against a contract and be the harness");
199 "' cannot be both the contract to check and be the harness");
204 "' cannot be both checked against contract and replaced by a contract");
209 "' cannot be checked against a contract");
218 "Function to replace '" +
id2string(
pair.first) +
"' not found");
226 "' cannot both be replaced with a contract and be the harness");
231 "' cannot both be the contract to use for replacement and be the "
238 std::set<irep_idt> &other_symbols)
249 const symbolt &symbol = entry.second;
388 "' used as contract for function pointer cannot be itself the object "
389 "of a contract check.");
398 "' used as contract for function pointer already the object of a "
399 "contract replacement with '" +
402 <<
"' already wrapped with itself in REPLACE mode"
410 "Function pointer contract '" + str +
"' not found.");
468 log.
status() <<
"Specializing cprover_contracts functions for assigns "
469 "clauses of at most "
492 "assert-false-assume-false",
523 auto begin = body.instructions.begin();
527 body.destructive_insert(begin,
payload);
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
bool generate_ansi_c_start_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Generate a _start function for a specific function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
struct configt::ansi_ct ansi_c
Base class for exceptions thrown in the cprover project.
std::string reason
The reason this exception was generated.
const symbolt & get_pure_contract_symbol(const irep_idt &contract_id, const std::optional< irep_idt > function_id_opt={})
Searches for a symbol named "contract::contract_id" in the symbol table.
const std::size_t get_assigns_clause_size(const irep_idt &contract_id)
Returns the size assigns clause of the given contract in number of targets.
void instrument_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
void get_instrumented_functions(std::set< irep_idt > &dest) const
Adds the names of instrumented functions to dest.
std::size_t get_max_assigns_clause_size() const
bool do_not_instrument(const irep_idt &id) const
True iff the symbol must not be instrumented because it is an internal symbol or a CPROVER symbol.
void instrument_harness_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
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...
void inhibit_front_end_builtins()
Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __...
void disable_checks()
Adds "checked" pragmas to instructions of all library functions instructions.
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.
void load(std::set< irep_idt > &to_instrument)
After calling this function, all library types and functions are present in the the goto_model.
std::set< irep_idt > lift_predicates(std::set< irep_idt > &discovered_function_pointer_contracts)
Collects and lifts all user-defined memory predicates.
void swap_and_wrap_check(const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
void swap_and_wrap_replace(const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts)
void get_swapped_functions(std::set< irep_idt > &dest) const
Adds the set of swapped functions to dest.
Entry point into the contracts transformation.
std::set< irep_idt > function_pointer_contracts
std::set< irep_idt > pure_contract_symbols
void instrument_harness_function()
void instrument_other_functions()
const loop_contract_configt loop_contract_config
void reinitialize_model()
Re-initialise the GOTO model.
const std::set< std::string > & to_exclude_from_nondet_static
void link_model_and_load_dfcc_library()
dfcct(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< std::pair< irep_idt, irep_idt > > &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const loop_contract_configt loop_contract_config, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static)
Class constructor.
dfcc_swap_and_wrapt swap_and_wrap
dfcc_lift_memory_predicatest memory_predicates
void wrap_checked_function()
void lift_memory_predicates()
const std::optional< std::pair< irep_idt, irep_idt > > & to_check
void check_transform_goto_model_preconditions()
Checks preconditions on arguments of transform_goto_model.
std::size_t max_assigns_clause_size
Tracks the maximum number of targets in any assigns clause handled in the transformation (used to spe...
void transform_goto_model()
Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame co...
dfcc_instrumentt instrument
void wrap_replaced_functions()
message_handlert & message_handler
const irep_idt & harness_id
const bool allow_recursive_calls
std::set< irep_idt > other_symbols
dfcc_contract_handlert contract_handler
const std::map< irep_idt, irep_idt > & to_replace
void partition_function_symbols(std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols)
Partitions the function symbols of the symbol table into pure contracts and other function symbols sy...
void wrap_discovered_function_pointer_contracts()
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
Exception thrown for bad function/contract specification pairs passed on the CLI.
invalid_function_contract_pair_exceptiont(std::string reason, std::string correct_format="")
std::string what() const override
A human readable description of what went wrong.
std::string correct_format
const irep_idt & id() const
message_handlert & get_message_handler()
mstreamt & status() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
typet type
Type of symbol.
irep_idt name
The unique identifier.
bool has_prefix(const std::string &s, const std::string &prefix)
static std::pair< irep_idt, irep_idt > parse_function_contract_pair(const irep_idt &cli_flag)
Main class orchestrating the the whole program transformation for function contracts with Dynamic Fra...
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
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, bool ignore_no_match)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
void dfcc(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const loop_contract_configt loop_contract_config, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
Applies function contracts transformation to GOTO model, using the dynamic frame condition checking a...
const std::string & id2string(const irep_idt &d)
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
void find_used_functions(const irep_idt &start, goto_functionst &functions, std::set< irep_idt > &seen)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
Loop contract configurations.