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 
11 #include <util/arith_tools.h>
13 #include <util/expr_initializer.h>
14 #include <util/message.h>
15 #include <util/nondet.h>
16 #include <util/nondet_bool.h>
17 #include <util/prefix.h>
18 
22 
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,
70  update_in_placet update_in_place,
71  const source_locationt &location);
72 public:
74  const source_locationt &loc,
75  const java_object_factory_parameterst _object_factory_parameters,
76  symbol_table_baset &_symbol_table,
79  : object_factory_parameters(_object_factory_parameters),
80  symbol_table(_symbol_table),
83  ID_java,
84  loc,
85  object_factory_parameters.function_id,
86  symbol_table),
87  log(log)
88  {}
89 
91  code_blockt &assignments,
92  const exprt &expr,
93  const java_class_typet &java_class_type,
94  const source_locationt &location);
95 
96  void gen_nondet_init(
97  code_blockt &assignments,
98  const exprt &expr,
99  bool is_sub,
100  bool skip_classid,
101  lifetimet lifetime,
102  const optionalt<typet> &override_type,
103  size_t depth,
105  const source_locationt &location);
106 
107  void add_created_symbol(const symbolt *symbol);
108 
109  void declare_created_symbols(code_blockt &init_code);
110 
111 private:
113  code_blockt &assignments,
114  const exprt &expr,
115  lifetimet lifetime,
117  size_t depth,
118  const update_in_placet &update_in_place,
119  const source_locationt &location);
120 
122  code_blockt &assignments,
123  const exprt &expr,
124  bool is_sub,
125  bool skip_classid,
126  lifetimet lifetime,
127  const struct_typet &struct_type,
128  size_t depth,
129  const update_in_placet &update_in_place,
130  const source_locationt &location);
131 
133  code_blockt &assignments,
134  lifetimet lifetime,
135  const pointer_typet &substitute_pointer_type,
136  size_t depth,
137  const source_locationt &location);
138 
140  const exprt &element,
141  update_in_placet update_in_place,
142  const typet &element_type,
143  size_t depth,
144  const source_locationt &location);
145 };
146 
190  code_blockt &assignments,
191  const exprt &expr,
192  const typet &target_type,
193  lifetimet lifetime,
194  size_t depth,
195  update_in_placet update_in_place,
196  const source_locationt &location)
197 {
198  PRECONDITION(expr.type().id() == ID_pointer);
199  PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
200 
201  const namespacet ns(symbol_table);
202  const typet &followed_target_type = ns.follow(target_type);
203  PRECONDITION(followed_target_type.id() == ID_struct);
204 
205  const auto &target_class_type = to_java_class_type(followed_target_type);
206  if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
207  {
208  assignments.append(gen_nondet_array_init(
209  expr,
210  update_in_place,
211  location,
212  [this, update_in_place, depth, location](
213  const exprt &element, const typet &element_type) -> code_blockt {
214  return assign_element(
215  element, update_in_place, element_type, depth + 1, location);
216  },
217  [this](const typet &type, std::string basename_prefix) -> symbol_exprt {
219  type, basename_prefix);
220  },
221  symbol_table,
223  return;
224  }
225  if(target_class_type.get_base("java::java.lang.Enum"))
226  {
227  if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
228  return;
229  }
230 
231  // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
232  // initialize the fields of the object pointed by `expr`; if in
233  // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
234  // (return value of `allocate_object`), emit a statement of the form
235  // `<expr> := address-of(<new-object>)` and recursively initialize such new
236  // object.
237  exprt init_expr;
238  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
239  {
240  init_expr = allocate_objects.allocate_object(
241  assignments, expr, target_type, lifetime, "tmp_object_factory");
242  }
243  else
244  {
245  if(expr.id() == ID_address_of)
246  init_expr = to_address_of_expr(expr).object();
247  else
248  {
249  init_expr = dereference_exprt(expr);
250  }
251  }
252 
254  assignments,
255  init_expr,
256  false, // is_sub
257  false, // skip_classid
258  lifetime,
259  {}, // no override type
260  depth + 1,
261  update_in_place,
262  location);
263 }
264 
269 {
271  std::unordered_set<irep_idt> &recursion_set;
274 
275 public:
279  explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
280  : recursion_set(_recursion_set)
281  { }
282 
285  {
286  if(!erase_entry.empty())
287  recursion_set.erase(erase_entry);
288  }
289 
292 
297  bool insert_entry(const irep_idt &entry)
298  {
299  INVARIANT(erase_entry.empty(), "insert_entry should only be called once");
300  INVARIANT(!entry.empty(), "entry should be a struct tag");
301  bool ret=recursion_set.insert(entry).second;
302  if(ret)
303  {
304  // We added something, so erase it when this is destroyed:
305  erase_entry=entry;
306  }
307  return ret;
308  }
309 };
310 
314 
317 {
318  std::string result;
319  result += numeric_cast_v<char>(interval.lower);
320  result += "-";
321  result += numeric_cast_v<char>(interval.upper);
322  return result;
323 }
324 
365  struct_exprt &struct_expr,
366  code_blockt &code,
367  const std::size_t &min_nondet_string_length,
368  const std::size_t &max_nondet_string_length,
369  const source_locationt &loc,
370  const irep_idt &function_id,
371  symbol_table_baset &symbol_table,
372  bool printable,
373  allocate_objectst &allocate_objects)
374 {
375  namespacet ns(symbol_table);
376  const struct_typet &struct_type =
377  to_struct_type(ns.follow(struct_expr.type()));
378  PRECONDITION(is_java_string_type(struct_type));
379 
380  // We allow type StringBuffer and StringBuilder to be initialized
381  // in the same way has String, because they have the same structure and
382  // are treated in the same way by CBMC.
383 
384  // Note that CharSequence cannot be used as classid because it's abstract,
385  // so it is replaced by String.
386  // \todo allow StringBuffer and StringBuilder as classid for Charsequence
387  if(struct_type.get_tag() == "java.lang.CharSequence")
388  {
390  struct_expr, ns, struct_tag_typet("java::java.lang.String"));
391  }
392 
393  // OK, this is a String type with the expected fields -- add code to `code`
394  // to set up pre-requisite variables and assign them in `struct_expr`.
395 
397  // length_expr = nondet(int);
398  const symbol_exprt length_expr =
399  allocate_objects.allocate_automatic_local_object(
400  java_int_type(), "tmp_object_factory");
401  const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
402  code.add(code_assignt(length_expr, nondet_length));
403 
404  // assume (length_expr >= min_nondet_string_length);
405  const exprt min_length =
406  from_integer(min_nondet_string_length, java_int_type());
407  code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
408 
409  // assume (length_expr <= max_input_length)
410  if(
411  max_nondet_string_length <=
412  to_integer_bitvector_type(length_expr.type()).largest())
413  {
414  exprt max_length =
415  from_integer(max_nondet_string_length, length_expr.type());
416  code.add(
417  code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
418  }
419 
420  const exprt data_expr =
421  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
422  struct_expr.operands()[struct_type.component_number("length")] = length_expr;
423 
424  const address_of_exprt array_pointer(
425  index_exprt(data_expr, from_integer(0, java_int_type())));
426 
428  array_pointer, data_expr, symbol_table, loc, function_id, code);
429 
431  data_expr, length_expr, symbol_table, loc, function_id, code);
432 
433  struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
434 
435  // Printable ASCII characters are between ' ' and '~'.
436  if(printable)
437  {
439  array_pointer,
440  length_expr,
442  symbol_table,
443  loc,
444  function_id,
445  code);
446  }
447 }
448 
474  code_blockt &assignments,
475  const exprt &expr,
476  lifetimet lifetime,
478  size_t depth,
479  const update_in_placet &update_in_place,
480  const source_locationt &location)
481 {
482  PRECONDITION(expr.type().id()==ID_pointer);
483  const namespacet ns(symbol_table);
484  const typet &subtype = pointer_type.subtype();
485  const typet &followed_subtype = ns.follow(subtype);
486  PRECONDITION(followed_subtype.id() == ID_struct);
487  const pointer_typet &replacement_pointer_type =
490 
491  // If we are changing the pointer, we generate code for creating a pointer
492  // to the substituted type instead
493  // TODO if we are comparing array types we need to compare their element
494  // types. this is for now done by implementing equality function especially
495  // for java types, technical debt TG-2707
496  if(!equal_java_types(replacement_pointer_type, pointer_type))
497  {
498  // update generic_parameter_specialization_map for the new pointer
500  generic_parameter_specialization_map_keys(
502  generic_parameter_specialization_map_keys.insert(
503  replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
504 
505  const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
506  assignments, lifetime, replacement_pointer_type, depth, location);
507 
508  // Having created a pointer to object of type replacement_pointer_type
509  // we now assign it back to the original pointer with a cast
510  // from pointer_type to replacement_pointer_type
511  assignments.add(
512  code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
513  return;
514  }
515 
516  // This deletes the recursion set entry on leaving this function scope,
517  // if one is set below.
518  recursion_set_entryt recursion_set_entry(recursion_set);
519 
520  // We need to prevent the possibility of this code to loop infinitely when
521  // initializing a data structure with recursive types or unbounded depth. We
522  // implement two mechanisms here. We keep a set of 'types seen', and
523  // detect when we perform a 2nd visit to the same type. We also detect the
524  // depth in the chain of (recursive) calls to the methods of this class.
525  // The depth counter is incremented only when a pointer is deferenced,
526  // including pointers to arrays.
527  //
528  // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
529  // the pointer to NULL instead of recursively initializing the struct to which
530  // it points.
531  const struct_typet &struct_type = to_struct_type(followed_subtype);
532  const irep_idt &struct_tag = struct_type.get_tag();
533 
534  // If this is a recursive type of some kind AND the depth is exceeded, set
535  // the pointer to null.
536  if(
537  !recursion_set_entry.insert_entry(struct_tag) &&
539  {
540  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
541  {
542  assignments.add(
543  code_assignt{expr, null_pointer_exprt{pointer_type}, location});
544  }
545  // Otherwise leave it as it is.
546  return;
547  }
548 
549  // If we may be about to initialize a non-null enum type, always run the
550  // clinit_wrapper of its class first.
551  // TODO: TG-4689 we may want to do this for all types, not just enums, as
552  // described in the Java language specification:
553  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
554  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
555  // But we would have to put this behavior behind an option as it would have an
556  // impact on running times.
557  // Note that it would be more consistent with the behaviour of the JVM to only
558  // run clinit_wrapper if we are about to initialize an object of which we know
559  // for sure that it is not null on any following branch. However, adding this
560  // case in gen_nondet_struct_init would slow symex down too much, so if we
561  // decide to do this for all types, we should do it here.
562  // Note also that this logic is mirrored in
563  // ci_lazy_methodst::initialize_instantiated_classes.
564  if(
565  const auto class_type =
566  type_try_dynamic_cast<java_class_typet>(followed_subtype))
567  {
568  if(class_type->get_base("java::java.lang.Enum"))
569  {
570  const irep_idt &class_name = class_type->get_name();
571  const irep_idt class_clinit = clinit_wrapper_name(class_name);
572  if(const auto clinit_func = symbol_table.lookup(class_clinit))
573  assignments.add(code_function_callt{clinit_func->symbol_expr()});
574  }
575  }
576 
577  code_blockt new_object_assignments;
578  code_blockt update_in_place_assignments;
579 
580  // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
581  // emit to `update_in_place_assignments` code for in-place initialization of
582  // the object pointed by `expr`, assuming that such object is of type
583  // `subtype`
584  if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
585  {
587  update_in_place_assignments,
588  expr,
589  subtype,
590  lifetime,
591  depth,
593  location);
594  }
595 
596  // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
597  // above to `assignments` and return
598  if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
599  {
600  assignments.append(update_in_place_assignments);
601  return;
602  }
603 
604  // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
605  // vector of assignments that create a new object (recursively initializes it)
606  // and asign to `expr` the address of such object
607  code_blockt non_null_inst;
608 
610  non_null_inst,
611  expr,
612  subtype,
613  lifetime,
614  depth,
615  update_in_placet::NO_UPDATE_IN_PLACE,
616  location);
617 
618  const code_assignt set_null_inst{
619  expr, null_pointer_exprt{pointer_type}, location};
620 
621  const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
622 
623  if(!allow_null)
624  {
625  // Add the following code to assignments:
626  // <expr> = <aoe>;
627  new_object_assignments.append(non_null_inst);
628  }
629  else
630  {
631  // if(NONDET(_Bool)
632  // {
633  // <expr> = <null pointer>
634  // }
635  // else
636  // {
637  // <code from recursive call to gen_nondet_init() with
638  // tmp$<temporary_counter>>
639  // }
640  code_ifthenelset null_check(
642  std::move(set_null_inst),
643  std::move(non_null_inst));
644 
645  new_object_assignments.add(std::move(null_check));
646  }
647 
648  // Similarly to above, maybe use a conditional if both the
649  // allocate-fresh and update-in-place cases are allowed:
650  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
651  {
652  assignments.append(new_object_assignments);
653  }
654  else
655  {
656  INVARIANT(update_in_place==update_in_placet::MAY_UPDATE_IN_PLACE,
657  "No-update and must-update should have already been resolved");
658 
659  code_ifthenelset update_check(
661  std::move(update_in_place_assignments),
662  std::move(new_object_assignments));
663 
664  assignments.add(std::move(update_check));
665  }
666 }
667 
692  code_blockt &assignments,
693  lifetimet lifetime,
694  const pointer_typet &replacement_pointer,
695  size_t depth,
696  const source_locationt &location)
697 {
698  const symbol_exprt new_symbol_expr =
700  replacement_pointer, "tmp_object_factory");
701 
702  // Generate a new object into this new symbol
704  assignments,
705  new_symbol_expr,
706  false, // is_sub
707  false, // skip_classid
708  lifetime,
709  {}, // no override_type
710  depth,
711  update_in_placet::NO_UPDATE_IN_PLACE,
712  location);
713 
714  return new_symbol_expr;
715 }
716 
728  const exprt &expr,
729  const std::list<std::string> &string_input_values,
730  symbol_table_baset &symbol_table)
731 {
732  alternate_casest cases;
733  for(const auto &val : string_input_values)
734  {
735  const symbol_exprt s =
736  get_or_create_string_literal_symbol(val, symbol_table, true);
737  cases.push_back(code_assignt(expr, s));
738  }
739  return cases;
740 }
741 
764  code_blockt &assignments,
765  const exprt &expr,
766  bool is_sub,
767  bool skip_classid,
768  lifetimet lifetime,
769  const struct_typet &struct_type,
770  size_t depth,
771  const update_in_placet &update_in_place,
772  const source_locationt &location)
773 {
774  const namespacet ns(symbol_table);
775  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
776 
777  typedef struct_typet::componentst componentst;
778  const irep_idt &struct_tag=struct_type.get_tag();
779 
780  const componentst &components=struct_type.components();
781 
782  // Should we write the whole object?
783  // * Not if this is a sub-structure (a superclass object), as our caller will
784  // have done this already
785  // * Not if the object has already been initialised by our caller, in which
786  // case they will set `skip_classid`
787  // * Not if we're re-initializing an existing object (i.e. update_in_place)
788  // * Always if it has a string type. Strings should not be partially updated,
789  // and the `length` and `data` components of string types need to be
790  // generated differently from object fields in the general case, see
791  // \ref java_object_factoryt::initialize_nondet_string_fields.
792 
793  const bool has_string_input_values =
795 
796  if(
797  is_java_string_type(struct_type) && has_string_input_values &&
798  !skip_classid)
799  { // We're dealing with a string and we should set fixed input values.
800  // We create a switch statement where each case is an assignment
801  // of one of the fixed input strings to the input variable in question
804  assignments.add(generate_nondet_switch(
806  cases,
807  java_int_type(),
808  ID_java,
809  location,
810  symbol_table));
811  }
812  else if(
813  (!is_sub && !skip_classid &&
814  update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) ||
815  is_java_string_type(struct_type))
816  {
817  // Add an initial all-zero write. Most of the fields of this will be
818  // overwritten, but it helps to have a whole-structure write that analysis
819  // passes can easily recognise leaves no uninitialised state behind.
820 
821  // This code mirrors the `remove_java_new` pass:
822  auto initial_object = zero_initializer(expr.type(), source_locationt(), ns);
823  CHECK_RETURN(initial_object.has_value());
825  to_struct_expr(*initial_object),
826  ns,
827  struct_tag_typet("java::" + id2string(struct_tag)));
828 
829  // If the initialised type is a special-cased String type (one with length
830  // and data fields introduced by string-library preprocessing), initialise
831  // those fields with nondet values
832  if(is_java_string_type(struct_type))
833  { // We're dealing with a string
835  to_struct_expr(*initial_object),
836  assignments,
839  location,
841  symbol_table,
844  }
845 
846  assignments.add(code_assignt(expr, *initial_object));
847  }
848 
849  for(const auto &component : components)
850  {
851  const typet &component_type=component.type();
852  irep_idt name=component.get_name();
853 
854  member_exprt me(expr, name, component_type);
855 
857  {
858  continue;
859  }
860  else if(name == "cproverMonitorCount")
861  {
862  // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
863  // nondet. This field is only present when the java core models are
864  // included in the class-path. It is used to implement a critical section,
865  // which is necessary to support concurrency.
866  if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
867  continue;
868  code_assignt code(me, from_integer(0, me.type()));
869  code.add_source_location() = location;
870  assignments.add(code);
871  }
872  else if(
873  is_java_string_type(struct_type) && (name == "length" || name == "data"))
874  {
875  // In this case these were set up above.
876  continue;
877  }
878  else
879  {
880  INVARIANT(!name.empty(), "Each component of a struct must have a name");
881 
882  bool _is_sub=name[0]=='@';
883 
884  // MUST_UPDATE_IN_PLACE only applies to this object.
885  // If this is a pointer to another object, offer the chance
886  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
887  update_in_placet substruct_in_place=
888  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE && !_is_sub ?
889  update_in_placet::MAY_UPDATE_IN_PLACE :
890  update_in_place;
892  assignments,
893  me,
894  _is_sub,
895  false, // skip_classid
896  lifetime,
897  {}, // no override_type
898  depth,
899  substruct_in_place,
900  location);
901  }
902  }
903 
904  // If cproverNondetInitialize() can be found in the symbol table as a method
905  // on this class or any parent, we add a call:
906  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
907  // expr.cproverNondetInitialize();
908  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
909 
910  resolve_inherited_componentt resolve_inherited_component{symbol_table};
912  cprover_nondet_initialize = resolve_inherited_component(
913  "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true);
914 
915  if(cprover_nondet_initialize)
916  {
917  const symbolt &cprover_nondet_initialize_symbol =
918  ns.lookup(cprover_nondet_initialize->get_full_component_identifier());
919  assignments.add(
920  code_function_callt{cprover_nondet_initialize_symbol.symbol_expr(),
921  {address_of_exprt{expr}}});
922  }
923 }
924 
940  const exprt &expr,
941  const typet &type,
942  const source_locationt &location,
943  const allocate_local_symbolt &allocate_local_symbol)
944 {
945  PRECONDITION(type == java_float_type() || type == java_double_type());
946 
947  code_blockt assignments;
948 
949  const auto &aux_int =
950  allocate_local_symbol(java_int_type(), "assume_integral_tmp");
951  assignments.add(code_declt(aux_int), location);
952  exprt nondet_rhs = side_effect_expr_nondett(java_int_type(), location);
953  code_assignt aux_assign(aux_int, nondet_rhs);
954  aux_assign.add_source_location() = location;
955  assignments.add(aux_assign);
956  assignments.add(
957  code_assumet(equal_exprt(typecast_exprt(aux_int, type), expr)));
958 
959  return assignments;
960 }
961 
998  code_blockt &assignments,
999  const exprt &expr,
1000  bool is_sub,
1001  bool skip_classid,
1002  lifetimet lifetime,
1003  const optionalt<typet> &override_type,
1004  size_t depth,
1005  update_in_placet update_in_place,
1006  const source_locationt &location)
1007 {
1008  const typet &type = override_type.has_value() ? *override_type : expr.type();
1009  const namespacet ns(symbol_table);
1010  const typet &followed_type = ns.follow(type);
1011 
1012  if(type.id()==ID_pointer)
1013  {
1014  // dereferenced type
1016 
1017  // If we are about to initialize a generic pointer type, add its concrete
1018  // types to the map and delete them on leaving this function scope.
1020  generic_parameter_specialization_map_keys(
1022  generic_parameter_specialization_map_keys.insert(
1024 
1026  assignments,
1027  expr,
1028  lifetime,
1029  pointer_type,
1030  depth,
1031  update_in_place,
1032  location);
1033  }
1034  else if(followed_type.id() == ID_struct)
1035  {
1036  const struct_typet struct_type = to_struct_type(followed_type);
1037 
1038  // If we are about to initialize a generic class (as a superclass object
1039  // for a different object), add its concrete types to the map and delete
1040  // them on leaving this function scope.
1042  generic_parameter_specialization_map_keys(
1044  if(is_sub)
1045  {
1046  const typet &symbol =
1047  override_type.has_value() ? *override_type : expr.type();
1048  PRECONDITION(symbol.id() == ID_struct_tag);
1049  generic_parameter_specialization_map_keys.insert(
1050  to_struct_tag_type(symbol), struct_type);
1051  }
1052 
1054  assignments,
1055  expr,
1056  is_sub,
1057  skip_classid,
1058  lifetime,
1059  struct_type,
1060  depth,
1061  update_in_place,
1062  location);
1063  }
1064  else
1065  {
1066  // types different from pointer or structure:
1067  // bool, int, float, byte, char, ...
1068  exprt rhs = type.id() == ID_c_bool
1069  ? get_nondet_bool(type, location)
1070  : side_effect_expr_nondett(type, location);
1071  code_assignt assign(expr, rhs);
1072  assign.add_source_location() = location;
1073 
1074  assignments.add(assign);
1076  {
1077  assignments.add(
1079  }
1080  // add assumes to obey numerical restrictions
1081  if(type != java_boolean_type() && type != java_char_type())
1082  {
1083  const auto &interval = object_factory_parameters.assume_inputs_interval;
1084  if(auto singleton = interval.as_singleton())
1085  {
1086  assignments.add(
1087  code_assignt{expr, from_integer(*singleton, expr.type())});
1088  }
1089  else
1090  {
1091  exprt within_bounds = interval.make_contains_expr(expr);
1092  if(!within_bounds.is_true())
1093  assignments.add(code_assumet(std::move(within_bounds)));
1094  }
1095 
1096  if(
1098  (type == java_float_type() || type == java_double_type()))
1099  {
1100  assignments.add(assume_expr_integral(
1101  expr,
1102  type,
1103  location,
1104  [this](
1105  const typet &type, std::string basename_prefix) -> symbol_exprt {
1107  type, basename_prefix);
1108  }));
1109  }
1110  }
1111  }
1112 }
1113 
1115 {
1117 }
1118 
1120 {
1122 }
1123 
1142  code_blockt &assignments,
1143  const exprt &lhs,
1144  const exprt &max_length_expr,
1145  const typet &element_type,
1146  const allocate_local_symbolt &allocate_local_symbol,
1147  const source_locationt &location)
1148 {
1149  const auto &length_sym_expr = generate_nondet_int(
1151  max_length_expr,
1152  "nondet_array_length",
1153  location,
1154  allocate_local_symbol,
1155  assignments);
1156 
1157  side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), location);
1158  java_new_array.copy_to_operands(length_sym_expr);
1159  java_new_array.set(ID_length_upper_bound, max_length_expr);
1160  java_new_array.type().subtype().set(ID_element_type, element_type);
1161  code_assignt assign(lhs, java_new_array);
1162  assign.add_source_location() = location;
1163  assignments.add(assign);
1164 }
1165 
1184  code_blockt &assignments,
1185  const exprt &init_array_expr,
1186  const typet &element_type,
1187  const exprt &max_length_expr,
1188  const source_locationt &location,
1189  const allocate_local_symbolt &allocate_local_symbol)
1190 {
1191  const array_typet array_type(element_type, max_length_expr);
1192 
1193  // TYPE (*array_data_init)[max_length_expr];
1194  const symbol_exprt &tmp_finite_array_pointer =
1195  allocate_local_symbol(pointer_type(array_type), "array_data_init");
1196 
1197  // array_data_init = ALLOCATE(TYPE [max_length_expr], max_length_expr, false);
1198  assignments.add(
1200  tmp_finite_array_pointer,
1201  max_length_expr));
1202  assignments.statements().back().add_source_location() = location;
1203 
1204  // *array_data_init = NONDET(TYPE [max_length_expr]);
1205  side_effect_expr_nondett nondet_data(array_type, location);
1206  const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};
1207  assignments.add(code_assignt(data_pointer_deref, std::move(nondet_data)));
1208  assignments.statements().back().add_source_location() = location;
1209 
1210  // init_array_expr = *array_data_init;
1211  address_of_exprt tmp_nondet_pointer(
1212  index_exprt(data_pointer_deref, from_integer(0, java_int_type())));
1213  assignments.add(code_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
1214  assignments.statements().back().add_source_location() = location;
1215 }
1216 
1227  const exprt &element,
1228  const update_in_placet update_in_place,
1229  const typet &element_type,
1230  const size_t depth,
1231  const source_locationt &location)
1232 {
1233  code_blockt assignments;
1234  bool new_item_is_primitive = element.type().id() != ID_pointer;
1235 
1236  // Use a temporary to initialise a new, or update an existing, non-primitive.
1237  // This makes it clearer that in a sequence like
1238  // `new_array_item->x = y; new_array_item->z = w;` that all the
1239  // `new_array_item` references must alias, cf. the harder-to-analyse
1240  // `some_expr[idx]->x = y; some_expr[idx]->z = w;`
1241  exprt init_expr;
1242  if(new_item_is_primitive)
1243  {
1244  init_expr = element;
1245  }
1246  else
1247  {
1249  element.type(), "new_array_item");
1250 
1251  // If we're updating an existing array item, read the existing object that
1252  // we (may) alter:
1253  if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
1254  assignments.add(code_assignt(init_expr, element));
1255  }
1256 
1257  // MUST_UPDATE_IN_PLACE only applies to this object.
1258  // If this is a pointer to another object, offer the chance
1259  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1260  update_in_placet child_update_in_place =
1261  update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE
1262  ? update_in_placet::MAY_UPDATE_IN_PLACE
1263  : update_in_place;
1265  assignments,
1266  init_expr,
1267  false, // is_sub
1268  false, // skip_classid
1269  // These are variable in number, so use dynamic allocator:
1271  element_type, // override
1272  depth,
1273  child_update_in_place,
1274  location);
1275 
1276  if(!new_item_is_primitive)
1277  {
1278  // We used a temporary variable to update or initialise an array item;
1279  // now write it into the array:
1280  assignments.add(code_assignt(element, init_expr));
1281  }
1282  return assignments;
1283 }
1284 
1326  code_blockt &assignments,
1327  const exprt &init_array_expr,
1328  const exprt &length_expr,
1329  const typet &element_type,
1330  const exprt &max_length_expr,
1331  update_in_placet update_in_place,
1332  const source_locationt &location,
1333  const array_element_generatort &element_generator,
1334  const allocate_local_symbolt &allocate_local_symbol,
1335  const symbol_tablet &symbol_table)
1336 {
1337  const symbol_exprt &array_init_symexpr =
1338  allocate_local_symbol(init_array_expr.type(), "array_data_init");
1339 
1340  code_assignt data_assign(array_init_symexpr, init_array_expr);
1341  data_assign.add_source_location() = location;
1342  assignments.add(data_assign);
1343 
1344  const symbol_exprt &counter_expr =
1345  allocate_local_symbol(length_expr.type(), "array_init_iter");
1346 
1347  code_blockt loop_body;
1348  if(update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
1349  {
1350  // Add a redundant if(counter == max_length) break
1351  // that is easier for the unwinder to understand.
1352  code_ifthenelset max_test(
1353  equal_exprt(counter_expr, max_length_expr), code_breakt{});
1354 
1355  loop_body.add(std::move(max_test));
1356  }
1357 
1358  const dereference_exprt element_at_counter =
1359  array_element_from_pointer(array_init_symexpr, counter_expr);
1360 
1361  loop_body.append(element_generator(element_at_counter, element_type));
1362 
1363  assignments.add(code_fort::from_index_bounds(
1365  length_expr,
1366  counter_expr,
1367  std::move(loop_body),
1368  location));
1369 }
1370 
1372  const exprt &expr,
1373  update_in_placet update_in_place,
1374  const source_locationt &location,
1375  const array_element_generatort &element_generator,
1376  const allocate_local_symbolt &allocate_local_symbol,
1377  const symbol_tablet &symbol_table,
1378  const size_t max_nondet_array_length)
1379 {
1380  PRECONDITION(expr.type().id() == ID_pointer);
1381  PRECONDITION(expr.type().subtype().id() == ID_struct_tag);
1382  PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
1383 
1384  code_blockt statements;
1385 
1386  const namespacet ns(symbol_table);
1387  const typet &type = ns.follow(expr.type().subtype());
1388  const struct_typet &struct_type = to_struct_type(type);
1389  const typet &element_type =
1390  static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
1391 
1392  auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
1393 
1394  // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1395  // initialize its elements
1396  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
1397  {
1399  statements,
1400  expr,
1401  max_length_expr,
1402  element_type,
1403  allocate_local_symbol,
1404  location);
1405  }
1406 
1407  // Otherwise we're updating the array in place, and use the
1408  // existing array allocation and length.
1409 
1410  INVARIANT(
1411  is_valid_java_array(struct_type),
1412  "Java struct array does not conform to expectations");
1413 
1414  dereference_exprt deref_expr(expr);
1415  const auto &comps = struct_type.components();
1416  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1417  exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());
1418 
1419  if(init_array_expr.type() != pointer_type(element_type))
1420  init_array_expr =
1421  typecast_exprt(init_array_expr, pointer_type(element_type));
1422 
1423  if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
1424  {
1425  // For arrays of non-primitive type, nondeterministically initialize each
1426  // element of the array
1428  statements,
1429  init_array_expr,
1430  length_expr,
1431  element_type,
1432  max_length_expr,
1433  update_in_place,
1434  location,
1435  element_generator,
1436  allocate_local_symbol,
1437  symbol_table);
1438  }
1439  else
1440  {
1441  // Arrays of primitive type can be initialized with a single instruction.
1442  // We don't do this for arrays of primitive booleans, because booleans are
1443  // represented as unsigned bytes, so each cell must be initialized as
1444  // 0 or 1 (see gen_nondet_init).
1446  statements,
1447  init_array_expr,
1448  element_type,
1449  max_length_expr,
1450  location,
1451  allocate_local_symbol);
1452  }
1453  return statements;
1454 }
1455 
1470  code_blockt &assignments,
1471  const exprt &expr,
1472  const java_class_typet &java_class_type,
1473  const source_locationt &location)
1474 {
1475  const irep_idt &class_name = java_class_type.get_name();
1476  const irep_idt values_name = id2string(class_name) + ".$VALUES";
1477  if(!symbol_table.has_symbol(values_name))
1478  {
1479  log.warning() << values_name
1480  << " is missing, so the corresponding Enum "
1481  "type will nondet initialised"
1482  << messaget::eom;
1483  return false;
1484  }
1485 
1486  const namespacet ns(symbol_table);
1487  const symbolt &values = ns.lookup(values_name);
1488 
1489  // Access members (length and data) of $VALUES array
1490  dereference_exprt deref_expr(values.symbol_expr());
1491  const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type()));
1492  PRECONDITION(is_valid_java_array(deref_struct_type));
1493  const auto &comps = deref_struct_type.components();
1494  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1495  const member_exprt enum_array_expr =
1496  member_exprt(deref_expr, "data", comps[2].type());
1497 
1498  const symbol_exprt &index_expr = generate_nondet_int(
1500  minus_exprt(length_expr, from_integer(1, java_int_type())),
1501  "enum_index_init",
1502  location,
1504  assignments);
1505 
1506  const dereference_exprt element_at_index =
1507  array_element_from_pointer(enum_array_expr, index_expr);
1508  code_assignt enum_assign(expr, typecast_exprt(element_at_index, expr.type()));
1509  assignments.add(enum_assign);
1510 
1511  return true;
1512 }
1513 
1514 static void assert_type_consistency(const code_blockt &assignments)
1515 {
1516  // In future we'll be able to use codet::validate for this;
1517  // at present that only verifies `lhs.type base_type_eq right.type`,
1518  // whereas we want to check exact equality.
1519  for(const auto &code : assignments.statements())
1520  {
1521  if(code.get_statement() != ID_assign)
1522  continue;
1523  const auto &assignment = to_code_assign(code);
1524  INVARIANT(
1525  assignment.lhs().type() == assignment.rhs().type(),
1526  "object factory should produce type-consistent assignments");
1527  }
1528 }
1529 
1542  const typet &type,
1543  const irep_idt base_name,
1544  code_blockt &init_code,
1545  symbol_table_baset &symbol_table,
1547  lifetimet lifetime,
1548  const source_locationt &loc,
1549  const select_pointer_typet &pointer_type_selector,
1550  message_handlert &log)
1551 {
1553  "::"+id2string(base_name);
1554 
1555  auxiliary_symbolt main_symbol;
1556  main_symbol.mode=ID_java;
1557  main_symbol.is_static_lifetime=false;
1558  main_symbol.name=identifier;
1559  main_symbol.base_name=base_name;
1560  main_symbol.type=type;
1561  main_symbol.location=loc;
1563 
1564  exprt object=main_symbol.symbol_expr();
1565 
1566  symbolt *main_symbol_ptr;
1567  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
1568  CHECK_RETURN(!moving_symbol_failed);
1569 
1570  java_object_factoryt state(
1571  loc, parameters, symbol_table, pointer_type_selector, log);
1572  code_blockt assignments;
1573  state.gen_nondet_init(
1574  assignments,
1575  object,
1576  false, // is_sub
1577  false, // skip_classid
1578  lifetime,
1579  {}, // no override_type
1580  1, // initial depth
1581  update_in_placet::NO_UPDATE_IN_PLACE,
1582  loc);
1583 
1584  state.add_created_symbol(main_symbol_ptr);
1585  state.declare_created_symbols(init_code);
1586 
1587  assert_type_consistency(assignments);
1588  init_code.append(assignments);
1589  return object;
1590 }
1591 
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:33
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:129
recursion_set_entryt::operator=
recursion_set_entryt & operator=(const recursion_set_entryt &)=delete
java_static_initializers.h
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
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
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:168
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
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:297
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:90
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_object_factoryt::symbol_table
symbol_table_baset & symbol_table
The symbol table.
Definition: java_object_factory.cpp:52
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:1183
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:1141
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:11
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:279
arith_tools.h
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
select_pointer_type.h
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
lifetimet::AUTOMATIC_LOCAL
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
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:14
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
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:473
java_string_literals.h
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
to_integer_bitvector_type
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
Definition: bitvector_types.h:142
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:79
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:1371
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:106
prefix.h
recursion_set_entryt
Recursion-set entry owner class.
Definition: java_object_factory.cpp:269
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
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:76
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:833
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
java_string_library_preprocess.h
Produce code for simple implementation of String Java libraries.
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:449
java_object_factory_parameters.h
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:727
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
bool_typet
The Boolean type.
Definition: std_types.h:36
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:57
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:147
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:33
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:80
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:32
equal_exprt
Equality.
Definition: std_expr.h:1225
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:776
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:317
assert_type_consistency
static void assert_type_consistency(const code_blockt &assignments)
Definition: java_object_factory.cpp:1514
java_class_typet
Definition: java_types.h:197
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:58
generic_parameter_specialization_map_keyst
Definition: generic_parameter_specialization_map_keys.h:15
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
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:20
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:176
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
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:73
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:73
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:168
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:83
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:890
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:73
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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:26
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:703
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1628
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:763
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:691
interval_constraint.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:271
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
java_object_factoryt
Definition: java_object_factory.cpp:32
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
recursion_set_entryt::~recursion_set_entryt
~recursion_set_entryt()
Removes erase_entry (if set) from the controlled set.
Definition: java_object_factory.cpp:284
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:1541
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:23
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
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
java_object_factoryt::allocate_objects
allocate_objectst allocate_objects
Definition: java_object_factory.cpp:59
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
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:62
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:474
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:206
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:364
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:189
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:31
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:273
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:316
minus_exprt
Binary minus.
Definition: std_expr.h:973
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:34
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:18
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:70
source_locationt
Definition: source_location.h:19
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
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:557
allocate_local_symbolt
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:18
java_object_factoryt::add_created_symbol
void add_created_symbol(const symbolt *symbol)
Definition: java_object_factory.cpp:1114
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
java_object_factoryt::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Definition: java_object_factory.cpp:1119
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:41
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:939
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
array_typet
Arrays with given size.
Definition: std_types.h:763
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:73
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:44
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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:997
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
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:89
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:61
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
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:72
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:214
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: bitvector_types.cpp:38
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:79
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:28
get_nondet_bool
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:21
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:1325
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:49
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
exprt::operands
operandst & operands()
Definition: expr.h:92
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
index_exprt
Array index operator.
Definition: std_expr.h:1328
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
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:1866
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
message.h
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:230
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:1469
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:1896
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:67
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1691
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:1226
nondet_bool.h
Nondeterministic boolean helper.
resolve_inherited_componentt
Definition: resolve_inherited_component.h:23
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:39