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>
14 #include <util/nondet.h>
16 
19 
21 #include "java_root_class.h"
22 #include "java_string_literals.h"
23 
25 {
29  std::vector<const symbolt *> &symbols_created;
30 
34 
36 
41  std::unordered_set<irep_idt> recursion_set;
42 
52 
55 
58 
63 
65  const exprt &expr,
66  const pointer_typet &ptr_type);
67 
69  code_blockt &assignments,
70  const exprt &expr,
71  const typet &target_type,
72  allocation_typet alloc_type,
73  size_t depth,
74  update_in_placet update_in_place,
75  const source_locationt &location);
76 
78  code_blockt &assignments,
79  const exprt &lhs,
80  const exprt &max_length_expr,
81  const typet &element_type,
82  const source_locationt &location);
83 
84 public:
86  std::vector<const symbolt *> &_symbols_created,
87  const source_locationt &loc,
88  const java_object_factory_parameterst _object_factory_parameters,
89  symbol_table_baset &_symbol_table,
91  : symbols_created(_symbols_created),
92  loc(loc),
93  object_factory_parameters(_object_factory_parameters),
94  symbol_table(_symbol_table),
95  ns(_symbol_table),
97  {}
98 
100  code_blockt &assignments,
101  const exprt &,
102  const typet &,
103  allocation_typet alloc_type);
104 
106  code_blockt &assignments,
107  const exprt &expr,
108  size_t depth,
110  const source_locationt &location);
111 
113  code_blockt &assignments,
114  const exprt &expr,
115  const java_class_typet &java_class_type,
116  const source_locationt &location);
117 
118  void gen_nondet_init(
119  code_blockt &assignments,
120  const exprt &expr,
121  bool is_sub,
122  irep_idt class_identifier,
123  bool skip_classid,
124  allocation_typet alloc_type,
125  bool override_,
126  const typet &override_type,
127  size_t depth,
129  const source_locationt &location);
130 
131 private:
133  code_blockt &assignments,
134  const exprt &expr,
135  allocation_typet alloc_type,
137  size_t depth,
138  const update_in_placet &update_in_place,
139  const source_locationt &location);
140 
142  code_blockt &assignments,
143  const exprt &expr,
144  bool is_sub,
145  irep_idt class_identifier,
146  bool skip_classid,
147  allocation_typet alloc_type,
148  const struct_typet &struct_type,
149  size_t depth,
150  const update_in_placet &update_in_place,
151  const source_locationt &location);
152 
154  code_blockt &assignments,
155  allocation_typet alloc_type,
156  const pointer_typet &substitute_pointer_type,
157  size_t depth,
158  const source_locationt &location);
159 
161  code_blockt &assignments,
162  const std::string &basename_prefix,
163  const exprt &min_length_expr,
164  const exprt &max_length_expr,
165  const source_locationt &location);
166 
168  code_blockt &assignments,
169  const exprt &instance_expr,
170  const irep_idt &method_name);
171 };
172 
188  const exprt &target_expr,
189  const typet &allocate_type,
190  symbol_table_baset &symbol_table,
191  const source_locationt &loc,
192  const irep_idt &function_id,
193  code_blockt &output_code,
194  std::vector<const symbolt *> &symbols_created,
195  bool cast_needed)
196 {
197  // build size expression
198  exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table));
199 
200  if(allocate_type.id()!=ID_empty)
201  {
202  INVARIANT(!object_size.is_nil(), "Size of Java objects should be known");
203  // malloc expression
204  side_effect_exprt malloc_expr(
205  ID_allocate, pointer_type(allocate_type), loc);
206  malloc_expr.copy_to_operands(object_size);
207  malloc_expr.copy_to_operands(false_exprt());
208  // create a symbol for the malloc expression so we can initialize
209  // without having to do it potentially through a double-deref, which
210  // breaks the to-SSA phase.
211  symbolt &malloc_sym = get_fresh_aux_symbol(
212  pointer_type(allocate_type),
213  id2string(function_id),
214  "malloc_site",
215  loc,
216  ID_java,
217  symbol_table);
218  symbols_created.push_back(&malloc_sym);
219  code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
220  assign.add_source_location()=loc;
221  output_code.add(assign);
222  exprt malloc_symbol_expr=malloc_sym.symbol_expr();
223  if(cast_needed)
224  malloc_symbol_expr=typecast_exprt(malloc_symbol_expr, target_expr.type());
225  code_assignt code(target_expr, malloc_symbol_expr);
226  code.add_source_location()=loc;
227  output_code.add(code);
228  return malloc_sym.symbol_expr();
229  }
230  else
231  {
232  // make null
233  null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type()));
234  code_assignt code(target_expr, null_pointer_expr);
235  code.add_source_location()=loc;
236  output_code.add(code);
237  return exprt();
238  }
239 }
240 
252  const exprt &target_expr,
253  symbol_table_baset &symbol_table,
254  const source_locationt &loc,
255  const irep_idt &function_id,
256  code_blockt &output_code)
257 {
258  std::vector<const symbolt *> symbols_created;
259  code_blockt tmp_block;
260  const typet &allocate_type=target_expr.type().subtype();
262  target_expr,
263  allocate_type,
264  symbol_table,
265  loc,
266  function_id,
267  tmp_block,
268  symbols_created,
269  false);
270 
271  // Add the following code to output_code for each symbol that's been created:
272  // <type> <identifier>;
273  for(const symbolt * const symbol_ptr : symbols_created)
274  {
275  code_declt decl(symbol_ptr->symbol_expr());
276  decl.add_source_location()=loc;
277  output_code.add(decl);
278  }
279 
280  for(const auto &code : tmp_block.statements())
281  output_code.add(code);
282 
283  return dynamic_object;
284 }
285 
298  code_blockt &assignments,
299  const exprt &target_expr,
300  const typet &allocate_type,
301  allocation_typet alloc_type)
302 {
303  const typet &allocate_type_resolved=ns.follow(allocate_type);
304  const typet &target_type=ns.follow(target_expr.type().subtype());
305  bool cast_needed=allocate_type_resolved!=target_type;
306  switch(alloc_type)
307  {
310  {
311  symbolt &aux_symbol = get_fresh_aux_symbol(
312  allocate_type,
314  "tmp_object_factory",
315  loc,
316  ID_java,
317  symbol_table);
318  if(alloc_type==allocation_typet::GLOBAL)
319  aux_symbol.is_static_lifetime=true;
320  symbols_created.push_back(&aux_symbol);
321 
322  exprt object=aux_symbol.symbol_expr();
323  exprt aoe=address_of_exprt(object);
324  if(cast_needed)
325  aoe=typecast_exprt(aoe, target_expr.type());
326  code_assignt code(target_expr, aoe);
327  code.add_source_location()=loc;
328  assignments.add(code);
329  return aoe;
330  }
332  {
334  target_expr,
335  allocate_type,
336  symbol_table,
337  loc,
339  assignments,
341  cast_needed);
342  }
343  default:
344  UNREACHABLE;
345  return exprt();
346  } // End switch
347 }
348 
351  const exprt &expr,
352  const pointer_typet &ptr_type)
353 {
354  null_pointer_exprt null_pointer_expr(ptr_type);
355  code_assignt code(expr, null_pointer_expr);
356  code.add_source_location()=loc;
357  return code;
358 }
359 
402  code_blockt &assignments,
403  const exprt &expr,
404  const typet &target_type,
405  allocation_typet alloc_type,
406  size_t depth,
407  update_in_placet update_in_place,
408  const source_locationt &location)
409 {
410  PRECONDITION(expr.type().id() == ID_pointer);
412 
413  if(target_type.id() == ID_struct)
414  {
415  const auto &target_class_type = to_java_class_type(target_type);
416  if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
417  {
419  assignments, expr, depth + 1, update_in_place, location);
420  return;
421  }
422  if(target_class_type.get_base("java::java.lang.Enum"))
423  {
424  gen_nondet_enum_init(assignments, expr, target_class_type, location);
425  return;
426  }
427  }
428 
429  // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
430  // initialize the fields of the object pointed by `expr`; if in
431  // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
432  // (return value of `allocate_object`), emit a statement of the form
433  // `<expr> := address-of(<new-object>)` and recursively initialize such new
434  // object.
435  exprt target;
436  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
437  {
438  target = allocate_object(assignments, expr, target_type, alloc_type);
439  INVARIANT(
440  target.type().id() == ID_pointer, "Pointer-typed expression expected");
441  }
442  else
443  {
444  target = expr;
445  }
446 
447  // we dereference the pointer and initialize the resulting object using a
448  // recursive call
449  exprt init_expr;
450  if(target.id() == ID_address_of)
451  init_expr = target.op0();
452  else
453  {
454  init_expr = dereference_exprt(target, target.type().subtype());
455  }
457  assignments,
458  init_expr,
459  false, // is_sub
460  "", // class_identifier
461  false, // skip_classid
462  alloc_type,
463  false, // override
464  typet(), // override type immaterial
465  depth + 1,
466  update_in_place,
467  location);
468 }
469 
474 {
476  std::unordered_set<irep_idt> &recursion_set;
479 
480 public:
484  explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
485  : recursion_set(_recursion_set)
486  { }
487 
490  {
491  if(erase_entry!=irep_idt())
492  recursion_set.erase(erase_entry);
493  }
494 
497 
502  bool insert_entry(const irep_idt &entry)
503  {
504  INVARIANT(
506  "insert_entry should only be called once");
507  INVARIANT(entry!=irep_idt(), "entry should be a struct tag");
508  bool ret=recursion_set.insert(entry).second;
509  if(ret)
510  {
511  // We added something, so erase it when this is destroyed:
512  erase_entry=entry;
513  }
514  return ret;
515  }
516 };
517 
522 static mp_integer max_value(const typet &type)
523 {
524  if(type.id() == ID_signedbv)
525  return to_signedbv_type(type).largest();
526  else if(type.id() == ID_unsignedbv)
527  return to_unsignedbv_type(type).largest();
528  UNREACHABLE;
529 }
530 
569  struct_exprt &struct_expr,
570  code_blockt &code,
571  const std::size_t &min_nondet_string_length,
572  const std::size_t &max_nondet_string_length,
573  const source_locationt &loc,
574  const irep_idt &function_id,
575  symbol_table_baset &symbol_table,
576  bool printable)
577 {
578  PRECONDITION(
580  ::implements_java_char_sequence(struct_expr.type()));
581 
582  namespacet ns(symbol_table);
583 
584  const struct_typet &struct_type =
585  to_struct_type(ns.follow(struct_expr.type()));
586 
587  // In case the type for String was not added to the symbol table,
588  // (typically when string refinement is not activated), `struct_type`
589  // just contains the standard Object fields (or may have some other model
590  // entirely), and in particular has no length and data fields.
591  PRECONDITION(
592  struct_type.has_component("length") && struct_type.has_component("data"));
593 
594  // We allow type StringBuffer and StringBuilder to be initialized
595  // in the same way has String, because they have the same structure and
596  // are treated in the same way by CBMC.
597 
598  // Note that CharSequence cannot be used as classid because it's abstract,
599  // so it is replaced by String.
600  // \todo allow StringBuffer and StringBuilder as classid for Charsequence
601  if(struct_type.get_tag() == "java.lang.CharSequence")
602  {
604  struct_expr, ns, struct_tag_typet("java::java.lang.String"));
605  }
606 
607  // OK, this is a String type with the expected fields -- add code to `code`
608  // to set up pre-requisite variables and assign them in `struct_expr`.
609 
611  // length_expr = nondet(int);
612  const symbolt length_sym = get_fresh_aux_symbol(
613  java_int_type(),
614  id2string(function_id),
615  "tmp_object_factory",
616  loc,
617  ID_java,
618  symbol_table);
619  const symbol_exprt length_expr = length_sym.symbol_expr();
620  const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
621  code.add(code_declt(length_expr));
622  code.add(code_assignt(length_expr, nondet_length));
623 
624  // assume (length_expr >= min_nondet_string_length);
625  const exprt min_length =
626  from_integer(min_nondet_string_length, java_int_type());
627  code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
628 
629  // assume (length_expr <= max_input_length)
630  if(max_nondet_string_length <= max_value(length_expr.type()))
631  {
632  exprt max_length =
633  from_integer(max_nondet_string_length, length_expr.type());
634  code.add(
635  code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
636  }
637 
638  const exprt data_expr =
639  make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
640  struct_expr.operands()[struct_type.component_number("length")] = length_expr;
641 
642  const address_of_exprt array_pointer(
643  index_exprt(data_expr, from_integer(0, java_int_type())));
644 
646  array_pointer, data_expr, symbol_table, loc, code);
647 
649  data_expr, length_expr, symbol_table, loc, code);
650 
651  struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
652 
653  // Printable ASCII characters are between ' ' and '~'.
654  if(printable)
655  {
657  array_pointer, length_expr, " -~", symbol_table, loc, code);
658  }
659 }
660 
685  code_blockt &assignments,
686  const exprt &expr,
687  allocation_typet alloc_type,
689  size_t depth,
690  const update_in_placet &update_in_place,
691  const source_locationt &location)
692 {
693  PRECONDITION(expr.type().id()==ID_pointer);
694  const pointer_typet &replacement_pointer_type =
697 
698  // If we are changing the pointer, we generate code for creating a pointer
699  // to the substituted type instead
700  // TODO if we are comparing array types we need to compare their element
701  // types. this is for now done by implementing equality function especially
702  // for java types, technical debt TG-2707
703  if(!equal_java_types(replacement_pointer_type, pointer_type))
704  {
705  // update generic_parameter_specialization_map for the new pointer
707  generic_parameter_specialization_map_keys(
709  generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
710  replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
711 
712  const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
713  assignments, alloc_type, replacement_pointer_type, depth, location);
714 
715  // Having created a pointer to object of type replacement_pointer_type
716  // we now assign it back to the original pointer with a cast
717  // from pointer_type to replacement_pointer_type
718  assignments.add(
719  code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
720  return;
721  }
722 
723  // This deletes the recursion set entry on leaving this function scope,
724  // if one is set below.
725  recursion_set_entryt recursion_set_entry(recursion_set);
726 
727  // If the pointed value is struct-typed, then we need to prevent the
728  // possibility of this code to loop infinitely when initializing a data
729  // structure with recursive types or unbounded depth. We implement two
730  // mechanisms here. We keep a set of 'types seen', and detect when we perform
731  // a 2nd visit to the same type. We also detect the depth in the chain of
732  // (recursive) calls to the methods of this class. The depth counter is
733  // incremented only when a pointer is deferenced, including pointers to
734  // arrays.
735  //
736  // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
737  // the pointer to NULL instead of recursively initializing the struct to which
738  // it points.
739  const typet &subtype=ns.follow(pointer_type.subtype());
740  if(subtype.id()==ID_struct)
741  {
742  const struct_typet &struct_type=to_struct_type(subtype);
743  const irep_idt &struct_tag=struct_type.get_tag();
744 
745  // If this is a recursive type of some kind AND the depth is exceeded, set
746  // the pointer to null.
747  if(!recursion_set_entry.insert_entry(struct_tag) &&
749  {
750  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
751  {
752  assignments.add(get_null_assignment(expr, pointer_type));
753  }
754  // Otherwise leave it as it is.
755  return;
756  }
757  }
758 
759  // If this is a void* we *must* initialise with null:
760  // (This can currently happen for some cases of #exception_value)
761  bool must_be_null = subtype == empty_typet();
762 
763  // If we may be about to initialize a non-null enum type, always run the
764  // clinit_wrapper of its class first.
765  // TODO: TG-4689 we may want to do this for all types, not just enums, as
766  // described in the Java language specification:
767  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
768  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
769  // But we would have to put this behavior behind an option as it would have an
770  // impact on running times.
771  // Note that it would be more consistent with the behaviour of the JVM to only
772  // run clinit_wrapper if we are about to initialize an object of which we know
773  // for sure that it is not null on any following branch. However, adding this
774  // case in gen_nondet_struct_init would slow symex down too much, so if we
775  // decide to do this for all types, we should do it here.
776  // Note also that this logic is mirrored in
777  // ci_lazy_methodst::initialize_instantiated_classes.
778  if(const auto class_type = type_try_dynamic_cast<java_class_typet>(subtype))
779  {
780  if(class_type->get_base("java::java.lang.Enum") && !must_be_null)
781  {
782  const irep_idt &class_name = class_type->get_name();
783  const irep_idt class_clinit = clinit_wrapper_name(class_name);
784  gen_method_call_if_present(assignments, expr, class_clinit);
785  }
786  }
787 
788  code_blockt new_object_assignments;
789  code_blockt update_in_place_assignments;
790 
791  // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
792  // emit to `update_in_place_assignments` code for in-place initialization of
793  // the object pointed by `expr`, assuming that such object is of type
794  // `subtype`
795  if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
796  {
798  update_in_place_assignments,
799  expr,
800  subtype,
801  alloc_type,
802  depth,
804  location);
805  }
806 
807  // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
808  // above to `assignments` and return
809  if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
810  {
811  assignments.append(update_in_place_assignments);
812  return;
813  }
814 
815  // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
816  // vector of assignments that create a new object (recursively initializes it)
817  // and asign to `expr` the address of such object
818  code_blockt non_null_inst;
819 
821  non_null_inst,
822  expr,
823  subtype,
824  alloc_type,
825  depth,
827  location);
828 
829  auto set_null_inst=get_null_assignment(expr, pointer_type);
830 
831  const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
832 
833  if(must_be_null)
834  {
835  // Add the following code to assignments:
836  // <expr> = nullptr;
837  new_object_assignments.add(set_null_inst);
838  }
839  else if(!allow_null)
840  {
841  // Add the following code to assignments:
842  // <expr> = <aoe>;
843  new_object_assignments.append(non_null_inst);
844  }
845  else
846  {
847  // if(NONDET(_Bool)
848  // {
849  // <expr> = <null pointer>
850  // }
851  // else
852  // {
853  // <code from recursive call to gen_nondet_init() with
854  // tmp$<temporary_counter>>
855  // }
856  code_ifthenelset null_check(
858  std::move(set_null_inst),
859  std::move(non_null_inst));
860 
861  new_object_assignments.add(std::move(null_check));
862  }
863 
864  // Similarly to above, maybe use a conditional if both the
865  // allocate-fresh and update-in-place cases are allowed:
866  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
867  {
868  assignments.append(new_object_assignments);
869  }
870  else
871  {
873  "No-update and must-update should have already been resolved");
874 
875  code_ifthenelset update_check(
877  std::move(update_in_place_assignments),
878  std::move(new_object_assignments));
879 
880  assignments.add(std::move(update_check));
881  }
882 }
883 
911  code_blockt &assignments,
912  allocation_typet alloc_type,
913  const pointer_typet &replacement_pointer,
914  size_t depth,
915  const source_locationt &location)
916 {
917  symbolt new_symbol = get_fresh_aux_symbol(
918  replacement_pointer,
920  "tmp_object_factory",
921  loc,
922  ID_java,
923  symbol_table);
924 
925  // Generate a new object into this new symbol
927  assignments,
928  new_symbol.symbol_expr(),
929  false, // is_sub
930  "", // class_identifier
931  false, // skip_classid
932  alloc_type,
933  false, // override
934  typet(), // override_type
935  depth,
937  location);
938 
939  return new_symbol.symbol_expr();
940 }
941 
953  const exprt &expr,
954  const std::list<std::string> &string_input_values,
955  symbol_table_baset &symbol_table)
956 {
957  alternate_casest cases;
958  for(const auto &val : string_input_values)
959  {
960  exprt name_literal(ID_java_string_literal);
961  name_literal.set(ID_value, val);
962  const symbol_exprt s =
963  get_or_create_string_literal_symbol(name_literal, symbol_table, true);
964  cases.push_back(code_assignt(expr, s));
965  }
966  return cases;
967 }
968 
1001  code_blockt &assignments,
1002  const exprt &expr,
1003  bool is_sub,
1004  irep_idt class_identifier,
1005  bool skip_classid,
1006  allocation_typet alloc_type,
1007  const struct_typet &struct_type,
1008  size_t depth,
1009  const update_in_placet &update_in_place,
1010  const source_locationt &location)
1011 {
1012  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
1013  PRECONDITION(struct_type.id()==ID_struct);
1014 
1015  typedef struct_typet::componentst componentst;
1016  const irep_idt &struct_tag=struct_type.get_tag();
1017 
1018  const componentst &components=struct_type.components();
1019 
1020  // Should we write the whole object?
1021  // * Not if this is a sub-structure (a superclass object), as our caller will
1022  // have done this already
1023  // * Not if the object has already been initialised by our caller, in which
1024  // case they will set `skip_classid`
1025  // * Not if we're re-initializing an existing object (i.e. update_in_place)
1026 
1027  bool skip_special_string_fields = false;
1028 
1029  if(!is_sub &&
1030  !skip_classid &&
1031  update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
1032  {
1033  class_identifier = struct_tag;
1034 
1035  const bool is_char_sequence =
1038  const bool has_length_and_data =
1039  struct_type.has_component("length") && struct_type.has_component("data");
1040  const bool has_string_input_values =
1042 
1043  if(is_char_sequence && has_length_and_data && has_string_input_values)
1044  { // We're dealing with a string and we should set fixed input values.
1045  skip_special_string_fields = true;
1046 
1047  // We create a switch statement where each case is an assignment
1048  // of one of the fixed input strings to the input variable in question
1049 
1050  const alternate_casest cases =
1052  expr,
1054  symbol_table);
1055  assignments.add(generate_nondet_switch(
1057  cases,
1058  java_int_type(),
1059  ID_java,
1060  loc,
1061  symbol_table));
1062  }
1063  else
1064  {
1065  // Add an initial all-zero write. Most of the fields of this will be
1066  // overwritten, but it helps to have a whole-structure write that analysis
1067  // passes can easily recognise leaves no uninitialised state behind.
1068 
1069  // This code mirrors the `remove_java_new` pass:
1070  auto initial_object =
1071  zero_initializer(struct_type, source_locationt(), ns);
1072  CHECK_RETURN(initial_object.has_value());
1073  const irep_idt qualified_clsid = "java::" + id2string(class_identifier);
1075  to_struct_expr(*initial_object), ns, struct_tag_typet(qualified_clsid));
1076 
1077  // If the initialised type is a special-cased String type (one with length
1078  // and data fields introduced by string-library preprocessing), initialise
1079  // those fields with nondet values
1080  if(is_char_sequence && has_length_and_data)
1081  { // We're dealing with a string
1082  skip_special_string_fields = true;
1084  to_struct_expr(*initial_object),
1085  assignments,
1088  loc,
1090  symbol_table,
1092  }
1093 
1094  assignments.add(code_assignt(expr, *initial_object));
1095  }
1096  }
1097 
1098  for(const auto &component : components)
1099  {
1100  const typet &component_type=component.type();
1101  irep_idt name=component.get_name();
1102 
1103  member_exprt me(expr, name, component_type);
1104 
1105  if(name=="@class_identifier")
1106  {
1107  continue;
1108  }
1109  else if(name == "cproverMonitorCount")
1110  {
1111  // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
1112  // nondet. This field is only present when the java core models are
1113  // included in the class-path. It is used to implement a critical section,
1114  // which is necessary to support concurrency.
1115  if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
1116  continue;
1117  code_assignt code(me, from_integer(0, me.type()));
1118  code.add_source_location() = loc;
1119  assignments.add(code);
1120  }
1121  else if(skip_special_string_fields && (name == "length" || name == "data"))
1122  {
1123  // In this case these were set up above.
1124  continue;
1125  }
1126  else
1127  {
1128  INVARIANT(!name.empty(), "Each component of a struct must have a name");
1129 
1130  bool _is_sub=name[0]=='@';
1131 
1132  // MUST_UPDATE_IN_PLACE only applies to this object.
1133  // If this is a pointer to another object, offer the chance
1134  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1135  update_in_placet substruct_in_place=
1136  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE && !_is_sub ?
1138  update_in_place;
1140  assignments,
1141  me,
1142  _is_sub,
1143  class_identifier,
1144  false, // skip_classid
1145  alloc_type,
1146  false, // override
1147  typet(), // override_type
1148  depth,
1149  substruct_in_place,
1150  location);
1151  }
1152  }
1153 
1154  // If <class_identifier>.cproverNondetInitialize() can be found in the
1155  // symbol table, we add a call:
1156  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1157  // expr.cproverNondetInitialize();
1158  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1159 
1160  const irep_idt init_method_name =
1161  "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V";
1162  gen_method_call_if_present(assignments, expr, init_method_name);
1163 }
1164 
1201  code_blockt &assignments,
1202  const exprt &expr,
1203  bool is_sub,
1204  irep_idt class_identifier,
1205  bool skip_classid,
1206  allocation_typet alloc_type,
1207  bool override_,
1208  const typet &override_type,
1209  size_t depth,
1210  update_in_placet update_in_place,
1211  const source_locationt &location)
1212 {
1213  const typet &type=
1214  override_ ? ns.follow(override_type) : ns.follow(expr.type());
1215 
1216 
1217  if(type.id()==ID_pointer)
1218  {
1219  // dereferenced type
1221 
1222  // If we are about to initialize a generic pointer type, add its concrete
1223  // types to the map and delete them on leaving this function scope.
1225  generic_parameter_specialization_map_keys(
1227  generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
1229 
1231  assignments,
1232  expr,
1233  alloc_type,
1234  pointer_type,
1235  depth,
1236  update_in_place,
1237  location);
1238  }
1239  else if(type.id()==ID_struct)
1240  {
1241  const struct_typet struct_type=to_struct_type(type);
1242 
1243  // If we are about to initialize a generic class (as a superclass object
1244  // for a different object), add its concrete types to the map and delete
1245  // them on leaving this function scope.
1247  generic_parameter_specialization_map_keys(
1249  if(is_sub)
1250  {
1251  const typet &symbol = override_ ? override_type : expr.type();
1252  PRECONDITION(symbol.id() == ID_struct_tag);
1253  generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
1254  to_struct_tag_type(symbol), struct_type);
1255  }
1256 
1258  assignments,
1259  expr,
1260  is_sub,
1261  class_identifier,
1262  skip_classid,
1263  alloc_type,
1264  struct_type,
1265  depth,
1266  update_in_place,
1267  location);
1268  }
1269  else
1270  {
1271  // types different from pointer or structure:
1272  // bool, int, float, byte, char, ...
1273  exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
1274  : side_effect_expr_nondett(type, loc);
1275  code_assignt assign(expr, rhs);
1276  assign.add_source_location()=loc;
1277 
1278  assignments.add(assign);
1279  }
1280 }
1281 
1293  code_blockt &assignments,
1294  const std::string &basename_prefix,
1295  const exprt &min_value_expr,
1296  const exprt &max_value_expr,
1297  const source_locationt &location)
1298 {
1299  PRECONDITION(min_value_expr.type() == max_value_expr.type());
1300  // Allocate a new symbol for the int
1301  const symbolt &int_symbol = get_fresh_aux_symbol(
1302  min_value_expr.type(),
1304  basename_prefix,
1305  loc,
1306  ID_java,
1307  symbol_table);
1308  symbols_created.push_back(&int_symbol);
1309  const auto &int_symbol_expr = int_symbol.symbol_expr();
1310 
1311  // Nondet-initialize it
1313  assignments,
1314  int_symbol_expr,
1315  false, // is_sub
1316  irep_idt(),
1317  false, // skip_classid
1318  allocation_typet::LOCAL, // immaterial, type is primitive
1319  false, // override
1320  typet(), // override type is immaterial
1321  0, // depth is immaterial, always non-null
1323  location);
1324 
1325  // Insert assumptions to bound its value
1326  const auto min_assume_expr =
1327  binary_relation_exprt(int_symbol_expr, ID_ge, min_value_expr);
1328  const auto max_assume_expr =
1329  binary_relation_exprt(int_symbol_expr, ID_le, max_value_expr);
1330  assignments.add(code_assumet(min_assume_expr));
1331  assignments.add(code_assumet(max_assume_expr));
1332 
1333  return int_symbol_expr;
1334 }
1335 
1352  code_blockt &assignments,
1353  const exprt &lhs,
1354  const exprt &max_length_expr,
1355  const typet &element_type,
1356  const source_locationt &location)
1357 {
1358  const auto &length_sym_expr = gen_nondet_int_init(
1359  assignments,
1360  "nondet_array_length",
1362  max_length_expr,
1363  location);
1364 
1365  side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), loc);
1366  java_new_array.copy_to_operands(length_sym_expr);
1367  java_new_array.set(ID_length_upper_bound, max_length_expr);
1368  java_new_array.type().subtype().set(ID_element_type, element_type);
1369  code_assignt assign(lhs, java_new_array);
1370  assign.add_source_location() = loc;
1371  assignments.add(assign);
1372 }
1373 
1381  code_blockt &assignments,
1382  const exprt &expr,
1383  size_t depth,
1384  update_in_placet update_in_place,
1385  const source_locationt &location)
1386 {
1387  PRECONDITION(expr.type().id()==ID_pointer);
1388  PRECONDITION(expr.type().subtype().id() == ID_struct_tag);
1390 
1391  const typet &type=ns.follow(expr.type().subtype());
1392  const struct_typet &struct_type=to_struct_type(type);
1393  const typet &element_type =
1394  static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
1395 
1396  auto max_length_expr=from_integer(
1398 
1399  // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
1400  // initialize its elements
1401  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
1402  {
1404  assignments, expr, max_length_expr, element_type, location);
1405  }
1406 
1407  // Otherwise we're updating the array in place, and use the
1408  // existing array allocation and length.
1409 
1410  INVARIANT(
1411  is_valid_java_array(struct_type),
1412  "Java struct array does not conform to expectations");
1413 
1414  dereference_exprt deref_expr(expr, expr.type().subtype());
1415  const auto &comps=struct_type.components();
1416  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1417  exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type());
1418 
1419  if(init_array_expr.type()!=pointer_type(element_type))
1420  init_array_expr=
1421  typecast_exprt(init_array_expr, pointer_type(element_type));
1422 
1423  // Interpose a new symbol, as the goto-symex stage can't handle array indexing
1424  // via a cast.
1425  symbolt &array_init_symbol = get_fresh_aux_symbol(
1426  init_array_expr.type(),
1428  "array_data_init",
1429  loc,
1430  ID_java,
1431  symbol_table);
1432  symbols_created.push_back(&array_init_symbol);
1433  const auto &array_init_symexpr=array_init_symbol.symbol_expr();
1434  code_assignt data_assign(array_init_symexpr, init_array_expr);
1435  data_assign.add_source_location()=loc;
1436  assignments.add(data_assign);
1437 
1438  // Emit init loop for(array_init_iter=0; array_init_iter!=array.length;
1439  // ++array_init_iter) init(array[array_init_iter]);
1440  symbolt &counter = get_fresh_aux_symbol(
1441  length_expr.type(),
1443  "array_init_iter",
1444  loc,
1445  ID_java,
1446  symbol_table);
1447  symbols_created.push_back(&counter);
1448  exprt counter_expr=counter.symbol_expr();
1449 
1450  exprt java_zero=from_integer(0, java_int_type());
1451  assignments.add(code_assignt(counter_expr, java_zero));
1452 
1453  std::string head_name = id2string(counter.base_name) + "_header";
1454  code_labelt init_head_label(head_name, code_skipt());
1455  code_gotot goto_head(head_name);
1456 
1457  assignments.add(std::move(init_head_label));
1458 
1459  std::string done_name = id2string(counter.base_name) + "_done";
1460  code_labelt init_done_label(done_name, code_skipt());
1461  code_gotot goto_done(done_name);
1462 
1463  const code_ifthenelset done_test(
1464  equal_exprt(counter_expr, length_expr), goto_done);
1465 
1466  assignments.add(std::move(done_test));
1467 
1468  if(update_in_place!=update_in_placet::MUST_UPDATE_IN_PLACE)
1469  {
1470  // Add a redundant if(counter == max_length) break
1471  // that is easier for the unwinder to understand.
1472  code_ifthenelset max_test(
1473  equal_exprt(counter_expr, max_length_expr), std::move(goto_done));
1474 
1475  assignments.add(std::move(max_test));
1476  }
1477 
1478  const dereference_exprt arraycellref(
1479  plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()),
1480  array_init_symexpr.type().subtype());
1481 
1482  // MUST_UPDATE_IN_PLACE only applies to this object.
1483  // If this is a pointer to another object, offer the chance
1484  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
1485  update_in_placet child_update_in_place=
1486  update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE ?
1488  update_in_place;
1490  assignments,
1491  arraycellref,
1492  false, // is_sub
1493  irep_idt(), // class_identifier
1494  false, // skip_classid
1495  // These are variable in number, so use dynamic allocator:
1497  true, // override
1498  element_type,
1499  depth,
1500  child_update_in_place,
1501  location);
1502 
1503  exprt java_one=from_integer(1, java_int_type());
1504  code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
1505 
1506  assignments.add(std::move(incr));
1507  assignments.add(std::move(goto_head));
1508  assignments.add(std::move(init_done_label));
1509 }
1510 
1519  code_blockt &assignments,
1520  const exprt &expr,
1521  const java_class_typet &java_class_type,
1522  const source_locationt &location)
1523 {
1524  const irep_idt &class_name = java_class_type.get_name();
1525  const irep_idt values_name = id2string(class_name) + ".$VALUES";
1526  INVARIANT(
1527  ns.get_symbol_table().has_symbol(values_name),
1528  "The $VALUES array (populated by clinit_wrapper) should be in the "
1529  "symbol table");
1530  const symbolt &values = ns.lookup(values_name);
1531 
1532  // Access members (length and data) of $VALUES array
1533  dereference_exprt deref_expr(values.symbol_expr());
1534  const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type()));
1535  PRECONDITION(is_valid_java_array(deref_struct_type));
1536  const auto &comps = deref_struct_type.components();
1537  const member_exprt length_expr(deref_expr, "length", comps[1].type());
1538  const member_exprt enum_array_expr =
1539  member_exprt(deref_expr, "data", comps[2].type());
1540 
1541  const symbol_exprt &index_expr = gen_nondet_int_init(
1542  assignments,
1543  "enum_index_init",
1545  minus_exprt(length_expr, from_integer(1, java_int_type())),
1546  location);
1547 
1548  // Generate statement using pointer arithmetic to access array element:
1549  // expr = (expr.type())*(enum_array_expr + index_expr);
1550  plus_exprt plus(enum_array_expr, index_expr);
1551  const dereference_exprt arraycellref(plus);
1552  code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type()));
1553  assignments.add(enum_assign);
1554 }
1555 
1562  const std::vector<const symbolt *> &symbols_created,
1563  const source_locationt &loc,
1564  code_blockt &init_code)
1565 {
1566  // Add the following code to init_code for each symbol that's been created:
1567  // <type> <identifier>;
1568  for(const symbolt * const symbol_ptr : symbols_created)
1569  {
1570  if(!symbol_ptr->is_static_lifetime)
1571  {
1572  code_declt decl(symbol_ptr->symbol_expr());
1573  decl.add_source_location()=loc;
1574  init_code.add(decl);
1575  }
1576  }
1577 }
1578 
1591  const typet &type,
1592  const irep_idt base_name,
1593  code_blockt &init_code,
1594  symbol_table_baset &symbol_table,
1596  allocation_typet alloc_type,
1597  const source_locationt &loc,
1598  const select_pointer_typet &pointer_type_selector)
1599 {
1601  "::"+id2string(base_name);
1602 
1603  auxiliary_symbolt main_symbol;
1604  main_symbol.mode=ID_java;
1605  main_symbol.is_static_lifetime=false;
1606  main_symbol.name=identifier;
1607  main_symbol.base_name=base_name;
1608  main_symbol.type=type;
1609  main_symbol.location=loc;
1611 
1612  exprt object=main_symbol.symbol_expr();
1613 
1614  symbolt *main_symbol_ptr;
1615  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
1616  CHECK_RETURN(!moving_symbol_failed);
1617 
1618  std::vector<const symbolt *> symbols_created;
1619  symbols_created.push_back(main_symbol_ptr);
1620  java_object_factoryt state(
1621  symbols_created,
1622  loc,
1623  parameters,
1624  symbol_table,
1625  pointer_type_selector);
1626  code_blockt assignments;
1627  state.gen_nondet_init(
1628  assignments,
1629  object,
1630  false, // is_sub
1631  "", // class_identifier
1632  false, // skip_classid
1633  alloc_type,
1634  false, // override
1635  typet(), // override_type is immaterial
1636  1, // initial depth
1638  loc);
1639 
1640  declare_created_symbols(symbols_created, loc, init_code);
1641 
1642  init_code.append(assignments);
1643  return object;
1644 }
1645 
1682  const exprt &expr,
1683  code_blockt &init_code,
1684  symbol_table_baset &symbol_table,
1685  const source_locationt &loc,
1686  bool skip_classid,
1687  allocation_typet alloc_type,
1688  const java_object_factory_parameterst &object_factory_parameters,
1689  const select_pointer_typet &pointer_type_selector,
1690  update_in_placet update_in_place)
1691 {
1692  std::vector<const symbolt *> symbols_created;
1693 
1694  java_object_factoryt state(
1695  symbols_created,
1696  loc,
1697  object_factory_parameters,
1698  symbol_table,
1699  pointer_type_selector);
1700  code_blockt assignments;
1701  state.gen_nondet_init(
1702  assignments,
1703  expr,
1704  false, // is_sub
1705  "", // class_identifier
1706  skip_classid,
1707  alloc_type,
1708  false, // override
1709  typet(), // override_type is immaterial
1710  1, // initial depth
1711  update_in_place,
1712  loc);
1713 
1714  declare_created_symbols(symbols_created, loc, init_code);
1715 
1716  init_code.append(assignments);
1717 }
1718 
1721  const typet &type,
1722  const irep_idt base_name,
1723  code_blockt &init_code,
1724  symbol_tablet &symbol_table,
1725  const java_object_factory_parameterst &object_factory_parameters,
1726  allocation_typet alloc_type,
1727  const source_locationt &location)
1728 {
1729  select_pointer_typet pointer_type_selector;
1730  return object_factory(
1731  type,
1732  base_name,
1733  init_code,
1734  symbol_table,
1735  object_factory_parameters,
1736  alloc_type,
1737  location,
1738  pointer_type_selector);
1739 }
1740 
1743  const exprt &expr,
1744  code_blockt &init_code,
1745  symbol_table_baset &symbol_table,
1746  const source_locationt &loc,
1747  bool skip_classid,
1748  allocation_typet alloc_type,
1749  const java_object_factory_parameterst &object_factory_parameters,
1750  update_in_placet update_in_place)
1751 {
1752  select_pointer_typet pointer_type_selector;
1754  expr,
1755  init_code,
1756  symbol_table,
1757  loc,
1758  skip_classid,
1759  alloc_type,
1760  object_factory_parameters,
1761  pointer_type_selector,
1762  update_in_place);
1763 }
1764 
1772  code_blockt &assignments,
1773  const exprt &instance_expr,
1774  const irep_idt &method_name)
1775 {
1776  if(const auto func = symbol_table.lookup(method_name))
1777  {
1778  const java_method_typet &type = to_java_method_type(func->type);
1779  code_function_callt fun_call(func->symbol_expr());
1780  if(type.has_this())
1781  fun_call.arguments().push_back(address_of_exprt(instance_expr));
1782  assignments.add(fun_call);
1783  }
1784 }
#define loc()
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
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)
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...
Semantic type conversion.
Definition: std_expr.h:2277
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 base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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 java_object_factory_parameterst object_factory_parameters
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
exprt & op0()
Definition: expr.h:84
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:49
typet java_int_type()
Definition: java_types.cpp:32
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt&#39;s operands.
Definition: expr.h:123
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
Goto Programs with Functions.
code_operandst & statements()
Definition: std_code.h:159
symbol_table_baset & symbol_table
The symbol table.
std::vector< componentt > componentst
Definition: std_types.h:203
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4471
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:205
Nondeterministic boolean helper.
const symbol_exprt gen_nondet_int_init(code_blockt &assignments, const std::string &basename_prefix, const exprt &min_length_expr, const exprt &max_length_expr, const source_locationt &location)
Nondeterministically initializes an int i in the range min <= i <= max, where min is the integer repr...
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
codet representation of a goto statement.
Definition: std_code.h:983
typet & type()
Return the type of the expression.
Definition: expr.h:68
Allocate global objects.
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table...
Definition: java_types.h:233
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Structure type, corresponds to C style structs.
Definition: std_types.h:276
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
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:762
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
bool is_static_lifetime
Definition: symbol.h:65
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
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:3890
Equality.
Definition: std_expr.h:1484
void insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type t...
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:799
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct...
Expression Initialization.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:259
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
argumentst & arguments()
Definition: std_code.h:1109
code_blockt generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
Pick nondeterministically between imperative actions &#39;switch_cases&#39;.
Definition: nondet.cpp:87
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects...
A codet representing the declaration of a local variable.
Definition: std_code.h:352
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 These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
The empty type.
Definition: std_types.h:48
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:3355
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
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:148
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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 ...
codet representation of a label for branch targets.
Definition: std_code.h:1256
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:102
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
java_object_factoryt(std::vector< const symbolt *> &_symbols_created, const source_locationt &loc, const java_object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
std::unordered_set< irep_idt > & recursion_set
Recursion set to modify.
codet representation of a function call statement.
Definition: std_code.h:1036
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
mp_integer largest() const
Definition: std_types.cpp:195
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
void gen_method_call_if_present(code_blockt &assignments, const exprt &instance_expr, const irep_idt &method_name)
Adds a call for the given method to the end of assignments if the method exists in the symbol table...
Operator to return the address of an object.
Definition: std_expr.h:3255
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1942
void gen_nondet_enum_init(code_blockt &assignments, const exprt &expr, const java_class_typet &java_class_type, const source_locationt &location)
We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet...
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
The Boolean constant false.
Definition: std_expr.h:4452
update_in_placet
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:215
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...
namespacet ns
A namespace built from exclusively one symbol table - the one above.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
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:170
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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.
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:54
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:46
The symbol table base class interface.
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:22
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:35
bool has_this() const
Definition: std_types.h:854
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(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 reference-typed object tree rooted at expr, allocating child objects...
const source_locationt & source_location() const
Definition: expr.h:228
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
static mp_integer max_value(const typet &type)
Get max value for an integer type.
size_t min_nondet_string_length
Minimum value for the non-deterministically-chosen length of a string.
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, 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...
symbol_exprt get_or_create_string_literal_symbol(const exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
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...
alternate_casest get_string_input_values_code(const exprt &expr, const std::list< std::string > &string_input_values, symbol_table_baset &symbol_table)
Creates an alternate_casest vector in which each item contains an assignment of a string from string_...
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...
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 java_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...
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:233
A codet representing sequential composition of program statements.
Definition: std_code.h:150
Binary minus.
Definition: std_expr.h:1106
A codet representing a skip statement.
Definition: std_code.h:237
codet representation of an if-then-else statement.
Definition: std_code.h:614
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
dstringt irep_idt
Definition: irep.h:32
exprt dynamic_object(const exprt &pointer)
recursion_set_entryt & operator=(const recursion_set_entryt &)=delete
~recursion_set_entryt()
Removes erase_entry (if set) from the controlled set.
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:38
irep_idt get_tag() const
Definition: std_types.h:226
An expression containing a side effect.
Definition: std_code.h:1560
operandst & operands()
Definition: expr.h:78
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:1920
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:75
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
void initialize_nondet_string_fields(struct_exprt &struct_expr, code_blockt &code, const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
Initialise length and data fields for a nondeterministic String structure.
const source_locationt & loc
The source location for new statements emitted during the operation of the methods in this class...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
A codet representing an assignment in the program.
Definition: std_code.h:256
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
std::vector< codet > alternate_casest
Definition: nondet.h:26
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:1595