CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_object_factory.cpp Source File

CBMC
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
9#include "java_object_factory.h"
10
11#include <util/arith_tools.h>
12#include <util/array_element_from_pointer.h>
13#include <util/expr_initializer.h>
14#include <util/fresh_symbol.h>
15#include <util/interval_constraint.h>
16#include <util/message.h>
17#include <util/nondet_bool.h>
18#include <util/symbol_table_base.h>
19
20#include <goto-programs/class_identifier.h>
21#include <goto-programs/goto_functions.h>
22
23#include "generic_parameter_specialization_map_keys.h"
24#include "java_object_factory_parameters.h"
25#include "java_static_initializers.h"
26#include "java_string_library_preprocess.h"
27#include "java_string_literals.h"
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,
71 const source_locationt &location);
72public:
89
91 code_blockt &assignments,
92 const exprt &expr,
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 std::optional<typet> &override_type,
103 size_t depth,
105 const source_locationt &location);
106
107 void add_created_symbol(const symbolt &symbol);
108
110
111private:
113 code_blockt &assignments,
114 const exprt &expr,
115 lifetimet lifetime,
117 size_t depth,
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,
128 size_t depth,
130 const source_locationt &location);
131
133 code_blockt &assignments,
134 lifetimet lifetime,
136 size_t depth,
137 const source_locationt &location);
138
140 const exprt &element,
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,
196 const source_locationt &location)
197{
198 PRECONDITION(expr.type().id() == ID_pointer);
200
201 const namespacet ns(symbol_table);
202 const auto &target_class_type =
204 if(target_class_type.get_tag().starts_with("java::array["))
205 {
206 assignments.append(gen_nondet_array_init(
207 expr,
209 location,
210 [this, update_in_place, depth, location](
211 const exprt &element, const typet &element_type) -> code_blockt {
212 return assign_element(
213 element, update_in_place, element_type, depth + 1, location);
214 },
215 [this](const typet &type, std::string basename_prefix) -> symbol_exprt {
217 type, basename_prefix);
218 },
220 object_factory_parameters.max_nondet_array_length));
221 return;
222 }
223 if(target_class_type.get_base("java::java.lang.Enum"))
224 {
225 if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
226 return;
227 }
228
229 // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
230 // initialize the fields of the object pointed by `expr`; if in
231 // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
232 // (return value of `allocate_object`), emit a statement of the form
233 // `<expr> := address-of(<new-object>)` and recursively initialize such new
234 // object.
237 {
239 assignments, expr, target_type, lifetime, "tmp_object_factory");
240 }
241 else
242 {
243 if(expr.id() == ID_address_of)
244 init_expr = to_address_of_expr(expr).object();
245 else
246 {
248 }
249 }
250
252 assignments,
253 init_expr,
254 false, // is_sub
255 false, // skip_classid
256 lifetime,
257 {}, // no override type
258 depth + 1,
260 location);
261}
262
267{
269 std::unordered_set<irep_idt> &recursion_set;
272
273public:
277 explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
279 { }
280
287
290
295 bool insert_entry(const irep_idt &entry)
296 {
297 INVARIANT(erase_entry.empty(), "insert_entry should only be called once");
298 INVARIANT(!entry.empty(), "entry should be a struct tag");
299 bool ret=recursion_set.insert(entry).second;
300 if(ret)
301 {
302 // We added something, so erase it when this is destroyed:
303 erase_entry=entry;
304 }
305 return ret;
306 }
307};
308
311 const integer_intervalt printable_char_range(' ', '~');
312
315{
316 std::string result;
317 result += numeric_cast_v<char>(interval.lower);
318 result += "-";
319 result += numeric_cast_v<char>(interval.upper);
320 return result;
321}
322
364 code_blockt &code,
365 const std::size_t &min_nondet_string_length,
366 const std::size_t &max_nondet_string_length,
367 const source_locationt &loc,
368 const irep_idt &function_id,
369 symbol_table_baset &symbol_table,
370 bool printable,
371 allocate_objectst &allocate_objects)
372{
373 namespacet ns(symbol_table);
377
378 // We allow type StringBuffer and StringBuilder to be initialized
379 // in the same way has String, because they have the same structure and
380 // are treated in the same way by CBMC.
381
382 // Note that CharSequence cannot be used as classid because it's abstract,
383 // so it is replaced by String.
384 // \todo allow StringBuffer and StringBuilder as classid for Charsequence
385 if(struct_type.get_tag() == "java.lang.CharSequence")
386 {
388 struct_expr, ns, struct_tag_typet("java::java.lang.String"));
389 }
390
391 // OK, this is a String type with the expected fields -- add code to `code`
392 // to set up pre-requisite variables and assign them in `struct_expr`.
393
395 // length_expr = nondet(int);
397 allocate_objects.allocate_automatic_local_object(
398 java_int_type(), "tmp_object_factory");
401
402 // assume (length_expr >= min_nondet_string_length);
403 const exprt min_length =
404 from_integer(min_nondet_string_length, java_int_type());
406
407 // assume (length_expr <= max_input_length)
408 if(
409 max_nondet_string_length <=
410 to_integer_bitvector_type(length_expr.type()).largest())
411 {
413 from_integer(max_nondet_string_length, length_expr.type());
414 code.add(
416 }
417
418 const exprt data_expr =
419 make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
420 struct_expr.operands()[struct_type.component_number("length")] = length_expr;
421
424
426 array_pointer, data_expr, symbol_table, loc, function_id, code);
427
429 data_expr, length_expr, symbol_table, loc, function_id, code);
430
431 struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
432
433 // Printable ASCII characters are between ' ' and '~'.
434 if(printable)
435 {
440 symbol_table,
441 loc,
442 function_id,
443 code);
444 }
445}
446
472 code_blockt &assignments,
473 const exprt &expr,
474 lifetimet lifetime,
476 size_t depth,
478 const source_locationt &location)
479{
480 PRECONDITION(expr.type().id()==ID_pointer);
481 const namespacet ns(symbol_table);
483 pointer_type_selector.convert_pointer_type(
485
486 // If we are changing the pointer, we generate code for creating a pointer
487 // to the substituted type instead
488 // TODO if we are comparing array types we need to compare their element
489 // types. this is for now done by implementing equality function especially
490 // for java types, technical debt TG-2707
492 {
493 // update generic_parameter_specialization_map for the new pointer
500
502 assignments, lifetime, replacement_pointer_type, depth, location);
503
504 // Having created a pointer to object of type replacement_pointer_type
505 // we now assign it back to the original pointer with a cast
506 // from pointer_type to replacement_pointer_type
507 assignments.add(code_frontend_assignt(
509 return;
510 }
511
512 // This deletes the recursion set entry on leaving this function scope,
513 // if one is set below.
515
516 // We need to prevent the possibility of this code to loop infinitely when
517 // initializing a data structure with recursive types or unbounded depth. We
518 // implement two mechanisms here. We keep a set of 'types seen', and
519 // detect when we perform a 2nd visit to the same type. We also detect the
520 // depth in the chain of (recursive) calls to the methods of this class.
521 // The depth counter is incremented only when a pointer is deferenced,
522 // including pointers to arrays.
523 //
524 // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
525 // the pointer to NULL instead of recursively initializing the struct to which
526 // it points.
530 const irep_idt &struct_tag = struct_type.get_tag();
531
532 // If this is a recursive type of some kind AND the depth is exceeded, set
533 // the pointer to null.
534 if(
535 !recursion_set_entry.insert_entry(struct_tag) &&
536 depth >= object_factory_parameters.max_nondet_tree_depth)
537 {
539 {
540 assignments.add(code_frontend_assignt{
541 expr, null_pointer_exprt{pointer_type}, location});
542 }
543 // Otherwise leave it as it is.
544 return;
545 }
546
547 // If we may be about to initialize a non-null enum type, always run the
548 // clinit_wrapper of its class first.
549 // TODO: TG-4689 we may want to do this for all types, not just enums, as
550 // described in the Java language specification:
551 // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
552 // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
553 // But we would have to put this behavior behind an option as it would have an
554 // impact on running times.
555 // Note that it would be more consistent with the behaviour of the JVM to only
556 // run clinit_wrapper if we are about to initialize an object of which we know
557 // for sure that it is not null on any following branch. However, adding this
558 // case in gen_nondet_struct_init would slow symex down too much, so if we
559 // decide to do this for all types, we should do it here.
560 // Note also that this logic is mirrored in
561 // ci_lazy_methodst::initialize_instantiated_classes.
562 if(
563 const auto class_type =
565 {
566 if(class_type->get_base("java::java.lang.Enum"))
567 {
568 const irep_idt &class_name = class_type->get_name();
569 const irep_idt class_clinit = clinit_wrapper_name(class_name);
571 assignments.add(code_function_callt{clinit_func->symbol_expr()});
572 }
573 }
574
577
578 // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
579 // emit to `update_in_place_assignments` code for in-place initialization of
580 // the object pointed by `expr`, assuming that such object is of type
581 // `tag_type`
583 {
586 expr,
587 tag_type,
588 lifetime,
589 depth,
591 location);
592 }
593
594 // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
595 // above to `assignments` and return
597 {
599 return;
600 }
601
602 // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
603 // vector of assignments that create a new object (recursively initializes it)
604 // and asign to `expr` the address of such object
606
609 expr,
610 tag_type,
611 lifetime,
612 depth,
614 location);
615
617 expr, null_pointer_exprt{pointer_type}, location};
618
619 const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
620
621 if(!allow_null)
622 {
623 // Add the following code to assignments:
624 // <expr> = <aoe>;
626 }
627 else
628 {
629 // if(NONDET(_Bool)
630 // {
631 // <expr> = <null pointer>
632 // }
633 // else
634 // {
635 // <code from recursive call to gen_nondet_init() with
636 // tmp$<temporary_counter>>
637 // }
640 std::move(set_null_inst),
641 std::move(non_null_inst));
642
643 new_object_assignments.add(std::move(null_check));
644 }
645
646 // Similarly to above, maybe use a conditional if both the
647 // allocate-fresh and update-in-place cases are allowed:
649 {
650 assignments.append(new_object_assignments);
651 }
652 else
653 {
655 "No-update and must-update should have already been resolved");
656
660 std::move(new_object_assignments));
661
662 assignments.add(std::move(update_check));
663 }
664}
665
690 code_blockt &assignments,
691 lifetimet lifetime,
693 size_t depth,
694 const source_locationt &location)
695{
698 replacement_pointer, "tmp_object_factory");
699
700 // Generate a new object into this new symbol
702 assignments,
704 false, // is_sub
705 false, // skip_classid
706 lifetime,
707 {}, // no override_type
708 depth,
710 location);
711
712 return new_symbol_expr;
713}
714
726 const exprt &expr,
727 const std::list<std::string> &string_input_values,
728 symbol_table_baset &symbol_table)
729{
730 alternate_casest cases;
731 for(const auto &val : string_input_values)
732 {
733 const symbol_exprt s =
734 get_or_create_string_literal_symbol(val, symbol_table, true);
735 cases.push_back(code_frontend_assignt(expr, s));
736 }
737 return cases;
738}
739
762 code_blockt &assignments,
763 const exprt &expr,
764 bool is_sub,
765 bool skip_classid,
766 lifetimet lifetime,
768 size_t depth,
770 const source_locationt &location)
771{
772 const namespacet ns(symbol_table);
773 PRECONDITION(expr.type().id() == ID_struct_tag);
774
775 typedef struct_typet::componentst componentst;
776 const irep_idt &struct_tag=struct_type.get_tag();
777
778 const componentst &components=struct_type.components();
779
780 // Should we write the whole object?
781 // * Not if this is a sub-structure (a superclass object), as our caller will
782 // have done this already
783 // * Not if the object has already been initialised by our caller, in which
784 // case they will set `skip_classid`
785 // * Not if we're re-initializing an existing object (i.e. update_in_place)
786 // * Always if it has a string type. Strings should not be partially updated,
787 // and the `length` and `data` components of string types need to be
788 // generated differently from object fields in the general case, see
789 // \ref java_object_factoryt::initialize_nondet_string_fields.
790
791 const bool has_string_input_values =
792 !object_factory_parameters.string_input_values.empty();
793
794 if(
797 { // We're dealing with a string and we should set fixed input values.
798 // We create a switch statement where each case is an assignment
799 // of one of the fixed input strings to the input variable in question
801 expr, object_factory_parameters.string_input_values, symbol_table);
802 assignments.add(generate_nondet_switch(
804 cases,
806 ID_java,
807 location,
808 symbol_table));
809 }
810 else if(
811 (!is_sub && !skip_classid &&
814 {
815 // Add an initial all-zero write. Most of the fields of this will be
816 // overwritten, but it helps to have a whole-structure write that analysis
817 // passes can easily recognise leaves no uninitialised state behind.
818
819 // This code mirrors the `remove_java_new` pass:
821 CHECK_RETURN(initial_object.has_value());
824 ns,
826
827 // If the initialised type is a special-cased String type (one with length
828 // and data fields introduced by string-library preprocessing), initialise
829 // those fields with nondet values
831 { // We're dealing with a string
834 assignments,
835 object_factory_parameters.min_nondet_string_length,
836 object_factory_parameters.max_nondet_string_length,
837 location,
838 object_factory_parameters.function_id,
840 object_factory_parameters.string_printable,
842 }
843
844 assignments.add(code_frontend_assignt(expr, *initial_object));
845 }
846
847 for(const auto &component : components)
848 {
849 const typet &component_type=component.type();
850 irep_idt name=component.get_name();
851
852 member_exprt me(expr, name, component_type);
853
855 {
856 continue;
857 }
858 else if(name == "cproverMonitorCount")
859 {
860 // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
861 // nondet. This field is only present when the java core models are
862 // included in the class-path. It is used to implement a critical section,
863 // which is necessary to support concurrency.
865 continue;
866 code_frontend_assignt code(me, from_integer(0, me.type()));
867 code.add_source_location() = location;
868 assignments.add(code);
869 }
870 else if(
871 is_java_string_type(struct_type) && (name == "length" || name == "data"))
872 {
873 // In this case these were set up above.
874 continue;
875 }
876 else
877 {
878 INVARIANT(!name.empty(), "Each component of a struct must have a name");
879
880 bool _is_sub=name[0]=='@';
881
882 // MUST_UPDATE_IN_PLACE only applies to this object.
883 // If this is a pointer to another object, offer the chance
884 // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
890 assignments,
891 me,
892 _is_sub,
893 false, // skip_classid
894 lifetime,
895 {}, // no override_type
896 depth,
898 location);
899 }
900 }
901
902 // If cproverNondetInitialize() can be found in the symbol table as a method
903 // on this class or any parent, we add a call:
904 // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 // expr.cproverNondetInitialize();
906 // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
907
909 std::optional<resolve_inherited_componentt::inherited_componentt>
911 "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true);
912
914 {
916 ns.lookup(cprover_nondet_initialize->get_full_component_identifier());
917 assignments.add(
919 {address_of_exprt{expr}}});
920 }
921}
922
938 const exprt &expr,
939 const typet &type,
940 const source_locationt &location,
942{
943 PRECONDITION(type == java_float_type() || type == java_double_type());
944
945 code_blockt assignments;
946
947 const auto &aux_int =
948 allocate_local_symbol(java_int_type(), "assume_integral_tmp");
949 assignments.add(code_declt(aux_int), location);
952 aux_assign.add_source_location() = location;
953 assignments.add(aux_assign);
954 assignments.add(
956
957 return assignments;
958}
959
996 code_blockt &assignments,
997 const exprt &expr,
998 bool is_sub,
999 bool skip_classid,
1000 lifetimet lifetime,
1001 const std::optional<typet> &override_type,
1002 size_t depth,
1004 const source_locationt &location)
1005{
1006 const typet &type = override_type.has_value() ? *override_type : expr.type();
1007 const namespacet ns(symbol_table);
1008
1009 if(type.id()==ID_pointer)
1010 {
1011 // dereferenced type
1013
1014 // If we are about to initialize a generic pointer type, add its concrete
1015 // types to the map and delete them on leaving this function scope.
1022
1024 assignments,
1025 expr,
1026 lifetime,
1028 depth,
1030 location);
1031 }
1032 else if(type.id() == ID_struct_tag)
1033 {
1035
1036 // If we are about to initialize a generic class (as a superclass object
1037 // for a different object), add its concrete types to the map and delete
1038 // them on leaving this function scope.
1042 if(is_sub)
1043 {
1044 const typet &symbol =
1045 override_type.has_value() ? *override_type : expr.type();
1046 PRECONDITION(symbol.id() == ID_struct_tag);
1049 }
1050
1052 assignments,
1053 expr,
1054 is_sub,
1056 lifetime,
1058 depth,
1060 location);
1061 }
1062 else
1063 {
1064 // types different from pointer or structure:
1065 // bool, int, float, byte, char, ...
1066 exprt rhs = type.id() == ID_c_bool
1067 ? get_nondet_bool(type, location)
1068 : side_effect_expr_nondett(type, location);
1069 code_frontend_assignt assign(expr, rhs);
1070 assign.add_source_location() = location;
1071
1072 assignments.add(assign);
1073 if(type == java_char_type() && object_factory_parameters.string_printable)
1074 {
1075 assignments.add(
1077 }
1078 // add assumes to obey numerical restrictions
1079 if(type != java_boolean_type() && type != java_char_type())
1080 {
1081 const auto &interval = object_factory_parameters.assume_inputs_interval;
1082 if(auto singleton = interval.as_singleton())
1083 {
1084 assignments.add(
1085 code_frontend_assignt{expr, from_integer(*singleton, expr.type())});
1086 }
1087 else
1088 {
1089 exprt within_bounds = interval.make_contains_expr(expr);
1090 if(within_bounds != true)
1091 assignments.add(code_assumet(std::move(within_bounds)));
1092 }
1093
1094 if(
1095 object_factory_parameters.assume_inputs_integral &&
1096 (type == java_float_type() || type == java_double_type()))
1097 {
1098 assignments.add(assume_expr_integral(
1099 expr,
1100 type,
1101 location,
1102 [this](
1103 const typet &type, std::string basename_prefix) -> symbol_exprt {
1105 type, basename_prefix);
1106 }));
1107 }
1108 }
1109 }
1110}
1111
1116
1121
1139 code_blockt &assignments,
1140 const exprt &lhs,
1141 const exprt &max_length_expr,
1142 const typet &element_type,
1144 const source_locationt &location)
1145{
1149 "nondet_array_length",
1150 location,
1152 assignments);
1153
1155 java_new_array.copy_to_operands(length_sym_expr);
1158 .subtype()
1159 .set(ID_element_type, element_type);
1161 assign.add_source_location() = location;
1162 assignments.add(assign);
1163}
1164
1183 code_blockt &assignments,
1184 const exprt &init_array_expr,
1185 const typet &element_type,
1186 const exprt &max_length_expr,
1187 const source_locationt &location,
1189{
1190 const array_typet array_type(element_type, max_length_expr);
1191
1192 // TYPE (*array_data_init)[max_length_expr];
1194 allocate_local_symbol(pointer_type(array_type), "array_data_init");
1195
1196 // array_data_init = ALLOCATE(TYPE [max_length_expr], max_length_expr, false);
1197 assignments.add(
1201 assignments.statements().back().add_source_location() = location;
1202
1203 // *array_data_init = NONDET(TYPE [max_length_expr]);
1206 assignments.add(
1208 assignments.statements().back().add_source_location() = location;
1209
1210 // init_array_expr = *array_data_init;
1213 assignments.add(
1215 assignments.statements().back().add_source_location() = location;
1216}
1217
1228 const exprt &element,
1230 const typet &element_type,
1231 const size_t depth,
1232 const source_locationt &location)
1233{
1234 code_blockt assignments;
1235 bool new_item_is_primitive = element.type().id() != ID_pointer;
1236
1237 // Use a temporary to initialise a new, or update an existing, non-primitive.
1238 // This makes it clearer that in a sequence like
1239 // `new_array_item->x = y; new_array_item->z = w;` that all the
1240 // `new_array_item` references must alias, cf. the harder-to-analyse
1241 // `some_expr[idx]->x = y; some_expr[idx]->z = w;`
1244 {
1245 init_expr = element;
1246 }
1247 else
1248 {
1250 element.type(), "new_array_item");
1251
1252 // If we're updating an existing array item, read the existing object that
1253 // we (may) alter:
1255 assignments.add(code_frontend_assignt(init_expr, element));
1256 }
1257
1258 // MUST_UPDATE_IN_PLACE only applies to this object.
1259 // If this is a pointer to another object, offer the chance
1260 // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1266 assignments,
1267 init_expr,
1268 false, // is_sub
1269 false, // skip_classid
1270 // These are variable in number, so use dynamic allocator:
1272 element_type, // override
1273 depth,
1275 location);
1276
1278 {
1279 // We used a temporary variable to update or initialise an array item;
1280 // now write it into the array:
1281 assignments.add(code_frontend_assignt(element, init_expr));
1282 }
1283 return assignments;
1284}
1285
1327 code_blockt &assignments,
1328 const exprt &init_array_expr,
1329 const exprt &length_expr,
1330 const typet &element_type,
1331 const exprt &max_length_expr,
1333 const source_locationt &location,
1336 const symbol_table_baset &symbol_table)
1337{
1339 allocate_local_symbol(init_array_expr.type(), "array_data_init");
1340
1342 data_assign.add_source_location() = location;
1343 assignments.add(data_assign);
1344
1345 const symbol_exprt &counter_expr =
1346 allocate_local_symbol(length_expr.type(), "array_init_iter");
1347
1350 {
1351 // Add a redundant if(counter == max_length) break
1352 // that is easier for the unwinder to understand.
1355
1356 loop_body.add(std::move(max_test));
1357 }
1358
1361
1362 loop_body.append(element_generator(element_at_counter, element_type));
1363
1368 std::move(loop_body),
1369 location));
1370}
1371
1373 const exprt &expr,
1375 const source_locationt &location,
1378 const symbol_table_baset &symbol_table,
1379 const size_t max_nondet_array_length)
1380{
1381 PRECONDITION(expr.type().id() == ID_pointer);
1382 PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_struct_tag);
1384
1385 code_blockt statements;
1386
1387 const namespacet ns(symbol_table);
1388 const struct_typet &struct_type =
1389 ns.follow_tag(to_struct_tag_type(to_pointer_type(expr.type()).base_type()));
1390 const typet &element_type = static_cast<const typet &>(
1391 to_pointer_type(expr.type()).base_type().find(ID_element_type));
1392
1393 auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
1394
1395 // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1396 // initialize its elements
1398 {
1400 statements,
1401 expr,
1403 element_type,
1405 location);
1406 }
1407
1408 // Otherwise we're updating the array in place, and use the
1409 // existing array allocation and length.
1410
1411 INVARIANT(
1413 "Java struct array does not conform to expectations");
1414
1416 const auto &comps = struct_type.components();
1417 const member_exprt length_expr(deref_expr, "length", comps[1].type());
1418 exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());
1419
1420 if(init_array_expr.type() != pointer_type(element_type))
1423
1424 if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
1425 {
1426 // For arrays of non-primitive type, nondeterministically initialize each
1427 // element of the array
1429 statements,
1432 element_type,
1435 location,
1438 symbol_table);
1439 }
1440 else
1441 {
1442 // Arrays of primitive type can be initialized with a single instruction.
1443 // We don't do this for arrays of primitive booleans, because booleans are
1444 // represented as unsigned bytes, so each cell must be initialized as
1445 // 0 or 1 (see gen_nondet_init).
1447 statements,
1449 element_type,
1451 location,
1453 }
1454 return statements;
1455}
1456
1471 code_blockt &assignments,
1472 const exprt &expr,
1474 const source_locationt &location)
1475{
1476 const irep_idt &class_name = java_class_type.get_name();
1477 const irep_idt values_name = id2string(class_name) + ".$VALUES";
1479 {
1480 log.warning() << values_name
1481 << " is missing, so the corresponding Enum "
1482 "type will nondet initialised"
1483 << messaget::eom;
1484 return false;
1485 }
1486
1487 const namespacet ns(symbol_table);
1488 const symbolt &values = ns.lookup(values_name);
1489
1490 // Access members (length and data) of $VALUES array
1492 const auto &deref_struct_type =
1495 const auto &comps = deref_struct_type.components();
1496 const member_exprt length_expr(deref_expr, "length", comps[1].type());
1498 member_exprt(deref_expr, "data", comps[2].type());
1499
1503 "enum_index_init",
1504 location,
1506 assignments);
1507
1511 expr, typecast_exprt(element_at_index, expr.type()));
1512 assignments.add(enum_assign);
1513
1514 return true;
1515}
1516
1517 static void assert_type_consistency(const code_blockt &assignments)
1518{
1519 // In future we'll be able to use codet::validate for this;
1520 // at present that only verifies `lhs.type base_type_eq right.type`,
1521 // whereas we want to check exact equality.
1522 for(const auto &code : assignments.statements())
1523 {
1524 if(code.get_statement() != ID_assign)
1525 continue;
1526 const auto &assignment = to_code_frontend_assign(code);
1527 INVARIANT(
1528 assignment.lhs().type() == assignment.rhs().type(),
1529 "object factory should produce type-consistent assignments");
1530 }
1531}
1532
1545 const typet &type,
1546 const irep_idt base_name,
1548 symbol_table_baset &symbol_table,
1550 lifetimet lifetime,
1551 const source_locationt &loc,
1552 const select_pointer_typet &pointer_type_selector,
1554{
1555 const symbolt &main_symbol = get_fresh_aux_symbol(
1556 type,
1558 id2string(base_name),
1559 loc,
1560 ID_java,
1561 symbol_table);
1562
1564
1565 exprt object=main_symbol.symbol_expr();
1566
1568 loc, parameters, symbol_table, pointer_type_selector, log);
1569 code_blockt assignments;
1570 state.gen_nondet_init(
1571 assignments,
1572 object,
1573 false, // is_sub
1574 false, // skip_classid
1575 lifetime,
1576 {}, // no override_type
1577 1, // initial depth
1579 loc);
1580
1581 state.add_created_symbol(main_symbol);
1583
1584 assert_type_consistency(assignments);
1585 init_code.append(assignments);
1586 return object;
1587}
1588
1622 const exprt &expr,
1624 symbol_table_baset &symbol_table,
1625 const source_locationt &loc,
1626 bool skip_classid,
1627 lifetimet lifetime,
1628 const java_object_factory_parameterst &object_factory_parameters,
1629 const select_pointer_typet &pointer_type_selector,
1632{
1634 loc, object_factory_parameters, symbol_table, pointer_type_selector, log);
1635 code_blockt assignments;
1636 state.gen_nondet_init(
1637 assignments,
1638 expr,
1639 false, // is_sub
1641 lifetime,
1642 {}, // no override_type
1643 1, // initial depth
1645 loc);
1646
1648
1649 assert_type_consistency(assignments);
1650 init_code.append(assignments);
1651}
1652
1655 const typet &type,
1656 const irep_idt base_name,
1658 symbol_table_baset &symbol_table,
1659 const java_object_factory_parameterst &object_factory_parameters,
1660 lifetimet lifetime,
1661 const source_locationt &location,
1663{
1664 select_pointer_typet pointer_type_selector;
1665 return object_factory(
1666 type,
1667 base_name,
1668 init_code,
1669 symbol_table,
1670 object_factory_parameters,
1671 lifetime,
1672 location,
1673 pointer_type_selector,
1674 log);
1675}
1676
1679 const exprt &expr,
1681 symbol_table_baset &symbol_table,
1682 const source_locationt &loc,
1683 bool skip_classid,
1684 lifetimet lifetime,
1685 const java_object_factory_parameterst &object_factory_parameters,
1688{
1689 select_pointer_typet pointer_type_selector;
1691 expr,
1692 init_code,
1693 symbol_table,
1694 loc,
1696 lifetime,
1697 object_factory_parameters,
1698 pointer_type_selector,
1700 log);
1701}
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:235
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:540
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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:806
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:784
The Boolean type.
Definition std_types.h:35
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.
Definition pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:101
Equality.
Definition std_expr.h:1339
Base class for all expressions.
Definition expr.h:57
typet & type()
Return the type of the expression.
Definition expr.h:85
const source_locationt & source_location() const
Definition expr.h:236
source_locationt & add_source_location()
Definition expr.h:241
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:1431
const irep_idt & id() const
Definition irep.h:388
Definition java_types.h:196
void gen_nondet_init(code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const std::optional< 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...
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,...
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:2866
Definition message.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & warning() const
Definition message.h:406
static eomt eom
Definition message.h:289
Binary minus.
Definition std_expr.h:1065
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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:134
The null pointer constant.
Definition pointer_expr.h:909
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.
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:1820
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:492
Structure type, corresponds to C style structs.
Definition std_types.h:230
std::vector< componentt > componentst
Definition std_types.h:139
Expression to hold a symbol (variable)
Definition std_expr.h:132
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:1995
The type of an expression, extends irept.
Definition type.h:29
std::optional< 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.
Author: Diffblue Ltd.
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:44
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
update_in_placet
@ MAY_UPDATE_IN_PLACE
@ NO_UPDATE_IN_PLACE
@ MUST_UPDATE_IN_PLACE
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:838
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:895
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:581
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:27
double log(double x)
Definition math.c:2416
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:83
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition nondet.h:19
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.
Definition pointer_expr.h:577
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition pointer_expr.h:93
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:291
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1843
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:517
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:208

AltStyle によって変換されたページ (->オリジナル) /