diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.class new file mode 100644 index 00000000000..1502d67eb09 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.java b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.java new file mode 100644 index 00000000000..3461863c6ba --- /dev/null +++ b/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"; + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.class new file mode 100644 index 00000000000..d2ddeb97fe5 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.java b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.java new file mode 100644 index 00000000000..5a98e3e8392 --- /dev/null +++ b/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(); + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc index b253e641784..963a276cd45 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc +++ b/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. diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test2.desc new file mode 100644 index 00000000000..2e200890fed --- /dev/null +++ b/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. diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index f7593c2a23e..32f7375dfd4 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/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 diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 8d3c23d50f3..e136b38c93a 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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(