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
15#include "java_types.h"
16#include "java_utils.h"
17
20
21#include <util/arith_tools.h>
24#include <util/ieee_float.h>
25#include <util/json.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
66followed_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
74static bool
75has_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
135static 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
147static 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
158static 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
170static 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
188static 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
201static 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);
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
223static json_arrayt
224get_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
332 const exprt &expr,
333 const jsont &json,
334 const optionalt<std::string> &type_from_array,
336
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
382static code_assignt assign_null(const exprt &expr)
383{
385}
386
391 const exprt &expr,
392 const jsont &json,
393 const optionalt<std::string> &type_from_array,
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
429static std::pair<symbol_exprt, code_with_references_listt>
431{
432 symbol_exprt length_expr = allocate.allocate_automatic_local_object(
433 java_int_type(), "user_specified_array_length");
435 code.add(
438 length_expr, ID_ge, from_integer(0, java_int_type())}});
439 return std::make_pair(length_expr, std::move(code));
440}
441
453static std::pair<code_with_references_listt, exprt>
455 const exprt &expr,
456 const jsont &json,
457 const optionalt<std::string> &type_from_array,
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
483 const exprt &array,
484 const jsont &json,
485 const exprt &given_length_expr,
486 const optionalt<std::string> &type_from_array,
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());
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
510 const jsont &json,
511 const exprt &expr,
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
525 const exprt &expr,
526 const jsont &json,
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 {
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
569 const exprt &expr,
570 const jsont &json,
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});
591 }
592 return result;
593}
594
597 const exprt &expr,
598 const jsont &json,
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
620 const exprt &expr,
621 const jsont &json,
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
661 const exprt &expr,
662 const jsont &json,
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
679 const exprt &expr,
680 const jsont &json,
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
707{
712 std::unordered_map<std::string, object_creation_referencet>::iterator
716};
717
734 const exprt &expr,
735 const std::string &id,
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 {
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
789 const exprt &expr,
790 const jsont &json,
791 const optionalt<std::string> &type_from_array,
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 {
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(
829 }
830 }
831 result.add(code_assignt{
832 expr, typecast_exprt::conditional_cast(reference.expr, expr.type())});
833 return result;
834}
835
845 const exprt &expr,
846 const jsont &json,
847 const optionalt<std::string> &type_from_array,
849{
852 {
853 if(json.is_null())
854 {
855 result.add(assign_null(expr));
856 return result;
857 }
858 else if(
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));
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 {
897 expr, json, *runtime_type, info);
898 }
899 else
900 return assign_pointer_from_json(expr, json, info);
901 }
902 else
903 result.append(
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)
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 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 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_array_data_component_from_json(const exprt &expr, const jsont &json, const optionalt< 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 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::pair< code_with_references_listt, exprt > assign_det_length_array_from_json(const exprt &expr, const jsont &json, const optionalt< 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 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.
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...
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 optionalt< std::string > get_type(const jsont &json)
If the argument has a "@type" key, return the corresponding value, else return an empty optional.
static bool is_reference(const jsont &json)
Return true iff the argument has a "@ref" key.
static code_with_references_listt assign_reference_from_json(const exprt &expr, const jsont &json, const optionalt< 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 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_nondet_length_array_from_json(const exprt &array, const jsont &json, const exprt &given_length_expr, const optionalt< 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 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_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.
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 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 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 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 ...
code_with_references_listt assign_from_json_rec(const exprt &expr, const jsont &json, const optionalt< std::string > &type_from_array, object_creation_infot &info)
Entry point of the recursive deterministic assignment algorithm.
static code_assignt assign_null(const exprt &expr)
One of the base cases of the recursive algorithm.
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: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.
Operator to dereference a pointer.
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
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:557
const componentst & components() const
Definition java_types.h:224
bool get_is_enumeration() const
is class an enumeration?
Definition java_types.h:404
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.
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: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.
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: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()
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_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
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,...
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
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:456
json_objectt & to_json_object(jsont &json)
Definition json.h:444
json_arrayt & to_json_array(jsont &json)
Definition json.h:426
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.
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: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
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.
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: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