Merge pull request #1507 from smowton/smowton/1420-fragments/factor_java_object_init

Java frontend: factor out root class initialisation

Author: smowton

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_pointer_casts.h"
 #include "java_types.h"
 #include "java_utils.h"
+#include "java_root_class.h"
 
 void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
 {
@@ -132,15 +133,7 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
   const auto &jlo_struct=to_struct_type(ns.follow(jlo_symbol));
   struct_exprt jlo_init(jlo_symbol);
   const auto &jls_struct=to_struct_type(ns.follow(string_type));
-
-  jlo_init.copy_to_operands(
-    constant_exprt(
-      "java::java.lang.String",
-      jlo_struct.components()[0].type()));
-  jlo_init.copy_to_operands(
-    from_integer(
-      0,
-      jlo_struct.components()[1].type()));
+  java_root_class_init(jlo_init, jlo_struct, false, "java::java.lang.String");
 
   // If string refinement *is* around, populate the actual
   // contents as well:

src/java_bytecode/java_root_class.cpp

@@ -8,8 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_root_class.h"
 
+#include <util/arith_tools.h>
 #include <util/symbol.h>
-#include <util/std_types.h>
 
 #include "java_types.h"
 
@@ -52,3 +52,26 @@ void java_root_class(symbolt &class_symbol)
     components.insert(components.begin(), component);
   }
 }
+
+/// Adds members for an object of the root class (usually java.lang.Object).
+/// \param jlo [out] : object to initialize
+/// \param root_type: type of the root class
+/// \param lock: lock field
+/// \param class_identifier: class identifier field
+void java_root_class_init(
+  struct_exprt &jlo,
+  const struct_typet &root_type,
+  const bool lock,
+  const irep_idt &class_identifier)
+{
+  jlo.operands().resize(root_type.components().size());
+
+  const std::size_t clsid_nb=root_type.component_number("@class_identifier");
+  const typet &clsid_type=root_type.components()[clsid_nb].type();
+  constant_exprt clsid(class_identifier, clsid_type);
+  jlo.operands()[clsid_nb]=clsid;
+
+  const std::size_t lock_nb=root_type.component_number("@lock");
+  const typet &lock_type=root_type.components()[lock_nb].type();
+  jlo.operands()[lock_nb]=from_integer(lock, lock_type);
+}

src/java_bytecode/java_root_class.h

@@ -18,4 +18,10 @@ Author: Daniel Kroening, [email protected]
 void java_root_class(
   class symbolt &class_symbol);
 
+void java_root_class_init(
+  struct_exprt &jlo,
+  const struct_typet &root_type,
+  bool lock,
+  const irep_idt &class_identifier);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H