43 int param_counter = 0;
44 for(
auto ¶meter : parameters)
46 if(parameter.get_identifier().empty())
48 const std::string param_base_name =
49 parameter.get_base_name().empty()
50 ?
"__param$" + std::to_string(param_counter++)
53 id2string(function_name) +
"::" + param_base_name;
54 parameter.set_base_name(param_base_name);
55 parameter.set_identifier(new_param_identifier);
57 new_param_sym.
name = new_param_identifier;
58 new_param_sym.
type = parameter.type();
59 new_param_sym.
base_name = param_base_name;
60 new_param_sym.
mode = function_symbol.mode;
61 new_param_sym.
module = function_symbol.module;
62 new_param_sym.
location = function_symbol.location;
63 symbol_table.
add(new_param_sym);
75 const irep_idt &function_name)
const override
77 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
92 const irep_idt &function_name)
const override
94 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
98 annotated_location.
set_comment(
"undefined function should be unreachable");
116 const irep_idt &function_name)
const override
118 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
122 annotated_location.
set_comment(
"undefined function should be unreachable");
166 const std::size_t initial_depth,
191 init_code.
append(assignments);
201 const std::string ¶m_name,
202 std::size_t param_number)
const
211 return std::binary_search(
222 const irep_idt &function_name)
const override
228 auto max_param_number = std::max_element(
233 "function " +
id2string(function_name) +
" does not take " +
234 std::to_string(*max_param_number + 1) +
" arguments",
235 "--generate-havocing-body"};
241 if(parameter_symbol.
type.
id() != ID_pointer)
244 "argument number " + std::to_string(number) +
" of function " +
245 id2string(function_name) +
" is not a pointer",
246 "--generate-havocing-body"};
251 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
260 parameter_symbol.
type.
id() == ID_pointer &&
266 auto goto_instruction =
288 auto label_instruction =
290 goto_instruction->complete_goto(label_instruction);
296 auto const &global_sym = symbol_table.
lookup_ref(global_id);
314 typet type(return_type);
315 type.
remove(ID_C_constant);
369 : runtime_error(reason)
377 const std::string &options,
382 if(options.empty() || options ==
"nondet-return")
385 std::vector<irep_idt>{},
387 object_factory_parameters,
391 if(options ==
"assume-false")
396 if(options ==
"assert-false")
401 if(options ==
"assert-false-assume-false")
407 const std::vector<std::string> option_components =
split_string(options,
',');
408 if(!option_components.empty() && option_components[0] ==
"havoc")
410 std::regex globals_regex;
411 std::regex params_regex;
412 std::vector<std::size_t> param_numbers;
413 for(std::size_t i = 1; i < option_components.size(); ++i)
415 const std::vector<std::string> key_value_pair =
417 if(key_value_pair.size() != 2)
420 "Expected key_value_pair of form argument:value");
422 if(key_value_pair[0] ==
"globals")
424 globals_regex = key_value_pair[1];
426 else if(key_value_pair[0] ==
"params")
428 auto param_identifiers =
split_string(key_value_pair[1],
';');
429 if(param_identifiers.size() == 1)
431 auto maybe_nondet_param_number =
433 if(!maybe_nondet_param_number.has_value())
435 params_regex = key_value_pair[1];
440 param_identifiers.begin(),
441 param_identifiers.end(),
442 std::back_inserter(param_numbers),
443 [](
const std::string ¶m_id) {
444 auto maybe_nondet_param_number = string2optional_size_t(param_id);
446 maybe_nondet_param_number.has_value(),
447 param_id +
" not a number");
448 return *maybe_nondet_param_number;
450 std::sort(param_numbers.begin(), param_numbers.end());
455 "Unknown option \"" + key_value_pair[0] +
"\"");
458 std::vector<irep_idt> globals_to_havoc;
461 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
462 for(
auto const &symbol : symbol_table.
symbols)
465 symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
466 std::regex_match(
id2string(symbol.first), globals_regex))
468 if(std::regex_match(
id2string(symbol.first), cprover_prefix))
470 messages.
warning() <<
"generate function bodies: "
471 <<
"matched global '" <<
id2string(symbol.first)
472 <<
"' begins with __CPROVER, "
473 <<
"havoc-ing this global may interfere"
476 globals_to_havoc.push_back(symbol.first);
479 if(param_numbers.empty())
481 std::move(globals_to_havoc),
482 std::move(params_regex),
483 object_factory_parameters,
487 std::move(globals_to_havoc),
488 std::move(param_numbers),
489 object_factory_parameters,
503 const std::regex &functions_regex,
509 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
510 bool did_generate_body =
false;
514 !function.second.body_available() &&
515 std::regex_match(
id2string(function.first), functions_regex))
517 if(std::regex_match(
id2string(function.first), cprover_prefix))
519 messages.
warning() <<
"generate function bodies: matched function '"
521 <<
"' begins with __CPROVER "
522 <<
"the generated body for this function "
525 did_generate_body =
true;
530 if(!did_generate_body)
533 <<
"generate function bodies: No function name matched regex"
539 const std::string &function_name,
540 const std::string &call_site_id,
558 auto const symbol = symbol_pair.second;
559 if(symbol.type.id() == ID_code && symbol.name == function_name)
561 function_mode = symbol.mode;
562 function_type = symbol.type;
570 symbolt havoc_function_symbol{};
571 havoc_function_symbol.
name = havoc_function_symbol.base_name =
572 havoc_function_symbol.pretty_name = function_name +
"." + call_site_id;
574 havoc_function_symbol.is_lvalue =
true;
575 havoc_function_symbol.mode = function_mode;
576 havoc_function_symbol.type = function_type;
580 auto const &generated_havoc =
590 !function.second.body_available() &&
591 havoc_function_symbol.name ==
id2string(function.first))
598 auto is_havoc_function_call = [&function_name](
const exprt &expr) {
599 if(expr.id() != ID_symbol)
601 std::string called_function_name =
603 if(called_function_name == function_name)
606 return (
has_prefix(called_function_name, function_name +
"."));
610 std::size_t counter = 0;
613 for(
auto &instruction : function.second.body.instructions)
615 if(instruction.is_function_call())
617 auto &called_function = instruction.call_function();
618 if(is_havoc_function_call(called_function))
620 if(++counter == *call_site_number)
622 called_function = generated_havoc.symbol_expr();
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
A codet representing sequential composition of program statements.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
const parameterst & parameters() const
const typet & return_type() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
The Boolean constant false.
generate_function_bodies_errort(const std::string &reason)
Base class for replace_function_body implementations.
void generate_function_body(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Replace the function body with one based on the replace_function_body class being used.
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
virtual void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const =0
Produce a body for the passed function At this point the body of function is always empty,...
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
bool body_available() const
void set_parameter_identifiers(const code_typet &code_type)
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
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_skip(const source_locationt &l=source_locationt::nil())
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())
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::vector< std::size_t > param_numbers_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
const std::vector< irep_idt > globals_to_havoc
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
bool should_havoc_param(const std::string ¶m_name, std::size_t param_number) const
optionalt< std::vector< std::size_t > > param_numbers_to_havoc
optionalt< std::regex > parameters_to_havoc
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
const c_object_factory_parameterst & object_factory_parameters
void havoc_expr_rec(const exprt &lhs, const std::size_t initial_depth, const source_locationt &source_location, const irep_idt &function_id, symbol_tablet &symbol_table, goto_programt &dest) const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool get_bool(const irep_idt &name) const
void remove(const irep_idt &name)
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
message_handlert & get_message_handler()
mstreamt & warning() const
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().
The null pointer constant.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
const typet & base_type() const
The type of the data what we point to.
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)
void gen_nondet_init(code_blockt &assignments, const exprt &expr, const std::size_t depth=0, recursion_sett recursion_set=recursion_sett(), const bool assign_const=true)
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
std::set< irep_idt > recursion_sett
void declare_created_symbols(code_blockt &init_code)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
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.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
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.
const std::string & id2string(const irep_idt &d)
std::unique_ptr< T > util_make_unique(Ts &&... ts)
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
optionalt< std::size_t > string2optional_size_t(const std::string &str, int base)
Convert string to size_t similar to the stoul or stoull functions, return nullopt when the conversion...
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)