47 std::unordered_map<std::string, object_creation_referencet> &
references;
67 return java_class_type;
117 if(!
json.is_object())
120 if(json_object.find(
"@type") == json_object.end())
122 return json_object[
"@type"].value;
133 if(!
json.is_object())
136 return json_object.find(
"@id") != json_object.end();
145 if(!
json.is_object())
148 return json_object.find(
"@ref") != json_object.end();
158 return json[
"@id"].value;
159 return json[
"@ref"].value;
174 json_object.find(
"name") != json_object.end(),
175 "JSON representation of enums should include name field");
177 (
json[
"name"].value);
186 if(!
json.is_object())
189 auto nondet_it = json_object.find(
"@nondetLength");
190 return nondet_it != json_object.end() && nondet_it->second.is_true();
199 if(!
json.is_object())
204 get_type(
json) || json_object.find(
"@nondetLength") != json_object.end());
206 return json[object_key];
228 const auto &first = *json_array.begin();
233 auto string_range =
make_range(wide_string.begin(), wide_string.end());
234 const auto json_range = string_range.map([](
const wchar_t &c) {
235 const std::u16string u16(1, c);
271 if(!type_from_json && !type_from_array)
275 return "java::" + *type_from_json;
277 type_from_array->find(
'L') == 0 &&
278 type_from_array->rfind(
';') == type_from_array->length() - 1,
279 "Types inferred from the type of a containing array should be of the "
280 "form Lmy.package.name.ClassName;");
281 return "java::" + type_from_array->substr(1, type_from_array->length() - 2);
285 const auto &replacement_class_type =
287 return replacement_class_type;
309 json_array_type->find(
'[') == 0,
310 "Array types in the JSON input should be of the form "
311 "[[...[Lmy.package.name.ClassName; (with n occurrences of [ for an "
312 "n-dimensional array)");
313 return json_array_type->substr(1);
315 else if(type_from_array)
318 type_from_array->find(
'[') == 0,
319 "For arrays that are themselves contained by an array from which a type "
320 "is inferred, such a type should be of the form "
321 "[[...[Lmy.package.name.ClassName;");
322 return type_from_array->substr(1);
357 ieee_float.from_double(std::stod(
json.value));
363 ieee_float.from_float(std::stof(
json.value));
393 const auto &data_component = java_class_type.components()[2];
394 const auto &element_type =
402 data_member_expr.
type(),
"user_specified_array_data_init");
410 for(
auto it = json_array.
begin(); it < json_array.
end(); it++, index++)
415 assign_from_json_rec(element_at_index, *it, inferred_element_type, info));
425 static std::pair<symbol_exprt, code_with_references_listt>
435 return std::make_pair(length_expr, std::move(code));
449 static std::pair<code_with_references_listt, exprt>
450 assign_det_length_array_from_json(
457 const auto &element_type =
460 const auto number_of_elements =
463 assign_array_data_component_from_json(expr,
json, type_from_array, info),
481 const exprt &given_length_expr,
486 const auto &element_type =
498 assign_array_data_component_from_json(array,
json, type_from_array, info));
533 component_name ==
"cproverMonitorCount")
538 if(component_name[0] ==
'@')
541 assign_struct_components_from_json(member_expr,
json, info));
545 const auto member_json = [&]() ->
jsont {
554 result.
append(assign_from_json_rec(member_expr, member_json, {}, info));
575 result.
add(assign_string_from_json(
json, expr, info));
586 result.
append(assign_struct_components_from_json(expr,
json, info));
599 exprt dereferenced_symbol_expr =
603 result.
add(std::move(code));
604 result.
append(assign_struct_from_json(dereferenced_symbol_expr,
json, info));
626 const irep_idt values_name = enum_name +
".$VALUES";
630 result.
append(assign_non_enum_pointer_from_json(expr,
json, info));
636 const auto &values_struct_type =
640 values_struct,
"data", values_struct_type.components()[2].
type()};
642 const exprt ordinal_expr =
664 return assign_enum_from_json(expr,
json, info);
666 return assign_non_enum_pointer_from_json(expr,
json, info);
685 const auto &new_symbol =
687 replacement_pointer_type,
"user_specified_subtype_symbol");
691 replacement_pointer_type);
694 auto result = assign_pointer_from_json(new_symbol,
json, info);
699 return assign_pointer_from_json(expr,
json, info);
702 struct get_or_create_reference_resultt
706 bool newly_allocated;
708 std::unordered_map<std::string, object_creation_referencet>::iterator
729 static get_or_create_reference_resultt get_or_create_reference(
731 const std::string &
id,
756 auto iterator_inserted_pair = info.
references.insert({id, reference});
757 return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
759 return {
false, id_it, {}};
793 auto get_reference_result = get_or_create_reference(expr,
id, info);
794 const bool is_new_id = get_reference_result.newly_allocated;
796 get_reference_result.reference->second;
803 reference.
array_length,
"an array reference should store its length");
806 result.
append(assign_nondet_length_array_from_json(
815 auto code_length_pair = assign_det_length_array_from_json(
816 reference.
expr,
json, type_from_array, info);
817 result.
append(std::move(code_length_pair.first));
818 reference.
array_length = std::move(code_length_pair.second);
851 result.
add(assign_null(expr));
862 return assign_reference_from_json(expr,
json, type_from_array, info);
869 length_code_pair.second.add(
871 length_code_pair.second.append(assign_nondet_length_array_from_json(
872 expr,
json, length_code_pair.first, type_from_array, info));
873 return length_code_pair.second;
878 const auto &element_type =
883 result.
append(assign_array_data_component_from_json(
884 expr,
json, type_from_array, info));
892 return assign_pointer_with_given_type_from_json(
896 return assign_pointer_from_json(expr,
json, info);
910 size_t max_user_array_length,
911 std::unordered_map<std::string, object_creation_referencet> &references)
916 const symbolt *function_symbol = symbol_table.
lookup(function_id);
917 INVARIANT(function_symbol,
"Function must appear in symbol table");
921 "Function " +
id2string(function_id) +
" must be declared by a class.");
922 const auto &class_type =
929 max_user_array_length,
932 assign_from_json_rec(expr,
json, {}, info);
936 assignments.statements().rbegin(),
937 assignments.statements().rend(),
938 [&](
const codet &c) {
939 code_with_references.add_to_front(code_without_referencest{c});
941 return code_with_references;
dereference_exprt array_element_from_pointer(const exprt &pointer, const exprt &index)
Generate statement using pointer arithmetic to access the element at the given index of a pointer arr...
static java_class_typet followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
static bool has_id(const jsont &json)
Return true iff the argument has a "@id" key.
static std::string get_id_or_reference_value(const jsont &json)
Return the unique ID of all objects that are reference-equal to this one.
static bool has_nondet_length(const jsont &json)
Return true iff the argument has a "@nondetLength": true entry.
static std::string get_enum_id(const exprt &expr, const jsont &json, const symbol_table_baset &symbol_table)
Return a unique ID for an enum, based on its type and name field.
static bool is_enum_with_type_equal_to_declaring_type(const exprt &expr, const symbol_table_baset &symbol_table, const java_class_typet &declaring_class_type)
This function is used as a workaround until reference-equal objects defined across several classes ar...
static bool is_reference(const jsont &json)
Return true iff the argument has a "@ref" key.
static jsont get_untyped(const jsont &json, const std::string &object_key)
For typed versions of primitive, string or array types, looks up their untyped contents with the key ...
static jsont get_untyped_primitive(const jsont &json)
get_untyped for primitive types.
static optionalt< java_class_typet > runtime_type(const jsont &json, const optionalt< std::string > &type_from_array, const symbol_table_baset &symbol_table)
Given a JSON representation of a (non-array) reference-typed object and a type inferred from the type...
static optionalt< std::string > element_type_from_array_type(const jsont &json, const optionalt< std::string > &type_from_array)
Given a JSON representation of an array and a type inferred from the type of a containing array,...
static json_arrayt get_untyped_array(const jsont &json, const typet &element_type)
get_untyped for array types.
static bool has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
static jsont get_untyped_string(const jsont &json)
get_untyped for string types.
static optionalt< std::string > get_type(const jsont &json)
If the argument has a "@type" key, return the corresponding value, else return an empty optional.
code_with_references_listt assign_from_json(const exprt &expr, const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > &needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references)
Given an expression expr representing a Java object or primitive and a JSON representation json of th...
pointer_typet pointer_type(const typet &subtype)
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.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
code_operandst & statements()
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.
Base class for all expressions.
typet & type()
Return the type of the expression.
The Boolean constant false.
bool get_is_enumeration() const
is class an enumeration?
const componentst & components() const
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.
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Allocation code which contains a reference.
A side_effect_exprt that returns a non-deterministically chosen value.
void set_function(const irep_idt &function)
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
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)
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)
Produce code for simple implementation of String Java libraries.
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.
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.
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 java_class_typet & to_java_class_type(const typet &type)
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
bool is_primitive_wrapper_type_id(const irep_idt &id)
Returns true iff the argument is the symbol-table identifier of a Java primitive wrapper type (for ex...
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
pointer_typet pointer_to_replacement_type(const pointer_typet &given_pointer_type, const java_class_typet &replacement_class_type)
Given a pointer type to a Java class and a type representing a more specific Java class,...
json_arrayt & to_json_array(jsont &json)
json_objectt & to_json_object(jsont &json)
json_stringt & to_json_string(jsont &json)
nonstd::optional< T > optionalt
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
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.
std::string utf16_native_endian_to_utf8(const char16_t utf16_char)
std::wstring utf8_to_utf16_native_endian(const std::string &in)
Convert UTF8-encoded string to UTF-16 with architecture-native endianness.