Add new JSON value assignment feature

This commit adds a new file containing a recursive algorithm which,
given an exprt and a JSON representation of a value for the exprt,
produces codet that assigns the exprt to that value.
Some helper functions in other files are also added.

Author: antlechner

jbmc/src/java_bytecode/Makefile

@@ -1,4 +1,5 @@
-SRC = bytecode_info.cpp \
+SRC = assignments_from_json.cpp \
+      bytecode_info.cpp \
       character_refine_preprocess.cpp \
       ci_lazy_methods.cpp \
       ci_lazy_methods_needed.cpp \

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -0,0 +1,119 @@
+/*******************************************************************\
+
+Module: Assignments to values specified in JSON files
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+
+#ifndef CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H
+#define CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H
+
+#include <util/std_code.h>
+
+/// Information to store when several references point to the same Java object.
+struct object_creation_referencet
+{
+  /// Expression for the symbol that stores the value that may be reference
+  /// equal to other values.
+  exprt expr;
+
+  /// If `symbol` is an array, this expression stores its length.
+  optionalt<symbol_exprt> array_length;
+};
+
+class jsont;
+class symbol_table_baset;
+class ci_lazy_methods_neededt;
+
+/// Given an expression \p expr representing a Java object or primitive and a
+/// JSON representation \p json of the value of a Java object or primitive of a
+/// compatible type, adds statements to \p block to assign \p expr to the
+/// deterministic value specified by \p 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:
+/// - A type name map with identity mappings such as
+///   `("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:
+/// - The representation of a Java object generally may or may not contain a
+///   `"@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.
+/// - The way we deal with reference-equal objects is that they all get assigned
+///   the same ID, and exactly one of them will have an `{"@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:
+/// - It seems that strings are always printed in "primitive" representation by
+///   json-io, i.e.\ they are always JSON strings, and never JSON objects with
+///   a `@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 \ref get_untyped_string.
+/// - json-io does not include the `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:
+/// - If two reference-equal objects are defined in the same function, they are
+///   correctly assigned the same value.
+///   However, the case where they are defined in two different functions is not
+///   supported. The object that is stored as a `{"@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.
+/// - The special floating-point values NaN and positive/negative infinity are
+///   not supported. Note that in json-io 4.10.1, these are printed as "null".
+///   Future versions of json-io will support these values, and this function
+///   should be consistent with that if possible.
+/// - json-io prints \\uFFFF as a single character, which is not read correctly
+///   by the JSON parser.
+/// - Not all assignments have source locations, and those that do only link to
+///   a function, not a line number.
+///
+/// For parameter documentation, see \ref det_creation_infot.
+void assign_from_json(
+  const exprt &expr,
+  const jsont &json,
+  const irep_idt &function_id,
+  code_blockt &block,
+  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);
+
+#endif // CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H

jbmc/src/java_bytecode/assignments_from_json.h

@@ -1110,7 +1110,13 @@ bool java_bytecode_languaget::convert_single_method(
         declaring_class(symbol_table.lookup_ref(function_id));
       INVARIANT(class_name, "json_clinit must be declared by a class.");
       writable_symbol.value = get_json_clinit_body(
-        *class_name, static_values_file, symbol_table, get_message_handler());
+        *class_name,
+        static_values_file,
+        symbol_table,
+        get_message_handler(),
+        needed_lazy_methods,
+        max_user_array_length,
+        references);
       break;
     }
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
 
+#include "assignments_from_json.h"
 #include "ci_lazy_methods.h"
 #include "ci_lazy_methods_needed.h"
 #include "java_class_loader.h"
@@ -227,6 +228,11 @@ class java_bytecode_languaget:public languaget
   std::unordered_set<std::string> no_load_classes;
 
   std::vector<load_extra_methodst> extra_methods;
+
+  /// Shared map to be used in all calls to \ref assign_from_json.
+  /// It tracks objects that have been specified as reference-equal in the JSON
+  /// file by mapping IDs of such objects to symbols that store their values.
+  std::unordered_map<std::string, object_creation_referencet> references;
 };
 
 std::unique_ptr<languaget> new_java_bytecode_language();

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -7,6 +7,7 @@ Author: Chris Smowton, [email protected]
 \*******************************************************************/
 
 #include "java_static_initializers.h"
