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 
20 
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 = to_java_class_type(
70  namespacet{symbol_table}.follow(pointer_type.base_type()));
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()).base_type());
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.base_type());
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 }
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...
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
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:1974
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition: std_code.h:217
A codet representing sequential composition of program statements.
Definition: std_code.h:130
code_operandst & statements()
Definition: std_code.h:138
codet representation of a function call statement.
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_base.h:29
Operator to dereference a pointer.
Definition: pointer_expr.h:648
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:2865
bool get_is_enumeration() const
is class an enumeration?
Definition: java_types.h:404
const componentst & components() const
Definition: java_types.h:224
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
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:2667
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The null pointer constant.
Definition: pointer_expr.h:723
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Allocation code which contains a reference.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
void set_function(const irep_idt &function)
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
irep_idt get_tag() const
Definition: std_types.h:168
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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:121
typet type
Type of symbol.
Definition: symbol.h:31
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
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:47
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)
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:31
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
Definition: java_types.cpp:163
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
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
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
signedbv_typet java_byte_type()
Definition: java_types.cpp:55
signedbv_typet java_short_type()
Definition: java_types.cpp:49
floatbv_typet java_double_type()
Definition: java_types.cpp:73
floatbv_typet java_float_type()
Definition: java_types.cpp:67
c_bool_typet java_boolean_type()
Definition: java_types.cpp:79
unsignedbv_typet java_char_type()
Definition: java_types.cpp:61
signedbv_typet java_long_type()
Definition: java_types.cpp:43
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
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
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:66
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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.
Author: Diffblue Ltd.
std::string utf16_native_endian_to_utf8(const char16_t utf16_char)
Definition: unicode.cpp:359
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