Go to the documentation of this file.
28 const std::string &option,
29 const std::list<std::string> &values)
35 auto const user_min_null_tree_depth =
36 string2optional<std::size_t>(value, 10);
37 if(user_min_null_tree_depth.has_value())
44 "failed to convert '" + value +
"' to integer",
53 auto const user_max_nondet_tree_depth =
54 string2optional<std::size_t>(value, 10);
55 if(user_max_nondet_tree_depth.has_value())
62 "failed to convert '" + value +
"' to integer",
87 [](
const std::string &opt) ->
irep_idt { return irep_idt{opt}; });
92 const auto list_of_members_string =
95 const auto list_of_members =
split_string(list_of_members_string,
',');
96 for(
const auto &member : list_of_members)
98 const auto selection_spec_strings =
split_string(member,
'.');
100 selection_specs.push_back({});
101 auto &selection_spec = selection_specs.back();
103 selection_spec_strings.begin(),
104 selection_spec_strings.end(),
105 std::back_inserter(selection_spec),
106 [](
const std::string &member_name_string) {
107 return irep_idt{member_name_string};
118 : initialization_config(std::move(initialization_config)),
119 goto_model(goto_model),
120 max_depth_var_name(get_fresh_global_name(
123 initialization_config.max_nondet_tree_depth,
125 min_depth_var_name(get_fresh_global_name(
128 initialization_config.min_null_tree_depth,
145 if(selection_spec.front() == lhs_id)
155 if(lhs.
id() == ID_symbol)
157 const auto maybe_cluster_index =
159 if(maybe_cluster_index.has_value())
163 const auto set_equal_case =
180 body.
add(set_equal_case);
194 if(lhs.
id() == ID_symbol)
200 if(size_var.has_value())
210 const auto &fun_type_params =
212 const typet &size_var_type = fun_type_params.back().type();
221 for(
const auto &irep_pair :
225 if(irep_pair.second == lhs_name)
234 const exprt &depth_symbol,
238 const bool is_nullable)
242 if(type.
id() == ID_struct_tag)
246 else if(type.
id() == ID_pointer)
252 if(lhs_name.has_value())
265 else if(type.
id() == ID_array)
286 bool is_nullable =
false;
287 bool has_size_param =
false;
288 if(expr.
id() == ID_symbol)
296 has_size_param =
true;
304 const std::string &pretty_type =
type2id(type);
311 depth_parameter.set_identifier(depth_symbol.
name);
312 fun_params.push_back(depth_parameter);
319 fun_params.push_back(result_parameter);
326 if(size_var.has_value())
329 symbol_table.lookup_ref(*size_var).symbol_expr();
338 fun_params.back().set_identifier(size_symbol.
name);
344 symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.
name);
364 if(malloc_sym ==
nullptr)
375 return malloc_sym->symbol_expr();
423 std::ostringstream out{};
424 out <<
"recursive_initialization_config {"
427 <<
"\n mode = " <<
mode
430 <<
"\n pointers_to_treat_as_arrays = [";
433 out <<
"\n " << pointer;
436 <<
"\n variables_that_hold_array_sizes = [";
439 out <<
"\n " << array_size;
442 out <<
"\n array_name_to_associated_size_variable = [";
443 for(
auto const &associated_array_size :
446 out <<
"\n " << associated_array_size.first <<
" -> "
447 << associated_array_size.second;
450 out <<
"\n pointers_to_treat_as_cstrings = [";
451 for(
const auto &pointer_to_treat_as_string_name :
454 out <<
"\n " << pointer_to_treat_as_string_name << std::endl;
462 const std::string &symbol_name,
463 const exprt &initial_value)
const
474 fresh_symbol.
value = initial_value;
475 return fresh_symbol.
name;
479 const std::string &symbol_name)
const
495 const std::string &symbol_name)
const
510 const std::string &symbol_name,
512 const exprt &init_value)
const
522 fresh_symbol.
value = init_value;
527 const std::string &fun_name,
528 const typet &fun_type)
536 function_symbol.
name = function_symbol.base_name =
537 function_symbol.pretty_name = fresh_name;
539 function_symbol.is_lvalue =
true;
541 function_symbol.type = fun_type;
549 const std::string &symbol_name,
550 const typet &symbol_type)
570 return maybe_symbol->symbol_expr();
575 if(type.
id() == ID_struct_tag)
581 else if(type.
id() == ID_pointer)
583 else if(type.
id() == ID_array)
585 const auto array_size =
591 else if(type.
id() == ID_signedbv)
593 else if(type.
id() == ID_unsignedbv)
602 if(free_sym ==
nullptr)
613 return free_sym->symbol_expr();
651 if(has_seen.has_value())
654 should_not_recurse.push_back(has_seen_expr);
660 null_and_return.
add(assign_null);
670 if(has_seen.has_value())
677 seen_assign_prev =
code_assignt{*has_seen, has_seen_prev};
692 if(has_seen.has_value())
694 then_case.add(seen_assign_prev);
710 const auto array_size =
714 for(std::size_t index = 0; index < array_size - 1; index++)
738 const auto array_size =
742 for(std::size_t index = 0; index < array_size; index++)
824 for(
auto array_size = min_array_size; array_size <= max_array_size;
869 body.add(
code_fort{for_init, for_cond, for_iter, for_body});
888 if(common_arguments_origin.has_value() && expr.
id() == ID_symbol)
893 return origin_name == expr_name;
907 if(!maybe_cluster_index.has_value())
916 .get_identifier() != expr_id &&
920 const auto condition =
947 const auto &function_pointer_type =
to_pointer_type(result_type.subtype());
949 const auto &function_type =
to_code_type(function_pointer_type.subtype());
951 std::vector<exprt> targets;
955 if(sym.second.type == function_type)
966 const auto function_pointer_selector =
972 auto function_pointer_index = std::size_t{0};
974 for(
const auto &target : targets)
977 if(function_pointer_index != targets.size() - 1)
980 function_pointer_selector,
981 from_integer(function_pointer_index, function_pointer_selector.type())};
989 ++function_pointer_index;
999 const std::vector<irep_idt> &selection_spec)
1005 auto component_member = lhs;
1008 for(
auto it = selection_spec.begin() + 1; it != selection_spec.end(); it++)
1010 if(component_member.type().id() != ID_struct_tag)
1013 "'" +
id2string(*it) +
"' is not a component name",
1017 const auto &struct_type =
to_struct_type(ns.follow_tag(struct_tag_type));
1020 for(
auto const &
component : struct_type.components())
1022 const auto &component_type =
component.type();
1023 const auto component_name =
component.get_name();
1025 if(*it == component_name)
1028 member_exprt{component_member, component_name, component_type};
1036 "'" +
id2string(*it) +
"' is not a component name",
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::set< irep_idt > pointers_to_treat_as_cstrings
std::string array_name(const namespacet &ns, const exprt &expr)
A codet representing sequential composition of program statements.
static exprt conditional_cast(const exprt &expr, const typet &type)
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & subtype() const
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
irep_idt min_depth_var_name
code_blockt build_array_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for arrays: simply iterates over elements and initialise each one.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
symbol_exprt get_fresh_local_typed_symexpr(const std::string &symbol_name, const typet &type, const exprt &init_value) const
Construct a new local symbol of type type initialised to init_value.
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
symbol_exprt get_symbol_expr(const irep_idt &symbol_name) const
Recover the symbol expression from symbol table.
codet representation of a for statement.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< parametert > parameterst
irep_idt build_constructor(const exprt &expr)
Check if a constructor for the type of expr already exists and create it if not.
void initialize_selected_member(const exprt &lhs, const exprt &depth, code_blockt &body, const std::vector< irep_idt > &selection_spec)
Select the specified struct-member to be non-deterministically initialized.
typet type
Type of symbol.
symbol_exprt get_malloc_function()
Get the malloc function as symbol exprt, and inserts it into the goto-model if it doesn't exist alrea...
Operator to dereference a pointer.
optionalt< irep_idt > get_associated_size_variable(const irep_idt &array_name) const
symbol_exprt get_fresh_local_symexpr(const std::string &symbol_name) const
Construct a new local symbol of type int initialised to 0.
irept & add(const irep_namet &name)
#define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
A codet representing the declaration of a local variable.
The plus expression Associativity is not specified.
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
std::vector< std::vector< irep_idt > > selection_specs
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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...
function_mapt function_map
Expression to hold a symbol (variable)
void free_cluster_origins(code_blockt &body)
bool is_array_size_parameter(const irep_idt &cmdline_arg) const
void initialize(const exprt &lhs, const exprt &depth, code_blockt &body)
Generate initialisation code for lhs into body.
optionalt< equal_cluster_idt > find_equal_cluster(const irep_idt &name) const
codet representation of an if-then-else statement.
code_blockt build_function_pointer_constructor(const symbol_exprt &result, bool is_nullable)
Constructor for function pointers.
irep_idt pretty_name
Language-specific display name.
std::set< irep_idt > pointers_to_treat_as_arrays
bool should_be_treated_as_array(const irep_idt &pointer_name) const
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool needs_freeing(const exprt &expr) const
std::size_t max_nondet_tree_depth
symbolt & get_fresh_param_symbol(const std::string ¶m_name, const typet ¶m_type)
Construct a new parameter symbol of type param_type.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
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.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
std::size_t max_dynamic_array_size
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
irep_idt mode
Language mode.
signedbv_typet signed_int_type()
code_blockt build_pointer_constructor(const exprt &depth, const symbol_exprt &result)
Generic constructor for all pointers: only builds one pointee (not an array) but may recourse in case...
bool arguments_may_be_equal
The null pointer constant.
const std::string & id2string(const irep_idt &d)
std::unordered_set< irep_idt > potential_null_function_pointers
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const
Construct a new global symbol of type int initialised to 0.
type_constructor_namest type_constructor_names
const irep_idt & get_identifier() const
auto optional_lookup(const map_like_collectiont &map, const keyt &key) -> optionalt< decltype(map.find(key) ->second)>
Lookup a key in a map, if found return the associated value, nullopt otherwise.
code_blockt build_array_string_constructor(const symbol_exprt &result) const
Constructor for strings: as array but the last element is zero.
An assumption, which must hold in subsequent code.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
code_blockt build_dynamic_array_constructor(const exprt &depth, const symbol_exprt &result, const exprt &size, const optionalt< irep_idt > &lhs_name)
Constructor for dynamic arrays: allocate memory for n elements (n is random but bounded) and initiali...
Binary multiplication Associativity is not specified.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
#define COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< exprt > operandst
void add(const codet &code)
recursive_initializationt(recursive_initialization_configt initialization_config, goto_modelt &goto_model)
const symbolt & get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type)
Construct a new function symbol of type fun_type.
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
irep_idt get_fresh_global_name(const std::string &symbol_name, const exprt &initial_value) const
Construct a new global symbol of type int and set it's value to initial_value.
nonstd::optional< T > optionalt
std::vector< optionalt< exprt > > common_arguments_origins
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
bitvector_typet char_type()
code_blockt build_constructor_body(const exprt &depth_symbol, const symbol_exprt &result_symbol, const optionalt< exprt > &size_symbol, const optionalt< irep_idt > &lhs_name, const bool is_nullable)
Case analysis for which constructor should be used.
A side_effect_exprt that returns a non-deterministically chosen value.
void free_if_possible(const exprt &expr, code_blockt &body)
std::set< irep_idt > variables_that_hold_array_sizes
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
bool should_be_treated_as_cstring(const irep_idt &pointer_name) const
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Extract member of struct or union.
exprt value
Initial value of symbol.
codet representation of a "return from a function" statement.
goto_functionst goto_functions
GOTO functions.
std::string type2id(const typet &type) const
Simple pretty-printer for typet.
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
std::size_t min_dynamic_array_size
symbol_exprt get_free_function()
Get the free function as symbol expression, and inserts it into the goto-model if it doesn't exist al...
std::size_t require_one_size_value(const std::string &option, const std::list< std::string > &values)
Returns the only Nat value of a single element list, throws an exception if not passed a single eleme...
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
A base class for relations, i.e., binary predicates whose two operands have the same type.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::size_t min_null_tree_depth
std::size_t equal_cluster_idt
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
code_blockt build_nondet_constructor(const symbol_exprt &result) const
Default constructor: assigns non-deterministic value of the right type.
#define COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT
Operator to return the address of an object.
unsignedbv_typet size_type()
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
A codet representing an assignment in the program.
std::string to_string() const
const recursive_initialization_configt initialization_config
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
symbol_tablet symbol_table
Symbol table.
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 ...
irep_idt name
The unique identifier.
irep_idt max_depth_var_name
An expression containing a side effect.
std::vector< std::set< irep_idt > > pointers_to_treat_equal
code_blockt build_struct_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for structures: simply iterates over members and initialise each one.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.