51 std::unordered_map<std::string, object_creation_referencet> &
references;
71 return java_class_type;
121 if(!
json.is_object())
124 if(json_object.find(
"@type") == json_object.end())
126 return json_object[
"@type"].value;
137 if(!
json.is_object())
140 return json_object.find(
"@id") != json_object.end();
149 if(!
json.is_object())
152 return json_object.find(
"@ref") != json_object.end();
162 return json[
"@id"].value;
163 return json[
"@ref"].value;
178 json_object.find(
"name") != json_object.end(),
179 "JSON representation of enums should include name field");
181 (
json[
"name"].value);
190 if(!
json.is_object())
193 auto nondet_it = json_object.find(
"@nondetLength");
194 return nondet_it != json_object.end() && nondet_it->second.is_true();
203 if(!
json.is_object())
208 get_type(
json) || json_object.find(
"@nondetLength") != json_object.end());
210 return json[object_key];
232 const auto &first = *json_array.begin();
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);
275 if(!type_from_json && !type_from_array)
279 return "java::" + *type_from_json;
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);
289 const auto &replacement_class_type =
291 return replacement_class_type;
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);
319 else if(type_from_array)
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);
361 ieee_float.from_double(std::stod(
json.value));
367 ieee_float.from_float(std::stof(
json.value));
397 const auto &data_component = java_class_type.components()[2];
398 const auto &element_type =
406 data_member_expr.
type(),
"user_specified_array_data_init");
414 for(
auto it = json_array.
begin(); it < json_array.
end(); it++, index++)
419 assign_from_json_rec(element_at_index, *it, inferred_element_type, info));
429 static std::pair<symbol_exprt, code_with_references_listt>
439 return std::make_pair(length_expr, std::move(code));
453 static std::pair<code_with_references_listt, exprt>
454 assign_det_length_array_from_json(
461 const auto &element_type =
464 const auto number_of_elements =
467 assign_array_data_component_from_json(expr,
json, type_from_array, info),
485 const exprt &given_length_expr,
490 const auto &element_type =
502 assign_array_data_component_from_json(array,
json, type_from_array, info));
537 component_name ==
"cproverMonitorCount")
542 if(component_name[0] ==
'@')
545 assign_struct_components_from_json(member_expr,
json, info));
549 const auto member_json = [&]() ->
jsont {
558 result.
append(assign_from_json_rec(member_expr, member_json, {}, info));
579 result.
add(assign_string_from_json(
json, expr, info));
590 result.
append(assign_struct_components_from_json(expr,
json, info));
603 exprt dereferenced_symbol_expr =
607 result.
add(std::move(code));
608 result.
append(assign_struct_from_json(dereferenced_symbol_expr,
json, info));
630 const irep_idt values_name = enum_name +
".$VALUES";
634 result.
append(assign_non_enum_pointer_from_json(expr,
json, info));
640 const auto &values_struct_type =
644 values_struct,
"data", values_struct_type.components()[2].
type()};
646 const exprt ordinal_expr =
668 return assign_enum_from_json(expr,
json, info);
670 return assign_non_enum_pointer_from_json(expr,
json, info);
689 const auto &new_symbol =
691 replacement_pointer_type,
"user_specified_subtype_symbol");
695 replacement_pointer_type);
698 auto result = assign_pointer_from_json(new_symbol,
json, info);
703 return assign_pointer_from_json(expr,
json, info);
706 struct get_or_create_reference_resultt
710 bool newly_allocated;
712 std::unordered_map<std::string, object_creation_referencet>::iterator
733 static get_or_create_reference_resultt get_or_create_reference(
735 const std::string &
id,
760 auto iterator_inserted_pair = info.
references.insert({id, reference});
761 return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
763 return {
false, id_it, {}};
797 auto get_reference_result = get_or_create_reference(expr,
id, info);
798 const bool is_new_id = get_reference_result.newly_allocated;
800 get_reference_result.reference->second;
807 reference.
array_length,
"an array reference should store its length");
810 result.
append(assign_nondet_length_array_from_json(
819 auto code_length_pair = assign_det_length_array_from_json(
820 reference.
expr,
json, type_from_array, info);
821 result.
append(std::move(code_length_pair.first));
822 reference.
array_length = std::move(code_length_pair.second);
855 result.
add(assign_null(expr));
866 return assign_reference_from_json(expr,
json, type_from_array, info);
873 length_code_pair.second.add(
875 length_code_pair.second.append(assign_nondet_length_array_from_json(
876 expr,
json, length_code_pair.first, type_from_array, info));
877 return length_code_pair.second;
882 const auto &element_type =
887 result.
append(assign_array_data_component_from_json(
888 expr,
json, type_from_array, info));
896 return assign_pointer_with_given_type_from_json(
900 return assign_pointer_from_json(expr,
json, info);
914 size_t max_user_array_length,
915 std::unordered_map<std::string, object_creation_referencet> &references)
920 const symbolt *function_symbol = symbol_table.
lookup(function_id);
921 INVARIANT(function_symbol,
"Function must appear in symbol table");
925 "Function " +
id2string(function_id) +
" must be declared by a class.");
926 const auto &class_type =
933 max_user_array_length,
936 assign_from_json_rec(expr,
json, {}, info);
940 assignments.statements().rbegin(),
941 assignments.statements().rend(),
942 [&](
const codet &c) {
943 code_with_references.add_to_front(code_without_referencest{c});
945 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...
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...
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 ...
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.
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)
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
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.
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.