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 =
215 numeric_cast<mp_integer>(lhs_array_type.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(
258 const irep_idt &function_name)
const override 260 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
262 auto add_instruction = [&]() {
263 auto instruction =
function.body.add_instruction();
264 instruction->function = function_name;
265 instruction->source_location = function_symbol.location;
269 for(
auto const ¶meter :
function.type.parameters())
272 parameter.type().id() == ID_pointer &&
277 auto goto_instruction = add_instruction();
280 symbol_exprt(parameter.get_identifier(), parameter.type()),
285 auto label_instruction = add_instruction();
286 goto_instruction->make_goto(
289 symbol_exprt(parameter.get_identifier(), parameter.type()),
291 label_instruction->make_skip();
297 auto const &global_sym = symbol_table.
lookup_ref(global_id);
304 if(
function.type.return_type() !=
void_typet())
306 auto return_instruction = add_instruction();
307 return_instruction->make_return();
310 function.type.return_type(), function_symbol.location));
312 auto end_function_instruction = add_instruction();
313 end_function_instruction->make_end_function();
327 : runtime_error(reason)
336 const std::string &options,
340 if(options.empty() || options ==
"nondet-return")
342 return util_make_unique<havoc_generate_function_bodiest>(
343 std::vector<irep_idt>{}, std::regex{}, message_handler);
346 if(options ==
"assume-false")
348 return util_make_unique<assume_false_generate_function_bodiest>();
351 if(options ==
"assert-false")
353 return util_make_unique<assert_false_generate_function_bodiest>();
356 if(options ==
"assert-false-assume-false")
362 const std::vector<std::string> option_components =
split_string(options,
',');
363 if(!option_components.empty() && option_components[0] ==
"havoc")
365 std::regex globals_regex;
366 std::regex params_regex;
367 for(std::size_t i = 1; i < option_components.size(); ++i)
369 const std::vector<std::string> key_value_pair =
371 if(key_value_pair.size() != 2)
374 "Expected key_value_pair of form argument:value");
376 if(key_value_pair[0] ==
"globals")
378 globals_regex = key_value_pair[1];
380 else if(key_value_pair[0] ==
"params")
382 params_regex = key_value_pair[1];
387 "Unknown option \"" + key_value_pair[0] +
"\"");
390 std::vector<irep_idt> globals_to_havoc;
393 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
394 for(
auto const &symbol : symbol_table.
symbols)
397 symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
398 std::regex_match(
id2string(symbol.first), globals_regex))
400 if(std::regex_match(
id2string(symbol.first), cprover_prefix))
402 messages.
warning() <<
"generate function bodies: " 403 <<
"matched global '" <<
id2string(symbol.first)
404 <<
"' begins with __CPROVER, " 405 <<
"havoc-ing this global may interfere" 408 globals_to_havoc.push_back(symbol.first);
411 return util_make_unique<havoc_generate_function_bodiest>(
412 std::move(globals_to_havoc), std::move(params_regex), message_handler);
455 const std::regex &functions_regex,
461 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
462 bool did_generate_body =
false;
466 !
function.second.body_available() &&
467 std::regex_match(
id2string(
function.first), functions_regex))
469 if(std::regex_match(
id2string(
function.first), cprover_prefix))
471 messages.
warning() <<
"generate function bodies: matched function '" 473 <<
"' begins with __CPROVER " 474 <<
"the generated body for this function " 477 did_generate_body =
true;
482 if(!did_generate_body)
485 <<
"generate function bodies: No function name matched regex" The void type, the same as empty_typet.
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.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
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
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
A side_effect_exprt that returns a non-deterministically chosen value.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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,...
A goto function, consisting of function type (see type), function body (see body),...
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 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 typet to a struct_union_typet.
const source_locationt & source_location() const
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 typet to a pointer_typet.
generate_function_bodies_errort(const std::string &reason)
codet representation of a "return from a function" statement.
const typet & subtype() const
message_handlert * message_handler
goto_functionst goto_functions
GOTO functions.
A codet representing an assignment in the program.
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,...