cprover
java_object_factory.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_object_factory.h"
10 
12 #include <util/expr_initializer.h>
13 #include <util/nondet.h>
14 #include <util/nondet_bool.h>
16 #include <util/prefix.h>
17 
21 
23 #include "java_root_class.h"
24 #include "java_string_literals.h"
25 #include "java_utils.h"
26 
28 {
30 
35  std::unordered_set<irep_idt> recursion_set;
36 
46 
49 
54 
56 
59 
61  code_blockt &assignments,
62  const exprt &expr,
63  const typet &target_type,
64  lifetimet lifetime,
65  size_t depth,
66  update_in_placet update_in_place,
67  const source_locationt &location);
68 public:
70  const source_locationt &loc,
71  const java_object_factory_parameterst _object_factory_parameters,
72  symbol_table_baset &_symbol_table,
75  : object_factory_parameters(_object_factory_parameters),
76  symbol_table(_symbol_table),
79  ID_java,
80  loc,
81  object_factory_parameters.function_id,
82  symbol_table),
83  log(log)
84  {}
85 
87  code_blockt &assignments,
88  const exprt &expr,
89  const java_class_typet &java_class_type,
90  const source_locationt &location);
91 
92  void gen_nondet_init(
93  code_blockt &assignments,
94  const exprt &expr,
95  bool is_sub,
96  bool skip_classid,
97  lifetimet lifetime,
98  const optionalt<typet> &override_type,
99  size_t depth,
101  const source_locationt &location);
102 
103  void add_created_symbol(const symbolt *symbol);
104 
105  void declare_created_symbols(code_blockt &init_code);
106 
107 private:
109  code_blockt &assignments,
110  const exprt &expr,
111  lifetimet lifetime,
113  size_t depth,
114  const update_in_placet &update_in_place,
115  const source_locationt &location);
116 
118  code_blockt &assignments,
119  const exprt &expr,
120  bool is_sub,
121  bool skip_classid,
122  lifetimet lifetime,
123  const struct_typet &struct_type,
124  size_t depth,
125  const update_in_placet &update_in_place,
126  const source_locationt &location);
127 
129  code_blockt &assignments,
130  lifetimet lifetime,
131  const pointer_typet &substitute_pointer_type,
132  size_t depth,
133  const source_locationt &location);
134 
136  const exprt &element,
137  update_in_placet update_in_place,
138  const typet &element_type,
139  size_t depth,
140  const source_locationt &location);
141 };
142 
186  code_blockt &assignments,
187  const exprt &expr,
188  const typet &target_type,
189  lifetimet lifetime,
190  size_t depth,
191  update_in_placet update_in_place,
192  const source_locationt &location)
193 {
194  PRECONDITION(expr.type().id() == ID_pointer);
196 
197  const namespacet ns(symbol_table);
198  const typet &followed_target_type = ns.follow(target_type);
199  PRECONDITION(followed_target_type.id() == ID_struct);
200 
201  const auto &target_class_type = to_java_class_type(followed_target_type);
202  if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
203  {
204  assignments.append(gen_nondet_array_init(
205  expr,
206  update_in_place,
207  location,
208  [this, update_in_place, depth, location](
209  const exprt &element, const typet &element_type) -> code_blockt {
210  return assign_element(
211  element, update_in_place, element_type, depth + 1, location);
212  },
213  [this](const typet &type, std::string basename_prefix) -> symbol_exprt {
215  type, basename_prefix);
216  },
217  symbol_table,
219  return;
220  }
221  if(target_class_type.get_base("java::java.lang.Enum"))
222  {
223  if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
224  return;
225  }
226 
227  // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
228  // initialize the fields of the object pointed by `expr`; if in
229  // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
230  // (return value of `allocate_object`), emit a statement of the form
231  // `<expr> := address-of(<new-object>)` and recursively initialize such new
232  // object.
233  exprt init_expr;
234  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
235  {
236  init_expr = allocate_objects.allocate_object(
237  assignments, expr, target_type, lifetime, "tmp_object_factory");
238  }
239  else
240  {
241  if(expr.id() == ID_address_of)
242  init_expr = to_address_of_expr(expr).object();
243  else
244  {
245  init_expr = dereference_exprt(expr);
246  }
247  }
248 
250  assignments,
251  init_expr,
252  false, // is_sub
253  false, // skip_classid
254  lifetime,
255  {}, // no override type
256  depth + 1,
257  update_in_place,
258  location);
259 }
260 
265 {
267  std::unordered_set<irep_idt> &recursion_set;
270 
271 public:
275  explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
276  : recursion_set(_recursion_set)
277  { }
278 
281  {
282  if(!erase_entry.empty())
283  recursion_set.erase(erase_entry);
284  }
285 
288 
293  bool insert_entry(const irep_idt &entry)
294  {
295  INVARIANT(erase_entry.empty(), "insert_entry should only be called once");
296  INVARIANT(!entry.empty(), "entry should be a struct tag");
297  bool ret=recursion_set.insert(entry).second;
298  if(ret)
299  {
300  // We added something, so erase it when this is destroyed:
301  erase_entry=entry;
302  }
303  return ret;
304  }
305 };
306 
310 
313 {
314  std::string result;
315  result += numeric_cast_v<char>(interval.lower);
316  result += "-";
317  result += numeric_cast_v<char>(interval.upper);
318  return result;
319 }
320 
361  struct_exprt &struct_expr,
362  code_blockt &code,
363  const std::size_t &min_nondet_string_length,
364  const std::size_t &max_nondet_string_length,
365  const source_locationt &loc,
366  const irep_idt &function_id,
367  symbol_table_baset &symbol_table,
368  bool printable,
369  allocate_objectst &allocate_objects)
370 {
371  namespacet ns(symbol_table);
372  const struct_typet &struct_type =
373  to_struct_type(ns.follow(struct_expr.type()));
374  PRECONDITION(is_java_string_type(struct_type));
375 
376  // We allow type StringBuffer and StringBuilder to be initialized
377  // in the same way has String, because they have the same structure and
378  // are treated in the same way by CBMC.
379 
380  // Note that CharSequence cannot be used as classid because it's abstract,
381  // so it is replaced by String.
382  // \todo allow StringBuffer and StringBuilder as classid for Charsequence
383  if(struct_type.get_tag() == "java.lang.CharSequence")
384  {
386  struct_expr, ns, struct_tag_typet("java::java.lang.String"));
387  }
388 
389  // OK, this is a String type with the expected fields -- add code to `code`
390  // to set up pre-requisite variables and assign them in `struct_expr`.
391 
393  // length_expr = nondet(int);
394  const symbol_exprt length_expr =
395  allocate_objects.allocate_automatic_local_object(
396  java_int_type(), "tmp_object_factory");
397  const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
398  code.add(code_assignt(length_expr, nondet_length));
399 
400  // assume (length_expr >= min_nondet_string_length);
401  const exprt min_length =
402  from_integer(min_nondet_string_length, java_int_type());
403  code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
404 
405  // assume (length_expr <= max_input_length)
406  if(
407  max_nondet_string_length <=
408  to_integer_bitvector_type(length_expr.type()).largest())
409  {
410  exprt max_length =
411  from_integer(max_nondet_string_length, length_expr.type());
412  code.add(
413  code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
414  }
415 
416  const exprt data_expr =
417  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
418  struct_expr.operands()[struct_type.component_number("length")] = length_expr;
419 
420  const address_of_exprt array_pointer(
421  index_exprt(data_expr, from_integer(0, java_int_type())));
422 
424  array_pointer, data_expr, symbol_table, loc, function_id, code);
425 
427  data_expr, length_expr, symbol_table, loc, function_id, code);
428 
429  struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
430 
431  // Printable ASCII characters are between ' ' and '~'.
432  if(printable)
433  {
435  array_pointer,
436  length_expr,
438  symbol_table,
439  loc,
440  function_id,
441  code);
442  }
443 }
444 
470  code_blockt &assignments,
471  const exprt &expr,
472  lifetimet lifetime,
474  size_t depth,
475  const update_in_placet &update_in_place,
476  const source_locationt &location)
477 {
478  PRECONDITION(expr.type().id()==ID_pointer);
479  const namespacet ns(symbol_table);
480  const typet &subtype = pointer_type.subtype();
481  const typet &followed_subtype = ns.follow(subtype);
482  PRECONDITION(followed_subtype.id() == ID_struct);
483  const pointer_typet &replacement_pointer_type =
486 
487  // If we are changing the pointer, we generate code for creating a pointer
488  // to the substituted type instead
489  // TODO if we are comparing array types we need to compare their element
490  // types. this is for now done by implementing equality function especially
491  // for java types, technical debt TG-2707
492  if(!equal_java_types(replacement_pointer_type, pointer_type))
493  {
494  // update generic_parameter_specialization_map for the new pointer
496  generic_parameter_specialization_map_keys(
498  generic_parameter_specialization_map_keys.insert(
499  replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
500 
501  const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
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(
508  code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
509  return;
510  }
511 
512  // This deletes the recursion set entry on leaving this function scope,
513  // if one is set below.
514  recursion_set_entryt recursion_set_entry(recursion_set);
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.
527  const struct_typet &struct_type = to_struct_type(followed_subtype);
528  const irep_idt &struct_tag = struct_type.get_tag();
529 
530  // If this is a recursive type of some kind AND the depth is exceeded, set
531  // the pointer to null.
532  if(
533  !recursion_set_entry.insert_entry(struct_tag) &&
535  {
536  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
537  {
538  assignments.add(
539  code_assignt{expr, null_pointer_exprt{pointer_type}, location});
540  }
541  // Otherwise leave it as it is.
542  return;
543  }
544 
545  // If we may be about to initialize a non-null enum type, always run the
546  // clinit_wrapper of its class first.
547  // TODO: TG-4689 we may want to do this for all types, not just enums, as
548  // described in the Java language specification:
549  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
550  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
551  // But we would have to put this behavior behind an option as it would have an
552  // impact on running times.
553  // Note that it would be more consistent with the behaviour of the JVM to only
554  // run clinit_wrapper if we are about to initialize an object of which we know
555  // for sure that it is not null on any following branch. However, adding this
556  // case in gen_nondet_struct_init would slow symex down too much, so if we
557  // decide to do this for all types, we should do it here.
558  // Note also that this logic is mirrored in
559  // ci_lazy_methodst::initialize_instantiated_classes.
560  if(
561  const auto class_type =
562  type_try_dynamic_cast<java_class_typet>(followed_subtype))
563  {
564  if(class_type->get_base("java::java.lang.Enum"))
565  {
566  const irep_idt &class_name = class_type->get_name();
567  const irep_idt class_clinit = clinit_wrapper_name(class_name);
568  if(const auto clinit_func = symbol_table.lookup(class_clinit))
569  assignments.add(code_function_callt{clinit_func->symbol_expr()});
570  }
571  }
572 
573  code_blockt new_object_assignments;
574  code_blockt update_in_place_assignments;
575 
576  // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
577  // emit to `update_in_place_assignments` code for in-place initialization of
578  // the object pointed by `expr`, assuming that such object is of type
579  // `subtype`
580  if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
581  {
583  update_in_place_assignments,
584  expr,
585  subtype,
586  lifetime,
587  depth,
589  location);
590  }
591 
592  // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
593  // above to `assignments` and return
594  if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
595  {
596  assignments.append(update_in_place_assignments);
597  return;
598  }
599 
600  // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
601  // vector of assignments that create a new object (recursively initializes it)
602  // and asign to `expr` the address of such object
603  code_blockt non_null_inst;
604 
606  non_null_inst,
607  expr,
608  subtype,
609  lifetime,
610  depth,
612  location);
613 
614  const code_assignt set_null_inst{
615  expr, null_pointer_exprt{pointer_type}, location};
616 
617  const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
618 
619  if(!allow_null)
620  {
621  // Add the following code to assignments:
622  // <expr> = <aoe>;
623  new_object_assignments.append(non_null_inst);
624  }
625  else
626  {
627  // if(NONDET(_Bool)
628  // {
629  // <expr> = <null pointer>
630  // }
631  // else
632  // {
633  // <code from recursive call to gen_nondet_init() with
634  // tmp$<temporary_counter>>
635  // }
636  code_ifthenelset null_check(
638  std::move(set_null_inst),
639  std::move(non_null_inst));
640 
641  new_object_assignments.add(std::move(null_check));
642  }
643 
644  // Similarly to above, maybe use a conditional if both the
645  // allocate-fresh and update-in-place cases are allowed:
646  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
647  {
648  assignments.append(new_object_assignments);
649  }
650  else
651  {
653  "No-update and must-update should have already been resolved");
654 
655  code_ifthenelset update_check(
657  std::move(update_in_place_assignments),
658  std::move(new_object_assignments));
659 
660  assignments.add(std::move(update_check));
661  }
662 }
663 
688  code_blockt &assignments,
689  lifetimet lifetime,
690  const pointer_typet &replacement_pointer,
691  size_t depth,
692  const source_locationt &location)
693 {
694  const symbol_exprt new_symbol_expr =
696  replacement_pointer, "tmp_object_factory");
697 
698  // Generate a new object into this new symbol
700  assignments,
701  new_symbol_expr,
702  false, // is_sub
703  false, // skip_classid
704  lifetime,
705  {}, // no override_type
706  depth,
708  location);
709 
710  return new_symbol_expr;
711 }
712 
724  const exprt &expr,
725  const std::list<std::string> &string_input_values,
726  symbol_table_baset &symbol_table)
727 {
728  alternate_casest cases;
729  for(const auto &val : string_input_values)
730  {
731  const symbol_exprt s =
732  get_or_create_string_literal_symbol(val, symbol_table, true);
733  cases.push_back(code_assignt(expr, s));
734  }
735  return cases;
736 }
737 
760  code_blockt &assignments,
761  const exprt &expr,
762  bool is_sub,
763  bool skip_classid,
764  lifetimet lifetime,
765  const struct_typet &struct_type,
766  size_t depth,
767  const update_in_placet &update_in_place,
768  const source_locationt &location)
769 {
770  const namespacet ns(symbol_table);
771  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
772 
773  typedef struct_typet::componentst componentst;
774  const irep_idt &struct_tag=struct_type.get_tag();
775 
776  const componentst &components=struct_type.components();
777 
778  // Should we write the whole object?
779  // * Not if this is a sub-structure (a superclass object), as our caller will
780  // have done this already
781  // * Not if the object has already been initialised by our caller, in which
782  // case they will set `skip_classid`
783  // * Not if we're re-initializing an existing object (i.e. update_in_place)
784  // * Always if it has a string type. Strings should not be partially updated,
785  // and the `length` and `data` components of string types need to be
786  // generated differently from object fields in the general case, see
787  // \ref java_object_factoryt::initialize_nondet_string_fields.
788 
789  const bool has_string_input_values =
791 
792  if(
793  is_java_string_type(struct_type) && has_string_input_values &&
794  !skip_classid)
795  { // We're dealing with a string and we should set fixed input values.
796  // We create a switch statement where each case is an assignment
797  // of one of the fixed input strings to the input variable in question
800  assignments.add(generate_nondet_switch(
802  cases,
803  java_int_type(),
804  ID_java,
805  location,
806  symbol_table));
807  }
808  else if(
809  (!is_sub && !skip_classid &&
810  update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) ||
811  is_java_string_type(struct_type))
812  {
813  // Add an initial all-zero write. Most of the fields of this will be
814  // overwritten, but it helps to have a whole-structure write that analysis
815  // passes can easily recognise leaves no uninitialised state behind.
816 
817  // This code mirrors the `remove_java_new` pass:
818  auto initial_object = zero_initializer(expr.type(), source_locationt(), ns);
819  CHECK_RETURN(initial_object.has_value());
821  to_struct_expr(*initial_object),
822  ns,
823  struct_tag_typet("java::" + id2string(struct_tag)));
824 
825  // If the initialised type is a special-cased String type (one with length
826  // and data fields introduced by string-library preprocessing), initialise
827  // those fields with nondet values
828  if(is_java_string_type(struct_type))
829  { // We're dealing with a string
831  to_struct_expr(*initial_object),
832  assignments,
835  location,
837  symbol_table,
840  }
841 
842  assignments.add(code_assignt(expr, *initial_object));
843  }
844 
845  for(const auto &component : components)
846  {
847  const typet &component_type=component.type();
848  irep_idt name=component.get_name();
849 
850  member_exprt me(expr, name, component_type);
851 
853  {
854  continue;
855  }
856  else if(name == "cproverMonitorCount")
857  {
858  // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
859  // nondet. This field is only present when the java core models are
860  // included in the class-path. It is used to implement a critical section,
861  // which is necessary to support concurrency.
862  if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
863  continue;
864  code_assignt code(me, from_integer(0, me.type()));
865  code.add_source_location() = location;
866  assignments.add(code);
867  }
868  else if(
869  is_java_string_type(struct_type) && (name == "length" || name == "data"))
870  {
871  // In this case these were set up above.
872  continue;
873  }
874  else
875  {
876  INVARIANT(!name.empty(), "Each component of a struct must have a name");
877 
878  bool _is_sub=name[0]=='@';
879 
880  // MUST_UPDATE_IN_PLACE only applies to this object.
881  // If this is a pointer to another object, offer the chance
882  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
883  update_in_placet substruct_in_place=
884  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE && !_is_sub ?
886  update_in_place;
888  assignments,
889  me,
890  _is_sub,
891  false, // skip_classid
892  lifetime,
893  {}, // no override_type
894  depth,
895  substruct_in_place,
896  location);
897  }
898  }
899 
900  // If cproverNondetInitialize() can be found in the symbol table as a method
901  // on this class or any parent, we add a call:
902  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
903  // expr.cproverNondetInitialize();
904  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 
906  resolve_inherited_componentt resolve_inherited_component{symbol_table};
908  cprover_nondet_initialize = resolve_inherited_component(
909  "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true);
910 
911  if(cprover_nondet_initialize)
912  {
913  const symbolt &cprover_nondet_initialize_symbol =
914  ns.lookup(cprover_nondet_initialize->get_full_component_identifier());
915  assignments.add(
916  code_function_callt{cprover_nondet_initialize_symbol.symbol_expr(),
917  {address_of_exprt{expr}}});
918  }
919 }
920 
936  const exprt &expr,
937  const typet &type,
938  const source_locationt &location,
939  const allocate_local_symbolt &allocate_local_symbol)
940 {
941  PRECONDITION(type == java_float_type() || type == java_double_type());
942 
943  code_blockt assignments;
944 
945  const auto &aux_int =
946  allocate_local_symbol(java_int_type(), "assume_integral_tmp");
947  assignments.add(code_declt(aux_int), location);
948  exprt nondet_rhs = side_effect_expr_nondett(java_int_type(), location);
949  code_assignt aux_assign(aux_int, nondet_rhs);
950  aux_assign.add_source_location() = location;
951  assignments.add(aux_assign);
952  assignments.add(
953  code_assumet(equal_exprt(typecast_exprt(aux_int, type), expr)));
954 
955  return assignments;
956 }
957 
994  code_blockt &assignments,
995  const exprt &expr,
996  bool is_sub,
997  bool skip_classid,
998  lifetimet lifetime,
999  const optionalt<typet> &override_type,
1000  size_t depth,
1001  update_in_placet update_in_place,
1002  const source_locationt &location)
1003 {
1004  const typet &type = override_type.has_value() ? *override_type : expr.type();
1005  const namespacet ns(symbol_table);
1006  const typet &followed_type = ns.follow(type);
1007 
1008  if(type.id()==ID_pointer)
1009  {
1010  // dereferenced type
1012 
1013  // If we are about to initialize a generic pointer type, add its concrete
1014  // types to the map and delete them on leaving this function scope.
1016  generic_parameter_specialization_map_keys(
1018  generic_parameter_specialization_map_keys.insert(
1020 
1022  assignments,
1023  expr,
1024  lifetime,
1025  pointer_type,
1026  depth,
1027  update_in_place,
1028  location);
1029  }
1030  else if(followed_type.id() == ID_struct)
1031  {
1032  const struct_typet struct_type = to_struct_type(followed_type);
1033 
1034  // If we are about to initialize a generic class (as a superclass object
1035  // for a different object), add its concrete types to the map and delete
1036  // them on leaving this function scope.
1038  generic_parameter_specialization_map_keys(
1040  if(is_sub)
1041  {
1042  const typet &symbol =
1043  override_type.has_value() ? *override_type : expr.type();
1044  PRECONDITION(symbol.id() == ID_struct_tag);
1045  generic_parameter_specialization_map_keys.insert(
1046  to_struct_tag_type(symbol), struct_type);
1047  }
1048 
1050  assignments,
1051  expr,
1052  is_sub,
1053  skip_classid,
1054  lifetime,
1055  struct_type,
1056  depth,
1057  update_in_place,
1058  location);
1059  }
1060  else
1061  {
1062  // types different from pointer or structure:
1063  // bool, int, float, byte, char, ...
1064  exprt rhs = type.id() == ID_c_bool
1065  ? get_nondet_bool(type, location)
1066  : side_effect_expr_nondett(type, location);
1067  code_assignt assign(expr, rhs);
1068  assign.add_source_location() = location;
1069 
1070  assignments.add(assign);
1072  {
1073  assignments.add(
1075  }
1076  // add assumes to obey numerical restrictions
1077  if(type != java_boolean_type() && type != java_char_type())
1078  {
1079  const auto &interval = object_factory_parameters.assume_inputs_interval;
1080  if(auto singleton = interval.as_singleton())
1081  {
1082  assignments.add(
1083  code_assignt{expr, from_integer(*singleton, expr.type())});
1084  }
1085  else
1086  {
1087  exprt within_bounds = interval.make_contains_expr(expr);
1088  if(!within_bounds.is_true())
1089  assignments.add(code_assumet(std::move(within_bounds)));
1090  }
1091 
1092  if(
1094  (type == java_float_type() || type == java_double_type()))
1095  {
1096  assignments.add(assume_expr_integral(
1097  expr,
1098  type,
1099  location,
1100  [this](
1101  const typet &type, std::string basename_prefix) -> symbol_exprt {
1103  type, basename_prefix);
1104  }));
1105  }
1106  }
1107  }
1108 }
1109 
1111 {
1113 }
1114 
1116 {
1118 }
1119 
1138  code_blockt &assignments,
1139  const exprt &lhs,
1140  const exprt &max_length_expr,
1141  const typet &element_type,
1142  const allocate_local_symbolt &allocate_local_symbol,
1143  const source_locationt &location)
1144 {
1145  const auto &length_sym_expr = generate_nondet_int(
1147  max_length_expr,
1148  "nondet_array_length",
1149  location,
1150  allocate_local_symbol,
1151  assignments);
1152 
1153  side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), location);
1154  java_new_array.copy_to_operands(length_sym_expr);
1155  java_new_array.set(ID_length_upper_bound, max_length_expr);
1156  java_new_array.type().subtype().set(ID_element_type, element_type);
1157  code_assignt assign(lhs, java_new_array);
1158  assign.add_source_location() = location;
1159  assignments.add(assign);
1160 }
1161 
1180  code_blockt &assignments,
1181  const exprt &init_array_expr,
1182  const typet &element_type,
1183  const exprt &max_length_expr,
1184  const source_locationt &location,
1185  const allocate_local_symbolt &allocate_local_symbol)
1186 {
1187  const array_typet array_type(element_type, max_length_expr);
1188 
1189  // TYPE (*array_data_init)[max_length_expr];
1190  const symbol_exprt &tmp_finite_array_pointer =
1191  allocate_local_symbol(pointer_type(array_type), "array_data_init");
1192 
1193  // array_data_init = ALLOCATE(TYPE [max_length_expr], max_length_expr, false);
1194  assignments.add(
1196  tmp_finite_array_pointer,
1197  max_length_expr));
1198  assignments.statements().back().add_source_location() = location;
1199 
1200  // *array_data_init = NONDET(TYPE [max_length_expr]);
1201  side_effect_expr_nondett nondet_data(array_type, location);
1202  const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};
1203  assignments.add(code_assignt(data_pointer_deref, std::move(nondet_data)));
1204  assignments.statements().back().add_source_location() = location;
1205 
1206  // init_array_expr = *array_data_init;
1207  address_of_exprt tmp_nondet_pointer(
1208  index_exprt(data_pointer_deref, from_integer(0, java_int_type())));
1209  assignments.add(code_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
1210  assignments.statements().back().add_source_location() = location;
1211 }
1212 
1223  const exprt &element,
1224  const update_in_placet update_in_place,
1225  const typet &element_type,
1226  const size_t depth,
1227  const source_locationt &location)
1228 {
1229  code_blockt assignments;
1230  bool new_item_is_primitive = element.type().id() != ID_pointer;
1231 
1232  // Use a temporary to initialise a new, or update an existing, non-primitive.
1233  // This makes it clearer that in a sequence like
1234  // `new_array_item->x = y; new_array_item->z = w;` that all the
1235  // `new_array_item` references must alias, cf. the harder-to-analyse
1236  // `some_expr[idx]->x = y; some_expr[idx]->z = w;`
1237  exprt init_expr;
1238  if(new_item_is_primitive)
1239  {
1240  init_expr = element;
1241  }
1242  else
1243  {
1245  element.type(), "new_array_item");
1246 
1247  // If we're updating an existing array item, read the existing object that
1248  // we (may) alter:
1249  if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
1250  assignments.add(code_assignt(init_expr, element));
1251  }
1252 
1253  // MUST_UPDATE_IN_PLACE only applies to this object.
1254  // If this is a pointer to another object, offer the chance
1255  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1256  update_in_placet child_update_in_place =
1257  update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE
1259  : update_in_place;
1261  assignments,
1262  init_expr,
1263  false, // is_sub
1264  false, // skip_classid
1265  // These are variable in number, so use dynamic allocator:
1267  element_type, // override
1268  depth,
1269  child_update_in_place,
1270  location);
1271 
1272  if(!new_item_is_primitive)
1273  {
1274  // We used a temporary variable to update or initialise an array item;
1275  // now write it into the array:
1276  assignments.add(code_assignt(element, init_expr));
1277  }
1278  return assignments;
1279 }
1280 
1322  code_blockt &assignments,
1323  const exprt &init_array_expr,
1324  const exprt &length_expr,
1325  const typet &element_type,
1326  const exprt &max_length_expr,
1327  update_in_placet update_in_place,
1328  const source_locationt &location,
1329  const array_element_generatort &element_generator,
1330  const allocate_local_symbolt &allocate_local_symbol,
1331  const symbol_tablet &symbol_table)
1332 {
1333  const symbol_exprt &array_init_symexpr =
1334  allocate_local_symbol(init_array_expr.type(), "array_data_init");
1335 
1336  code_assignt data_assign(array_init_symexpr, init_array_expr);
1337  data_assign.add_source_location() = location;
1338  assignments.add(data_assign);
1339 
1340  const symbol_exprt &counter_expr =
1341  allocate_local_symbol(length_expr.type(), "array_init_iter");
1342 
1343  code_blockt loop_body;
1344  if(update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
1345  {
1346  // Add a redundant if(counter == max_length) break
1347  // that is easier for the unwinder to understand.
1348  code_ifthenelset max_test(
1349  equal_exprt(counter_expr, max_length_expr), code_breakt{});
1350 
1351  loop_body.add(std::move(max_test));
1352  }
1353 
1354  const dereference_exprt element_at_counter =
1355  array_element_from_pointer(array_init_symexpr, counter_expr);
1356 
1357  loop_body.append(element_generator(element_at_counter, element_type));
1358 
1359  assignments.add(code_fort::from_index_bounds(
1361  length_expr,
1362  counter_expr,
1363  std::move(loop_body),
1364  location));
1365 }
1366 
1368  const exprt &expr,
1369  update_in_placet update_in_place,
1370  const source_locationt &location,
1371  const array_element_generatort &element_generator,
1372  const allocate_local_symbolt &allocate_local_symbol,
1373  const symbol_tablet &symbol_table,
1374  const size_t max_nondet_array_length)
1375 {
1376  PRECONDITION(expr.type().id() == ID_pointer);
1377  PRECONDITION(expr.type().subtype().id() == ID_struct_tag);
1379 
1380  code_blockt statements;
1381 
1382  const namespacet ns(symbol_table);
1383  const typet &type = ns.follow(expr.type().subtype());
1384  const struct_typet &struct_type = to_struct_type(type);
1385  const typet &element_type =
1386  static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
1387 
1388  auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
1389 
1390  // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1391  // initialize its elements
1392  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
1393  {
1395  statements,
1396  expr,
1397  max_length_expr,
1398  element_type,
1399  allocate_local_symbol,
1400  location);
1401  }
1402 
1403  // Otherwise we're updating the array in place, and use the
1404  // existing array allocation and length.
1405 
1406  INVARIANT(
1407  is_valid_java_array(struct_type),
1408  "Java struct array does not conform to expectations");
1409 
1410  dereference_exprt deref_expr(expr);
1411  const auto &comps = struct_type.components();
1412  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1413  exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());
1414 
1415  if(init_array_expr.type() != pointer_type(element_type))
1416  init_array_expr =
1417  typecast_exprt(init_array_expr, pointer_type(element_type));
1418 
1419  if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
1420  {
1421  // For arrays of non-primitive type, nondeterministically initialize each
1422  // element of the array
1424  statements,
1425  init_array_expr,
1426  length_expr,
1427  element_type,
1428  max_length_expr,
1429  update_in_place,
1430  location,
1431  element_generator,
1432  allocate_local_symbol,
1433  symbol_table);
1434  }
1435  else
1436  {
1437  // Arrays of primitive type can be initialized with a single instruction.
1438  // We don't do this for arrays of primitive booleans, because booleans are
1439  // represented as unsigned bytes, so each cell must be initialized as
1440  // 0 or 1 (see gen_nondet_init).
1442  statements,
1443  init_array_expr,
1444  element_type,
1445  max_length_expr,
1446  location,
1447  allocate_local_symbol);
1448  }
1449  return statements;
1450 }
1451 
1466  code_blockt &assignments,
1467  const exprt &expr,
1468  const java_class_typet &java_class_type,
1469  const source_locationt &location)
1470 {
1471  const irep_idt &class_name = java_class_type.get_name();
1472  const irep_idt values_name = id2string(class_name) + ".$VALUES";
1473  if(!symbol_table.has_symbol(values_name))
1474  {
1475  log.warning() << values_name
1476  << " is missing, so the corresponding Enum "
1477  "type will nondet initialised"
1478  << messaget::eom;
1479  return false;
1480  }
1481 
1482  const namespacet ns(symbol_table);
1483  const symbolt &values = ns.lookup(values_name);
1484 
1485  // Access members (length and data) of $VALUES array
1486  dereference_exprt deref_expr(values.symbol_expr());
1487  const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type()));
1488  PRECONDITION(is_valid_java_array(deref_struct_type));
1489  const auto &comps = deref_struct_type.components();
1490  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1491  const member_exprt enum_array_expr =
1492  member_exprt(deref_expr, "data", comps[2].type());
1493 
1494  const symbol_exprt &index_expr = generate_nondet_int(
1496  minus_exprt(length_expr, from_integer(1, java_int_type())),
1497  "enum_index_init",
1498  location,
1500  assignments);
1501 
1502  const dereference_exprt element_at_index =
1503  array_element_from_pointer(enum_array_expr, index_expr);
1504  code_assignt enum_assign(expr, typecast_exprt(element_at_index, expr.type()));
1505  assignments.add(enum_assign);
1506 
1507  return true;
1508 }
1509 
1510 static void assert_type_consistency(const code_blockt &assignments)
1511 {
1512  // In future we'll be able to use codet::validate for this;
1513  // at present that only verifies `lhs.type base_type_eq right.type`,
1514  // whereas we want to check exact equality.
1515  for(const auto &code : assignments.statements())
1516  {
1517  if(code.get_statement() != ID_assign)
1518  continue;
1519  const auto &assignment = to_code_assign(code);
1520  INVARIANT(
1521  assignment.lhs().type() == assignment.rhs().type(),
1522  "object factory should produce type-consistent assignments");
1523  }
1524 }
1525 
1538  const typet &type,
1539  const irep_idt base_name,
1540  code_blockt &init_code,
1541  symbol_table_baset &symbol_table,
1543  lifetimet lifetime,
1544  const source_locationt &loc,
1545  const select_pointer_typet &pointer_type_selector,
1546  message_handlert &log)
1547 {
1549  "::"+id2string(base_name);
1550 
1551  auxiliary_symbolt main_symbol;
1552  main_symbol.mode=ID_java;
1553  main_symbol.is_static_lifetime=false;
1554  main_symbol.name=identifier;
1555  main_symbol.base_name=base_name;
1556  main_symbol.type=type;
1557  main_symbol.location=loc;
1559 
1560  exprt object=main_symbol.symbol_expr();
1561 
1562  symbolt *main_symbol_ptr;
1563  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
1564  CHECK_RETURN(!moving_symbol_failed);
1565 
1566  java_object_factoryt state(
1567  loc, parameters, symbol_table, pointer_type_selector, log);
1568  code_blockt assignments;
1569  state.gen_nondet_init(
1570  assignments,
1571  object,
1572  false, // is_sub
1573  false, // skip_classid
1574  lifetime,
1575  {}, // no override_type
1576  1, // initial depth
1578  loc);
1579 
1580  state.add_created_symbol(main_symbol_ptr);
1581  state.declare_created_symbols(init_code);
1582 
1583  assert_type_consistency(assignments);
1584  init_code.append(assignments);
1585  return object;
1586 }
1587 
1625  const exprt &expr,
1626  code_blockt &init_code,
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,
1633  update_in_placet update_in_place,
1634  message_handlert &log)
1635 {
1636  java_object_factoryt state(
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
1643  skip_classid,
1644  lifetime,
1645  {}, // no override_type
1646  1, // initial depth
1647  update_in_place,
1648  loc);
1649 
1650  state.declare_created_symbols(init_code);
1651 
1652  assert_type_consistency(assignments);
1653  init_code.append(assignments);
1654 }
1655 
1658  const typet &type,
1659  const irep_idt base_name,
1660  code_blockt &init_code,
1661  symbol_tablet &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,
1683  code_blockt &init_code,
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,
1689  update_in_placet update_in_place,
1690  message_handlert &log)
1691 {
1692  select_pointer_typet pointer_type_selector;
1694  expr,
1695  init_code,
1696  symbol_table,
1697  loc,
1698  skip_classid,
1699  lifetime,
1700  object_factory_parameters,
1701  pointer_type_selector,
1702  update_in_place,
1703  log);
1704 }
java_object_factoryt::object_factory_parameters
const java_object_factory_parameterst object_factory_parameters
Definition: java_object_factory.cpp:29
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
recursion_set_entryt::operator=
recursion_set_entryt & operator=(const recursion_set_entryt &)=delete
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
add_pointer_to_array_association
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...
Definition: java_string_library_preprocess.cpp:644
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
recursion_set_entryt::insert_entry
bool insert_entry(const irep_idt &entry)
Try to add an entry to the controlled set.
Definition: java_object_factory.cpp:293
generate_nondet_switch
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:93
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_root_class.h
java_object_factoryt::symbol_table
symbol_table_baset & symbol_table
The symbol table.
Definition: java_object_factory.cpp:48
array_primitive_init_code
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.
Definition: java_object_factory.cpp:1179
allocate_nondet_length_array
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.
Definition: java_object_factory.cpp:1137
generic_parameter_specialization_map_keyst::insert
void insert(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Author: Diffblue Ltd.
Definition: generic_parameter_specialization_map_keys.cpp:13
JAVA_CLASS_IDENTIFIER_FIELD_NAME
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Definition: class_identifier.h:20
recursion_set_entryt::recursion_set_entryt
recursion_set_entryt(std::unordered_set< irep_idt > &_recursion_set)
Initialize a recursion-set entry owner operating on a given set.
Definition: java_object_factory.cpp:275
add_array_to_length_association
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...
Definition: java_string_library_preprocess.cpp:675
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
generate_nondet_int
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:17
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
update_in_placet::MAY_UPDATE_IN_PLACE
@ MAY_UPDATE_IN_PLACE
java_object_factoryt::gen_nondet_pointer_init
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.
Definition: java_object_factory.cpp:469
java_string_literals.h
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:82
gen_nondet_array_init
code_blockt gen_nondet_array_init(const exprt &expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table, const size_t max_nondet_array_length)
Synthesize GOTO for generating a array of nondet length to be stored in the expr.
Definition: java_object_factory.cpp:1367
allocate_objectst::add_created_symbol
void add_created_symbol(const symbolt *symbol_ptr)
Add a pointer to a symbol to the list of pointers to symbols created so far.
Definition: allocate_objects.cpp:218
generic_parameter_specialization_map_keys.h
Author: Diffblue Ltd.
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
recursion_set_entryt
Recursion-set entry owner class.
Definition: java_object_factory.cpp:265
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
object_factory_parameterst::string_input_values
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
Definition: object_factory_parameters.h:79
is_valid_java_array
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:834
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
get_string_input_values_code
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_...
Definition: java_object_factory.cpp:723
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
bool_typet
The Boolean type.
Definition: std_types.h:37
java_object_factoryt::pointer_type_selector
const select_pointer_typet & pointer_type_selector
Resolves pointer types potentially using some heuristics, for example to replace pointers to interfac...
Definition: java_object_factory.cpp:53
messaget::eom
static eomt eom
Definition: message.h:297
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
generic_parameter_specialization_mapt
Author: Diffblue Ltd.
Definition: generic_parameter_specialization_map.h:24
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
make_nondet_infinite_char_array
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.
Definition: java_string_library_preprocess.cpp:612
printable_char_range
const integer_intervalt printable_char_range(' ', '~')
Interval that represents the printable character range range U+0020-U+007E, i.e.
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
get_or_create_string_literal_symbol
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.
Definition: java_string_literals.cpp:38
struct_union_typet::component_number
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:36
equal_exprt
Equality.
Definition: std_expr.h:1190
update_in_placet
update_in_placet
Definition: java_object_factory.h:105
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
assert_type_consistency
static void assert_type_consistency(const code_blockt &assignments)
Definition: java_object_factory.cpp:1510
java_class_typet
Definition: java_types.h:199
update_in_placet::MUST_UPDATE_IN_PLACE
@ MUST_UPDATE_IN_PLACE
interval_templatet
Definition: interval_template.h:20
object_factory_parameterst::max_nondet_tree_depth
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
Definition: object_factory_parameters.h:61
generic_parameter_specialization_map_keyst
Definition: generic_parameter_specialization_map_keys.h:16
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
select_pointer_typet::convert_pointer_type
virtual pointer_typet convert_pointer_type(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
Select what type should be used for a given pointer type.
Definition: select_pointer_type.cpp:17
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
recursion_set_entryt::recursion_set_entryt
recursion_set_entryt(const recursion_set_entryt &)=delete
object_factory_parameterst::string_printable
bool string_printable
Force string content to be ASCII printable characters when set to true.
Definition: object_factory_parameters.h:76
java_object_factoryt::java_object_factoryt
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)
Definition: java_object_factory.cpp:69
java_object_factory_parameterst::assume_inputs_interval
interval_uniont assume_inputs_interval
Force numerical primitive inputs to fall within the interval.
Definition: java_object_factory_parameters.h:27
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:163
interval_templatet::upper
T upper
Definition: interval_template.h:44
set_class_identifier
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.
Definition: class_identifier.cpp:82
equal_java_types
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:891
expr_initializer.h
Expression Initialization.
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_object_factory.h
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
alternate_casest
std::vector< codet > alternate_casest
Definition: nondet.h:74
is_java_string_type
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:33
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1598
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
java_object_factoryt::gen_nondet_struct_init
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...
Definition: java_object_factory.cpp:759
java_object_factoryt::gen_nondet_subtype_pointer_init
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.
Definition: java_object_factory.cpp:687
interval_constraint.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
recursion_set_entryt::recursion_set
std::unordered_set< irep_idt > & recursion_set
Recursion set to modify.
Definition: java_object_factory.cpp:267
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
java_object_factoryt
Definition: java_object_factory.cpp:28
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
recursion_set_entryt::~recursion_set_entryt
~recursion_set_entryt()
Removes erase_entry (if set) from the controlled set.
Definition: java_object_factory.cpp:280
object_factory
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...
Definition: java_object_factory.cpp:1537
allocate_objectst::allocate_object
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,...
Definition: allocate_objects.cpp:32
select_pointer_typet
Definition: select_pointer_type.h:26
array_element_from_pointer
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...
Definition: array_element_from_pointer.cpp:12
java_object_factoryt::allocate_objects
allocate_objectst allocate_objects
Definition: java_object_factory.cpp:55
java_object_factory_parameterst::assume_inputs_integral
bool assume_inputs_integral
Force double and float inputs to be integral.
Definition: java_object_factory_parameters.h:30
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_integer_bitvector_type
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
Definition: std_types.h:1199
gen_nondet_init
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...
Definition: java_object_factory.cpp:1624
java_object_factoryt::log
messaget log
Log for reporting warnings and errors in object creation.
Definition: java_object_factory.cpp:58
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
initialize_nondet_string_fields
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.
Definition: java_object_factory.cpp:360
array_element_from_pointer.h
java_object_factoryt::gen_pointer_target_init
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,...
Definition: java_object_factory.cpp:185
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
recursion_set_entryt::erase_entry
irep_idt erase_entry
Entry to erase on destruction, if non-empty.
Definition: java_object_factory.cpp:269
integer_interval_to_string
static irep_idt integer_interval_to_string(const integer_intervalt &interval)
Converts and integer_intervalt to a a string of the for [lower]-[upper].
Definition: java_object_factory.cpp:312
minus_exprt
Binary minus.
Definition: std_expr.h:940
object_factory_parameterst::max_nondet_array_length
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
Definition: object_factory_parameters.h:37
allocate_objectst::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Definition: allocate_objects.cpp:226
lifetimet
lifetimet
Selects the kind of objects allocated.
Definition: allocate_objects.h:21
object_factory_parameterst::min_null_tree_depth
size_t min_null_tree_depth
To force a certain depth of non-null objects.
Definition: object_factory_parameters.h:73
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
java_class_typet::get_name
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:559
allocate_local_symbolt
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:19
java_object_factoryt::add_created_symbol
void add_created_symbol(const symbolt *symbol)
Definition: java_object_factory.cpp:1110
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
java_object_factoryt::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Definition: java_object_factory.cpp:1115
object_factory_parameterst::max_nondet_string_length
size_t max_nondet_string_length
Maximum value for the non-deterministically-chosen length of a string.
Definition: object_factory_parameters.h:44
assume_expr_integral
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.
Definition: java_object_factory.cpp:935
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
array_typet
Arrays with given size.
Definition: std_types.h:965
interval_constraint
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 ...
Definition: interval_constraint.cpp:12
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:74
object_factory_parameterst::min_nondet_string_length
size_t min_nondet_string_length
Minimum value for the non-deterministically-chosen length of a string.
Definition: object_factory_parameters.h:47
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
nondet.h
java_object_factoryt::gen_nondet_init
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...
Definition: java_object_factory.cpp:993
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:87
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
update_in_placet::NO_UPDATE_IN_PLACE
@ NO_UPDATE_IN_PLACE
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_functions.h
Goto Programs with Functions.
make_allocate_code
code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
Definition: allocate_objects.cpp:255
clinit_wrapper_name
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...
Definition: java_static_initializers.cpp:65
class_identifier.h
Extract class identifier.
code_fort::from_index_bounds
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:212
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: std_types.cpp:171
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
lifetimet::DYNAMIC
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
allocate_objectst
Definition: allocate_objects.h:31
get_nondet_bool
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:22
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
array_loop_init_code
static void array_loop_init_code(code_blockt &assignments, const exprt &init_array_expr, const exprt &length_expr, const typet &element_type, const exprt &max_length_expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table)
Create code to nondeterministically initialize each element of an array in a loop.
Definition: java_object_factory.cpp:1321
java_object_factoryt::generic_parameter_specialization_map
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)...
Definition: java_object_factory.cpp:45
exprt::operands
operandst & operands()
Definition: expr.h:95
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
symbol_table_baset::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
allocate_objectst::allocate_automatic_local_object
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.
Definition: allocate_objects.cpp:70
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
java_utils.h
array_element_generatort
std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)> array_element_generatort
Definition: java_object_factory.h:135
messaget::warning
mstreamt & warning() const
Definition: message.h:404
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
java_object_factoryt::gen_nondet_enum_init
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...
Definition: java_object_factory.cpp:1465
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
add_character_set_constraint
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...
Definition: java_string_library_preprocess.cpp:707
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:68
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656
validation_modet::INVARIANT
@ INVARIANT
java_object_factoryt::assign_element
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.
Definition: java_object_factory.cpp:1222
nondet_bool.h
Nondeterministic boolean helper.
resolve_inherited_componentt
Definition: resolve_inherited_component.h:22
interval_templatet::lower
T lower
Definition: interval_template.h:44
java_object_factoryt::recursion_set
std::unordered_set< irep_idt > recursion_set
This is employed in conjunction with the depth above.
Definition: java_object_factory.cpp:35