Add NullPointerException for Java synchronized blocks with null monitor

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.java

@@ -0,0 +1,25 @@
+public class MonitorExitTest {
+  // This test verifies monitorexit behavior with null
+  // Note: In normal Java code, you can't call monitorexit directly,
+  // but the synchronized block generates both monitorenter and monitorexit
+  public static void main(String[] args) {
+    final Object o = null;
+    boolean exceptionCaught = false;
+
+    try {
+      // This will generate both monitorenter and monitorexit bytecodes
+      synchronized (o) {
+        // Should not reach here
+        assert false;
+      }
+      // Should not reach here either
+      assert false;
+    }
+    catch (NullPointerException e) {
+      exceptionCaught = true;
+    }
+
+    // Verify that the exception was caught
+    assert exceptionCaught : "NullPointerException should have been thrown";
+  }
+}

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.java

@@ -0,0 +1,33 @@
+public class SyncTest {
+  // Test that synchronized with null throws NullPointerException
+  public static void testNull() {
+    final Object o = null;
+    try {
+      synchronized (o) {
+        assert false; // Should not reach here
+      }
+      assert false; // Should not reach here either
+    }
+    catch (NullPointerException e) {
+      // Expected - this is the correct behavior
+    }
+  }
+
+  // Test that synchronized with non-null object works
+  public static void testNonNull() {
+    final Object o = new Object();
+    try {
+      synchronized (o) {
+        // Should execute normally
+      }
+    }
+    catch (NullPointerException e) {
+      assert false; // Should not throw for non-null object
+    }
+  }
+
+  public static void main(String[] args) {
+    testNull();
+    testNonNull();
+  }
+}

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

@@ -7,6 +7,6 @@ Sync
 --
 ^warning: ignoring
 --
-This checks that the synchronized keyword on a null object will always throw.
-
-This is currently not working as explicit throws have been removed from the underlying model due to performance considerations.
+This checks that the synchronized keyword on a null object will always throw
+NullPointerException.  The null check is now performed during bytecode
+conversion.

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test2.desc

@@ -0,0 +1,12 @@
+CORE
+SyncTest
+--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Comprehensive test for synchronized blocks with both null and non-null objects.
+Verifies that NullPointerException is thrown for null and normal execution for
+non-null.

jbmc/src/java_bytecode/README.md

@@ -294,6 +294,12 @@ of a synchronized block.
 `monitorexit` is converted to a call to
 `java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V`.
 
+Before calling these monitor methods, a null check is performed on the object
+reference. If the reference is null, a `NullPointerException` is thrown, as
+specified by the Java bytecode specification. This ensures that the behavior
+matches the JVM specification where both `monitorenter` and `monitorexit`
+throw `NullPointerException` when their argument is null.
+
 \subsection converting-synchronized-methods Converting Synchronized Methods
 
 Synchronized methods make it impossible for two invocations of the same method

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2108,15 +2108,61 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
   if(!threading_support || !symbol_table.has_symbol(descriptor))
     return code_skipt();
 
-  // becomes a function call
+  PRECONDITION(op.size() == 1);
+  const exprt &objectref = op[0];
+
+  // Create null check for the monitor object
+  // According to JVM spec, monitorenter and monitorexit throw
+  // NullPointerException if objectref is null
+  const equal_exprt is_null{
+    objectref, null_pointer_exprt{to_pointer_type(objectref.type())}};
+
+  // Create the NullPointerException throw code
+  irep_idt exc_class_name{"java::java.lang.NullPointerException"};
+
+  // Ensure the exception class exists
+  if(!symbol_table.has_symbol(exc_class_name))
+  {
+    generate_class_stub(
+      "java.lang.NullPointerException",
+      symbol_table,
+      log.get_message_handler(),
+      struct_union_typet::componentst{});
+  }
+
+  pointer_typet exc_ptr_type = pointer_type(struct_tag_typet{exc_class_name});
+
+  // Allocate and throw an instance of NullPointerException
+  symbolt &new_symbol = fresh_java_symbol(
+    exc_ptr_type,
+    "monitor_null_exception",
+    source_location,
+    "monitor_null_exception",
+    symbol_table);
+
+  side_effect_exprt new_instance{ID_java_new, exc_ptr_type, source_location};
+  code_assignt assign_new{new_symbol.symbol_expr(), new_instance};
+
+  side_effect_expr_throwt throw_expr{irept{}, typet{}, source_location};
+  throw_expr.copy_to_operands(new_symbol.symbol_expr());
+
+  code_blockt throw_block{
+    {std::move(assign_new), code_expressiont{std::move(throw_expr)}}};
+
+  // Create the monitor function call
   java_method_typet type(
     {java_method_typet::parametert(java_reference_type(java_void_type()))},
     java_void_type());
-  code_function_callt call(symbol_exprt(descriptor, type), {op[0]});
+  code_function_callt call{symbol_exprt(descriptor, type), {objectref}};
   call.add_source_location() = source_location;
   if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
     needed_lazy_methods->add_needed_method(descriptor);
-  return std::move(call);
+
+  // Return if-then-else: if null, throw exception; else, call monitor function
+  code_ifthenelset if_code{is_null, throw_block, call};
+  if_code.add_source_location() = source_location;
+
+  return std::move(if_code);
 }
 
 void java_bytecode_convert_methodt::convert_dup2(