cprover
Loading...
Searching...
No Matches
assignments_from_json.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Assignments to values specified in JSON files
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
11#include <util/arith_tools.h>
14#include <util/ieee_float.h>
15#include <util/json.h>
17#include <util/unicode.h>
18
21
23
28#include "java_types.h"
29#include "java_utils.h"
30
36{
42
45
48 std::optional<ci_lazy_methods_neededt> &needed_lazy_methods;
49
53 std::unordered_map<std::string, object_creation_referencet> &references;
54
57
61
65};
66
68followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
69{
71 return to_java_class_type(namespacet{symbol_table}.follow_tag(
72 to_struct_tag_type(pointer_type.base_type())));
73}
74
75static bool
76has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
77{
78 return followed_class_type(expr, symbol_table).get_is_enumeration();
79}
80
106 const exprt &expr,
107 const symbol_table_baset &symbol_table,
108 const java_class_typet &declaring_class_type)
109{
111 return followed_class_type(expr, symbol_table) == declaring_class_type &&
112 declaring_class_type.get_is_enumeration();
113}
114
120static std::optional<std::string> get_type(const jsont &json)
121{
122 if(!json.is_object())
123 return {};
124 const auto &json_object = to_json_object(json);
125 if(json_object.find("@type") == json_object.end())
126 return {};
127 return json_object["@type"].value;
128}
129
136static bool has_id(const jsont &json)
137{
138 if(!json.is_object())
139 return false;
140 const auto &json_object = to_json_object(json);
141 return json_object.find("@id") != json_object.end();
142}
143
148static bool is_reference(const jsont &json)
149{
150 if(!json.is_object())
151 return false;
152 const auto &json_object = to_json_object(json);
153 return json_object.find("@ref") != json_object.end();
154}
155
159static std::string get_id_or_reference_value(const jsont &json)
160{
162 if(has_id(json))
163 return json["@id"].value;
164 return json["@ref"].value;
165}
166
171static std::string get_enum_id(
172 const exprt &expr,
173 const jsont &json,
174 const symbol_table_baset &symbol_table)
175{
176 PRECONDITION(json.is_object());
177 const auto &json_object = to_json_object(json);
178 INVARIANT(
179 json_object.find("name") != json_object.end(),
180 "JSON representation of enums should include name field");
181 return id2string(followed_class_type(expr, symbol_table).get_tag()) + '.' +
182 (json["name"].value);
183}
184
189static bool has_nondet_length(const jsont &json)
190{
191 if(!json.is_object())
192 return false;
193 const auto &json_object = to_json_object(json);
194 auto nondet_it = json_object.find("@nondetLength");
195 return nondet_it != json_object.end() && nondet_it->second.is_true();
196}
197
202static jsont get_untyped(const jsont &json, const std::string &object_key)
203{
204 if(!json.is_object())
205 return json;
206
207 const auto &json_object = to_json_object(json);
209 get_type(json) || json_object.find("@nondetLength") != json_object.end());
210
211 return json[object_key];
212}
213
216{
217 return get_untyped(json, "value");
218}
219
224static json_arrayt
225get_untyped_array(const jsont &json, const typet &element_type)
226{
227 const jsont untyped = get_untyped(json, "@items");
228 PRECONDITION(untyped.is_array());
229 const auto &json_array = to_json_array(untyped);
230 if(element_type == java_char_type())
231 {
232 PRECONDITION(json_array.size() == 1);
233 const auto &first = *json_array.begin();
234 PRECONDITION(first.is_string());
235 const auto &json_string = to_json_string(first);
236
237 const auto wide_string = utf8_to_utf16_native_endian(json_string.value);
238 auto string_range = make_range(wide_string.begin(), wide_string.end());
239 const auto json_range = string_range.map([](const wchar_t &c) {
240 const std::u16string u16(1, c);
242 });
243 return json_arrayt{json_range.begin(), json_range.end()};
244 }
245 return json_array;
246}
247
253{
254 return get_untyped(json, "value");
255}
256
270static std::optional<java_class_typet> runtime_type(
271 const jsont &json,
272 const std::optional<std::string> &type_from_array,
273 const symbol_table_baset &symbol_table)
274{
275 const auto type_from_json = get_type(json);
276 if(!type_from_json && !type_from_array)
277 return {}; // no runtime type specified, use compile-time type
278 const auto runtime_type = [&]() -> std::string {
279 if(type_from_json)
280 return "java::" + *type_from_json;
281 INVARIANT(
282 type_from_array->find('L') == 0 &&
283 type_from_array->rfind(';') == type_from_array->length() - 1,
284 "Types inferred from the type of a containing array should be of the "
285 "form Lmy.package.name.ClassName;");
286 return "java::" + type_from_array->substr(1, type_from_array->length() - 2);
287 }();
288 if(!symbol_table.has_symbol(runtime_type))
289 return {}; // Fall back to compile-time type if runtime type was not found
290 const auto &replacement_class_type =
292 return replacement_class_type;
293}
294
307static std::optional<std::string> element_type_from_array_type(
308 const jsont &json,
309 const std::optional<std::string> &type_from_array)
310{
311 if(const auto json_array_type = get_type(json))
312 {
313 INVARIANT(
314 json_array_type->find('[') == 0,
315 "Array types in the JSON input should be of the form "
316 "[[...[Lmy.package.name.ClassName; (with n occurrences of [ for an "
317 "n-dimensional array)");
318 return json_array_type->substr(1);
319 }
320 else if(type_from_array)
321 {
322 INVARIANT(
323 type_from_array->find('[') == 0,
324 "For arrays that are themselves contained by an array from which a type "
325 "is inferred, such a type should be of the form "
326 "[[...[Lmy.package.name.ClassName;");
327 return type_from_array->substr(1);
328 }
329 return {};
330}
331
333 const exprt &expr,
334 const jsont &json,
335 const std::optional<std::string> &type_from_array,
337
343{
345 if(json.is_null()) // field is not mentioned in json, leave as default value
346 return result;
347 if(expr.type() == java_boolean_type())
348 {
350 expr, json.is_true() ? (exprt)true_exprt{} : (exprt)false_exprt{}});
351 }
352 else if(
353 expr.type() == java_int_type() || expr.type() == java_byte_type() ||
354 expr.type() == java_short_type() || expr.type() == java_long_type())
355 {
357 expr, from_integer(std::stoll(json.value), expr.type())});
358 }
359 else if(expr.type() == java_double_type())
360 {
361 ieee_floatt ieee_float(to_floatbv_type(expr.type()));
362 ieee_float.from_double(std::stod(json.value));
363 result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
364 }
365 else if(expr.type() == java_float_type())
366 {
367 ieee_floatt ieee_float(to_floatbv_type(expr.type()));
368 ieee_float.from_float(std::stof(json.value));
369 result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
370 }
371 else if(expr.type() == java_char_type())
372 {
373 const std::wstring wide_value = utf8_to_utf16_native_endian(json.value);
374 PRECONDITION(wide_value.length() == 1);
376 expr, from_integer(wide_value.front(), expr.type())});
377 }
378 return result;
379}
380
384{
387}
388
393 const exprt &expr,
394 const jsont &json,
395 const std::optional<std::string> &type_from_array,
397{
398 const auto &java_class_type = followed_class_type(expr, info.symbol_table);
399 const auto &data_component = java_class_type.components()[2];
400 const auto &element_type = java_array_element_type(
402 const exprt data_member_expr = typecast_exprt::conditional_cast(
403 member_exprt{dereference_exprt{expr}, "data", data_component.type()},
404 pointer_type(element_type));
405
406 const symbol_exprt &array_init_data =
408 data_member_expr.type(), "user_specified_array_data_init");
410 result.add(
411 code_frontend_assignt{array_init_data, data_member_expr, info.loc});
412
413 size_t index = 0;
414 const std::optional<std::string> inferred_element_type =
415 element_type_from_array_type(json, type_from_array);
416 const json_arrayt json_array = get_untyped_array(json, element_type);
417 for(auto it = json_array.begin(); it < json_array.end(); it++, index++)
418 {
419 const dereference_exprt element_at_index = array_element_from_pointer(
420 array_init_data, from_integer(index, java_int_type()));
421 result.append(
422 assign_from_json_rec(element_at_index, *it, inferred_element_type, info));
423 }
424 return result;
425}
426
432static std::pair<symbol_exprt, code_with_references_listt>
434{
435 symbol_exprt length_expr = allocate.allocate_automatic_local_object(
436 java_int_type(), "user_specified_array_length");
439 length_expr, side_effect_expr_nondett{java_int_type(), loc}});
441 length_expr, ID_ge, from_integer(0, java_int_type())}});
442 return std::make_pair(length_expr, std::move(code));
443}
444
456static std::pair<code_with_references_listt, exprt>
458 const exprt &expr,
459 const jsont &json,
460 const std::optional<std::string> &type_from_array,
462{
464 const auto &element_type = java_array_element_type(
466 const json_arrayt json_array = get_untyped_array(json, element_type);
467 const auto number_of_elements =
468 from_integer(json_array.size(), java_int_type());
469 return {
470 assign_array_data_component_from_json(expr, json, type_from_array, info),
471 number_of_elements};
472}
473
486 const exprt &array,
487 const jsont &json,
488 const exprt &given_length_expr,
489 const std::optional<std::string> &type_from_array,
491{
493 const auto &element_type = java_array_element_type(
495 const json_arrayt json_array = get_untyped_array(json, element_type);
497 exprt number_of_elements = from_integer(json_array.size(), java_int_type());
499 binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements},
501 given_length_expr,
502 ID_le,
504 result.append(
505 assign_array_data_component_from_json(array, json, type_from_array, info));
506 return result;
507}
508
513 const jsont &json,
514 const exprt &expr,
516{
517 const auto json_string = get_untyped_string(json);
518 PRECONDITION(json_string.is_string());
520 expr,
522 json_string.value, info.symbol_table, true)};
523}
524
529 const exprt &expr,
530 const jsont &json,
532{
533 const java_class_typet &java_class_type = to_java_class_type(
536 for(const auto &component : java_class_type.components())
537 {
538 const irep_idt &component_name = component.get_name();
539 if(
540 component_name == JAVA_CLASS_IDENTIFIER_FIELD_NAME ||
541 component_name == "cproverMonitorCount")
542 {
543 continue;
544 }
545 member_exprt member_expr{expr, component_name, component.type()};
546 if(component_name[0] == '@') // component is parent struct type
547 {
548 result.append(
549 assign_struct_components_from_json(member_expr, json, info));
550 }
551 else // component is class field (pointer to struct)
552 {
553 const auto member_json = [&]() -> jsont {
554 if(
555 is_primitive_wrapper_type_id(java_class_type.get_name()) &&
556 id2string(component_name) == "value")
557 {
559 }
560 return json[id2string(component_name)];
561 }();
562 result.append(assign_from_json_rec(member_expr, member_json, {}, info));
563 }
564 }
565 return result;
566}
567
573 const exprt &expr,
574 const jsont &json,
576{
577 const namespacet ns{info.symbol_table};
578 const java_class_typet &java_class_type =
579 to_java_class_type(ns.follow_tag(to_struct_tag_type(expr.type())));
581 if(is_java_string_type(java_class_type))
582 {
583 result.add(assign_string_from_json(json, expr, info));
584 }
585 else
586 {
587 auto initial_object = zero_initializer(expr.type(), info.loc, ns);
588 CHECK_RETURN(initial_object.has_value());
590 to_struct_expr(*initial_object),
591 ns,
592 struct_tag_typet("java::" + id2string(java_class_type.get_tag())));
593 result.add(code_frontend_assignt{expr, *initial_object});
595 }
596 return result;
597}
598
601 const exprt &expr,
602 const jsont &json,
604{
606 code_blockt output_code;
607 exprt dereferenced_symbol_expr =
609 output_code, expr, to_pointer_type(expr.type()).base_type());
610 for(codet &code : output_code.statements())
611 result.add(std::move(code));
612 result.append(assign_struct_from_json(dereferenced_symbol_expr, json, info));
613 return result;
614}
615
624 const exprt &expr,
625 const jsont &json,
627{
628 const auto &java_class_type = followed_class_type(expr, info.symbol_table);
629 const std::string &enum_name = id2string(java_class_type.get_name());
631 if(const auto func = info.symbol_table.lookup(clinit_wrapper_name(enum_name)))
632 result.add(code_function_callt{func->symbol_expr()});
633
634 const irep_idt values_name = enum_name + ".$VALUES";
635 if(!info.symbol_table.has_symbol(values_name))
636 {
637 // Fallback: generate a new enum instance instead of getting it from $VALUES
638 result.append(assign_non_enum_pointer_from_json(expr, json, info));
639 return result;
640 }
641
642 dereference_exprt values_struct{
643 info.symbol_table.lookup_ref(values_name).symbol_expr()};
644 const namespacet ns{info.symbol_table};
645 const auto &values_struct_type =
646 ns.follow_tag(to_struct_tag_type(values_struct.type()));
647 PRECONDITION(is_valid_java_array(values_struct_type));
648 const member_exprt values_data = member_exprt{
649 values_struct, "data", values_struct_type.components()[2].type()};
650
651 const exprt ordinal_expr =
652 from_integer(std::stoi(json["ordinal"].value), java_int_type());
653
655 expr,
657 array_element_from_pointer(values_data, ordinal_expr), expr.type())});
658 return result;
659}
660
666 const exprt &expr,
667 const jsont &json,
669{
670 // This check can be removed when tracking reference-equal objects across
671 // different classes has been implemented.
672 if(has_enum_type(expr, info.symbol_table))
673 return assign_enum_from_json(expr, json, info);
674 else
675 return assign_non_enum_pointer_from_json(expr, json, info);
676}
677
684 const exprt &expr,
685 const jsont &json,
688{
689 const auto &pointer_type = to_pointer_type(expr.type());
690 pointer_typet replacement_pointer_type =
692 if(!equal_java_types(pointer_type, replacement_pointer_type))
693 {
694 const auto &new_symbol =
696 replacement_pointer_type, "user_specified_subtype_symbol");
697 if(info.needed_lazy_methods)
698 {
699 info.needed_lazy_methods->add_all_needed_classes(
700 replacement_pointer_type);
701 }
702
703 auto result = assign_pointer_from_json(new_symbol, json, info);
704 result.add(
706 return result;
707 }
708 else
709 return assign_pointer_from_json(expr, json, info);
710}
711
713{
718 std::unordered_map<std::string, object_creation_referencet>::iterator
722};
723
740 const exprt &expr,
741 const std::string &id,
743{
744 const auto &pointer_type = to_pointer_type(expr.type());
745 const auto id_it = info.references.find(id);
746 if(id_it == info.references.end())
747 {
750 if(is_java_array_type(expr.type()))
751 {
753 pointer_type, "user_specified_array_ref");
754 reference.array_length =
756 java_int_type(), "user_specified_array_length");
757 code.add(reference_allocationt{id, info.loc});
758 }
759 else
760 {
761 code_blockt block;
763 block, expr, pointer_type.base_type());
764 code.add(block);
765 }
766 auto iterator_inserted_pair = info.references.insert({id, reference});
767 return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
768 }
769 return {false, id_it, {}};
770}
771
795 const exprt &expr,
796 const jsont &json,
797 const std::optional<std::string> &type_from_array,
799{
800 const std::string &id = has_enum_type(expr, info.symbol_table)
801 ? get_enum_id(expr, json, info.symbol_table)
803 auto get_reference_result = get_or_create_reference(expr, id, info);
804 const bool is_new_id = get_reference_result.newly_allocated;
805 object_creation_referencet &reference =
806 get_reference_result.reference->second;
807 code_with_references_listt result = std::move(get_reference_result.code);
808 if(has_id(json) || (is_new_id && has_enum_type(expr, info.symbol_table)))
809 {
810 if(is_java_array_type(expr.type()))
811 {
812 INVARIANT(
813 reference.array_length, "an array reference should store its length");
815 {
817 reference.expr,
818 json,
819 *reference.array_length,
820 type_from_array,
821 info));
822 }
823 else
824 {
825 auto code_length_pair = assign_det_length_array_from_json(
826 reference.expr, json, type_from_array, info);
827 result.append(std::move(code_length_pair.first));
828 reference.array_length = std::move(code_length_pair.second);
829 }
830 }
831 else
832 {
833 result.append(
835 }
836 }
838 expr, typecast_exprt::conditional_cast(reference.expr, expr.type())});
839 return result;
840}
841
851 const exprt &expr,
852 const jsont &json,
853 const std::optional<std::string> &type_from_array,
855{
858 {
859 if(json.is_null())
860 {
861 result.add(assign_null(expr));
862 return result;
863 }
864 else if(
867 expr, info.symbol_table, info.declaring_class_type))
868 // The last condition can be replaced with
869 // has_enum_type(expr, info.symbol_table) once tracking reference-equality
870 // across different classes has been implemented.
871 {
872 return assign_reference_from_json(expr, json, type_from_array, info);
873 }
874 else if(is_java_array_type(expr.type()))
875 {
877 {
878 auto length_code_pair = nondet_length(info.allocate_objects, info.loc);
879 length_code_pair.second.add(
880 allocate_array(expr, length_code_pair.first, info.loc));
881 length_code_pair.second.append(assign_nondet_length_array_from_json(
882 expr, json, length_code_pair.first, type_from_array, info));
883 return length_code_pair.second;
884 }
885 else
886 {
888 const auto &element_type = java_array_element_type(
890 const std::size_t length = get_untyped_array(json, element_type).size();
891 result.add(allocate_array(
892 expr, from_integer(length, java_int_type()), info.loc));
894 expr, json, type_from_array, info));
895 return result;
896 }
897 }
898 else if(
899 const auto runtime_type =
900 ::runtime_type(json, type_from_array, info.symbol_table))
901 {
903 expr, json, *runtime_type, info);
904 }
905 else
906 return assign_pointer_from_json(expr, json, info);
907 }
908 else
909 result.append(
911 return result;
912}
913
915 const exprt &expr,
916 const jsont &json,
917 const irep_idt &function_id,
918 symbol_table_baset &symbol_table,
919 std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
920 size_t max_user_array_length,
921 std::unordered_map<std::string, object_creation_referencet> &references)
922{
923 source_locationt location{};
924 location.set_function(function_id);
925 allocate_objectst allocate(ID_java, location, function_id, symbol_table);
926 const symbolt *function_symbol = symbol_table.lookup(function_id);
927 INVARIANT(function_symbol, "Function must appear in symbol table");
928 const auto class_name = declaring_class(*function_symbol);
929 INVARIANT(
930 class_name,
931 "Function " + id2string(function_id) + " must be declared by a class.");
932 const auto &class_type =
933 to_java_class_type(symbol_table.lookup_ref(*class_name).type);
934 object_creation_infot info{allocate,
935 symbol_table,
936 needed_lazy_methods,
937 references,
938 location,
939 max_user_array_length,
940 class_type};
941 code_with_references_listt code_with_references =
942 assign_from_json_rec(expr, json, {}, info);
943 code_blockt assignments;
944 allocate.declare_created_symbols(assignments);
945 std::for_each(
946 assignments.statements().rbegin(),
947 assignments.statements().rend(),
948 [&](const codet &c) {
949 code_with_references.add_to_front(code_without_referencest{c});
950 });
951 return code_with_references;
952}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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 code_with_references_listt assign_array_data_component_from_json(const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
In the case of an assignment of an array given a JSON representation, this function assigns the data ...
static std::optional< java_class_typet > runtime_type(const jsont &json, const std::optional< 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 code_frontend_assignt assign_null(const exprt &expr)
One of the base cases of the recursive algorithm.
static std::pair< symbol_exprt, code_with_references_listt > nondet_length(allocate_objectst &allocate, source_locationt loc)
Declare a non-deterministic length expression.
static code_with_references_listt assign_reference_from_json(const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where expr corresponds to a Java object that is...
static java_class_typet followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
static code_with_references_listt assign_pointer_from_json(const exprt &expr, const jsont &json, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where expr is a pointer to a struct,...
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 std::optional< std::string > element_type_from_array_type(const jsont &json, const std::optional< std::string > &type_from_array)
Given a JSON representation of an array and a type inferred from the type of a containing array,...
static bool has_nondet_length(const jsont &json)
Return true iff the argument has a "@nondetLength": true entry.
static code_with_references_listt assign_nondet_length_array_from_json(const exprt &array, const jsont &json, const exprt &given_length_expr, const std::optional< std::string > &type_from_array, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where expr represents an array which is flagged...
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 std::optional< std::string > get_type(const jsont &json)
If the argument has a "@type" key, return the corresponding value, else return an empty optional.
static std::pair< code_with_references_listt, exprt > assign_det_length_array_from_json(const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where expr represents an array which is not fla...
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 code_with_references_listt assign_struct_components_from_json(const exprt &expr, const jsont &json, object_creation_infot &info)
Helper function for assign_struct_from_json which recursively assigns values to all of the fields of ...
static code_with_references_listt assign_pointer_with_given_type_from_json(const exprt &expr, const jsont &json, const java_class_typet &runtime_type, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where expr is a pointer to a struct,...
static get_or_create_reference_resultt get_or_create_reference(const exprt &expr, const std::string &id, object_creation_infot &info)
Helper function for assign_reference_from_json.
static code_with_references_listt assign_primitive_from_json(const exprt &expr, const jsont &json)
One of the base cases (primitive case) of the recursion.
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)
code_with_references_listt assign_from_json_rec(const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
Entry point of the recursive deterministic assignment algorithm.
static jsont get_untyped_string(const jsont &json)
get_untyped for string types.
static code_with_references_listt assign_struct_from_json(const exprt &expr, const jsont &json, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where expr is a struct, which is the result of ...
static code_frontend_assignt assign_string_from_json(const jsont &json, const exprt &expr, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where expr represents a string.
code_with_references_listt assign_from_json(const exprt &expr, const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< 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...
static code_with_references_listt assign_non_enum_pointer_from_json(const exprt &expr, const jsont &json, object_creation_infot &info)
Same as assign_pointer_from_json without special cases (enums).
static code_with_references_listt assign_enum_from_json(const exprt &expr, const jsont &json, object_creation_infot &info)
One of the cases in the recursive algorithm: the case where the expression to be assigned a value is ...
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:235
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:2125
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
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
A codet representing an assignment in the program.
Definition std_code.h:24
goto_instruction_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.
Operator to dereference a pointer.
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3077
constant_exprt to_expr() const
void from_float(const float f)
void from_double(const double d)
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:556
const componentst & components() const
Definition java_types.h:223
bool get_is_enumeration() const
is class an enumeration?
Definition java_types.h:403
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:2849
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
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:493
irep_idt get_tag() const
Definition std_types.h:168
Expression to hold a symbol (variable)
Definition std_expr.h:131
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.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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:3068
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
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.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
std::optional< 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:44
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()
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
signedbv_typet java_byte_type()
signedbv_typet java_short_type()
floatbv_typet java_double_type()
floatbv_typet java_float_type()
c_bool_typet java_boolean_type()
unsignedbv_typet java_char_type()
signedbv_typet java_long_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.
const java_reference_typet & to_java_reference_type(const typet &type)
Definition java_types.h:629
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:581
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
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...
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
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,...
json_stringt & to_json_string(jsont &json)
Definition json.h:454
json_objectt & to_json_object(jsont &json)
Definition json.h:442
json_arrayt & to_json_array(jsont &json)
Definition json.h:424
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
#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:97
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1900
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
std::unordered_map< std::string, object_creation_referencet >::iterator reference
symbol expression(s) for the given ID.
code_with_references_listt code
initialization code for the reference
bool newly_allocated
true if a new symbol was allocated for the given ID and false if the ID was found in the reference ma...
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.
std::optional< 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...
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.
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.
std::optional< exprt > array_length
If symbol is an array, this expression stores its length.
exprt expr
Expression for the symbol that stores the value that may be reference equal to other values.
Author: Diffblue Ltd.
std::string utf16_native_endian_to_utf8(const char16_t utf16_char)
Definition unicode.cpp:360
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:192
dstringt irep_idt