Go to the documentation of this file.
29 const std::string &option,
30 const std::list<std::string> &values)
36 auto const user_min_null_tree_depth =
37 string2optional<std::size_t>(value, 10);
38 if(user_min_null_tree_depth.has_value())
45 "failed to convert '" + value +
"' to integer",
54 auto const user_max_nondet_tree_depth =
55 string2optional<std::size_t>(value, 10);
56 if(user_max_nondet_tree_depth.has_value())
63 "failed to convert '" + value +
"' to integer",
88 [](
const std::string &opt) ->
irep_idt { return irep_idt{opt}; });
93 const auto list_of_members_string =
96 const auto list_of_members =
split_string(list_of_members_string,
',');
97 for(
const auto &member : list_of_members)
99 const auto selection_spec_strings =
split_string(member,
'.');
101 selection_specs.push_back({});
102 auto &selection_spec = selection_specs.back();
104 selection_spec_strings.begin(),
105 selection_spec_strings.end(),
106 std::back_inserter(selection_spec),
107 [](
const std::string &member_name_string) {
108 return irep_idt{member_name_string};
119 : initialization_config(std::move(initialization_config)),
120 goto_model(goto_model),
121 max_depth_var_name(get_fresh_global_name(
124 initialization_config.max_nondet_tree_depth,
126 min_depth_var_name(get_fresh_global_name(
129 initialization_config.min_null_tree_depth,
146 if(selection_spec.front() == lhs_id)
156 if(lhs.
id() == ID_symbol)
158 const auto maybe_cluster_index =
160 if(maybe_cluster_index.has_value())
164 const auto set_equal_case =
173 const auto should_make_equal =
177 should_make_equal, set_equal_case, proper_init_case});
181 body.
add(set_equal_case);
195 if(lhs.
id() == ID_symbol)
201 if(size_var.has_value())
211 const auto &fun_type_params =
214 type_try_dynamic_cast<pointer_typet>(fun_type_params.back().type());
215 INVARIANT(size_var_type,
"Size parameter must have pointer type.");
222 for(
const auto &irep_pair :
226 if(irep_pair.second == lhs_name)
244 const exprt &depth_symbol,
248 const bool is_nullable)
252 if(type.
id() == ID_struct_tag)
256 else if(type.
id() == ID_pointer)
267 if(lhs_name.has_value())
278 else if(type.
id() == ID_array)
299 bool is_nullable =
false;
300 bool has_size_param =
false;
301 if(expr.
id() == ID_symbol)
309 has_size_param =
true;
317 const std::string &pretty_type =
type2id(type);
324 depth_parameter.set_identifier(depth_symbol.
name);
325 fun_params.push_back(depth_parameter);
332 fun_params.push_back(result_parameter);
339 if(size_var.has_value())
342 symbol_table.lookup_ref(*size_var).symbol_expr();
351 fun_params.back().set_identifier(size_symbol.
name);
357 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",
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
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.
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.
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
Fresh auxiliary symbol creation.
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.
#define FILE_LOCAL_PREFIX
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
typet remove_const(typet type)
Remove const qualifier from type (if any).
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.
code_blockt build_null_pointer(const symbol_exprt &result_symbol)
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)
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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.
An assumption, which must hold in subsequent code.
void set_file(const irep_idt &file)
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)
#define GOTO_HARNESS_PREFIX
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.
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.
source_locationt location
Source code location of definition of symbol.
#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)
bool has_prefix(const std::string &s, const std::string &prefix)
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
static symbolt & get_fresh_global_symbol(symbol_tablet &symbol_table, const std::string &symbol_base_name, typet symbol_type, irep_idt mode)
Operator to return the address of an object.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
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
irep_idt module
Name of module the symbol belongs to.
const recursive_initialization_configt initialization_config
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
API to expression classes.
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.
Mangle names of file-local functions to make them unique.
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.