#include "assignments_from_json.h"
#include <util/arith_tools.h>
#include <util/array_element_from_pointer.h>
#include <util/expr_initializer.h>
#include <util/ieee_float.h>
#include <util/json.h>
#include <util/symbol_table_base.h>
#include <util/unicode.h>
#include <goto-programs/allocate_objects.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_instruction_code.h>
#include "ci_lazy_methods_needed.h"
#include "code_with_references.h"
#include "java_static_initializers.h"
#include "java_string_literals.h"
#include "java_types.h"
#include "java_utils.h"

Include dependency graph for assignments_from_json.cpp:

Classes
struct	object_creation_infot
	Values passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json. More...

Functions
static java_class_typet	followed_class_type (const exprt &expr, const symbol_table_baset &symbol_table)

static bool	has_enum_type (const exprt &expr, const symbol_table_baset &symbol_table)

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 are tracked correctly. More...

static std::optional< std::string >	get_type (const jsont &json)
	If the argument has a "@type" key, return the corresponding value, else return an empty optional. More...

static bool	has_id (const jsont &json)
	Return true iff the argument has a "@id" key. More...

static bool	is_reference (const jsont &json)
	Return true iff the argument has a "@ref" key. More...

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. More...

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. More...

static bool	has_nondet_length (const jsont &json)
	Return true iff the argument has a `"@nondetLength": true` entry. More...

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 specific to their type. More...

static jsont	get_untyped_primitive (const jsont &json)
	get_untyped for primitive types. More...

static json_arrayt	get_untyped_array (const jsont &json, const typet &element_type)
	get_untyped for array types. More...

static jsont	get_untyped_string (const jsont &json)
	get_untyped for string types. More...

static std::optional< java_class_typet >	runtime_type (const jsont &json, const std::optional< 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 of a containing array, get the runtime type of the corresponding pointer expression. More...

static std::optional< std::string >	element_type_from_array_type (const jsont &json, const std::optional< std::string > &type_from_array)
	Given a JSON representation of an array and a type inferred from the type of a containing array, get the element type by removing the leading '['. More...

Function Documentation

◆ element_type_from_array_type()

static std::optional<std::string> element_type_from_array_type	(	const jsont &	json,
		const std::optional< std::string > &	type_from_array
	)

static

Given a JSON representation of an array and a type inferred from the type of a containing array, get the element type by removing the leading '['.

Types for arrays are stored in the format "[Lmy.package.name.ClassName;". In this case, the returned value would be "Lmy.package.name.ClassName;". type_from_array would only have a value if this array is stored within another array, i.e. within a ClassName[][]. Keeping track of array types in this way is necessary to assign generic arrays with no compile-time types.

Parameters

json	JSON representation of an array. If it contains a `@type` field, this takes priority over `type_from_array`.
type_from_array	may contain a type name from a containing array.

Returns: if the type of an array was given, the type of its elements.

Definition at line 307 of file assignments_from_json.cpp.

◆ followed_class_type()

static java_class_typet followed_class_type	(	const exprt &	expr,
		const symbol_table_baset &	symbol_table
	)

static

Definition at line 67 of file assignments_from_json.cpp.

◆ get_enum_id()

static std::string get_enum_id	(	const exprt &	expr,
		const jsont &	json,
		const symbol_table_baset &	symbol_table
	)

static

Return a unique ID for an enum, based on its type and name field.

This is needed for the enum workaround until reference-equality across different classes is supported. See is_enum_with_type_equal_to_declaring_type.

Definition at line 171 of file assignments_from_json.cpp.

◆ get_id_or_reference_value()

static std::string get_id_or_reference_value ( const jsont & json )

static

Return the unique ID of all objects that are reference-equal to this one.

This is the value corresponding to a "@id" or "@ref" key. See has_id and is_reference.

Definition at line 159 of file assignments_from_json.cpp.

◆ get_type()

static std::optional<std::string> get_type ( const jsont & json )

static

If the argument has a "@type" key, return the corresponding value, else return an empty optional.

A runtime type that is different from the objects compile-time type should be specified in json in this way. Type values are of the format "my.package.name.ClassName".

Definition at line 120 of file assignments_from_json.cpp.

◆ get_untyped()

static jsont get_untyped	(	const jsont &	json,
		const std::string &	object_key
	)

static

For typed versions of primitive, string or array types, looks up their untyped contents with the key specific to their type.

See the examples on assign_from_json for the terminology used here (typed vs. untyped).

Definition at line 202 of file assignments_from_json.cpp.

◆ get_untyped_array()

static json_arrayt get_untyped_array	(	const jsont &	json,
		const typet &	element_type
	)

static

get_untyped for array types.

char arrays are treated as a special case as they are represented as an array of a single String element by json-io, rather than an array of one or more char elements.

Definition at line 225 of file assignments_from_json.cpp.

◆ get_untyped_primitive()

static jsont get_untyped_primitive ( const jsont & json )

static

get_untyped for primitive types.

Definition at line 215 of file assignments_from_json.cpp.

◆ get_untyped_string()

static jsont get_untyped_string ( const jsont & json )

static

get_untyped for string types.

Note that this differs from the standard serialization of java.lang.String in json-io, but is consistent with the serialization of StringBuilder and StringBuffer.

Definition at line 252 of file assignments_from_json.cpp.

◆ has_enum_type()

static bool has_enum_type	(	const exprt &	expr,
		const symbol_table_baset &	symbol_table
	)

static

Definition at line 76 of file assignments_from_json.cpp.

◆ has_id()

static bool has_id ( const jsont & json )

static

Return true iff the argument has a "@id" key.

The presence of such a key means that there exist objects that are reference-equal to this object. The corresponding value is the unique ID of all objects that are reference- equal to this one. All other key-value pairs of json should be as usual.

Definition at line 136 of file assignments_from_json.cpp.

◆ has_nondet_length()

static bool has_nondet_length ( const jsont & json )

static

Return true iff the argument has a "@nondetLength": true entry.

If such an entry is present on a JSON representation of an array, it means that the array should be assigned a nondeterministic length, constrained to be at least the number of elements specified for this array.

Definition at line 189 of file assignments_from_json.cpp.

◆ is_enum_with_type_equal_to_declaring_type()

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
	)

