cprover
Loading...
Searching...
No Matches
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>
16#include <util/message.h>
17#include <util/nondet_bool.h>
18#include <util/prefix.h>
20
23
29#include "java_utils.h"
30#include "select_pointer_type.h"
31
33{
35
40 std::unordered_set<irep_idt> recursion_set;
41
51
54
59
61
64
66 code_blockt &assignments,
67 const exprt &expr,
68 const typet &target_type,
69 lifetimet lifetime,
70 size_t depth,
72 const source_locationt &location);
73public:
90
92 code_blockt &assignments,
93 const exprt &expr,
95 const source_locationt &location);
96
97 void gen_nondet_init(
98 code_blockt &assignments,
99 const exprt &expr,
100 bool is_sub,
101 bool skip_classid,
102 lifetimet lifetime,
104 size_t depth,
106 const source_locationt &location);
107
108 void add_created_symbol(const symbolt &symbol);
109
111
112private:
114 code_blockt &assignments,
115 const exprt &expr,
116 lifetimet lifetime,
118 size_t depth,
120 const source_locationt &location);
121
123 code_blockt &assignments,
124 const exprt &expr,
125 bool is_sub,
126 bool skip_classid,
127 lifetimet lifetime,
129 size_t depth,
131 const source_locationt &location);
132
134 code_blockt &assignments,
135 lifetimet lifetime,
137 size_t depth,
138 const source_locationt &location);
139
141 const exprt &element,
143 const typet &element_type,
144 size_t depth,
145 const source_locationt &location);
146};
147
191 code_blockt &assignments,
192 const exprt &expr,
193 const typet &target_type,
194 lifetimet lifetime,
195 size_t depth,
197 const source_locationt &location)
198{
199 PRECONDITION(expr.type().id() == ID_pointer);
201
202 const namespacet ns(symbol_table);
203 const typet &followed_target_type = ns.follow(target_type);
205
207 if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
208 {
209 assignments.append(gen_nondet_array_init(
210 expr,
212 location,
213 [this, update_in_place, depth, location](
214 const exprt &element, const typet &element_type) -> code_blockt {
215 return assign_element(
216 element, update_in_place, element_type, depth + 1, location);
217 },
218 [this](const typet &type, std::string basename_prefix) -> symbol_exprt {
220 type, basename_prefix);
221 },
223 object_factory_parameters.max_nondet_array_length));
224 return;
225 }
226 if(target_class_type.get_base("java::java.lang.Enum"))
227 {
228 if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
229 return;
230 }
231
232 // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
233 // initialize the fields of the object pointed by `expr`; if in
234 // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
235 // (return value of `allocate_object`), emit a statement of the form
236 // `<expr> := address-of(<new-object>)` and recursively initialize such new
237 // object.
240 {
242 assignments, expr, target_type, lifetime, "tmp_object_factory");
243 }
244 else
245 {
246 if(expr.id() == ID_address_of)
247 init_expr = to_address_of_expr(expr).object();
248 else
249 {
251 }
252 }
253
255 assignments,
256 init_expr,
257 false, // is_sub
258 false, // skip_classid
259 lifetime,
260 {}, // no override type
261 depth + 1,
263 location);
264}
265
270{
272 std::unordered_set<irep_idt> &recursion_set;
275
276public:
280 explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
282 { }
283
290
293
298 bool insert_entry(const irep_idt &entry)
299 {
300 INVARIANT(erase_entry.empty(), "insert_entry should only be called once");
301 INVARIANT(!entry.empty(), "entry should be a struct tag");
302 bool ret=recursion_set.insert(entry).second;
303 if(ret)
304 {
305 // We added something, so erase it when this is destroyed:
306 erase_entry=entry;
307 }
308 return ret;
309 }
310};
311
315
318{
319 std::string result;
320 result += numeric_cast_v<char>(interval.lower);
321 result += "-";
322 result += numeric_cast_v<char>(interval.upper);
323 return result;
324}
325
367 code_blockt &code,
368 const std::size_t &min_nondet_string_length,
369 const std::size_t &max_nondet_string_length,
370 const source_locationt &loc,
371 const irep_idt &function_id,
372 symbol_table_baset &symbol_table,
373 bool printable,
374 allocate_objectst &allocate_objects)
375{
376 namespacet ns(symbol_table);
380
381 // We allow type StringBuffer and StringBuilder to be initialized
382 // in the same way has String, because they have the same structure and
383 // are treated in the same way by CBMC.
384
385 // Note that CharSequence cannot be used as classid because it's abstract,
386 // so it is replaced by String.
387 // \todo allow StringBuffer and StringBuilder as classid for Charsequence
388 if(struct_type.get_tag() == "java.lang.CharSequence")
389 {
391 struct_expr, ns, struct_tag_typet("java::java.lang.String"));
392 }
393
394 // OK, this is a String type with the expected fields -- add code to `code`
395 // to set up pre-requisite variables and assign them in `struct_expr`.
396
398 // length_expr = nondet(int);
400 allocate_objects.allocate_automatic_local_object(
401 java_int_type(), "tmp_object_factory");
404
405 // assume (length_expr >= min_nondet_string_length);
406 const exprt min_length =
407 from_integer(min_nondet_string_length, java_int_type());
409
410 // assume (length_expr <= max_input_length)
411 if(
412 max_nondet_string_length <=
413 to_integer_bitvector_type(length_expr.type()).largest())
414 {
416 from_integer(max_nondet_string_length, length_expr.type());
417 code.add(
419 }
420
421 const exprt data_expr =
422 make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
423 struct_expr.operands()[struct_type.component_number("length")] = length_expr;
424
427
429 array_pointer, data_expr, symbol_table, loc, function_id, code);
430
432 data_expr, length_expr, symbol_table, loc, function_id, code);
433
434 struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
435
436 // Printable ASCII characters are between ' ' and '~'.
437 if(printable)
438 {
443 symbol_table,
444 loc,
445 function_id,
446 code);
447 }
448}
449
475 code_blockt &assignments,
476 const exprt &expr,
477 lifetimet lifetime,
479 size_t depth,
481 const source_locationt &location)
482{
483 PRECONDITION(expr.type().id()==ID_pointer);
484 const namespacet ns(symbol_table);
485 const typet &subtype = pointer_type.base_type();
486 const typet &followed_subtype = ns.follow(subtype);
489 pointer_type_selector.convert_pointer_type(
491
492 // If we are changing the pointer, we generate code for creating a pointer
493 // to the substituted type instead
494 // TODO if we are comparing array types we need to compare their element
495 // types. this is for now done by implementing equality function especially
496 // for java types, technical debt TG-2707
498 {
499 // update generic_parameter_specialization_map for the new pointer
505 ns.follow(replacement_pointer_type.base_type()));
506
508 assignments, lifetime, replacement_pointer_type, depth, location);
509
510 // Having created a pointer to object of type replacement_pointer_type
511 // we now assign it back to the original pointer with a cast
512 // from pointer_type to replacement_pointer_type
513 assignments.add(code_frontend_assignt(
515 return;
516 }
517
518 // This deletes the recursion set entry on leaving this function scope,
519 // if one is set below.
521
522 // We need to prevent the possibility of this code to loop infinitely when
523 // initializing a data structure with recursive types or unbounded depth. We
524 // implement two mechanisms here. We keep a set of 'types seen', and
525 // detect when we perform a 2nd visit to the same type. We also detect the
526 // depth in the chain of (recursive) calls to the methods of this class.
527 // The depth counter is incremented only when a pointer is deferenced,
528 // including pointers to arrays.
529 //
530 // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
531 // the pointer to NULL instead of recursively initializing the struct to which
532 // it points.
534 const irep_idt &struct_tag = struct_type.get_tag();
535
536 // If this is a recursive type of some kind AND the depth is exceeded, set
537 // the pointer to null.
538 if(
539 !recursion_set_entry.insert_entry(struct_tag) &&
540 depth >= object_factory_parameters.max_nondet_tree_depth)
541 {
543 {
544 assignments.add(code_frontend_assignt{
545 expr, null_pointer_exprt{pointer_type}, location});
546 }
547 // Otherwise leave it as it is.
548 return;
549 }
550
551 // If we may be about to initialize a non-null enum type, always run the
552 // clinit_wrapper of its class first.
553 // TODO: TG-4689 we may want to do this for all types, not just enums, as
554 // described in the Java language specification:
555 // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
556 // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
557 // But we would have to put this behavior behind an option as it would have an
558 // impact on running times.
559 // Note that it would be more consistent with the behaviour of the JVM to only
560 // run clinit_wrapper if we are about to initialize an object of which we know
561 // for sure that it is not null on any following branch. However, adding this
562 // case in gen_nondet_struct_init would slow symex down too much, so if we
563 // decide to do this for all types, we should do it here.
564 // Note also that this logic is mirrored in
565 // ci_lazy_methodst::initialize_instantiated_classes.
566 if(
567 const auto class_type =
569 {
570 if(class_type->get_base("java::java.lang.Enum"))
571 {
572 const irep_idt &class_name = class_type->get_name();
573 const irep_idt class_clinit = clinit_wrapper_name(class_name);
575 assignments.add(code_function_callt{clinit_func->symbol_expr()});
576 }
577 }
578
581
582 // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
583 // emit to `update_in_place_assignments` code for in-place initialization of
584 // the object pointed by `expr`, assuming that such object is of type
585 // `subtype`
587 {
590 expr,
591 subtype,
592 lifetime,
593 depth,
595 location);
596 }
597
598 // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
599 // above to `assignments` and return
601 {
603 return;
604 }
605
606 // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
607 // vector of assignments that create a new object (recursively initializes it)
608 // and asign to `expr` the address of such object
610
613 expr,
614 subtype,
615 lifetime,
616 depth,
618 location);
619
621 expr, null_pointer_exprt{pointer_type}, location};
622
623 const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
624
625 if(!allow_null)
626 {
627 // Add the following code to assignments:
628 // <expr> = <aoe>;
630 }
631 else
632 {
633 // if(NONDET(_Bool)
634 // {
635 // <expr> = <null pointer>
636 // }
637 // else
638 // {
639 // <code from recursive call to gen_nondet_init() with
640 // tmp$<temporary_counter>>
641 // }
644 std::move(set_null_inst),
645 std::move(non_null_inst));
646
647 new_object_assignments.add(std::move(null_check));
648 }
649
650 // Similarly to above, maybe use a conditional if both the
651 // allocate-fresh and update-in-place cases are allowed:
653 {
654 assignments.append(new_object_assignments);
655 }
656 else
657 {
659 "No-update and must-update should have already been resolved");
660
664 std::move(new_object_assignments));
665
666 assignments.add(std::move(update_check));
667 }
668}
669
694 code_blockt &assignments,
695 lifetimet lifetime,
697 size_t depth,
698 const source_locationt &location)
699{
702 replacement_pointer, "tmp_object_factory");
703
704 // Generate a new object into this new symbol
706 assignments,
708 false, // is_sub
709 false, // skip_classid
710 lifetime,
711 {}, // no override_type
712 depth,
714 location);
715
716 return new_symbol_expr;
717}
718
730 const exprt &expr,
731 const std::list<std::string> &string_input_values,
732 symbol_table_baset &symbol_table)
733{
734 alternate_casest cases;
735 for(const auto &val : string_input_values)
736 {
737 const symbol_exprt s =
738 get_or_create_string_literal_symbol(val, symbol_table, true);
739 cases.push_back(code_frontend_assignt(expr, s));
740 }
741 return cases;
742}
743
766 code_blockt &assignments,
767 const exprt &expr,
768 bool is_sub,
769 bool skip_classid,
770 lifetimet lifetime,
772 size_t depth,
774 const source_locationt &location)
775{
776 const namespacet ns(symbol_table);
777 PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
778
779 typedef struct_typet::componentst componentst;
780 const irep_idt &struct_tag=struct_type.get_tag();
781
782 const componentst &components=struct_type.components();
783
784 // Should we write the whole object?
785 // * Not if this is a sub-structure (a superclass object), as our caller will
786 // have done this already
787 // * Not if the object has already been initialised by our caller, in which
788 // case they will set `skip_classid`
789 // * Not if we're re-initializing an existing object (i.e. update_in_place)
790 // * Always if it has a string type. Strings should not be partially updated,
791 // and the `length` and `data` components of string types need to be
792 // generated differently from object fields in the general case, see
793 // \ref java_object_factoryt::initialize_nondet_string_fields.
794
795 const bool has_string_input_values =
796 !object_factory_parameters.string_input_values.empty();
797
798 if(
801 { // We're dealing with a string and we should set fixed input values.
802 // We create a switch statement where each case is an assignment
803 // of one of the fixed input strings to the input variable in question
805 expr, object_factory_parameters.string_input_values, symbol_table);
806 assignments.add(generate_nondet_switch(
808 cases,
810 ID_java,
811 location,
812 symbol_table));
813 }
814 else if(
815 (!is_sub && !skip_classid &&
818 {
819 // Add an initial all-zero write. Most of the fields of this will be
820 // overwritten, but it helps to have a whole-structure write that analysis
821 // passes can easily recognise leaves no uninitialised state behind.
822
823 // This code mirrors the `remove_java_new` pass:
825 CHECK_RETURN(initial_object.has_value());
828 ns,
830
831 // If the initialised type is a special-cased String type (one with length
832 // and data fields introduced by string-library preprocessing), initialise
833 // those fields with nondet values
835 { // We're dealing with a string
838 assignments,
839 object_factory_parameters.min_nondet_string_length,
840 object_factory_parameters.max_nondet_string_length,
841 location,
842 object_factory_parameters.function_id,
844 object_factory_parameters.string_printable,
846 }
847
848 assignments.add(code_frontend_assignt(expr, *initial_object));
849 }
850
851 for(const auto &component : components)
852 {
853 const typet &component_type=component.type();
854 irep_idt name=component.get_name();
855
856 member_exprt me(expr, name, component_type);
857
859 {
860 continue;
861 }
862 else if(name == "cproverMonitorCount")
863 {
864 // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
865 // nondet. This field is only present when the java core models are
866 // included in the class-path. It is used to implement a critical section,
867 // which is necessary to support concurrency.
869 continue;
870 code_frontend_assignt code(me, from_integer(0, me.type()));
871 code.add_source_location() = location;
872 assignments.add(code);
873 }
874 else if(
875 is_java_string_type(struct_type) && (name == "length" || name == "data"))
876 {
877 // In this case these were set up above.
878 continue;
879 }
880 else
881 {
882 INVARIANT(!name.empty(), "Each component of a struct must have a name");
883
884 bool _is_sub=name[0]=='@';
885
886 // MUST_UPDATE_IN_PLACE only applies to this object.
887 // If this is a pointer to another object, offer the chance
888 // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
894 assignments,
895 me,
896 _is_sub,
897 false, // skip_classid
898 lifetime,
899 {}, // no override_type
900 depth,
902 location);
903 }
904 }
905
906 // If cproverNondetInitialize() can be found in the symbol table as a method
907 // on this class or any parent, we add a call:
908 // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
909 // expr.cproverNondetInitialize();
910 // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
911
915 "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true);
916
918 {
920 ns.lookup(cprover_nondet_initialize->get_full_component_identifier());
921 assignments.add(
923 {address_of_exprt{expr}}});
924 }
925}
926
942 const exprt &expr,
943 const typet &type,
944 const source_locationt &location,
946{
947 PRECONDITION(type == java_float_type() || type == java_double_type());
948
949 code_blockt assignments;
950
951 const auto &aux_int =
952 allocate_local_symbol(java_int_type(), "assume_integral_tmp");
953 assignments.add(code_declt(aux_int), location);
956 aux_assign.add_source_location() = location;
957 assignments.add(aux_assign);
958 assignments.add(
960
961 return assignments;
962}
963
1000 code_blockt &assignments,
1001 const exprt &expr,
1002 bool is_sub,
1003 bool skip_classid,
1004 lifetimet lifetime,
1006 size_t depth,
1008 const source_locationt &location)
1009{
1010 const typet &type = override_type.has_value() ? *override_type : expr.type();
1011 const namespacet ns(symbol_table);
1012 const typet &followed_type = ns.follow(type);
1013
1014 if(type.id()==ID_pointer)
1015 {
1016 // dereferenced type
1018
1019 // If we are about to initialize a generic pointer type, add its concrete
1020 // types to the map and delete them on leaving this function scope.
1026
1028 assignments,
1029 expr,
1030 lifetime,
1032 depth,
1034 location);
1035 }
1036 else if(followed_type.id() == ID_struct)
1037 {
1039
1040 // If we are about to initialize a generic class (as a superclass object
1041 // for a different object), add its concrete types to the map and delete
1042 // them on leaving this function scope.
1046 if(is_sub)
1047 {
1048 const typet &symbol =
1049 override_type.has_value() ? *override_type : expr.type();
1050 PRECONDITION(symbol.id() == ID_struct_tag);
1053 }
1054
1056 assignments,
1057 expr,
1058 is_sub,
1060 lifetime,
1062 depth,
1064 location);
1065 }
1066 else
1067 {
1068 // types different from pointer or structure:
1069 // bool, int, float, byte, char, ...
1070 exprt rhs = type.id() == ID_c_bool
1071 ? get_nondet_bool(type, location)
1072 : side_effect_expr_nondett(type, location);
1073 code_frontend_assignt assign(expr, rhs);
1074 assign.add_source_location() = location;
1075
1076 assignments.add(assign);
1077 if(type == java_char_type() && object_factory_parameters.string_printable)
1078 {
1079 assignments.add(
1081 }
1082 // add assumes to obey numerical restrictions
1083 if(type != java_boolean_type() && type != java_char_type())
1084 {
1085 const auto &interval = object_factory_parameters.assume_inputs_interval;
1086 if(auto singleton = interval.as_singleton())
1087 {
1088 assignments.add(
1089 code_frontend_assignt{expr, from_integer(*singleton, expr.type())});
1090 }
1091 else
1092 {
1093 exprt within_bounds = interval.make_contains_expr(expr);
1094 if(!within_bounds.is_true())
1095 assignments.add(code_assumet(std::move(within_bounds)));
1096 }
1097
1098 if(
1099 object_factory_parameters.assume_inputs_integral &&
1100 (type == java_float_type() || type == java_double_type()))
1101 {
1102 assignments.add(assume_expr_integral(
1103 expr,
1104 type,
1105 location,
1106 [this](
1107 const typet &type, std::string basename_prefix) -> symbol_exprt {
1109 type, basename_prefix);
1110 }));
1111 }
1112 }
1113 }
1114}
1115
1120
1125
1143 code_blockt &assignments,
1144 const exprt &lhs,
1145 const exprt &max_length_expr,
1146 const typet &element_type,
1148 const source_locationt &location)
1149{
1153 "nondet_array_length",
1154 location,
1156 assignments);
1157
1159 java_new_array.copy_to_operands(length_sym_expr);
1162 .subtype()
1163 .set(ID_element_type, element_type);
1165 assign.add_source_location() = location;
1166 assignments.add(assign);
1167}
1168
1187 code_blockt &assignments,
1188 const exprt &init_array_expr,
1189 const typet &element_type,
1190 const exprt &max_length_expr,
1191 const source_locationt &location,
1193{
1194 const array_typet array_type(element_type, max_length_expr);
1195
1196 // TYPE (*array_data_init)[max_length_expr];
1198 allocate_local_symbol(pointer_type(array_type), "array_data_init");
1199
1200 // array_data_init = ALLOCATE(TYPE [max_length_expr], max_length_expr, false);
1201 assignments.add(
1205 assignments.statements().back().add_source_location() = location;
1206
1207 // *array_data_init = NONDET(TYPE [max_length_expr]);
1210 assignments.add(
1212 assignments.statements().back().add_source_location() = location;
1213
1214 // init_array_expr = *array_data_init;
1217 assignments.add(
1219 assignments.statements().back().add_source_location() = location;
1220}
1221
1232 const exprt &element,
1234 const typet &element_type,
1235 const size_t depth,
1236 const source_locationt &location)
1237{
1238 code_blockt assignments;
1239 bool new_item_is_primitive = element.type().id() != ID_pointer;
1240
1241 // Use a temporary to initialise a new, or update an existing, non-primitive.
1242 // This makes it clearer that in a sequence like
1243 // `new_array_item->x = y; new_array_item->z = w;` that all the
1244 // `new_array_item` references must alias, cf. the harder-to-analyse
1245 // `some_expr[idx]->x = y; some_expr[idx]->z = w;`
1248 {
1249 init_expr = element;
1250 }
1251 else
1252 {
1254 element.type(), "new_array_item");
1255
1256 // If we're updating an existing array item, read the existing object that
1257 // we (may) alter:
1259 assignments.add(code_frontend_assignt(init_expr, element));
1260 }
1261
1262 // MUST_UPDATE_IN_PLACE only applies to this object.
1263 // If this is a pointer to another object, offer the chance
1264 // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1270 assignments,
1271 init_expr,
1272 false, // is_sub
1273 false, // skip_classid
1274 // These are variable in number, so use dynamic allocator:
1276 element_type, // override
1277 depth,
1279 location);
1280
1282 {
1283 // We used a temporary variable to update or initialise an array item;
1284 // now write it into the array:
1285 assignments.add(code_frontend_assignt(element, init_expr));
1286 }
1287 return assignments;
1288}
1289
1331 code_blockt &assignments,
1332 const exprt &init_array_expr,
1333 const exprt &length_expr,
1334 const typet &element_type,
1335 const exprt &max_length_expr,
1337 const source_locationt &location,
1340 const symbol_table_baset &symbol_table)
1341{
1343 allocate_local_symbol(init_array_expr.type(), "array_data_init");
1344
1346 data_assign.add_source_location() = location;
1347 assignments.add(data_assign);
1348
1349 const symbol_exprt &counter_expr =
1350 allocate_local_symbol(length_expr.type(), "array_init_iter");
1351
1354 {
1355 // Add a redundant if(counter == max_length) break
1356 // that is easier for the unwinder to understand.
1359
1360 loop_body.add(std::move(max_test));
1361 }
1362
1365
1366 loop_body.append(element_generator(element_at_counter, element_type));
1367
1372 std::move(loop_body),
1373 location));
1374}
1375
1377 const exprt &expr,
1379 const source_locationt &location,
1382 const symbol_table_baset &symbol_table,
1383 const size_t max_nondet_array_length)
1384{
1385 PRECONDITION(expr.type().id() == ID_pointer);
1386 PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_struct_tag);
1388
1389 code_blockt statements;
1390
1391 const namespacet ns(symbol_table);
1392 const typet &type = ns.follow(to_pointer_type(expr.type()).base_type());
1394 const typet &element_type = static_cast<const typet &>(
1395 to_pointer_type(expr.type()).base_type().find(ID_element_type));
1396
1397 auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
1398
1399 // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1400 // initialize its elements
1402 {
1404 statements,
1405 expr,
1407 element_type,
1409 location);
1410 }
1411
1412 // Otherwise we're updating the array in place, and use the
1413 // existing array allocation and length.
1414
1415 INVARIANT(
1417 "Java struct array does not conform to expectations");
1418
1420 const auto &comps = struct_type.components();
1421 const member_exprt length_expr(deref_expr, "length", comps[1].type());
1422 exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());
1423
1424 if(init_array_expr.type() != pointer_type(element_type))
1427
1428 if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
1429 {
1430 // For arrays of non-primitive type, nondeterministically initialize each
1431 // element of the array
1433 statements,
1436 element_type,
1439 location,
1442 symbol_table);
1443 }
1444 else
1445 {
1446 // Arrays of primitive type can be initialized with a single instruction.
1447 // We don't do this for arrays of primitive booleans, because booleans are
1448 // represented as unsigned bytes, so each cell must be initialized as
1449 // 0 or 1 (see gen_nondet_init).
1451 statements,
1453 element_type,
1455 location,
1457 }
1458 return statements;
1459}
1460
1475 code_blockt &assignments,
1476 const exprt &expr,
1478 const source_locationt &location)
1479{
1480 const irep_idt &class_name = java_class_type.get_name();
1481 const irep_idt values_name = id2string(class_name) + ".$VALUES";
1483 {
1485 << " is missing, so the corresponding Enum "
1486 "type will nondet initialised"
1487 << messaget::eom;
1488 return false;
1489 }
1490
1491 const namespacet ns(symbol_table);
1492 const symbolt &values = ns.lookup(values_name);
1493
1494 // Access members (length and data) of $VALUES array
1498 const auto &comps = deref_struct_type.components();
1499 const member_exprt length_expr(deref_expr, "length", comps[1].type());
1501 member_exprt(deref_expr, "data", comps[2].type());
1502
1506 "enum_index_init",
1507 location,
1509 assignments);
1510
1514 expr, typecast_exprt(element_at_index, expr.type()));
1515 assignments.add(enum_assign);
1516
1517 return true;
1518}
1519
1520static void assert_type_consistency(const code_blockt &assignments)
1521{
1522 // In future we'll be able to use codet::validate for this;
1523 // at present that only verifies `lhs.type base_type_eq right.type`,
1524 // whereas we want to check exact equality.
1525 for(const auto &code : assignments.statements())
1526 {
1527 if(code.get_statement() != ID_assign)
1528 continue;
1529 const auto &assignment = to_code_frontend_assign(code);
1530 INVARIANT(
1531 assignment.lhs().type() == assignment.rhs().type(),
1532 "object factory should produce type-consistent assignments");
1533 }
1534}
1535
1548 const typet &type,
1549 const irep_idt base_name,
1551 symbol_table_baset &symbol_table,
1553 lifetimet lifetime,
1554 const source_locationt &loc,
1555 const select_pointer_typet &pointer_type_selector,
1556 message_handlert &log)
1557{
1558 const symbolt &main_symbol = get_fresh_aux_symbol(
1559 type,
1561 id2string(base_name),
1562 loc,
1563 ID_java,
1564 symbol_table);
1565
1567
1568 exprt object=main_symbol.symbol_expr();
1569
1571 loc, parameters, symbol_table, pointer_type_selector, log);
1572 code_blockt assignments;
1573 state.gen_nondet_init(
1574 assignments,
1575 object,
1576 false, // is_sub
1577 false, // skip_classid
1578 lifetime,
1579 {}, // no override_type
1580 1, // initial depth
1582 loc);
1583
1584 state.add_created_symbol(main_symbol);
1586
1587 assert_type_consistency(assignments);
1588 init_code.append(assignments);
1589 return object;
1590}
1591
1625 const exprt &expr,
1627 symbol_table_baset &symbol_table,
1628 const source_locationt &loc,
1629 bool skip_classid,
1630 lifetimet lifetime,
1631 const java_object_factory_parameterst &object_factory_parameters,
1632 const select_pointer_typet &pointer_type_selector,
1634 message_handlert &log)
1635{
1637 loc, object_factory_parameters, symbol_table, pointer_type_selector, log);
1638 code_blockt assignments;
1639 state.gen_nondet_init(
1640 assignments,
1641 expr,
1642 false, // is_sub
1644 lifetime,
1645 {}, // no override_type
1646 1, // initial depth
1648 loc);
1649
1651
1652 assert_type_consistency(assignments);
1653 init_code.append(assignments);
1654}
1655
1658 const typet &type,
1659 const irep_idt base_name,
1661 symbol_table_baset &symbol_table,
1662 const java_object_factory_parameterst &object_factory_parameters,
1663 lifetimet lifetime,
1664 const source_locationt &location,
1665 message_handlert &log)
1666{
1667 select_pointer_typet pointer_type_selector;
1668 return object_factory(
1669 type,
1670 base_name,
1671 init_code,
1672 symbol_table,
1673 object_factory_parameters,
1674 lifetime,
1675 location,
1676 pointer_type_selector,
1677 log);
1678}
1679
1682 const exprt &expr,
1684 symbol_table_baset &symbol_table,
1685 const source_locationt &loc,
1686 bool skip_classid,
1687 lifetimet lifetime,
1688 const java_object_factory_parameterst &object_factory_parameters,
1690 message_handlert &log)
1691{
1692 select_pointer_typet pointer_type_selector;
1694 expr,
1695 init_code,
1696 symbol_table,
1697 loc,
1699 lifetime,
1700 object_factory_parameters,
1701 pointer_type_selector,
1703 log);
1704}
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)
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:240
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:707
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:86
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 goto_instruction_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:155
A codet representing an assignment in the program.
Definition std_code.h:24
goto_instruction_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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool empty() const
Definition dstring.h:90
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Array index operator.
Definition std_expr.h:1410
const irep_idt & id() const
Definition irep.h:396
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:2794
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:1006
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().
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
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.
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:1819
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
std::vector< componentt > componentst
Definition std_types.h:140
Expression to hold a symbol (variable)
Definition std_expr.h:113
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.
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:2017
The type of an expression, extends irept.
Definition type.h:29
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.
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_table_baset &symbol_table)
Create code to nondeterministically initialize each element of an array in a loop.
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_table_baset &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_...
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
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()
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
floatbv_typet java_double_type()
floatbv_typet java_float_type()
c_bool_typet java_boolean_type()
unsignedbv_typet java_char_type()
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,...
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:82
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
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
#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:77
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1842
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
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Author: Diffblue Ltd.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175