cprover
assignments_from_json.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Assignments to values specified in JSON files
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
10 
11 #include "ci_lazy_methods_needed.h"
12 #include "code_with_references.h"
15 #include "java_string_literals.h"
16 #include "java_utils.h"
17 
19 #include <util/allocate_objects.h>
21 #include <util/expr_initializer.h>
22 #include <util/prefix.h>
23 #include <util/unicode.h>
24 
30 {
36 
39 
43 
47  std::unordered_map<std::string, object_creation_referencet> &references;
48 
51 
55 
59 };
60 
61 static java_class_typet
62 followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
63 {
65  const java_class_typet &java_class_type =
66  to_java_class_type(namespacet{symbol_table}.follow(pointer_type.subtype()));
67  return java_class_type;
68 }
69 
70 static bool
71 has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
72 {
73  return followed_class_type(expr, symbol_table).get_is_enumeration();
74 }
75 
101  const exprt &expr,
102  const symbol_table_baset &symbol_table,
103  const java_class_typet &declaring_class_type)
104 {
106  return followed_class_type(expr, symbol_table) == declaring_class_type &&
107  declaring_class_type.get_is_enumeration();
108 }
109 
116 {
117  if(!json.is_object())
118  return {};
119  const auto &json_object = to_json_object(json);
120  if(json_object.find("@type") == json_object.end())
121  return {};
122  return json_object["@type"].value;
123 }
124 
131 static bool has_id(const jsont &json)
132 {
133  if(!json.is_object())
134  return false;
135  const auto &json_object = to_json_object(json);
136  return json_object.find("@id") != json_object.end();
137 }
138 
143 static bool is_reference(const jsont &json)
144 {
145  if(!json.is_object())
146  return false;
147  const auto &json_object = to_json_object(json);
148  return json_object.find("@ref") != json_object.end();
149 }
150 
154 static std::string get_id_or_reference_value(const jsont &json)
155 {
157  if(has_id(json))
158  return json["@id"].value;
159  return json["@ref"].value;
160 }
161 
166 static std::string get_enum_id(
167  const exprt &expr,
168  const jsont &json,
169  const symbol_table_baset &symbol_table)
170 {
171  PRECONDITION(json.is_object());
172  const auto &json_object = to_json_object(json);
173  INVARIANT(
174  json_object.find("name") != json_object.end(),
175  "JSON representation of enums should include name field");
176  return id2string(followed_class_type(expr, symbol_table).get_tag()) + '.' +
177  (json["name"].value);
178 }
179 
184 static bool has_nondet_length(const jsont &json)
185 {
186  if(!json.is_object())
187  return false;
188  const auto &json_object = to_json_object(json);
189  auto nondet_it = json_object.find("@nondetLength");
190  return nondet_it != json_object.end() && nondet_it->second.is_true();
191 }
192 
197 static jsont get_untyped(const jsont &json, const std::string &object_key)
198 {
199  if(!json.is_object())
200  return json;
201 
202  const auto &json_object = to_json_object(json);
203  PRECONDITION(
204  get_type(json) || json_object.find("@nondetLength") != json_object.end());
205 
206  return json[object_key];
207 }
208 
211 {
212  return get_untyped(json, "value");
213 }
214 
219 static json_arrayt
220 get_untyped_array(const jsont &json, const typet &element_type)
221 {
222  const jsont untyped = get_untyped(json, "@items");
223  PRECONDITION(untyped.is_array());
224  const auto &json_array = to_json_array(untyped);
225  if(element_type == java_char_type())
226  {
227  PRECONDITION(json_array.size() == 1);
228  const auto &first = *json_array.begin();
229  PRECONDITION(first.is_string());
230  const auto &json_string = to_json_string(first);
231 
232  const auto wide_string = utf8_to_utf16_native_endian(json_string.value);
233  auto string_range = make_range(wide_string.begin(), wide_string.end());
234  const auto json_range = string_range.map([](const wchar_t &c) {
235  const std::u16string u16(1, c);
237  });
238  return json_arrayt{json_range.begin(), json_range.end()};
239  }
240  return json_array;
241 }
242 
248 {
249  return get_untyped(json, "value");
250 }
251 
266  const jsont &json,
267  const optionalt<std::string> &type_from_array,
268  const symbol_table_baset &symbol_table)
269 {
270  const auto type_from_json = get_type(json);
271  if(!type_from_json && !type_from_array)
272  return {}; // no runtime type specified, use compile-time type
273  const auto runtime_type = [&]() -> std::string {
274  if(type_from_json)
275  return "java::" + *type_from_json;
276  INVARIANT(
277  type_from_array->find('L') == 0 &&
278  type_from_array->rfind(';') == type_from_array->length() - 1,
279  "Types inferred from the type of a containing array should be of the "
280  "form Lmy.package.name.ClassName;");
281  return "java::" + type_from_array->substr(1, type_from_array->length() - 2);
282  }();
283  if(!symbol_table.has_symbol(runtime_type))
284  return {}; // Fall back to compile-time type if runtime type was not found
285  const auto &replacement_class_type =
287  return replacement_class_type;
288 }
289 
303  const jsont &json,
304  const optionalt<std::string> &type_from_array)
305 {
306  if(const auto json_array_type = get_type(json))
307  {
308  INVARIANT(
309  json_array_type->find('[') == 0,
310  "Array types in the JSON input should be of the form "
311  "[[...[Lmy.package.name.ClassName; (with n occurrences of [ for an "
312  "n-dimensional array)");
313  return json_array_type->substr(1);
314  }
315  else if(type_from_array)
316  {
317  INVARIANT(
318  type_from_array->find('[') == 0,
319  "For arrays that are themselves contained by an array from which a type "
320  "is inferred, such a type should be of the form "
321  "[[...[Lmy.package.name.ClassName;");
322  return type_from_array->substr(1);
323  }
324  return {};
325 }
326 
327 code_with_references_listt assign_from_json_rec(
328  const exprt &expr,
329  const jsont &json,
330  const optionalt<std::string> &type_from_array,
331  object_creation_infot &info);
332 
337 assign_primitive_from_json(const exprt &expr, const jsont &json)
338 {
340  if(json.is_null()) // field is not mentioned in json, leave as default value
341  return result;
342  if(expr.type() == java_boolean_type())
343  {
344  result.add(code_assignt{
345  expr, json.is_true() ? (exprt)true_exprt{} : (exprt)false_exprt{}});
346  }
347  else if(
348  expr.type() == java_int_type() || expr.type() == java_byte_type() ||
349  expr.type() == java_short_type() || expr.type() == java_long_type())
350  {
351  result.add(
352  code_assignt{expr, from_integer(std::stoll(json.value), expr.type())});
353  }
354  else if(expr.type() == java_double_type())
355  {
356  ieee_floatt ieee_float(to_floatbv_type(expr.type()));
357  ieee_float.from_double(std::stod(json.value));
358  result.add(code_assignt{expr, ieee_float.to_expr()});
359  }
360  else if(expr.type() == java_float_type())
361  {
362  ieee_floatt ieee_float(to_floatbv_type(expr.type()));
363  ieee_float.from_float(std::stof(json.value));
364  result.add(code_assignt{expr, ieee_float.to_expr()});
365  }
366  else if(expr.type() == java_char_type())
367  {
368  const std::wstring wide_value = utf8_to_utf16_native_endian(json.value);
369  PRECONDITION(wide_value.length() == 1);
370  result.add(
371  code_assignt{expr, from_integer(wide_value.front(), expr.type())});
372  }
373  return result;
374 }
375 
378 static code_assignt assign_null(const exprt &expr)
379 {
380  return code_assignt{expr, null_pointer_exprt{to_pointer_type(expr.type())}};
381 }
382 
386 static code_with_references_listt assign_array_data_component_from_json(
387  const exprt &expr,
388  const jsont &json,
389  const optionalt<std::string> &type_from_array,
390  object_creation_infot &info)
391 {
392  const auto &java_class_type = followed_class_type(expr, info.symbol_table);
393  const auto &data_component = java_class_type.components()[2];
394  const auto &element_type =
396  const exprt data_member_expr = typecast_exprt::conditional_cast(
397  member_exprt{dereference_exprt{expr}, "data", data_component.type()},
398  pointer_type(element_type));
399 
400  const symbol_exprt &array_init_data =
402  data_member_expr.type(), "user_specified_array_data_init");
404  result.add(code_assignt{array_init_data, data_member_expr, info.loc});
405 
406  size_t index = 0;
407  const optionalt<std::string> inferred_element_type =
408  element_type_from_array_type(json, type_from_array);
409  const json_arrayt json_array = get_untyped_array(json, element_type);
410  for(auto it = json_array.begin(); it < json_array.end(); it++, index++)
411  {
412  const dereference_exprt element_at_index = array_element_from_pointer(
413  array_init_data, from_integer(index, java_int_type()));
414  result.append(
415  assign_from_json_rec(element_at_index, *it, inferred_element_type, info));
416  }
417  return result;
418 }
419 
425 static std::pair<symbol_exprt, code_with_references_listt>
426 nondet_length(allocate_objectst &allocate, source_locationt loc)
427 {
428  symbol_exprt length_expr = allocate.allocate_automatic_local_object(
429  java_int_type(), "user_specified_array_length");
431  code.add(
432  code_assignt{length_expr, side_effect_expr_nondett{java_int_type(), loc}});
434  length_expr, ID_ge, from_integer(0, java_int_type())}});
435  return std::make_pair(length_expr, std::move(code));
436 }
437 
449 static std::pair<code_with_references_listt, exprt>
450 assign_det_length_array_from_json(
451  const exprt &expr,
452  const jsont &json,
453  const optionalt<std::string> &type_from_array,
454  object_creation_infot &info)
455 {
457  const auto &element_type =
459  const json_arrayt json_array = get_untyped_array(json, element_type);
460  const auto number_of_elements =
461  from_integer(json_array.size(), java_int_type());
462  return {
463  assign_array_data_component_from_json(expr, json, type_from_array, info),
464  number_of_elements};
465 }
466 
478 static code_with_references_listt assign_nondet_length_array_from_json(
479  const exprt &array,
480  const jsont &json,
481  const exprt &given_length_expr,
482  const optionalt<std::string> &type_from_array,
483  object_creation_infot &info)
484 {
486  const auto &element_type =
488  const json_arrayt json_array = get_untyped_array(json, element_type);
490  exprt number_of_elements = from_integer(json_array.size(), java_int_type());
491  result.add(code_assumet{and_exprt{
492  binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements},
494  given_length_expr,
495  ID_le,
497  result.append(
498  assign_array_data_component_from_json(array, json, type_from_array, info));
499  return result;
500 }
501 
505 static code_assignt assign_string_from_json(
506  const jsont &json,
507  const exprt &expr,
508  object_creation_infot &info)
509 {
510  const auto json_string = get_untyped_string(json);
511  PRECONDITION(json_string.is_string());
512  return code_assignt{expr,
514  json_string.value, info.symbol_table, true)};
515 }
516 
520 static code_with_references_listt assign_struct_components_from_json(
521  const exprt &expr,
522  const jsont &json,
523  object_creation_infot &info)
524 {
525  const java_class_typet &java_class_type =
526  to_java_class_type(namespacet{info.symbol_table}.follow(expr.type()));
528  for(const auto &component : java_class_type.components())
529  {
530  const irep_idt &component_name = component.get_name();
531  if(
532  component_name == JAVA_CLASS_IDENTIFIER_FIELD_NAME ||
533  component_name == "cproverMonitorCount")
534  {
535  continue;
536  }
537  member_exprt member_expr{expr, component_name, component.type()};
538  if(component_name[0] == '@') // component is parent struct type
539  {
540  result.append(
541  assign_struct_components_from_json(member_expr, json, info));
542  }
543  else // component is class field (pointer to struct)
544  {
545  const auto member_json = [&]() -> jsont {
546  if(
547  is_primitive_wrapper_type_id(java_class_type.get_name()) &&
548  id2string(component_name) == "value")
549  {
550  return get_untyped_primitive(json);
551  }
552  return json[id2string(component_name)];
553  }();
554  result.append(assign_from_json_rec(member_expr, member_json, {}, info));
555  }
556  }
557  return result;
558 }
559 
564 static code_with_references_listt assign_struct_from_json(
565  const exprt &expr,
566  const jsont &json,
567  object_creation_infot &info)
568 {
569  const namespacet ns{info.symbol_table};
570  const java_class_typet &java_class_type =
571  to_java_class_type(ns.follow(expr.type()));
573  if(is_java_string_type(java_class_type))
574  {
575  result.add(assign_string_from_json(json, expr, info));
576  }
577  else
578  {
579  auto initial_object = zero_initializer(expr.type(), info.loc, ns);
580  CHECK_RETURN(initial_object.has_value());
582  to_struct_expr(*initial_object),
583  ns,
584  struct_tag_typet("java::" + id2string(java_class_type.get_tag())));
585  result.add(code_assignt{expr, *initial_object});
586  result.append(assign_struct_components_from_json(expr, json, info));
587  }
588  return result;
589 }
590 
592 static code_with_references_listt assign_non_enum_pointer_from_json(
593  const exprt &expr,
594  const jsont &json,
595  object_creation_infot &info)
596 {
598  code_blockt output_code;
599  exprt dereferenced_symbol_expr =
601  output_code, expr, to_pointer_type(expr.type()).subtype());
602  for(codet &code : output_code.statements())
603  result.add(std::move(code));
604  result.append(assign_struct_from_json(dereferenced_symbol_expr, json, info));
605  return result;
606 }
607 
615 static code_with_references_listt assign_enum_from_json(
616  const exprt &expr,
617  const jsont &json,
618  object_creation_infot &info)
619 {
620  const auto &java_class_type = followed_class_type(expr, info.symbol_table);
621  const std::string &enum_name = id2string(java_class_type.get_name());
623  if(const auto func = info.symbol_table.lookup(clinit_wrapper_name(enum_name)))
624  result.add(code_function_callt{func->symbol_expr()});
625 
626  const irep_idt values_name = enum_name + ".$VALUES";
627  if(!info.symbol_table.has_symbol(values_name))
628  {
629  // Fallback: generate a new enum instance instead of getting it from $VALUES
630  result.append(assign_non_enum_pointer_from_json(expr, json, info));
631  return result;
632  }
633 
634  dereference_exprt values_struct{
635  info.symbol_table.lookup_ref(values_name).symbol_expr()};
636  const auto &values_struct_type =
637  to_struct_type(namespacet{info.symbol_table}.follow(values_struct.type()));
638  PRECONDITION(is_valid_java_array(values_struct_type));
639  const member_exprt values_data = member_exprt{
640  values_struct, "data", values_struct_type.components()[2].type()};
641 
642  const exprt ordinal_expr =
643  from_integer(std::stoi(json["ordinal"].value), java_int_type());
644 
645  result.add(code_assignt{
646  expr,
648  array_element_from_pointer(values_data, ordinal_expr), expr.type())});
649  return result;
650 }
651 
656 static code_with_references_listt assign_pointer_from_json(
657  const exprt &expr,
658  const jsont &json,
659  object_creation_infot &info)
660 {
661  // This check can be removed when tracking reference-equal objects across
662  // different classes has been implemented.
663  if(has_enum_type(expr, info.symbol_table))
664  return assign_enum_from_json(expr, json, info);
665  else
666  return assign_non_enum_pointer_from_json(expr, json, info);
667 }
668 
674 static code_with_references_listt assign_pointer_with_given_type_from_json(
675  const exprt &expr,
676  const jsont &json,
678  object_creation_infot &info)
679 {
680  const auto &pointer_type = to_pointer_type(expr.type());
681  pointer_typet replacement_pointer_type =
683  if(!equal_java_types(pointer_type, replacement_pointer_type))
684  {
685  const auto &new_symbol =
687  replacement_pointer_type, "user_specified_subtype_symbol");
688  if(info.needed_lazy_methods)
689  {
690  info.needed_lazy_methods->add_all_needed_classes(
691  replacement_pointer_type);
692  }
693 
694  auto result = assign_pointer_from_json(new_symbol, json, info);
695  result.add(code_assignt{expr, typecast_exprt{new_symbol, pointer_type}});
696  return result;
697  }
698  else
699  return assign_pointer_from_json(expr, json, info);
700 }
701 
702 struct get_or_create_reference_resultt
703 {
706  bool newly_allocated;
708  std::unordered_map<std::string, object_creation_referencet>::iterator
709  reference;
712 };
713 
729 static get_or_create_reference_resultt get_or_create_reference(
730  const exprt &expr,
731  const std::string &id,
732  object_creation_infot &info)
733 {
734  const auto &pointer_type = to_pointer_type(expr.type());
735  const auto id_it = info.references.find(id);
736  if(id_it == info.references.end())
737  {
739  object_creation_referencet reference;
740  if(is_java_array_type(expr.type()))
741  {
743  pointer_type, "user_specified_array_ref");
744  reference.array_length =
746  java_int_type(), "user_specified_array_length");
747  code.add(reference_allocationt{id, info.loc});
748  }
749  else
750  {
751  code_blockt block;
753  block, expr, pointer_type.subtype());
754  code.add(block);
755  }
756  auto iterator_inserted_pair = info.references.insert({id, reference});
757  return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
758  }
759  return {false, id_it, {}};
760 }
761 
784 static code_with_references_listt assign_reference_from_json(
785  const exprt &expr,
786  const jsont &json,
787  const optionalt<std::string> &type_from_array,
788  object_creation_infot &info)
789 {
790  const std::string &id = has_enum_type(expr, info.symbol_table)
791  ? get_enum_id(expr, json, info.symbol_table)
793  auto get_reference_result = get_or_create_reference(expr, id, info);
794  const bool is_new_id = get_reference_result.newly_allocated;
795  object_creation_referencet &reference =
796  get_reference_result.reference->second;
797  code_with_references_listt result = std::move(get_reference_result.code);
798  if(has_id(json) || (is_new_id && has_enum_type(expr, info.symbol_table)))
799  {
800  if(is_java_array_type(expr.type()))
801  {
802  INVARIANT(
803  reference.array_length, "an array reference should store its length");
805  {
806  result.append(assign_nondet_length_array_from_json(
807  reference.expr,
808  json,
809  *reference.array_length,
810  type_from_array,
811  info));
812  }
813  else
814  {
815  auto code_length_pair = assign_det_length_array_from_json(
816  reference.expr, json, type_from_array, info);
817  result.append(std::move(code_length_pair.first));
818  reference.array_length = std::move(code_length_pair.second);
819  }
820  }
821  else
822  {
823  result.append(
824  assign_struct_from_json(dereference_exprt(reference.expr), json, info));
825  }
826  }
827  result.add(code_assignt{
828  expr, typecast_exprt::conditional_cast(reference.expr, expr.type())});
829  return result;
830 }
831 
840 code_with_references_listt assign_from_json_rec(
841  const exprt &expr,
842  const jsont &json,
843  const optionalt<std::string> &type_from_array,
844  object_creation_infot &info)
845 {
848  {
849  if(json.is_null())
850  {
851  result.add(assign_null(expr));
852  return result;
853  }
854  else if(
855  is_reference(json) || has_id(json) ||
857  expr, info.symbol_table, info.declaring_class_type))
858  // The last condition can be replaced with
859  // has_enum_type(expr, info.symbol_table) once tracking reference-equality
860  // across different classes has been implemented.
861  {
862  return assign_reference_from_json(expr, json, type_from_array, info);
863  }
864  else if(is_java_array_type(expr.type()))
865  {
867  {
868  auto length_code_pair = nondet_length(info.allocate_objects, info.loc);
869  length_code_pair.second.add(
870  allocate_array(expr, length_code_pair.first, info.loc));
871  length_code_pair.second.append(assign_nondet_length_array_from_json(
872  expr, json, length_code_pair.first, type_from_array, info));
873  return length_code_pair.second;
874  }
875  else
876  {
878  const auto &element_type =
880  const std::size_t length = get_untyped_array(json, element_type).size();
881  result.add(allocate_array(
882  expr, from_integer(length, java_int_type()), info.loc));
883  result.append(assign_array_data_component_from_json(
884  expr, json, type_from_array, info));
885  return result;
886  }
887  }
888  else if(
889  const auto runtime_type =
890  ::runtime_type(json, type_from_array, info.symbol_table))
891  {
892  return assign_pointer_with_given_type_from_json(
893  expr, json, *runtime_type, info);
894  }
895  else
896  return assign_pointer_from_json(expr, json, info);
897  }
898  else
899  result.append(
900  assign_primitive_from_json(expr, get_untyped_primitive(json)));
901  return result;
902 }
903 
905  const exprt &expr,
906  const jsont &json,
907  const irep_idt &function_id,
908  symbol_table_baset &symbol_table,
909  optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
910  size_t max_user_array_length,
911  std::unordered_map<std::string, object_creation_referencet> &references)
912 {
913  source_locationt location{};
914  location.set_function(function_id);
915  allocate_objectst allocate(ID_java, location, function_id, symbol_table);
916  const symbolt *function_symbol = symbol_table.lookup(function_id);
917  INVARIANT(function_symbol, "Function must appear in symbol table");
918  const auto class_name = declaring_class(*function_symbol);
919  INVARIANT(
920  class_name,
921  "Function " + id2string(function_id) + " must be declared by a class.");
922  const auto &class_type =
923  to_java_class_type(symbol_table.lookup_ref(*class_name).type);
924  object_creation_infot info{allocate,
925  symbol_table,
926  needed_lazy_methods,
927  references,
928  location,
929  max_user_array_length,
930  class_type};
931  code_with_references_listt code_with_references =
932  assign_from_json_rec(expr, json, {}, info);
933  code_blockt assignments;
934  allocate.declare_created_symbols(assignments);
935  std::for_each(
936  assignments.statements().rbegin(),
937  assignments.statements().rend(),
938  [&](const codet &c) {
939  code_with_references.add_to_front(code_without_referencest{c});
940  });
941  return code_with_references;
942 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
dereference_exprt array_element_from_pointer(const exprt &pointer, const exprt &index)
Generate statement using pointer arithmetic to access the element at the given index of a pointer arr...
static java_class_typet followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
static bool has_id(const jsont &json)
Return true iff the argument has a "@id" key.
static std::string get_id_or_reference_value(const jsont &json)
Return the unique ID of all objects that are reference-equal to this one.
static bool has_nondet_length(const jsont &json)
Return true iff the argument has a "@nondetLength": true entry.
static std::string get_enum_id(const exprt &expr, const jsont &json, const symbol_table_baset &symbol_table)
Return a unique ID for an enum, based on its type and name field.
static bool is_enum_with_type_equal_to_declaring_type(const exprt &expr, const symbol_table_baset &symbol_table, const java_class_typet &declaring_class_type)
This function is used as a workaround until reference-equal objects defined across several classes ar...
static bool is_reference(const jsont &json)
Return true iff the argument has a "@ref" key.
static jsont get_untyped(const jsont &json, const std::string &object_key)
For typed versions of primitive, string or array types, looks up their untyped contents with the key ...
static jsont get_untyped_primitive(const jsont &json)
get_untyped for primitive types.
static optionalt< java_class_typet > runtime_type(const jsont &json, const optionalt< std::string > &type_from_array, const symbol_table_baset &symbol_table)
Given a JSON representation of a (non-array) reference-typed object and a type inferred from the type...
static optionalt< std::string > element_type_from_array_type(const jsont &json, const optionalt< std::string > &type_from_array)
Given a JSON representation of an array and a type inferred from the type of a containing array,...
static json_arrayt get_untyped_array(const jsont &json, const typet &element_type)
get_untyped for array types.
static bool has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
static jsont get_untyped_string(const jsont &json)
get_untyped for string types.
static optionalt< std::string > get_type(const jsont &json)
If the argument has a "@type" key, return the corresponding value, else return an empty optional.
code_with_references_listt assign_from_json(const exprt &expr, const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > &needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references)
Given an expression expr representing a Java object or primitive and a JSON representation json of th...
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Context-insensitive lazy methods container.
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.
Extract class identifier.
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
exprt allocate_dynamic_object_symbol(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generates code for allocating a dynamic object.
exprt allocate_dynamic_object(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that derefer...
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Boolean AND.
Definition: std_expr.h:1835
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:644
A codet representing an assignment in the program.
Definition: std_code.h:295
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
A codet representing sequential composition of program statements.
Definition: std_code.h:170
code_operandst & statements()
Definition: std_code.h:178
codet representation of a function call statement.
Definition: std_code.h:1215
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
void append(code_with_references_listt &&other)
void add(code_without_referencest code)
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
Operator to dereference a pointer.
Definition: pointer_expr.h:256
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2726
bool get_is_enumeration() const
is class an enumeration?
Definition: java_types.h:406
const componentst & components() const
Definition: java_types.h:226
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:559
arrayt::iterator end()
Definition: json.h:251
std::size_t size() const
Definition: json.h:202
arrayt::iterator begin()
Definition: json.h:236
Definition: json.h:27
bool is_array() const
Definition: json.h:61
Extract member of struct or union.
Definition: std_expr.h:2528
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The null pointer constant.
Definition: std_expr.h:2751
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
Allocation code which contains a reference.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
void set_function(const irep_idt &function)
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:498
irep_idt get_tag() const
Definition: std_types.h:163
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
typet type
Type of symbol.
Definition: symbol.h:31
The Boolean constant true.
Definition: std_expr.h:2717
Semantic type conversion.
Definition: std_expr.h:1781
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
codet allocate_array(const exprt &expr, const exprt &array_length_expr, const source_locationt &loc)
Allocate a fresh array of length array_length_expr and assigns expr to it.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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...
static irep_idt get_tag(const typet &type)
Produce code for simple implementation of String Java libraries.
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
signedbv_typet java_int_type()
Definition: java_types.cpp:32
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
Definition: java_types.cpp:164
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Definition: java_types.cpp:834
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
Definition: java_types.cpp:891
const typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
Definition: java_types.cpp:145
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
signedbv_typet java_short_type()
Definition: java_types.cpp:50
floatbv_typet java_double_type()
Definition: java_types.cpp:74
floatbv_typet java_float_type()
Definition: java_types.cpp:68
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
signedbv_typet java_long_type()
Definition: java_types.cpp:44
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:571
bool is_primitive_wrapper_type_id(const irep_idt &id)
Returns true iff the argument is the symbol-table identifier of a Java primitive wrapper type (for ex...
Definition: java_utils.cpp:108
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
Definition: java_utils.cpp:26
pointer_typet pointer_to_replacement_type(const pointer_typet &given_pointer_type, const java_class_typet &replacement_class_type)
Given a pointer type to a Java class and a type representing a more specific Java class,...
Definition: java_utils.cpp:272
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
json_stringt & to_json_string(jsont &json)
Definition: json.h:456
nonstd::optional< T > optionalt
Definition: optional.h:35
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1520
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
Values passed around between most functions of the recursive deterministic assignment algorithm enter...
allocate_objectst & allocate_objects
Handles allocation of new symbols, adds them to its symbol table (which will usually be the same as t...
const source_locationt & loc
Source location associated with the newly added codet.
size_t max_user_array_length
Maximum value allowed for any (constant or variable length) arrays in user code.
symbol_table_baset & symbol_table
Used for looking up symbols corresponding to Java classes and methods.
optionalt< ci_lazy_methods_neededt > & needed_lazy_methods
Where runtime types differ from compile-time types, we need to mark the runtime types as needed by la...
std::unordered_map< std::string, object_creation_referencet > & references
Map to keep track of reference-equal objects.
const java_class_typet & declaring_class_type
Used for the workaround for enums only.
Information to store when several references point to the same Java object.
exprt expr
Expression for the symbol that stores the value that may be reference equal to other values.
optionalt< exprt > array_length
If symbol is an array, this expression stores its length.
std::string utf16_native_endian_to_utf8(const char16_t utf16_char)
Definition: unicode.cpp:361
std::wstring utf8_to_utf16_native_endian(const std::string &in)
Convert UTF8-encoded string to UTF-16 with architecture-native endianness.
Definition: unicode.cpp:193