92 std::unordered_set<irep_idt>
100 p_impl->message_handler = &message_handler;
106 const std::string &option,
107 const std::list<std::string> &values)
112 if(
p_impl->recursive_initialization_config.handle_option(option, values))
122 p_impl->nondet_globals =
true;
126 p_impl->function_parameters_to_treat_as_arrays.insert(
127 values.begin(), values.end());
131 for(
auto const &value : values)
133 for(
auto const ¶m_cluster :
split_string(value,
';'))
135 std::set<irep_idt> equal_param_set;
136 for(
auto const ¶m_id :
split_string(param_cluster,
','))
138 equal_param_set.insert(param_id);
140 p_impl->function_parameters_to_treat_equal.push_back(
141 std::move(equal_param_set));
147 for(
auto const &array_size_pair : values)
157 p_impl->function_parameters_to_treat_as_arrays.insert(array);
158 auto const inserted =
159 p_impl->function_parameter_to_associated_array_size.emplace(
164 "can not have two associated array sizes for one array",
171 "'" + array_size_pair +
172 "' is in an invalid format for array size pair",
174 "array_name:size_name, where both are the names of function "
181 p_impl->function_parameters_to_treat_as_cstrings.insert(
182 values.begin(), values.end());
186 p_impl->recursive_initialization_config.arguments_may_be_equal =
true;
194 p_impl->recursive_initialization_config
195 .potential_null_function_pointers,
196 p_impl->recursive_initialization_config.potential_null_function_pointers
198 [](
const std::string &
opt) ->
irep_idt { return irep_idt{opt}; });
206 p_impl->recursive_initialization_config
207 .potential_null_function_pointers,
208 p_impl->recursive_initialization_config.potential_null_function_pointers
210 [](
const std::string &
opt) ->
irep_idt { return irep_idt{opt}; });
215 "function harness generator cannot handle this option",
"--" + option};
221 const irep_idt &harness_function_name)
223 p_impl->generate(goto_model, harness_function_name);
228 const irep_idt &harness_function_name)
281 auto globals = std::vector<symbol_exprt>{};
282 for(
const auto &symbol_table_entry : *symbol_table)
284 const auto &symbol = symbol_table_entry.second;
287 globals.push_back(symbol.symbol_expr());
290 for(
auto const &global : globals)
292 generate_initialisation_code_for(function_body, global);
301 recursive_initialization->initialize(
303 if(recursive_initialization->needs_freeing(lhs))
310 if(
p_impl->function == ID_empty_string)
312 "required parameter entry function not set",
315 p_impl->recursive_initialization_config.min_dynamic_array_size >
316 p_impl->recursive_initialization_config.max_dynamic_array_size)
319 "min dynamic array size cannot be greater than max dynamic array size",
324 const auto function_to_call_pointer =
326 if(function_to_call_pointer ==
nullptr)
330 "' does not exist in the symbol table",
335 for(
auto const &equal_cluster :
p_impl->function_parameters_to_treat_equal)
337 for(
auto const &pointer_id : equal_cluster)
339 std::string decorated_pointer_id =
341 bool is_a_param =
false;
343 for(
auto const &formal_param : ftype.parameters())
345 if(formal_param.get_identifier() == decorated_pointer_id)
348 if(formal_param.type().id() != ID_pointer)
351 id2string(pointer_id) +
" is not a pointer parameter",
354 if(common_type.
id() != ID_empty)
356 if(common_type != formal_param.type())
359 "pointer arguments of conflicting type",
364 common_type = formal_param.type();
370 id2string(pointer_id) +
" is not a parameter",
380 for(
const auto &nullable :
381 p_impl->recursive_initialization_config.potential_null_function_pointers)
383 const auto &function_pointer_symbol_pointer =
386 if(function_pointer_symbol_pointer ==
nullptr)
389 "nullable function pointer `" +
id2string(nullable) +
390 "' not found in symbol table",
394 const auto &function_pointer_type = function_pointer_symbol_pointer->type;
399 "`" +
id2string(nullable) +
"' is not a pointer",
407 "`" +
id2string(nullable) +
"' is not pointing to a function",
416 auto function_found = symbol_table->lookup(
function);
418 if(function_found ==
nullptr)
421 "function that should be harnessed is not found " +
id2string(
function),
425 return *function_found;
431 if(symbol_table->lookup(harness_function_name))
434 "harness function already exists in the symbol table",
445 symbolt harness_function_symbol{};
446 harness_function_symbol.
name = harness_function_symbol.base_name =
447 harness_function_symbol.pretty_name = harness_function_name;
449 harness_function_symbol.is_lvalue =
true;
452 harness_function_symbol.value = std::move(function_body);
454 symbol_table->insert(harness_function_symbol);
456 goto_convert(*symbol_table, *goto_functions, *message_handler);
465 const auto ¶meters = function_type.parameters();
473 std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
474 for(
const auto ¶meter : parameters)
476 auto argument = allocate_objects.allocate_automatic_local_object(
477 remove_const(parameter.type()), parameter.get_base_name());
478 parameter_name_to_argument_name.insert(
479 {parameter.get_base_name(), argument.get_identifier()});
480 arguments.push_back(argument);
483 for(
const auto &pair : parameter_name_to_argument_name)
485 auto const ¶meter_name = pair.first;
486 auto const &argument_name = pair.second;
487 if(function_parameters_to_treat_as_arrays.count(parameter_name) != 0)
489 function_arguments_to_treat_as_arrays.insert(argument_name);
492 if(function_parameters_to_treat_as_cstrings.count(parameter_name) != 0)
494 function_arguments_to_treat_as_cstrings.insert(argument_name);
497 auto it = function_parameter_to_associated_array_size.
find(parameter_name);
498 if(it != function_parameter_to_associated_array_size.end())
500 auto const &associated_array_size_parameter = it->second;
501 auto associated_array_size_argument =
502 parameter_name_to_argument_name.
find(associated_array_size_parameter);
504 associated_array_size_argument == parameter_name_to_argument_name.end())
507 "could not find parameter to associate the array size of array \"" +
508 id2string(parameter_name) +
"\" (Expected parameter: \"" +
509 id2string(associated_array_size_parameter) +
"\" on function \"" +
514 function_argument_to_associated_array_size.insert(
515 {argument_name, associated_array_size_argument->second});
520 for(
auto const &equal_cluster : function_parameters_to_treat_equal)
522 std::set<irep_idt> cluster_argument_names;
523 for(
auto const ¶meter_name : equal_cluster)
526 parameter_name_to_argument_name.count(parameter_name) != 0,
527 id2string(parameter_name) +
" is not a parameter");
528 cluster_argument_names.insert(
529 parameter_name_to_argument_name[parameter_name]);
531 function_arguments_to_treat_equal.push_back(
532 std::move(cluster_argument_names));
535 allocate_objects.declare_created_symbols(function_body);
544 for(
auto const &argument : arguments)
546 generate_initialisation_code_for(function_body, argument);
547 if(recursive_initialization->needs_freeing(argument))
551 std::move(arguments)};
554 function_body.
add(std::move(function_call));
560 std::unordered_set<irep_idt> nullables;
561 for(
const auto &nullable :
562 recursive_initialization_config.potential_null_function_pointers)
564 const auto &nullable_name =
id2string(nullable);
565 const auto &function_prefix =
id2string(
function) +
"::";
566 if(
has_prefix(nullable_name, function_prefix))
569 "__goto_harness::" + nullable_name.substr(function_prefix.size()));
573 nullables.insert(nullable_name);
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
signedbv_typet signed_int_type()
A codet representing sequential composition of program statements.
void add(const codet &code)
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
void validate_options(const goto_modelt &goto_model) override
Check if options are in a sane state, throw otherwise.
~function_call_harness_generatort() override
std::unique_ptr< implt > p_impl
function_call_harness_generatort(ui_message_handlert &message_handler)
void handle_option(const std::string &option, const std::list< std::string > &values) override
Handle a command line argument.
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
Generate a harness according to the set options.
A collection of goto functions.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irept & find(const irep_idt &name) const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static bool is_initialization_allowed(const symbolt &symbol)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
irep_idt name
The unique identifier.
The type of an expression, extends irept.
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
bool has_prefix(const std::string &s, const std::string &prefix)
code_function_callt function_to_call(symbol_table_baset &symbol_table, const irep_idt &id, const irep_idt &argument)
#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT
#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT
#define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING
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.
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
const std::string & id2string(const irep_idt &d)
std::string require_exactly_one_value(const std::string &option, const std::list< std::string > &values)
Returns the only value of a single element list, throws an exception if not passed a single element l...
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
This contains implementation details of function call harness generator to avoid leaking them out int...
std::set< irep_idt > function_parameters_to_treat_as_arrays
symbol_tablet * symbol_table
goto_functionst * goto_functions
std::set< symbol_exprt > global_pointers
std::set< irep_idt > function_arguments_to_treat_as_arrays
irep_idt harness_function_name
std::map< irep_idt, irep_idt > function_parameter_to_associated_array_size
void call_function(const code_function_callt::argumentst &arguments, code_blockt &function_body)
Write initialisation code for each of the arguments into function_body, then insert a call to the ent...
std::map< irep_idt, irep_idt > function_argument_to_associated_array_size
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
std::vector< std::set< irep_idt > > function_arguments_to_treat_equal
const symbolt & lookup_function_to_call()
Return a reference to the entry function or throw if it doesn't exist.
code_function_callt::argumentst declare_arguments(code_blockt &function_body)
Declare local variables for each of the parameters of the entry function and return them.
void add_harness_function_to_goto_model(code_blockt function_body)
Update the goto-model with the new harness function.
std::unique_ptr< recursive_initializationt > recursive_initialization
void generate_nondet_globals(code_blockt &function_body)
Iterate over the symbol table and generate initialisation code for globals into the function body.
ui_message_handlert * message_handler
recursive_initialization_configt recursive_initialization_config
void generate_initialisation_code_for(code_blockt &block, const exprt &lhs)
Generate initialisation code for one lvalue inside block.
std::set< irep_idt > function_parameters_to_treat_as_cstrings
std::vector< std::set< irep_idt > > function_parameters_to_treat_equal
std::set< irep_idt > function_arguments_to_treat_as_cstrings
std::unordered_set< irep_idt > map_function_parameters_to_function_argument_names()
For function parameters that are pointers to functions we want to be able to specify whether or not t...
void ensure_harness_does_not_already_exist()
Throw if the harness function already exists in the symbol table.
std::set< irep_idt > pointers_to_treat_as_cstrings
std::vector< std::set< irep_idt > > pointers_to_treat_equal
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
std::set< irep_idt > variables_that_hold_array_sizes
std::set< irep_idt > pointers_to_treat_as_arrays
std::unordered_set< irep_idt > potential_null_function_pointers
typet remove_const(typet type)
Remove const qualifier from type (if any).