cprover
recursive_initialization.h
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: recursive_initialization
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
9 #ifndef CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
10 #define CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
11 
12 #include <map>
13 #include <set>
14 
16 #include <util/expr.h>
17 #include <util/message.h>
18 #include <util/optional.h>
19 #include <util/prefix.h>
20 #include <util/std_types.h>
21 
23 #include "goto_harness_generator.h"
24 
26 {
27  std::size_t min_null_tree_depth = 1;
28  std::size_t max_nondet_tree_depth = 2;
30  std::unordered_set<irep_idt> potential_null_function_pointers;
31 
32  // array stuff
33  std::size_t max_dynamic_array_size = 2;
34  std::size_t min_dynamic_array_size = 1;
35 
36  std::set<irep_idt> pointers_to_treat_as_arrays;
37  std::set<irep_idt> variables_that_hold_array_sizes;
38  std::map<irep_idt, irep_idt> array_name_to_associated_array_size_variable;
39 
40  std::set<irep_idt> pointers_to_treat_as_cstrings;
41  std::vector<std::set<irep_idt>> pointers_to_treat_equal;
42 
43  bool arguments_may_be_equal = false;
44 
45  std::vector<std::vector<irep_idt>> selection_specs;
46 
47  std::string to_string() const; // for debugging purposes
48 
54  bool handle_option(
55  const std::string &option,
56  const std::list<std::string> &values);
57 };
58 
62 {
63 public:
64  using recursion_sett = std::set<irep_idt>;
65  using equal_cluster_idt = std::size_t;
67  {
71  bool operator<(const constructor_keyt &other) const
72  {
74  std::tie(
75  other.constructor_type,
76  other.is_nullable,
77  other.has_size_parameter);
78  };
79  bool operator==(const constructor_keyt &other) const
80  {
81  return std::tie(constructor_type, is_nullable, has_size_parameter) ==
82  std::tie(
83  other.constructor_type,
84  other.is_nullable,
85  other.has_size_parameter);
86  };
87  };
88  using type_constructor_namest = std::map<constructor_keyt, irep_idt>;
89 
93 
98  void initialize(const exprt &lhs, const exprt &depth, code_blockt &body);
99 
104 
105  bool is_initialization_allowed(const symbolt &symbol)
106  {
107  return (
108  symbol.is_static_lifetime && symbol.is_lvalue &&
109  symbol.type.id() != ID_code &&
111  }
112 
113  bool needs_freeing(const exprt &expr) const;
114  void free_if_possible(const exprt &expr, code_blockt &body);
115  void free_cluster_origins(code_blockt &body);
116 
117 private:
123  std::vector<optionalt<exprt>> common_arguments_origins;
124 
129 
130  bool should_be_treated_as_array(const irep_idt &pointer_name) const;
132  bool is_array_size_parameter(const irep_idt &cmdline_arg) const;
135  bool should_be_treated_as_cstring(const irep_idt &pointer_name) const;
136 
144  const std::string &symbol_name,
145  const exprt &initial_value) const;
146 
150  symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const;
151 
155  symbol_exprt get_fresh_local_symexpr(const std::string &symbol_name) const;
156 
163  const std::string &symbol_name,
164  const typet &type,
165  const exprt &init_value) const;
166 
171  const symbolt &
172  get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type);
173 
179  const std::string &param_name,
180  const typet &param_type);
181 
185  symbol_exprt get_symbol_expr(const irep_idt &symbol_name) const;
186 
191  std::string type2id(const typet &type) const;
192 
201  const exprt &depth_symbol,
203  const optionalt<exprt> &size_symbol,
204  const optionalt<irep_idt> &lhs_name,
205  const bool is_nullable);
206 
211  irep_idt build_constructor(const exprt &expr);
212 
218  const symbol_exprt &result,
219  bool is_nullable);
220 
228  build_pointer_constructor(const exprt &depth, const symbol_exprt &result);
229 
236  build_struct_constructor(const exprt &depth, const symbol_exprt &result);
237 
242 
249  build_array_constructor(const exprt &depth, const symbol_exprt &result);
250 
259  const exprt &depth,
260  const symbol_exprt &result,
261  const exprt &size,
262  const optionalt<irep_idt> &lhs_name);
263 
268 
277  const exprt &lhs,
278  const exprt &depth,
279  code_blockt &body,
280  const std::vector<irep_idt> &selection_spec);
281 };
282 
283 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
recursive_initialization_configt::pointers_to_treat_as_cstrings
std::set< irep_idt > pointers_to_treat_as_cstrings
Definition: recursive_initialization.h:40
array_name
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:20
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:173
recursive_initializationt::is_initialization_allowed
bool is_initialization_allowed(const symbolt &symbol)
Definition: recursive_initialization.h:105
recursive_initializationt::min_depth_var_name
irep_idt min_depth_var_name
Definition: recursive_initialization.h:121
recursive_initializationt::constructor_keyt::is_nullable
bool is_nullable
Definition: recursive_initialization.h:69
recursive_initializationt::build_array_constructor
code_blockt build_array_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for arrays: simply iterates over elements and initialise each one.
Definition: recursive_initialization.cpp:730
recursive_initializationt::get_fresh_local_typed_symexpr
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.
Definition: recursive_initialization.cpp:509
recursive_initializationt::goto_model
goto_modelt & goto_model
Definition: recursive_initialization.h:119
recursive_initializationt::constructor_keyt::operator==
bool operator==(const constructor_keyt &other) const
Definition: recursive_initialization.h:79
recursive_initializationt::get_symbol_expr
symbol_exprt get_symbol_expr(const irep_idt &symbol_name) const
Recover the symbol expression from symbol table.
Definition: recursive_initialization.cpp:566
typet
The type of an expression, extends irept.
Definition: type.h:29
recursive_initializationt::build_constructor
irep_idt build_constructor(const exprt &expr)
Check if a constructor for the type of expr already exists and create it if not.
Definition: recursive_initialization.cpp:275
recursive_initializationt::initialize_selected_member
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.
Definition: recursive_initialization.cpp:995
optional.h
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
recursive_initializationt
Class for generating initialisation code for compound structures.
Definition: recursive_initialization.h:62
recursive_initializationt::get_malloc_function
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...
Definition: recursive_initialization.cpp:361
recursive_initializationt::get_associated_size_variable
optionalt< irep_idt > get_associated_size_variable(const irep_idt &array_name) const
Definition: recursive_initialization.cpp:406
recursive_initializationt::get_fresh_local_symexpr
symbol_exprt get_fresh_local_symexpr(const std::string &symbol_name) const
Construct a new local symbol of type int initialised to 0.
Definition: recursive_initialization.cpp:494
prefix.h
recursive_initializationt::constructor_keyt::constructor_type
typet constructor_type
Definition: recursive_initialization.h:68
recursive_initializationt::type_constructor_namest
std::map< constructor_keyt, irep_idt > type_constructor_namest
Definition: recursive_initialization.h:88
goto_model.h
recursive_initialization_configt::array_name_to_associated_array_size_variable
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
Definition: recursive_initialization.h:38
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
goto_harness_generator.h
recursive_initialization_configt::selection_specs
std::vector< std::vector< irep_idt > > selection_specs
Definition: recursive_initialization.h:45
function_harness_generator_options.h
recursive_initializationt::constructor_keyt::has_size_parameter
bool has_size_parameter
Definition: recursive_initialization.h:70
recursive_initialization_configt::mode
irep_idt mode
Definition: recursive_initialization.h:29
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
recursive_initializationt::free_cluster_origins
void free_cluster_origins(code_blockt &body)
Definition: recursive_initialization.cpp:932
recursive_initializationt::is_array_size_parameter
bool is_array_size_parameter(const irep_idt &cmdline_arg) const
Definition: recursive_initialization.cpp:398
recursive_initializationt::initialize
void initialize(const exprt &lhs, const exprt &depth, code_blockt &body)
Generate initialisation code for lhs into body.
Definition: recursive_initialization.cpp:135
recursive_initializationt::find_equal_cluster
optionalt< equal_cluster_idt > find_equal_cluster(const irep_idt &name) const
Definition: recursive_initialization.cpp:386
recursive_initializationt::recursion_sett
std::set< irep_idt > recursion_sett
Definition: recursive_initialization.h:64
recursive_initializationt::build_function_pointer_constructor
code_blockt build_function_pointer_constructor(const symbol_exprt &result, bool is_nullable)
Constructor for function pointers.
Definition: recursive_initialization.cpp:940
recursive_initializationt::constructor_keyt
Definition: recursive_initialization.h:67
expr.h
recursive_initialization_configt::pointers_to_treat_as_arrays
std::set< irep_idt > pointers_to_treat_as_arrays
Definition: recursive_initialization.h:36
recursive_initializationt::should_be_treated_as_array
bool should_be_treated_as_array(const irep_idt &pointer_name) const
Definition: recursive_initialization.cpp:378
recursive_initializationt::needs_freeing
bool needs_freeing(const exprt &expr) const
Definition: recursive_initialization.cpp:882
recursive_initialization_configt::max_nondet_tree_depth
std::size_t max_nondet_tree_depth
Definition: recursive_initialization.h:28
recursive_initializationt::get_fresh_param_symbol
symbolt & get_fresh_param_symbol(const std::string &param_name, const typet &param_type)
Construct a new parameter symbol of type param_type.
Definition: recursive_initialization.cpp:548
recursive_initialization_configt::max_dynamic_array_size
std::size_t max_dynamic_array_size
Definition: recursive_initialization.h:33
result_symbol
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:597
recursive_initializationt::build_pointer_constructor
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...
Definition: recursive_initialization.cpp:616
recursive_initialization_configt::arguments_may_be_equal
bool arguments_may_be_equal
Definition: recursive_initialization.h:43
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
recursive_initialization_configt::potential_null_function_pointers
std::unordered_set< irep_idt > potential_null_function_pointers
Definition: recursive_initialization.h:30
recursive_initializationt::get_fresh_global_symexpr
symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const
Construct a new global symbol of type int initialised to 0.
Definition: recursive_initialization.cpp:478
recursive_initializationt::type_constructor_names
type_constructor_namest type_constructor_names
Definition: recursive_initialization.h:122
recursive_initializationt::build_array_string_constructor
code_blockt build_array_string_constructor(const symbol_exprt &result) const
Constructor for strings: as array but the last element is zero.
Definition: recursive_initialization.cpp:702
std_types.h
recursive_initializationt::build_dynamic_array_constructor
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...
Definition: recursive_initialization.cpp:780
irept::id
const irep_idt & id() const
Definition: irep.h:418
recursive_initializationt::recursive_initializationt
recursive_initializationt(recursive_initialization_configt initialization_config, goto_modelt &goto_model)
Definition: recursive_initialization.cpp:115
recursive_initializationt::get_fresh_fun_symbol
const symbolt & get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type)
Construct a new function symbol of type fun_type.
Definition: recursive_initialization.cpp:526
recursive_initializationt::get_fresh_global_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.
Definition: recursive_initialization.cpp:461
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
recursive_initializationt::common_arguments_origins
std::vector< optionalt< exprt > > common_arguments_origins
Definition: recursive_initialization.h:123
recursive_initialization_configt::handle_option
bool handle_option(const std::string &option, const std::list< std::string > &values)
Parse the options specific for recursive initialisation.
Definition: recursive_initialization.cpp:27
recursive_initializationt::build_constructor_body
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.
Definition: recursive_initialization.cpp:233
recursive_initializationt::free_if_possible
void free_if_possible(const exprt &expr, code_blockt &body)
Definition: recursive_initialization.cpp:899
recursive_initializationt::constructor_keyt::operator<
bool operator<(const constructor_keyt &other) const
Definition: recursive_initialization.h:71
recursive_initialization_configt::variables_that_hold_array_sizes
std::set< irep_idt > variables_that_hold_array_sizes
Definition: recursive_initialization.h:37
recursive_initializationt::should_be_treated_as_cstring
bool should_be_treated_as_cstring(const irep_idt &pointer_name) const
Definition: recursive_initialization.cpp:414
recursive_initializationt::type2id
std::string type2id(const typet &type) const
Simple pretty-printer for typet.
Definition: recursive_initialization.cpp:573
recursive_initialization_configt::min_dynamic_array_size
std::size_t min_dynamic_array_size
Definition: recursive_initialization.h:34
symbolt
Symbol table entry.
Definition: symbol.h:28
recursive_initializationt::get_free_function
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...
Definition: recursive_initialization.cpp:599
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
recursive_initialization_configt
Definition: recursive_initialization.h:26
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
recursive_initialization_configt::min_null_tree_depth
std::size_t min_null_tree_depth
Definition: recursive_initialization.h:27
recursive_initializationt::equal_cluster_idt
std::size_t equal_cluster_idt
Definition: recursive_initialization.h:65
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
recursive_initializationt::build_nondet_constructor
code_blockt build_nondet_constructor(const symbol_exprt &result) const
Default constructor: assigns non-deterministic value of the right type.
Definition: recursive_initialization.cpp:769
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
message.h
recursive_initialization_configt::to_string
std::string to_string() const
Definition: recursive_initialization.cpp:421
recursive_initializationt::initialization_config
const recursive_initialization_configt initialization_config
Definition: recursive_initialization.h:118
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
recursive_initializationt::max_depth_var_name
irep_idt max_depth_var_name
Definition: recursive_initialization.h:120
recursive_initialization_configt::pointers_to_treat_equal
std::vector< std::set< irep_idt > > pointers_to_treat_equal
Definition: recursive_initialization.h:41
recursive_initializationt::build_struct_constructor
code_blockt build_struct_constructor(const exprt &depth, const symbol_exprt &result)
Constructor for structures: simply iterates over members and initialise each one.
Definition: recursive_initialization.cpp:752