static

This function is used as a workaround until reference-equal objects defined across several classes are tracked correctly.

Once reference-equality works in all cases, this function can be removed. Until then, in the case of an enum expression that needs to be assigned a value, we distinguish between two cases: 1) the declaring class of the enum expression is the same as the type of the enum expression. For example, for an enum Pet {DOG, CAT}, the declaring class of the expression Pet.DOG is Pet, and the type of the expression is also Pet. The same is true for the expressions that represent the elements of the $VALUES array of Pet, and for any user-defined Pet-typed fields in Pet.java. In this case, initialize the expression just as a regular object that has known reference-equal objects. (Corresponds to creating the enum constant in Java or referencing it directly.) See assign_reference_from_json. 2) otherwise, initialize it by indexing the $VALUES array with the given ordinal. An example of this case would be the field pet in class MyClass { Pet pet; } (its declaring class is MyClass and its own type is Pet). See assign_enum_from_json.

Parameters

expr	an expression representing a Java object.
symbol_table	used for looking up the type of `expr`.
declaring_class_type	type of the class where `expr` is declared.

Returns: true if expr has an enum type and is declared within the definition of that same type, false otherwise.

Definition at line 105 of file assignments_from_json.cpp.

◆ is_reference()

static bool is_reference ( const jsont & json )

static

Return true iff the argument has a "@ref" key.

The corresponding value is the unique ID of all objects that are reference- equal to this one. Any other key-value pairs of json will be ignored.

Definition at line 148 of file assignments_from_json.cpp.

◆ runtime_type()

static std::optional<java_class_typet> runtime_type	(	const jsont &	json,
		const std::optional< std::string > &	type_from_array,
		const symbol_table_baset &	symbol_table
	)

static

Given a JSON representation of a (non-array) reference-typed object and a type inferred from the type of a containing array, get the runtime type of the corresponding pointer expression.

Parameters

json	JSON representation of a non-array object. If it contains a `@type` field, this takes priority over `type_from_array`. Types for non- array objects are stored in the JSON in the format "my.package.name.ClassName".
type_from_array	may contain an element type name given by a containing array. Such types are stored in the form "Lmy.package.name.ClassName;".
symbol_table	used to look up the type given its name.

Returns: runtime type of the object, if specified by at least one of the parameters.

Definition at line 270 of file assignments_from_json.cpp.

Classes

Functions

Function Documentation

◆ element_type_from_array_type()

◆ followed_class_type()

◆ get_enum_id()

◆ get_id_or_reference_value()

◆ get_type()

◆ get_untyped()

◆ get_untyped_array()

◆ get_untyped_primitive()

◆ get_untyped_string()

◆ has_enum_type()

◆ has_id()

◆ has_nondet_length()

◆ is_enum_with_type_equal_to_declaring_type()

◆ is_reference()

◆ runtime_type()