JBMC: Zero-initialized 'cproverMonitorCount' component and removed

'@lock' field (fixes diffblue#2307)

The 'cproverMonitorCount' field is a counter in the 'java.lang.Object'
model (part of the java core models library). This field is used to
implement a critical section and is thus necessary to support
concurrency.

This commit makes sure that this field (if present) is always zero
initialized as it is not meant to be non-deterministic.

This field is present only if the java core models library is loaded.

Additionally, the commit removes '@lock' field from root class
(usually: 'java.lang.Object') as it has been superseded by a locking
mechanism implemented in the java core models library.

Modified relevant unit/regression tests to reflect this change.

Author: Degiorgio

jbmc/regression/jbmc/json_trace2/test.desc

@@ -5,6 +5,6 @@ activate-multi-line-match
 EXIT=0
 SIGNAL=0
 "outputID": "return",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "output",\n *"thread": 0,\n *"values": \[\n *\{\n *"binary": "00000000",\n *"data": "false",\n *"name": "integer",\n *"type": "boolean",\n *"width": 8
-"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; boolean @lock; \} \*"
+"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; \} \*"
 --
 ^warning: ignoring

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -536,7 +536,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
 /// cprover_associate_length_to_array_func(
 ///   *string_data_pointer, tmp_object_factory);
 /// arg = { [email protected]={
-///   .@class_identifier=\"java::java.lang.String\", .@lock=false },
+///   .@class_identifier=\"java::java.lang.String\" },
 ///   .length=tmp_object_factory,
 ///   .data=*string_data_pointer };
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -570,11 +570,10 @@ codet initialize_nondet_string_struct(
     ? "java::java.lang.String"
     : "java::" + id2string(struct_type.get_tag());
 
-  // @lock = false:
   const symbol_typet jlo_symbol("java::java.lang.Object");
   const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol));
   struct_exprt jlo_init(jlo_symbol);
-  java_root_class_init(jlo_init, jlo_type, false, class_id);
+  java_root_class_init(jlo_init, jlo_type, class_id);
 
   struct_exprt struct_expr(obj.type());
   struct_expr.copy_to_operands(jlo_init);
@@ -1065,9 +1064,17 @@ void java_object_factoryt::gen_nondet_struct_init(
     {
       continue;
     }
-    else if(name=="@lock")
+    else if(name == "cproverMonitorCount")
     {
-      continue;
+      // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
+      // nondet. This field is only present when the java core models are
+      // included in the class-path. It is used to implement a critical section,
+      // which is necessary to support concurrency.
+      if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
+        continue;
+      code_assignt code(me, from_integer(0, me.type()));
+      code.add_source_location() = loc;
+      assignments.copy_to_operands(code);
     }
     else
     {

jbmc/src/java_bytecode/java_root_class.cpp

@@ -13,34 +13,16 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_types.h"
 
-/*******************************************************************
-
- Function: java_root_class
-
- Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
+/// Create components to an object of the root class (usually java.lang.Object)
+/// Specifically, we add a new component, '\@class_identifier'. This used
+/// primary to replace an expression like 'e instanceof A' with
+/// 'e.\@class_identifier == "A"'
+/// \param class_symbol: class symbol
 void java_root_class(symbolt &class_symbol)
 {
   struct_typet &struct_type=to_struct_type(class_symbol.type);
   struct_typet::componentst &components=struct_type.components();
 
-  {
-    // for monitorenter/monitorexit
-    struct_typet::componentt component;
-    component.set_name("@lock");
-    component.set_pretty_name("@lock");
-    component.type()=java_boolean_type();
-
-    // add at the beginning
-    components.insert(components.begin(), component);
-  }
-
   {
     // the class identifier is used for stuff such as 'instanceof'
     struct_typet::componentt component;
@@ -56,13 +38,11 @@ void java_root_class(symbolt &class_symbol)
 /// 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, generally begins with
 ///        "java::" prefix.
 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());
@@ -72,7 +52,15 @@ void java_root_class_init(
   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);
+  // Check if the 'cproverMonitorCount' component exists and initialize it.
+  // This field is only present when the java core models are embedded. It is
+  // used to implement a critical section, which is necessary to support
+  // concurrency.
+  if(root_type.has_component("cproverMonitorCount"))
+  {
+    const std::size_t count_nb =
+      root_type.component_number("cproverMonitorCount");
+    const typet &count_type = root_type.components()[count_nb].type();
+    jlo.operands()[count_nb] = from_integer(0, count_type);
+  }
 }

jbmc/src/java_bytecode/java_root_class.h

@@ -21,7 +21,6 @@ void java_root_class(
 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

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -840,12 +840,12 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
   PRECONDITION(implements_java_char_sequence_pointer(lhs.type()));
   dereference_exprt deref=checked_dereference(lhs, lhs.type().subtype());
 
-  // A String has a field Object with @clsid = String and @lock = false:
+  // A String has a field Object with @clsid = String
   const symbolt &jlo_symbol=*symbol_table.lookup("java::java.lang.Object");
   const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type);
   struct_exprt jlo_init(jlo_struct);
   irep_idt clsid = get_tag(lhs.type().subtype());
-  java_root_class_init(jlo_init, jlo_struct, false, clsid);
+  java_root_class_init(jlo_init, jlo_struct, clsid);
 
   struct_exprt struct_rhs(deref.type());
   struct_rhs.copy_to_operands(jlo_init);

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -94,12 +94,12 @@ symbol_exprt get_or_create_string_literal_symbol(
   namespacet ns(symbol_table);
 
   // Regardless of string refinement setting, at least initialize
-  // the literal with @clsid = String and @lock = false:
+  // the literal with @clsid = String
   symbol_typet jlo_symbol("java::java.lang.Object");
   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));
-  java_root_class_init(jlo_init, jlo_struct, false, "java::java.lang.String");
+  java_root_class_init(jlo_init, jlo_struct, "java::java.lang.String");
 
   // If string refinement *is* around, populate the actual
   // contents as well:
@@ -197,7 +197,7 @@ symbol_exprt get_or_create_string_literal_symbol(
   else if(jls_struct.get_bool(ID_incomplete_class))
   {
     // Case where java.lang.String was stubbed, and so directly defines
-    // @class_identifier and @lock:
+    // @class_identifier
     new_symbol.value = jlo_init;
   }
 

jbmc/unit/java-testing-utils/require_goto_statements.cpp

@@ -355,8 +355,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
   // After we have found the declaration of the final assignment's
   // right hand side, then we want to identify that the type
   // is the one we expect, e.g.:
-  // struct java.lang.Integer { __CPROVER_string @class_identifier;
-  // boolean @lock; } tmp_object_factory$2;
+  // struct java.lang.Integer { __CPROVER_string @class_identifier; }
+  // tmp_object_factory$2;
   const auto &component_declaration =
     require_goto_statements::require_declaration_of_name(
       component_tmp_name, entry_point_instructions);

jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp

@@ -50,8 +50,8 @@ SCENARIO(
         //  [email protected] =
         //     (struct java.lang.Object *) tmp_object_factory$2;
         //  tmp_object_factory$2 = &tmp_object_factory$3;
-        //  struct java.lang.Integer { __CPROVER_string @class_identifier;
-        //     boolean @lock; } tmp_object_factory$3;
+        //  struct java.lang.Integer { __CPROVER_string @class_identifier; }
+        //  tmp_object_factory$3;
         require_goto_statements::require_struct_component_assignment(
           this_tmp_name,
           {"Wrapper"},
@@ -455,8 +455,8 @@ SCENARIO(
       {
         //   [email protected] =
         // &tmp_object_factory$2;
-        // struct java.lang.Object { __CPROVER_string @class_identifier;
-        //   boolean @lock; } tmp_object_factory$2;
+        // struct java.lang.Object { __CPROVER_string @class_identifier; }
+        // tmp_object_factory$2;
         require_goto_statements::require_struct_component_assignment(
           this_tmp_name,
           {"UnsupportedWrapper1"},

jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp

@@ -559,8 +559,8 @@ SCENARIO(
         THEN("Object 'f' has unspecialized field 'field'")
         {
           // tmp_object_factory$2.field = &tmp_object_factory$3;
-          // struct java.lang.Object { __CPROVER_string @class_identifier;
-          //   boolean @lock; } tmp_object_factory$3;
+          // struct java.lang.Object { __CPROVER_string @class_identifier; }
+          // tmp_object_factory$3;
           require_goto_statements::require_struct_component_assignment(
             field_input_name,
             {},

jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -83,7 +83,7 @@ SCENARIO(
           "return_array = cprover_associate_length_to_array_func"
             "(*string_data_pointer, tmp_object_factory);",
           "arg = { [email protected]={ .@class_identifier"
-            "=\"java::java.lang.String\", .@lock=false },"
+            "=\"java::java.lang.String\" },"
             " .length=tmp_object_factory, "
             ".data=*string_data_pointer };"};