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

Degiorgio · 2018-06-26T14:38:51Z

Previously, the conversion of synchronized methods only took place if
the --java-threading flag is specified, while in the case of
synchronized blocks the conversion is undertaken with and without the
aforementioned flag. This commit fixes this asymmetry by replacing
the instructions monitorenter and moinitorexit with code_skipt if
the 'java-threading' option is not specified (instead of instrumenting
calls to 'java::java.lang.Object.monitorexit/enter').

The 'monitorenter' and monitiorexit instructions are also replaced with
a 'code_skipt' if the Java-core-models library is not loaded. This
prevents JBMC from outputting missing function-body warnings.

Commit also modifies relevant regression tests.

Degiorgio · 2018-06-26T15:04:37Z

Note for reviewers: clang-format is complaining, the code that it is complaining about is small change in 'convert_instructions', this large function does not follow the clang-format style and thus for the sake of consistency I left it as is.

cesaro · 2018-06-26T15:29:59Z

Pointer bump in TG: https://github.com/diffblue/test-gen/pull/1987

allredj

Passed Diffblue compatibility checks (cbmc commit: 85a3a96).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77355924

thk123

I'm kind of confused how it all works and would appreciate one extra test, but otherwise LGTM

thk123 · 2018-06-26T16:20:33Z

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1040,7 +1040,8 @@ bool java_bytecode_languaget::convert_single_method(
      throw_assertion_error,
      std::move(needed_lazy_methods),
      string_preprocess,
-      class_hierarchy);
+      class_hierarchy,
+      threading_support);


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

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)

thk123 · 2018-06-26T16:22:14Z

jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc

@@ -0,0 +1,9 @@
+CORE
+A.class
+--function 'A.aStatic' --lazy-methods


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.

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.

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.

allredj

Can't see any major problem, but I'd be interested in the answer to @thk123's question.

allredj · 2018-06-26T16:24:20Z

jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading


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).

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

Previously, the conversation of synchronized methods only took place if the 'java-threading' flag is specified, while in the case of synchronized blocks the conversation is undertaken with and without the aforementioned flag. This commit fixes this asymmetry by replacing the instructions 'monitorenter' and 'moinitorexit' with 'code_skipt' if the 'java-threading' option is not specified (instead of instrumenting calls to 'java::java.lang.Object.monitorexit/enter'). The 'monitorenter' and monitiorexit instructions are also replaced with a 'code_skipt' if the Java-core-models library is not loaded. This prevents JBMC from outputting missing function-body warnings. Commit also modifies relevant regression tests.

Degiorgio · 2018-06-26T17:01:46Z

@thk123 addressed your complaints.

allredj

Passed Diffblue compatibility checks (cbmc commit: da76500).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77371338

kroening · 2018-06-27T08:38:37Z

I am overall unhappy about the fact that the font-end gets configured to support/not support concurrency. That should not be near the language front-end.

cesaro · 2018-06-27T08:57:42Z

In our view the option is not meant to stay, it is meant to disappear after the support for concurrency in Java is more mature. No such option exists for C, it shouldn't exist for Java.

thk123 · 2018-06-27T09:42:17Z

jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc

@@ -0,0 +1,9 @@
+CORE
+A.class
+--function 'A.aStatic' --lazy-methods


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.

thk123 · 2018-06-27T12:36:45Z

@kroening Are you happy with what @cesaro has said? (I would like to merge this).

