52 std::unordered_map<std::string, object_creation_referencet> &
references;
72 return java_class_type;
122 if(!
json.is_object())
125 if(json_object.find(
"@type") == json_object.end())
127 return json_object[
"@type"].value;
138 if(!
json.is_object())
141 return json_object.find(
"@id") != json_object.end();
150 if(!
json.is_object())
153 return json_object.find(
"@ref") != json_object.end();
163 return json[
"@id"].value;
164 return json[
"@ref"].value;
179 json_object.find(
"name") != json_object.end(),
180 "JSON representation of enums should include name field");
182 (
json[
"name"].value);
191 if(!
json.is_object())
194 auto nondet_it = json_object.find(
"@nondetLength");
195 return nondet_it != json_object.end() && nondet_it->second.is_true();
204 if(!
json.is_object())
209 get_type(
json) || json_object.find(
"@nondetLength") != json_object.end());
211 return json[object_key];
233 const auto &first = *json_array.begin();
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);
276 if(!type_from_json && !type_from_array)
280 return "java::" + *type_from_json;
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);
290 const auto &replacement_class_type =
292 return replacement_class_type;
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);
320 else if(type_from_array)
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);
399 const auto &data_component = java_class_type.components()[2];
408 data_member_expr.
type(),
"user_specified_array_data_init");
417 for(
auto it = json_array.
begin(); it < json_array.
end(); it++, index++)
432static std::pair<symbol_exprt, code_with_references_listt>
442 return std::make_pair(length_expr, std::move(code));
456static std::pair<code_with_references_listt, exprt>
467 const auto number_of_elements =
488 const exprt &given_length_expr,
541 component_name ==
"cproverMonitorCount")
546 if(component_name[0] ==
'@')
553 const auto member_json = [&]() ->
jsont {
607 exprt dereferenced_symbol_expr =
611 result.
add(std::move(code));
629 const std::string &enum_name =
id2string(java_class_type.get_name());
634 const irep_idt values_name = enum_name +
".$VALUES";
644 const auto &values_struct_type =
648 values_struct,
"data", values_struct_type.components()[2].
type()};
650 const exprt ordinal_expr =
693 const auto &new_symbol =
695 replacement_pointer_type,
"user_specified_subtype_symbol");
699 replacement_pointer_type);
717 std::unordered_map<std::string, object_creation_referencet>::iterator
740 const std::string &
id,
765 auto iterator_inserted_pair = info.
references.insert({id, reference});
766 return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
768 return {
false, id_it, {}};
803 const bool is_new_id = get_reference_result.newly_allocated;
805 get_reference_result.reference->second;
812 reference.
array_length,
"an array reference should store its length");
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);
878 length_code_pair.second.add(
881 expr,
json, length_code_pair.first, type_from_array, info));
882 return length_code_pair.second;
893 expr,
json, type_from_array, info));
919 size_t max_user_array_length,
920 std::unordered_map<std::string, object_creation_referencet> &references)
925 const symbolt *function_symbol = symbol_table.
lookup(function_id);
926 INVARIANT(function_symbol,
"Function must appear in symbol table");
930 "Function " +
id2string(function_id) +
" must be declared by a class.");
931 const auto &class_type =
938 max_user_array_length,
945 assignments.statements().rbegin(),
946 assignments.statements().rend(),
947 [&](
const codet &c) {
948 code_with_references.add_to_front(code_without_referencest{c});
950 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 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)
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...
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
code_operandst & statements()
A codet representing an assignment in the program.
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.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
The Boolean constant false.
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.
const componentst & components() const
bool get_is_enumeration() const
is class an enumeration?
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 ...
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.
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.
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.
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.
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)
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)
const java_class_typet & to_java_class_type(const typet &type)
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)
json_objectt & to_json_object(jsont &json)
json_arrayt & to_json_array(jsont &json)
nonstd::optional< T > optionalt
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)
#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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
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.
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.