JBMC: Zero-initialized 'monitorCount' component (fixes diffblue#2307)

The 'monitorCount' 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.

Author: Degiorgio

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1077,6 +1077,18 @@ void java_object_factoryt::gen_nondet_struct_init(
     {
       continue;
     }
+    else if(name == "monitorCount")
+    {
+      // Zero-initialize 'monitorCount' field as it is not meant to be nondet.
+      // 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(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
     {
       INVARIANT(!name.empty(), "Each component of a struct must have a name");

jbmc/src/java_bytecode/java_root_class.cpp

@@ -75,4 +75,15 @@ void java_root_class_init(
   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
+  // concurrency.
+  if(root_type.has_component("monitorCount"))
+  {
+    const std::size_t count_nb = root_type.component_number("monitorCount");
+    const typet &count_type = root_type.components()[count_nb].type();
+    jlo.operands()[count_nb] = from_integer(0, count_type);
+  }
 }