31 const std::string &option,
32 const std::list<std::string> &values)
38 auto const user_min_null_tree_depth =
39 string2optional<std::size_t>(value, 10);
40 if(user_min_null_tree_depth.has_value())
47 "failed to convert '" + value +
"' to integer",
56 auto const user_max_nondet_tree_depth =
57 string2optional<std::size_t>(value, 10);
58 if(user_max_nondet_tree_depth.has_value())
65 "failed to convert '" + value +
"' to integer",
90 [](
const std::string &opt) ->
irep_idt { return irep_idt{opt}; });
95 const auto list_of_members_string =
98 const auto list_of_members =
split_string(list_of_members_string,
',');
99 for(
const auto &member : list_of_members)
101 const auto selection_spec_strings =
split_string(member,
'.');
103 selection_specs.push_back({});
104 auto &selection_spec = selection_specs.back();
106 selection_spec_strings.begin(),
107 selection_spec_strings.end(),
108 std::back_inserter(selection_spec),
109 [](
const std::string &member_name_string) {
110 return irep_idt{member_name_string};
121 : initialization_config(std::move(initialization_config)),
122 goto_model(goto_model),
123 max_depth_var_name(get_fresh_global_name(
126 initialization_config.max_nondet_tree_depth,
128 min_depth_var_name(get_fresh_global_name(
131 initialization_config.min_null_tree_depth,
148 if(selection_spec.front() == lhs_id)
158 if(lhs.
id() == ID_symbol)
160 const auto maybe_cluster_index =
162 if(maybe_cluster_index.has_value())
166 const auto set_equal_case =
175 const auto should_make_equal =
179 should_make_equal, set_equal_case, proper_init_case});
183 body.
add(set_equal_case);
197 if(lhs.
id() == ID_symbol)
203 if(size_var.has_value())
213 const auto &fun_type_params =
216 type_try_dynamic_cast<pointer_typet>(fun_type_params.back().type());
217 INVARIANT(size_var_type,
"Size parameter must have pointer type.");
224 for(
const auto &irep_pair :
228 if(irep_pair.second == lhs_name)
246 const exprt &depth_symbol,
250 const bool is_nullable)
254 if(type.
id() == ID_struct_tag)
258 else if(type.
id() == ID_pointer)
269 if(lhs_name.has_value())
280 else if(type.
id() == ID_array)
301 bool is_nullable =
false;
302 bool has_size_param =
false;
303 if(expr.
id() == ID_symbol)
311 has_size_param =
true;
319 const std::string &pretty_type =
type2id(type);
326 depth_parameter.set_identifier(depth_symbol.
name);
327 fun_params.push_back(depth_parameter);
334 fun_params.push_back(result_parameter);
341 if(size_var.has_value())
344 symbol_table.lookup_ref(*size_var).symbol_expr();
353 fun_params.back().set_identifier(size_symbol.
name);
359 symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.
name);
377 if(malloc_sym ==
nullptr)
388 return malloc_sym->symbol_expr();
436 std::ostringstream out{};
437 out <<
"recursive_initialization_config {"
440 <<
"\n mode = " <<
mode
443 <<
"\n pointers_to_treat_as_arrays = [";
446 out <<
"\n " << pointer;
449 <<
"\n variables_that_hold_array_sizes = [";
452 out <<
"\n " << array_size;
455 out <<
"\n array_name_to_associated_size_variable = [";
456 for(
auto const &associated_array_size :
459 out <<
"\n " << associated_array_size.first <<
" -> "
460 << associated_array_size.second;
463 out <<
"\n pointers_to_treat_as_cstrings = [";
464 for(
const auto &pointer_to_treat_as_string_name :
467 out <<
"\n " << pointer_to_treat_as_string_name << std::endl;
476 const std::string &symbol_base_name,
483 std::move(symbol_type),
497 fresh_symbol.
location = std::move(source_location);
502 const std::string &symbol_name,
503 const exprt &initial_value)
const
510 fresh_symbol.value = initial_value;
511 return fresh_symbol.name;
515 const std::string &symbol_name)
const
523 return fresh_symbol.symbol_expr();
527 const std::string &symbol_name)
const
542 const std::string &symbol_name,
543 const typet &type)
const
558 const std::string &fun_name,
559 const typet &fun_type)
567 function_symbol.
name = function_symbol.base_name =
568 function_symbol.pretty_name = fresh_name;
570 function_symbol.is_lvalue =
true;
572 function_symbol.type = fun_type;
580 const std::string &symbol_name,
581 const typet &symbol_type)
602 return maybe_symbol->symbol_expr();
607 if(type.
id() == ID_struct_tag)
613 else if(type.
id() == ID_pointer)
615 else if(type.
id() == ID_array)
617 const auto array_size =
623 else if(type.
id() == ID_signedbv)
625 else if(type.
id() == ID_unsignedbv)
634 if(free_sym ==
nullptr)
645 return free_sym->symbol_expr();
684 if(has_seen.has_value())
687 should_not_recurse.push_back(has_seen_expr);
695 const auto should_recurse_nondet =
700 should_recurse_nondet};
704 if(has_seen.has_value())
711 seen_assign_prev =
code_assignt{*has_seen, has_seen_prev};
715 const typet non_const_pointer_type =
732 if(has_seen.has_value())
734 then_case.add(seen_assign_prev);
750 const auto array_size =
754 for(std::size_t index = 0; index < array_size; index++)
786 if(
component.type().get_bool(ID_C_constant))
794 return std::move(member_expr);
797 initialize(component_initialisation_lhs, depth, body);
807 auto const nondet_symbol =
823 const typet &element_type = dynamic_array_type.
subtype();
856 const typet mutable_dynamic_array_type =
862 for(
auto array_size = min_array_size; array_size <= max_array_size;
907 body.add(
code_fort{for_init, for_cond, for_iter, for_body});
926 if(common_arguments_origin.has_value() && expr.
id() == ID_symbol)
931 return origin_name == expr_name;
945 if(!maybe_cluster_index.has_value())
954 .get_identifier() != expr_id &&
958 const auto condition =
985 const auto &function_pointer_type =
to_pointer_type(result_type.subtype());
987 const auto &function_type =
to_code_type(function_pointer_type.subtype());
989 std::vector<exprt> targets;
993 if(sym.second.type == function_type)
1004 const auto function_pointer_selector =
1006 body.add(
code_declt{function_pointer_selector});
1007 auto function_pointer_index = std::size_t{0};
1009 for(
const auto &target : targets)
1012 auto const sym_to_lookup =
1013 target.
id() == ID_address_of
1033 if(function_pointer_index != targets.size() - 1)
1036 function_pointer_selector,
1037 from_integer(function_pointer_index, function_pointer_selector.type())};
1045 ++function_pointer_index;
1055 const std::vector<irep_idt> &selection_spec)
1061 auto component_member = lhs;
1064 for(
auto it = selection_spec.begin() + 1; it != selection_spec.end(); it++)
1066 if(component_member.type().id() != ID_struct_tag)
1069 "'" +
id2string(*it) +
"' is not a component name",
1073 const auto &struct_type =
to_struct_type(ns.follow_tag(struct_tag_type));
1076 for(
auto const &
component : struct_type.components())
1078 const auto &component_type =
component.type();
1079 const auto component_name =
component.get_name();
1081 if(*it == component_name)
1084 member_exprt{component_member, component_name, component_type};
1092 "'" +
id2string(*it) +
"' is not a component name",
std::string array_name(const namespacet &ns, const exprt &expr)
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
unsignedbv_typet size_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
Operator to return the address of an object.
const exprt & size() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
A base class for relations, i.e., binary predicates whose two operands have the same type.
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
void add(const codet &code)
A codet representing the declaration of a local variable.
codet representation of a for statement.
codet representation of a function call statement.
codet representation of an if-then-else statement.
codet representation of a "return from a function" statement.
std::vector< parametert > parameterst
const parameterst & parameters() 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.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
symbol_tablet symbol_table
Symbol table.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
irept & add(const irep_namet &name)
const irep_idt & id() const
Extract member of struct or union.
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
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.
std::vector< optionalt< exprt > > common_arguments_origins
std::string type2id(const typet &type) const
Simple pretty-printer for typet.
void free_if_possible(const exprt &expr, code_blockt &body)
type_constructor_namest type_constructor_names
code_blockt build_nondet_constructor(const symbol_exprt &result) const
Default constructor: assigns non-deterministic value of the right type.
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...
code_blockt build_struct_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for structures: simply iterates over members and initialise each one.
irep_idt build_constructor(const exprt &expr)
Check if a constructor for the type of expr already exists and create it if not.
irep_idt max_depth_var_name
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.
code_blockt build_function_pointer_constructor(const symbol_exprt &result, bool is_nullable)
Constructor for function pointers.
const recursive_initialization_configt initialization_config
irep_idt min_depth_var_name
symbol_exprt get_fresh_local_typed_symexpr(const std::string &symbol_name, const typet &type) const
Construct a new local symbol of type type initialised to init_value.
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...
code_blockt build_array_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for arrays: simply iterates over elements and initialise each one.
optionalt< equal_cluster_idt > find_equal_cluster(const irep_idt &name) const
recursive_initializationt(recursive_initialization_configt initialization_config, goto_modelt &goto_model)
std::size_t equal_cluster_idt
void free_cluster_origins(code_blockt &body)
bool should_be_treated_as_array(const irep_idt &pointer_name) const
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.
void initialize(const exprt &lhs, const exprt &depth, code_blockt &body)
Generate initialisation code for lhs into body.
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...
bool needs_freeing(const exprt &expr) const
const symbolt & get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type)
Construct a new function symbol of type fun_type.
bool should_be_treated_as_cstring(const irep_idt &pointer_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.
bool is_array_size_parameter(const irep_idt &cmdline_arg) const
symbol_exprt get_symbol_expr(const irep_idt &symbol_name) const
Recover the symbol expression from symbol table.
symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const
Construct a new global symbol of type int initialised to 0.
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...
optionalt< irep_idt > get_associated_size_variable(const irep_idt &array_name) const
symbolt & get_fresh_param_symbol(const std::string ¶m_name, const typet ¶m_type)
Construct a new parameter symbol of type param_type.
An expression containing a side effect.
void set_file(const irep_idt &file)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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 pretty_name
Language-specific display name.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT
#define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT
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.
const std::string & id2string(const irep_idt &d)
Mangle names of file-local functions to make them unique.
#define FILE_LOCAL_PREFIX
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...
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...
nonstd::optional< T > optionalt
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.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
code_blockt build_null_pointer(const symbol_exprt &result_symbol)
static symbolt & get_fresh_global_symbol(symbol_tablet &symbol_table, const std::string &symbol_base_name, typet symbol_type, irep_idt mode)
#define GOTO_HARNESS_PREFIX
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
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
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
std::vector< std::vector< irep_idt > > selection_specs
bool arguments_may_be_equal
std::size_t max_dynamic_array_size
std::set< irep_idt > variables_that_hold_array_sizes
std::size_t max_nondet_tree_depth
std::set< irep_idt > pointers_to_treat_as_arrays
std::size_t min_null_tree_depth
std::size_t min_dynamic_array_size
std::string to_string() const
std::unordered_set< irep_idt > potential_null_function_pointers
typet remove_const(typet type)
Remove const qualifier from type (if any).