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
22
27#include "java_types.h"
28#include "java_utils.h"
29
65
67followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
68{
71 namespacet{symbol_table}.follow(pointer_type.base_type()));
72 return java_class_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
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
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
271 const jsont &json,
273 const symbol_table_baset &symbol_table)
274{
275 const auto type_from_json = get_type(json);
277 return {}; // no runtime type specified, use compile-time type
278 const auto runtime_type = [&]() -> std::string {
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 =
291 to_java_class_type(symbol_table.lookup_ref(runtime_type).type);
293}
294
308 const jsont &json,
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,
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 {
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 {
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,
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(
401 to_struct_tag_type(to_pointer_type(expr.type()).base_type()));
403 member_exprt{dereference_exprt{expr}, "data", data_component.type()},
404 pointer_type(element_type));
405
407 info.allocate_objects.allocate_automatic_local_object(
408 data_member_expr.type(), "user_specified_array_data_init");
410 result.add(
412
413 size_t index = 0;
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 {
421 result.append(
423 }
424 return result;
425}
426
432static std::pair<symbol_exprt, code_with_references_listt>
434{
436 java_int_type(), "user_specified_array_length");
442 return std::make_pair(length_expr, std::move(code));
443}
444
456static std::pair<code_with_references_listt, exprt>
473
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{
534 to_java_class_type(namespacet{info.symbol_table}.follow(expr.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(
550 }
551 else // component is class field (pointer to struct)
552 {
553 const auto member_json = [&]() -> jsont {
554 if(
556 id2string(component_name) == "value")
557 {
559 }
560 return json[id2string(component_name)];
561 }();
563 }
564 }
565 return result;
566}
567
573 const exprt &expr,
574 const jsont &json,
576{
577 const namespacet ns{info.symbol_table};
579 to_java_class_type(ns.follow(expr.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());
591 ns,
592 struct_tag_typet("java::" + id2string(java_class_type.get_tag())));
595 }
596 return result;
597}
598
601 const exprt &expr,
602 const jsont &json,
604{
608 info.allocate_objects.allocate_dynamic_object(
609 output_code, expr, to_pointer_type(expr.type()).base_type());
610 for(codet &code : output_code.statements())
611 result.add(std::move(code));
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
639 return result;
640 }
641
643 info.symbol_table.lookup_ref(values_name).symbol_expr()};
644 const auto &values_struct_type =
645 to_struct_type(namespacet{info.symbol_table}.follow(values_struct.type()));
648 values_struct, "data", values_struct_type.components()[2].type()};
649
650 const exprt ordinal_expr =
651 from_integer(std::stoi(json["ordinal"].value), java_int_type());
652
654 expr,
657 return result;
658}
659
665 const exprt &expr,
666 const jsont &json,
668{
669 // This check can be removed when tracking reference-equal objects across
670 // different classes has been implemented.
671 if(has_enum_type(expr, info.symbol_table))
672 return assign_enum_from_json(expr, json, info);
673 else
675}
676
683 const exprt &expr,
684 const jsont &json,
687{
688 const auto &pointer_type = to_pointer_type(expr.type());
692 {
693 const auto &new_symbol =
694 info.allocate_objects.allocate_automatic_local_object(
695 replacement_pointer_type, "user_specified_subtype_symbol");
696 if(info.needed_lazy_methods)
697 {
698 info.needed_lazy_methods->add_all_needed_classes(
700 }
701
702 auto result = assign_pointer_from_json(new_symbol, json, info);
703 result.add(
705 return result;
706 }
707 else
708 return assign_pointer_from_json(expr, json, info);
709}
710
712{
717 std::unordered_map<std::string, object_creation_referencet>::iterator
721};
722
739 const exprt &expr,
740 const std::string &id,
742{
743 const auto &pointer_type = to_pointer_type(expr.type());
744 const auto id_it = info.references.find(id);
745 if(id_it == info.references.end())
746 {
749 if(is_java_array_type(expr.type()))
750 {
751 reference.expr = info.allocate_objects.allocate_automatic_local_object(
752 pointer_type, "user_specified_array_ref");
753 reference.array_length =
754 info.allocate_objects.allocate_automatic_local_object(
755 java_int_type(), "user_specified_array_length");
756 code.add(reference_allocationt{id, info.loc});
757 }
758 else
759 {
760 code_blockt block;
761 reference.expr = info.allocate_objects.allocate_dynamic_object_symbol(
762 block, expr, pointer_type.base_type());
763 code.add(block);
764 }
765 auto iterator_inserted_pair = info.references.insert({id, reference});
766 return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
767 }
768 return {false, id_it, {}};
769}
770
794 const exprt &expr,
795 const jsont &json,
798{
799 const std::string &id = has_enum_type(expr, info.symbol_table)
800 ? get_enum_id(expr, json, info.symbol_table)
803 const bool is_new_id = get_reference_result.newly_allocated;
804 object_creation_referencet &reference =
805 get_reference_result.reference->second;
806 code_with_references_listt result = std::move(get_reference_result.code);
807 if(has_id(json) || (is_new_id && has_enum_type(expr, info.symbol_table)))
808 {
809 if(is_java_array_type(expr.type()))
810 {
811 INVARIANT(
812 reference.array_length, "an array reference should store its length");
814 {
816 reference.expr,
817 json,
818 *reference.array_length,
820 info));
821 }
822 else
823 {
825 reference.expr, json, type_from_array, info);
826 result.append(std::move(code_length_pair.first));
827 reference.array_length = std::move(code_length_pair.second);
828 }
829 }
830 else
831 {
832 result.append(
834 }
835 }
837 expr, typecast_exprt::conditional_cast(reference.expr, expr.type())});
838 return result;
839}
840
850 const exprt &expr,
851 const jsont &json,
854{
857 {
858 if(json.is_null())
859 {
860 result.add(assign_null(expr));
861 return result;
862 }
863 else if(
866 expr, info.symbol_table, info.declaring_class_type))
867 // The last condition can be replaced with
868 // has_enum_type(expr, info.symbol_table) once tracking reference-equality
869 // across different classes has been implemented.
870 {
872 }
873 else if(is_java_array_type(expr.type()))
874 {
876 {
877 auto length_code_pair = nondet_length(info.allocate_objects, info.loc);
878 length_code_pair.second.add(
879 allocate_array(expr, length_code_pair.first, info.loc));
881 expr, json, length_code_pair.first, type_from_array, info));
882 return length_code_pair.second;
883 }
884 else
885 {
887 const auto &element_type = java_array_element_type(
888 to_struct_tag_type(to_java_reference_type(expr.type()).base_type()));
889 const std::size_t length = get_untyped_array(json, element_type).size();
890 result.add(allocate_array(
891 expr, from_integer(length, java_int_type()), info.loc));
893 expr, json, type_from_array, info));
894 return result;
895 }
896 }
897 else if(
898 const auto runtime_type =
899 ::runtime_type(json, type_from_array, info.symbol_table))
900 {
902 expr, json, *runtime_type, info);
903 }
904 else
905 return assign_pointer_from_json(expr, json, info);
906 }
907 else
908 result.append(
910 return result;
911}
912
914 const exprt &expr,
915 const jsont &json,
916 const irep_idt &function_id,
917 symbol_table_baset &symbol_table,
918 optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
919 size_t max_user_array_length,
920 std::unordered_map<std::string, object_creation_referencet> &references)
921{
922 source_locationt location{};
923 location.set_function(function_id);
924 allocate_objectst allocate(ID_java, location, function_id, symbol_table);
925 const symbolt *function_symbol = symbol_table.lookup(function_id);
926 INVARIANT(function_symbol, "Function must appear in symbol table");
927 const auto class_name = declaring_class(*function_symbol);
928 INVARIANT(
929 class_name,
930 "Function " + id2string(function_id) + " must be declared by a class.");
931 const auto &class_type =
932 to_java_class_type(symbol_table.lookup_ref(*class_name).type);
934 symbol_table,
935 needed_lazy_methods,
936 references,
937 location,
938 max_user_array_length,
939 class_type};
941 assign_from_json_rec(expr, json, {}, info);
942 code_blockt assignments;
943 allocate.declare_created_symbols(assignments);
944 std::for_each(
945 assignments.statements().rbegin(),
946 assignments.statements().rend(),
947 [&](const codet &c) {
948 code_with_references.add_to_front(code_without_referencest{c});
949 });
951}
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_frontend_assignt assign_null(const exprt &expr)
One of the base cases of the recursive algorithm.
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_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_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.
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:240
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:2071
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
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
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:3017
bool get_is_enumeration() const
is class an enumeration?
Definition java_types.h:404
Definition json.h:27
Extract member of struct or union.
Definition std_expr.h:2794
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
Expression to hold a symbol (variable)
Definition std_expr.h:113
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
The Boolean constant true.
Definition std_expr.h:3008
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
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.
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_reference_typet & to_java_reference_type(const typet &type)
Definition java_types.h:630
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
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:77
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1842
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