6fd77f4 Merge pull request diffblue#2472 from smowton/smowton/fix/nondet-stringbuilders 5423ea4 Merge pull request diffblue#2488 from polgreen/common_call_graph_funcs a2a5662 Merge pull request diffblue#2263 from JohnDumbell/bugfix/nondet_direct_return bbf0d02 Merge pull request diffblue#2482 from antlechner/antonia/direct-children-of-class c982c21 Merge pull request diffblue#2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix 8e7b6e7 Java object factory: initialize AbstractStringBuilder-derived types correctly 9af7ef1 Add tests for new class_hierarchy_grapht functions 79cad15 Fix existing class hierarchy test syntax dbac316 Add documentation to class_hierarchyt 3ecac30 Move non-graph function below graph functions 4badd8f Add useful functions to class_hierarchy_grapht 610467e Merge pull request diffblue#2480 from smowton/smowton/admin/graph-unit-tests 2431ac0 Doxygen formatting for dependence_graph test includes 19a1ceb factor out common call graph unit test functions into header deff59d Add tests for grapht::make_chordal and grapht::connected_subgraphs e94208f Merge pull request diffblue#2428 from tautschnig/vs-ref d00d833 Fix: several grapht functions were uncompilable if ever called b9014de Merge pull request diffblue#2381 from polgreen/depth_limited_search 7c767ab Merge pull request diffblue#2485 from tautschnig/vs-unreachable da76500 JBMC: Fixed asymmetry between synchronized blocks and methods. 5918640 Merge pull request diffblue#2487 from JohnDumbell/bugfix/add_java_load_class d65c655 Merge pull request diffblue#2484 from tautschnig/vs-printf 91e8b89 Fix for nondet replacement on a direct return (pre-remove returns) 904132d unit tests for depth limited search on call graph 2c76d0d call graph helper interface to depth limited search 64fdb9b depht limited search for grapht e708bfb Adds --java-load-class to tests that require it 6665c69 Remove unreachable instructions 6e4d5a7 printf does not and should not have a left-hand side 2111f7c Merge pull request diffblue#2475 from tautschnig/vs-wmm 6566d10 Merge pull request diffblue#2469 from tautschnig/vs-string2 3703974 Merge pull request diffblue#2477 from tautschnig/vs-string-abstraction cf797da Merge pull request diffblue#2473 from tautschnig/vs-update c07a09b Merge pull request diffblue#2476 from tautschnig/vs-cex e504e80 Remove unused parameter in string abstraction 4d88b98 Remove unused parameter in counterexample beautification 888f168 Remove unused parameter from update_scores 461754d Remove unused parameters in goto-instrument/wmm 93300aa Use string2unsigned when reading/expecting an unsigned 1a7033a String refinement: Take a reference to avoid copy git-subtree-dir: cbmc git-subtree-split: 6fd77f4

Degiorgio requested review from cesaro, mgudemann, peterschrammel, smowton and thk123 as code owners June 26, 2018 14:38

allredj reviewed Jun 26, 2018

View reviewed changes

thk123 reviewed Jun 26, 2018

View reviewed changes

allredj reviewed Jun 26, 2018

View reviewed changes

Degiorgio force-pushed the jbmc-synchronoization-asymmetry-fix branch from 85a3a96 to da76500 Compare June 26, 2018 16:58

allredj reviewed Jun 26, 2018

View reviewed changes

peterschrammel approved these changes Jun 26, 2018

View reviewed changes

thk123 approved these changes Jun 27, 2018

View reviewed changes

thk123 merged commit c982c21 into diffblue:develop Jun 27, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

Degiorgio commented Jun 26, 2018 •

edited by cesaro

Loading

Degiorgio commented Jun 26, 2018 •

edited

Loading

cesaro commented Jun 26, 2018

allredj left a comment

thk123 left a comment

thk123 Jun 26, 2018

Degiorgio Jun 26, 2018 •

edited

Loading

thk123 Jun 26, 2018

Degiorgio Jun 26, 2018 •

edited

Loading

thk123 Jun 27, 2018

allredj left a comment

allredj Jun 26, 2018

Degiorgio Jun 26, 2018

Degiorgio commented Jun 26, 2018

allredj left a comment

kroening commented Jun 27, 2018

cesaro commented Jun 27, 2018

thk123 Jun 27, 2018

thk123 commented Jun 27, 2018 •

edited

Loading

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

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

Conversation

Degiorgio commented Jun 26, 2018 • edited by cesaro Loading

Degiorgio commented Jun 26, 2018 • edited Loading

cesaro commented Jun 26, 2018

allredj left a comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

thk123 Jun 26, 2018

Choose a reason for hiding this comment

Degiorgio Jun 26, 2018 • edited Loading

Choose a reason for hiding this comment

thk123 Jun 26, 2018

Choose a reason for hiding this comment

Degiorgio Jun 26, 2018 • edited Loading

Choose a reason for hiding this comment

thk123 Jun 27, 2018

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj Jun 26, 2018

Choose a reason for hiding this comment

Degiorgio Jun 26, 2018

Choose a reason for hiding this comment

Degiorgio commented Jun 26, 2018

allredj left a comment

Choose a reason for hiding this comment

kroening commented Jun 27, 2018

cesaro commented Jun 27, 2018

thk123 Jun 27, 2018

Choose a reason for hiding this comment

thk123 commented Jun 27, 2018 • edited Loading

Degiorgio commented Jun 26, 2018 •

edited by cesaro

Loading

Degiorgio commented Jun 26, 2018 •

edited

Loading

Degiorgio Jun 26, 2018 •

edited

Loading

Degiorgio Jun 26, 2018 •

edited

Loading

thk123 commented Jun 27, 2018 •

edited

Loading