62 res +=
"Invalid function-contract mapping";
63 res +=
"\nReason: " +
reason;
73static std::pair<irep_idt, irep_idt>
76 auto const correct_format_message =
77 "the format for function and contract pairs is "
78 "`<function_name>[/<contract_name>]`";
80 std::string cli_flag_str =
id2string(cli_flag);
82 auto split =
split_string(cli_flag_str,
'/',
true,
false);
86 return std::make_pair(cli_flag, cli_flag);
88 else if(split.size() == 2)
90 auto function_name = split[0];
91 if(function_name.empty())
94 "couldn't find function name before '/' in '" + cli_flag_str +
"'",
95 correct_format_message};
97 auto contract_name = split[1];
98 if(contract_name.empty())
101 "couldn't find contract name after '/' in '" + cli_flag_str +
"'",
102 correct_format_message};
104 return std::make_pair(function_name, contract_name);
109 "couldn't parse '" + cli_flag_str +
"'", correct_format_message};
117 const std::optional<irep_idt> &to_check,
118 const bool allow_recursive_calls,
119 const std::set<irep_idt> &to_replace,
121 const std::set<std::string> &to_exclude_from_nondet_static,
124 std::map<irep_idt, irep_idt> to_replace_map;
125 for(
const auto &cli_flag : to_replace)
133 : std::optional<std::pair<irep_idt, irep_idt>>{},
134 allow_recursive_calls,
136 loop_contract_config,
138 to_exclude_from_nondet_static);
145 const std::optional<std::pair<irep_idt, irep_idt>> &
to_check,
147 const std::map<irep_idt, irep_idt> &
to_replace,
198 "' either not found or has no body");
205 "Function to check '" +
id2string(pair.first) +
206 "' either not found or has no body");
214 "' cannot be both be checked against a contract and be the harness");
219 "' cannot be both the contract to check and be the harness");
224 "' cannot be both checked against contract and replaced by a contract");
228 "CPROVER function or builtin '" +
id2string(pair.first) +
229 "' cannot be checked against a contract");
238 "Function to replace '" +
id2string(pair.first) +
"' not found");
246 "' cannot both be replaced with a contract and be the harness");
251 "' cannot both be the contract to use for replacement and be the "
257 std::set<irep_idt> &contract_symbols,
263 const symbolt &symbol = entry.second;
273 contract_symbols.insert(sym_name);
286 log.status() <<
"Loading CPROVER C library (" <<
config.ansi_c.arch <<
")"
309 log.status() <<
"Instrumenting harness function '" <<
harness_id <<
"'"
320 std::set<irep_idt> predicates =
322 for(
const auto &predicate : predicates)
335 const auto &pair =
to_check.value();
336 const auto &wrapper_id = pair.first;
337 const auto &contract_id = pair.second;
338 log.status() <<
"Wrapping '" << wrapper_id <<
"' with contract '"
352 const std::size_t assigns_clause_size =
364 const auto &wrapper_id = pair.first;
365 const auto &contract_id = pair.second;
366 log.status() <<
"Wrapping '" << wrapper_id <<
"' with contract '"
378 std::set<irep_idt> swapped;
381 std::set<irep_idt> new_contracts;
385 if(swapped.find(fp_contract) != swapped.end())
402 "' used as contract for function pointer cannot be itself the object "
403 "of a contract check.");
410 found->first == found->second,
412 "' used as contract for function pointer already the object of a "
413 "contract replacement with '" +
415 log.status() <<
"Function pointer contract '" << fp_contract
416 <<
"' already wrapped with itself in REPLACE mode"
424 "Function pointer contract '" + str +
"' not found.");
429 log.status() <<
"Wrapping function pointer contract '" << fp_contract
433 fp_contract, fp_contract, new_contracts);
434 swapped.insert(fp_contract);
478 auto assigns_clause_size =
instrument.get_max_assigns_clause_size();
482 log.status() <<
"Specializing cprover_contracts functions for assigns "
483 "clauses of at most "
487 library.inhibit_front_end_builtins();
524 std::set<irep_idt> instrumented_functions;
525 instrument.get_instrumented_functions(instrumented_functions);
536 auto &body = init_function.body;
537 auto begin = body.instructions.begin();
539 library.add_instrumented_functions_map_init_instructions(
540 instrumented_functions, begin->source_location(), payload);
541 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.
API to expression classes that are internal to the C frontend.
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
cprover_exception_baset(std::string reason)
This constructor is marked protected to ensure this class isn't used directly.
std::string reason
The reason this exception was generated.
Entry point into the contracts transformation.
std::set< irep_idt > function_pointer_contracts
std::set< irep_idt > pure_contract_symbols
dfcc_spec_functionst spec_functions
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
dfcc_contract_clauses_codegent contract_clauses_codegen
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()
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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
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,...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
Goto Programs with Functions.
Goto Programs with Functions.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
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...
Initialize a Goto Program.
const std::string & id2string(const irep_idt &d)
Abstract interface to support a programming language.
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.
API to expression classes for 'mathematical' expressions.
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...
API to expression classes for Pointers.
Various predicates over pointers in programs.
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)
#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
API to expression classes.
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.