cprover
java_object_factory.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include <util/arith_tools.h>
14#include <util/fresh_symbol.h>
15#include <util/message.h>
16#include <util/nondet_bool.h>
17#include <util/prefix.h>
18
22
28#include "java_utils.h"
29#include "select_pointer_type.h"
30
32{
34
39 std::unordered_set<irep_idt> recursion_set;
40
50
53
58
60
63
65 code_blockt &assignments,
66 const exprt &expr,
67 const typet &target_type,
68 lifetimet lifetime,
69 size_t depth,
70 update_in_placet update_in_place,
71 const source_locationt &location);
72public:
74 const source_locationt &loc,
75 const java_object_factory_parameterst _object_factory_parameters,
76 symbol_table_baset &_symbol_table,
79 : object_factory_parameters(_object_factory_parameters),
80 symbol_table(_symbol_table),
83 ID_java,
84 loc,
85 object_factory_parameters.function_id,
87 log(log)
88 {}
89
91 code_blockt &assignments,
92 const exprt &expr,
93 const java_class_typet &java_class_type,
94 const source_locationt &location);
95
96 void gen_nondet_init(
97 code_blockt &assignments,
98 const exprt &expr,
99 bool is_sub,
100 bool skip_classid,
101 lifetimet lifetime,
102 const optionalt<typet> &override_type,
103 size_t depth,
105 const source_locationt &location);
106
107 void add_created_symbol(const symbolt &symbol);
108
109 void declare_created_symbols(code_blockt &init_code);
110
111private:
113 code_blockt &assignments,
114 const exprt &expr,
115 lifetimet lifetime,
117 size_t depth,
118 const update_in_placet &update_in_place,
119 const source_locationt &location);
120
122 code_blockt &assignments,
123 const exprt &expr,
124 bool is_sub,
125 bool skip_classid,
126 lifetimet lifetime,
127 const struct_typet &struct_type,
128 size_t depth,
129 const update_in_placet &update_in_place,
130 const source_locationt &location);
131
133 code_blockt &assignments,
134 lifetimet lifetime,
135 const pointer_typet &substitute_pointer_type,
136 size_t depth,
137 const source_locationt &location);
138
140 const exprt &element,
141 update_in_placet update_in_place,
142 const typet &element_type,
143 size_t depth,
144 const source_locationt &location);
145};
146
190 code_blockt &assignments,
191 const exprt &expr,
192 const typet &target_type,
193 lifetimet lifetime,
194 size_t depth,
195 update_in_placet update_in_place,
196 const source_locationt &location)
197{
198 PRECONDITION(expr.type().id() == ID_pointer);
200
201 const namespacet ns(symbol_table);
202 const typet &followed_target_type = ns.follow(target_type);
203 PRECONDITION(followed_target_type.id() == ID_struct);
204
205 const auto &target_class_type = to_java_class_type(followed_target_type);
206 if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
207 {
208 assignments.append(gen_nondet_array_init(
209 expr,
210 update_in_place,
211 location,
212 [this, update_in_place, depth, location](
213 const exprt &element, const typet &element_type) -> code_blockt {
214 return assign_element(
215 element, update_in_place, element_type, depth + 1, location);
216 },
217 [this](const typet &type, std::string basename_prefix) -> symbol_exprt {
219 type, basename_prefix);
220 },
223 return;
224 }
225 if(target_class_type.get_base("java::java.lang.Enum"))
226 {
227 if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
228 return;
229 }
230
231 // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
232 // initialize the fields of the object pointed by `expr`; if in
233 // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
234 // (return value of `allocate_object`), emit a statement of the form
235 // `<expr> := address-of(<new-object>)` and recursively initialize such new
236 // object.
237 exprt init_expr;
238 if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
239 {
241 assignments, expr, target_type, lifetime, "tmp_object_factory");
242 }
243 else
244 {
245 if(expr.id() == ID_address_of)
246 init_expr = to_address_of_expr(expr).object();
247 else
248 {
249 init_expr = dereference_exprt(expr);
250 }
251 }
252
254 assignments,
255 init_expr,
256 false, // is_sub
257 false, // skip_classid
258 lifetime,
259 {}, // no override type
260 depth + 1,
261 update_in_place,
262 location);
263}
264
269{
271 std::unordered_set<irep_idt> &recursion_set;
274
275public:
279 explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
280 : recursion_set(_recursion_set)
281 { }
282
285 {
286 if(!erase_entry.empty())
288 }
289
292
297 bool insert_entry(const irep_idt &entry)
298 {
299 INVARIANT(erase_entry.empty(), "insert_entry should only be called once");
300 INVARIANT(!entry.empty(), "entry should be a struct tag");
301 bool ret=recursion_set.insert(entry).second;
302 if(ret)
303 {
304 // We added something, so erase it when this is destroyed:
305 erase_entry=entry;
306 }
307 return ret;
308 }
309};
310
314
317{
318 std::string result;
319 result += numeric_cast_v<char>(interval.lower);
320 result += "-";
321 result += numeric_cast_v<char>(interval.upper);
322 return result;
323}
324
365 struct_exprt &struct_expr,
366 code_blockt &code,
367 const std::size_t &min_nondet_string_length,
368 const std::size_t &max_nondet_string_length,
369 const source_locationt &loc,
370 const irep_idt &function_id,
371 symbol_table_baset &symbol_table,
372 bool printable,
373 allocate_objectst &allocate_objects)
374{
375 namespacet ns(symbol_table);
376 const struct_typet &struct_type =
377 to_struct_type(ns.follow(struct_expr.type()));
378 PRECONDITION(is_java_string_type(struct_type));
379
380 // We allow type StringBuffer and StringBuilder to be initialized
381 // in the same way has String, because they have the same structure and
382 // are treated in the same way by CBMC.
383
384 // Note that CharSequence cannot be used as classid because it's abstract,
385 // so it is replaced by String.
386 // \todo allow StringBuffer and StringBuilder as classid for Charsequence
387 if(struct_type.get_tag() == "java.lang.CharSequence")
388 {
390 struct_expr, ns, struct_tag_typet("java::java.lang.String"));
391 }
392
393 // OK, this is a String type with the expected fields -- add code to `code`
394 // to set up pre-requisite variables and assign them in `struct_expr`.
395
397 // length_expr = nondet(int);
398 const symbol_exprt length_expr =
399 allocate_objects.allocate_automatic_local_object(
400 java_int_type(), "tmp_object_factory");
401 const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
402 code.add(code_frontend_assignt(length_expr, nondet_length));
403
404 // assume (length_expr >= min_nondet_string_length);
405 const exprt min_length =
406 from_integer(min_nondet_string_length, java_int_type());
407 code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
408
409 // assume (length_expr <= max_input_length)
410 if(
411 max_nondet_string_length <=
412 to_integer_bitvector_type(length_expr.type()).largest())
413 {
414 exprt max_length =
415 from_integer(max_nondet_string_length, length_expr.type());
416 code.add(
417 code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
418 }
419
420 const exprt data_expr =
421 make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
422 struct_expr.operands()[struct_type.component_number("length")] = length_expr;
423
424 const address_of_exprt array_pointer(
425 index_exprt(data_expr, from_integer(0, java_int_type())));
426
428 array_pointer, data_expr, symbol_table, loc, function_id, code);
429
431 data_expr, length_expr, symbol_table, loc, function_id, code);
432
433 struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
434
435 // Printable ASCII characters are between ' ' and '~'.
436 if(printable)
437 {
439 array_pointer,
440 length_expr,
442 symbol_table,
443 loc,
444 function_id,
445 code);
446 }
447}
448
474 code_blockt &assignments,
475 const exprt &expr,
476 lifetimet lifetime,
478 size_t depth,
479 const update_in_placet &update_in_place,
480 const source_locationt &location)
481{
482 PRECONDITION(expr.type().id()==ID_pointer);
483 const namespacet ns(symbol_table);
484 const typet &subtype = pointer_type.base_type();
485 const typet &followed_subtype = ns.follow(subtype);
486 PRECONDITION(followed_subtype.id() == ID_struct);
487 const pointer_typet &replacement_pointer_type =
490
491 // If we are changing the pointer, we generate code for creating a pointer
492 // to the substituted type instead
493 // TODO if we are comparing array types we need to compare their element
494 // types. this is for now done by implementing equality function especially
495 // for java types, technical debt TG-2707
496 if(!equal_java_types(replacement_pointer_type, pointer_type))
497 {
498 // update generic_parameter_specialization_map for the new pointer
500 generic_parameter_specialization_map_keys(
502 generic_parameter_specialization_map_keys.insert(
503 replacement_pointer_type,
504 ns.follow(replacement_pointer_type.base_type()));
505
506 const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
507 assignments, lifetime, replacement_pointer_type, depth, location);
508
509 // Having created a pointer to object of type replacement_pointer_type
510 // we now assign it back to the original pointer with a cast
511 // from pointer_type to replacement_pointer_type
512 assignments.add(code_frontend_assignt(
513 expr, typecast_exprt(real_pointer_symbol, pointer_type)));
514 return;
515 }
516
517 // This deletes the recursion set entry on leaving this function scope,
518 // if one is set below.
519 recursion_set_entryt recursion_set_entry(recursion_set);
520
521 // We need to prevent the possibility of this code to loop infinitely when
522 // initializing a data structure with recursive types or unbounded depth. We
523 // implement two mechanisms here. We keep a set of 'types seen', and
524 // detect when we perform a 2nd visit to the same type. We also detect the
525 // depth in the chain of (recursive) calls to the methods of this class.
526 // The depth counter is incremented only when a pointer is deferenced,
527 // including pointers to arrays.
528 //
529 // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
530 // the pointer to NULL instead of recursively initializing the struct to which
531 // it points.
532 const struct_typet &struct_type = to_struct_type(followed_subtype);
533 const irep_idt &struct_tag = struct_type.get_tag();
534
535 // If this is a recursive type of some kind AND the depth is exceeded, set
536 // the pointer to null.
537 if(
538 !recursion_set_entry.insert_entry(struct_tag) &&
540 {
541 if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
542 {
543 assignments.add(code_frontend_assignt{
544 expr, null_pointer_exprt{pointer_type}, location});
545 }
546 // Otherwise leave it as it is.
547 return;
548 }
549
550 // If we may be about to initialize a non-null enum type, always run the
551 // clinit_wrapper of its class first.
552 // TODO: TG-4689 we may want to do this for all types, not just enums, as
553 // described in the Java language specification:
554 // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
555 // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
556 // But we would have to put this behavior behind an option as it would have an
557 // impact on running times.
558 // Note that it would be more consistent with the behaviour of the JVM to only
559 // run clinit_wrapper if we are about to initialize an object of which we know
560 // for sure that it is not null on any following branch. However, adding this
561 // case in gen_nondet_struct_init would slow symex down too much, so if we
562 // decide to do this for all types, we should do it here.
563 // Note also that this logic is mirrored in
564 // ci_lazy_methodst::initialize_instantiated_classes.
565 if(
566 const auto class_type =
567 type_try_dynamic_cast<java_class_typet>(followed_subtype))
568 {
569 if(class_type->get_base("java::java.lang.Enum"))
570 {
571 const irep_idt &class_name = class_type->get_name();
572 const irep_idt class_clinit = clinit_wrapper_name(class_name);
573 if(const auto clinit_func = symbol_table.lookup(class_clinit))
574 assignments.add(code_function_callt{clinit_func->symbol_expr()});
575 }
576 }
577
578 code_blockt new_object_assignments;
579 code_blockt update_in_place_assignments;
580
581 // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
582 // emit to `update_in_place_assignments` code for in-place initialization of
583 // the object pointed by `expr`, assuming that such object is of type
584 // `subtype`
585 if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
586 {
588 update_in_place_assignments,
589 expr,
590 subtype,
591 lifetime,
592 depth,
594 location);
595 }
596
597 // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
598 // above to `assignments` and return
599 if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
600 {
601 assignments.append(update_in_place_assignments);
602 return;
603 }
604
605 // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
606 // vector of assignments that create a new object (recursively initializes it)
607 // and asign to `expr` the address of such object
608 code_blockt non_null_inst;
609
611 non_null_inst,
612 expr,
613 subtype,
614 lifetime,
615 depth,
617 location);
618
619 const code_frontend_assignt set_null_inst{
620 expr, null_pointer_exprt{pointer_type}, location};
621
622 const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
623
624 if(!allow_null)
625 {
626 // Add the following code to assignments:
627 // <expr> = <aoe>;
628 new_object_assignments.append(non_null_inst);
629 }
630 else
631 {
632 // if(NONDET(_Bool)
633 // {
634 // <expr> = <null pointer>
635 // }
636 // else
637 // {
638 // <code from recursive call to gen_nondet_init() with
639 // tmp$<temporary_counter>>
640 // }
641 code_ifthenelset null_check(
643 std::move(set_null_inst),
644 std::move(non_null_inst));
645
646 new_object_assignments.add(std::move(null_check));
647 }
648
649 // Similarly to above, maybe use a conditional if both the
650 // allocate-fresh and update-in-place cases are allowed:
651 if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
652 {
653 assignments.append(new_object_assignments);
654 }
655 else
656 {
658 "No-update and must-update should have already been resolved");
659
660 code_ifthenelset update_check(
662 std::move(update_in_place_assignments),
663 std::move(new_object_assignments));
664
665 assignments.add(std::move(update_check));
666 }
667}
668
693 code_blockt &assignments,
694 lifetimet lifetime,
695 const pointer_typet &replacement_pointer,
696 size_t depth,
697 const source_locationt &location)
698{
699 const symbol_exprt new_symbol_expr =
701 replacement_pointer, "tmp_object_factory");
702
703 // Generate a new object into this new symbol
705 assignments,
706 new_symbol_expr,
707 false, // is_sub
708 false, // skip_classid
709 lifetime,
710 {}, // no override_type
711 depth,
713 location);
714
715 return new_symbol_expr;
716}
717
729 const exprt &expr,
730 const std::list<std::string> &string_input_values,
731 symbol_table_baset &symbol_table)
732{
733 alternate_casest cases;
734 for(const auto &val : string_input_values)
735 {
736 const symbol_exprt s =
737 get_or_create_string_literal_symbol(val, symbol_table, true);
738 cases.push_back(code_frontend_assignt(expr, s));
739 }
740 return cases;
741}
742
765 code_blockt &assignments,
766 const exprt &expr,
767 bool is_sub,
768 bool skip_classid,
769 lifetimet lifetime,
770 const struct_typet &struct_type,
771 size_t depth,
772 const update_in_placet &update_in_place,
773 const source_locationt &location)
774{
775 const namespacet ns(symbol_table);
776 PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
777
778 typedef struct_typet::componentst componentst;
779 const irep_idt &struct_tag=struct_type.get_tag();
780
781 const componentst &components=struct_type.components();
782
783 // Should we write the whole object?
784 // * Not if this is a sub-structure (a superclass object), as our caller will
785 // have done this already
786 // * Not if the object has already been initialised by our caller, in which
787 // case they will set `skip_classid`
788 // * Not if we're re-initializing an existing object (i.e. update_in_place)
789 // * Always if it has a string type. Strings should not be partially updated,
790 // and the `length` and `data` components of string types need to be
791 // generated differently from object fields in the general case, see
792 // \ref java_object_factoryt::initialize_nondet_string_fields.
793
794 const bool has_string_input_values =
796
797 if(
798 is_java_string_type(struct_type) && has_string_input_values &&
799 !skip_classid)
800 { // We're dealing with a string and we should set fixed input values.
801 // We create a switch statement where each case is an assignment
802 // of one of the fixed input strings to the input variable in question
805 assignments.add(generate_nondet_switch(
807 cases,
809 ID_java,
810 location,
811 symbol_table));
812 }
813 else if(
814 (!is_sub && !skip_classid &&
815 update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) ||
816 is_java_string_type(struct_type))
817 {
818 // Add an initial all-zero write. Most of the fields of this will be
819 // overwritten, but it helps to have a whole-structure write that analysis
820 // passes can easily recognise leaves no uninitialised state behind.
821
822 // This code mirrors the `remove_java_new` pass:
823 auto initial_object = zero_initializer(expr.type(), source_locationt(), ns);
824 CHECK_RETURN(initial_object.has_value());
826 to_struct_expr(*initial_object),
827 ns,
828 struct_tag_typet("java::" + id2string(struct_tag)));
829
830 // If the initialised type is a special-cased String type (one with length
831 // and data fields introduced by string-library preprocessing), initialise
832 // those fields with nondet values
833 if(is_java_string_type(struct_type))
834 { // We're dealing with a string
836 to_struct_expr(*initial_object),
837 assignments,
840 location,
845 }
846
847 assignments.add(code_frontend_assignt(expr, *initial_object));
848 }
849
850 for(const auto &component : components)
851 {
852 const typet &component_type=component.type();
853 irep_idt name=component.get_name();
854
855 member_exprt me(expr, name, component_type);
856
858 {
859 continue;
860 }
861 else if(name == "cproverMonitorCount")
862 {
863 // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
864 // nondet. This field is only present when the java core models are
865 // included in the class-path. It is used to implement a critical section,
866 // which is necessary to support concurrency.
867 if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
868 continue;
869 code_frontend_assignt code(me, from_integer(0, me.type()));
870 code.add_source_location() = location;
871 assignments.add(code);
872 }
873 else if(
874 is_java_string_type(struct_type) && (name == "length" || name == "data"))
875 {
876 // In this case these were set up above.
877 continue;
878 }
879 else
880 {
881 INVARIANT(!name.empty(), "Each component of a struct must have a name");
882
883 bool _is_sub=name[0]=='@';
884
885 // MUST_UPDATE_IN_PLACE only applies to this object.
886 // If this is a pointer to another object, offer the chance
887 // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
888 update_in_placet substruct_in_place=
889 update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE && !_is_sub ?
891 update_in_place;
893 assignments,
894 me,
895 _is_sub,
896 false, // skip_classid
897 lifetime,
898 {}, // no override_type
899 depth,
900 substruct_in_place,
901 location);
902 }
903 }
904
905 // If cproverNondetInitialize() can be found in the symbol table as a method
906 // on this class or any parent, we add a call:
907 // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
908 // expr.cproverNondetInitialize();
909 // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
910
911 resolve_inherited_componentt resolve_inherited_component{symbol_table};
913 cprover_nondet_initialize = resolve_inherited_component(
914 "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true);
915
916 if(cprover_nondet_initialize)
917 {
918 const symbolt &cprover_nondet_initialize_symbol =
919 ns.lookup(cprover_nondet_initialize->get_full_component_identifier());
920 assignments.add(
921 code_function_callt{cprover_nondet_initialize_symbol.symbol_expr(),
922 {address_of_exprt{expr}}});
923 }
924}
925
941 const exprt &expr,
942 const typet &type,
943 const source_locationt &location,
944 const allocate_local_symbolt &allocate_local_symbol)
945{
946 PRECONDITION(type == java_float_type() || type == java_double_type());
947
948 code_blockt assignments;
949
950 const auto &aux_int =
951 allocate_local_symbol(java_int_type(), "assume_integral_tmp");
952 assignments.add(code_declt(aux_int), location);
953 exprt nondet_rhs = side_effect_expr_nondett(java_int_type(), location);
954 code_frontend_assignt aux_assign(aux_int, nondet_rhs);
955 aux_assign.add_source_location() = location;
956 assignments.add(aux_assign);
957 assignments.add(
958 code_assumet(equal_exprt(typecast_exprt(aux_int, type), expr)));
959
960 return assignments;
961}
962
999 code_blockt &assignments,
1000 const exprt &expr,
1001 bool is_sub,
1002 bool skip_classid,
1003 lifetimet lifetime,
1004 const optionalt<typet> &override_type,
1005 size_t depth,
1006 update_in_placet update_in_place,
1007 const source_locationt &location)
1008{
1009 const typet &type = override_type.has_value() ? *override_type : expr.type();
1010 const namespacet ns(symbol_table);
1011 const typet &followed_type = ns.follow(type);
1012
1013 if(type.id()==ID_pointer)
1014 {
1015 // dereferenced type
1017
1018 // If we are about to initialize a generic pointer type, add its concrete
1019 // types to the map and delete them on leaving this function scope.
1021 generic_parameter_specialization_map_keys(
1023 generic_parameter_specialization_map_keys.insert(
1025
1027 assignments,
1028 expr,
1029 lifetime,
1031 depth,
1032 update_in_place,
1033 location);
1034 }
1035 else if(followed_type.id() == ID_struct)
1036 {
1037 const struct_typet struct_type = to_struct_type(followed_type);
1038
1039 // If we are about to initialize a generic class (as a superclass object
1040 // for a different object), add its concrete types to the map and delete
1041 // them on leaving this function scope.
1043 generic_parameter_specialization_map_keys(
1045 if(is_sub)
1046 {
1047 const typet &symbol =
1048 override_type.has_value() ? *override_type : expr.type();
1049 PRECONDITION(symbol.id() == ID_struct_tag);
1050 generic_parameter_specialization_map_keys.insert(
1051 to_struct_tag_type(symbol), struct_type);
1052 }
1053
1055 assignments,
1056 expr,
1057 is_sub,
1058 skip_classid,
1059 lifetime,
1060 struct_type,
1061 depth,
1062 update_in_place,
1063 location);
1064 }
1065 else
1066 {
1067 // types different from pointer or structure:
1068 // bool, int, float, byte, char, ...
1069 exprt rhs = type.id() == ID_c_bool
1070 ? get_nondet_bool(type, location)
1071 : side_effect_expr_nondett(type, location);
1072 code_frontend_assignt assign(expr, rhs);
1073 assign.add_source_location() = location;
1074
1075 assignments.add(assign);
1077 {
1078 assignments.add(
1080 }
1081 // add assumes to obey numerical restrictions
1082 if(type != java_boolean_type() && type != java_char_type())
1083 {
1085 if(auto singleton = interval.as_singleton())
1086 {
1087 assignments.add(
1088 code_frontend_assignt{expr, from_integer(*singleton, expr.type())});
1089 }
1090 else
1091 {
1092 exprt within_bounds = interval.make_contains_expr(expr);
1093 if(!within_bounds.is_true())
1094 assignments.add(code_assumet(std::move(within_bounds)));
1095 }
1096
1097 if(
1099 (type == java_float_type() || type == java_double_type()))
1100 {
1101 assignments.add(assume_expr_integral(
1102 expr,
1103 type,
1104 location,
1105 [this](
1106 const typet &type, std::string basename_prefix) -> symbol_exprt {
1108 type, basename_prefix);
1109 }));
1110 }
1111 }
1112 }
1113}
1114
1116{
1118}
1119
1121{
1123}
1124
1143 code_blockt &assignments,
1144 const exprt &lhs,
1145 const exprt &max_length_expr,
1146 const typet &element_type,
1147 const allocate_local_symbolt &allocate_local_symbol,
1148 const source_locationt &location)
1149{
1150 const auto &length_sym_expr = generate_nondet_int(
1152 max_length_expr,
1153 "nondet_array_length",
1154 location,
1155 allocate_local_symbol,
1156 assignments);
1157
1158 side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), location);
1159 java_new_array.copy_to_operands(length_sym_expr);
1160 java_new_array.set(ID_length_upper_bound, max_length_expr);
1161 java_new_array.type().subtype().set(ID_element_type, element_type);
1162 code_frontend_assignt assign(lhs, java_new_array);
1163 assign.add_source_location() = location;
1164 assignments.add(assign);
1165}
1166
1185 code_blockt &assignments,
1186 const exprt &init_array_expr,
1187 const typet &element_type,
1188 const exprt &max_length_expr,
1189 const source_locationt &location,
1190 const allocate_local_symbolt &allocate_local_symbol)
1191{
1192 const array_typet array_type(element_type, max_length_expr);
1193
1194 // TYPE (*array_data_init)[max_length_expr];
1195 const symbol_exprt &tmp_finite_array_pointer =
1196 allocate_local_symbol(pointer_type(array_type), "array_data_init");
1197
1198 // array_data_init = ALLOCATE(TYPE [max_length_expr], max_length_expr, false);
1199 assignments.add(
1201 tmp_finite_array_pointer,
1202 max_length_expr));
1203 assignments.statements().back().add_source_location() = location;
1204
1205 // *array_data_init = NONDET(TYPE [max_length_expr]);
1206 side_effect_expr_nondett nondet_data(array_type, location);
1207 const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};
1208 assignments.add(
1209 code_frontend_assignt(data_pointer_deref, std::move(nondet_data)));
1210 assignments.statements().back().add_source_location() = location;
1211
1212 // init_array_expr = *array_data_init;
1213 address_of_exprt tmp_nondet_pointer(
1214 index_exprt(data_pointer_deref, from_integer(0, java_int_type())));
1215 assignments.add(
1216 code_frontend_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
1217 assignments.statements().back().add_source_location() = location;
1218}
1219
1230 const exprt &element,
1231 const update_in_placet update_in_place,
1232 const typet &element_type,
1233 const size_t depth,
1234 const source_locationt &location)
1235{
1236 code_blockt assignments;
1237 bool new_item_is_primitive = element.type().id() != ID_pointer;
1238
1239 // Use a temporary to initialise a new, or update an existing, non-primitive.
1240 // This makes it clearer that in a sequence like
1241 // `new_array_item->x = y; new_array_item->z = w;` that all the
1242 // `new_array_item` references must alias, cf. the harder-to-analyse
1243 // `some_expr[idx]->x = y; some_expr[idx]->z = w;`
1244 exprt init_expr;
1245 if(new_item_is_primitive)
1246 {
1247 init_expr = element;
1248 }
1249 else
1250 {
1252 element.type(), "new_array_item");
1253
1254 // If we're updating an existing array item, read the existing object that
1255 // we (may) alter:
1256 if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
1257 assignments.add(code_frontend_assignt(init_expr, element));
1258 }
1259
1260 // MUST_UPDATE_IN_PLACE only applies to this object.
1261 // If this is a pointer to another object, offer the chance
1262 // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1263 update_in_placet child_update_in_place =
1266 : update_in_place;
1268 assignments,
1269 init_expr,
1270 false, // is_sub
1271 false, // skip_classid
1272 // These are variable in number, so use dynamic allocator:
1274 element_type, // override
1275 depth,
1276 child_update_in_place,
1277 location);
1278
1279 if(!new_item_is_primitive)
1280 {
1281 // We used a temporary variable to update or initialise an array item;
1282 // now write it into the array:
1283 assignments.add(code_frontend_assignt(element, init_expr));
1284 }
1285 return assignments;
1286}
1287
1329 code_blockt &assignments,
1330 const exprt &init_array_expr,
1331 const exprt &length_expr,
1332 const typet &element_type,
1333 const exprt &max_length_expr,
1334 update_in_placet update_in_place,
1335 const source_locationt &location,
1336 const array_element_generatort &element_generator,
1337 const allocate_local_symbolt &allocate_local_symbol,
1338 const symbol_tablet &symbol_table)
1339{
1340 const symbol_exprt &array_init_symexpr =
1341 allocate_local_symbol(init_array_expr.type(), "array_data_init");
1342
1343 code_frontend_assignt data_assign(array_init_symexpr, init_array_expr);
1344 data_assign.add_source_location() = location;
1345 assignments.add(data_assign);
1346
1347 const symbol_exprt &counter_expr =
1348 allocate_local_symbol(length_expr.type(), "array_init_iter");
1349
1350 code_blockt loop_body;
1351 if(update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
1352 {
1353 // Add a redundant if(counter == max_length) break
1354 // that is easier for the unwinder to understand.
1355 code_ifthenelset max_test(
1356 equal_exprt(counter_expr, max_length_expr), code_breakt{});
1357
1358 loop_body.add(std::move(max_test));
1359 }
1360
1361 const dereference_exprt element_at_counter =
1362 array_element_from_pointer(array_init_symexpr, counter_expr);
1363
1364 loop_body.append(element_generator(element_at_counter, element_type));
1365
1368 length_expr,
1369 counter_expr,
1370 std::move(loop_body),
1371 location));
1372}
1373
1375 const exprt &expr,
1376 update_in_placet update_in_place,
1377 const source_locationt &location,
1378 const array_element_generatort &element_generator,
1379 const allocate_local_symbolt &allocate_local_symbol,
1380 const symbol_tablet &symbol_table,
1381 const size_t max_nondet_array_length)
1382{
1383 PRECONDITION(expr.type().id() == ID_pointer);
1384 PRECONDITION(expr.type().subtype().id() == ID_struct_tag);
1386
1387 code_blockt statements;
1388
1389 const namespacet ns(symbol_table);
1390 const typet &type = ns.follow(expr.type().subtype());
1391 const struct_typet &struct_type = to_struct_type(type);
1392 const typet &element_type =
1393 static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
1394
1395 auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
1396
1397 // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1398 // initialize its elements
1399 if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
1400 {
1402 statements,
1403 expr,
1404 max_length_expr,
1405 element_type,
1406 allocate_local_symbol,
1407 location);
1408 }
1409
1410 // Otherwise we're updating the array in place, and use the
1411 // existing array allocation and length.
1412
1413 INVARIANT(
1414 is_valid_java_array(struct_type),
1415 "Java struct array does not conform to expectations");
1416
1417 dereference_exprt deref_expr(expr);
1418 const auto &comps = struct_type.components();
1419 const member_exprt length_expr(deref_expr, "length", comps[1].type());
1420 exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());
1421
1422 if(init_array_expr.type() != pointer_type(element_type))
1423 init_array_expr =
1424 typecast_exprt(init_array_expr, pointer_type(element_type));
1425
1426 if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
1427 {
1428 // For arrays of non-primitive type, nondeterministically initialize each
1429 // element of the array
1431 statements,
1432 init_array_expr,
1433 length_expr,
1434 element_type,
1435 max_length_expr,
1436 update_in_place,
1437 location,
1438 element_generator,
1439 allocate_local_symbol,
1440 symbol_table);
1441 }
1442 else
1443 {
1444 // Arrays of primitive type can be initialized with a single instruction.
1445 // We don't do this for arrays of primitive booleans, because booleans are
1446 // represented as unsigned bytes, so each cell must be initialized as
1447 // 0 or 1 (see gen_nondet_init).
1449 statements,
1450 init_array_expr,
1451 element_type,
1452 max_length_expr,
1453 location,
1454 allocate_local_symbol);
1455 }
1456 return statements;
1457}
1458
1473 code_blockt &assignments,
1474 const exprt &expr,
1475 const java_class_typet &java_class_type,
1476 const source_locationt &location)
1477{
1478 const irep_idt &class_name = java_class_type.get_name();
1479 const irep_idt values_name = id2string(class_name) + ".$VALUES";
1480 if(!symbol_table.has_symbol(values_name))
1481 {
1482 log.warning() << values_name
1483 << " is missing, so the corresponding Enum "
1484 "type will nondet initialised"
1485 << messaget::eom;
1486 return false;
1487 }
1488
1489 const namespacet ns(symbol_table);
1490 const symbolt &values = ns.lookup(values_name);
1491
1492 // Access members (length and data) of $VALUES array
1493 dereference_exprt deref_expr(values.symbol_expr());
1494 const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type()));
1495 PRECONDITION(is_valid_java_array(deref_struct_type));
1496 const auto &comps = deref_struct_type.components();
1497 const member_exprt length_expr(deref_expr, "length", comps[1].type());
1498 const member_exprt enum_array_expr =
1499 member_exprt(deref_expr, "data", comps[2].type());
1500
1501 const symbol_exprt &index_expr = generate_nondet_int(
1503 minus_exprt(length_expr, from_integer(1, java_int_type())),
1504 "enum_index_init",
1505 location,
1507 assignments);
1508
1509 const dereference_exprt element_at_index =
1510 array_element_from_pointer(enum_array_expr, index_expr);
1511 code_frontend_assignt enum_assign(
1512 expr, typecast_exprt(element_at_index, expr.type()));
1513 assignments.add(enum_assign);
1514
1515 return true;
1516}
1517
1518static void assert_type_consistency(const code_blockt &assignments)
1519{
1520 // In future we'll be able to use codet::validate for this;
1521 // at present that only verifies `lhs.type base_type_eq right.type`,
1522 // whereas we want to check exact equality.
1523 for(const auto &code : assignments.statements())
1524 {
1525 if(code.get_statement() != ID_assign)
1526 continue;
1527 const auto &assignment = to_code_frontend_assign(code);
1528 INVARIANT(
1529 assignment.lhs().type() == assignment.rhs().type(),
1530 "object factory should produce type-consistent assignments");
1531 }
1532}
1533
1546 const typet &type,
1547 const irep_idt base_name,
1548 code_blockt &init_code,
1549 symbol_table_baset &symbol_table,
1551 lifetimet lifetime,
1552 const source_locationt &loc,
1553 const select_pointer_typet &pointer_type_selector,
1554 message_handlert &log)
1555{
1556 const symbolt &main_symbol = get_fresh_aux_symbol(
1557 type,
1559 id2string(base_name),
1560 loc,
1561 ID_java,
1562 symbol_table);
1563
1565
1566 exprt object=main_symbol.symbol_expr();
1567
1569 loc, parameters, symbol_table, pointer_type_selector, log);
1570 code_blockt assignments;
1571 state.gen_nondet_init(
1572 assignments,
1573 object,
1574 false, // is_sub
1575 false, // skip_classid
1576 lifetime,
1577 {}, // no override_type
1578 1, // initial depth
1580 loc);
1581
1582 state.add_created_symbol(main_symbol);
1583 state.declare_created_symbols(init_code);
1584
1585 assert_type_consistency(assignments);
1586 init_code.append(assignments);
1587 return object;
1588}
1589
1623 const exprt &expr,
1624 code_blockt &init_code,
1625 symbol_table_baset &symbol_table,
1626 const source_locationt &loc,
1627 bool skip_classid,
1628 lifetimet lifetime,
1629 const java_object_factory_parameterst &object_factory_parameters,
1630 const select_pointer_typet &pointer_type_selector,
1631 update_in_placet update_in_place,
1632 message_handlert &log)
1633{
1635 loc, object_factory_parameters, symbol_table, pointer_type_selector, log);
1636 code_blockt assignments;
1637 state.gen_nondet_init(
1638 assignments,
1639 expr,
1640 false, // is_sub
1641 skip_classid,
1642 lifetime,
1643 {}, // no override_type
1644 1, // initial depth
1645 update_in_place,
1646 loc);
1647
1648 state.declare_created_symbols(init_code);
1649
1650 assert_type_consistency(assignments);
1651 init_code.append(assignments);
1652}
1653
1656 const typet &type,
1657 const irep_idt base_name,
1658 code_blockt &init_code,
1659 symbol_tablet &symbol_table,
1660 const java_object_factory_parameterst &object_factory_parameters,
1661 lifetimet lifetime,
1662 const source_locationt &location,
1663 message_handlert &log)
1664{
1665 select_pointer_typet pointer_type_selector;
1666 return object_factory(
1667 type,
1668 base_name,
1669 init_code,
1670 symbol_table,
1671 object_factory_parameters,
1672 lifetime,
1673 location,
1674 pointer_type_selector,
1675 log);
1676}
1677
1680 const exprt &expr,
1681 code_blockt &init_code,
1682 symbol_table_baset &symbol_table,
1683 const source_locationt &loc,
1684 bool skip_classid,
1685 lifetimet lifetime,
1686 const java_object_factory_parameterst &object_factory_parameters,
1687 update_in_placet update_in_place,
1688 message_handlert &log)
1689{
1690 select_pointer_typet pointer_type_selector;
1692 expr,
1693 init_code,
1694 symbol_table,
1695 loc,
1696 skip_classid,
1697 lifetime,
1698 object_factory_parameters,
1699 pointer_type_selector,
1700 update_in_place,
1701 log);
1702}
code_frontend_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
lifetimet
Selects the kind of objects allocated.
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
dereference_exprt array_element_from_pointer(const exprt &pointer, const exprt &index)
Generate statement using pointer arithmetic to access the element at the given index of a pointer arr...
static std::pair< symbol_exprt, code_with_references_listt > nondet_length(allocate_objectst &allocate, source_locationt loc)
Declare a non-deterministic length expression.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Extract class identifier.
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
void add_created_symbol(const symbolt &symbol)
Add a pointer to a symbol to the list of pointers to symbols created so far.
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
Allocates a new object, either by creating a local variable with automatic lifetime,...
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Arrays with given size.
Definition: std_types.h:763
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
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
code_operandst & statements()
Definition: std_code.h:138
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:89
void add(const codet &code)
Definition: std_code.h:168
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1182
A codet representing the declaration of a local variable.
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
Definition: std_code.cpp:158
A codet representing an assignment in the program.
Definition: std_code.h:24
codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition: std_code.h:460
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
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
void insert(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Author: Diffblue Ltd.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Array index operator.
Definition: std_expr.h:1328
mp_integer largest() const
Return the largest value that can be represented using this type.
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:557
generic_parameter_specialization_mapt generic_parameter_specialization_map
Every time the non-det generator visits a type and the type is generic (either a struct or a pointer)...
const java_object_factory_parameterst object_factory_parameters
allocate_objectst allocate_objects
void add_created_symbol(const symbolt &symbol)
std::unordered_set< irep_idt > recursion_set
This is employed in conjunction with the depth above.
const select_pointer_typet & pointer_type_selector
Resolves pointer types potentially using some heuristics, for example to replace pointers to interfac...
messaget log
Log for reporting warnings and errors in object creation.
symbol_table_baset & symbol_table
The symbol table.
symbol_exprt gen_nondet_subtype_pointer_init(code_blockt &assignments, lifetimet lifetime, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location)
Generate codet assignments to initalize the selected concrete type.
void declare_created_symbols(code_blockt &init_code)
void gen_pointer_target_init(code_blockt &assignments, const exprt &expr, const typet &target_type, lifetimet lifetime, size_t depth, update_in_placet update_in_place, const source_locationt &location)
Initializes the pointer-typed lvalue expression expr to point to an object of type target_type,...
void gen_nondet_init(code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const optionalt< typet > &override_type, size_t depth, update_in_placet, const source_locationt &location)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
bool gen_nondet_enum_init(code_blockt &assignments, const exprt &expr, const java_class_typet &java_class_type, const source_locationt &location)
We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet...
java_object_factoryt(const source_locationt &loc, const java_object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector, message_handlert &log)
void gen_nondet_struct_init(code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const struct_typet &struct_type, size_t depth, const update_in_placet &update_in_place, const source_locationt &location)
Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializ...
void gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, lifetimet lifetime, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place, const source_locationt &location)
Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree.
code_blockt assign_element(const exprt &element, update_in_placet update_in_place, const typet &element_type, size_t depth, const source_locationt &location)
Generate codet for assigning an individual element inside the array.
Extract member of struct or union.
Definition: std_expr.h:2667
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
Binary minus.
Definition: std_expr.h:973
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The null pointer constant.
Definition: pointer_expr.h:723
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Recursion-set entry owner class.
recursion_set_entryt(const recursion_set_entryt &)=delete
recursion_set_entryt(std::unordered_set< irep_idt > &_recursion_set)
Initialize a recursion-set entry owner operating on a given set.
recursion_set_entryt & operator=(const recursion_set_entryt &)=delete
bool insert_entry(const irep_idt &entry)
Try to add an entry to the controlled set.
~recursion_set_entryt()
Removes erase_entry (if set) from the controlled set.
std::unordered_set< irep_idt > & recursion_set
Recursion set to modify.
irep_idt erase_entry
Entry to erase on destruction, if non-empty.
virtual pointer_typet convert_pointer_type(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
Select what type should be used for a given pointer type.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
An expression containing a side effect.
Definition: std_code.h:1450
Struct constructor from list of elements.
Definition: std_expr.h:1722
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Structure type, corresponds to C style structs.
Definition: std_types.h:231
irep_idt get_tag() const
Definition: std_types.h:168
const componentst & components() const
Definition: std_types.h:147
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:40
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
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.
Goto Programs with Functions.
exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
Given an exprt and an integer interval return an exprt that represents restricting the expression to ...
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static void assert_type_consistency(const code_blockt &assignments)
void initialize_nondet_string_fields(struct_exprt &struct_expr, code_blockt &code, const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable, allocate_objectst &allocate_objects)
Initialise length and data fields for a nondeterministic String structure.
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
static void array_primitive_init_code(code_blockt &assignments, const exprt &init_array_expr, const typet &element_type, const exprt &max_length_expr, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
Create code to nondeterministically initialize arrays of primitive type.
static void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type, const allocate_local_symbolt &allocate_local_symbol, const source_locationt &location)
Allocates a fresh array and emits an assignment writing to lhs the address of the new array.
static irep_idt integer_interval_to_string(const integer_intervalt &interval)
Converts and integer_intervalt to a a string of the for [lower]-[upper].
static code_blockt assume_expr_integral(const exprt &expr, const typet &type, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
Generate code block that verifies that an expression of type float or double has integral value.
const integer_intervalt printable_char_range(' ', '~')
Interval that represents the printable character range range U+0020-U+007E, i.e.
code_blockt gen_nondet_array_init(const exprt &expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table, const size_t max_nondet_array_length)
Synthesize GOTO for generating a array of nondet length to be stored in the expr.
alternate_casest get_string_input_values_code(const exprt &expr, const std::list< std::string > &string_input_values, symbol_table_baset &symbol_table)
Creates an alternate_casest vector in which each item contains an assignment of a string from string_...
static void array_loop_init_code(code_blockt &assignments, const exprt &init_array_expr, const exprt &length_expr, const typet &element_type, const exprt &max_length_expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table)
Create code to nondeterministically initialize each element of an array in a loop.
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)> array_element_generatort
update_in_placet
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_range, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
Produce code for simple implementation of String Java libraries.
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
signedbv_typet java_int_type()
Definition: java_types.cpp:31
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Definition: java_types.cpp:833
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
Definition: java_types.cpp:890
floatbv_typet java_double_type()
Definition: java_types.cpp:73
floatbv_typet java_float_type()
Definition: java_types.cpp:67
c_bool_typet java_boolean_type()
Definition: java_types.cpp:79
unsignedbv_typet java_char_type()
Definition: java_types.cpp:61
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
Definition: java_utils.cpp:26
code_blockt generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
Pick nondeterministically between imperative actions 'switch_cases'.
Definition: nondet.cpp:91
symbol_exprt generate_nondet_int(const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value,...
Definition: nondet.cpp:15
std::vector< codet > alternate_casest
Definition: nondet.h:73
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:18
Nondeterministic boolean helper.
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:21
nonstd::optional< T > optionalt
Definition: optional.h:35
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
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const code_frontend_assignt & to_code_frontend_assign(const codet &code)
Definition: std_code.h:113
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
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
interval_uniont assume_inputs_interval
Force numerical primitive inputs to fall within the interval.
bool assume_inputs_integral
Force double and float inputs to be integral.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
bool string_printable
Force string content to be ASCII printable characters when set to true.
size_t max_nondet_string_length
Maximum value for the non-deterministically-chosen length of a string.
size_t min_nondet_string_length
Minimum value for the non-deterministically-chosen length of a string.