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
64
66followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
67{
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
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,
272 const symbol_table_baset &symbol_table)
273{
274 const auto type_from_json = get_type(json);
276 return {}; // no runtime type specified, use compile-time type
277 const auto runtime_type = [&]() -> std::string {
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 =
292}
293
307 const jsont &json,
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,
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 {
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 {
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,
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 =
401 member_exprt{dereference_exprt{expr}, "data", data_component.type()},
402 pointer_type(element_type));
403
405 info.allocate_objects.allocate_automatic_local_object(
406 data_member_expr.type(), "user_specified_array_data_init");
409
410 size_t index = 0;
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 {
418 result.append(
420 }
421 return result;
422}
423
429static std::pair<symbol_exprt, code_with_references_listt>
431{
433 java_int_type(), "user_specified_array_length");
435 code.add(
439 return std::make_pair(length_expr, std::move(code));
440}
441
453static std::pair<code_with_references_listt, exprt>
470
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{
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(
546 }
547 else // component is class field (pointer to struct)
548 {
549 const auto member_json = [&]() -> jsont {
550 if(
552 id2string(component_name) == "value")
553 {
555 }
556 return json[id2string(component_name)];
557 }();
559 }
560 }
561 return result;
562}
563
569 const exprt &expr,
570 const jsont &json,
572{
573 const namespacet ns{info.symbol_table};
575 to_java_class_type(ns.follow(expr.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());
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{
604 info.allocate_objects.allocate_dynamic_object(
605 output_code, expr, to_pointer_type(expr.type()).base_type());
606 for(codet &code : output_code.statements())
607 result.add(std::move(code));
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
635 return result;
636 }
637
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()));
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,
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
671}
672
679 const exprt &expr,
680 const jsont &json,
683{
684 const auto &pointer_type = to_pointer_type(expr.type());
688 {
689 const auto &new_symbol =
690 info.allocate_objects.allocate_automatic_local_object(
691 replacement_pointer_type, "user_specified_subtype_symbol");
692 if(info.needed_lazy_methods)
693 {
694 info.needed_lazy_methods->add_all_needed_classes(
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 {
746 reference.expr = info.allocate_objects.allocate_automatic_local_object(
747 pointer_type, "user_specified_array_ref");
748 reference.array_length =
749 info.allocate_objects.allocate_automatic_local_object(
750 java_int_type(), "user_specified_array_length");
751 code.add(reference_allocationt{id, info.loc});
752 }
753 else
754 {
755 code_blockt block;
756 reference.expr = info.allocate_objects.allocate_dynamic_object_symbol(
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,
793{
794 const std::string &id = has_enum_type(expr, info.symbol_table)
795 ? get_enum_id(expr, json, info.symbol_table)
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,
815 info));
816 }
817 else
818 {
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,
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 {
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));
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);
929 symbol_table,
930 needed_lazy_methods,
931 references,
932 location,
933 max_user_array_length,
934 class_type};
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 });
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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
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: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
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
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
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