+#include "assignments_from_json.h"
 #include "java_object_factory.h"
 #include "java_utils.h"
 #include <goto-programs/class_hierarchy.h>
@@ -755,7 +756,10 @@ code_blockt get_json_clinit_body(
   const irep_idt &class_id,
   const std::string &static_values_file,
   symbol_table_baset &symbol_table,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+  size_t max_user_array_length,
+  std::unordered_map<std::string, object_creation_referencet> &references)
 {
   jsont json;
   if(
@@ -792,9 +796,15 @@ code_blockt get_json_clinit_body(
         code_blockt body;
         for(const auto &value_pair : static_field_values)
         {
-          // TODO append code to `body` to assign value_pair.first to
-          // TODO value_pair.second
-          (void)value_pair;
+          assign_from_json(
+            value_pair.first,
+            value_pair.second,
+            clinit_function_name(class_id),
+            body,
+            symbol_table,
+            needed_lazy_methods,
+            max_user_array_length,
+            references);
         }
         return body;
       }

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -9,6 +9,8 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
 
+#include "assignments_from_json.h"
+#include "ci_lazy_methods_needed.h"
 #include "java_object_factory_parameters.h"
 #include "select_pointer_type.h"
 #include "synthetic_methods_map.h"
@@ -62,12 +64,21 @@ code_ifthenelset get_clinit_wrapper_body(
 ///   values are maps from static field names to values.
 /// \param symbol_table: used to look up and create new symbols
 /// \param message_handler: used to log any errors with parsing the JSON
+/// \param needed_lazy_methods: used to mark any runtime types given in the JSON
+///   file as needed
+/// \param max_user_array_length: maximum value for constant or variable length
+///   arrays. Any arrays that were specified to be of nondeterministic length in
+///   the JSON file will be limited by this value.
+/// \param references: map to keep track of reference-equal objets.
 /// \return the body of the json_clinit function as a code block.
 code_blockt get_json_clinit_body(
   const irep_idt &class_id,
   const std::string &static_values_file,
   symbol_table_baset &symbol_table,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+  size_t max_user_array_length,
+  std::unordered_map<std::string, object_creation_referencet> &references);
 
 class stub_global_initializer_factoryt
 {

jbmc/src/java_bytecode/java_static_initializers.h

@@ -183,6 +183,18 @@ irep_idt resolve_friendly_method_name(
   }
 }
 
+pointer_typet pointer_to_replacement_type(
+  const pointer_typet &given_pointer_type,
+  const java_class_typet &replacement_class_type)
+{
+  if(can_cast_type<struct_tag_typet>(given_pointer_type.subtype()))
+  {
+    struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
+    return pointer_type(struct_tag_subtype);
+  }
+  return pointer_type(replacement_class_type);
+}
+
 dereference_exprt checked_dereference(const exprt &expr)
 {
   dereference_exprt result(expr);

jbmc/src/java_bytecode/java_utils.cpp

@@ -77,6 +77,13 @@ irep_idt resolve_friendly_method_name(
   const symbol_table_baset &symbol_table,
   std::string &error);
 
+/// Given a pointer type to a Java class and a type representing a more specific
+/// Java class, return a pointer type to the more specific class with the same
+/// structure as the original pointer type.
+pointer_typet pointer_to_replacement_type(
+  const pointer_typet &given_pointer_type,
+  const java_class_typet &replacement_class_type);
+
 /// Dereference an expression and flag it for a null-pointer check
 /// \param expr: expression to dereference and check
 dereference_exprt checked_dereference(const exprt &expr);

jbmc/src/java_bytecode/java_utils.h

@@ -446,4 +446,16 @@ inline const json_objectt &to_json_object(const jsont &json)
   return static_cast<const json_objectt &>(json);
 }
 
+inline json_stringt &to_json_string(jsont &json)
+{
+  PRECONDITION(json.kind == jsont::kindt::J_STRING);
+  return static_cast<json_stringt &>(json);
+}
+
+inline const json_stringt &to_json_string(const jsont &json)
+{
+  PRECONDITION(json.kind == jsont::kindt::J_STRING);
+  return static_cast<const json_stringt &>(json);
+}
+
 #endif // CPROVER_UTIL_JSON_H