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 }
java_static_initializers.h
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
has_nondet_length
static bool has_nondet_length(const jsont &json)
Return true iff the argument has a "@nondetLength": true entry.
Definition: assignments_from_json.cpp:184
ieee_floatt
Definition: ieee_float.h:120
code_with_references_listt::add
void add(code_without_referencest code)
Definition: code_with_references.cpp:50
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
has_enum_type
static bool has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
Definition: assignments_from_json.cpp:71
JAVA_CLASS_IDENTIFIER_FIELD_NAME
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Definition: class_identifier.h:20
allocate_array
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.
Definition: code_with_references.cpp:13
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
object_creation_infot::needed_lazy_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...
Definition: assignments_from_json.cpp:42
code_with_references.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
java_string_literals.h
typet
The type of an expression, extends irept.
Definition: type.h:29
java_long_type
signedbv_typet java_long_type()
Definition: java_types.cpp:44
java_array_element_type
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
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
java_class_typet::get_is_enumeration
bool get_is_enumeration() const
is class an enumeration?
Definition: java_types.h:406
get_enum_id
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.
Definition: assignments_from_json.cpp:166
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:579
prefix.h
object_creation_infot::max_user_array_length
size_t max_user_array_length
Maximum value allowed for any (constant or variable length) arrays in user code.
Definition: assignments_from_json.cpp:54
and_exprt
Boolean AND.
Definition: std_expr.h:2137
object_creation_infot::allocate_objects
allocate_objectst & allocate_objects
Handles allocation of new symbols, adds them to its symbol table (which will usually be the same as t...
Definition: assignments_from_json.cpp:35
is_valid_java_array
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
Definition: java_types.cpp:834
exprt
Base class for all expressions.
Definition: expr.h:53
java_string_library_preprocess.h
Produce code for simple implementation of String Java libraries.
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
object_creation_infot::references
std::unordered_map< std::string, object_creation_referencet > & references
Map to keep track of reference-equal objects.
Definition: assignments_from_json.cpp:47
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
get_untyped
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 ...
Definition: assignments_from_json.cpp:197
object_creation_infot::loc
const source_locationt & loc
Source location associated with the newly added codet.
Definition: assignments_from_json.cpp:50
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
get_or_create_string_literal_symbol
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
Definition: java_string_literals.cpp:38
jsont
Definition: json.h:27
object_creation_infot::declaring_class_type
const java_class_typet & declaring_class_type
Used for the workaround for enums only.
Definition: assignments_from_json.cpp:58
is_reference
static bool is_reference(const jsont &json)
Return true iff the argument has a "@ref" key.
Definition: assignments_from_json.cpp:143
json_arrayt::end
arrayt::iterator end()
Definition: json.h:251
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
json_arrayt
Definition: json.h:165
runtime_type
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...
Definition: assignments_from_json.cpp:265
java_class_typet
Definition: java_types.h:199
get_id_or_reference_value
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.
Definition: assignments_from_json.cpp:154
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
object_creation_infot
Values passed around between most functions of the recursive deterministic assignment algorithm enter...
Definition: assignments_from_json.cpp:30
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:163
json_arrayt::begin
arrayt::iterator begin()
Definition: json.h:236
object_creation_referencet::expr
exprt expr
Expression for the symbol that stores the value that may be reference equal to other values.
Definition: code_with_references.h:27
set_class_identifier
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Definition: class_identifier.cpp:82
equal_java_types
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
Definition: java_types.cpp:891
expr_initializer.h
Expression Initialization.
is_java_string_type
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
Definition: java_utils.cpp:33
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
reference_allocationt
Allocation code which contains a reference.
Definition: code_with_references.h:77
get_untyped_string
static jsont get_untyped_string(const jsont &json)
get_untyped for string types.
Definition: assignments_from_json.cpp:247
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
allocate_objectst::allocate_dynamic_object_symbol
exprt allocate_dynamic_object_symbol(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generates code for allocating a dynamic object.
Definition: allocate_objects.cpp:124
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
ci_lazy_methods_needed.h
Context-insensitive lazy methods container.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
element_type_from_array_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,...
Definition: assignments_from_json.cpp:302
object_creation_infot::symbol_table
symbol_table_baset & symbol_table
Used for looking up symbols corresponding to Java classes and methods.
Definition: assignments_from_json.cpp:38
array_element_from_pointer
dereference_exprt array_element_from_pointer(const exprt &pointer, const exprt &index)
Generate statement using pointer arithmetic to access the element at the given index of a pointer arr...
Definition: array_element_from_pointer.cpp:12
is_java_array_type
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
Definition: java_types.cpp:164
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
utf16_native_endian_to_utf8
std::string utf16_native_endian_to_utf8(const char16_t utf16_char)
Definition: unicode.cpp:361
is_enum_with_type_equal_to_declaring_type
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...
Definition: assignments_from_json.cpp:100
object_creation_referencet
Information to store when several references point to the same Java object.
Definition: code_with_references.h:24
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
array_element_from_pointer.h
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
utf8_to_utf16_native_endian
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
pointer_to_replacement_type
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:279
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:50
object_creation_referencet::array_length
optionalt< exprt > array_length
If symbol is an array, this expression stores its length.
Definition: code_with_references.h:33
allocate_objectst::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Definition: allocate_objects.cpp:226
source_locationt
Definition: source_location.h:20
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
java_class_typet::get_name
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:559
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1513
code_with_references_listt::append
void append(code_with_references_listt &&other)
Definition: code_with_references.cpp:67
assignments_from_json.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
java_class_typet::components
const componentst & components() const
Definition: java_types.h:226
json_arrayt::size
std::size_t size() const
Definition: json.h:202
get_untyped_array
static json_arrayt get_untyped_array(const jsont &json, const typet &element_type)
get_untyped for array types.
Definition: assignments_from_json.cpp:220
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:74
code_with_references_listt
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
Definition: code_with_references.h:93
to_json_string
json_stringt & to_json_string(jsont &json)
Definition: json.h:456
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
followed_class_type
static java_class_typet followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
Definition: assignments_from_json.cpp:62
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
jsont::is_array
bool is_array() const
Definition: json.h:61
unicode.h
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
clinit_wrapper_name
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
Definition: java_static_initializers.cpp:65
class_identifier.h
Extract class identifier.
get_type
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.
Definition: assignments_from_json.cpp:115
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
allocate_objectst
Definition: allocate_objects.h:31
allocate_objectst::allocate_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...
Definition: allocate_objects.cpp:171
has_id
static bool has_id(const jsont &json)
Return true iff the argument has a "@id" key.
Definition: assignments_from_json.cpp:131
get_untyped_primitive
static jsont get_untyped_primitive(const jsont &json)
get_untyped for primitive types.
Definition: assignments_from_json.cpp:210
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
is_primitive_wrapper_type_id
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:115
allocate_objectst::allocate_automatic_local_object
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
Definition: allocate_objects.cpp:70
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
java_utils.h
allocate_objects.h
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
assign_from_json
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...
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:68
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656
json_stringt
Definition: json.h:270
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:38