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  const source_locationt &location);
74 
76  code_blockt &assignments,
77  const exprt &lhs,
78  const exprt &max_length_expr,
79  const typet &element_type,
80  const source_locationt &location);
81 
82 public:
84  std::vector<const symbolt *> &_symbols_created,
85  const source_locationt &loc,
86  const object_factory_parameterst _object_factory_parameters,
87  symbol_table_baset &_symbol_table,
89  : symbols_created(_symbols_created),
90  loc(loc),
91  object_factory_parameters(_object_factory_parameters),
92  symbol_table(_symbol_table),
93  ns(_symbol_table),
95  {}
96 
98  code_blockt &assignments,
99  const exprt &,
100  const typet &,
101  allocation_typet alloc_type);
102 
104  code_blockt &assignments,
105  const exprt &expr,
106  size_t depth,
108  const source_locationt &location);
109 
110  void gen_nondet_init(
111  code_blockt &assignments,
112  const exprt &expr,
113  bool is_sub,
114  irep_idt class_identifier,
115  bool skip_classid,
116  allocation_typet alloc_type,
117  bool override_,
118  const typet &override_type,
119  size_t depth,
121  const source_locationt &location);
122 
123 private:
125  code_blockt &assignments,
126  const exprt &expr,
127  allocation_typet alloc_type,
129  size_t depth,
130  const update_in_placet &update_in_place,
131  const source_locationt &location);
132 
134  code_blockt &assignments,
135  const exprt &expr,
136  bool is_sub,
137  irep_idt class_identifier,
138  bool skip_classid,
139  allocation_typet alloc_type,
140  const struct_typet &struct_type,
141  size_t depth,
142  const update_in_placet &update_in_place,
143  const source_locationt &location);
144 
146  code_blockt &assignments,
147  allocation_typet alloc_type,
148  const pointer_typet &substitute_pointer_type,
149  size_t depth,
150  const source_locationt &location);
151 };
152 
167  const exprt &target_expr,
168  const typet &allocate_type,
169  symbol_table_baset &symbol_table,
170  const source_locationt &loc,
171  const irep_idt &function_id,
172  code_blockt &output_code,
173  std::vector<const symbolt *> &symbols_created,
174  bool cast_needed)
175 {
176  // build size expression
177  exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table));
178 
179  if(allocate_type.id()!=ID_empty)
180  {
181  INVARIANT(!object_size.is_nil(), "Size of Java objects should be known");
182  // malloc expression
183  side_effect_exprt malloc_expr(
184  ID_allocate, pointer_type(allocate_type), loc);
185  malloc_expr.copy_to_operands(object_size);
186  malloc_expr.copy_to_operands(false_exprt());
187  // create a symbol for the malloc expression so we can initialize
188  // without having to do it potentially through a double-deref, which
189  // breaks the to-SSA phase.
190  symbolt &malloc_sym = get_fresh_aux_symbol(
191  pointer_type(allocate_type),
192  id2string(function_id),
193  "malloc_site",
194  loc,
195  ID_java,
196  symbol_table);
197  symbols_created.push_back(&malloc_sym);
198  code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
199  assign.add_source_location()=loc;
200  output_code.copy_to_operands(assign);
201  exprt malloc_symbol_expr=malloc_sym.symbol_expr();
202  if(cast_needed)
203  malloc_symbol_expr=typecast_exprt(malloc_symbol_expr, target_expr.type());
204  code_assignt code(target_expr, malloc_symbol_expr);
205  code.add_source_location()=loc;
206  output_code.copy_to_operands(code);
207  return malloc_sym.symbol_expr();
208  }
209  else
210  {
211  // make null
212  null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type()));
213  code_assignt code(target_expr, null_pointer_expr);
214  code.add_source_location()=loc;
215  output_code.copy_to_operands(code);
216  return exprt();
217  }
218 }
219 
230  const exprt &target_expr,
231  symbol_table_baset &symbol_table,
232  const source_locationt &loc,
233  const irep_idt &function_id,
234  code_blockt &output_code)
235 {
236  std::vector<const symbolt *> symbols_created;
237  code_blockt tmp_block;
238  const typet &allocate_type=target_expr.type().subtype();
240  target_expr,
241  allocate_type,
242  symbol_table,
243  loc,
244  function_id,
245  tmp_block,
246  symbols_created,
247  false);
248 
249  // Add the following code to output_code for each symbol that's been created:
250  // <type> <identifier>;
251  for(const symbolt * const symbol_ptr : symbols_created)
252  {
253  code_declt decl(symbol_ptr->symbol_expr());
254  decl.add_source_location()=loc;
255  output_code.add(decl);
256  }
257 
258  for(const exprt &code : tmp_block.operands())
259  output_code.add(to_code(code));
260  return dynamic_object;
261 }
262 
275  code_blockt &assignments,
276  const exprt &target_expr,
277  const typet &allocate_type,
278  allocation_typet alloc_type)
279 {
280  const typet &allocate_type_resolved=ns.follow(allocate_type);
281  const typet &target_type=ns.follow(target_expr.type().subtype());
282  bool cast_needed=allocate_type_resolved!=target_type;
283  switch(alloc_type)
284  {
287  {
288  symbolt &aux_symbol = get_fresh_aux_symbol(
289  allocate_type,
291  "tmp_object_factory",
292  loc,
293  ID_java,
294  symbol_table);
295  if(alloc_type==allocation_typet::GLOBAL)
296  aux_symbol.is_static_lifetime=true;
297  symbols_created.push_back(&aux_symbol);
298 
299  exprt object=aux_symbol.symbol_expr();
300  exprt aoe=address_of_exprt(object);
301  if(cast_needed)
302  aoe=typecast_exprt(aoe, target_expr.type());
303  code_assignt code(target_expr, aoe);
304  code.add_source_location()=loc;
305  assignments.copy_to_operands(code);
306  return aoe;
307  }
309  {
311  target_expr,
312  allocate_type,
313  symbol_table,
314  loc,
316  assignments,
318  cast_needed);
319  }
320  default:
321  UNREACHABLE;
322  return exprt();
323  } // End switch
324 }
325 
328  const exprt &expr,
329  const pointer_typet &ptr_type)
330 {
331  null_pointer_exprt null_pointer_expr(ptr_type);
332  code_assignt code(expr, null_pointer_expr);
333  code.add_source_location()=loc;
334  return code;
335 }
336 
377  code_blockt &assignments,
378  const exprt &expr,
379  const typet &target_type,
380  allocation_typet alloc_type,
381  size_t depth,
382  update_in_placet update_in_place,
383  const source_locationt &location)
384 {
385  PRECONDITION(expr.type().id()==ID_pointer);
387 
388  if(target_type.id()==ID_struct &&
389  has_prefix(
390  id2string(to_struct_type(target_type).get_tag()),
391  "java::array["))
392  {
394  assignments, expr, depth + 1, update_in_place, location);
395  }
396  else
397  {
398  // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
399  // initialize the fields of the object pointed by `expr`; if in
400  // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
401  // (return value of `allocate_object`), emit a statement of the form
402  // `<expr> := address-of(<new-object>)` and recursively initialize such new
403  // object.
404  exprt target;
405  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
406  {
407  target=allocate_object(
408  assignments,
409  expr,
410  target_type,
411  alloc_type);
412  INVARIANT(
413  target.type().id()==ID_pointer,
414  "Pointer-typed expression expected");
415  }
416  else
417  {
418  target=expr;
419  }
420 
421  // we dereference the pointer and initialize the resulting object using a
422  // recursive call
423  exprt init_expr;
424  if(target.id()==ID_address_of)
425  init_expr=target.op0();
426  else
427  {
428  init_expr=
429  dereference_exprt(target, target.type().subtype());
430  }
432  assignments,
433  init_expr,
434  false, // is_sub
435  "", // class_identifier
436  false, // skip_classid
437  alloc_type,
438  false,
439  typet(),
440  depth + 1,
441  update_in_place,
442  location);
443  }
444 }
445 
450 {
452  std::unordered_set<irep_idt> &recursion_set;
455 
456 public:
460  explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
461  : recursion_set(_recursion_set)
462  { }
463 
466  {
467  if(erase_entry!=irep_idt())
468  recursion_set.erase(erase_entry);
469  }
470 
473 
478  bool insert_entry(const irep_idt &entry)
479  {
480  INVARIANT(
482  "insert_entry should only be called once");
483  INVARIANT(entry!=irep_idt(), "entry should be a struct tag");
484  bool ret=recursion_set.insert(entry).second;
485  if(ret)
486  {
487  // We added something, so erase it when this is destroyed:
488  erase_entry=entry;
489  }
490  return ret;
491  }
492 };
493 
498 static mp_integer max_value(const typet &type)
499 {
500  if(type.id() == ID_signedbv)
501  return to_signedbv_type(type).largest();
502  else if(type.id() == ID_unsignedbv)
503  return to_unsignedbv_type(type).largest();
504  UNREACHABLE;
505 }
506 
511 static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
512 {
513  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
514  alloc.copy_to_operands(size);
515  alloc.copy_to_operands(false_exprt());
516  return code_assignt(lhs, alloc);
517 }
518 
557  struct_exprt &struct_expr,
558  code_blockt &code,
559  const std::size_t &max_nondet_string_length,
560  const source_locationt &loc,
561  const irep_idt &function_id,
562  symbol_table_baset &symbol_table,
563  bool printable)
564 {
566  struct_expr.type()))
567  {
568  return false;
569  }
570 
571  namespacet ns(symbol_table);
572 
573  const struct_typet &struct_type =
574  to_struct_type(ns.follow(struct_expr.type()));
575 
576  // In case the type for String was not added to the symbol table,
577  // (typically when string refinement is not activated), `struct_type`
578  // just contains the standard Object fields (or may have some other model
579  // entirely), and in particular has no length and data fields.
580  if(!struct_type.has_component("length") || !struct_type.has_component("data"))
581  return false;
582 
583  // We allow type StringBuffer and StringBuilder to be initialized
584  // in the same way has String, because they have the same structure and
585  // are treated in the same way by CBMC.
586 
587  // Note that CharSequence cannot be used as classid because it's abstract,
588  // so it is replaced by String.
589  // \todo allow StringBuffer and StringBuilder as classid for Charsequence
590  if(struct_type.get_tag() == "java.lang.CharSequence")
591  {
593  struct_expr, ns, symbol_typet("java::java.lang.String"));
594  }
595 
596  // OK, this is a String type with the expected fields -- add code to `code`
597  // to set up pre-requisite variables and assign them in `struct_expr`.
598 
600  // length_expr = nondet(int);
601  const symbolt length_sym = get_fresh_aux_symbol(
602  java_int_type(),
603  id2string(function_id),
604  "tmp_object_factory",
605  loc,
606  ID_java,
607  symbol_table);
608  const symbol_exprt length_expr = length_sym.symbol_expr();
609  const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
610  code.add(code_declt(length_expr));
611  code.add(code_assignt(length_expr, nondet_length));
612 
613  // assume (length_expr >= 0);
614  code.add(
615  code_assumet(
617  length_expr, ID_ge, from_integer(0, java_int_type()))));
618 
619  // assume (length_expr <= max_input_length)
620  if(max_nondet_string_length <= max_value(length_expr.type()))
621  {
622  exprt max_length =
623  from_integer(max_nondet_string_length, length_expr.type());
624  code.add(
625  code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
626  }
627 
628  // char (*array_data_init)[INFINITY];
629  const typet data_ptr_type = pointer_type(
631 
632  symbolt &data_pointer_sym = get_fresh_aux_symbol(
633  data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table);
634  const auto data_pointer = data_pointer_sym.symbol_expr();
635  code.add(code_declt(data_pointer));
636 
637  // Dynamic allocation: `data array = allocate char[INFINITY]`
638  code.add(make_allocate_code(data_pointer, infinity_exprt(java_int_type())));
639 
640  // `data_expr` is `*data_pointer`
641  // data_expr = nondet(char[INFINITY]) // we use infinity for variable size
642  const dereference_exprt data_expr(data_pointer);
643  const exprt nondet_array =
644  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
645  code.add(code_assignt(data_expr, nondet_array));
646 
647  struct_expr.operands()[struct_type.component_number("length")] = length_expr;
648 
649  const address_of_exprt array_pointer(
650  index_exprt(data_expr, from_integer(0, java_int_type())));
651 
653  array_pointer, data_expr, symbol_table, loc, code);
654 
656  data_expr, length_expr, symbol_table, loc, code);
657 
658  struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
659 
660  // Printable ASCII characters are between ' ' and '~'.
661  if(printable)
662  {
664  array_pointer, length_expr, " -~", symbol_table, loc, code);
665  }
666 
667  return true;
668 }
669 
692  code_blockt &assignments,
693  const exprt &expr,
694  allocation_typet alloc_type,
696  size_t depth,
697  const update_in_placet &update_in_place,
698  const source_locationt &location)
699 {
700  PRECONDITION(expr.type().id()==ID_pointer);
701  const pointer_typet &replacement_pointer_type =
704 
705  // If we are changing the pointer, we generate code for creating a pointer
706  // to the substituted type instead
707  // TODO if we are comparing array types we need to compare their element
708  // types. this is for now done by implementing equality function especially
709  // for java types, technical debt TG-2707
710  if(!equal_java_types(replacement_pointer_type, pointer_type))
711  {
712  // update generic_parameter_specialization_map for the new pointer
714  generic_parameter_specialization_map_keys(
716  generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
717  replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
718 
719  const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
720  assignments, alloc_type, replacement_pointer_type, depth, location);
721 
722  // Having created a pointer to object of type replacement_pointer_type
723  // we now assign it back to the original pointer with a cast
724  // from pointer_type to replacement_pointer_type
725  assignments.add(
726  code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
727  return;
728  }
729 
730  // This deletes the recursion set entry on leaving this function scope,
731  // if one is set below.
732  recursion_set_entryt recursion_set_entry(recursion_set);
733 
734  // If the pointed value is struct-typed, then we need to prevent the
735  // possibility of this code to loop infinitely when initializing a data
736  // structure with recursive types or unbounded depth. We implement two
737  // mechanisms here. We keep a set of 'types seen', and detect when we perform
738  // a 2nd visit to the same type. We also detect the depth in the chain of
739  // (recursive) calls to the methods of this class. The depth counter is
740  // incremented only when a pointer is deferenced, including pointers to
741  // arrays.
742  //
743  // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
744  // the pointer to NULL instead of recursively initializing the struct to which
745  // it points.
746  const typet &subtype=ns.follow(pointer_type.subtype());
747  if(subtype.id()==ID_struct)
748  {
749  const struct_typet &struct_type=to_struct_type(subtype);
750  const irep_idt &struct_tag=struct_type.get_tag();
751 
752  // If this is a recursive type of some kind AND the depth is exceeded, set
753  // the pointer to null.
754  if(!recursion_set_entry.insert_entry(struct_tag) &&
756  {
757  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
758  {
759  assignments.copy_to_operands(
761  }
762  // Otherwise leave it as it is.
763  return;
764  }
765  }
766 
767  code_blockt new_object_assignments;
768  code_blockt update_in_place_assignments;
769 
770  // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
771  // emit to `update_in_place_assignments` code for in-place initialization of
772  // the object pointed by `expr`, assuming that such object is of type
773  // `subtype`
774  if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
775  {
777  update_in_place_assignments,
778  expr,
779  subtype,
780  alloc_type,
781  depth,
783  location);
784  }
785 
786  // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
787  // above to `assignments` and return
788  if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
789  {
790  assignments.append(update_in_place_assignments);
791  return;
792  }
793 
794  // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
795  // vector of assignments that create a new object (recursively initializes it)
796  // and asign to `expr` the address of such object
797  code_blockt non_null_inst;
798 
800  non_null_inst,
801  expr,
802  subtype,
803  alloc_type,
804  depth,
806  location);
807 
808  auto set_null_inst=get_null_assignment(expr, pointer_type);
809 
810  const bool allow_null =
812 
813  // Alternatively, if this is a void* we *must* initialise with null:
814  // (This can currently happen for some cases of #exception_value)
815  bool must_be_null = subtype == empty_typet();
816 
817  if(must_be_null)
818  {
819  // Add the following code to assignments:
820  // <expr> = nullptr;
821  new_object_assignments.add(set_null_inst);
822  }
823  else if(!allow_null)
824  {
825  // Add the following code to assignments:
826  // <expr> = <aoe>;
827  new_object_assignments.append(non_null_inst);
828  }
829  else
830  {
831  // if(NONDET(_Bool)
832  // {
833  // <expr> = <null pointer>
834  // }
835  // else
836  // {
837  // <code from recursive call to gen_nondet_init() with
838  // tmp$<temporary_counter>>
839  // }
840  code_ifthenelset null_check;
841  null_check.cond() = side_effect_expr_nondett(bool_typet(), location);
842  null_check.then_case()=set_null_inst;
843  null_check.else_case()=non_null_inst;
844 
845  new_object_assignments.add(null_check);
846  }
847 
848  // Similarly to above, maybe use a conditional if both the
849  // allocate-fresh and update-in-place cases are allowed:
850  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
851  {
852  assignments.append(new_object_assignments);
853  }
854  else
855  {
857  "No-update and must-update should have already been resolved");
858 
859  code_ifthenelset update_check;
860  update_check.cond() =
862  update_check.then_case()=update_in_place_assignments;
863  update_check.else_case()=new_object_assignments;
864 
865  assignments.add(update_check);
866  }
867 }
868 
894  code_blockt &assignments,
895  allocation_typet alloc_type,
896  const pointer_typet &replacement_pointer,
897  size_t depth,
898  const source_locationt &location)
899 {
900  symbolt new_symbol = get_fresh_aux_symbol(
901  replacement_pointer,
903  "tmp_object_factory",
904  loc,
905  ID_java,
906  symbol_table);
907 
908  // Generate a new object into this new symbol
910  assignments,
911  new_symbol.symbol_expr(),
912  false, // is_sub
913  "", // class_identifier
914  false, // skip_classid
915  alloc_type,
916  false, // override
917  typet(), // override_type
918  depth,
920  location);
921 
922  return new_symbol.symbol_expr();
923 }
924 
955  code_blockt &assignments,
956  const exprt &expr,
957  bool is_sub,
958  irep_idt class_identifier,
959  bool skip_classid,
960  allocation_typet alloc_type,
961  const struct_typet &struct_type,
962  size_t depth,
963  const update_in_placet &update_in_place,
964  const source_locationt &location)
965 {
966  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
967  PRECONDITION(struct_type.id()==ID_struct);
968 
969  typedef struct_typet::componentst componentst;
970  const irep_idt &struct_tag=struct_type.get_tag();
971 
972  const componentst &components=struct_type.components();
973 
974  // Should we write the whole object?
975  // * Not if this is a sub-structure (a superclass object), as our caller will
976  // have done this already
977  // * Not if the object has already been initialised by our caller, in whic
978  // case they will set `skip_classid`
979  // * Not if we're re-initializing an existing object (i.e. update_in_place)
980 
981  bool skip_special_string_fields = false;
982 
983  if(!is_sub &&
984  !skip_classid &&
985  update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
986  {
987  class_identifier = struct_tag;
988 
989  // Add an initial all-zero write. Most of the fields of this will be
990  // overwritten, but it helps to have a whole-structure write that analysis
991  // passes can easily recognise leaves no uninitialised state behind.
992 
993  // This code mirrors the `remove_java_new` pass:
994  null_message_handlert nullout;
995  exprt initial_object =
997  struct_type, source_locationt(), ns, nullout);
998  irep_idt qualified_clsid = "java::" + id2string(class_identifier);
1000  to_struct_expr(initial_object), ns, symbol_typet(qualified_clsid));
1001 
1002  // If the initialised type is a special-cased String type (one with length
1003  // and data fields introduced by string-library preprocessing), initialise
1004  // those fields with nondet values:
1005  skip_special_string_fields =
1007  to_struct_expr(initial_object),
1008  assignments,
1010  loc,
1012  symbol_table,
1014 
1015  assignments.copy_to_operands(
1016  code_assignt(expr, initial_object));
1017  }
1018 
1019  for(const auto &component : components)
1020  {
1021  const typet &component_type=component.type();
1022  irep_idt name=component.get_name();
1023 
1024  member_exprt me(expr, name, component_type);
1025 
1026  if(name=="@class_identifier")
1027  {
1028  continue;
1029  }
1030  else if(name == "cproverMonitorCount")
1031  {
1032  // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
1033  // nondet. This field is only present when the java core models are
1034  // included in the class-path. It is used to implement a critical section,
1035  // which is necessary to support concurrency.
1036  if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
1037  continue;
1038  code_assignt code(me, from_integer(0, me.type()));
1039  code.add_source_location() = loc;
1040  assignments.copy_to_operands(code);
1041  }
1042  else if(skip_special_string_fields && (name == "length" || name == "data"))
1043  {
1044  // In this case these were set up by initialise_nondet_string_fields
1045  // above.
1046  continue;
1047  }
1048  else
1049  {
1050  INVARIANT(!name.empty(), "Each component of a struct must have a name");
1051 
1052  bool _is_sub=name[0]=='@';
1053 
1054  // MUST_UPDATE_IN_PLACE only applies to this object.
1055  // If this is a pointer to another object, offer the chance
1056  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1057  update_in_placet substruct_in_place=
1058  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE && !_is_sub ?
1060  update_in_place;
1062  assignments,
1063  me,
1064  _is_sub,
1065  class_identifier,
1066  false, // skip_classid
1067  alloc_type,
1068  false, // override
1069  typet(), // override_type
1070  depth,
1071  substruct_in_place,
1072  location);
1073  }
1074  }
1075 
1076  // If <class_identifier>.cproverNondetInitialize() can be found in the
1077  // symbol table, we add a call:
1078  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1079  // expr.cproverNondetInitialize();
1080  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1081 
1082  const irep_idt init_method_name =
1083  "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V";
1084 
1085  if(const auto func = symbol_table.lookup(init_method_name))
1086  {
1087  const java_method_typet &type = to_java_method_type(func->type);
1088  code_function_callt fun_call;
1089  fun_call.function() = func->symbol_expr();
1090  if(type.has_this())
1091  fun_call.arguments().push_back(address_of_exprt(expr));
1092 
1093  assignments.add(fun_call);
1094  }
1095 }
1096 
1131  code_blockt &assignments,
1132  const exprt &expr,
1133  bool is_sub,
1134  irep_idt class_identifier,
1135  bool skip_classid,
1136  allocation_typet alloc_type,
1137  bool override_,
1138  const typet &override_type,
1139  size_t depth,
1140  update_in_placet update_in_place,
1141  const source_locationt &location)
1142 {
1143  const typet &type=
1144  override_ ? ns.follow(override_type) : ns.follow(expr.type());
1145 
1146 
1147  if(type.id()==ID_pointer)
1148  {
1149  // dereferenced type
1151 
1152  // If we are about to initialize a generic pointer type, add its concrete
1153  // types to the map and delete them on leaving this function scope.
1155  generic_parameter_specialization_map_keys(
1157  generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
1159 
1161  assignments,
1162  expr,
1163  alloc_type,
1164  pointer_type,
1165  depth,
1166  update_in_place,
1167  location);
1168  }
1169  else if(type.id()==ID_struct)
1170  {
1171  const struct_typet struct_type=to_struct_type(type);
1172 
1173  // If we are about to initialize a generic class (as a superclass object
1174  // for a different object), add its concrete types to the map and delete
1175  // them on leaving this function scope.
1177  generic_parameter_specialization_map_keys(
1179  if(is_sub)
1180  {
1181  const typet &symbol = override_ ? override_type : expr.type();
1182  PRECONDITION(symbol.id() == ID_symbol);
1183  generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
1184  to_symbol_type(symbol), struct_type);
1185  }
1186 
1188  assignments,
1189  expr,
1190  is_sub,
1191  class_identifier,
1192  skip_classid,
1193  alloc_type,
1194  struct_type,
1195  depth,
1196  update_in_place,
1197  location);
1198  }
1199  else
1200  {
1201  // types different from pointer or structure:
1202  // bool, int, float, byte, char, ...
1203  exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type)
1204  : side_effect_expr_nondett(type, loc);
1205  code_assignt assign(expr, rhs);
1206  assign.add_source_location()=loc;
1207 
1208  assignments.copy_to_operands(assign);
1209  }
1210 }
1211 
1226  code_blockt &assignments,
1227  const exprt &lhs,
1228  const exprt &max_length_expr,
1229  const typet &element_type,
1230  const source_locationt &location)
1231 {
1232  symbolt &length_sym = get_fresh_aux_symbol(
1233  java_int_type(),
1235  "nondet_array_length",
1236  loc,
1237  ID_java,
1238  symbol_table);
1239  symbols_created.push_back(&length_sym);
1240  const auto &length_sym_expr=length_sym.symbol_expr();
1241 
1242  // Initialize array with some undetermined length:
1244  assignments,
1245  length_sym_expr,
1246  false, // is_sub
1247  irep_idt(),
1248  false, // skip_classid
1249  allocation_typet::LOCAL, // immaterial, type is primitive
1250  false, // override
1251  typet(), // override type is immaterial
1252  0, // depth is immaterial, always non-null
1254  location);
1255 
1256  // Insert assumptions to bound its length:
1258  assume1(length_sym_expr, ID_ge, from_integer(0, java_int_type()));
1260  assume2(length_sym_expr, ID_le, max_length_expr);
1261  code_assumet assume_inst1(assume1);
1262  code_assumet assume_inst2(assume2);
1263  assignments.move_to_operands(assume_inst1);
1264  assignments.move_to_operands(assume_inst2);
1265 
1266  side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), loc);
1267  java_new_array.copy_to_operands(length_sym_expr);
1268  java_new_array.set(ID_length_upper_bound, max_length_expr);
1269  java_new_array.type().subtype().set(ID_element_type, element_type);
1270  code_assignt assign(lhs, java_new_array);
1271  assign.add_source_location()=loc;
1272  assignments.copy_to_operands(assign);
1273 }
1274 
1282  code_blockt &assignments,
1283  const exprt &expr,
1284  size_t depth,
1285  update_in_placet update_in_place,
1286  const source_locationt &location)
1287 {
1288  PRECONDITION(expr.type().id()==ID_pointer);
1289  PRECONDITION(expr.type().subtype().id()==ID_symbol);
1291 
1292  const typet &type=ns.follow(expr.type().subtype());
1293  const struct_typet &struct_type=to_struct_type(type);
1294  const typet &element_type =
1295  static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
1296 
1297  auto max_length_expr=from_integer(
1299 
1300  // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1301  // initialize its elements
1302  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
1303  {
1305  assignments, expr, max_length_expr, element_type, location);
1306  }
1307 
1308  // Otherwise we're updating the array in place, and use the
1309  // existing array allocation and length.
1310 
1311  INVARIANT(
1312  is_valid_java_array(struct_type),
1313  "Java struct array does not conform to expectations");
1314 
1315  dereference_exprt deref_expr(expr, expr.type().subtype());
1316  const auto &comps=struct_type.components();
1317  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1318  exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type());
1319 
1320  if(init_array_expr.type()!=pointer_type(element_type))
1321  init_array_expr=
1322  typecast_exprt(init_array_expr, pointer_type(element_type));
1323 
1324  // Interpose a new symbol, as the goto-symex stage can't handle array indexing
1325  // via a cast.
1326  symbolt &array_init_symbol = get_fresh_aux_symbol(
1327  init_array_expr.type(),
1329  "array_data_init",
1330  loc,
1331  ID_java,
1332  symbol_table);
1333  symbols_created.push_back(&array_init_symbol);
1334  const auto &array_init_symexpr=array_init_symbol.symbol_expr();
1335  codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
1336  data_assign.add_source_location()=loc;
1337  assignments.copy_to_operands(data_assign);
1338 
1339  // Emit init loop for(array_init_iter=0; array_init_iter!=array.length;
1340  // ++array_init_iter) init(array[array_init_iter]);
1341  symbolt &counter = get_fresh_aux_symbol(
1342  length_expr.type(),
1344  "array_init_iter",
1345  loc,
1346  ID_java,
1347  symbol_table);
1348  symbols_created.push_back(&counter);
1349  exprt counter_expr=counter.symbol_expr();
1350 
1351  exprt java_zero=from_integer(0, java_int_type());
1352  assignments.copy_to_operands(code_assignt(counter_expr, java_zero));
1353 
1354  std::string head_name = id2string(counter.base_name) + "_header";
1355  code_labelt init_head_label(head_name, code_skipt());
1356  code_gotot goto_head(head_name);
1357 
1358  assignments.move_to_operands(init_head_label);
1359 
1360  std::string done_name = id2string(counter.base_name) + "_done";
1361  code_labelt init_done_label(done_name, code_skipt());
1362  code_gotot goto_done(done_name);
1363 
1364  code_ifthenelset done_test;
1365  done_test.cond()=equal_exprt(counter_expr, length_expr);
1366  done_test.then_case()=goto_done;
1367 
1368  assignments.move_to_operands(done_test);
1369 
1370  if(update_in_place!=update_in_placet::MUST_UPDATE_IN_PLACE)
1371  {
1372  // Add a redundant if(counter == max_length) break
1373  // that is easier for the unwinder to understand.
1374  code_ifthenelset max_test;
1375  max_test.cond()=equal_exprt(counter_expr, max_length_expr);
1376  max_test.then_case()=goto_done;
1377 
1378  assignments.move_to_operands(max_test);
1379  }
1380 
1381  const dereference_exprt arraycellref(
1382  plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()),
1383  array_init_symexpr.type().subtype());
1384 
1385  // MUST_UPDATE_IN_PLACE only applies to this object.
1386  // If this is a pointer to another object, offer the chance
1387  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1388  update_in_placet child_update_in_place=
1389  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE ?
1391  update_in_place;
1393  assignments,
1394  arraycellref,
1395  false, // is_sub
1396  irep_idt(), // class_identifier
1397  false, // skip_classid
1398  // These are variable in number, so use dynamic allocator:
1400  true, // override
1401  element_type,
1402  depth,
1403  child_update_in_place,
1404  location);
1405 
1406  exprt java_one=from_integer(1, java_int_type());
1407  code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
1408 
1409  assignments.move_to_operands(incr);
1410  assignments.move_to_operands(goto_head);
1411  assignments.move_to_operands(init_done_label);
1412 }
1413 
1420  const std::vector<const symbolt *> &symbols_created,
1421  const source_locationt &loc,
1422  code_blockt &init_code)
1423 {
1424  // Add the following code to init_code for each symbol that's been created:
1425  // <type> <identifier>;
1426  for(const symbolt * const symbol_ptr : symbols_created)
1427  {
1428  if(!symbol_ptr->is_static_lifetime)
1429  {
1430  code_declt decl(symbol_ptr->symbol_expr());
1431  decl.add_source_location()=loc;
1432  init_code.add(decl);
1433  }
1434  }
1435 }
1436 
1449  const typet &type,
1450  const irep_idt base_name,
1451  code_blockt &init_code,
1452  symbol_table_baset &symbol_table,
1453  object_factory_parameterst parameters,
1454  allocation_typet alloc_type,
1455  const source_locationt &loc,
1456  const select_pointer_typet &pointer_type_selector)
1457 {
1459  "::"+id2string(base_name);
1460 
1461  auxiliary_symbolt main_symbol;
1462  main_symbol.mode=ID_java;
1463  main_symbol.is_static_lifetime=false;
1464  main_symbol.name=identifier;
1465  main_symbol.base_name=base_name;
1466  main_symbol.type=type;
1467  main_symbol.location=loc;
1469 
1470  exprt object=main_symbol.symbol_expr();
1471 
1472  symbolt *main_symbol_ptr;
1473  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
1474  CHECK_RETURN(!moving_symbol_failed);
1475 
1476  std::vector<const symbolt *> symbols_created;
1477  symbols_created.push_back(main_symbol_ptr);
1478  java_object_factoryt state(
1479  symbols_created,
1480  loc,
1481  parameters,
1482  symbol_table,
1483  pointer_type_selector);
1484  code_blockt assignments;
1485  state.gen_nondet_init(
1486  assignments,
1487  object,
1488  false, // is_sub
1489  "", // class_identifier
1490  false, // skip_classid
1491  alloc_type,
1492  false, // override
1493  typet(), // override_type is immaterial
1494  1, // initial depth
1496  loc);
1497 
1498  declare_created_symbols(symbols_created, loc, init_code);
1499 
1500  init_code.append(assignments);
1501  return object;
1502 }
1503 
1540  const exprt &expr,
1541  code_blockt &init_code,
1542  symbol_table_baset &symbol_table,
1543  const source_locationt &loc,
1544  bool skip_classid,
1545  allocation_typet alloc_type,
1546  const object_factory_parameterst &object_factory_parameters,
1547  const select_pointer_typet &pointer_type_selector,
1548  update_in_placet update_in_place)
1549 {
1550  std::vector<const symbolt *> symbols_created;
1551 
1552  java_object_factoryt state(
1553  symbols_created,
1554  loc,
1555  object_factory_parameters,
1556  symbol_table,
1557  pointer_type_selector);
1558  code_blockt assignments;
1559  state.gen_nondet_init(
1560  assignments,
1561  expr,
1562  false, // is_sub
1563  "", // class_identifier
1564  skip_classid,
1565  alloc_type,
1566  false, // override
1567  typet(), // override_type is immaterial
1568  1, // initial depth
1569  update_in_place,
1570  loc);
1571 
1572  declare_created_symbols(symbols_created, loc, init_code);
1573 
1574  init_code.append(assignments);
1575 }
1576 
1579  const typet &type,
1580  const irep_idt base_name,
1581  code_blockt &init_code,
1582  symbol_tablet &symbol_table,
1583  const object_factory_parameterst &object_factory_parameters,
1584  allocation_typet alloc_type,
1585  const source_locationt &location)
1586 {
1587  select_pointer_typet pointer_type_selector;
1588  return object_factory(
1589  type,
1590  base_name,
1591  init_code,
1592  symbol_table,
1593  object_factory_parameters,
1594  alloc_type,
1595  location,
1596  pointer_type_selector);
1597 }
1598 
1601  const exprt &expr,
1602  code_blockt &init_code,
1603  symbol_table_baset &symbol_table,
1604  const source_locationt &loc,
1605  bool skip_classid,
1606  allocation_typet alloc_type,
1607  const object_factory_parameterst &object_factory_parameters,
1608  update_in_placet update_in_place)
1609 {
1610  select_pointer_typet pointer_type_selector;
1612  expr,
1613  init_code,
1614  symbol_table,
1615  loc,
1616  skip_classid,
1617  alloc_type,
1618  object_factory_parameters,
1619  pointer_type_selector,
1620  update_in_place);
1621 }
#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.
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, const source_locationt &location)
Initializes the pointer-typed lvalue expression expr to point to an object of type target_type...
exprt size_of_expr(const typet &type, const namespacet &ns)
const codet & then_case() const
Definition: std_code.h:486
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, const source_locationt &location)
Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializ...
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)...
bool is_nil() const
Definition: irep.h:172
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:44
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:1296
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:476
irep_idt get_tag(const typet &type)
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:4518
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:803
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:266
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:738
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:204
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:3869
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:775
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.
bool initialize_nondet_string_fields(struct_exprt &struct_expr, code_blockt &code, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
Check if a structure is a nondeterministic String structure, and if it is initialize its length and d...
Expression Initialization.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:259
An expression denoting infinity.
Definition: std_expr.h:4692
void add(const codet &code)
Definition: std_code.h:112
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:890
A reference into the symbol table.
Definition: std_types.h:110
size_t max_nondet_tree_depth
Maximum depth for object hierarchy on input.
A declaration of a local variable.
Definition: std_code.h:254
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:1435
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:3282
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:977
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:100
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
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:858
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
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1838
The boolean constant false.
Definition: std_expr.h:4497
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)
Pointer Logic.
void gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, allocation_typet alloc_type, 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...
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:1254
An assumption, which must hold in subsequent code.
Definition: std_code.h:357
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
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:289
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...
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:878
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.
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
bool has_this() const
Definition: std_types.h:866
symbol_exprt gen_nondet_subtype_pointer_init(code_blockt &assignments, allocation_typet alloc_type, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location)
Generate codet assignments to initalize the selected concrete type.
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 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, const source_locationt &location)
Initializes a primitive-typed or referece-typed object tree rooted at expr, allocating child objects ...
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:271
static mp_integer max_value(const typet &type)
Get max value for an integer type.
void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type, const source_locationt &location)
Allocates a fresh array and emits an assignment writing to lhs the address of the new array...
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:89
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
arrays with given size
Definition: std_types.h:1013
Skip.
Definition: std_code.h:179
An if-then-else.
Definition: std_code.h:466
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:1459
dstringt irep_idt
Definition: irep.h:32
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.
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
irep_idt get_tag() const
Definition: std_types.h:266
An expression containing a side effect.
Definition: std_code.h:1271
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:496
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:73
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:196
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...
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr, size_t depth, update_in_placet, const source_locationt &location)
Create code to initialize a Java array whose size will be at most max_nondet_array_length.
array index operator
Definition: std_expr.h:1462