diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc index 67a22ad6437..82ef54ea9ea 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Sync.class ---lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +--lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ 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 70f7c5ebd89..d5774c48850 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Sync.class ---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc index 161c0d0e8b2..493e8c23d1f 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Sync.class ---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class index b8b5fa6d05e..c77a1bff465 100644 Binary files a/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class and b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java index 2b4ac81400d..61c7868011b 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java @@ -14,6 +14,25 @@ public void me0() } } + // expected verification success + public static void aStatic() throws java.io.IOException + { + Object _lock = new Object(); + try + { + synchronized (_lock) + { + if(true) + throw new java.io.IOException(); + } + } + catch (java.io.IOException e) + { + return; + } + assert false; // unreachable + } + // expected verification success // -- // base-case, no synchronization diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class index 62a64a5c829..5abf894f8d8 100644 Binary files a/jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class and b/jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc index cdc51533471..7912d6324d2 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc @@ -1,6 +1,6 @@ CORE A.class ---function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions +--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading ATOMIC_BEGIN ATOMIC_END -- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc index 228f2385c1a..74628ecb54d 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc @@ -1,6 +1,6 @@ CORE A.class ---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc index cb79b066cca..46957f0ab60 100644 --- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc @@ -1,6 +1,6 @@ CORE A.class ---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc new file mode 100644 index 00000000000..32d07281ff0 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc @@ -0,0 +1,10 @@ +CORE +A.class +--function 'A.aStatic' --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that throwing an exception from a synchronization blocks does not cause reachability issues when the java-threading flag is not specified. + diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 023b8a596d1..8e0a1ba9120 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1026,8 +1026,6 @@ codet java_bytecode_convert_methodt::convert_instructions( } if(i_it->statement=="athrow" || - i_it->statement=="monitorenter" || - i_it->statement=="monitorexit" || i_it->statement=="putfield" || i_it->statement=="getfield" || i_it->statement=="checkcast" || @@ -1042,7 +1040,9 @@ codet java_bytecode_convert_methodt::convert_instructions( i_it->statement=="invokestatic" || i_it->statement=="invokevirtual" || i_it->statement=="invokespecial" || - i_it->statement=="invokeinterface") + i_it->statement=="invokeinterface" || + (threading_support && (i_it->statement=="monitorenter" || + i_it->statement=="monitorexit"))) { const std::vector handler = try_catch_handler(i_it->address, method.exception_table); @@ -1986,6 +1986,9 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit( "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" : "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V"; + if(!threading_support || !symbol_table.has_symbol(descriptor)) + return code_skipt(); + // becomes a function call code_typet type( {code_typet::parametert(java_reference_type(void_typet()))}, @@ -3099,7 +3102,9 @@ void java_bytecode_convert_method( bool throw_assertion_error, optionalt needed_lazy_methods, java_string_library_preprocesst &string_preprocess, - const class_hierarchyt &class_hierarchy) + const class_hierarchyt &class_hierarchy, + bool threading_support) + { if(std::regex_match( id2string(class_symbol.name), @@ -3118,7 +3123,8 @@ void java_bytecode_convert_method( throw_assertion_error, needed_lazy_methods, string_preprocess, - class_hierarchy); + class_hierarchy, + threading_support); java_bytecode_convert_method(class_symbol, method); } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/jbmc/src/java_bytecode/java_bytecode_convert_method.h index a3c6ad6ebe0..4fa21fc85dd 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -36,7 +36,8 @@ void java_bytecode_convert_method( bool throw_assertion_error, optionalt needed_lazy_methods, java_string_library_preprocesst &string_preprocess, - const class_hierarchyt &class_hierarchy); + const class_hierarchyt &class_hierarchy, + bool threading_support); void java_bytecode_convert_method_lazy( const symbolt &class_symbol, diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 4cb7ca0183b..6e1c9b45567 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -39,11 +39,13 @@ class java_bytecode_convert_methodt:public messaget bool throw_assertion_error, optionalt needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, - const class_hierarchyt &class_hierarchy) + const class_hierarchyt &class_hierarchy, + bool threading_support) : messaget(_message_handler), symbol_table(symbol_table), max_array_length(_max_array_length), throw_assertion_error(throw_assertion_error), + threading_support(threading_support), needed_lazy_methods(std::move(needed_lazy_methods)), string_preprocess(_string_preprocess), slots_for_parameters(0), @@ -67,6 +69,7 @@ class java_bytecode_convert_methodt:public messaget symbol_table_baset &symbol_table; const size_t max_array_length; const bool throw_assertion_error; + const bool threading_support; optionalt needed_lazy_methods; /// Fully qualified name of the method under translation. diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index ecf8cc2f4e6..83ef0b6d78c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1040,7 +1040,8 @@ bool java_bytecode_languaget::convert_single_method( throw_assertion_error, std::move(needed_lazy_methods), string_preprocess, - class_hierarchy); + class_hierarchy, + threading_support); return false; }