cprover
recursive_initialization.cpp
Go to the documentation of this file.
1/******************************************************************\
2
3Module: recursive_initialization
4
5Author: 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
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",
126 initialization_config.max_nondet_tree_depth,
127 signed_int_type()))),
128 min_depth_var_name(get_fresh_global_name(
129 "min_depth",
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});
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)};
241 nullptr_expr};
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};
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,
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(
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
604std::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
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)}});
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 {
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 {
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{};
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{
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 {
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{
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) &&
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 code_assignt assign_null(const exprt &expr)
One of the base cases of the recursive algorithm.
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:542
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.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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...
STL namespace.
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
static symbolt & get_fresh_global_symbol(symbol_tablet &symbol_table, const std::string &symbol_base_name, typet symbol_type, irep_idt mode)
code_blockt build_null_pointer(const symbol_exprt &result_symbol)
#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 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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
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