#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/class_identifier.h>#include <goto-programs/goto_instruction_code.h>#include <ansi-c/allocate_objects.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:Go to the source code of this file.
Classes | |
| struct | object_creation_infot |
| Values passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json. More... | |
| struct | get_or_create_reference_resultt |
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. | |
| 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. | |
| static bool | has_id (const jsont &json) |
| Return true iff the argument has a "@id" key. | |
| static bool | is_reference (const jsont &json) |
| Return true iff the argument has a "@ref" 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 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 | has_nondet_length (const jsont &json) |
Return true iff the argument has a "@nondetLength" entry. | |
| 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. | |
| static jsont | get_untyped_primitive (const jsont &json) |
| get_untyped for primitive types. | |
| static json_arrayt | get_untyped_array (const jsont &json, const typet &element_type) |
| get_untyped for array types. | |
| static jsont | get_untyped_string (const jsont &json) |
| get_untyped for string types. | |
| 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. | |
| 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 '['. | |
| code_with_references_listt | assign_from_json_rec (const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info) |
| Entry point of the recursive deterministic assignment algorithm. | |
| 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 code_frontend_assignt | assign_null (const exprt &expr) |
| One of the base cases of the recursive algorithm. | |
| static code_with_references_listt | assign_array_data_component_from_json (const exprt &expr, const jsont &json, const std::optional< 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 component of the array, which contains the array elements. | |
| static std::pair< symbol_exprt, code_with_references_listt > | nondet_length (allocate_objectst &allocate, source_locationt loc) |
| Declare a non-deterministic length expression. | |
| static std::pair< code_with_references_listt, exprt > | assign_det_length_array_from_json (const exprt &expr, const jsont &json, const std::optional< 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 flagged with @nondetLength. | |
| static code_with_references_listt | assign_nondet_length_array_from_json (const exprt &array, const jsont &json, const exprt &given_length_expr, const std::optional< 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 with @nondetLength. | |
| 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_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 the Java object represented by expr (the components of its type and all of its parent 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 dereferencing a pointer that corresponds to the Java object described in json. | |
| 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 an enum constant that is referenced outside of the definition of its type. | |
| 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, whose type is the same as the runtime-type of the corresponding Java object. | |
| 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, and runtime_type is the runtime type of the corresponding Java object, which may be more specific than the type pointed to by expr.type() (the compile-time type of the object). | |
| 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_reference_from_json (const exprt &expr, const jsont &json, const std::optional< 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 reference-equal to one or more other Java objects represented in the initial JSON file. | |
| code_with_references_listt | assign_from_json (const exprt &expr, const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< 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 the value of a Java object or primitive of a compatible type, adds statements to block to assign expr to the deterministic value specified by json. | |
|
static |
In the case of an assignment of an array given a JSON representation, this function assigns the data component of the array, which contains the array elements.
expr is a pointer to the array containing the component.
Definition at line 392 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where expr represents an array which is not flagged with @nondetLength.
The length of the array is given by symbol given_length_expr. We assume that an array with this symbol as its length has already been allocated and that expr has been assigned to it. We constraint the length of the array to be the number of elements, which is known and constant. For the assignment of the array elements, see assign_array_data_component_from_json. For the overall algorithm, see assign_from_json_rec.
Definition at line 457 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where the expression to be assigned a value is an enum constant that is referenced outside of the definition of its type.
(See is_enum_with_type_equal_to_declaring_type for this temporary distinction. See assign_from_json for details about the recursion.) Once reference-equality of fields in different classes is supported, this function can be removed.
Definition at line 623 of file assignments_from_json.cpp.
| code_with_references_listt assign_from_json | ( | const exprt & | expr, |
| const jsont & | json, | ||
| const irep_idt & | function_id, | ||
| symbol_table_baset & | symbol_table, | ||
| std::optional< 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 the value of a Java object or primitive of a compatible type, adds statements to block to assign expr to the deterministic value specified by json.
The expected format of the JSON representation is mostly the same as that of the json-io serialization library (https://github.com/jdereg/json-io) if run with the following options, as of version 4.10.1:
("java.lang.Boolean", "java.lang.Boolean") for all primitive wrapper types, java.lang.Class, java.lang.String and java.util.Date. That is, we are not using the json-io default shorthands for those types.WRITE_LONGS_AS_STRINGS should be set to true to avoid a loss of precision when representing longs.Some examples of json-io representations that may not be obvious include:
"@type" key. The value corresponding to such a key specifies the runtime type of the object (or the boxed type if the object is primitive). If no "@type" key is present, it is assumed that the runtime type is the same as the compile-time type. Most reference-typed objects are represented as JSON objects (i.e. key-value maps) either way, so the "@type" key is just an additional key in the map. However, primitive types, arrays and string types without a "@type" key are not represented as JSON objects. For example, "untyped" ints are just represented as e.g. 1234, i.e. a JSON number. The "typed" version of this int then becomes {"@type":"java.lang.Integer","value":1234}, i.e. a JSON object, with the original ("untyped") JSON number stored in the "value" entry. For arrays, the corresponding key is called "@items", not "value". Typed versions of primitive types are probably not necessary, but json-io will sometimes produce such values, which is why we support both typed and untyped versions.{"@id": some_ID} entry, in addition to its usual representation. All the other objects with this ID are represented simply as {"@ref": some_ID}, with no further entries.The above rule has the following exceptions:
@type key. For cases where we don't know that an expression has a string type (e.g. if its type is generic and specialized to java.lang.String), we need to sometimes represent strings as JSON objects with a @type key. In this case, the content of the string will be the value associated with a value key (similarly to StringBuilder in json-io). See get_untyped_string.ordinal field of enums in its representation, but our algorithm depends on it being present. It may be possible to rewrite parts of it to set the ordinal depending on the order of elements seen in the $VALUES array, but it would generally make things more complicated.For examples of JSON representations of objects, see the regression tests for this feature in jbmc/regression/jbmc/deterministic_assignments_json.
Known limitations:
{"@ref":1} or similar will generally either point to a freshly allocated symbol or an out-of-scope symbol. The {"@id":1} (or similar) object may be assigned correctly, or it may point to an out-of-scope symbol. This is because the symbol for the shared value is currently allocated dynamically. To fix this limitation, static allocation would have to be used instead, together with a static boolean to keep track of whether or not the symbol has been allocated already.For parameter documentation, see object_creation_infot.
Definition at line 914 of file assignments_from_json.cpp.
| code_with_references_listt assign_from_json_rec | ( | const exprt & | expr, |
| const jsont & | json, | ||
| const std::optional< std::string > & | type_from_array, | ||
| object_creation_infot & | info | ||
| ) |
Entry point of the recursive deterministic assignment algorithm.
| expr | expression to assign a deterministic value to. In the case of the entry point, this is either a pointer to a struct, or an expression corresponding to a Java primitive. |
| json | a JSON representation of the deterministic value to assign. |
| type_from_array | if expr was found as an element of an array, the element type of this array. |
| info | references used throughout the recursive algorithm. |
Definition at line 850 of file assignments_from_json.cpp.
|
static |
Same as assign_pointer_from_json without special cases (enums).
Definition at line 600 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where expr represents an array which is flagged with @nondetLength.
The length of the array is given by symbol given_length_expr. We assume that an array with this symbol as its length has already been allocated and that expr has been assigned to it. We constrain the length of the array to be greater or equal to the number of elements specified in json. For the assignment of the array elements, see assign_array_data_component_from_json. For the overall algorithm, see assign_from_json_rec.
Definition at line 485 of file assignments_from_json.cpp.
|
static |
One of the base cases of the recursive algorithm.
See assign_from_json_rec.
Definition at line 383 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where expr is a pointer to a struct, whose type is the same as the runtime-type of the corresponding Java object.
See assign_from_json_rec.
Definition at line 665 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where expr is a pointer to a struct, and runtime_type is the runtime type of the corresponding Java object, which may be more specific than the type pointed to by expr.type() (the compile-time type of the object).
See assign_from_json_rec.
Definition at line 683 of file assignments_from_json.cpp.
|
static |
One of the base cases (primitive case) of the recursion.
For characters, the encoding in json is assumed to be UTF-8. See assign_from_json_rec.
Definition at line 342 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where expr corresponds to a Java object that is reference-equal to one or more other Java objects represented in the initial JSON file.
See assign_from_json_rec. Such an object will either have the key-value pair @id: some_key in json, together with a full representation of the object, or it will only have one key-value pair, @ref: some_key. For each key, there is only one @id field in the JSON file. A special case is enums, which are always represented as a full object without any @id or @ref keys. This is mostly the same as the output from json-io for enums, except that in our representation, we need to include the ordinal field so that e.g. switch statements on enums will work. We keep track of object IDs using a map from IDs to symbol expressions. Usually the ID is the some_key from the example above, except for enums, where the ID is of the form my.package.name.EnumName.CONSTANT. The first time we see an ID (@id, @ref or enum constant), we allocate a symbol for it. The first time we see the full representation of the object (@id or enum constant) we initialize the allocated memory. This strategy may need to be changed to support reference-equality of fields across several different classes (e.g. as soon as we find a @ref for the first time we might want to search the whole initial JSON file for the corresponding @id).
Definition at line 794 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where expr represents a string.
See assign_from_json_rec.
Definition at line 512 of file assignments_from_json.cpp.
|
static |
Helper function for assign_struct_from_json which recursively assigns values to all of the fields of the Java object represented by expr (the components of its type and all of its parent types).
Definition at line 528 of file assignments_from_json.cpp.
|
static |
One of the cases in the recursive algorithm: the case where expr is a struct, which is the result of dereferencing a pointer that corresponds to the Java object described in json.
See assign_from_json_rec.
Definition at line 572 of file assignments_from_json.cpp.
|
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.
| 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. |
Definition at line 307 of file assignments_from_json.cpp.
|
static |
Definition at line 68 of file assignments_from_json.cpp.
|
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.
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.
|
static |
Helper function for assign_reference_from_json.
Look up the given id in the reference map and gets or creates the symbol for it. In the case of arrays, if the first time we see an ID is in a @ref object (rather than @id), we do not know what the length of the array will be, so we need to allocate an array of nondeterministic length. The length will be constrained (in assign_nondet_length_array_from_json) once we find the corresponding @id object.
| expr | expression representing the Java object for which a symbol is retrieved or allocated. |
| id | key in the reference map for this object |
| info | references used throughout the recursive algorithm. |
Definition at line 739 of file assignments_from_json.cpp.
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.
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 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 for primitive types.
Definition at line 215 of file assignments_from_json.cpp.
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.
Definition at line 76 of file assignments_from_json.cpp.
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.
Return true iff the argument has a "@nondetLength" entry. : true
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.
|
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.
| 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. |
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.
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.
|
static |
Declare a non-deterministic length expression.
| [out] | allocate | allocation functor |
| loc | location for the created code |
Definition at line 433 of file assignments_from_json.cpp.
|
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.
| 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. |
Definition at line 270 of file assignments_from_json.cpp.
1.9.8