Skip to content

JBMC: Fixed asymmetry between synchronized blocks and methods. #2486

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 27, 2018
Merged

JBMC: Fixed asymmetry between synchronized blocks and methods. #2486

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Binary file modified jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class
View file
Open in desktop
Binary file not shown.
19 changes: 19 additions & 0 deletions jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Binary file modified jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this test doesn't check that line 26 is actually reached. Maybe add a check for the coverage goal (also in the other .desc files).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test is not testing for coverage, see test4.desc.

ATOMIC_BEGIN
ATOMIC_END
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
10 changes: 10 additions & 0 deletions jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
A.class
--function 'A.aStatic' --lazy-methods
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is missing --java-threading so the fact the core models aren't provided isn't relevant (so comment is wrong), I'd duplicate this test one with --java-threading and no models, one without --java-threading and models to check it is all working as expected.

Copy link
Contributor Author

@Degiorgio Degiorgio Jun 26, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This 'java-threading' flag is missing on purpose. Java-threading option requires certain core models, but it is not the case that including the core models requires the java-threading option. There are other pre-existing tests that specifically test that synchronized blocks work as expected with core-models (and java-threading flag). Core models are nothing but additional classes in the class-path as such without the java-threading flag such a test would be useless/duplicate.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So the options are:

  • no core modes and no --java-threading (Tested here)
  • core models and --java-threading (tested elsewhere)
  • --java-threading and no core models (invalid combination so no tests)
  • core models and no --java-threading (I think this could benefit from a test to check nothing unexpected happens just because the symbol java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V is defined.

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
--
Tests that throwing an exception from a synchronization blocks does not cause reachability issues when the java-threading flag is not specified.

16 changes: 11 additions & 5 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1026,8 +1026,6 @@ codet java_bytecode_convert_methodt::convert_instructions(
}

if(i_it->statement=="athrow" ||
i_it->statement=="monitorenter" ||
i_it->statement=="monitorexit" ||
i_it->statement=="putfield" ||
i_it->statement=="getfield" ||
i_it->statement=="checkcast" ||
Expand All @@ -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<unsigned int> handler =
try_catch_handler(i_it->address, method.exception_table);
Expand Down Expand Up @@ -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()))},
Expand Down Expand Up @@ -3099,7 +3102,9 @@ void java_bytecode_convert_method(
bool throw_assertion_error,
optionalt<ci_lazy_methods_neededt> 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),
Expand All @@ -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);
}
Expand Down
3 changes: 2 additions & 1 deletion jbmc/src/java_bytecode/java_bytecode_convert_method.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,8 @@ void java_bytecode_convert_method(
bool throw_assertion_error,
optionalt<ci_lazy_methods_neededt> 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,
Expand Down
5 changes: 4 additions & 1 deletion jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,11 +39,13 @@ class java_bytecode_convert_methodt:public messaget
bool throw_assertion_error,
optionalt<ci_lazy_methods_neededt> 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),
Expand All @@ -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<ci_lazy_methods_neededt> needed_lazy_methods;

/// Fully qualified name of the method under translation.
Expand Down
3 changes: 2 additions & 1 deletion jbmc/src/java_bytecode/java_bytecode_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't work out how this is ever set? Did this flag always exist and just wasn't used?

Copy link
Contributor Author

@Degiorgio Degiorgio Jun 26, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It existed before (and was/is used for other stuff), it is set parse_options if the java-threading flag is specified. The flag is required to analyze multi-threaded programs, if set JBMC does some specialized instrumentation for synchronized methods, slightly changes the behavior of symex (by allowing the handling of unsound pointers), introduces thread-blocks where necessary and as of this commit does some specialized instrumentation for synchronized blocks (before this commit we did instrumentation for synchronized block regardless of this flag)

return false;
}

Expand Down