34 int param_counter = 0;
35 for(
auto ¶meter :
function.type.parameters())
37 if(parameter.get_identifier().empty())
39 const std::string param_base_name =
40 parameter.get_base_name().empty()
44 id2string(function_name) +
"::" + param_base_name;
45 parameter.set_base_name(param_base_name);
46 parameter.set_identifier(new_param_identifier);
48 new_param_sym.
name = new_param_identifier;
49 new_param_sym.
type = parameter.type();
50 new_param_sym.
base_name = param_base_name;
51 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
52 new_param_sym.
mode = function_symbol.mode;
53 new_param_sym.
module = function_symbol.module;
54 new_param_sym.
location = function_symbol.location;
55 symbol_table.
add(new_param_sym);
59 function_symbol.
type =
function.type;
68 const irep_idt &function_name)
const override 70 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
72 auto add_instruction = [&]() {
73 auto instruction =
function.body.add_instruction();
74 instruction->function = function_name;
75 instruction->source_location = function_symbol.location;
78 auto assume_instruction = add_instruction();
80 auto end_instruction = add_instruction();
81 end_instruction->make_end_function();
91 const irep_idt &function_name)
const override 93 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
95 auto add_instruction = [&]() {
96 auto instruction =
function.body.add_instruction();
97 instruction->function = function_name;
98 instruction->source_location = function_symbol.location;
99 instruction->source_location.set_function(function_name);
102 auto assert_instruction = add_instruction();
105 std::ostringstream comment_stream;
106 comment_stream <<
id2string(ID_assertion) <<
" " 107 <<
format(assert_instruction->guard);
108 assert_instruction->source_location.set_comment(comment_stream.str());
109 assert_instruction->source_location.set_property_class(ID_assertion);
110 auto end_instruction = add_instruction();
111 end_instruction->make_end_function();
122 const irep_idt &function_name)
const override 124 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
126 auto add_instruction = [&]() {
127 auto instruction =
function.body.add_instruction();
128 instruction->function = function_name;
129 instruction->source_location = function_symbol.location;
130 instruction->source_location.set_function(function_name);
133 auto assert_instruction = add_instruction();
135 assert_instruction->source_location.set_function(function_name);
137 std::ostringstream comment_stream;
138 comment_stream <<
id2string(ID_assertion) <<
" " 139 <<
format(assert_instruction->guard);
140 assert_instruction->source_location.set_comment(comment_stream.str());
141 assert_instruction->source_location.set_property_class(ID_assertion);
142 auto assume_instruction = add_instruction();
143 assume_instruction->make_assumption(
false_exprt());
144 auto end_instruction = add_instruction();
145 end_instruction->make_end_function();
169 const irep_idt &function_name)
const 174 if(!lhs_type.get_bool(ID_C_constant))
178 if(lhs_type.id() == ID_struct || lhs_type.id() == ID_union)
191 for(
auto const &component : lhs_struct_type.components())
200 else if(lhs_type.id() == ID_array)
203 if(!lhs_array_type.subtype().get_bool(ID_C_constant))
205 bool constant_known_array_size = lhs_array_type.size().is_constant();
206 if(!constant_known_array_size)
209 <<
" in function " << function_name
210 <<
": Unknown array size" <<
eom;
214 auto const array_size =
217 array_size.has_value(),
218 "Array size should be known constant integer");
219 if(array_size.value() == 0)
225 <<
" in function " << function_name <<
": Array size 0" 230 for(
mp_integer i = 0; i < array_size.value(); ++i)
246 auto assign_instruction = add_instruction();
247 assign_instruction->make_assignment(
257 const irep_idt &function_name)
const override 259 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
261 auto add_instruction = [&]() {
262 auto instruction =
function.body.add_instruction();
263 instruction->function = function_name;
264 instruction->source_location = function_symbol.location;
268 for(
auto const ¶meter :
function.type.parameters())
271 parameter.type().id() == ID_pointer &&
276 auto goto_instruction = add_instruction();
279 symbol_exprt(parameter.get_identifier(), parameter.type()),
284 auto label_instruction = add_instruction();
285 goto_instruction->make_goto(
288 symbol_exprt(parameter.get_identifier(), parameter.type()),
290 label_instruction->make_skip();
296 auto const &global_sym = symbol_table.
lookup_ref(global_id);
303 if(
function.type.return_type() !=
void_typet())
305 auto return_instruction = add_instruction();
306 return_instruction->make_return();
307 return_instruction->code =
310 auto end_function_instruction = add_instruction();
311 end_function_instruction->make_end_function();
325 : runtime_error(reason)
334 const std::string &options,
338 if(options.empty() || options ==
"nondet-return")
340 return util_make_unique<havoc_generate_function_bodiest>(
344 if(options ==
"assume-false")
346 return util_make_unique<assume_false_generate_function_bodiest>();
349 if(options ==
"assert-false")
351 return util_make_unique<assert_false_generate_function_bodiest>();
354 if(options ==
"assert-false-assume-false")
360 const std::vector<std::string> option_components =
split_string(options,
',');
361 if(!option_components.empty() && option_components[0] ==
"havoc")
363 std::regex globals_regex;
364 std::regex params_regex;
365 for(std::size_t i = 1; i < option_components.size(); ++i)
367 const std::vector<std::string> key_value_pair =
369 if(key_value_pair.size() != 2)
372 "Expected key_value_pair of form argument:value");
374 if(key_value_pair[0] ==
"globals")
376 globals_regex = key_value_pair[1];
378 else if(key_value_pair[0] ==
"params")
380 params_regex = key_value_pair[1];
385 "Unknown option \"" + key_value_pair[0] +
"\"");
388 std::vector<irep_idt> globals_to_havoc;
391 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
392 for(
auto const &symbol : symbol_table.
symbols)
395 symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
396 std::regex_match(
id2string(symbol.first), globals_regex))
398 if(std::regex_match(
id2string(symbol.first), cprover_prefix))
400 messages.
warning() <<
"generate function bodies: " 401 <<
"matched global '" <<
id2string(symbol.first)
402 <<
"' begins with __CPROVER, " 403 <<
"havoc-ing this global may interfere" 406 globals_to_havoc.push_back(symbol.first);
409 return util_make_unique<havoc_generate_function_bodiest>(
410 std::move(globals_to_havoc), std::move(params_regex),
message_handler);
453 const std::regex &functions_regex,
459 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
460 bool did_generate_body =
false;
464 !
function.second.body_available() &&
465 std::regex_match(
id2string(
function.first), functions_regex))
467 if(std::regex_match(
id2string(
function.first), cprover_prefix))
469 messages.
warning() <<
"generate function bodies: matched function '" 471 <<
"' begins with __CPROVER " 472 <<
"the generated body for this function " 475 did_generate_body =
true;
480 if(!did_generate_body)
483 <<
"generate function bodies: No function name matched regex"
irep_idt name
The unique identifier.
virtual void generate_function_body_impl(goto_functiont &function, const 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...
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, message_handlert &message_handler)
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
irep_idt mode
Language mode.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
The null pointer constant.
irep_idt module
Name of module the symbol belongs to.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
static mstreamt & eom(mstreamt &m)
#define INVARIANT(CONDITION, REASON)
Base class for replace_function_body implementations.
Extract member of struct or union.
mstreamt & warning() const
std::regex parameters_to_havoc
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
instructionst::iterator targett
Operator to dereference a pointer.
#define PRECONDITION(CONDITION)
A side effect that returns a non-deterministically chosen value.
const typet & follow(const typet &) const
void generate_function_body_impl(goto_functiont &function, const 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...
The boolean constant false.
void generate_function_body_impl(goto_functiont &function, const 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 std::vector< irep_idt > globals_to_havoc
void havoc_expr_rec(const exprt &lhs, const namespacet &ns, const std::function< goto_programt::targett(void)> &add_instruction, const irep_idt &function_name) const
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
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 A list of currently accepted command line argumen...
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter...
void generate_function_body_impl(goto_functiont &function, const 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(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...
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
std::unique_ptr< T > util_make_unique(Ts &&... ts)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
generate_function_bodies_errort(const std::string &reason)
goto_programt coverage_criteriont message_handlert & message_handler
const typet & subtype() const
message_handlert * message_handler
goto_functionst goto_functions
GOTO functions.
void generate_function_body_impl(goto_functiont &function, const 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...