From da7650048dfc85ef415f3e1bf7794d61c121aaa7 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Mon, 25 Jun 2018 18:41:06 +0100 Subject: [PATCH] JBMC: Fixed asymmetry between synchronized blocks and methods. Previously, the conversation of synchronized methods only took place if the 'java-threading' flag is specified, while in the case of synchronized blocks the conversation is undertaken with and without the aforementioned flag. This commit fixes this asymmetry by replacing the instructions 'monitorenter' and 'moinitorexit' with 'code_skipt' if the 'java-threading' option is not specified (instead of instrumenting calls to 'java::java.lang.Object.monitorexit/enter'). The 'monitorenter' and monitiorexit instructions are also replaced with a 'code_skipt' if the Java-core-models library is not loaded. This prevents JBMC from outputting missing function-body warnings. Commit also modifies relevant regression tests. --- .../test.desc | 2 +- .../synchronized-blocks-null-throw/test.desc | 2 +- .../synchronized-blocks-throw/test.desc | 2 +- .../synchronized-blocks/A.class | Bin 1039 -> 1243 bytes .../synchronized-blocks/A.java | 19 ++++++++++++++++++ .../synchronized-blocks/B.class | Bin 541 -> 541 bytes .../synchronized-blocks/test1.desc | 2 +- .../synchronized-blocks/test2.desc | 2 +- .../synchronized-blocks/test3.desc | 2 +- .../synchronized-blocks/test4.desc | 10 +++++++++ .../java_bytecode_convert_method.cpp | 16 ++++++++++----- .../java_bytecode_convert_method.h | 3 ++- .../java_bytecode_convert_method_class.h | 5 ++++- .../java_bytecode/java_bytecode_language.cpp | 3 ++- 14 files changed, 54 insertions(+), 14 deletions(-) create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc 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 b8b5fa6d05eb241cb790e79cc45a556a8cba357c..c77a1bff465a11254e27da3d8c40be800c7bb915 100644 GIT binary patch literal 1243 zcmY*ZSx*yD7(I8o%ybwiw217Bfv^);v9rmfeugb2~fl-VZ7)R8=3rx^8 zr()8;6sGTsJR;lRLvy<_S)Meu81lmgCs=s)GXzDBcN2t0$fbn4Q^b|fABp_ky2q$li9h>M^ zJe+p!9l`09{u)MfG_$4`)#yVQj~VSj;FhI66^$yI_=Ql>d=3A+ik2JH@VsVP2(6^5 zcyINIw~xM-JF0JD8_CNHsHCM8Q}L@rF?q@qgZ-rl8hbX8Nr_W4B?A2#qXya3qlM8n zS{)vr4k)*DDi6rqQW%o*n6;su<$PvC!IFEWci3J|V)z0f^3aoU?K`UC=P*3gTH|M^ z(vDFt@7mz;0~uLVV%9*VKwUJ%s85`tB>2PZ_gHBVHyBdUNzkq`=x0{SnN5{J&rr>= z{f`~J!!A#*GF2&4m>{EUGRm!%_ruYRk<2(VCaB0H8oBEOn5H%3k&3|gNB)6yQk%un w(3t2<)hwL^ZLH;%y0k1tNy(E_8qA3EWlz^Go~5$37ODL z2Dm1a4bY7GVy28YZM>W&A236qvAUVcM{Tpxsj%N|m8GTeD{se1G}?1;J;W7DI(|eD9P#bH`(+bY0;}UF?Tp zWksygLY}vz@dU7&jLhyA%>x)p9;(f}W>82Ebx<49>PU8}gL+Qa#`^XD;3)&z%sI11 zM*I``A{dj2(q Yzu^2+^LNLFyo(jSly!RoZq$za0l#5PCIA2c 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 62a64a5c829c35e1568670ac5cde1b96ae47a7a0..5abf894f8d89148856eeab9441c49b23d6b94083 100644 GIT binary patch delta 49 zcmbQsGM8mT5+kP_0}F!#13!b~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; }