From 2a0d2f9b65b01aef4a5b12c5b809495ad48bad97 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Fri, 15 Jun 2018 13:54:51 +0100 Subject: [PATCH 1/7] AppVeyor fix: remove existing clones of the java models library. This commit changes the AppVeyor configuration file such that the java models library is freshly downloaded for every build. This prevents JBMC from being called with an out-of-sync version of the models library, resulting in non-deterministic behaviour. --- appveyor.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/appveyor.yml b/appveyor.yml index 65e6511e7d4..0caa0e1168c 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -18,6 +18,7 @@ install: Move-Item win_flex.exe bin\flex.exe -force Move-Item FlexLexer.h include\FlexLexer.h -force Remove-Item bin\data -Force -Recurse -ErrorAction SilentlyContinue + Remove-Item java-models-library-master -Force -Recurse -ErrorAction SilentlyContinue Move-Item data bin\data -force bison -V flex -V From 0b90c17a8cac0b1abca6ec2a370f9493e802921b Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Thu, 14 Jun 2018 17:26:45 +0100 Subject: [PATCH 2/7] JBMC: Moved format_classpath.sh to scripts/format_classpath.sh 'format_classpath.sh' is used in regression tests that make use of the 'classpath' option. This script is needed to deal with the fact that classpath syntex is OS-dependent. The java concurrency regression tests make heavy use of this option as such this commit moves 'format_classpath.sh' to 'scripts/format_classpath.sh'. Furthermore, this commit makes a very small change to 'appveyor.yml' that enables existing java concurrency regression tests to run on Windows. --- appveyor.yml | 1 - jbmc/regression/jbmc/overlay-class/correct-test.desc | 2 +- jbmc/regression/jbmc/overlay-class/duplicate-test.desc | 2 +- jbmc/regression/jbmc/overlay-class/misordered-test.desc | 2 +- jbmc/regression/jbmc/overlay-class/unmarked-test.desc | 2 +- .../jbmc/overlay-class => scripts}/format_classpath.sh | 0 6 files changed, 4 insertions(+), 5 deletions(-) rename {jbmc/regression/jbmc/overlay-class => scripts}/format_classpath.sh (100%) diff --git a/appveyor.yml b/appveyor.yml index 0caa0e1168c..f17933269bb 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -91,7 +91,6 @@ test_script: rmdir /s /q jbmc\classpath1 rmdir /s /q jbmc\jar-file3 rmdir /s /q jbmc\tableswitch2 - rmdir /s /q jbmc-concurrency\explicit_thread_blocks cd ../.. make -C jbmc/regression test diff --git a/jbmc/regression/jbmc/overlay-class/correct-test.desc b/jbmc/regression/jbmc/overlay-class/correct-test.desc index fea8647abf4..ecde48e8a55 100644 --- a/jbmc/regression/jbmc/overlay-class/correct-test.desc +++ b/jbmc/regression/jbmc/overlay-class/correct-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh . annotations correct-overlay` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh . annotations correct-overlay` --verbosity 10 ^Getting class `Test' from file \.[\\/]Test\.class$ ^Getting class `Test' from file correct-overlay[\\/]Test\.class$ ^Adding symbol from overlay class: field 'x'$ diff --git a/jbmc/regression/jbmc/overlay-class/duplicate-test.desc b/jbmc/regression/jbmc/overlay-class/duplicate-test.desc index 1ac968acb9c..2bfce7a5ca3 100644 --- a/jbmc/regression/jbmc/overlay-class/duplicate-test.desc +++ b/jbmc/regression/jbmc/overlay-class/duplicate-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh . annotations . correct-overlay` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh . annotations . correct-overlay` --verbosity 10 ^Getting class `Test' from file \.[\\/]Test\.class$ ^Getting class `Test' from file correct-overlay[\\/]Test\.class$ ^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$ diff --git a/jbmc/regression/jbmc/overlay-class/misordered-test.desc b/jbmc/regression/jbmc/overlay-class/misordered-test.desc index acd447a376f..6505d5449d1 100644 --- a/jbmc/regression/jbmc/overlay-class/misordered-test.desc +++ b/jbmc/regression/jbmc/overlay-class/misordered-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh annotations correct-overlay .` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh annotations correct-overlay .` --verbosity 10 ^Getting class `Test' from file correct-overlay[\\/]Test\.class$ ^Getting class `Test' from file \.[\\/]Test\.class$ ^Skipping class Test marked with OverlayClassImplementation but found before original definition$ diff --git a/jbmc/regression/jbmc/overlay-class/unmarked-test.desc b/jbmc/regression/jbmc/overlay-class/unmarked-test.desc index 915f857fb87..cbf0430a3a6 100644 --- a/jbmc/regression/jbmc/overlay-class/unmarked-test.desc +++ b/jbmc/regression/jbmc/overlay-class/unmarked-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh . annotations unmarked-overlay` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh . annotations unmarked-overlay` --verbosity 10 ^Getting class `Test' from file \.[\\/]Test\.class$ ^Getting class `Test' from file unmarked-overlay[\\/]Test\.class$ ^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$ diff --git a/jbmc/regression/jbmc/overlay-class/format_classpath.sh b/scripts/format_classpath.sh similarity index 100% rename from jbmc/regression/jbmc/overlay-class/format_classpath.sh rename to scripts/format_classpath.sh From 0691f030bc65971f78f90c133200c09362420deb Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Tue, 29 May 2018 16:49:48 +0100 Subject: [PATCH 3/7] JBMC: Zero-initialized 'cproverMonitorCount' component and removed '@lock' field (fixes #2307) The 'cproverMonitorCount' field is a counter in the 'java.lang.Object' model (part of the java core models library). This field is used to implement a critical section and is thus necessary to support concurrency. This commit makes sure that this field (if present) is always zero initialized as it is not meant to be non-deterministic. This field is present only if the java core models library is loaded. Additionally, the commit removes '@lock' field from root class (usually: 'java.lang.Object') as it has been superseded by a locking mechanism implemented in the java core models library. Modified relevant unit/regression tests to reflect this change. --- jbmc/regression/jbmc/json_trace2/test.desc | 2 +- .../src/java_bytecode/java_object_factory.cpp | 17 ++++--- jbmc/src/java_bytecode/java_root_class.cpp | 44 +++++++------------ jbmc/src/java_bytecode/java_root_class.h | 1 - .../java_string_library_preprocess.cpp | 4 +- .../java_bytecode/java_string_literals.cpp | 6 +-- .../require_goto_statements.cpp | 4 +- .../generic_bases_test.cpp | 8 ++-- .../generic_parameters_test.cpp | 4 +- .../gen_nondet_string_init.cpp | 2 +- 10 files changed, 43 insertions(+), 49 deletions(-) diff --git a/jbmc/regression/jbmc/json_trace2/test.desc b/jbmc/regression/jbmc/json_trace2/test.desc index 13d8774fb25..390b8c6d3d3 100644 --- a/jbmc/regression/jbmc/json_trace2/test.desc +++ b/jbmc/regression/jbmc/json_trace2/test.desc @@ -5,6 +5,6 @@ activate-multi-line-match EXIT=0 SIGNAL=0 "outputID": "return",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "output",\n *"thread": 0,\n *"values": \[\n *\{\n *"binary": "00000000",\n *"data": "false",\n *"name": "integer",\n *"type": "boolean",\n *"width": 8 -"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; boolean @lock; \} \*" +"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; \} \*" -- ^warning: ignoring diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index d4af87e9637..bba09f713f9 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -536,7 +536,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) /// cprover_associate_length_to_array_func( /// *string_data_pointer, tmp_object_factory); /// arg = { .@java.lang.Object={ -/// .@class_identifier=\"java::java.lang.String\", .@lock=false }, +/// .@class_identifier=\"java::java.lang.String\" }, /// .length=tmp_object_factory, /// .data=*string_data_pointer }; /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -570,11 +570,10 @@ codet initialize_nondet_string_struct( ? "java::java.lang.String" : "java::" + id2string(struct_type.get_tag()); - // @lock = false: const symbol_typet jlo_symbol("java::java.lang.Object"); const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol)); struct_exprt jlo_init(jlo_symbol); - java_root_class_init(jlo_init, jlo_type, false, class_id); + java_root_class_init(jlo_init, jlo_type, class_id); struct_exprt struct_expr(obj.type()); struct_expr.copy_to_operands(jlo_init); @@ -1065,9 +1064,17 @@ void java_object_factoryt::gen_nondet_struct_init( { continue; } - else if(name=="@lock") + else if(name == "cproverMonitorCount") { - continue; + // Zero-initialize 'cproverMonitorCount' field as it is not meant to be + // nondet. This field is only present when the java core models are + // included in the class-path. It is used to implement a critical section, + // which is necessary to support concurrency. + if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE) + continue; + code_assignt code(me, from_integer(0, me.type())); + code.add_source_location() = loc; + assignments.copy_to_operands(code); } else { diff --git a/jbmc/src/java_bytecode/java_root_class.cpp b/jbmc/src/java_bytecode/java_root_class.cpp index 4c2d98b43b9..3d33b2b6678 100644 --- a/jbmc/src/java_bytecode/java_root_class.cpp +++ b/jbmc/src/java_bytecode/java_root_class.cpp @@ -13,34 +13,16 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" -/******************************************************************* - - Function: java_root_class - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - +/// Create components to an object of the root class (usually java.lang.Object) +/// Specifically, we add a new component, '\@class_identifier'. This used +/// primary to replace an expression like 'e instanceof A' with +/// 'e.\@class_identifier == "A"' +/// \param class_symbol: class symbol void java_root_class(symbolt &class_symbol) { struct_typet &struct_type=to_struct_type(class_symbol.type); struct_typet::componentst &components=struct_type.components(); - { - // for monitorenter/monitorexit - struct_typet::componentt component; - component.set_name("@lock"); - component.set_pretty_name("@lock"); - component.type()=java_boolean_type(); - - // add at the beginning - components.insert(components.begin(), component); - } - { // the class identifier is used for stuff such as 'instanceof' struct_typet::componentt component; @@ -56,13 +38,11 @@ void java_root_class(symbolt &class_symbol) /// Adds members for an object of the root class (usually java.lang.Object). /// \param jlo [out] : object to initialize /// \param root_type: type of the root class -/// \param lock: lock field /// \param class_identifier: class identifier field, generally begins with /// "java::" prefix. void java_root_class_init( struct_exprt &jlo, const struct_typet &root_type, - const bool lock, const irep_idt &class_identifier) { jlo.operands().resize(root_type.components().size()); @@ -72,7 +52,15 @@ void java_root_class_init( constant_exprt clsid(class_identifier, clsid_type); jlo.operands()[clsid_nb]=clsid; - const std::size_t lock_nb=root_type.component_number("@lock"); - const typet &lock_type=root_type.components()[lock_nb].type(); - jlo.operands()[lock_nb]=from_integer(lock, lock_type); + // Check if the 'cproverMonitorCount' component exists and initialize it. + // This field is only present when the java core models are embedded. It is + // used to implement a critical section, which is necessary to support + // concurrency. + if(root_type.has_component("cproverMonitorCount")) + { + const std::size_t count_nb = + root_type.component_number("cproverMonitorCount"); + const typet &count_type = root_type.components()[count_nb].type(); + jlo.operands()[count_nb] = from_integer(0, count_type); + } } diff --git a/jbmc/src/java_bytecode/java_root_class.h b/jbmc/src/java_bytecode/java_root_class.h index 583556de857..3c1f148ee0f 100644 --- a/jbmc/src/java_bytecode/java_root_class.h +++ b/jbmc/src/java_bytecode/java_root_class.h @@ -21,7 +21,6 @@ void java_root_class( void java_root_class_init( struct_exprt &jlo, const struct_typet &root_type, - bool lock, const irep_idt &class_identifier); #endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 822fcd46a97..1f901d6bda0 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -840,12 +840,12 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( PRECONDITION(implements_java_char_sequence_pointer(lhs.type())); dereference_exprt deref=checked_dereference(lhs, lhs.type().subtype()); - // A String has a field Object with @clsid = String and @lock = false: + // A String has a field Object with @clsid = String const symbolt &jlo_symbol=*symbol_table.lookup("java::java.lang.Object"); const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type); struct_exprt jlo_init(jlo_struct); irep_idt clsid = get_tag(lhs.type().subtype()); - java_root_class_init(jlo_init, jlo_struct, false, clsid); + java_root_class_init(jlo_init, jlo_struct, clsid); struct_exprt struct_rhs(deref.type()); struct_rhs.copy_to_operands(jlo_init); diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index b4de86b1cd4..b090adfaef4 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -94,12 +94,12 @@ symbol_exprt get_or_create_string_literal_symbol( namespacet ns(symbol_table); // Regardless of string refinement setting, at least initialize - // the literal with @clsid = String and @lock = false: + // the literal with @clsid = String symbol_typet jlo_symbol("java::java.lang.Object"); const auto &jlo_struct = to_struct_type(ns.follow(jlo_symbol)); struct_exprt jlo_init(jlo_symbol); const auto &jls_struct = to_struct_type(ns.follow(string_type)); - java_root_class_init(jlo_init, jlo_struct, false, "java::java.lang.String"); + java_root_class_init(jlo_init, jlo_struct, "java::java.lang.String"); // If string refinement *is* around, populate the actual // contents as well: @@ -197,7 +197,7 @@ symbol_exprt get_or_create_string_literal_symbol( else if(jls_struct.get_bool(ID_incomplete_class)) { // Case where java.lang.String was stubbed, and so directly defines - // @class_identifier and @lock: + // @class_identifier new_symbol.value = jlo_init; } diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 77a91721713..ed6bc73ff04 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -355,8 +355,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( // After we have found the declaration of the final assignment's // right hand side, then we want to identify that the type // is the one we expect, e.g.: - // struct java.lang.Integer { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$2; + // struct java.lang.Integer { __CPROVER_string @class_identifier; } + // tmp_object_factory$2; const auto &component_declaration = require_goto_statements::require_declaration_of_name( component_tmp_name, entry_point_instructions); diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp index 389e1f43056..472e119494d 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp @@ -50,8 +50,8 @@ SCENARIO( // tmp_object_factory$1.@Wrapper.field = // (struct java.lang.Object *) tmp_object_factory$2; // tmp_object_factory$2 = &tmp_object_factory$3; - // struct java.lang.Integer { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$3; + // struct java.lang.Integer { __CPROVER_string @class_identifier; } + // tmp_object_factory$3; require_goto_statements::require_struct_component_assignment( this_tmp_name, {"Wrapper"}, @@ -455,8 +455,8 @@ SCENARIO( { // tmp_object_factory$1.@UnsupportedWrapper1.field = // &tmp_object_factory$2; - // struct java.lang.Object { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$2; + // struct java.lang.Object { __CPROVER_string @class_identifier; } + // tmp_object_factory$2; require_goto_statements::require_struct_component_assignment( this_tmp_name, {"UnsupportedWrapper1"}, diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp index 9d7b1633b35..c80824631c6 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp @@ -559,8 +559,8 @@ SCENARIO( THEN("Object 'f' has unspecialized field 'field'") { // tmp_object_factory$2.field = &tmp_object_factory$3; - // struct java.lang.Object { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$3; + // struct java.lang.Object { __CPROVER_string @class_identifier; } + // tmp_object_factory$3; require_goto_statements::require_struct_component_assignment( field_input_name, {}, diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 31071dace29..032348e8ed6 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -83,7 +83,7 @@ SCENARIO( "return_array = cprover_associate_length_to_array_func" "(*string_data_pointer, tmp_object_factory);", "arg = { .@java.lang.Object={ .@class_identifier" - "=\"java::java.lang.String\", .@lock=false }," + "=\"java::java.lang.String\" }," " .length=tmp_object_factory, " ".data=*string_data_pointer };"}; From 4d91aa5f17c2ecff0e2939e1ed1f14e677f69ad3 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Fri, 12 Jan 2018 17:17:16 +0000 Subject: [PATCH 4/7] JBMC: Modified the instrumentation of monitorexit/enter instructions The monitorenter and monitorexit instructions are used by the JVM to coordinate access to an object in the context of multiple threads. We have previously added two methods to the object model that use a counter to implement a reentrant lock. Calls to 'org.cprover.CProver.atomicBegin:()V"' and 'org.cprover.CProver.atomicEnd:()V' ensure that multiple threads do not race in the access/modification of this counter. In-order to support synchronization blocks, when the monitorexit/moniitorenter bytecode instruction is executed JBMC must call the aforementioned object model. To this end, this commit makes the following changes: 1. Transforms the monitorenter and monitorexit bytecode instructions into function-calls to the object model. Specifically, 'java.lang.Object.monitorenter:(Ljava/lang/Object;)V' and 'java.lang.Object.monitorexit:(Ljava/lang/Object;)V'. 2. Transforms 'org.cprover.CProver.atomicBegin:()V"' and 'org.cprover.CProver.atomicEnd:()V' into the appropriate codet instructions. Added the appropriate target-handlers if monitorenter or monitorexit are in the context of a try-catch block. --- .../java_bytecode_convert_method.cpp | 79 ++++++++++--------- .../java_bytecode_convert_method_class.h | 13 ++- .../java_bytecode/simple_method_stubbing.cpp | 15 +++- src/goto-programs/builtin_functions.cpp | 2 + 4 files changed, 59 insertions(+), 50 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 7829d813b08..841dd8ac62c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1021,6 +1021,8 @@ 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" || @@ -1246,6 +1248,20 @@ codet java_bytecode_convert_methodt::convert_instructions( "function expected to have exactly one parameter"); c = replace_call_to_cprover_assume(i_it->source_location, c); } + // replace calls to CProver.atomicBegin + else if(statement == "invokestatic" && + arg0.get(ID_identifier) == + "java::org.cprover.CProver.atomicBegin:()V") + { + c = codet(ID_atomic_begin); + } + // replace calls to CProver.atomicEnd + else if(statement == "invokestatic" && + arg0.get(ID_identifier) == + "java::org.cprover.CProver.atomicEnd:()V") + { + c = codet(ID_atomic_end); + } else if(statement=="invokeinterface" || statement=="invokespecial" || statement=="invokevirtual" || @@ -1634,13 +1650,9 @@ codet java_bytecode_convert_methodt::convert_instructions( results[0]= binary_predicate_exprt(op[0], ID_java_instanceof, arg0); } - else if(statement=="monitorenter") + else if(statement == "monitorenter" || statement == "monitorexit") { - c = convert_monitorenter(i_it->source_location, op); - } - else if(statement=="monitorexit") - { - c = convert_monitorexit(i_it->source_location, op); + c = convert_monitorenterexit(statement, op, i_it->source_location); } else if(statement=="swap") { @@ -1960,6 +1972,29 @@ codet java_bytecode_convert_methodt::convert_switch( return code_switch; } +codet java_bytecode_convert_methodt::convert_monitorenterexit( + const irep_idt &statement, + const exprt::operandst &op, + const source_locationt &source_location) +{ + const irep_idt descriptor = (statement == "monitorenter") ? + "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" : + "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V"; + + // becomes a function call + code_typet type( + {code_typet::parametert(java_reference_type(void_typet()))}, + void_typet()); + code_function_callt call; + call.function() = symbol_exprt(descriptor, type); + call.lhs().make_nil(); + call.arguments().push_back(op[0]); + call.add_source_location() = source_location; + if(needed_lazy_methods && symbol_table.has_symbol(descriptor)) + needed_lazy_methods->add_needed_method(descriptor); + return call; +} + void java_bytecode_convert_methodt::convert_dup2( exprt::operandst &op, exprt::operandst &results) @@ -2399,38 +2434,6 @@ codet &java_bytecode_convert_methodt::do_exception_handling( return c; } -codet java_bytecode_convert_methodt::convert_monitorexit( - const source_locationt &location, - const exprt::operandst &op) const -{ - code_typet type; - type.return_type() = void_typet(); - type.parameters().resize(1); - type.parameters()[0].type() = java_reference_type(void_typet()); - code_function_callt call; - call.function() = symbol_exprt("java::monitorexit", type); - call.lhs().make_nil(); - call.arguments().push_back(op[0]); - call.add_source_location() = location; - return call; -} - -codet java_bytecode_convert_methodt::convert_monitorenter( - const source_locationt &location, - const exprt::operandst &op) const -{ - code_typet type; - type.return_type() = void_typet(); - type.parameters().resize(1); - type.parameters()[0].type() = java_reference_type(void_typet()); - code_function_callt call; - call.function() = symbol_exprt("java::monitorenter", type); - call.lhs().make_nil(); - call.arguments().push_back(op[0]); - call.add_source_location() = location; - return call; -} - void java_bytecode_convert_methodt::convert_multianewarray( const source_locationt &location, const exprt &arg0, 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 6e2975ed337..4cb7ca0183b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -420,14 +420,6 @@ class java_bytecode_convert_methodt:public messaget codet &c, exprt::operandst &results); - codet convert_monitorenter( - const source_locationt &location, - const exprt::operandst &op) const; - - codet convert_monitorexit( - const source_locationt &location, - const exprt::operandst &op) const; - codet &do_exception_handling( const methodt &method, const std::set &working_set, @@ -446,6 +438,11 @@ class java_bytecode_convert_methodt:public messaget codet &c, exprt::operandst &results) const; + codet convert_monitorenterexit( + const irep_idt &statement, + const exprt::operandst &op, + const source_locationt &source_location); + codet &replace_call_to_cprover_assume(source_locationt location, codet &c); void convert_invoke( diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index 099b956e442..4fa38a5ea03 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -233,10 +233,17 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) void java_simple_method_stubst::check_method_stub(const irep_idt &symname) { const symbolt &sym = *symbol_table.lookup(symname); - if( - !sym.is_type && sym.value.id() == ID_nil && sym.type.id() == ID_code && - // Don't stub internal locking primitives: - sym.name != "java::monitorenter" && sym.name != "java::monitorexit") + if(!sym.is_type && sym.value.id() == ID_nil && + sym.type.id() == ID_code && + // do not stub internal locking calls as 'create_method_stub' does not + // automatically create the appropriate symbols for the formal parameters. + // This means that symex will (rightfully) crash when it encounters the + // function call as it will not be able to find symbols for the fromal + // parameters. + sym.name != + "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" && + sym.name != + "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V") { create_method_stub(*symbol_table.get_writeable(symname)); } diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 330c4c1f152..a15f5833e89 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -855,12 +855,14 @@ void goto_convertt::do_function_call_symbol( } else if(identifier==CPROVER_PREFIX "atomic_begin" || identifier=="__CPROVER::atomic_begin" || + identifier=="java::org.cprover.CProver.atomicBegin:()V" || identifier=="__VERIFIER_atomic_begin") { do_atomic_begin(lhs, function, arguments, dest); } else if(identifier==CPROVER_PREFIX "atomic_end" || identifier=="__CPROVER::atomic_end" || + identifier=="java::org.cprover.CProver.atomicEnd:()V" || identifier=="__VERIFIER_atomic_end") { do_atomic_end(lhs, function, arguments, dest); From 7efa7bf555a32b6f71915f8be05c1f46cbb7514e Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Tue, 29 May 2018 16:58:24 +0100 Subject: [PATCH 5/7] JBMC: Regression tests for multi-threaded java programs --- .../anonymous-java.lang.thread/A$1.class | Bin 0 -> 671 bytes .../anonymous-java.lang.thread/A$2.class | Bin 0 -> 660 bytes .../anonymous-java.lang.thread/A.class | Bin 0 -> 483 bytes .../anonymous-java.lang.thread/A.java | 39 ++++++ .../anonymous-java.lang.thread/test.desc | 6 + .../anonymous-java.lang.thread/test2.desc | 5 + .../A.class | Bin .../A.java | 0 .../test.desc | 3 +- .../explicit-thread-blocks/test2.desc | 5 + .../explicit_thread_blocks/test2.desc | 6 - .../get-current-thread/A.class | Bin 0 -> 1413 bytes .../get-current-thread/A.java | 112 ++++++++++++++++++ .../get-current-thread/B.class | Bin 0 -> 613 bytes .../get-current-thread/C.class | Bin 0 -> 587 bytes .../get-current-thread/test.desc | 6 + .../get-current-thread/test2.desc | 9 ++ .../get-current-thread/test3.desc | 9 ++ .../get-current-thread/test4.desc | 6 + .../get-current-thread/test5.desc | 6 + .../get-current-thread/test6.desc | 6 + .../get-current-thread/test_bug.desc | 18 +++ .../java-lang-runnable/A.class | Bin 0 -> 601 bytes .../java-lang-runnable/A.java | 87 ++++++++++++++ .../java-lang-runnable/B.class | Bin 0 -> 722 bytes .../java-lang-runnable/C.class | Bin 0 -> 795 bytes .../java-lang-runnable/test.desc | 6 + .../java-lang-runnable/test2.desc | 5 + .../java-lang-runnable/test3.desc | 6 + .../java-lang-runnable/test4.desc | 6 + .../jbmc-concurrency/java-lang-thread/A.class | Bin 0 -> 601 bytes .../jbmc-concurrency/java-lang-thread/A.java | 87 ++++++++++++++ .../jbmc-concurrency/java-lang-thread/B.class | Bin 0 -> 674 bytes .../jbmc-concurrency/java-lang-thread/C.class | Bin 0 -> 747 bytes .../java-lang-thread/test.desc | 6 + .../java-lang-thread/test2.desc | 5 + .../java-lang-thread/test3.desc | 6 + .../java-lang-thread/test4.desc | 6 + .../jbmc-concurrency/several-threads/A.class | Bin 0 -> 516 bytes .../jbmc-concurrency/several-threads/A.java | 102 ++++++++++++++++ .../jbmc-concurrency/several-threads/B.class | Bin 0 -> 769 bytes .../jbmc-concurrency/several-threads/C.class | Bin 0 -> 751 bytes .../jbmc-concurrency/several-threads/D.class | Bin 0 -> 607 bytes .../several-threads/test.desc | 6 + .../several-threads/test2.desc | 5 + .../several-threads/test3.desc | 6 + .../Sync.class | Bin 0 -> 641 bytes .../synchronized-blocks-illegal-state/Sync.j | 23 ++++ .../test.desc | 13 ++ .../synchronized-blocks-null-throw/Sync.class | Bin 0 -> 698 bytes .../synchronized-blocks-null-throw/Sync.java | 12 ++ .../synchronized-blocks-null-throw/test.desc | 10 ++ .../synchronized-blocks-throw/Sync.class | Bin 0 -> 961 bytes .../synchronized-blocks-throw/Sync.java | 35 ++++++ .../synchronized-blocks-throw/test.desc | 10 ++ .../synchronized-blocks/A.class | Bin 0 -> 1039 bytes .../synchronized-blocks/A.java | 60 ++++++++++ .../synchronized-blocks/B.class | Bin 0 -> 541 bytes .../synchronized-blocks/test.desc | 9 ++ .../synchronized-blocks/test1.desc | 7 ++ .../synchronized-blocks/test2.desc | 8 ++ .../synchronized-blocks/test3.desc | 8 ++ .../synchronized-blocks/test_sync.desc | 8 ++ .../test_sync_baseline.desc | 8 ++ 64 files changed, 778 insertions(+), 8 deletions(-) create mode 100644 jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class create mode 100644 jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class create mode 100644 jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.class create mode 100644 jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java create mode 100644 jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc rename jbmc/regression/jbmc-concurrency/{explicit_thread_blocks => explicit-thread-blocks}/A.class (100%) rename jbmc/regression/jbmc-concurrency/{explicit_thread_blocks => explicit-thread-blocks}/A.java (100%) rename jbmc/regression/jbmc-concurrency/{explicit_thread_blocks => explicit-thread-blocks}/test.desc (51%) create mode 100644 jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc delete mode 100644 jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/A.class create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/A.java create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/B.class create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/C.class create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc create mode 100644 jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/A.class create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/A.java create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/B.class create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/C.class create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/A.class create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/A.java create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/B.class create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/C.class create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc create mode 100644 jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/A.class create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/A.java create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/B.class create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/C.class create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/D.class create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/test2.desc create mode 100644 jbmc/regression/jbmc-concurrency/several-threads/test3.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.j create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.java create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.java create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class new file mode 100644 index 0000000000000000000000000000000000000000..6fa94cda14f0885e72a1441fcdb9a4acb617f762 GIT binary patch literal 671 zcmYLHQBTuQ6#j18ty?Lsn+Q`t5r>Ykh#1~nj16K!0=_^@9b z1xYl~cYl*Hes>nu=H7eGx##=NcTW5J@AsboHqou3ig^bP7OJqZsNK6Z?l~x7!N!t< z`&hQ|z{ZNe%~p_QQsq&aWG|yE=*Kb?5QhTgd>Cb|Cj#cK|BP-gN}~KZjW+$&Hv-mH z8cKoMZj{K^qm#Z=2O3U*8YSG@I%#@84+ih{g7?K;r8kHRB4niT zNVlB~;xvnrqdl1q)6m63%($4w4Hq?SJwn^X6kLI(My$s{a*6n5j-UNFvR5D=G#tC(Zk6b&HF}WXO1ZG2-MM{R(rPx_MA{84w z#1e<>aQueX)Zzfo)0!DExoYqrP^YyFgD>E8)-E7AmoPrl6KHTR^8~T{Dwrwq`$hiK z&N+nFy@08WbC|s^uuic!?{&{GSHwK$3{yW)dV7iTFU@O=c^j~3*Qn5=hB`JFz4gD| zA8<4k%wE^q9BTmT4f`7^r?9P0u*|QpCUjRaHAM-A`+_6D+_+j3w|QFp>+YaM%OP8p GC!c@4%W-A^ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class new file mode 100644 index 0000000000000000000000000000000000000000..70267c266d223db22b575c22e45558423391f5cf GIT binary patch literal 660 zcmYLH-%ry}6#j18ty?Ls8;Db;3>+}VBF6CMVr&o-67U5=0&iu#VU^OF+s^p6@ZzJ- zDoCPjKqzulo^GKTtTjM)8-%GDcW6Sj-ows!85OER*@}e~v%;!ytr7Jsz|Xfbn$R_4y@A0*vx ASO5S3 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.class b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.class new file mode 100644 index 0000000000000000000000000000000000000000..374de28031ae816ad1e8a3204c317cf4c187a5b3 GIT binary patch literal 483 zcmaKnUrPc(6vfZ%>TWx2YW~Zze}aV>Bt;KF5iCL=NIfJ$kE;%~qARRx^tF1Zpr8-X zhl)b}l?+YX+u^+{#@OciOE4b;wX!1-;#x!r+FlIeje}<@=k1!r)(-}s|9+2R& zIJ5YzIU+-M@~<$jsY|qXpOCC)EoPrm|kD3X%>i(+Yt{ST!~N|lr?QuH6^ RNH)lo%vqi+X8oC8=@W(cKD7V< literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java new file mode 100644 index 00000000000..e7d7ec5f0d3 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java @@ -0,0 +1,39 @@ +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + int x = 0; + + // expected verfication success + public void me() + { + Thread t = new Thread() + { + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44 || x == 10); + } + }; + t.start(); + x = 10; + } + + // expected verfication failure + public void me2() + { + Thread t = new Thread() + { + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44); + } + }; + t.start(); + x = 10; + } +} diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc new file mode 100644 index 00000000000..e7468745c1d --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me:()V' --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/anonymous-java.lang.thread/test2.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc new file mode 100644 index 00000000000..4918125c3a4 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function 'A.me2:()V' --lazy-methods --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.class b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.class similarity index 100% rename from jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.class rename to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.class diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.java b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.java similarity index 100% rename from jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.java rename to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.java diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc similarity index 51% rename from jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test.desc rename to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc index 9dd422bc973..1538f4a7c5c 100644 --- a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test.desc +++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc @@ -1,7 +1,6 @@ CORE A.class ---function "A.me:()V" --lazy-methods --java-threading - +--function 'A.me:()V' --lazy-methods --java-threading ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc new file mode 100644 index 00000000000..f7ae486d700 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function 'A.me2:()V' --lazy-methods --java-threading +^SIGNAL=0$ +^VERIFICATION FAILED diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc deleted file mode 100644 index 10a64a0e08b..00000000000 --- a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -A.class ---function "A.me2:()V" --lazy-methods --java-threading - -^SIGNAL=0$ -^VERIFICATION FAILED diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/A.class b/jbmc/regression/jbmc-concurrency/get-current-thread/A.class new file mode 100644 index 0000000000000000000000000000000000000000..b7af59c5440dd4e8f6080cbcacba5ded8ffb7764 GIT binary patch literal 1413 zcma)5TTc@~7(LV5mhBeWA{Qx&+)F{K(&B{*Lb*t6)d(?x7qheztkTwOTmFl@_~^5k zfRRMs{Y}PrX1DCd7qy#yv-8c&IdjhU?T=qyzX8bNv5r2ZbKc z=6bbh9vsOESM~)$`D(q|S{Cr9W?l*e3XO^s=qXm~@@czvAgx`sS-@9gi0-t^^4pU6 zu9FPaT!o1Y!Lk>wT*YgmVw@;j?>EUir8xjhOb4rQy*wk%n1 zIjGy~)R>x~!;xmov^rVZnA%oucFB6h*(flODtdQ%(XQ8(uS;rI&^}7jz4gKo>m|@% zk^n2+PY7x?n0@SmV3`5uuA1oqAm{H_lB?8Dvg^F6{|RrW_Q!WjX7qF-^{ zZ~#Op(t=t*iDr81X8)tH&fOYf0G=}S2r zy!vN^?aL=l5&k#R2$^nB$0(mMOk><;@CN0KJVEDJM7@SB*# zyeDTw$r*Qfa-1nSafc^;hAz(`r*sMW4lEEdOUN8Q`$Zm^a3R)M9aWzp9@Z}qVeyRO z1)_Vi=jblYouS8T1IO(pBIfDALwdf<9$F#Zq>Gp9NRK;sG2+FGvu8+nFwT|M39~_% zO5d0_^RcCE%lO zg+z=dy7xmF?~Kqc-n}pPoO|B6_x<_%;}@{Ox=W3=%Wdw|aOmV=-eJL|OxxkE%OXn- z_Z*fLYA9z{(OUJBM4L2>qhvcw{QgJ>f*dI-n_(2DPZZYL`k}(^#er7TUxblm@^x%Whez3b;j4Au5PgHs%S&d>Y&`D@?Ft#I;rkMb;mm`*B$u$%% zCCM@eG}`$n@+FoW8B@?%xh+UmlFN@SQD5aEJ|tF(;-19Tn7SikId%R!r3@%9@ zSoUY8eo}saN#%F0P%0E=iiZwG=`9`JaYGOb)uGDGvE)V}2(wM+8`U!$`wO;pfj!Z= Sc9Qp(DS1zGzjMVixBdZ0sBmlm literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/C.class b/jbmc/regression/jbmc-concurrency/get-current-thread/C.class new file mode 100644 index 0000000000000000000000000000000000000000..1b5081b3c4550d7edfe3f61d9a66b70a5f397de2 GIT binary patch literal 587 zcmYL_!B5ms5XOIR+uiP#!ose?>Vl%8fCu-&kr+wAghY)A#6-fS+rF&TwI#1De+(Cn zo`pn=CVKaeGEOV(9^TB$eBXTY&HVZM;}@{Sx=V{CmmYUoINU8m-(lIM&XU85%RTNp ztSZz<-oB!{7G#+=d7LKMZkz?fv5o{eQZ%;XB+j2Jtc}fg3foU3t!TfB6aA+6Jk;i} zBnxbcL@|4i2jQpJ!O3;CxgCzL``v@IFrj`Km+Z#QvyZ`P;4w$r;ep3P9(lOTczDbz zdL=p-2gzu#b7O4JnAC_V-(k(;F;5ipQ`+GNqXY5WP0eT!o|yDhn}Pqf%8JfN=YC;~ zPV)c6{oQIKS-m~g@W*lm#bTth*yw07S(eHR0ptWntjaN4a^{*uF%0v)(z8@7d9n}U zOMWYomE`)A6(s^YQ4&V;%rVkLF?JGD!!3+yvG7g+W=Ge4=nzoPNGRH#)7 zbJd`sD24Qi=n7(?`ZT#Uk=&{TVWH!Eqj`p7f5Emcv8OsWPRjl|HSa~~_jWaA@gE_7 BX;%OM literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc new file mode 100644 index 00000000000..500630ed419 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc new file mode 100644 index 00000000000..eb912a30fe3 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc @@ -0,0 +1,9 @@ +KNOWNBUG +A.class +--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +-- +Same bug as the one highlighted in 'test_bug.desc' diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc new file mode 100644 index 00000000000..ddf8a72a449 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc @@ -0,0 +1,9 @@ +KNOWNBUG +A.class +--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +-- +Same bug as the one highlighted in 'test_bug.desc' diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc new file mode 100644 index 00000000000..f3bc4b1b843 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc new file mode 100644 index 00000000000..88b37371847 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc new file mode 100644 index 00000000000..7ba18d7a64e --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc new file mode 100644 index 00000000000..09ba6a5fcb0 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc @@ -0,0 +1,18 @@ +KNOWNBUG +A.class +--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +-- +For some reason symex assigns 'g' to zero, even though +the only viable assignment should be one. +This issue seems to only occur when a variable is +assigned inside the local scope of a thread-block. + +If instead, we call a function from inside the thread-block and +then assign 'g' to 1 then as expected the only viable +assignment to 'g' is 1 (see test4.desc) + +Seems related to: https://github.com/diffblue/cbmc/issues/1630/ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.class b/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.class new file mode 100644 index 0000000000000000000000000000000000000000..67d8320cfba326520442ebd7c5cf04acacf60f03 GIT binary patch literal 601 zcmZ8e+fKqj6r61f#ZoR_DBi#eka#Cip46DAiBG7B5~Ghr8ZCjE)Z%~n0*NGkfFEU? ztxClMwsRi{cnlz~Gf6+$LJD&{R$zMMxBug34UwSV#JFGN zHN|HFX6TipmqpCeXJ+KH&G%BsNd5XSiV?}vVdzE53k*`El=n%L-T#q(w?t|3zqCYY MnbHbH7DWp3U#x3SSO5S3 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.java b/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.java new file mode 100644 index 00000000000..b111a123a39 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.java @@ -0,0 +1,87 @@ +// JBMC, concurrency tests that make use of +// the java.lang.Runnable model + +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + // calling start from outside. + // expected verfication success. + public void me3() + { + C c = new C(); + Thread tmp = new Thread(c); + tmp.start(); + c.setX(); + } + + // calling start from outside, no race-condition on B.x + // expected verfication success. + public void me4() + { + B b = new B(); + Thread tmp = new Thread(b); + tmp.start(); + } + + // expected verfication failed + public void me2() + { + B b = new B(); + b.me(); + } + + // expected verfication success. + public void me() + { + C c = new C(); + c.me(); + } +} + +class B implements Runnable +{ + int x = 0; + + @Override + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44); + } + + public void me() + { + Thread tmp = new Thread(this); + tmp.start(); + x = 10; + } +} + + +class C implements Runnable +{ + int x = 0; + + @Override + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44 || x == 10); + } + + public void me() + { + Thread tmp = new Thread(this); + tmp.start(); + setX(); + } + + public void setX() + { + x = 10; + } +} diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/B.class b/jbmc/regression/jbmc-concurrency/java-lang-runnable/B.class new file mode 100644 index 0000000000000000000000000000000000000000..f7dcdd34d57b838344441f711c8863b792f52d56 GIT binary patch literal 722 zcmZWm-%ry}7(KV`+N~?DD+tr6n}}G-;?xkuxEK*JF&RjNn84fJdZWeBncLR*xA5Yl z&;Ei$5`Fh?GRE%~+(K+}+urYd=iGC?`|Hp59{`rnvQb98gc2^P*JTS=Y#69pXxK2( zRIjTRW^G)^F&flI^wS9t$o&Mld#NHZavM-)Siej$Z+~e=K zgDN}+6FBFf0+*qts_g-fU$s~MxmuHQC>h)_wEbEN9xCz;2R=Nq``E&Qg8++X8lU&} zL_cNl#@rWK9G}>p@w@+*AE=~-B;}H5l`+0LpeZp-ha!oj2uJ29bea)BBicoihF=DQ z1C8#5QUPvF1*4roi^38*Nq_Uy!RTuTM__^e4caH#F-)mi&i08BQ04rHvq^QO+YHgN?v|yn{NLW`MQk;?qHfw6YMt{G&RhO)R&>> z>Ql!scgU61T|7iFaP2eRP89D_&U=(^nX=qR5w(%Z5^1WZ>Xi;*AHXs`!qC4!ADg1X Tslm^U6reeel#dHk(s1!FTdaHd literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/C.class b/jbmc/regression/jbmc-concurrency/java-lang-runnable/C.class new file mode 100644 index 0000000000000000000000000000000000000000..765482752bb5f3f688aff6f44b87ac8dde7d0dc8 GIT binary patch literal 795 zcmZuv-%ry}7(KV`)~&0qYzPxX5fHaB*$eT-p^^c{I51&^INrMLMvJ2}ZD;&jc;V4! ze~m;EefMuN#&ZX5G5XNk-gCb1+;hI$AHTkS1F(jQ1sii|Sh%T{TPEf$7??A0+d>ix zYFV_%ESb1tVHtN#6it)_#5+Du1@cQ?6v;65dqK46M_#KdJ7f+8l2t$O^g629wXvcUt|L$D zH4|kU_ptg`_4C$|Y{vq*vA|wG2reQ_7wiAR4^-+z6ni1tvSYs1<-`Q0Ix_M@*%>+H z0OCFgj_VNfoVg8-1sX4k(Ez8Q(s7sI!^C7K`L)an!MEj}LAd%CXdk!}xTdgS_d0L% z5s|4;Pm{RPExAsa4en=X)sN6mFf;3vPcf+g$2vvk97gjDiSJ5M8%pLV25j=b*g^)| zDB=mGi6kL@qR8=~FgoTw^x-kNb0nLzXVzB+NVx-~#}+U2o*|7o!|pKPE;V=)Tvfb9 zDyVp->sbHEw#S1TNMUBwur@3QCUVvQnG=}Cdl>pB=;I9ZO2ze|?*ugav9di&NW+ca DW+8+C literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc new file mode 100644 index 00000000000..95ec31a0c1f --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me:()V' --lazy-methods --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/java-lang-runnable/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc new file mode 100644 index 00000000000..4ba443c769d --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function 'A.me2:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^SIGNAL=0$ +^VERIFICATION FAILED diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc new file mode 100644 index 00000000000..248eae75e64 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me4:()V' --lazy-methods --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/java-lang-runnable/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc new file mode 100644 index 00000000000..3db62d553c4 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me3:()V' --lazy-methods --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/java-lang-thread/A.class b/jbmc/regression/jbmc-concurrency/java-lang-thread/A.class new file mode 100644 index 0000000000000000000000000000000000000000..033ac00382142e99fd1a2e9c4312eece8270618a GIT binary patch literal 601 zcmZ9JSx>@16ot=}rC2MQvWOz!ilUMzPijnn#3$55iIK+wjg~-3So~kUKq84hz#nBi zQx(Kca%SfCp6}k?etf>Y11Mle!xG{uRy8PcPiSysP0G58qy`mnDI4;2N}f_G(ke0n z-V4jN2A2Y^?EZs*yWDM>0)dKUn>WKw-RxD3dYchf$1FH{>gb7p(qUM;?+$wn^U9Jr z-r{k~crkSN5fBh1fuOwS+lKv=uRixoqbc8Q>ezA;$~v|Y&=GNN#kus`ddqAK1Y+6B zjBz)#ZQ0JbY}L~r7(HgV`{v*g8R#5=d^`}c0cw!9BzGaB2V;m=9t1*EuM-5<_&YKU@;%dgy@d2kihbkQ~Kc~CQ!-o&2w@iEX-I@ zw#$lS#mI`2waS$sZ)M6m;!jg##oxY&&}Im~({zf6G-r^ZmGh*^um5BHZiUvx|JGev N_h`-16s1W)>L{(WQ^xl++vg4_I}Uzd+z7lpTEC-2hc&wg^l?NDmbHG3l7e@urTl7oL0{3 zSHnTm#RXgx5bwC22uv@^G>udi50ms^oXWjH6jIq0u)A>*XZHlm*45_%*7`7v1g3g% z5{BXt`-2k`cWaode)KrjBlg<$SMsg&Fa_Vk z1UwIuI3-Zm)s=xvUaYMBqk5#&Pzm^BY5S#$WT=NPd02!`+y@RWdsxC1fw@+1+`5@3 ziKblD2})@uRmKQoeSN_60<&S1#wrR&hcZl-Q(*L6G5aqyk|6}{> zc!w$PGS@2Ux+r6I0Ev)(2STXP9Fs9?ph#0aAkD-Pas*EE%Z(0crKR)k7@fFP!UkqzUe?1rv+7E+F3XYzUlR^pYfq({K0$O|E2Lh9w zFbcM^!-F8+mBpmvEE1U5Nxj~iP4Dd)svMHik|2E{P;B=4XIkdYAd7p!gHU$r>o;F} z?>q}ODi$nESU87Cfto~D`(E^Nb^V{Y`*A#o1?(}k`zj7RUp6mUxFHp0P@(m<0mniE zuE31b8P{)TQ6wGTmT3w}>cuJJjQMt-n-G}xgCvXte>9oF(u@Sxu#Y)zQRmVX9vTMh zn)J-C0uOUQpvt!;RtP>#_XNUKze4%QFRoi+d3TF{=q{0|QBRk+)NQ!-3LD%nP@12h z9$~g_uN-4a0=9XK@+q|L2?{@?q>@WkDF!^GwMQsp0}dYJ0udeJ7aT4H)1xuBpyp$$ zr_j5!XLOc_D7r(G#uoqTZJ~rG4EdD3xu@|N)ys37ARu5JD&+j9=yLlL!6!&+Vr jRI26>9LdVrp! zXNaio9iku_n0xQJ-#O=gKQA9o&j5C?Vj_f;fwTz)DG3<^SrfVdUBIFVzW_gS67mL? z3={~yN~hm(cM0n1+8IHs4K5r)o;0Gd#6h*W6Kh9Mqn(<;876sNve}tGa#j zO)wjS@v!Y2bcF4zZg%Zk+d>!-0_|Cddqs`GzJ($p7M8tEl@Jwb`P%MZmQPw;r|lB- zk!ue*Ya_=!XS&75lTQPQCC4bE9B1OJm!_acE(kG>KCh`EAVawp>IPqlP(w2)%_-Ew z(gfPCBn*`o{N`pyQs7MFH`FXHQ^i!Hps>jQxHP?fQ}1>UkX^M*``pANcVj0kyLHQb613 zcRYc7-4DF|!EwtA4`ngoa1aPg9K>$>ZNq(ckyVZfWvcDoMHAzoKM3326JJu&wfkN7 zy=!6;1rrmvW+D$upd_n*46%;6UTgS2q2P;k<3)bxbw=X2bUYwHi;gf$ z^K%d|q42+OE5Itr#TaQkT$bn*UyG~|{2I;~grk0g@`;hab(u@p8)Q_OxiR8&p(e-! zr}-6%_KGBjkLqWrCs?wzA?EGW5Hq%A3{kYL+z^wtWe$-$ht@np>ZhEcBr^($o-NL* zQQtN;v5RSfgc6r8o4IB{HJQrd=uj}}Ukx)r_jMueyWNJt5&O@*3p!HE}eNgZT6h~Lsn zkDU2xB`U$4--HmercG3F*!8|QJF_#-zy5sx0bmpB77D25k;gT)T{m&Vf`O`un-;QI zRNIn?TNZ9(*~A?aD+1yJ*As!+WiO6plmw$Nei+1Fe<*z-J%MZ^2!rIlfL>pHE?_iA zz7#07f>1skAM|Ckt1c6c#-YGWC-DYv+upmgu695u*BA`XM6Awe91Y~-KvA+=clW*b zo{h^W*_gp48$~z*W!2pndg1Ght#en8qG%KeI8$i%O(Z>Ek!v>UDA8`y#HtM!YZop) z>+j1!B2b!gcgA7(&-OyS^?&=GN}7oiFCwit#hXJ;NnqZWaS%y=VveDcF#(RKheZy* z00A2s{|i$APFV$GWpFVp(OI5Wcth}OxhD{={tenERsvU4FJ*6&(P3w9!r6nKB6YX> z6`JvqB$tQAXXuBRs~Sges+l7cPGNLUkol<;wN$Z`zP?B0F5UD{!wbw4%|iS}jnl)z z^Y%d;Wcjo*3zV|*ee{X+Z0cc^>#WadDuu;;VhYlXOuuybRcJUZb z94rfn?_BQ$3NOMWkt&S_ak3pH;bC9)*f|ie+ff{)uLaE7%Z`AxHRwr!h4)b`KMubh zO0}zp*;d0?U~VT3yI($p-|nkcBGWyA>2|k&Z{zL^hN>&yMp|TVHa>^Pp@%uldzgXi zVHTc1NmrZwFg|K-{^NS1)IgDG+rf&5r+6mdPsVmXDH#%ZVN%-a^G*UwJ()yG_Qpm; zOowdnLI?D*`AmSp#eBdoX#}1uE@FY6+*LUt_;-U#h`>CD@slSa=vt<(Qc+_iH`a7m z*S^)juTv15!D#=2d4giuuaA%``|b#{e_-ujV(MD^8JS-`%YH?&23eY@U=4Y8ZHOCG z_yj17GoDkUxtzdv{{yv7QHvK`91B|6IFQTR7jRDCSU+Hyr!Xh^%+b_Y<`fKXLq|Ty H@RsfXmbqX{ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test.desc b/jbmc/regression/jbmc-concurrency/several-threads/test.desc new file mode 100644 index 00000000000..ffdd51daf44 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/several-threads/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function A.me --lazy-methods --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/several-threads/test2.desc b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc new file mode 100644 index 00000000000..cdf16ddd945 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function A.me2 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc new file mode 100644 index 00000000000..71b16a75d28 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function A.me3 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.class new file mode 100644 index 0000000000000000000000000000000000000000..97d5db1f4d5717ee4a1f1ea79fe092e4943e6a84 GIT binary patch literal 641 zcmYLFO-~b16g{u=rmr&$v=prsMW_&iU}VFR7!ffsX?0Oz0=wz-34_B7nVI^r^l$J7 zx<(U8G=W5R{v;Rbd4sf@_i^sI=bm$a{rP?lU>!>?DrhR)c2LHw!W|dV{O`J$!##z0 zfte*g%XFHDNt`_oGrt$rZ;DLFsMSi@$ z_A-j}z8`fGI!IEA=X(2NppT7B4-Q;`=9s;ConSjnlayACvO>$leJl#p#?05fLmlKy zJ%)A;(&WQclIj@UintbmMqg)Ps{5k}#>#*N?qm-wZneTii(1oo;>&_CS$IzJH^*D> zwpY#|P7M)LJj(@WO4SkdGfHd*S}VKlpR1QcR647dk1mF&x4*zT!Nd>9-80x1r=&?r zI3zo4H#aCdO@UG&-+)a-@~w#4sFS@wpEaVhkbl`yVnwka6lQ)yK2x|cMaIpMo%O;Z iFkLTygF1ndLrCi@ER*7D%ykMQYop{nHGvvM`PM&)Fm^%! literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.j b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.j new file mode 100644 index 00000000000..313a722565c --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.j @@ -0,0 +1,23 @@ +.class public Sync +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f()V +Start: + aload_0 + monitorexit +End: + new java/lang/AssertionError + dup + invokespecial java/lang/AssertionError/()V + athrow + return +Handle: + return +.catch java/lang/IllegalMonitorStateException from Start to End using Handle +.end method diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc new file mode 100644 index 00000000000..67a22ad6437 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc @@ -0,0 +1,13 @@ +KNOWNBUG +Sync.class +--lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Note: requires jasmin to compile the bytecode instructions +This checks that an extra monitorexit will always trigger an IllegalMonitorException. + +This is currently not working as explicit throws have been removed from the underlying model due to performance considerations. diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.class new file mode 100644 index 0000000000000000000000000000000000000000..4dc0adc576b14731b146c633e17ec3fbadcb50c3 GIT binary patch literal 698 zcmZuuT~8B16g|`ZnC*6J3kVjKYM~HRgcsfabI;y$&b>c>fBOMo6$>sLOc!C}F2_9=2BtagbIiD? z;{nG*hKZ)1BtoS!j*?e0@q3}@Gq4>7drd|%U1u;BAH8ERH{!lvsI+7xI)lTWP+J;I zg+pIP3{#8mTl@Y8etWVHKC|5)y(esIwCk1{+*gLpY+NeF|p7KHy;+-^Kj zfp{%-&tmsD3YK*{4<&dWif|cfdH)yJqBoU_6+=BQbp~PhHkMH;)aIu^9BFH$Qg`H- z^U%aRLp8_0>FtXkrAhopKfUI_tvwZgyz*ShUpGP;AldJWL@Lq05k{`l0TpO^J7~}f z99jvh*0dGM3^47C&NAI*C^CxH<1?_42I3Z-cJ@f)Km}FGHS`1pm=v3=^<=w!v2;0v z(^sp?>s zIOhmImSLDDB}d#MiBc&o~9YY2Tl{;)8gApC00+DBqtds=Ayg>VaRjo=ta6Gp<>r}1Pid4w5Ky=D+ zo#3`WI6d@OK+Ab0DbSL4T)9wNUzPr%N+z&wIj+FD^h$os+O)D2%PnV%f$zBGNmZCA z2A2JzU~Sa%xioj+I^0YkHf2}-OfiaH&9~(}NA-*s-?;XeYGC1z=B z1AVZ%ChdR)o?p(|8@{(G{cP@G-BOdX3<@5_^8B2~Ap)K0zqB|ho*bgu3DjX}8zpMzqSWYzIy>5LLJ3~E)R_`uEl1w#C&1<=~1WZ*3fZifz@oxJtZ z3fjo<9>gvkw&WSD2g8WtJi6#JRrIq|Blhk9p`|^9^O^8xXqlzL_sl*b+Iu8FAi9mF z1L%Zfhx>?cshh!D(_v=m6Ey89D@KlX5L*~I8a>=WTcHu(fmX<^snILwDk$KY0Qp0Vye=S+YzuusVjH?f bdf|_VDveLpI@MUUjv!>-RWH$BhcEpG5$3&E literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.java b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.java new file mode 100644 index 00000000000..3496ab7714f --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.java @@ -0,0 +1,35 @@ +import org.cprover.CProver; + +public class Sync +{ + int field; + public static void main(String[] args) + { + Sync o = new Sync(); + try + { + o.field=0; + synchronized (o) + { + // Make sure the monitor is taken. + assert(CProver.getMonitorCount(o) == 1); + if (CProver.nondetBoolean()) + throw new RuntimeException(); + o.field++; + } + } + catch(RuntimeException e) + { + o.field++; + } + catch(Throwable e) + {} + + // Make sure we did not execute in an unexpected way. + if (o.field != 1) + assert false; + + // Make sure the monitor is free. + assert(CProver.getMonitorCount(o) == 0); + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc new file mode 100644 index 00000000000..161c0d0e8b2 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +Sync.class +--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Checks all possible paths to ensure monitorexit is executed even after a throw. + +This is currently not working as explicit throws have been removed from the underlying model due to performance considerations. diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class new file mode 100644 index 0000000000000000000000000000000000000000..b8b5fa6d05eb241cb790e79cc45a556a8cba357c GIT binary patch literal 1039 zcmY*XTTjzq7=FI3Tf5PXvEdxZS0YU$elll;Nkf?*f43o@9led-sgSZ{`&L%2Y^{TiX(&`6}>9@V$ktWMSmO-=^BVb zMNf>!ptOdhHLPMJj#1pJgi^F_T~!wp1vB@pp^ z!zC5Pc1rsK>0+a##_|~@YWNmysw>qk&U~TI;Ew2&6DJdXCTrvy1tSm7immC(u^MF2^rUkXiW* z&-S0Vu#vS_0}6!huh4EK61(SB?D=$Pv1YOKlGrX%N?#RPlgKJL*k8vQp~vwBGa-O_b>W-kF=; zb(Ii89Jx26@5t$DrNMhty|{{Kd7^uV&w z3)@CQGi3V@t623tmnH|hLY7+B+771p)+m3&fao#2iJrt5;^9K(ao(1h3*)f!2yvca zlpYbfhv^W)w`_1Fu`iJ2U}BE4c~%F0M`W4l5n<;6k*-94KCnp165D(LQE#ksl=hHu z?qHVkZ%*kBVe^>la_={Y?&scTUvH^Z7(|l1BvL^%0wW2|16J5wrG+(&VVykshw)9C Tp)jPFh(hv{RKW Date: Wed, 30 May 2018 15:05:17 +0100 Subject: [PATCH 6/7] JBMC: Support for synchronized methods This commit adds support for synchronized methods by instrumenting all methods marked with the synchronization flag with calls to 'monitorenter' and 'monitorexit'. These two methods are located in the java models library and implement a critical section. To this end the following changes are made: 1. New irep_id, 'is_synchronized', to represent the synchronized keyword and appropriate changes to 'java_byecode_convert_method.cpp' to set this flag when a synchronized method is encountered. 2. Setting of the 'is_static' flag when the method in question is static. 3. Functions to find and instrument synchronized methods. Specifically, calls to "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V" are respectively instrumented at the start and end of a synchronized method . Note, the former is instrumented at every point where the execution of the synchronized methods terminates. Specifically out of order return statements and exceptions. Static synchronized methods are not supported yet as the synchronization semantics for static methods is different (locking on the class instead the of the object). Upon encountering a static synchronized method the current implementation will ignore the synchronized flag. (showing a warning in the process). This may obviously result in superfluous interleavings. Note: instrumentation of synchronized methods is only triggered if the '--java-threading' command line option is specified. Note': instrumentation of synchronized methods requires the use of the java core models library as the locking mechanism is implemented in the model 'java.long.Object'. --- jbmc/src/java_bytecode/Makefile | 2 +- ..._bytecode_concurrency_instrumentation.cpp} | 265 +++++++++++++++++- ...va_bytecode_concurrency_instrumentation.h} | 8 +- .../java_bytecode_convert_method.cpp | 5 + .../java_bytecode/java_bytecode_language.cpp | 7 +- src/util/irep_ids.def | 1 + 6 files changed, 277 insertions(+), 11 deletions(-) rename jbmc/src/java_bytecode/{java_bytecode_convert_threadblock.cpp => java_bytecode_concurrency_instrumentation.cpp} (58%) rename jbmc/src/java_bytecode/{java_bytecode_convert_threadblock.h => java_bytecode_concurrency_instrumentation.h} (53%) diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index df1511612ce..c3964a40375 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -8,7 +8,7 @@ SRC = bytecode_info.cpp \ jar_file.cpp \ java_bytecode_convert_class.cpp \ java_bytecode_convert_method.cpp \ - java_bytecode_convert_threadblock.cpp \ + java_bytecode_concurrency_instrumentation.cpp \ java_bytecode_instrument.cpp \ java_bytecode_internal_additions.cpp \ java_bytecode_language.cpp \ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp similarity index 58% rename from jbmc/src/java_bytecode/java_bytecode_convert_threadblock.cpp rename to jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index 13e6c43894d..7f37854913f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -6,7 +6,7 @@ Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com \*******************************************************************/ -#include "java_bytecode_convert_threadblock.h" +#include "java_bytecode_concurrency_instrumentation.h" #include "expr2java.h" #include "java_types.h" @@ -14,6 +14,7 @@ Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com #include #include #include +#include #include // Disable linter to allow an std::string constant. @@ -38,7 +39,7 @@ static symbolt add_or_get_symbol( const bool is_thread_local, const bool is_static_lifetime) { - const symbolt* psymbol = nullptr; + const symbolt *psymbol = nullptr; namespacet ns(symbol_table); ns.lookup(name, psymbol); if(psymbol != nullptr) @@ -89,6 +90,186 @@ static const std::string get_thread_block_identifier( return integer2string(lbl_id); } +/// Creates a monitorenter/monitorexit code_function_callt for +/// the given synchronization object. +/// \param symbol_table: a symbol table +/// \param is_enter: indicates whether we are creating a monitorenter or +/// monitorexit. +/// \param object: expression representing a 'java.Lang.Object'. This object is +/// used to achieve object-level locking by calling monitoroenter/monitorexit. +static codet get_monitor_call( + const symbol_tablet &symbol_table, + bool is_enter, + const exprt &object) +{ + const irep_idt symbol = + is_enter ? "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" + : "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V"; + + auto it = symbol_table.symbols.find(symbol); + + // If the 'java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V' or + // 'java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V' method is not + // found symex will rightfully complain as it cannot find the symbol + // associated with the method in question. To avoid this and thereby ensuring + // JBMC works both with and without the models, we replace the aforementioned + // methods with skips when we cannot find them. + // + // Note: this can only happen if the java-core-models library is not loaded. + // + // Note': we explicitly prevent JBMC from stubbing these methods. + if(it == symbol_table.symbols.end()) + return code_skipt(); + + // Otherwise we create a function call + code_function_callt call; + call.function() = symbol_exprt(symbol, it->second.type); + call.lhs().make_nil(); + call.arguments().push_back(object); + return call; +} + +/// Introduces a monitorexit before every return recursively. +/// Note: this breaks sharing on \p code +/// \param [out] code: current element to modify +/// \param monitorexit: codet to insert before the return +static void monitor_exits(codet &code, const codet &monitorexit) +{ + const irep_idt &statement = code.get_statement(); + if(statement == ID_return) + { + // Replace the return with a monitor exit plus return block + code_blockt return_block; + return_block.add(monitorexit); + return_block.move_to_operands(code); + code = return_block; + } + else if( + statement == ID_label || statement == ID_block || + statement == ID_decl_block) + { + // If label or block found, explore the code inside the block + Forall_operands(it, code) + { + codet &sub_code = to_code(*it); + monitor_exits(sub_code, monitorexit); + } + } +} + +/// Transforms the codet stored in \c symbol.value. The \p symbol is expected to +/// be a Java synchronized method. Java synchronized methods do not have +/// explicit calls to the instructions monitorenter and monitorexit, the JVM +/// interprets the synchronized flag in a method and uses monitor of the object +/// to implement locking and unlocking. Therefore JBMC has to emulate this same +/// behavior. We insert a call to our model of monitorenter at the beginning of +/// the method and calls to our model of monitorexit at each return instruction. +/// We wrap the entire body of the method with an exception handler that will +/// call our model of monitorexit if the method returns exceptionally. +/// +/// Example: +/// +/// \code +/// synchronized int amethod(int p) +/// { +/// int x = 0; +/// if(p == 0) +/// return -1; +/// x = p / 10 +/// return x +/// } +/// \endcode +/// +/// Is transformed into the codet equivalent of: +/// +/// \code +/// synchronized int amethod(int p) +/// { +/// try +/// { +/// java::java.lang.Object.monitorenter(this); +/// int x = 0; +/// if(p == 0) +/// { +/// java::java.lang.Object.monitorexit(this); +/// return -1; +/// } +/// java::java.lang.Object.monitorexit(this); +/// return x +/// } +/// catch(java::java.lang.Throwable e) +/// { +/// // catch every exception, including errors! +/// java::java.lang.Object.monitorexit(this); +/// throw e; +/// } +/// } +/// \endcode +/// +/// \param symbol_table: a symbol_table +/// \param symbol: writeable symbol hosting code to synchronize +/// \param sync_object: object to use as a lock +static void instrument_synchronized_code( + symbol_tablet &symbol_table, + symbolt &symbol, + const exprt &sync_object) +{ + PRECONDITION(!symbol.type.get_bool(ID_is_static)); + + codet &code = to_code(symbol.value); + + // Get the calls to the functions that implement the critical section + codet monitorenter = get_monitor_call(symbol_table, true, sync_object); + codet monitorexit = get_monitor_call(symbol_table, false, sync_object); + + // Create a unique catch label and empty throw type (i.e. any) + // and catch-push them at the beginning of the code (i.e. begin try) + code_push_catcht catch_push; + irep_idt handler("pc-synchronized-catch"); + irep_idt exception_id; + code_push_catcht::exception_listt &exception_list = + catch_push.exception_list(); + exception_list.push_back( + code_push_catcht::exception_list_entryt(exception_id, handler)); + + // Create a catch-pop to indicate the end of the try block + code_pop_catcht catch_pop; + + // Create the finally block with the same label targeted in the catch-push + const symbolt &tmp_symbol = get_fresh_aux_symbol( + java_reference_type(symbol_typet("java::java.lang.Throwable")), + id2string(symbol.name), + "caught-synchronized-exception", + code.source_location(), + ID_java, + symbol_table); + symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type); + catch_var.set(ID_C_base_name, tmp_symbol.base_name); + code_landingpadt catch_statement(catch_var); + codet catch_instruction = catch_statement; + code_labelt catch_label(handler, code_blockt()); + code_blockt &catch_block = to_code_block(catch_label.code()); + catch_block.add(catch_instruction); + catch_block.add(monitorexit); + + // Re-throw exception + side_effect_expr_throwt throw_expr; + throw_expr.copy_to_operands(catch_var); + catch_block.add(code_expressiont(throw_expr)); + + // Write a monitorexit before every return + monitor_exits(code, monitorexit); + + // Wrap the code into a try finally + code_blockt try_block; + try_block.move_to_operands(monitorenter); + try_block.move_to_operands(catch_push); + try_block.move_to_operands(code); + try_block.move_to_operands(catch_pop); + try_block.move_to_operands(catch_label); + code = try_block; +} + /// Transforms the codet stored in in \p f_code, which is a call to function /// CProver.startThread:(I)V into a block of code as described by the /// documentation of function convert_thread_block @@ -284,20 +465,20 @@ static void instrument_getCurrentThreadID( /// /// Note': the ID of the thread is assigned after the thread is created, this /// creates bogus interleavings. Currently, it's not possible to -/// assign the thread ID before the creation of the thead, due to a bug in +/// assign the thread ID before the creation of the thread, due to a bug in /// symex. See https://github.com/diffblue/cbmc/issues/1630/for more details. /// /// \param symbol_table: a symbol table void convert_threadblock(symbol_tablet &symbol_table) { using instrument_callbackt = - std::function; + std::function; using expr_replacement_mapt = - std::unordered_map; + std::unordered_map; namespacet ns(symbol_table); - for(auto entry : symbol_table) + for(const auto &entry : symbol_table) { expr_replacement_mapt expr_replacement_map; const symbolt &symbol = entry.second; @@ -361,3 +542,75 @@ void convert_threadblock(symbol_tablet &symbol_table) } } } + +/// Iterate through the symbol table to find and instrument synchronized +/// methods. +/// +/// Synchronized methods make it impossible for two invocations of the same +/// method on the same object to interleave. In-order to replicate +/// these semantics a call to +/// "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and +/// "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V" is instrumented +/// at the start and end of the method. Note, that the former is instrumented +/// at every statement where the execution can exit the method in question. +/// Specifically, out of order return statements and exceptions. The latter +/// is dealt with by instrumenting a try catch block. +/// +/// Note: Static synchronized methods are not supported yet as the +/// synchronization semantics for static methods is different (locking on the +/// class instead the of the object). Upon encountering a static synchronized +/// method the current implementation will ignore the synchronized flag. +/// (showing a warning in the process). This may result in superfluous +/// interleavings. +/// +/// Note': This method requires the availability of +/// "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and +/// "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V". +/// (java-library-models). If they are not available code_skipt will inserted +/// instead of calls to the aforementioned methods. +/// +/// \param symbol_table: a symbol table +/// \param message_handler: status output +void convert_synchronized_methods( + symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + namespacet ns(symbol_table); + for(const auto &entry : symbol_table) + { + const symbolt &symbol = entry.second; + + if(symbol.type.id() != ID_code) + continue; + if(symbol.value.is_nil()) + continue; + if(!symbol.type.get_bool(ID_is_synchronized)) + continue; + + if(symbol.type.get_bool(ID_is_static)) + { + messaget message(message_handler); + message.warning() << "Java method '" << entry.first + << "' is static and synchronized." + << " This is unsupported, the synchronized keyword" + << " will be ignored." + << messaget::eom; + continue; + } + + // find the object to synchronize on + const irep_idt this_id(id2string(symbol.name) + "::this"); + exprt this_expr(this_id); + + auto it = symbol_table.symbols.find(this_id); + + if(it == symbol_table.symbols.end()) + // failed to find object to synchronize on + continue; + + // get writeable reference and instrument the method + symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first); + instrument_synchronized_code( + symbol_table, w_symbol, it->second.symbol_expr()); + } +} diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.h b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h similarity index 53% rename from jbmc/src/java_bytecode/java_bytecode_convert_threadblock.h rename to jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h index ef02f92b79e..a757e400370 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.h +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h @@ -5,11 +5,15 @@ Module: Java Convert Thread blocks Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com \*******************************************************************/ -#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H -#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H +#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H +#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H #include +#include void convert_threadblock(symbol_tablet &symbol_table); +void convert_synchronized_methods( + symbol_tablet &symbol_table, + message_handlert &message_handler); #endif diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 841dd8ac62c..3c284340085 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -366,6 +366,11 @@ void java_bytecode_convert_method_lazy( else member_type.set_access(ID_default); + if(m.is_synchronized) + member_type.set(ID_is_synchronized, true); + if(m.is_static) + member_type.set(ID_is_static, true); + // do we need to add 'this' as a parameter? if(!m.is_static) { diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index aa88a8c19ac..5c15f43abee 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -22,9 +22,9 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "java_bytecode_concurrency_instrumentation.h" #include "java_bytecode_convert_class.h" #include "java_bytecode_convert_method.h" -#include "java_bytecode_convert_threadblock.h" #include "java_bytecode_internal_additions.h" #include "java_bytecode_instrument.h" #include "java_bytecode_typecheck.h" @@ -755,9 +755,12 @@ bool java_bytecode_languaget::typecheck( bool res = java_bytecode_typecheck( symbol_table, get_message_handler(), string_refinement_enabled); - // now instrument thread-blocks + // now instrument thread-blocks and synchronized methods. if(threading_support) + { convert_threadblock(symbol_table); + convert_synchronized_methods(symbol_table, get_message_handler()); + } return res; } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index c7b233c17ab..05e84f1d9f2 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -384,6 +384,7 @@ IREP_ID_TWO(C_is_anonymous, #is_anonymous) IREP_ID_ONE(is_enum_constant) IREP_ID_ONE(is_inline) IREP_ID_ONE(is_extern) +IREP_ID_ONE(is_synchronized) IREP_ID_ONE(is_global) IREP_ID_ONE(is_thread_local) IREP_ID_ONE(is_parameter) From 68ac56610f166bfd978ad30c0262fa15d9bf76b8 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 30 May 2018 15:12:01 +0100 Subject: [PATCH 7/7] JBMC: Regression tests for synchronized methods --- .../Sync.class | Bin 0 -> 1021 bytes .../Sync.java | 45 ++++++++++ .../test.desc | 10 +++ .../synchronized-methods/A.class | Bin 0 -> 1040 bytes .../synchronized-methods/A.java | 80 ++++++++++++++++++ .../synchronized-methods/B.class | Bin 0 -> 338 bytes .../synchronized-methods/C.class | Bin 0 -> 387 bytes .../synchronized-methods/test1.desc | 7 ++ .../synchronized-methods/test2.desc | 8 ++ .../synchronized-methods/test3.desc | 8 ++ .../synchronized-methods/test_sync.desc | 8 ++ .../test_sync_baseline.desc | 8 ++ .../test_sync_static.desc | 9 ++ 13 files changed, 183 insertions(+) create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.java create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/A.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/A.java create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/B.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/C.class create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc create mode 100644 jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.class new file mode 100644 index 0000000000000000000000000000000000000000..68926d9f5d829594ea652c35db44c681840a3e8a GIT binary patch literal 1021 zcmZuvT~8B16g{)ucImP$Enij?r3IxQN)^!;h=Ej0OaP5l6Y#}lJ2Z=Bmu$C0e~P@w z8_)OwMiP1VN2zB@p@xvn+_`(^&OPVeJHP+@`~_eJk4z+yGcayKLoQA;p}bql+%_<2 zB9DTCiv~(2Oyo=$%G|+S15*Og4Ocd50^*s#z=Yjw${=)ouldAn+UpIePSylsbFSxx zj|C$6!W#j-;@6}=-;(RemDbj}3|^^V9&FjJCor6UyR>QV*yV=p)yvf|aJ~Ahx|pbj zw)1}3-fqVmC{sCAl4OIcF3>aQG&)pf)o%rkeCn#i@#;sP!)2ds^Mi^{F#<#R|GILTa<;&}_jQRX4UT{f ztjVSu$lAFy_APAjfc;-Xmh((<{2F){DIk?mMG=V-VS8wY_&3U3D71J4aX^QOX=80r zM;up>p|3*s5a9Nn{6JB8AT?ZGVlK+h+nzaYMg z-eZ`&*L!lnglVSC@R@0Cx*}g4xO&iw1iy6qe3%gfxXQ?J+G&hn9@prBi2j#{nt>66 zkT7uFOeR<~$J|l7LanN>Y>^W5&lfcm&!wuOPgV3or$0s&S*ps>Q@l`#h6(ZYbaKD$ z=ykM`UALd zBs;#TGjs;tK(c1JHZeXY&9)EOU_d)aG5k2sD8TS39Egu8wX8%Slpnrtay7wGa175~Kz!tc ze!3tvPvMpiP4%F`GX(ljog9Efh)e>veR!R9)mi8uxP5_8C8K>tICGB3DdZ8xGoKLF zjxnmnc;py^9caW2d{bKoJQYcVIgfGUIHI(nj1*|&4yz>lrOt7jq!T{r2mUj}?ut*k zz5e}Q;*l<~&zHSCfwqyo%#k?&137Yl&yqJ@DVd}}(40nYgM7o7WQbG9;4V)#9rL-KS&2yFK7h32`V36*|9pM{IK-w#gjR|WtD0#o!FqxXK|C89XA6N`P@I-kIqwS8?%s_c zJew9)(7Y@wdsRP;tQ(rqgdOGTig{+|0)0KL-Mu|8y%G2KAI-DLu!J;2j3mP{QZ63| zTHfhQO!d$ij-53Hw)jZI@92A$m11y|TC>_lzzWd$2P9W-2wtcJ4d0^&9B{)CJK66{ ro665b`8(8K{FwL&+Wsd({=^PXdc2X}z9Ix0UTf}gp1V>4%Pyebsrl(HU(ZeQ-w|hGU8*9=4o{(uy=b`0%tf+ zw4i;S=6YP;PjxX-(~O8+)VUxmD^;cOb*U>sYY=BY=J0Y}7qLD~jnq5Zzf%t?LJL8J zWm7!({B9`d7^a`8{I)-t6