JBMC: Removed '@lock' field from root class (usually: 'java.lang.Object')

This is not needed any more as it has been superseded by a locking
mechanism implemented in the java models library.

Modified unit/regression tests to reflect the 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

@@ -539,7 +539,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 };
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -573,11 +573,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);
@@ -1073,10 +1072,6 @@ void java_object_factoryt::gen_nondet_struct_init(
     {
       continue;
     }
-    else if(name=="@lock")
-    {
-      continue;
-    }
     else if(name == "monitorCount")
     {
       // Zero-initialize 'monitorCount' field as it is not meant to be nondet.

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,10 +52,6 @@ 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 'monitorCount' 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

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

@@ -544,8 +544,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 };"};