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/expr_initializer.h>
12 #include <util/fresh_symbol.h>
13 #include <util/nondet_bool.h>
15 
18 
20 #include "java_root_class.h"
21 
23 {
27  std::vector<const symbolt *> &symbols_created;
28 
32 
34 
39  std::unordered_set<irep_idt> recursion_set;
40 
50 
53 
56 
61 
63  const exprt &expr,
64  const pointer_typet &ptr_type);
65 
67  code_blockt &assignments,
68  const exprt &expr,
69  const typet &target_type,
70  allocation_typet alloc_type,
71  size_t depth,
72  update_in_placet update_in_place);
73 
75  code_blockt &assignments,
76  const exprt &lhs,
77  const exprt &max_length_expr,
78  const typet &element_type);
79 
80 public:
82  std::vector<const symbolt *> &_symbols_created,
83  const source_locationt &loc,
84  const object_factory_parameterst _object_factory_parameters,
85  symbol_table_baset &_symbol_table,
87  : symbols_created(_symbols_created),
88  loc(loc),
89  object_factory_parameters(_object_factory_parameters),
90  symbol_table(_symbol_table),
91  ns(_symbol_table),
93  {}
94 
96  code_blockt &assignments,
97  const exprt &,
98  const typet &,
99  allocation_typet alloc_type);
100 
102  code_blockt &assignments,
103  const exprt &expr,
104  size_t depth,
106 
107  void gen_nondet_init(
108  code_blockt &assignments,
109  const exprt &expr,
110  bool is_sub,
111  irep_idt class_identifier,
112  bool skip_classid,
113  allocation_typet alloc_type,
114  bool override_,
115  const typet &override_type,
116  size_t depth,
118 
119 private:
121  code_blockt &assignments,
122  const exprt &expr,
123  const irep_idt &class_identifier,
124  allocation_typet alloc_type,
126  size_t depth,
127  const update_in_placet &update_in_place);
128 
130  code_blockt &assignments,
131  const exprt &expr,
132  bool is_sub,
133  irep_idt class_identifier,
134  bool skip_classid,
135  allocation_typet alloc_type,
136  const struct_typet &struct_type,
137  size_t depth,
138  const update_in_placet &update_in_place);
139 
141  code_blockt &assignments,
142  allocation_typet alloc_type,
143  const pointer_typet &substitute_pointer_type,
144  size_t depth);
145 };
146 
161  const exprt &target_expr,
162  const typet &allocate_type,
163  symbol_table_baset &symbol_table,
164  const source_locationt &loc,
165  const irep_idt &function_id,
166  code_blockt &output_code,
167  std::vector<const symbolt *> &symbols_created,
168  bool cast_needed)
169 {
170  // build size expression
171  exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table));
172 
173  if(allocate_type.id()!=ID_empty)
174  {
175  INVARIANT(!object_size.is_nil(), "Size of Java objects should be known");
176  // malloc expression
177  side_effect_exprt malloc_expr(ID_allocate, pointer_type(allocate_type));
178  malloc_expr.copy_to_operands(object_size);
179  malloc_expr.copy_to_operands(false_exprt());
180  // create a symbol for the malloc expression so we can initialize
181  // without having to do it potentially through a double-deref, which
182  // breaks the to-SSA phase.
183  symbolt &malloc_sym = get_fresh_aux_symbol(
184  pointer_type(allocate_type),
185  id2string(function_id),
186  "malloc_site",
187  loc,
188  ID_java,
189  symbol_table);
190  symbols_created.push_back(&malloc_sym);
191  code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
192  assign.add_source_location()=loc;
193  output_code.copy_to_operands(assign);
194  exprt malloc_symbol_expr=malloc_sym.symbol_expr();
195  if(cast_needed)
196  malloc_symbol_expr=typecast_exprt(malloc_symbol_expr, target_expr.type());
197  code_assignt code(target_expr, malloc_symbol_expr);
198  code.add_source_location()=loc;
199  output_code.copy_to_operands(code);
200  return malloc_sym.symbol_expr();
201  }
202  else
203  {
204  // make null
205  null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type()));
206  code_assignt code(target_expr, null_pointer_expr);
207  code.add_source_location()=loc;
208  output_code.copy_to_operands(code);
209  return exprt();
210  }
211 }
212 
223  const exprt &target_expr,
224  symbol_table_baset &symbol_table,
225  const source_locationt &loc,
226  const irep_idt &function_id,
227  code_blockt &output_code)
228 {
229  std::vector<const symbolt *> symbols_created;
230  code_blockt tmp_block;
231  const typet &allocate_type=target_expr.type().subtype();
233  target_expr,
234  allocate_type,
235  symbol_table,
236  loc,
237  function_id,
238  tmp_block,
239  symbols_created,
240  false);
241 
242  // Add the following code to output_code for each symbol that's been created:
243  // <type> <identifier>;
244  for(const symbolt * const symbol_ptr : symbols_created)
245  {
246  code_declt decl(symbol_ptr->symbol_expr());
247  decl.add_source_location()=loc;
248  output_code.add(decl);
249  }
250 
251  for(const exprt &code : tmp_block.operands())
252  output_code.add(to_code(code));
253  return dynamic_object;
254 }
255 
268  code_blockt &assignments,
269  const exprt &target_expr,
270  const typet &allocate_type,
271  allocation_typet alloc_type)
272 {
273  const typet &allocate_type_resolved=ns.follow(allocate_type);
274  const typet &target_type=ns.follow(target_expr.type().subtype());
275  bool cast_needed=allocate_type_resolved!=target_type;
276  switch(alloc_type)
277  {
280  {
281  symbolt &aux_symbol = get_fresh_aux_symbol(
282  allocate_type,
284  "tmp_object_factory",
285  loc,
286  ID_java,
287  symbol_table);
288  if(alloc_type==allocation_typet::GLOBAL)
289  aux_symbol.is_static_lifetime=true;
290  symbols_created.push_back(&aux_symbol);
291 
292  exprt object=aux_symbol.symbol_expr();
293  exprt aoe=address_of_exprt(object);
294  if(cast_needed)
295  aoe=typecast_exprt(aoe, target_expr.type());
296  code_assignt code(target_expr, aoe);
297  code.add_source_location()=loc;
298  assignments.copy_to_operands(code);
299  return aoe;
300  }
302  {
304  target_expr,
305  allocate_type,
306  symbol_table,
307  loc,
309  assignments,
311  cast_needed);
312  }
313  default:
314  UNREACHABLE;
315  return exprt();
316  } // End switch
317 }
318 
321  const exprt &expr,
322  const pointer_typet &ptr_type)
323 {
324  null_pointer_exprt null_pointer_expr(ptr_type);
325  code_assignt code(expr, null_pointer_expr);
326  code.add_source_location()=loc;
327  return code;
328 }
329 
370  code_blockt &assignments,
371  const exprt &expr,
372  const typet &target_type,
373  allocation_typet alloc_type,
374  size_t depth,
375  update_in_placet update_in_place)
376 {
377  PRECONDITION(expr.type().id()==ID_pointer);
379 
380  if(target_type.id()==ID_struct &&
381  has_prefix(
382  id2string(to_struct_type(target_type).get_tag()),
383  "java::array["))
384  {
386  assignments,
387  expr,
388  depth+1,
389  update_in_place);
390  }
391  else
392  {
393  // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
394  // initialize the fields of the object pointed by `expr`; if in
395  // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
396  // (return value of `allocate_object`), emit a statement of the form
397  // `<expr> := address-of(<new-object>)` and recursively initialize such new
398  // object.
399  exprt target;
400  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
401  {
402  target=allocate_object(
403  assignments,
404  expr,
405  target_type,
406  alloc_type);
407  INVARIANT(
408  target.type().id()==ID_pointer,
409  "Pointer-typed expression expected");
410  }
411  else
412  {
413  target=expr;
414  }
415 
416  // we dereference the pointer and initialize the resulting object using a
417  // recursive call
418  exprt init_expr;
419  if(target.id()==ID_address_of)
420  init_expr=target.op0();
421  else
422  {
423  init_expr=
424  dereference_exprt(target, target.type().subtype());
425  }
427  assignments,
428  init_expr,
429  false, // is_sub
430  "", // class_identifier
431  false, // skip_classid
432  alloc_type,
433  false, // override
434  typet(), // override type immaterial
435  depth+1,
436  update_in_place);
437  }
438 }
439 
444 {
446  std::unordered_set<irep_idt> &recursion_set;
449 
450 public:
454  explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
455  : recursion_set(_recursion_set)
456  { }
457 
460  {
461  if(erase_entry!=irep_idt())
462  recursion_set.erase(erase_entry);
463  }
464 
467 
472  bool insert_entry(const irep_idt &entry)
473  {
474  INVARIANT(
476  "insert_entry should only be called once");
477  INVARIANT(entry!=irep_idt(), "entry should be a struct tag");
478  bool ret=recursion_set.insert(entry).second;
479  if(ret)
480  {
481  // We added something, so erase it when this is destroyed:
482  erase_entry=entry;
483  }
484  return ret;
485  }
486 };
487 
492 static mp_integer max_value(const typet &type)
493 {
494  if(type.id() == ID_signedbv)
495  return to_signedbv_type(type).largest();
496  else if(type.id() == ID_unsignedbv)
497  return to_unsignedbv_type(type).largest();
498  UNREACHABLE;
499 }
500 
505 static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
506 {
507  side_effect_exprt alloc(ID_allocate, lhs.type());
508  alloc.copy_to_operands(size);
509  alloc.copy_to_operands(false_exprt());
510  return code_assignt(lhs, alloc);
511 }
512 
546  const exprt &obj,
547  const std::size_t &max_nondet_string_length,
548  const source_locationt &loc,
549  const irep_idt &function_id,
550  symbol_table_baset &symbol_table,
551  bool printable)
552 {
553  PRECONDITION(
555 
556  const namespacet ns(symbol_table);
557  code_blockt code;
558 
559  // `obj` is `*expr`
560  const struct_typet &struct_type = to_struct_type(ns.follow(obj.type()));
561  // @clsid = java::java.lang.String or similar.
562  // We allow type StringBuffer and StringBuilder to be initialized
563  // in the same way has String, because they have the same structure and
564  // are treated in the same way by CBMC.
565  // Note that CharSequence cannot be used as classid because it's abstract,
566  // so it is replaced by String.
567  // \todo allow StringBuffer and StringBuilder as classid for Charsequence
568  const irep_idt &class_id =
569  struct_type.get_tag() == "java.lang.CharSequence"
570  ? "java::java.lang.String"
571  : "java::" + id2string(struct_type.get_tag());
572 
573  // @lock = false:
574  const symbol_typet jlo_symbol("java::java.lang.Object");
575  const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol));
576  struct_exprt jlo_init(jlo_symbol);
577  java_root_class_init(jlo_init, jlo_type, false, class_id);
578 
579  struct_exprt struct_expr(obj.type());
580  struct_expr.copy_to_operands(jlo_init);
581 
582  // In case the type for string was not added to the symbol table,
583  // (typically when string refinement is not activated), `struct_type`
584  // just contains the standard Object field and no length and data fields.
585  if(struct_type.has_component("length"))
586  {
588  // length_expr = nondet(int);
589  const symbolt length_sym = get_fresh_aux_symbol(
590  java_int_type(),
591  id2string(function_id),
592  "tmp_object_factory",
593  loc,
594  ID_java,
595  symbol_table);
596  const symbol_exprt length_expr = length_sym.symbol_expr();
597  const side_effect_expr_nondett nondet_length(length_expr.type());
598  code.add(code_declt(length_expr));
599  code.add(code_assignt(length_expr, nondet_length));
600 
601  // assume (length_expr >= 0);
602  code.add(
603  code_assumet(
605  length_expr, ID_ge, from_integer(0, java_int_type()))));
606 
607  // assume (length_expr <= max_input_length)
608  if(max_nondet_string_length <= max_value(length_expr.type()))
609  {
610  exprt max_length =
611  from_integer(max_nondet_string_length, length_expr.type());
612  code.add(
613  code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
614  }
615 
616  // char (*array_data_init)[INFINITY];
617  const typet data_ptr_type = pointer_type(
619 
620  symbolt &data_pointer_sym = get_fresh_aux_symbol(
621  data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table);
622  const auto data_pointer = data_pointer_sym.symbol_expr();
623  code.add(code_declt(data_pointer));
624 
625  // Dynamic allocation: `data array = allocate char[INFINITY]`
626  code.add(make_allocate_code(data_pointer, infinity_exprt(java_int_type())));
627 
628  // `data_expr` is `*data_pointer`
629  // data_expr = nondet(char[INFINITY]) // we use infinity for variable size
630  const dereference_exprt data_expr(data_pointer);
631  const exprt nondet_array =
632  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
633  code.add(code_assignt(data_expr, nondet_array));
634 
635  struct_expr.copy_to_operands(length_expr);
636 
637  const address_of_exprt array_pointer(
638  index_exprt(data_expr, from_integer(0, java_int_type())));
639 
641  array_pointer, data_expr, symbol_table, loc, code);
642 
644  data_expr, length_expr, symbol_table, loc, code);
645 
646  struct_expr.copy_to_operands(array_pointer);
647 
648  // Printable ASCII characters are between ' ' and '~'.
649  if(printable)
650  {
652  array_pointer, length_expr, " -~", symbol_table, loc, code);
653  }
654  }
655 
656  // tmp_object = struct_expr;
657  code.add(code_assignt(obj, struct_expr));
658  return code;
659 }
660 
673  const exprt &expr,
674  const std::size_t &max_nondet_string_length,
675  bool printable,
676  symbol_table_baset &symbol_table,
677  const source_locationt &loc,
678  const irep_idt &function_id,
679  code_blockt &code)
680 {
681  const namespacet ns(symbol_table);
682  const dereference_exprt obj(expr, expr.type().subtype());
683  const struct_typet &struct_type =
684  to_struct_type(ns.follow(to_symbol_type(obj.type())));
685 
686  // if no String model is loaded then we cannot construct a String object
687  if(struct_type.get_bool(ID_incomplete_class))
688  return true;
689 
690  const exprt malloc_site = allocate_dynamic_object_with_decl(
691  expr, symbol_table, loc, function_id, code);
692 
693  code.add(
695  dereference_exprt(malloc_site, struct_type),
696  max_nondet_string_length,
697  loc,
698  function_id,
699  symbol_table,
700  printable));
701  return false;
702 }
703 
729  code_blockt &assignments,
730  const exprt &expr,
731  const irep_idt &class_identifier,
732  allocation_typet alloc_type,
734  size_t depth,
735  const update_in_placet &update_in_place)
736 {
737  PRECONDITION(expr.type().id()==ID_pointer);
738  const pointer_typet &replacement_pointer_type =
741 
742  // If we are changing the pointer, we generate code for creating a pointer
743  // to the substituted type instead
744  // TODO if we are comparing array types we need to compare their element
745  // types. this is for now done by implementing equality function especially
746  // for java types, technical debt TG-2707
747  if(!equal_java_types(replacement_pointer_type, pointer_type))
748  {
749  // update generic_parameter_specialization_map for the new pointer
751  generic_parameter_specialization_map_keys(
753  generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
754  replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
755 
756  const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
757  assignments, alloc_type, replacement_pointer_type, depth);
758 
759  // Having created a pointer to object of type replacement_pointer_type
760  // we now assign it back to the original pointer with a cast
761  // from pointer_type to replacement_pointer_type
762  assignments.add(
763  code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
764  return;
765  }
766 
767  // This deletes the recursion set entry on leaving this function scope,
768  // if one is set below.
769  recursion_set_entryt recursion_set_entry(recursion_set);
770 
771  // If the pointed value is struct-typed, then we need to prevent the
772  // possibility of this code to loop infinitely when initializing a data
773  // structure with recursive types or unbounded depth. We implement two
774  // mechanisms here. We keep a set of 'types seen', and detect when we perform
775  // a 2nd visit to the same type. We also detect the depth in the chain of
776  // (recursive) calls to the methods of this class. The depth counter is
777  // incremented only when a pointer is deferenced, including pointers to
778  // arrays.
779  //
780  // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
781  // the pointer to NULL instead of recursively initializing the struct to which
782  // it points.
783  const typet &subtype=ns.follow(pointer_type.subtype());
784  if(subtype.id()==ID_struct)
785  {
786  const struct_typet &struct_type=to_struct_type(subtype);
787  const irep_idt &struct_tag=struct_type.get_tag();
788 
789  // If this is a recursive type of some kind AND the depth is exceeded, set
790  // the pointer to null.
791  if(!recursion_set_entry.insert_entry(struct_tag) &&
793  {
794  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
795  {
796  assignments.copy_to_operands(
798  }
799  // Otherwise leave it as it is.
800  return;
801  }
802  }
803 
804  code_blockt new_object_assignments;
805  code_blockt update_in_place_assignments;
806 
807  // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
808  // emit to `update_in_place_assignments` code for in-place initialization of
809  // the object pointed by `expr`, assuming that such object is of type
810  // `subtype`
811  if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
812  {
814  update_in_place_assignments,
815  expr,
816  subtype,
817  alloc_type,
818  depth,
820  }
821 
822  // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
823  // above to `assignments` and return
824  if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
825  {
826  assignments.append(update_in_place_assignments);
827  return;
828  }
829 
830  // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
831  // vector of assignments that create a new object (recursively initializes it)
832  // and asign to `expr` the address of such object
833  code_blockt non_null_inst;
834 
835  // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not
836  // have the expected fields (typically this happens if --refine-strings was not passed). In this
837  // case we fall back to normal pointer target init.
838  bool string_init_succeeded = false;
839 
841  expr.type()))
842  {
843  string_init_succeeded =
845  expr,
848  symbol_table,
849  loc,
851  assignments);
852  }
853 
854  if(!string_init_succeeded)
855  {
857  non_null_inst,
858  expr,
859  subtype,
860  alloc_type,
861  depth,
863  }
864 
865  auto set_null_inst=get_null_assignment(expr, pointer_type);
866 
867  const bool allow_null =
869 
870  // Alternatively, if this is a void* we *must* initialise with null:
871  // (This can currently happen for some cases of #exception_value)
872  bool must_be_null = subtype == empty_typet();
873 
874  if(must_be_null)
875  {
876  // Add the following code to assignments:
877  // <expr> = nullptr;
878  new_object_assignments.add(set_null_inst);
879  }
880  else if(!allow_null)
881  {
882  // Add the following code to assignments:
883  // <expr> = <aoe>;
884  new_object_assignments.append(non_null_inst);
885  }
886  else
887  {
888  // if(NONDET(_Bool)
889  // {
890  // <expr> = <null pointer>
891  // }
892  // else
893  // {
894  // <code from recursive call to gen_nondet_init() with
895  // tmp$<temporary_counter>>
896  // }
897  code_ifthenelset null_check;
898  null_check.cond()=side_effect_expr_nondett(bool_typet());
899  null_check.then_case()=set_null_inst;
900  null_check.else_case()=non_null_inst;
901 
902  new_object_assignments.add(null_check);
903  }
904 
905  // Similarly to above, maybe use a conditional if both the
906  // allocate-fresh and update-in-place cases are allowed:
907  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
908  {
909  assignments.append(new_object_assignments);
910  }
911  else
912  {
914  "No-update and must-update should have already been resolved");
915 
916  code_ifthenelset update_check;
917  update_check.cond()=side_effect_expr_nondett(bool_typet());
918  update_check.then_case()=update_in_place_assignments;
919  update_check.else_case()=new_object_assignments;
920 
921  assignments.add(update_check);
922  }
923 }
924 
950  code_blockt &assignments,
951  allocation_typet alloc_type,
952  const pointer_typet &replacement_pointer,
953  size_t depth)
954 {
955  symbolt new_symbol = get_fresh_aux_symbol(
956  replacement_pointer,
958  "tmp_object_factory",
959  loc,
960  ID_java,
961  symbol_table);
962 
963  // Generate a new object into this new symbol
965  assignments,
966  new_symbol.symbol_expr(),
967  false, // is_sub
968  "", // class_identifier
969  false, // skip_classid
970  alloc_type,
971  false, // override
972  typet(), // override_type
973  depth,
975 
976  return new_symbol.symbol_expr();
977 }
978 
1009  code_blockt &assignments,
1010  const exprt &expr,
1011  bool is_sub,
1012  irep_idt class_identifier,
1013  bool skip_classid,
1014  allocation_typet alloc_type,
1015  const struct_typet &struct_type,
1016  size_t depth,
1017  const update_in_placet &update_in_place)
1018 {
1019  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
1020  PRECONDITION(struct_type.id()==ID_struct);
1021 
1022  typedef struct_typet::componentst componentst;
1023  const irep_idt &struct_tag=struct_type.get_tag();
1024 
1025  const componentst &components=struct_type.components();
1026 
1027  // Should we write the whole object?
1028  // * Not if this is a sub-structure (a superclass object), as our caller will
1029  // have done this already
1030  // * Not if the object has already been initialised by our caller, in whic
1031  // case they will set `skip_classid`
1032  // * Not if we're re-initializing an existing object (i.e. update_in_place)
1033 
1034  if(!is_sub &&
1035  !skip_classid &&
1036  update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
1037  {
1038  class_identifier = struct_tag;
1039 
1040  // Add an initial all-zero write. Most of the fields of this will be
1041  // overwritten, but it helps to have a whole-structure write that analysis
1042  // passes can easily recognise leaves no uninitialised state behind.
1043 
1044  // This code mirrors the `remove_java_new` pass:
1045  null_message_handlert nullout;
1046  exprt zero_object=
1048  struct_type, source_locationt(), ns, nullout);
1049  irep_idt qualified_clsid = "java::" + id2string(class_identifier);
1051  to_struct_expr(zero_object), ns, symbol_typet(qualified_clsid));
1052 
1053  assignments.copy_to_operands(
1054  code_assignt(expr, zero_object));
1055  }
1056 
1057  for(const auto &component : components)
1058  {
1059  const typet &component_type=component.type();
1060  irep_idt name=component.get_name();
1061 
1062  member_exprt me(expr, name, component_type);
1063 
1064  if(name=="@class_identifier")
1065  {
1066  continue;
1067  }
1068  else if(name=="@lock")
1069  {
1070  continue;
1071  }
1072  else
1073  {
1074  INVARIANT(!name.empty(), "Each component of a struct must have a name");
1075 
1076  bool _is_sub=name[0]=='@';
1077 
1078  // MUST_UPDATE_IN_PLACE only applies to this object.
1079  // If this is a pointer to another object, offer the chance
1080  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1081  update_in_placet substruct_in_place=
1082  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE && !_is_sub ?
1084  update_in_place;
1086  assignments,
1087  me,
1088  _is_sub,
1089  class_identifier,
1090  false, // skip_classid
1091  alloc_type,
1092  false, // override
1093  typet(), // override_type
1094  depth,
1095  substruct_in_place);
1096  }
1097  }
1098 
1099  // If <class_identifier>.cproverNondetInitialize() can be found in the
1100  // symbol table, we add a call:
1101  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1102  // expr.cproverNondetInitialize();
1103  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1104 
1105  const irep_idt init_method_name =
1106  "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V";
1107 
1108  if(const auto func = symbol_table.lookup(init_method_name))
1109  {
1110  const code_typet &type = to_code_type(func->type);
1111  code_function_callt fun_call;
1112  fun_call.function() = func->symbol_expr();
1113  if(type.has_this())
1114  fun_call.arguments().push_back(address_of_exprt(expr));
1115 
1116  assignments.add(fun_call);
1117  }
1118 }
1119 
1154  code_blockt &assignments,
1155  const exprt &expr,
1156  bool is_sub,
1157  irep_idt class_identifier,
1158  bool skip_classid,
1159  allocation_typet alloc_type,
1160  bool override_,
1161  const typet &override_type,
1162  size_t depth,
1163  update_in_placet update_in_place)
1164 {
1165  const typet &type=
1166  override_ ? ns.follow(override_type) : ns.follow(expr.type());
1167 
1168 
1169  if(type.id()==ID_pointer)
1170  {
1171  // dereferenced type
1173 
1174  // If we are about to initialize a generic pointer type, add its concrete
1175  // types to the map and delete them on leaving this function scope.
1177  generic_parameter_specialization_map_keys(
1179  generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
1181 
1183  assignments,
1184  expr,
1185  class_identifier,
1186  alloc_type,
1187  pointer_type,
1188  depth,
1189  update_in_place);
1190  }
1191  else if(type.id()==ID_struct)
1192  {
1193  const struct_typet struct_type=to_struct_type(type);
1194 
1195  // If we are about to initialize a generic class (as a superclass object
1196  // for a different object), add its concrete types to the map and delete
1197  // them on leaving this function scope.
1199  generic_parameter_specialization_map_keys(
1201  if(is_sub)
1202  {
1203  const typet &symbol = override_ ? override_type : expr.type();
1204  PRECONDITION(symbol.id() == ID_symbol);
1205  generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
1206  to_symbol_type(symbol), struct_type);
1207  }
1208 
1210  assignments,
1211  expr,
1212  is_sub,
1213  class_identifier,
1214  skip_classid,
1215  alloc_type,
1216  struct_type,
1217  depth,
1218  update_in_place);
1219  }
1220  else
1221  {
1222  // types different from pointer or structure:
1223  // bool, int, float, byte, char, ...
1224  exprt rhs=type.id()==ID_c_bool?
1225  get_nondet_bool(type):
1227  code_assignt assign(expr, rhs);
1228  assign.add_source_location()=loc;
1229 
1230  assignments.copy_to_operands(assign);
1231  }
1232 }
1233 
1248  code_blockt &assignments,
1249  const exprt &lhs,
1250  const exprt &max_length_expr,
1251  const typet &element_type)
1252 {
1253  symbolt &length_sym = get_fresh_aux_symbol(
1254  java_int_type(),
1256  "nondet_array_length",
1257  loc,
1258  ID_java,
1259  symbol_table);
1260  symbols_created.push_back(&length_sym);
1261  const auto &length_sym_expr=length_sym.symbol_expr();
1262 
1263  // Initialize array with some undetermined length:
1265  assignments,
1266  length_sym_expr,
1267  false, // is_sub
1268  irep_idt(),
1269  false, // skip_classid
1270  allocation_typet::LOCAL, // immaterial, type is primitive
1271  false, // override
1272  typet(), // override type is immaterial
1273  0, // depth is immaterial, always non-null
1275 
1276  // Insert assumptions to bound its length:
1278  assume1(length_sym_expr, ID_ge, from_integer(0, java_int_type()));
1280  assume2(length_sym_expr, ID_le, max_length_expr);
1281  code_assumet assume_inst1(assume1);
1282  code_assumet assume_inst2(assume2);
1283  assignments.move_to_operands(assume_inst1);
1284  assignments.move_to_operands(assume_inst2);
1285 
1286  side_effect_exprt java_new_array(ID_java_new_array, lhs.type());
1287  java_new_array.copy_to_operands(length_sym_expr);
1288  java_new_array.set(ID_length_upper_bound, max_length_expr);
1289  java_new_array.type().subtype().set(ID_C_element_type, element_type);
1290  code_assignt assign(lhs, java_new_array);
1291  assign.add_source_location()=loc;
1292  assignments.copy_to_operands(assign);
1293 }
1294 
1302  code_blockt &assignments,
1303  const exprt &expr,
1304  size_t depth,
1305  update_in_placet update_in_place)
1306 {
1307  PRECONDITION(expr.type().id()==ID_pointer);
1308  PRECONDITION(expr.type().subtype().id()==ID_symbol);
1310 
1311  const typet &type=ns.follow(expr.type().subtype());
1312  const struct_typet &struct_type=to_struct_type(type);
1313  const typet &element_type=
1314  static_cast<const typet &>(expr.type().subtype().find(ID_C_element_type));
1315 
1316  auto max_length_expr=from_integer(
1318 
1319  // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1320  // initialize its elements
1321  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
1322  {
1324  assignments,
1325  expr,
1326  max_length_expr,
1327  element_type);
1328  }
1329 
1330  // Otherwise we're updating the array in place, and use the
1331  // existing array allocation and length.
1332 
1333  INVARIANT(
1334  is_valid_java_array(struct_type),
1335  "Java struct array does not conform to expectations");
1336 
1337  dereference_exprt deref_expr(expr, expr.type().subtype());
1338  const auto &comps=struct_type.components();
1339  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1340  exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type());
1341 
1342  if(init_array_expr.type()!=pointer_type(element_type))
1343  init_array_expr=
1344  typecast_exprt(init_array_expr, pointer_type(element_type));
1345 
1346  // Interpose a new symbol, as the goto-symex stage can't handle array indexing
1347  // via a cast.
1348  symbolt &array_init_symbol = get_fresh_aux_symbol(
1349  init_array_expr.type(),
1351  "array_data_init",
1352  loc,
1353  ID_java,
1354  symbol_table);
1355  symbols_created.push_back(&array_init_symbol);
1356  const auto &array_init_symexpr=array_init_symbol.symbol_expr();
1357  codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
1358  data_assign.add_source_location()=loc;
1359  assignments.copy_to_operands(data_assign);
1360 
1361  // Emit init loop for(array_init_iter=0; array_init_iter!=array.length;
1362  // ++array_init_iter) init(array[array_init_iter]);
1363  symbolt &counter = get_fresh_aux_symbol(
1364  length_expr.type(),
1366  "array_init_iter",
1367  loc,
1368  ID_java,
1369  symbol_table);
1370  symbols_created.push_back(&counter);
1371  exprt counter_expr=counter.symbol_expr();
1372 
1373  exprt java_zero=from_integer(0, java_int_type());
1374  assignments.copy_to_operands(code_assignt(counter_expr, java_zero));
1375 
1376  std::string head_name = id2string(counter.base_name) + "_header";
1377  code_labelt init_head_label(head_name, code_skipt());
1378  code_gotot goto_head(head_name);
1379 
1380  assignments.move_to_operands(init_head_label);
1381 
1382  std::string done_name = id2string(counter.base_name) + "_done";
1383  code_labelt init_done_label(done_name, code_skipt());
1384  code_gotot goto_done(done_name);
1385 
1386  code_ifthenelset done_test;
1387  done_test.cond()=equal_exprt(counter_expr, length_expr);
1388  done_test.then_case()=goto_done;
1389 
1390  assignments.move_to_operands(done_test);
1391 
1392  if(update_in_place!=update_in_placet::MUST_UPDATE_IN_PLACE)
1393  {
1394  // Add a redundant if(counter == max_length) break
1395  // that is easier for the unwinder to understand.
1396  code_ifthenelset max_test;
1397  max_test.cond()=equal_exprt(counter_expr, max_length_expr);
1398  max_test.then_case()=goto_done;
1399 
1400  assignments.move_to_operands(max_test);
1401  }
1402 
1403  const dereference_exprt arraycellref(
1404  plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()),
1405  array_init_symexpr.type().subtype());
1406 
1407  // MUST_UPDATE_IN_PLACE only applies to this object.
1408  // If this is a pointer to another object, offer the chance
1409  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1410  update_in_placet child_update_in_place=
1411  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE ?
1413  update_in_place;
1415  assignments,
1416  arraycellref,
1417  false, // is_sub
1418  irep_idt(), // class_identifier
1419  false, // skip_classid
1420  // These are variable in number, so use dynamic allocator:
1422  true, // override
1423  element_type,
1424  depth,
1425  child_update_in_place);
1426 
1427  exprt java_one=from_integer(1, java_int_type());
1428  code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
1429 
1430  assignments.move_to_operands(incr);
1431  assignments.move_to_operands(goto_head);
1432  assignments.move_to_operands(init_done_label);
1433 }
1434 
1441  const std::vector<const symbolt *> &symbols_created,
1442  const source_locationt &loc,
1443  code_blockt &init_code)
1444 {
1445  // Add the following code to init_code for each symbol that's been created:
1446  // <type> <identifier>;
1447  for(const symbolt * const symbol_ptr : symbols_created)
1448  {
1449  if(!symbol_ptr->is_static_lifetime)
1450  {
1451  code_declt decl(symbol_ptr->symbol_expr());
1452  decl.add_source_location()=loc;
1453  init_code.add(decl);
1454  }
1455  }
1456 }
1457 
1470  const typet &type,
1471  const irep_idt base_name,
1472  code_blockt &init_code,
1473  symbol_table_baset &symbol_table,
1474  object_factory_parameterst parameters,
1475  allocation_typet alloc_type,
1476  const source_locationt &loc,
1477  const select_pointer_typet &pointer_type_selector)
1478 {
1480  "::"+id2string(base_name);
1481 
1482  auxiliary_symbolt main_symbol;
1483  main_symbol.mode=ID_java;
1484  main_symbol.is_static_lifetime=false;
1485  main_symbol.name=identifier;
1486  main_symbol.base_name=base_name;
1487  main_symbol.type=type;
1488  main_symbol.location=loc;
1490 
1491  exprt object=main_symbol.symbol_expr();
1492 
1493  symbolt *main_symbol_ptr;
1494  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
1495  CHECK_RETURN(!moving_symbol_failed);
1496 
1497  std::vector<const symbolt *> symbols_created;
1498  symbols_created.push_back(main_symbol_ptr);
1499  java_object_factoryt state(
1500  symbols_created,
1501  loc,
1502  parameters,
1503  symbol_table,
1504  pointer_type_selector);
1505  code_blockt assignments;
1506  state.gen_nondet_init(
1507  assignments,
1508  object,
1509  false, // is_sub
1510  "", // class_identifier
1511  false, // skip_classid
1512  alloc_type,
1513  false, // override
1514  typet(), // override_type is immaterial
1515  1, // initial depth
1517 
1518  declare_created_symbols(symbols_created, loc, init_code);
1519 
1520  init_code.append(assignments);
1521  return object;
1522 }
1523 
1560  const exprt &expr,
1561  code_blockt &init_code,
1562  symbol_table_baset &symbol_table,
1563  const source_locationt &loc,
1564  bool skip_classid,
1565  allocation_typet alloc_type,
1566  const object_factory_parameterst &object_factory_parameters,
1567  const select_pointer_typet &pointer_type_selector,
1568  update_in_placet update_in_place)
1569 {
1570  std::vector<const symbolt *> symbols_created;
1571 
1572  java_object_factoryt state(
1573  symbols_created,
1574  loc,
1575  object_factory_parameters,
1576  symbol_table,
1577  pointer_type_selector);
1578  code_blockt assignments;
1579  state.gen_nondet_init(
1580  assignments,
1581  expr,
1582  false, // is_sub
1583  "", // class_identifier
1584  skip_classid,
1585  alloc_type,
1586  false, // override
1587  typet(), // override_type is immaterial
1588  1, // initial depth
1589  update_in_place);
1590 
1591  declare_created_symbols(symbols_created, loc, init_code);
1592 
1593  init_code.append(assignments);
1594 }
1595 
1598  const typet &type,
1599  const irep_idt base_name,
1600  code_blockt &init_code,
1601  symbol_tablet &symbol_table,
1602  const object_factory_parameterst &object_factory_parameters,
1603  allocation_typet alloc_type,
1604  const source_locationt &location)
1605 {
1606  select_pointer_typet pointer_type_selector;
1607  return object_factory(
1608  type,
1609  base_name,
1610  init_code,
1611  symbol_table,
1612  object_factory_parameters,
1613  alloc_type,
1614  location,
1615  pointer_type_selector);
1616 }
1617 
1620  const exprt &expr,
1621  code_blockt &init_code,
1622  symbol_table_baset &symbol_table,
1623  const source_locationt &loc,
1624  bool skip_classid,
1625  allocation_typet alloc_type,
1626  const object_factory_parameterst &object_factory_parameters,
1627  update_in_placet update_in_place)
1628 {
1629  select_pointer_typet pointer_type_selector;
1631  expr,
1632  init_code,
1633  symbol_table,
1634  loc,
1635  skip_classid,
1636  alloc_type,
1637  object_factory_parameters,
1638  pointer_type_selector,
1639  update_in_place);
1640 }
#define loc()
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
allocation_typet
Selects the kind of allocation used by java_object_factory et al.
exprt size_of_expr(const typet &type, const namespacet &ns)
const codet & then_case() const
Definition: std_code.h:481
const object_factory_parameterst object_factory_parameters
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
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)...
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
code_assignt get_null_assignment(const exprt &expr, const pointer_typet &ptr_type)
Returns a codet that assigns expr, of type ptr_type, a NULL value.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
exprt & op0()
Definition: expr.h:72
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
const select_pointer_typet & pointer_type_selector
Resolves pointer types potentially using some heuristics, for example to replace pointers to interfac...
irep_idt mode
Language mode.
Definition: symbol.h:52
static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating object of size size and assigning it to lhs
const exprt & cond() const
Definition: std_code.h:471
irep_idt get_tag(const typet &type)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
typet java_int_type()
Definition: java_types.cpp:32
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Goto Programs with Functions.
symbol_table_baset & symbol_table
The symbol table.
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
Fresh auxiliary symbol creation.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
The null pointer constant.
Definition: std_expr.h:4520
recursion_set_entryt(std::unordered_set< irep_idt > &_recursion_set)
Initialize a recursion-set entry owner operating on a given set.
Allocate local stacked objects.
const componentst & components() const
Definition: std_types.h:245
Nondeterministic boolean helper.
A ‘goto’ instruction.
Definition: std_code.h:774
typet & type()
Definition: expr.h:56
Allocate global objects.
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
Structure type.
Definition: std_types.h:297
exprt get_nondet_bool(const typet &type)
Definition: nondet_bool.h:20
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:696
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const symbol_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct...
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
Extract member of struct or union.
Definition: std_expr.h:3871
void gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, const irep_idt &class_identifier, allocation_typet alloc_type, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place)
Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree...
equality
Definition: std_expr.h:1354
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:733
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.
Expression Initialization.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:189
An expression denoting infinity.
Definition: std_expr.h:4694
void add(const codet &code)
Definition: std_code.h:111
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:860
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr, size_t depth, update_in_placet)
Create code to initialize a Java array whose size will be at most max_nondet_array_length.
A reference into the symbol table.
Definition: std_types.h:110
size_t max_nondet_tree_depth
Maximum depth for object hierarchy on input.
static bool add_nondet_string_pointer_initialization(const exprt &expr, const std::size_t &max_nondet_string_length, bool printable, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add code for the initialization of a string using a nondeterministic content and association of its a...
A declaration of a local variable.
Definition: std_code.h:253
static void declare_created_symbols(const std::vector< const symbolt *> &symbols_created, const source_locationt &loc, code_blockt &init_code)
Add code_declt instructions to init_code for every non-static symbol in symbols_created ...
The pointer type.
Definition: std_types.h:1426
The empty type.
Definition: std_types.h:54
std::vector< const symbolt * > & symbols_created
Every new variable initialized by the code emitted by the methods of this class gets a symbol in the ...
bool string_printable
Force string content to be ASCII printable characters when set to true.
Operator to dereference a pointer.
Definition: std_expr.h:3284
The symbol table.
Definition: symbol_table.h:19
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A label for branch targets.
Definition: std_code.h:947
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:101
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
std::unordered_set< irep_idt > & recursion_set
Recursion set to modify.
A function call.
Definition: std_code.h:828
The plus expression.
Definition: std_expr.h:893
const typet & follow(const typet &) const
Definition: namespace.cpp:55
mp_integer largest() const
Definition: std_types.cpp:167
void gen_nondet_init(code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool skip_classid, allocation_typet alloc_type, bool override_, const typet &override_type, size_t depth, update_in_placet)
Initializes a primitive-typed or referece-typed object tree rooted at expr, allocating child objects ...
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
Operator to return the address of an object.
Definition: std_expr.h:3170
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1838
void gen_pointer_target_init(code_blockt &assignments, const exprt &expr, const typet &target_type, allocation_typet alloc_type, size_t depth, update_in_placet update_in_place)
Initializes the pointer-typed lvalue expression expr to point to an object of type target_type...
The boolean constant false.
Definition: std_expr.h:4499
update_in_placet
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:255
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const bool lock, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
Pointer Logic.
const void insert_pairs_for_pointer(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic pointer type ...
namespacet ns
A namespace built from exclusively one symbol table - the one above.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
An assumption, which must hold in subsequent code.
Definition: std_code.h:354
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
exprt allocate_dynamic_object_with_decl(const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code)
Generates code for allocating a dynamic object.
Allocate dynamic objects (using MALLOC)
mp_integer largest() const
Definition: std_types.cpp:142
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
static irep_idt entry_point()
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, object_factory_parameterst parameters, allocation_typet alloc_type, const source_locationt &loc, const select_pointer_typet &pointer_type_selector)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
void gen_nondet_struct_init(code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool skip_classid, allocation_typet alloc_type, const struct_typet &struct_type, size_t depth, const update_in_placet &update_in_place)
Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializ...
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & function()
Definition: std_code.h:848
irep_idt erase_entry
Entry to erase on destruction, if non-empty.
exprt allocate_dynamic_object(const exprt &target_expr, const typet &allocate_type, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code, std::vector< const symbolt *> &symbols_created, bool cast_needed)
Generates code for allocating a dynamic object.
Base class for all expressions.
Definition: expr.h:42
size_t max_nondet_string_length
Maximum value for the non-deterministically-chosen length of a string.
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
bool has_this() const
Definition: std_types.h:866
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type)
Allocates a fresh array and emits an assignment writing to lhs the address of the new array...
#define UNREACHABLE
Definition: invariant.h:250
static mp_integer max_value(const typet &type)
Get max value for an integer type.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
Recursion-set entry owner class.
std::unordered_set< irep_idt > recursion_set
This is employed in conjunction with the depth above.
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
static bool implements_java_char_sequence_pointer(const typet &type)
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
arrays with given size
Definition: std_types.h:1004
Skip.
Definition: std_code.h:178
An if-then-else.
Definition: std_code.h:461
java_object_factoryt(std::vector< const symbolt *> &_symbols_created, const source_locationt &loc, const object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
dstringt irep_idt
Definition: irep.h:31
exprt dynamic_object(const exprt &pointer)
A statement in a programming language.
Definition: std_code.h:21
recursion_set_entryt & operator=(const recursion_set_entryt &)=delete
~recursion_set_entryt()
Removes erase_entry (if set) from the controlled set.
codet initialize_nondet_string_struct(const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
Initialize a nondeterministic String structure.
typet java_char_type()
Definition: java_types.cpp:57
static bool implements_java_char_sequence(const typet &type)
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
const typet & subtype() const
Definition: type.h:33
symbol_exprt gen_nondet_subtype_pointer_init(code_blockt &assignments, allocation_typet alloc_type, const pointer_typet &substitute_pointer_type, size_t depth)
Generate codet assignments to initalize the selected concrete type.
irep_idt get_tag() const
Definition: std_types.h:266
An expression containing a side effect.
Definition: std_code.h:1238
operandst & operands()
Definition: expr.h:66
bool insert_entry(const irep_idt &entry)
Try to add an entry to the controlled set.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1815
const codet & else_case() const
Definition: std_code.h:491
exprt allocate_object(code_blockt &assignments, const exprt &, const typet &, allocation_typet alloc_type)
Installs a new symbol in the symbol table, pushing the corresponding symbolt object to the field symb...
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const source_locationt & loc
The source location for new statements emitted during the operation of the methods in this class...
Assignment.
Definition: std_code.h:195
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.
const void insert_pairs_for_symbol(const symbol_typet &symbol_type, const typet &symbol_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type t...
array index operator
Definition: std_expr.h:1462