cprover
recursive_initialization.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: recursive_initialization
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
12 #include <util/allocate_objects.h>
13 #include <util/arith_tools.h>
14 #include <util/c_types.h>
15 #include <util/fresh_symbol.h>
16 #include <util/irep.h>
17 #include <util/optional_utils.h>
19 #include <util/rename.h>
20 #include <util/std_code.h>
21 #include <util/std_expr.h>
22 #include <util/string2int.h>
23 #include <util/string_utils.h>
24 
25 #include <functional>
26 #include <iterator>
27 
29  const std::string &option,
30  const std::list<std::string> &values)
31 {
33  {
34  auto const value =
36  auto const user_min_null_tree_depth =
37  string2optional<std::size_t>(value, 10);
38  if(user_min_null_tree_depth.has_value())
39  {
40  min_null_tree_depth = user_min_null_tree_depth.value();
41  }
42  else
43  {
45  "failed to convert '" + value + "' to integer",
47  }
48  return true;
49  }
51  {
52  auto const value =
54  auto const user_max_nondet_tree_depth =
55  string2optional<std::size_t>(value, 10);
56  if(user_max_nondet_tree_depth.has_value())
57  {
58  max_nondet_tree_depth = user_max_nondet_tree_depth.value();
59  }
60  else
61  {
63  "failed to convert '" + value + "' to integer",
65  }
66  return true;
67  }
69  {
72  return true;
73  }
75  {
78  return true;
79  }
81  {
82  std::transform(
83  values.begin(),
84  values.end(),
85  std::inserter(
88  [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
89  return true;
90  }
92  {
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)
98  {
99  const auto selection_spec_strings = split_string(member, '.');
100 
101  selection_specs.push_back({});
102  auto &selection_spec = selection_specs.back();
103  std::transform(
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};
109  });
110  }
111  return true;
112  }
113  return false;
114 }
115 
117  recursive_initialization_configt initialization_config,
118  goto_modelt &goto_model)
119  : initialization_config(std::move(initialization_config)),
120  goto_model(goto_model),
121  max_depth_var_name(get_fresh_global_name(
122  "max_depth",
123  from_integer(
124  initialization_config.max_nondet_tree_depth,
125  signed_int_type()))),
126  min_depth_var_name(get_fresh_global_name(
127  "min_depth",
128  from_integer(
129  initialization_config.min_null_tree_depth,
130  signed_int_type())))
131 {
133  this->initialization_config.pointers_to_treat_equal.size());
134 }
135 
137  const exprt &lhs,
138  const exprt &depth,
139  code_blockt &body)
140 {
141  if(lhs.id() == ID_symbol && !initialization_config.selection_specs.empty())
142  {
143  auto lhs_id = to_symbol_expr(lhs).get_identifier();
144  for(const auto &selection_spec : initialization_config.selection_specs)
145  {
146  if(selection_spec.front() == lhs_id)
147  {
148  initialize_selected_member(lhs, depth, body, selection_spec);
149  return;
150  }
151  }
152  }
153  // special handling for the case that pointer arguments should be treated
154  // equal: if the equality is enforced (rather than the pointers may be equal),
155  // then we don't even build the constructor functions
156  if(lhs.id() == ID_symbol)
157  {
158  const auto maybe_cluster_index =
159  find_equal_cluster(to_symbol_expr(lhs).get_identifier());
160  if(maybe_cluster_index.has_value())
161  {
162  if(common_arguments_origins[*maybe_cluster_index].has_value())
163  {
164  const auto set_equal_case =
165  code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]};
167  {
168  const irep_idt &fun_name = build_constructor(lhs);
169  const symbolt &fun_symbol =
171  const auto proper_init_case = code_function_callt{
172  fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}}};
173  const auto should_make_equal =
174  get_fresh_local_typed_symexpr("should_make_equal", bool_typet{});
175  body.add(code_declt{should_make_equal});
176  body.add(code_ifthenelset{
177  should_make_equal, set_equal_case, proper_init_case});
178  }
179  else
180  {
181  body.add(set_equal_case);
182  }
183  return;
184  }
185  else
186  {
187  common_arguments_origins[*maybe_cluster_index] = lhs;
188  }
189  }
190  }
191 
192  const irep_idt &fun_name = build_constructor(lhs);
193  const symbolt &fun_symbol = goto_model.symbol_table.lookup_ref(fun_name);
194 
195  if(lhs.id() == ID_symbol)
196  {
197  const irep_idt &lhs_name = to_symbol_expr(lhs).get_identifier();
198  if(should_be_treated_as_array(lhs_name))
199  {
200  auto size_var = get_associated_size_variable(lhs_name);
201  if(size_var.has_value())
202  {
203  const symbol_exprt &size_symbol =
204  goto_model.symbol_table.lookup_ref(size_var.value()).symbol_expr();
206  fun_symbol.symbol_expr(),
207  {depth, address_of_exprt{lhs}, address_of_exprt{size_symbol}}});
208  }
209  else
210  {
211  const auto &fun_type_params =
212  to_code_type(fun_symbol.type).parameters();
213  const pointer_typet *size_var_type =
214  type_try_dynamic_cast<pointer_typet>(fun_type_params.back().type());
215  INVARIANT(size_var_type, "Size parameter must have pointer type.");
217  fun_symbol.symbol_expr(),
218  {depth, address_of_exprt{lhs}, null_pointer_exprt{*size_var_type}}});
219  }
220  return;
221  }
222  for(const auto &irep_pair :
224  {
225  // skip initialisation of array-size variables
226  if(irep_pair.second == lhs_name)
227  return;
228  }
229  }
230  body.add(code_function_callt{fun_symbol.symbol_expr(),
231  {depth, address_of_exprt{lhs}}});
232 }
233 
235 {
236  const typet &type_to_construct = result_symbol.type().subtype();
237  const null_pointer_exprt nullptr_expr{to_pointer_type(type_to_construct)};
238  const code_assignt assign_null{dereference_exprt{result_symbol},
239  nullptr_expr};
240  return code_blockt{{assign_null, code_returnt{}}};
241 }
242 
244  const exprt &depth_symbol,
246  const optionalt<exprt> &size_symbol,
247  const optionalt<irep_idt> &lhs_name,
248  const bool is_nullable)
249 {
250  PRECONDITION(result_symbol.type().id() == ID_pointer);
251  const typet &type = result_symbol.type().subtype();
252  if(type.id() == ID_struct_tag)
253  {
254  return build_struct_constructor(depth_symbol, result_symbol);
255  }
256  else if(type.id() == ID_pointer)
257  {
258  if(type.subtype().id() == ID_code)
259  {
261  }
262  if(type.subtype().id() == ID_empty)
263  {
264  // always initalize void* pointers as NULL
266  }
267  if(lhs_name.has_value())
268  {
269  if(should_be_treated_as_array(*lhs_name))
270  {
271  CHECK_RETURN(size_symbol.has_value());
273  depth_symbol, result_symbol, *size_symbol, lhs_name);
274  }
275  }
276  return build_pointer_constructor(depth_symbol, result_symbol);
277  }
278  else if(type.id() == ID_array)
279  {
280  return build_array_constructor(depth_symbol, result_symbol);
281  }
282  else
283  {
285  }
286 }
287 
289 {
290  // for `expr` of type T builds a declaration of a function:
291  //
292  // void type_constructor_T(int depth_T, T *result);
293  //
294  // or in case a `size` is associated with the `expr`
295  //
296  // void type_constructor_T(int depth_T, T *result_T, int *size);
297  optionalt<irep_idt> size_var;
298  optionalt<irep_idt> expr_name;
299  bool is_nullable = false;
300  bool has_size_param = false;
301  if(expr.id() == ID_symbol)
302  {
303  expr_name = to_symbol_expr(expr).get_identifier();
305  expr_name.value());
306  if(should_be_treated_as_array(*expr_name))
307  {
308  size_var = get_associated_size_variable(*expr_name);
309  has_size_param = true;
310  }
311  }
312  const typet &type = expr.type();
313  const constructor_keyt key{type, is_nullable, has_size_param};
314  if(type_constructor_names.find(key) != type_constructor_names.end())
315  return type_constructor_names[key];
316 
317  const std::string &pretty_type = type2id(type);
318  symbolt &depth_symbol =
319  get_fresh_param_symbol("depth_" + pretty_type, signed_int_type());
320  depth_symbol.value = from_integer(0, signed_int_type());
321 
322  code_typet::parameterst fun_params;
323  code_typet::parametert depth_parameter{signed_int_type()};
324  depth_parameter.set_identifier(depth_symbol.name);
325  fun_params.push_back(depth_parameter);
326 
327  const typet &result_type = pointer_type(type);
328  const symbolt &result_symbol =
329  get_fresh_param_symbol("result_" + pretty_type, result_type);
330  code_typet::parametert result_parameter{result_type};
331  result_parameter.set_identifier(result_symbol.name);
332  fun_params.push_back(result_parameter);
333 
334  auto &symbol_table = goto_model.symbol_table;
335  optionalt<exprt> size_symbol_expr;
336  if(expr_name.has_value() && should_be_treated_as_array(*expr_name))
337  {
338  typet size_var_type;
339  if(size_var.has_value())
340  {
341  const symbol_exprt &size_var_symbol_expr =
342  symbol_table.lookup_ref(*size_var).symbol_expr();
343  size_var_type = pointer_type(size_var_symbol_expr.type());
344  }
345  else
346  size_var_type = pointer_type(signed_int_type());
347 
348  const symbolt &size_symbol =
349  get_fresh_param_symbol("size_" + pretty_type, size_var_type);
350  fun_params.push_back(code_typet::parametert{size_var_type});
351  fun_params.back().set_identifier(size_symbol.name);
352  size_symbol_expr = size_symbol.symbol_expr();
353  }
354  const symbolt &function_symbol = get_fresh_fun_symbol(
355  "type_constructor_" + pretty_type, code_typet{fun_params, empty_typet{}});
356  type_constructor_names[key] = function_symbol.name;
357  symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.name);
358 
359  // the body is specific for each type of expression
360  mutable_symbol->value = build_constructor_body(
361  depth_symbol.symbol_expr(),
363  size_symbol_expr,
364  // the expression name may be needed to decide if expr should be treated as
365  // a string
366  expr_name,
367  is_nullable);
368 
369  goto_model.goto_functions.function_map[function_symbol.name].type =
370  to_code_type(function_symbol.type);
371  return type_constructor_names.at(key);
372 }
373 
375 {
376  auto malloc_sym = goto_model.symbol_table.lookup("malloc");
377  if(malloc_sym == nullptr)
378  {
379  symbolt new_malloc_sym;
380  new_malloc_sym.type = code_typet{code_typet{
382  new_malloc_sym.name = new_malloc_sym.pretty_name =
383  new_malloc_sym.base_name = "malloc";
384  new_malloc_sym.mode = initialization_config.mode;
385  goto_model.symbol_table.insert(new_malloc_sym);
386  return new_malloc_sym.symbol_expr();
387  }
388  return malloc_sym->symbol_expr();
389 }
390 
392  const irep_idt &array_name) const
393 {
396 }
397 
400 {
401  for(equal_cluster_idt index = 0;
403  ++index)
404  {
405  if(initialization_config.pointers_to_treat_equal[index].count(name) != 0)
406  return index;
407  }
408  return {};
409 }
410 
412  const irep_idt &cmdline_arg) const
413 {
415  cmdline_arg) !=
417 }
418 
420  const irep_idt &array_name) const
421 {
422  return optional_lookup(
424  array_name);
425 }
426 
428  const irep_idt &pointer_name) const
429 {
431  pointer_name) != 0;
432 }
433 
435 {
436  std::ostringstream out{};
437  out << "recursive_initialization_config {"
438  << "\n min_null_tree_depth = " << min_null_tree_depth
439  << "\n max_nondet_tree_depth = " << max_nondet_tree_depth
440  << "\n mode = " << mode
441  << "\n max_dynamic_array_size = " << max_dynamic_array_size
442  << "\n min_dynamic_array_size = " << min_dynamic_array_size
443  << "\n pointers_to_treat_as_arrays = [";
444  for(auto const &pointer : pointers_to_treat_as_arrays)
445  {
446  out << "\n " << pointer;
447  }
448  out << "\n ]"
449  << "\n variables_that_hold_array_sizes = [";
450  for(auto const &array_size : variables_that_hold_array_sizes)
451  {
452  out << "\n " << array_size;
453  }
454  out << "\n ]";
455  out << "\n array_name_to_associated_size_variable = [";
456  for(auto const &associated_array_size :
458  {
459  out << "\n " << associated_array_size.first << " -> "
460  << associated_array_size.second;
461  }
462  out << "\n ]";
463  out << "\n pointers_to_treat_as_cstrings = [";
464  for(const auto &pointer_to_treat_as_string_name :
466  {
467  out << "\n " << pointer_to_treat_as_string_name << std::endl;
468  }
469  out << "\n ]";
470  out << "\n}";
471  return out.str();
472 }
473 
475  symbol_tablet &symbol_table,
476  const std::string &symbol_base_name,
477  typet symbol_type,
478  irep_idt mode)
479 {
480  source_locationt source_location{};
481  source_location.set_file(GOTO_HARNESS_PREFIX "harness.c");
482  symbolt &fresh_symbol = get_fresh_aux_symbol(
483  std::move(symbol_type),
485  symbol_base_name,
487  mode,
488  symbol_table);
489  fresh_symbol.base_name = fresh_symbol.pretty_name = symbol_base_name;
490  fresh_symbol.is_static_lifetime = true;
491  fresh_symbol.is_lvalue = true;
492  fresh_symbol.is_auxiliary = false;
493  fresh_symbol.is_file_local = false;
494  fresh_symbol.is_thread_local = false;
495  fresh_symbol.is_state_var = false;
496  fresh_symbol.module = GOTO_HARNESS_PREFIX "harness";
497  fresh_symbol.location = std::move(source_location);
498  return fresh_symbol;
499 }
500 
502  const std::string &symbol_name,
503  const exprt &initial_value) const
504 {
505  auto &fresh_symbol = get_fresh_global_symbol(
507  symbol_name,
508  signed_int_type(), // FIXME why always signed_int_type???
510  fresh_symbol.value = initial_value;
511  return fresh_symbol.name;
512 }
513 
515  const std::string &symbol_name) const
516 {
517  auto &fresh_symbol = get_fresh_global_symbol(
519  symbol_name,
520  signed_int_type(),
522  fresh_symbol.value = from_integer(0, signed_int_type());
523  return fresh_symbol.symbol_expr();
524 }
525 
527  const std::string &symbol_name) const
528 {
529  symbolt &fresh_symbol = get_fresh_aux_symbol(
530  signed_int_type(),
532  symbol_name,
536  fresh_symbol.is_lvalue = true;
537  fresh_symbol.value = from_integer(0, signed_int_type());
538  return fresh_symbol.symbol_expr();
539 }
540 
542  const std::string &symbol_name,
543  const typet &type) const
544 {
545  symbolt &fresh_symbol = get_fresh_aux_symbol(
546  type,
548  symbol_name,
552  fresh_symbol.is_lvalue = true;
553  fresh_symbol.mode = initialization_config.mode;
554  return fresh_symbol.symbol_expr();
555 }
556 
558  const std::string &fun_name,
559  const typet &fun_type)
560 {
561  irep_idt fresh_name(fun_name);
562 
563  get_new_name(fresh_name, namespacet{goto_model.symbol_table}, '_');
564 
565  // create the function symbol
566  symbolt function_symbol{};
567  function_symbol.name = function_symbol.base_name =
568  function_symbol.pretty_name = fresh_name;
569 
570  function_symbol.is_lvalue = true;
571  function_symbol.mode = initialization_config.mode;
572  function_symbol.type = fun_type;
573 
574  auto r = goto_model.symbol_table.insert(function_symbol);
575  CHECK_RETURN(r.second);
576  return *goto_model.symbol_table.lookup(fresh_name);
577 }
578 
580  const std::string &symbol_name,
581  const typet &symbol_type)
582 {
583  symbolt &param_symbol = get_fresh_aux_symbol(
584  symbol_type,
586  symbol_name,
590  param_symbol.is_parameter = true;
591  param_symbol.is_lvalue = true;
592  param_symbol.mode = initialization_config.mode;
593 
594  return param_symbol;
595 }
596 
599 {
600  auto maybe_symbol = goto_model.symbol_table.lookup(symbol_name);
601  CHECK_RETURN(maybe_symbol != nullptr);
602  return maybe_symbol->symbol_expr();
603 }
604 
605 std::string recursive_initializationt::type2id(const typet &type) const
606 {
607  if(type.id() == ID_struct_tag)
608  {
609  auto st_tag = id2string(to_struct_tag_type(type).get_identifier());
610  std::replace(st_tag.begin(), st_tag.end(), '-', '_');
611  return st_tag;
612  }
613  else if(type.id() == ID_pointer)
614  return "ptr_" + type2id(type.subtype());
615  else if(type.id() == ID_array)
616  {
617  const auto array_size =
618  numeric_cast_v<std::size_t>(to_constant_expr(to_array_type(type).size()));
619  return "arr_" + type2id(type.subtype()) + "_" + std::to_string(array_size);
620  }
621  else if(type == char_type())
622  return "char";
623  else if(type.id() == ID_signedbv)
624  return "int";
625  else if(type.id() == ID_unsignedbv)
626  return "uint";
627  else
628  return "";
629 }
630 
632 {
633  auto free_sym = goto_model.symbol_table.lookup("free");
634  if(free_sym == nullptr)
635  {
636  symbolt new_free_sym;
637  new_free_sym.type = code_typet{code_typet{
639  new_free_sym.name = new_free_sym.pretty_name = new_free_sym.base_name =
640  "free";
641  new_free_sym.mode = initialization_config.mode;
642  goto_model.symbol_table.insert(new_free_sym);
643  return new_free_sym.symbol_expr();
644  }
645  return free_sym->symbol_expr();
646 }
647 
649  const exprt &depth,
650  const symbol_exprt &result)
651 {
652  PRECONDITION(result.type().id() == ID_pointer);
653  const typet &type = result.type().subtype();
654  PRECONDITION(type.id() == ID_pointer);
655  PRECONDITION(type.subtype().id() != ID_empty);
656 
657  code_blockt body{};
658  // build:
659  // void type_constructor_ptr_T(int depth, T** result)
660  // {
661  // if(has_seen && depth >= max_depth)
662  // *result=NULL;
663  // return
664  // if(nondet()) {
665  // size_t has_seen_prev;
666  // has_seen_prev = T_has_seen;
667  // T_has_seen = 1;
668  // *result = malloc(sizeof(T));
669  // type_constructor_T(depth+1, *result);
670  // T_has_seen=has_seen_prev;
671  // }
672  // else
673  // *result=NULL;
674  // }
675 
676  binary_predicate_exprt depth_gt_max_depth{
677  depth, ID_ge, get_symbol_expr(max_depth_var_name)};
678  exprt::operandst should_not_recurse{depth_gt_max_depth};
679 
680  optionalt<symbol_exprt> has_seen;
682  has_seen = get_fresh_global_symexpr("has_seen_" + type2id(type.subtype()));
683 
684  if(has_seen.has_value())
685  {
686  equal_exprt has_seen_expr{*has_seen, from_integer(1, has_seen->type())};
687  should_not_recurse.push_back(has_seen_expr);
688  }
689 
690  null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
691  const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
692  code_blockt null_and_return{{assign_null, code_returnt{}}};
693  body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
694 
695  const auto should_recurse_nondet =
696  get_fresh_local_typed_symexpr("should_recurse_nondet", bool_typet{});
697  body.add(code_declt{should_recurse_nondet});
698  exprt::operandst should_recurse_ops{
700  should_recurse_nondet};
701  code_blockt then_case{};
702 
703  code_assignt seen_assign_prev{};
704  if(has_seen.has_value())
705  {
706  const symbol_exprt &has_seen_prev =
707  get_fresh_local_symexpr("has_seen_prev_" + type2id(type.subtype()));
708  then_case.add(code_declt{has_seen_prev});
709  then_case.add(code_assignt{has_seen_prev, *has_seen});
710  then_case.add(code_assignt{*has_seen, from_integer(1, has_seen->type())});
711  seen_assign_prev = code_assignt{*has_seen, has_seen_prev};
712  }
713 
714  // we want to initialize the pointee as non-const even for pointer to const
715  const typet non_const_pointer_type =
717  const symbol_exprt &local_result =
718  get_fresh_local_typed_symexpr("local_result", non_const_pointer_type);
719 
720  then_case.add(code_declt{local_result});
722  then_case.add(
723  code_function_callt{local_result,
725  {*size_of_expr(non_const_pointer_type.subtype(), ns)}});
726  initialize(
727  dereference_exprt{local_result},
728  plus_exprt{depth, from_integer(1, depth.type())},
729  then_case);
730  then_case.add(code_assignt{dereference_exprt{result}, local_result});
731 
732  if(has_seen.has_value())
733  {
734  then_case.add(seen_assign_prev);
735  }
736 
737  body.add(
738  code_ifthenelset{disjunction(should_recurse_ops), then_case, assign_null});
739  return body;
740 }
741 
743  const exprt &depth,
744  const symbol_exprt &result)
745 {
746  PRECONDITION(result.type().id() == ID_pointer);
747  const typet &type = result.type().subtype();
748  PRECONDITION(type.id() == ID_array);
749  const array_typet &array_type = to_array_type(type);
750  const auto array_size =
751  numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
752  code_blockt body{};
753 
754  for(std::size_t index = 0; index < array_size; index++)
755  {
756  initialize(
758  depth,
759  body);
760  }
761  return body;
762 }
763 
765  const exprt &depth,
766  const symbol_exprt &result)
767 {
768  PRECONDITION(result.type().id() == ID_pointer);
769  const typet &struct_type = result.type().subtype();
770  PRECONDITION(struct_type.id() == ID_struct_tag);
771  code_blockt body{};
773  for(const auto &component :
774  ns.follow_tag(to_struct_tag_type(struct_type)).components())
775  {
776  if(component.get_is_padding())
777  {
778  continue;
779  }
780  // if the struct component is const we need to cast away the const
781  // for initialisation purposes.
782  // As far as I'm aware that's the closest thing to a 'correct' way
783  // to initialize dynamically allocated structs with const components
784  exprt component_initialisation_lhs = [&result, &component]() -> exprt {
785  auto member_expr = member_exprt{dereference_exprt{result}, component};
786  if(component.type().get_bool(ID_C_constant))
787  {
788  return dereference_exprt{
789  typecast_exprt{address_of_exprt{std::move(member_expr)},
791  }
792  else
793  {
794  return std::move(member_expr);
795  }
796  }();
797  initialize(component_initialisation_lhs, depth, body);
798  }
799  return body;
800 }
801 
803  const symbol_exprt &result) const
804 {
805  PRECONDITION(result.type().id() == ID_pointer);
806  code_blockt body{};
807  auto const nondet_symbol =
808  get_fresh_local_typed_symexpr("nondet", result.type().subtype());
809  body.add(code_declt{nondet_symbol});
810  body.add(code_assignt{dereference_exprt{result}, nondet_symbol});
811  return body;
812 }
813 
815  const exprt &depth,
816  const symbol_exprt &result,
817  const exprt &size,
818  const optionalt<irep_idt> &lhs_name)
819 {
820  PRECONDITION(result.type().id() == ID_pointer);
821  const typet &dynamic_array_type = result.type().subtype();
822  PRECONDITION(dynamic_array_type.id() == ID_pointer);
823  const typet &element_type = dynamic_array_type.subtype();
824  PRECONDITION(element_type.id() != ID_empty);
825 
826  // builds:
827  // void type_constructor_ptr_T(int depth, T** result, int* size)
828  // {
829  // int nondet_size;
830  // assume(nondet_size >= min_array_size && nondet_size <= max_array_size);
831  // T* local_result = malloc(nondet_size * sizeof(T));
832  // for (int i = 0; i < nondet_size; ++i)
833  // {
834  // type_construct_T(depth+1, local_result+i);
835  // }
836  // *result = local_result;
837  // if (size!=NULL)
838  // *size = nondet_size;
839  // }
840 
841  const auto min_array_size = initialization_config.min_dynamic_array_size;
842  const auto max_array_size = initialization_config.max_dynamic_array_size;
843  PRECONDITION(max_array_size >= min_array_size);
844 
845  code_blockt body{};
846  const symbol_exprt &nondet_size = get_fresh_local_symexpr("nondet_size");
847  body.add(code_declt{nondet_size});
848 
849  body.add(code_assumet{and_exprt{
851  nondet_size, ID_ge, from_integer(min_array_size, nondet_size.type())},
853  nondet_size, ID_le, from_integer(max_array_size, nondet_size.type())}}});
854 
855  // we want the local result to be mutable so we can initialise it
856  const typet mutable_dynamic_array_type =
857  pointer_type(remove_const(element_type));
858  const symbol_exprt &local_result =
859  get_fresh_local_typed_symexpr("local_result", mutable_dynamic_array_type);
860  body.add(code_declt{local_result});
862  for(auto array_size = min_array_size; array_size <= max_array_size;
863  ++array_size)
864  {
865  body.add(code_ifthenelset{
866  equal_exprt{nondet_size, from_integer(array_size, nondet_size.type())},
867  code_function_callt{local_result,
869  {mult_exprt{from_integer(array_size, size_type()),
870  *size_of_expr(element_type, ns)}}}});
871  }
872 
873  const symbol_exprt &index_iter = get_fresh_local_symexpr("index");
874  body.add(code_declt{index_iter});
875  code_assignt for_init{index_iter, from_integer(0, index_iter.type())};
876  binary_relation_exprt for_cond{index_iter, ID_lt, nondet_size};
877  side_effect_exprt for_iter{
878  ID_preincrement, {index_iter}, typet{}, source_locationt{}};
879  code_blockt for_body{};
880  if(lhs_name.has_value() && should_be_treated_as_cstring(*lhs_name))
881  {
882  code_blockt else_case{};
883  initialize(
884  dereference_exprt{plus_exprt{local_result, index_iter}},
885  plus_exprt{depth, from_integer(1, depth.type())},
886  else_case);
887  else_case.add(code_assumet{
888  notequal_exprt{dereference_exprt{plus_exprt{local_result, index_iter}},
889  from_integer(0, char_type())}});
890 
891  for_body.add(code_ifthenelset{
892  equal_exprt{
893  index_iter,
894  minus_exprt{nondet_size, from_integer(1, nondet_size.type())}},
895  code_assignt{dereference_exprt{plus_exprt{local_result, index_iter}},
896  from_integer(0, char_type())},
897  else_case});
898  }
899  else
900  {
901  initialize(
902  dereference_exprt{plus_exprt{local_result, index_iter}},
903  plus_exprt{depth, from_integer(1, depth.type())},
904  for_body);
905  }
906 
907  body.add(code_fort{for_init, for_cond, for_iter, for_body});
908  body.add(code_assignt{dereference_exprt{result}, local_result});
909 
910  CHECK_RETURN(size.type().id() == ID_pointer);
911  body.add(code_ifthenelset{
913  code_assignt{
914  dereference_exprt{size},
915  typecast_exprt::conditional_cast(nondet_size, size.type().subtype())}});
916 
917  return body;
918 }
919 
921 {
922  if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code)
923  return false;
924  for(auto const &common_arguments_origin : common_arguments_origins)
925  {
926  if(common_arguments_origin.has_value() && expr.id() == ID_symbol)
927  {
928  auto origin_name =
929  to_symbol_expr(*common_arguments_origin).get_identifier();
930  auto expr_name = to_symbol_expr(expr).get_identifier();
931  return origin_name == expr_name;
932  }
933  }
934  return true;
935 }
936 
938  const exprt &expr,
939  code_blockt &body)
940 {
941  PRECONDITION(expr.id() == ID_symbol);
942  const auto expr_id = to_symbol_expr(expr).get_identifier();
943  const auto maybe_cluster_index = find_equal_cluster(expr_id);
944  const auto call_free = code_function_callt{get_free_function(), {expr}};
945  if(!maybe_cluster_index.has_value())
946  {
947  // not in any equality cluster -> just free
948  body.add(call_free);
949  return;
950  }
951 
952  if(
953  to_symbol_expr(*common_arguments_origins[*maybe_cluster_index])
954  .get_identifier() != expr_id &&
956  {
957  // in equality cluster but not common origin -> free if not equal to origin
958  const auto condition =
959  notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]};
960  body.add(code_ifthenelset{condition, call_free});
961  }
962  else
963  {
964  // expr is common origin, leave freeing until the rest of the cluster is
965  // freed
966  return;
967  }
968 }
969 
971 {
972  for(auto const &origin : common_arguments_origins)
973  {
974  body.add(code_function_callt{get_free_function(), {*origin}});
975  }
976 }
977 
979  const symbol_exprt &result,
980  bool is_nullable)
981 {
983  const auto &result_type = to_pointer_type(result.type());
984  PRECONDITION(can_cast_type<pointer_typet>(result_type.subtype()));
985  const auto &function_pointer_type = to_pointer_type(result_type.subtype());
986  PRECONDITION(can_cast_type<code_typet>(function_pointer_type.subtype()));
987  const auto &function_type = to_code_type(function_pointer_type.subtype());
988 
989  std::vector<exprt> targets;
990 
991  for(const auto &sym : goto_model.get_symbol_table())
992  {
993  if(sym.second.type == function_type)
994  {
995  targets.push_back(address_of_exprt{sym.second.symbol_expr()});
996  }
997  }
998 
999  if(is_nullable)
1000  targets.push_back(null_pointer_exprt{function_pointer_type});
1001 
1002  code_blockt body{};
1003 
1004  const auto function_pointer_selector =
1005  get_fresh_local_symexpr("function_pointer_selector");
1006  body.add(code_declt{function_pointer_selector});
1007  auto function_pointer_index = std::size_t{0};
1008 
1009  for(const auto &target : targets)
1010  {
1011  auto const assign = code_assignt{dereference_exprt{result}, target};
1012  auto const sym_to_lookup =
1013  target.id() == ID_address_of
1014  ?
1015  // This is either address of or pointer; in pointer case, we don't
1016  // need to do anything. In the address of case, the operand is
1017  // a symbol representing a target function.
1019  : "";
1020  // skip referencing globals because the corresponding symbols in the symbol
1021  // table are no longer marked as file local.
1022  if(has_prefix(id2string(sym_to_lookup), FILE_LOCAL_PREFIX))
1023  {
1024  continue;
1025  }
1026  else if(
1027  goto_model.get_symbol_table().lookup(sym_to_lookup) &&
1028  goto_model.get_symbol_table().lookup(sym_to_lookup)->is_file_local)
1029  {
1030  continue;
1031  }
1032 
1033  if(function_pointer_index != targets.size() - 1)
1034  {
1035  auto const condition = equal_exprt{
1036  function_pointer_selector,
1037  from_integer(function_pointer_index, function_pointer_selector.type())};
1038  auto const then = code_blockt{{assign, code_returnt{}}};
1039  body.add(code_ifthenelset{condition, then});
1040  }
1041  else
1042  {
1043  body.add(assign);
1044  }
1045  ++function_pointer_index;
1046  }
1047 
1048  return body;
1049 }
1050 
1052  const exprt &lhs,
1053  const exprt &depth,
1054  code_blockt &body,
1055  const std::vector<irep_idt> &selection_spec)
1056 {
1057  PRECONDITION(lhs.id() == ID_symbol);
1058  PRECONDITION(lhs.type().id() == ID_struct_tag);
1059  PRECONDITION(!selection_spec.empty());
1060 
1061  auto component_member = lhs;
1063 
1064  for(auto it = selection_spec.begin() + 1; it != selection_spec.end(); it++)
1065  {
1066  if(component_member.type().id() != ID_struct_tag)
1067  {
1069  "'" + id2string(*it) + "' is not a component name",
1071  }
1072  const auto &struct_tag_type = to_struct_tag_type(component_member.type());
1073  const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
1074 
1075  bool found = false;
1076  for(auto const &component : struct_type.components())
1077  {
1078  const auto &component_type = component.type();
1079  const auto component_name = component.get_name();
1080 
1081  if(*it == component_name)
1082  {
1083  component_member =
1084  member_exprt{component_member, component_name, component_type};
1085  found = true;
1086  break;
1087  }
1088  }
1089  if(!found)
1090  {
1092  "'" + id2string(*it) + "' is not a component name",
1094  }
1095  }
1096  initialize(component_member, depth, body);
1097 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
recursive_initialization_configt::pointers_to_treat_as_cstrings
std::set< irep_idt > pointers_to_treat_as_cstrings
Definition: recursive_initialization.h:41
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:170
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
Definition: common_harness_generator_options.h:17
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
recursive_initializationt::get_fresh_local_typed_symexpr
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.
Definition: recursive_initialization.cpp:541
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
recursive_initializationt::min_depth_var_name
irep_idt min_depth_var_name
Definition: recursive_initialization.h:124
arith_tools.h
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:742
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
recursive_initializationt::goto_model
goto_modelt & goto_model
Definition: recursive_initialization.h:122
get_new_name
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
Definition: rename.cpp:19
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:598
code_fort
codet representation of a for statement.
Definition: std_code.h:1020
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
recursive_initialization.h
fresh_symbol.h
Fresh auxiliary symbol creation.
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:288
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:1051
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
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:374
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
recursive_initializationt::get_associated_size_variable
optionalt< irep_idt > get_associated_size_variable(const irep_idt &array_name) const
Definition: recursive_initialization.cpp:419
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:526
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT
#define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT
Definition: common_harness_generator_options.h:19
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
FILE_LOCAL_PREFIX
#define FILE_LOCAL_PREFIX
Definition: name_mangler.h:16
and_exprt
Boolean AND.
Definition: std_expr.h:2137
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
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:39
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
recursive_initialization_configt::selection_specs
std::vector< std::vector< irep_idt > > selection_specs
Definition: recursive_initialization.h:46
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
bool_typet
The Boolean type.
Definition: std_types.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
harness_options_parser::require_exactly_one_value
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...
Definition: goto_harness_generator.cpp:21
recursive_initialization_configt::mode
irep_idt mode
Definition: recursive_initialization.h:30
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
equal_exprt
Equality.
Definition: std_expr.h:1190
recursive_initializationt::free_cluster_origins
void free_cluster_origins(code_blockt &body)
Definition: recursive_initialization.cpp:970
recursive_initializationt::is_array_size_parameter
bool is_array_size_parameter(const irep_idt &cmdline_arg) const
Definition: recursive_initialization.cpp:411
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:136
recursive_initializationt::find_equal_cluster
optionalt< equal_cluster_idt > find_equal_cluster(const irep_idt &name) const
Definition: recursive_initialization.cpp:399
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
notequal_exprt
Disequality.
Definition: std_expr.h:1248
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:978
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
recursive_initializationt::constructor_keyt
Definition: recursive_initialization.h:68
recursive_initialization_configt::pointers_to_treat_as_arrays
std::set< irep_idt > pointers_to_treat_as_arrays
Definition: recursive_initialization.h:37
recursive_initializationt::should_be_treated_as_array
bool should_be_treated_as_array(const irep_idt &pointer_name) const
Definition: recursive_initialization.cpp:391
array_typet::size
const exprt & size() const
Definition: std_types.h:973
remove_const
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
recursive_initializationt::needs_freeing
bool needs_freeing(const exprt &expr) const
Definition: recursive_initialization.cpp:920
recursive_initialization_configt::max_nondet_tree_depth
std::size_t max_nondet_tree_depth
Definition: recursive_initialization.h:29
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:579
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
build_null_pointer
code_blockt build_null_pointer(const symbol_exprt &result_symbol)
Definition: recursive_initialization.cpp:234
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
can_cast_type< code_typet >
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:933
recursive_initialization_configt::max_dynamic_array_size
std::size_t max_dynamic_array_size
Definition: recursive_initialization.h:34
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
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
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
rename.h
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:648
recursive_initialization_configt::arguments_may_be_equal
bool arguments_may_be_equal
Definition: recursive_initialization.h:44
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
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:31
can_cast_type< struct_tag_typet >
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
Definition: std_types.h:502
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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:514
recursive_initializationt::type_constructor_names
type_constructor_namest type_constructor_names
Definition: recursive_initialization.h:125
optional_utils.h
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
optional_lookup
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.
Definition: optional_utils.h:17
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:96
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
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:814
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
irept::id
const irep_idt & id() const
Definition: irep.h:418
COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT
#define COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT
Definition: common_harness_generator_options.h:13
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
recursive_initializationt::recursive_initializationt
recursive_initializationt(recursive_initialization_configt initialization_config, goto_modelt &goto_model)
Definition: recursive_initialization.cpp:116
GOTO_HARNESS_PREFIX
#define GOTO_HARNESS_PREFIX
Definition: recursive_initialization.h:25
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:557
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
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:501
std_code.h
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:126
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:28
minus_exprt
Binary minus.
Definition: std_expr.h:940
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
source_locationt
Definition: source_location.h:20
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:243
recursive_initializationt::free_if_possible
void free_if_possible(const exprt &expr, code_blockt &body)
Definition: recursive_initialization.cpp:937
recursive_initialization_configt::variables_that_hold_array_sizes
std::set< irep_idt > variables_that_hold_array_sizes
Definition: recursive_initialization.h:38
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1513
recursive_initializationt::should_be_treated_as_cstring
bool should_be_treated_as_cstring(const irep_idt &pointer_name) const
Definition: recursive_initialization.cpp:427
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
array_typet
Arrays with given size.
Definition: std_types.h:965
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
recursive_initializationt::type2id
std::string type2id(const typet &type) const
Simple pretty-printer for typet.
Definition: recursive_initialization.cpp:605
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
Definition: common_harness_generator_options.h:15
recursive_initialization_configt::min_dynamic_array_size
std::size_t min_dynamic_array_size
Definition: recursive_initialization.h:35
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:631
harness_options_parser::require_one_size_value
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...
Definition: goto_harness_generator.cpp:41
goto_modelt::get_symbol_table
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:77
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:67
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
code_typet::parametert
Definition: std_types.h:753
recursive_initialization_configt
Definition: recursive_initialization.h:27
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:28
recursive_initializationt::equal_cluster_idt
std::size_t equal_cluster_idt
Definition: recursive_initialization.h:66
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
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:802
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
r
static int8_t r
Definition: irep_hash.h:59
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT
#define COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT
Definition: common_harness_generator_options.h:12
get_fresh_global_symbol
static symbolt & get_fresh_global_symbol(symbol_tablet &symbol_table, const std::string &symbol_base_name, typet symbol_type, irep_idt mode)
Definition: recursive_initialization.cpp:474
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
Definition: common_harness_generator_options.h:16
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
recursive_initialization_configt::to_string
std::string to_string() const
Definition: recursive_initialization.cpp:434
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
recursive_initializationt::initialization_config
const recursive_initialization_configt initialization_config
Definition: recursive_initialization.h:121
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
std_expr.h
API to expression classes.
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
allocate_objects.h
c_types.h
get_fresh_aux_symbol
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 ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
name_mangler.h
Mangle names of file-local functions to make them unique.
recursive_initializationt::max_depth_var_name
irep_idt max_depth_var_name
Definition: recursive_initialization.h:123
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
validation_modet::INVARIANT
@ INVARIANT
irep.h
recursive_initialization_configt::pointers_to_treat_equal
std::vector< std::set< irep_idt > > pointers_to_treat_equal
Definition: recursive_initialization.h:42
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:764
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939