From f5f00d10f05f35f0b405123eafa8085af597b945 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 20:43:53 +0100 Subject: [PATCH] Add NullPointerException for Java synchronized blocks with null monitor Implement null checking for `monitorenter`/`monitorexit` bytecode instructions to throw `NullPointerException` when the monitor object is null, as per Java bytecode specification. Fixes: #1236 --- .../MonitorExitTest.class | Bin 0 -> 824 bytes .../MonitorExitTest.java | 25 +++++++++ .../SyncTest.class | Bin 0 -> 943 bytes .../SyncTest.java | 33 +++++++++++ .../synchronized-blocks-null-throw/test.desc | 6 +- .../synchronized-blocks-null-throw/test2.desc | 12 ++++ jbmc/src/java_bytecode/README.md | 6 ++ .../java_bytecode_convert_method.cpp | 52 +++++++++++++++++- 8 files changed, 128 insertions(+), 6 deletions(-) create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/MonitorExitTest.java create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/SyncTest.java create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test2.desc 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 0000000000000000000000000000000000000000..1502d67eb09dff7c7ba7f276cab38269df23ab2f GIT binary patch literal 824 zcmZuvT~8B16g{)ucD73k{h|~KSP-?Sd?XSd6pYBngO+O2h6H@twi7zI?2_Fr`dj)3 z`iv$v(ZnY9&7b50@lGpLjSo9_cF(!z-h1x;xcc%9z&7rg&=BI#V+bR{kT|t2tTo$m zPS#%6PDMRnh-^wn2G1Bm#pS~&3`9B17{(A|m^g3=bG^L}GN=ll*y$z9_k|Zo*YS6y zZ`EwkU|`1_;|#fx`t~(z&+}Z*L|k=|WSAdO$}QV|<4PwGq+b{3O4C4^;o<*~g5Pvo zcB9a=E<~Xwgi{Ebp8MWW(vxbsEW>26G?E|A_jLKtL=Mv&Gcn{bOEZlqJ2nl&kZlNG zdZKaDb0x5X76IhQF@wJ2HU#CBq$A3$vzqX#YHR||Ea^~s@$DaFD}g7S6DrFPC!PAc z1M7Ui=eSMwjfz)Q`$HjPvu^)hf?07}UR~@<_18F?Q6kd|j03w{N|(7Fw3O zx3IChZ#M#k_@d)F!Bd64>daOW2_!XACekn!67`R6W7BREHaKOq+qNG#p4(n=+SYE% zZYro9jjTc`D!X)rTJ?R;Paz}pd4+NWS?{!3uRO;MY=8Ab!#|WG2sBBNCq(o>h#7;znTn zW2$K53)R&p^0Jh77gIfX)2t-Z)n_Q2;Z`*CY&hOB&vEurA=$m_o*suOlvhZ6L+J?G c;AH#0LQ8sgh*vwS(9@5Y`Ajx@KMYU*2L_&`ZU6uP literal 0 HcmV?d00001 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(