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"
14 #include "java_string_literals.h"
15 #include "java_types.h"
16 #include "java_utils.h"
17 
19 
20 #include <util/allocate_objects.h>
21 #include <util/arith_tools.h>
23 #include <util/expr_initializer.h>
24 #include <util/ieee_float.h>
25 #include <util/json.h>
26 #include <util/symbol_table_base.h>
27 #include <util/unicode.h>
28 
34 {
40 
43 
47 
51  std::unordered_map<std::string, object_creation_referencet> &references;
52 
55 
59 
63 };
64 
65 static java_class_typet
66 followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
67 {
69  const java_class_typet &java_class_type =
70  to_java_class_type(namespacet{symbol_table}.follow(pointer_type.subtype()));
71  return java_class_type;
72 }
73 
74 static bool
75 has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
76 {
77  return followed_class_type(expr, symbol_table).get_is_enumeration();
78 }
79 
105  const exprt &expr,
106  const symbol_table_baset &symbol_table,
107  const java_class_typet &declaring_class_type)
108 {
110  return followed_class_type(expr, symbol_table) == declaring_class_type &&
111  declaring_class_type.get_is_enumeration();
112 }
113 
120 {
121  if(!json.is_object())
122  return {};
123  const auto &json_object = to_json_object(json);
124  if(json_object.find("@type") == json_object.end())
125  return {};
126  return json_object["@type"].value;
127 }
128 
135 static bool has_id(const jsont &json)
136 {
137  if(!json.is_object())
138  return false;
139  const auto &json_object = to_json_object(json);
140  return json_object.find("@id") != json_object.end();
141 }
142 
147 static bool is_reference(const jsont &json)
148 {
149  if(!json.is_object())
150  return false;
151  const auto &json_object = to_json_object(json);
152  return json_object.find("@ref") != json_object.end();
153 }
154 
158 static std::string get_id_or_reference_value(const jsont &json)
159 {
161  if(has_id(json))
162  return json["@id"].value;
163  return json["@ref"].value;
164 }
165 
170 static std::string get_enum_id(
171  const exprt &expr,
172  const jsont &json,
173  const symbol_table_baset &symbol_table)
174 {
175  PRECONDITION(json.is_object());
176  const auto &json_object = to_json_object(json);
177  INVARIANT(
178  json_object.find("name") != json_object.end(),
179  "JSON representation of enums should include name field");
180  return id2string(followed_class_type(expr, symbol_table).get_tag()) + '.' +
181  (json["name"].value);
182 }
183 
188 static bool has_nondet_length(const jsont &json)
189 {
190  if(!json.is_object())
191  return false;
192  const auto &json_object = to_json_object(json);
193  auto nondet_it = json_object.find("@nondetLength");
194  return nondet_it != json_object.end() && nondet_it->second.is_true();
195 }
196 
201 static jsont get_untyped(const jsont &json, const std::string &object_key)
202 {
203  if(!json.is_object())
204  return json;
205 
206  const auto &json_object = to_json_object(json);
207  PRECONDITION(
208  get_type(json) || json_object.find("@nondetLength") != json_object.end());
209 
210  return json[object_key];
211 }
212 
215 {
216  return get_untyped(json, "value");
217 }
218 
223 static json_arrayt
224 get_untyped_array(const jsont &json, const typet &element_type)
225 {
226  const jsont untyped = get_untyped(json, "@items");
227  PRECONDITION(untyped.is_array());
228  const auto &json_array = to_json_array(untyped);
229  if(element_type == java_char_type())
230  {
231  PRECONDITION(json_array.size() == 1);
232  const auto &first = *json_array.begin();
233  PRECONDITION(first.is_string());
234  const auto &json_string = to_json_string(first);
235 
236  const auto wide_string = utf8_to_utf16_native_endian(json_string.value);
237  auto string_range = make_range(wide_string.begin(), wide_string.end());
238  const auto json_range = string_range.map([](const wchar_t &c) {
239  const std::u16string u16(1, c);
241  });
242  return json_arrayt{json_range.begin(), json_range.end()};
243  }
244  return json_array;
245 }
246 
252 {
253  return get_untyped(json, "value");
254 }
255 
270  const jsont &json,
271  const optionalt<std::string> &type_from_array,
272  const symbol_table_baset &symbol_table)
273 {
274  const auto type_from_json = get_type(json);
275  if(!type_from_json && !type_from_array)
276  return {}; // no runtime type specified, use compile-time type
277  const auto runtime_type = [&]() -> std::string {
278  if(type_from_json)
279  return "java::" + *type_from_json;
280  INVARIANT(
281  type_from_array->find('L') == 0 &&
282  type_from_array->rfind(';') == type_from_array->length() - 1,
283  "Types inferred from the type of a containing array should be of the "
284  "form Lmy.package.name.ClassName;");
285  return "java::" + type_from_array->substr(1, type_from_array->length() - 2);
286  }();
287  if(!symbol_table.has_symbol(runtime_type))
288  return {}; // Fall back to compile-time type if runtime type was not found
289  const auto &replacement_class_type =
291  return replacement_class_type;
292 }
293 
307  const jsont &json,
308  const optionalt<std::string> &type_from_array)
309 {
310  if(const auto json_array_type = get_type(json))
311  {
312  INVARIANT(
313  json_array_type->find('[') == 0,
314  "Array types in the JSON input should be of the form "
315  "[[...[Lmy.package.name.ClassName; (with n occurrences of [ for an "
316  "n-dimensional array)");
317  return json_array_type->substr(1);
318  }
319  else if(type_from_array)
320  {
321  INVARIANT(
322  type_from_array->find('[') == 0,
323  "For arrays that are themselves contained by an array from which a type "
324  "is inferred, such a type should be of the form "
325  "[[...[Lmy.package.name.ClassName;");
326  return type_from_array->substr(1);
327  }
328  return {};
329 }
330 
331 code_with_references_listt assign_from_json_rec(
332  const exprt &expr,
333  const jsont &json,
334  const optionalt<std::string> &type_from_array,
335  object_creation_infot &info);
336 
341 assign_primitive_from_json(const exprt &expr, const jsont &json)
342 {
344  if(json.is_null()) // field is not mentioned in json, leave as default value
345  return result;
346  if(expr.type() == java_boolean_type())
347  {
348  result.add(code_assignt{
349  expr, json.is_true() ? (exprt)true_exprt{} : (exprt)false_exprt{}});
350  }
351  else if(
352  expr.type() == java_int_type() || expr.type() == java_byte_type() ||
353  expr.type() == java_short_type() || expr.type() == java_long_type())
354  {
355  result.add(
356  code_assignt{expr, from_integer(std::stoll(json.value), expr.type())});
357  }
358  else if(expr.type() == java_double_type())
359  {
360  ieee_floatt ieee_float(to_floatbv_type(expr.type()));
361  ieee_float.from_double(std::stod(json.value));
362  result.add(code_assignt{expr, ieee_float.to_expr()});
363  }
364  else if(expr.type() == java_float_type())
365  {
366  ieee_floatt ieee_float(to_floatbv_type(expr.type()));
367  ieee_float.from_float(std::stof(json.value));
368  result.add(code_assignt{expr, ieee_float.to_expr()});
369  }
370  else if(expr.type() == java_char_type())
371  {
372  const std::wstring wide_value = utf8_to_utf16_native_endian(json.value);
373  PRECONDITION(wide_value.length() == 1);
374  result.add(
375  code_assignt{expr, from_integer(wide_value.front(), expr.type())});
376  }
377  return result;
378 }
379 
382 static code_assignt assign_null(const exprt &expr)
383 {
384  return code_assignt{expr, null_pointer_exprt{to_pointer_type(expr.type())}};
385 }
386 
390 static code_with_references_listt assign_array_data_component_from_json(
391  const exprt &expr,
392  const jsont &json,
393  const optionalt<std::string> &type_from_array,
394  object_creation_infot &info)
395 {
396  const auto &java_class_type = followed_class_type(expr, info.symbol_table);
397  const auto &data_component = java_class_type.components()[2];
398  const auto &element_type =
400  const exprt data_member_expr = typecast_exprt::conditional_cast(
401  member_exprt{dereference_exprt{expr}, "data", data_component.type()},
402  pointer_type(element_type));
403 
404  const symbol_exprt &array_init_data =
406  data_member_expr.type(), "user_specified_array_data_init");
408  result.add(code_assignt{array_init_data, data_member_expr, info.loc});
409 
410  size_t index = 0;
411  const optionalt<std::string> inferred_element_type =
412  element_type_from_array_type(json, type_from_array);
413  const json_arrayt json_array = get_untyped_array(json, element_type);
414  for(auto it = json_array.begin(); it < json_array.end(); it++, index++)
415  {
416  const dereference_exprt element_at_index = array_element_from_pointer(
417  array_init_data, from_integer(index, java_int_type()));
418  result.append(
419  assign_from_json_rec(element_at_index, *it, inferred_element_type, info));
420  }
421  return result;
422 }
423 
429 static std::pair<symbol_exprt, code_with_references_listt>
430 nondet_length(allocate_objectst &allocate, source_locationt loc)
431 {
432  symbol_exprt length_expr = allocate.allocate_automatic_local_object(
433  java_int_type(), "user_specified_array_length");
435  code.add(
436  code_assignt{length_expr, side_effect_expr_nondett{java_int_type(), loc}});
438  length_expr, ID_ge, from_integer(0, java_int_type())}});
439  return std::make_pair(length_expr, std::move(code));
440 }
441 
453 static std::pair<code_with_references_listt, exprt>
454 assign_det_length_array_from_json(
455  const exprt &expr,
456  const jsont &json,
457  const optionalt<std::string> &type_from_array,
458  object_creation_infot &info)
459 {
461  const auto &element_type =
463  const json_arrayt json_array = get_untyped_array(json, element_type);
464  const auto number_of_elements =
465  from_integer(json_array.size(), java_int_type());
466  return {
467  assign_array_data_component_from_json(expr, json, type_from_array, info),
468  number_of_elements};
469 }
470 
482 static code_with_references_listt assign_nondet_length_array_from_json(
483  const exprt &array,
484  const jsont &json,
485  const exprt &given_length_expr,
486  const optionalt<std::string> &type_from_array,
487  object_creation_infot &info)
488 {
490  const auto &element_type =
492  const json_arrayt json_array = get_untyped_array(json, element_type);
494  exprt number_of_elements = from_integer(json_array.size(), java_int_type());
495  result.add(code_assumet{and_exprt{
496  binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements},
498  given_length_expr,
499  ID_le,
501  result.append(
502  assign_array_data_component_from_json(array, json, type_from_array, info));
503  return result;
504 }
505 
509 static code_assignt assign_string_from_json(
510  const jsont &json,
511  const exprt &expr,
512  object_creation_infot &info)
513 {
514  const auto json_string = get_untyped_string(json);
515  PRECONDITION(json_string.is_string());
516  return code_assignt{expr,
518  json_string.value, info.symbol_table, true)};
519 }
520 
524 static code_with_references_listt assign_struct_components_from_json(
525  const exprt &expr,
526  const jsont &json,
527  object_creation_infot &info)
528 {
529  const java_class_typet &java_class_type =
530  to_java_class_type(namespacet{info.symbol_table}.follow(expr.type()));
532  for(const auto &component : java_class_type.components())
533  {
534  const irep_idt &component_name = component.get_name();
535  if(
536  component_name == JAVA_CLASS_IDENTIFIER_FIELD_NAME ||
537  component_name == "cproverMonitorCount")
538  {
539  continue;
540  }
541  member_exprt member_expr{expr, component_name, component.type()};
542  if(component_name[0] == '@') // component is parent struct type
543  {
544  result.append(
545  assign_struct_components_from_json(member_expr, json, info));
546  }
547  else // component is class field (pointer to struct)
548  {
549  const auto member_json = [&]() -> jsont {
550  if(
551  is_primitive_wrapper_type_id(java_class_type.get_name()) &&
552  id2string(component_name) == "value")
553  {
554  return get_untyped_primitive(json);
555  }
556  return json[id2string(component_name)];
557  }();
558  result.append(assign_from_json_rec(member_expr, member_json, {}, info));
559  }
560  }
561  return result;
562 }
563 
568 static code_with_references_listt assign_struct_from_json(
569  const exprt &expr,
570  const jsont &json,
571  object_creation_infot &info)
572 {
573  const namespacet ns{info.symbol_table};
574  const java_class_typet &java_class_type =
575  to_java_class_type(ns.follow(expr.type()));
577  if(is_java_string_type(java_class_type))
578  {
579  result.add(assign_string_from_json(json, expr, info));
580  }
581  else
582  {
583  auto initial_object = zero_initializer(expr.type(), info.loc, ns);
584  CHECK_RETURN(initial_object.has_value());
586  to_struct_expr(*initial_object),
587  ns,
588  struct_tag_typet("java::" + id2string(java_class_type.get_tag())));
589  result.add(code_assignt{expr, *initial_object});
590  result.append(assign_struct_components_from_json(expr, json, info));
591  }
592  return result;
593 }
594 
596 static code_with_references_listt assign_non_enum_pointer_from_json(
597  const exprt &expr,
598  const jsont &json,
599  object_creation_infot &info)
600 {
602  code_blockt output_code;
603  exprt dereferenced_symbol_expr =
605  output_code, expr, to_pointer_type(expr.type()).subtype());
606  for(codet &code : output_code.statements())
607  result.add(std::move(code));
608  result.append(assign_struct_from_json(dereferenced_symbol_expr, json, info));
609  return result;
610 }
611 
619 static code_with_references_listt assign_enum_from_json(
620  const exprt &expr,
621  const jsont &json,
622  object_creation_infot &info)
623 {
624  const auto &java_class_type = followed_class_type(expr, info.symbol_table);
625  const std::string &enum_name = id2string(java_class_type.get_name());
627  if(const auto func = info.symbol_table.lookup(clinit_wrapper_name(enum_name)))
628  result.add(code_function_callt{func->symbol_expr()});
629 
630  const irep_idt values_name = enum_name + ".$VALUES";
631  if(!info.symbol_table.has_symbol(values_name))
632  {
633  // Fallback: generate a new enum instance instead of getting it from $VALUES
634  result.append(assign_non_enum_pointer_from_json(expr, json, info));
635  return result;
636  }
637 
638  dereference_exprt values_struct{
639  info.symbol_table.lookup_ref(values_name).symbol_expr()};
640  const auto &values_struct_type =
641  to_struct_type(namespacet{info.symbol_table}.follow(values_struct.type()));
642  PRECONDITION(is_valid_java_array(values_struct_type));
643  const member_exprt values_data = member_exprt{
644  values_struct, "data", values_struct_type.components()[2].type()};
645 
646  const exprt ordinal_expr =
647  from_integer(std::stoi(json["ordinal"].value), java_int_type());
648 
649  result.add(code_assignt{
650  expr,
652  array_element_from_pointer(values_data, ordinal_expr), expr.type())});
653  return result;
654 }
655 
660 static code_with_references_listt assign_pointer_from_json(
661  const exprt &expr,
662  const jsont &json,
663  object_creation_infot &info)
664 {
665  // This check can be removed when tracking reference-equal objects across
666  // different classes has been implemented.
667  if(has_enum_type(expr, info.symbol_table))
668  return assign_enum_from_json(expr, json, info);
669  else
670  return assign_non_enum_pointer_from_json(expr, json, info);
671 }
672 
678 static code_with_references_listt assign_pointer_with_given_type_from_json(
679  const exprt &expr,
680  const jsont &json,
682  object_creation_infot &info)
683 {
684  const auto &pointer_type = to_pointer_type(expr.type());
685  pointer_typet replacement_pointer_type =
687  if(!equal_java_types(pointer_type, replacement_pointer_type))
688  {
689  const auto &new_symbol =
691  replacement_pointer_type, "user_specified_subtype_symbol");
692  if(info.needed_lazy_methods)
693  {
694  info.needed_lazy_methods->add_all_needed_classes(
695  replacement_pointer_type);
696  }
697 
698  auto result = assign_pointer_from_json(new_symbol, json, info);
699  result.add(code_assignt{expr, typecast_exprt{new_symbol, pointer_type}});
700  return result;
701  }
702  else
703  return assign_pointer_from_json(expr, json, info);
704 }
705 
706 struct get_or_create_reference_resultt
707 {
710  bool newly_allocated;
712  std::unordered_map<std::string, object_creation_referencet>::iterator
713  reference;
716 };
717 
733 static get_or_create_reference_resultt get_or_create_reference(
734  const exprt &expr,
735  const std::string &id,
736  object_creation_infot &info)
737 {
738  const auto &pointer_type = to_pointer_type(expr.type());
739  const auto id_it = info.references.find(id);
740  if(id_it == info.references.end())
741  {
743  object_creation_referencet reference;
744  if(is_java_array_type(expr.type()))
745  {
747  pointer_type, "user_specified_array_ref");
748  reference.array_length =
750  java_int_type(), "user_specified_array_length");
751  code.add(reference_allocationt{id, info.loc});
752  }
753  else
754  {
755  code_blockt block;
757  block, expr, pointer_type.subtype());
758  code.add(block);
759  }
760  auto iterator_inserted_pair = info.references.insert({id, reference});
761  return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
762  }
763  return {false, id_it, {}};
764 }
765 
788 static code_with_references_listt assign_reference_from_json(
789  const exprt &expr,
790  const jsont &json,
791  const optionalt<std::string> &type_from_array,
792  object_creation_infot &info)
793 {
794  const std::string &id = has_enum_type(expr, info.symbol_table)
795  ? get_enum_id(expr, json, info.symbol_table)
797  auto get_reference_result = get_or_create_reference(expr, id, info);
798  const bool is_new_id = get_reference_result.newly_allocated;
799  object_creation_referencet &reference =
800  get_reference_result.reference->second;
801  code_with_references_listt result = std::move(get_reference_result.code);
802  if(has_id(json) || (is_new_id && has_enum_type(expr, info.symbol_table)))
803  {
804  if(is_java_array_type(expr.type()))
805  {
806  INVARIANT(
807  reference.array_length, "an array reference should store its length");
809  {
810  result.append(assign_nondet_length_array_from_json(
811  reference.expr,
812  json,
813  *reference.array_length,
814  type_from_array,
815  info));
816  }
817  else
818  {
819  auto code_length_pair = assign_det_length_array_from_json(
820  reference.expr, json, type_from_array, info);
821  result.append(std::move(code_length_pair.first));
822  reference.array_length = std::move(code_length_pair.second);
823  }
824  }
825  else
826  {
827  result.append(
828  assign_struct_from_json(dereference_exprt(reference.expr), json, info));
829  }
830  }
831  result.add(code_assignt{
832  expr, typecast_exprt::conditional_cast(reference.expr, expr.type())});
833  return result;
834 }
835 
844 code_with_references_listt assign_from_json_rec(
845  const exprt &expr,
846  const jsont &json,
847  const optionalt<std::string> &type_from_array,
848  object_creation_infot &info)
849 {
852  {
853  if(json.is_null())
854  {
855  result.add(assign_null(expr));
856  return result;
857  }
858  else if(
859  is_reference(json) || has_id(json) ||
861  expr, info.symbol_table, info.declaring_class_type))
862  // The last condition can be replaced with
863  // has_enum_type(expr, info.symbol_table) once tracking reference-equality
864  // across different classes has been implemented.
865  {
866  return assign_reference_from_json(expr, json, type_from_array, info);
867  }
868  else if(is_java_array_type(expr.type()))
869  {
871  {
872  auto length_code_pair = nondet_length(info.allocate_objects, info.loc);
873  length_code_pair.second.add(
874  allocate_array(expr, length_code_pair.first, info.loc));
875  length_code_pair.second.append(assign_nondet_length_array_from_json(
876  expr, json, length_code_pair.first, type_from_array, info));
877  return length_code_pair.second;
878  }
879  else
880  {
882  const auto &element_type =
884  const std::size_t length = get_untyped_array(json, element_type).size();
885  result.add(allocate_array(
886  expr, from_integer(length, java_int_type()), info.loc));
887  result.append(assign_array_data_component_from_json(
888  expr, json, type_from_array, info));
889  return result;
890  }
891  }
892  else if(
893  const auto runtime_type =
894  ::runtime_type(json, type_from_array, info.symbol_table))
895  {
896  return assign_pointer_with_given_type_from_json(
897  expr, json, *runtime_type, info);
898  }
899  else
900  return assign_pointer_from_json(expr, json, info);
901  }
902  else
903  result.append(
904  assign_primitive_from_json(expr, get_untyped_primitive(json)));
905  return result;
906 }
907 
909  const exprt &expr,
910  const jsont &json,
911  const irep_idt &function_id,
912  symbol_table_baset &symbol_table,
913  optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
914  size_t max_user_array_length,
915  std::unordered_map<std::string, object_creation_referencet> &references)
916 {
917  source_locationt location{};
918  location.set_function(function_id);
919  allocate_objectst allocate(ID_java, location, function_id, symbol_table);
920  const symbolt *function_symbol = symbol_table.lookup(function_id);
921  INVARIANT(function_symbol, "Function must appear in symbol table");
922  const auto class_name = declaring_class(*function_symbol);
923  INVARIANT(
924  class_name,
925  "Function " + id2string(function_id) + " must be declared by a class.");
926  const auto &class_type =
927  to_java_class_type(symbol_table.lookup_ref(*class_name).type);
928  object_creation_infot info{allocate,
929  symbol_table,
930  needed_lazy_methods,
931  references,
932  location,
933  max_user_array_length,
934  class_type};
935  code_with_references_listt code_with_references =
936  assign_from_json_rec(expr, json, {}, info);
937  code_blockt assignments;
938  allocate.declare_created_symbols(assignments);
939  std::for_each(
940  assignments.statements().rbegin(),
941  assignments.statements().rend(),
942  [&](const codet &c) {
943  code_with_references.add_to_front(code_without_referencest{c});
944  });
945  return code_with_references;
946 }
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:188
ieee_floatt
Definition: ieee_float.h:117
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:168
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
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:75
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
arith_tools.h
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:125
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
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:46
code_with_references.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
java_string_literals.h
typet
The type of an expression, extends irept.
Definition: type.h:28
java_long_type
signedbv_typet java_long_type()
Definition: java_types.cpp:43
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
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:144
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
java_class_typet::get_is_enumeration
bool get_is_enumeration() const
is class an enumeration?
Definition: java_types.h:404
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:170
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:571
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:58
and_exprt
Boolean AND.
Definition: std_expr.h:1920
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:39
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:833
exprt
Base class for all expressions.
Definition: expr.h:54
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
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:51
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
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:201
object_creation_infot::loc
const source_locationt & loc
Source location associated with the newly added codet.
Definition: assignments_from_json.cpp:54
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:80
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:62
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: pointer_expr.h:49
is_reference
static bool is_reference(const jsont &json)
Return true iff the argument has a "@ref" key.
Definition: assignments_from_json.cpp:147
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:317
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:269
java_class_typet
Definition: java_types.h:197
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:158
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:176
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
object_creation_infot
Values passed around between most functions of the recursive deterministic assignment algorithm enter...
Definition: assignments_from_json.cpp:34
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:168
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:83
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:890
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:26
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:703
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:251
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:643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:565
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
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:121
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:306
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:42
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:163
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
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:359
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:104
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:474
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
array_element_from_pointer.h
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:31
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:191
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:272
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:49
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:19
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:55
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
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:557
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:2613
java_class_typet::components
const componentst & components() const
Definition: java_types.h:224
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:224
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:73
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:66
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
ieee_float.h
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:61
jsont::is_array
bool is_array() const
Definition: json.h:61
json.h
unicode.h
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:72
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:119
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:79
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:28
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:135
get_untyped_primitive
static jsont get_untyped_primitive(const jsont &json)
get_untyped for primitive types.
Definition: assignments_from_json.cpp:214
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
java_types.h
symbol_table_base.h
Author: Diffblue Ltd.
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:108
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:1866
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
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:67
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1691
json_stringt
Definition: json.h:270
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:38