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 
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>
18 #include <util/pointer_expr.h>
20 #include <util/rename.h>
21 #include <util/std_code.h>
22 #include <util/string2int.h>
23 #include <util/string_utils.h>
24 
25 #include <iterator>
26 
28 #include "goto_harness_generator.h"
29 
31  const std::string &option,
32  const std::list<std::string> &values)
33 {
35  {
36  auto const value =
38  auto const user_min_null_tree_depth =
39  string2optional<std::size_t>(value, 10);
40  if(user_min_null_tree_depth.has_value())
41  {
42  min_null_tree_depth = user_min_null_tree_depth.value();
43  }
44  else
45  {
47  "failed to convert '" + value + "' to integer",
49  }
50  return true;
51  }
53  {
54  auto const value =
56  auto const user_max_nondet_tree_depth =
57  string2optional<std::size_t>(value, 10);
58  if(user_max_nondet_tree_depth.has_value())
59  {
60  max_nondet_tree_depth = user_max_nondet_tree_depth.value();
61  }
62  else
63  {
65  "failed to convert '" + value + "' to integer",
67  }
68  return true;
69  }
71  {
74  return true;
75  }
77  {
80  return true;
81  }
83  {
85  values.begin(),
86  values.end(),
87  std::inserter(
90  [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
91  return true;
92  }
94  {
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)
100  {
101  const auto selection_spec_strings = split_string(member, '.');
102 
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};
111  });
112  }
113  return true;
114  }
115  return false;
116 }
117 
119  recursive_initialization_configt initialization_config,
120  goto_modelt &goto_model)
121  : initialization_config(std::move(initialization_config)),
122  goto_model(goto_model),
123  max_depth_var_name(get_fresh_global_name(
124  "max_depth",
125  from_integer(
126  initialization_config.max_nondet_tree_depth,
127  signed_int_type()))),
128  min_depth_var_name(get_fresh_global_name(
129  "min_depth",
130  from_integer(
131  initialization_config.min_null_tree_depth,
132  signed_int_type())))
133 {
135  this->initialization_config.pointers_to_treat_equal.size());
136 }
137 
139  const exprt &lhs,
140  const exprt &depth,
141  code_blockt &body)
142 {
143  if(lhs.id() == ID_symbol && !initialization_config.selection_specs.empty())
144  {
145  auto lhs_id = to_symbol_expr(lhs).get_identifier();
146  for(const auto &selection_spec : initialization_config.selection_specs)
147  {
148  if(selection_spec.front() == lhs_id)
149  {
150  initialize_selected_member(lhs, depth, body, selection_spec);
151  return;
152  }
153  }
154  }
155  // special handling for the case that pointer arguments should be treated
156  // equal: if the equality is enforced (rather than the pointers may be equal),
157  // then we don't even build the constructor functions
158  if(lhs.id() == ID_symbol)
159  {
160  const auto maybe_cluster_index =
162  if(maybe_cluster_index.has_value())
163  {
164  if(common_arguments_origins[*maybe_cluster_index].has_value())
165  {
166  const auto set_equal_case =
167  code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]};
169  {
170  const irep_idt &fun_name = build_constructor(lhs);
171  const symbolt &fun_symbol =
173  const auto proper_init_case = code_function_callt{
174  fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}}};
175  const auto should_make_equal =
176  get_fresh_local_typed_symexpr("should_make_equal", bool_typet{});
177  body.add(code_declt{should_make_equal});
178  body.add(code_ifthenelset{
179  should_make_equal, set_equal_case, proper_init_case});
180  }
181  else
182  {
183  body.add(set_equal_case);
184  }
185  return;
186  }
187  else
188  {
189  common_arguments_origins[*maybe_cluster_index] = lhs;
190  }
191  }
192  }
193 
194  const irep_idt &fun_name = build_constructor(lhs);
195  const symbolt &fun_symbol = goto_model.symbol_table.lookup_ref(fun_name);
196 
197  if(lhs.id() == ID_symbol)
198  {
199  const irep_idt &lhs_name = to_symbol_expr(lhs).get_identifier();
200  if(should_be_treated_as_array(lhs_name))
201  {
202  auto size_var = get_associated_size_variable(lhs_name);
203  if(size_var.has_value())
204  {
205  const symbol_exprt &size_symbol =
206  goto_model.symbol_table.lookup_ref(size_var.value()).symbol_expr();
208  fun_symbol.symbol_expr(),
209  {depth, address_of_exprt{lhs}, address_of_exprt{size_symbol}}});
210  }
211  else
212  {
213  const auto &fun_type_params =
214  to_code_type(fun_symbol.type).parameters();
215  const pointer_typet *size_var_type =
216  type_try_dynamic_cast<pointer_typet>(fun_type_params.back().type());
217  INVARIANT(size_var_type, "Size parameter must have pointer type.");
219  fun_symbol.symbol_expr(),
220  {depth, address_of_exprt{lhs}, null_pointer_exprt{*size_var_type}}});
221  }
222  return;
223  }
224  for(const auto &irep_pair :
226  {
227  // skip initialisation of array-size variables
228  if(irep_pair.second == lhs_name)
229  return;
230  }
231  }
232  body.add(code_function_callt{fun_symbol.symbol_expr(),
233  {depth, address_of_exprt{lhs}}});
234 }
235 
237 {
238  const typet &type_to_construct = result_symbol.type().subtype();
239  const null_pointer_exprt nullptr_expr{to_pointer_type(type_to_construct)};
240  const code_assignt assign_null{dereference_exprt{result_symbol},
241  nullptr_expr};
242  return code_blockt{{assign_null, code_frontend_returnt{}}};
243 }
244 
246  const exprt &depth_symbol,
248  const optionalt<exprt> &size_symbol,
249  const optionalt<irep_idt> &lhs_name,
250  const bool is_nullable)
251 {
252  PRECONDITION(result_symbol.type().id() == ID_pointer);
253  const typet &type = result_symbol.type().subtype();
254  if(type.id() == ID_struct_tag)
255  {
256  return build_struct_constructor(depth_symbol, result_symbol);
257  }
258  else if(type.id() == ID_pointer)
259  {
260  if(type.subtype().id() == ID_code)
261  {
263  }
264  if(type.subtype().id() == ID_empty)
265  {
266  // always initalize void* pointers as NULL
268  }
269  if(lhs_name.has_value())
270  {
271  if(should_be_treated_as_array(*lhs_name))
272  {
273  CHECK_RETURN(size_symbol.has_value());
275  depth_symbol, result_symbol, *size_symbol, lhs_name);
276  }
277  }
278  return build_pointer_constructor(depth_symbol, result_symbol);
279  }
280  else if(type.id() == ID_array)
281  {
282  return build_array_constructor(depth_symbol, result_symbol);
283  }
284  else
285  {
287  }
288 }
289 
291 {
292  // for `expr` of type T builds a declaration of a function:
293  //
294  // void type_constructor_T(int depth_T, T *result);
295  //
296  // or in case a `size` is associated with the `expr`
297  //
298  // void type_constructor_T(int depth_T, T *result_T, int *size);
299  optionalt<irep_idt> size_var;
300  optionalt<irep_idt> expr_name;
301  bool is_nullable = false;
302  bool has_size_param = false;
303  if(expr.id() == ID_symbol)
304  {
305  expr_name = to_symbol_expr(expr).get_identifier();
307  expr_name.value());
308  if(should_be_treated_as_array(*expr_name))
309  {
310  size_var = get_associated_size_variable(*expr_name);
311  has_size_param = true;
312  }
313  }
314  const typet &type = expr.type();
315  const constructor_keyt key{type, is_nullable, has_size_param};
316  if(type_constructor_names.find(key) != type_constructor_names.end())
317  return type_constructor_names[key];
318 
319  const std::string &pretty_type = type2id(type);
320  symbolt &depth_symbol =
321  get_fresh_param_symbol("depth_" + pretty_type, signed_int_type());
322  depth_symbol.value = from_integer(0, signed_int_type());
323 
324  code_typet::parameterst fun_params;
325  code_typet::parametert depth_parameter{signed_int_type()};
326  depth_parameter.set_identifier(depth_symbol.name);
327  fun_params.push_back(depth_parameter);
328 
329  const typet &result_type = pointer_type(type);
330  const symbolt &result_symbol =
331  get_fresh_param_symbol("result_" + pretty_type, result_type);
332  code_typet::parametert result_parameter{result_type};
333  result_parameter.set_identifier(result_symbol.name);
334  fun_params.push_back(result_parameter);
335 
336  auto &symbol_table = goto_model.symbol_table;
337  optionalt<exprt> size_symbol_expr;
338  if(expr_name.has_value() && should_be_treated_as_array(*expr_name))
339  {
340  typet size_var_type;
341  if(size_var.has_value())
342  {
343  const symbol_exprt &size_var_symbol_expr =
344  symbol_table.lookup_ref(*size_var).symbol_expr();
345  size_var_type = pointer_type(size_var_symbol_expr.type());
346  }
347  else
348  size_var_type = pointer_type(signed_int_type());
349 
350  const symbolt &size_symbol =
351  get_fresh_param_symbol("size_" + pretty_type, size_var_type);
352  fun_params.push_back(code_typet::parametert{size_var_type});
353  fun_params.back().set_identifier(size_symbol.name);
354  size_symbol_expr = size_symbol.symbol_expr();
355  }
356  const symbolt &function_symbol = get_fresh_fun_symbol(
357  "type_constructor_" + pretty_type, code_typet{fun_params, empty_typet{}});
358  type_constructor_names[key] = function_symbol.name;
359  symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.name);
360 
361  // the body is specific for each type of expression
362  mutable_symbol->value = build_constructor_body(
363  depth_symbol.symbol_expr(),
365  size_symbol_expr,
366  // the expression name may be needed to decide if expr should be treated as
367  // a string
368  expr_name,
369  is_nullable);
370 
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 =
563 
564  // create the function symbol
565  symbolt function_symbol{};
566  function_symbol.name = function_symbol.base_name =
567  function_symbol.pretty_name = fresh_name;
568 
569  function_symbol.is_lvalue = true;
570  function_symbol.mode = initialization_config.mode;
571  function_symbol.type = fun_type;
572 
573  auto r = goto_model.symbol_table.insert(function_symbol);
574  CHECK_RETURN(r.second);
575  return *goto_model.symbol_table.lookup(fresh_name);
576 }
577 
579  const std::string &symbol_name,
580  const typet &symbol_type)
581 {
582  symbolt &param_symbol = get_fresh_aux_symbol(
583  symbol_type,
585  symbol_name,
589  param_symbol.is_parameter = true;
590  param_symbol.is_lvalue = true;
591  param_symbol.mode = initialization_config.mode;
592 
593  return param_symbol;
594 }
595 
598 {
599  auto maybe_symbol = goto_model.symbol_table.lookup(symbol_name);
600  CHECK_RETURN(maybe_symbol != nullptr);
601  return maybe_symbol->symbol_expr();
602 }
603 
604 std::string recursive_initializationt::type2id(const typet &type) const
605 {
606  if(type.id() == ID_struct_tag)
607  {
608  auto st_tag = id2string(to_struct_tag_type(type).get_identifier());
609  std::replace(st_tag.begin(), st_tag.end(), '-', '_');
610  return st_tag;
611  }
612  else if(type.id() == ID_pointer)
613  return "ptr_" + type2id(type.subtype());
614  else if(type.id() == ID_array)
615  {
616  const auto array_size =
617  numeric_cast_v<std::size_t>(to_constant_expr(to_array_type(type).size()));
618  return "arr_" + type2id(type.subtype()) + "_" + std::to_string(array_size);
619  }
620  else if(type == char_type())
621  return "char";
622  else if(type.id() == ID_signedbv)
623  return "int";
624  else if(type.id() == ID_unsignedbv)
625  return "uint";
626  else
627  return "";
628 }
629 
631 {
632  auto free_sym = goto_model.symbol_table.lookup("free");
633  if(free_sym == nullptr)
634  {
635  symbolt new_free_sym;
636  new_free_sym.type = code_typet{code_typet{
638  new_free_sym.name = new_free_sym.pretty_name = new_free_sym.base_name =
639  "free";
640  new_free_sym.mode = initialization_config.mode;
641  goto_model.symbol_table.insert(new_free_sym);
642  return new_free_sym.symbol_expr();
643  }
644  return free_sym->symbol_expr();
645 }
646 
648  const exprt &depth,
649  const symbol_exprt &result)
650 {
651  PRECONDITION(result.type().id() == ID_pointer);
652  const typet &type = result.type().subtype();
653  PRECONDITION(type.id() == ID_pointer);
654  PRECONDITION(type.subtype().id() != ID_empty);
655 
656  code_blockt body{};
657  // build:
658  // void type_constructor_ptr_T(int depth, T** result)
659  // {
660  // if(has_seen && depth >= max_depth)
661  // *result=NULL;
662  // return
663  // if(nondet()) {
664  // size_t has_seen_prev;
665  // has_seen_prev = T_has_seen;
666  // T_has_seen = 1;
667  // *result = malloc(sizeof(T));
668  // type_constructor_T(depth+1, *result);
669  // T_has_seen=has_seen_prev;
670  // }
671  // else
672  // *result=NULL;
673  // }
674 
675  binary_predicate_exprt depth_gt_max_depth{
676  depth, ID_ge, get_symbol_expr(max_depth_var_name)};
677  exprt::operandst should_not_recurse{depth_gt_max_depth};
678 
679  optionalt<symbol_exprt> has_seen;
681  has_seen = get_fresh_global_symexpr("has_seen_" + type2id(type.subtype()));
682 
683  if(has_seen.has_value())
684  {
685  equal_exprt has_seen_expr{*has_seen, from_integer(1, has_seen->type())};
686  should_not_recurse.push_back(has_seen_expr);
687  }
688 
689  null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
690  const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
691  code_blockt null_and_return{{assign_null, code_frontend_returnt{}}};
692  body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
693 
694  const auto should_recurse_nondet =
695  get_fresh_local_typed_symexpr("should_recurse_nondet", bool_typet{});
696  body.add(code_declt{should_recurse_nondet});
697  exprt::operandst should_recurse_ops{
699  should_recurse_nondet};
700  code_blockt then_case{};
701 
702  code_assignt seen_assign_prev{};
703  if(has_seen.has_value())
704  {
705  const symbol_exprt &has_seen_prev =
706  get_fresh_local_symexpr("has_seen_prev_" + type2id(type.subtype()));
707  then_case.add(code_declt{has_seen_prev});
708  then_case.add(code_assignt{has_seen_prev, *has_seen});
709  then_case.add(code_assignt{*has_seen, from_integer(1, has_seen->type())});
710  seen_assign_prev = code_assignt{*has_seen, has_seen_prev};
711  }
712 
713  // we want to initialize the pointee as non-const even for pointer to const
714  const typet non_const_pointer_type =
716  const symbol_exprt &local_result =
717  get_fresh_local_typed_symexpr("local_result", non_const_pointer_type);
718 
719  then_case.add(code_declt{local_result});
721  then_case.add(
722  code_function_callt{local_result,
724  {*size_of_expr(non_const_pointer_type.subtype(), ns)}});
725  initialize(
726  dereference_exprt{local_result},
727  plus_exprt{depth, from_integer(1, depth.type())},
728  then_case);
729  then_case.add(code_assignt{dereference_exprt{result}, local_result});
730 
731  if(has_seen.has_value())
732  {
733  then_case.add(seen_assign_prev);
734  }
735 
736  body.add(
737  code_ifthenelset{disjunction(should_recurse_ops), then_case, assign_null});
738  return body;
739 }
740 
742  const exprt &depth,
743  const symbol_exprt &result)
744 {
745  PRECONDITION(result.type().id() == ID_pointer);
746  const typet &type = result.type().subtype();
747  PRECONDITION(type.id() == ID_array);
748  const array_typet &array_type = to_array_type(type);
749  const auto array_size =
750  numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
751  code_blockt body{};
752 
753  for(std::size_t index = 0; index < array_size; index++)
754  {
755  initialize(
757  depth,
758  body);
759  }
760  return body;
761 }
762 
764  const exprt &depth,
765  const symbol_exprt &result)
766 {
767  PRECONDITION(result.type().id() == ID_pointer);
768  const typet &struct_type = result.type().subtype();
769  PRECONDITION(struct_type.id() == ID_struct_tag);
770  code_blockt body{};
772  for(const auto &component :
773  ns.follow_tag(to_struct_tag_type(struct_type)).components())
774  {
775  if(component.get_is_padding())
776  {
777  continue;
778  }
779  // if the struct component is const we need to cast away the const
780  // for initialisation purposes.
781  // As far as I'm aware that's the closest thing to a 'correct' way
782  // to initialize dynamically allocated structs with const components
783  exprt component_initialisation_lhs = [&result, &component]() -> exprt {
784  auto member_expr = member_exprt{dereference_exprt{result}, component};
785  if(component.type().get_bool(ID_C_constant))
786  {
787  return dereference_exprt{
788  typecast_exprt{address_of_exprt{std::move(member_expr)},
790  }
791  else
792  {
793  return std::move(member_expr);
794  }
795  }();
796  initialize(component_initialisation_lhs, depth, body);
797  }
798  return body;
799 }
800 
802  const symbol_exprt &result) const
803 {
804  PRECONDITION(result.type().id() == ID_pointer);
805  code_blockt body{};
806  auto const nondet_symbol =
807  get_fresh_local_typed_symexpr("nondet", result.type().subtype());
808  body.add(code_declt{nondet_symbol});
809  body.add(code_assignt{dereference_exprt{result}, nondet_symbol});
810  return body;
811 }
812 
814  const exprt &depth,
815  const symbol_exprt &result,
816  const exprt &size,
817  const optionalt<irep_idt> &lhs_name)
818 {
819  PRECONDITION(result.type().id() == ID_pointer);
820  const typet &dynamic_array_type = result.type().subtype();
821  PRECONDITION(dynamic_array_type.id() == ID_pointer);
822  const typet &element_type = dynamic_array_type.subtype();
823  PRECONDITION(element_type.id() != ID_empty);
824 
825  // builds:
826  // void type_constructor_ptr_T(int depth, T** result, int* size)
827  // {
828  // int nondet_size;
829  // assume(nondet_size >= min_array_size && nondet_size <= max_array_size);
830  // T* local_result = malloc(nondet_size * sizeof(T));
831  // for (int i = 0; i < nondet_size; ++i)
832  // {
833  // type_construct_T(depth+1, local_result+i);
834  // }
835  // *result = local_result;
836  // if (size!=NULL)
837  // *size = nondet_size;
838  // }
839 
840  const auto min_array_size = initialization_config.min_dynamic_array_size;
841  const auto max_array_size = initialization_config.max_dynamic_array_size;
842  PRECONDITION(max_array_size >= min_array_size);
843 
844  code_blockt body{};
845  const symbol_exprt &nondet_size = get_fresh_local_symexpr("nondet_size");
846  body.add(code_declt{nondet_size});
847 
848  body.add(code_assumet{and_exprt{
850  nondet_size, ID_ge, from_integer(min_array_size, nondet_size.type())},
852  nondet_size, ID_le, from_integer(max_array_size, nondet_size.type())}}});
853 
854  // we want the local result to be mutable so we can initialise it
855  const typet mutable_dynamic_array_type =
856  pointer_type(remove_const(element_type));
857  const symbol_exprt &local_result =
858  get_fresh_local_typed_symexpr("local_result", mutable_dynamic_array_type);
859  body.add(code_declt{local_result});
861  for(auto array_size = min_array_size; array_size <= max_array_size;
862  ++array_size)
863  {
864  body.add(code_ifthenelset{
865  equal_exprt{nondet_size, from_integer(array_size, nondet_size.type())},
866  code_function_callt{local_result,
868  {mult_exprt{from_integer(array_size, size_type()),
869  *size_of_expr(element_type, ns)}}}});
870  }
871 
872  const symbol_exprt &index_iter = get_fresh_local_symexpr("index");
873  body.add(code_declt{index_iter});
874  code_assignt for_init{index_iter, from_integer(0, index_iter.type())};
875  binary_relation_exprt for_cond{index_iter, ID_lt, nondet_size};
876  side_effect_exprt for_iter{
877  ID_preincrement, {index_iter}, typet{}, source_locationt{}};
878  code_blockt for_body{};
879  if(lhs_name.has_value() && should_be_treated_as_cstring(*lhs_name))
880  {
881  code_blockt else_case{};
882  initialize(
883  dereference_exprt{plus_exprt{local_result, index_iter}},
884  plus_exprt{depth, from_integer(1, depth.type())},
885  else_case);
886  else_case.add(code_assumet{
887  notequal_exprt{dereference_exprt{plus_exprt{local_result, index_iter}},
888  from_integer(0, char_type())}});
889 
890  for_body.add(code_ifthenelset{
891  equal_exprt{
892  index_iter,
893  minus_exprt{nondet_size, from_integer(1, nondet_size.type())}},
894  code_assignt{dereference_exprt{plus_exprt{local_result, index_iter}},
895  from_integer(0, char_type())},
896  else_case});
897  }
898  else
899  {
900  initialize(
901  dereference_exprt{plus_exprt{local_result, index_iter}},
902  plus_exprt{depth, from_integer(1, depth.type())},
903  for_body);
904  }
905 
906  body.add(code_fort{for_init, for_cond, for_iter, for_body});
907  body.add(code_assignt{dereference_exprt{result}, local_result});
908 
909  CHECK_RETURN(size.type().id() == ID_pointer);
910  body.add(code_ifthenelset{
912  code_assignt{
913  dereference_exprt{size},
914  typecast_exprt::conditional_cast(nondet_size, size.type().subtype())}});
915 
916  return body;
917 }
918 
920 {
921  if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code)
922  return false;
923  for(auto const &common_arguments_origin : common_arguments_origins)
924  {
925  if(common_arguments_origin.has_value() && expr.id() == ID_symbol)
926  {
927  auto origin_name =
928  to_symbol_expr(*common_arguments_origin).get_identifier();
929  auto expr_name = to_symbol_expr(expr).get_identifier();
930  return origin_name == expr_name;
931  }
932  }
933  return true;
934 }
935 
937  const exprt &expr,
938  code_blockt &body)
939 {
940  PRECONDITION(expr.id() == ID_symbol);
941  const auto expr_id = to_symbol_expr(expr).get_identifier();
942  const auto maybe_cluster_index = find_equal_cluster(expr_id);
943  const auto call_free = code_function_callt{get_free_function(), {expr}};
944  if(!maybe_cluster_index.has_value())
945  {
946  // not in any equality cluster -> just free
947  body.add(call_free);
948  return;
949  }
950 
951  if(
952  to_symbol_expr(*common_arguments_origins[*maybe_cluster_index])
953  .get_identifier() != expr_id &&
955  {
956  // in equality cluster but not common origin -> free if not equal to origin
957  const auto condition =
958  notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]};
959  body.add(code_ifthenelset{condition, call_free});
960  }
961  else
962  {
963  // expr is common origin, leave freeing until the rest of the cluster is
964  // freed
965  return;
966  }
967 }
968 
970 {
971  for(auto const &origin : common_arguments_origins)
972  {
973  body.add(code_function_callt{get_free_function(), {*origin}});
974  }
975 }
976 
978  const symbol_exprt &result,
979  bool is_nullable)
980 {
982  const auto &result_type = to_pointer_type(result.type());
983  PRECONDITION(can_cast_type<pointer_typet>(result_type.base_type()));
984  const auto &function_pointer_type = to_pointer_type(result_type.base_type());
985  PRECONDITION(can_cast_type<code_typet>(function_pointer_type.base_type()));
986  const auto &function_type = to_code_type(function_pointer_type.base_type());
987 
988  std::vector<exprt> targets;
989 
990  for(const auto &sym : goto_model.get_symbol_table())
991  {
992  if(sym.second.type == function_type)
993  {
994  targets.push_back(address_of_exprt{sym.second.symbol_expr()});
995  }
996  }
997 
998  if(is_nullable)
999  targets.push_back(null_pointer_exprt{function_pointer_type});
1000 
1001  code_blockt body{};
1002 
1003  const auto function_pointer_selector =
1004  get_fresh_local_symexpr("function_pointer_selector");
1005  body.add(code_declt{function_pointer_selector});
1006  auto function_pointer_index = std::size_t{0};
1007 
1008  for(const auto &target : targets)
1009  {
1010  auto const assign = code_assignt{dereference_exprt{result}, target};
1011  auto const sym_to_lookup =
1012  target.id() == ID_address_of
1013  ?
1014  // This is either address of or pointer; in pointer case, we don't
1015  // need to do anything. In the address of case, the operand is
1016  // a symbol representing a target function.
1018  : "";
1019  // skip referencing globals because the corresponding symbols in the symbol
1020  // table are no longer marked as file local.
1021  if(has_prefix(id2string(sym_to_lookup), FILE_LOCAL_PREFIX))
1022  {
1023  continue;
1024  }
1025  else if(
1026  goto_model.get_symbol_table().lookup(sym_to_lookup) &&
1027  goto_model.get_symbol_table().lookup(sym_to_lookup)->is_file_local)
1028  {
1029  continue;
1030  }
1031 
1032  if(function_pointer_index != targets.size() - 1)
1033  {
1034  auto const condition = equal_exprt{
1035  function_pointer_selector,
1036  from_integer(function_pointer_index, function_pointer_selector.type())};
1037  auto const then = code_blockt{{assign, code_frontend_returnt{}}};
1038  body.add(code_ifthenelset{condition, then});
1039  }
1040  else
1041  {
1042  body.add(assign);
1043  }
1044  ++function_pointer_index;
1045  }
1046 
1047  return body;
1048 }
1049 
1051  const exprt &lhs,
1052  const exprt &depth,
1053  code_blockt &body,
1054  const std::vector<irep_idt> &selection_spec)
1055 {
1056  PRECONDITION(lhs.id() == ID_symbol);
1057  PRECONDITION(lhs.type().id() == ID_struct_tag);
1058  PRECONDITION(!selection_spec.empty());
1059 
1060  auto component_member = lhs;
1062 
1063  for(auto it = selection_spec.begin() + 1; it != selection_spec.end(); it++)
1064  {
1065  if(component_member.type().id() != ID_struct_tag)
1066  {
1068  "'" + id2string(*it) + "' is not a component name",
1070  }
1071  const auto &struct_tag_type = to_struct_tag_type(component_member.type());
1072  const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
1073 
1074  bool found = false;
1075  for(auto const &component : struct_type.components())
1076  {
1077  const auto &component_type = component.type();
1078  const auto component_name = component.get_name();
1079 
1080  if(*it == component_name)
1081  {
1082  component_member =
1083  member_exprt{component_member, component_name, component_type};
1084  found = true;
1085  break;
1086  }
1087  }
1088  if(!found)
1089  {
1091  "'" + id2string(*it) + "' is not a component name",
1093  }
1094  }
1095  initialize(component_member, depth, body);
1096 }
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:19
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
unsignedbv_typet size_type()
Definition: c_types.cpp:68
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
bitvector_typet char_type()
Definition: c_types.cpp:124
Operator to return the address of an object.
Definition: pointer_expr.h:361
Boolean AND.
Definition: std_expr.h:1974
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition: std_code.h:217
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
A codet representing the declaration of a local variable.
codet representation of a for statement.
Definition: std_code.h:734
codet representation of a "return from a function" statement.
Definition: std_code.h:893
codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition: std_code.h:460
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const parameterst & parameters() const
Definition: std_types.h:655
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: goto_model.h:77
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
Array index operator.
Definition: std_expr.h:1328
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
Extract member of struct or union.
Definition: std_expr.h:2667
Binary minus.
Definition: std_expr.h:973
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Disequality.
Definition: std_expr.h:1283
The null pointer constant.
Definition: pointer_expr.h:723
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
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 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
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)
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 &param_name, const typet &param_type)
Construct a new parameter symbol of type param_type.
An expression containing a side effect.
Definition: std_code.h:1450
void set_file(const irep_idt &file)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_auxiliary
Definition: symbol.h:67
bool is_file_local
Definition: symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
bool is_parameter
Definition: symbol.h:67
bool is_thread_local
Definition: symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bool is_state_var
Definition: symbol.h:62
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
#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)
Definition: converter.cpp:13
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)
Definition: irep.h:47
static int8_t r
Definition: irep_hash.h:60
Mangle names of file-local functions to make them unique.
#define FILE_LOCAL_PREFIX
Definition: name_mangler.h:16
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
Definition: optional.h:35
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.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:66
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
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
irep_idt get_new_name(const irep_idt &name, const namespacet &ns, char delimiter)
Build and identifier not yet present in the namespace ns based on name.
Definition: rename.cpp:16
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:34
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:22
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
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:461
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:731
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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
std::set< irep_idt > variables_that_hold_array_sizes
std::set< irep_idt > pointers_to_treat_as_arrays
std::unordered_set< irep_idt > potential_null_function_pointers
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32