Fix primitive wrapper types in JSON value retriever

Following the format of the json-io library, the JSON input to the
value retriever does not distinguish between primitive types and their
corresponding wrapper types. A class Foo with a field fooField of type
Integer might appear as
{
  "@type":"org.cprover.Foo",
  "fooField":100
}
To support this "primitive representation", we need a special case in
the struct assignment part.

Author: antlechner

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -532,7 +532,16 @@ static void assign_struct_components_from_json(
       assign_struct_components_from_json(member_expr, json, info);
     else // component is class field (pointer to struct)
     {
-      const jsont member_json = json[id2string(component_name)];
+      const auto member_json = [&]() -> jsont {
+        if(
+          is_primitive_wrapper_type_name(id2string(
+            strip_java_namespace_prefix(java_class_type.get_name()))) &&
+          id2string(component_name) == "value")
+        {
+          return get_untyped_primitive(json);
+        }
+        return json[id2string(component_name)];
+      }();
       assign_from_json_rec(member_expr, member_json, {}, info);
     }
   }

jbmc/src/java_bytecode/java_utils.cpp

@@ -38,6 +38,20 @@ bool is_java_string_type(const struct_typet &struct_type)
          struct_type.has_component("data");
 }
 
+bool is_primitive_wrapper_type_name(const std::string &type_name)
+{
+  static const std::unordered_set<std::string> primitive_wrapper_type_names = {
+    "java.lang.Boolean",
+    "java.lang.Byte",
+    "java.lang.Character",
+    "java.lang.Double",
+    "java.lang.Float",
+    "java.lang.Integer",
+    "java.lang.Long",
+    "java.lang.Short"};
+  return primitive_wrapper_type_names.count(type_name) > 0;
+}
+
 unsigned java_local_variable_slots(const typet &t)
 {
 

jbmc/src/java_bytecode/java_utils.h

@@ -31,6 +31,10 @@ bool java_is_array_type(const typet &type);
 /// and in particular may not have length and data fields.
 bool is_java_string_type(const struct_typet &struct_type);
 
+/// Returns true iff the argument is the fully qualified name of a Java
+/// primitive wrapper type.
+bool is_primitive_wrapper_type_name(const std::string &type_name);
+
 void generate_class_stub(
   const irep_idt &class_name,
   symbol_table_baset &symbol_table,