Java concurrency, support for synchronization #2280

Degiorgio · 2018-06-05T14:12:54Z

PR enables basic support for analyzing concurrent java programs. Specifically, it adds support for synchronized methods, synchronized blocks and multiple regressions tests.

test-gen PR: https://github.com/diffblue/test-gen/pull/1908

tautschnig

Some of my comments I'd normally consider blockers, but really I'm not authoritative on Java.

To help reviewers, please please please be consistent in your code formatting (with the clang-format prescribed one being the preferred style). It's quite distracting as-is.

tautschnig · 2018-06-05T14:17:45Z

jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc

@@ -0,0 +1,7 @@
+KNOWNBUG


Please add a comment that explains what the problem is.

tautschnig · 2018-06-05T14:17:54Z

jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc

@@ -0,0 +1,7 @@
+KNOWNBUG


done. test2.desc and test3.desc do not work due to the same bug. I created another test 'get-current-thread/test_bug.desc' that showcases the issue. I also added comment over there explaining what the issue is exactly.

tautschnig · 2018-06-05T14:19:58Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+/// /param name: base name of the temporary variable, to be append with "_tmp"
+/// /param type: type of the temporary variable
+/// /return returns new variable
+static symbol_exprt tmp_variable(


Use get_fresh_aux_symbol.

tautschnig · 2018-06-05T14:21:59Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+
+  // If the functions for monitorenter or monitorexit do not exist
+  // (this can only happen if the java-models libary was not downloaded).
+  // We implement them as skips because symex would crash, since it cannot find


Any such "crash" (whatever that is) would be a bug and that needs to be fixed. I'm confused.

This is badly worded. If the methods "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V" are not found (this happens when the java-core-models-library is not loaded and the method in question is synchronized). Symex will rightfully complain as it cannot find the symbols associated with function calls to the aforementioned methods (Note: we prevent JBMC from stubbing these methods). To avoid this and thereby ensuring JBMC works with and without the models, we simply replace such calls with skips when the java-core -models-library is not loaded.

Will reword comment to make this clear.

I'll do a PR that adds these symbols.

@kroening In your PR (#2286) you are unconditionally adding the symbols for monitorenter/exit, while what's needed is adding them only when core models cannot be found (or simply returning code_skipt, as this pr is currently doing). Note: that the actual locking mechanism is implemented in these models as such they are not empty stubs.

tautschnig · 2018-06-05T14:25:33Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+
+  // Otherwise we create a function call
+  code_function_callt call;
+  call.function() = symbol_exprt(symbol, type);


That type must be the same that the symbol in the symbol table has, but here you are constructing it from scratch. This is at best redundant.

Your right ofc, done.

tautschnig · 2018-06-05T14:25:57Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+  const irep_idt &statement=code.get_statement();
+  if(statement == ID_return)
+  {
+    // Relace the return with a monitor exit plus return block


Typo: s/Relace/Replace/

tautschnig · 2018-06-05T14:26:45Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+  }
+  else if((statement == ID_label)
+    || (statement == ID_block)
+    || (statement == ID_decl_block))


Unnecessary parentheses

tautschnig · 2018-06-05T14:28:24Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+    // 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");


Is this a magic string?

Yes, it is used to create a unique catch label. It only used locally in that function right now, should it be prefixed with 'CPROVER'?

How would you guarantee that it genuinely is unique? I'd recommend to use some string that cannot possibly be used by a user, for example by using a - somewhere in there.

tautschnig · 2018-06-05T14:29:55Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+/// \param symbol_table: a symbol table
+void convert_synchronized_methods(symbol_tablet &symbol_table)
+{
+  for(auto entry : symbol_table)


const auto &entry

romainbrenguier · 2018-06-06T18:00:28Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+  const typet &type)
+{
+  irep_idt base_name = name + "_tmp";
+  irep_idt identifier = prefix + "::" + id2string(base_name);


addressing by using 'get_fresh_aux_symbol' instead.

romainbrenguier · 2018-06-06T18:02:10Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+/// \param symbol_table: a symbol table
+/// \param is_enter: Indicates whether we are creating a monitorenter or exit.
+/// \param object: An expression representing object  the object that need to
+/// perform a monitorenter/monitorexit operation


there is some mistake in this sentence

romainbrenguier · 2018-06-06T18:02:49Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+/// \param object: An expression representing object  the object that need to
+/// perform a monitorenter/monitorexit operation
+static codet get_monitor_call(
+  symbol_tablet &symbol_table,


Is the symbol_table modified? if no it should be const and if yes it should be documented

no it should be constant. fixing.

romainbrenguier · 2018-06-06T18:03:32Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+  if(is_enter)
+    symbol="java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V";
+  else
+    symbol="java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";


use ternary if

romainbrenguier · 2018-06-06T18:03:43Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+    symbol="java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
+
+  symbol_tablet::symbolst::const_iterator it
+    = symbol_table.symbols.find(symbol);


romainbrenguier · 2018-06-06T18:04:45Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+}
+
+/// Introduces a monitorexit before every return recursively
+/// \param code current element to check


not really checking but rather modifying

Degiorgio · 2018-06-07T15:46:08Z

@tautschnig, @romainbrenguier addressed the issues you raised.

thk123 · 2018-06-08T08:51:31Z

@Degiorgio please put fixes #2307 in a commit message as part of this PR (and preferably add the example as a regression if not already covered by an existing test).

cesaro

Review of the first 4 commits. We need to change the name of the monitor count, and other smaller changes.

cesaro · 2018-06-08T09:38:19Z

jbmc/src/java_bytecode/simple_method_stubbing.cpp

-    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


Explain why they are excluded from being stubbed

cesaro · 2018-06-08T09:54:11Z

jbmc/src/java_bytecode/java_object_factory.cpp

+      // Zero-initialize 'monitorCount' field as it is not meant to be nondet.
+      // 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.


The field monitorCount in our model of java.lang.Object has to be renamed, as otherwise it may conflict with a field with equal name in the code under analysis. I propose cproverMonitorCount.

This modification has been implemented in your 3rd commit. It should be merged to the first commit. Don't forget to modify the commit message on thee 1st commit as well.

cesaro · 2018-06-08T09:57:11Z

jbmc/src/java_bytecode/java_root_class.cpp

+  // 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("monitorCount"))


Update name, as suggested above.

cesaro · 2018-06-08T10:14:59Z

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

+^VERIFICATION SUCCESSFUL$
+--
+--
+tests that synchronization blocks do not cause issues when the java core models library is not loaded


Capitalize the first word, as in previous .desc files.

cesaro

Merge 3rd commit into 1st

cesaro · 2018-06-11T11:19:38Z

jbmc/src/java_bytecode/simple_method_stubbing.cpp

+    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 is only half of the reason. Add , and symex will crash when a function has no formal parameters, or whatever the reason is.

cesaro · 2018-06-11T11:28:29Z

jbmc/src/java_bytecode/java_object_factory.cpp

+      // Zero-initialize 'monitorCount' field as it is not meant to be nondet.
+      // 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.


This modification has been implemented in your 3rd commit. It should be merged to the first commit. Don't forget to modify the commit message on thee 1st commit as well.

cesaro

Review of the last 2 commits: better doxygen and one more tests.

cesaro · 2018-06-11T11:37:28Z

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 \


In the message of previous-last commit, please explain what the behavior of JBMC will be in the presence of a static synchronized method.

cesaro · 2018-06-11T12:07:38Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+/// The resulting thread-safe codet is stored in the value field of \p symbol.
+///
+/// \param symbol_table: a symbol_table
+/// \param symbol: writeable symbol hosting code to synchronized


Typo: to synchronize

cesaro · 2018-06-11T12:10:37Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+{
+  codet &code = to_code(symbol.value);
+
+  // Get interposition code for the monitor lock/unlock


Library interposition is a technique very different from what's going on in here. Rephrase to say something like Get the calls to the functions that implement the lock/unlock mechanism..

cesaro · 2018-06-11T12:15:58Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+/// Transforms the codet stored in in the value field of \p symbol. This
+/// expected to be a codet that needs to be synchronized, the transformation
+/// makes it thread-safe as described in the documentation of function
+/// convert_synchronized_methods


Describe here in pseudocode how the original codet is being transformed into a synchronized block, similar to how we documented the handling of class initializers.

cesaro · 2018-06-11T12:25:22Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h


 #include <util/symbol_table.h>

 void convert_threadblock(symbol_tablet &symbol_table);

+void convert_synchronized_methods(symbol_tablet &symbol_table);


Nit: remove empty line 14?

cesaro · 2018-06-11T12:34:07Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+
+    bool is_static = (symbol.type.get(ID_is_static) == "1");
+    if(is_static)
+      // FIXME: handle static synchronized methods


Ok, static synchronized methods seem to be treated as simply static methods. This will produce many dataraces and unexpected results. Warn the user about this. Example: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/remove_function.cpp#L44

yes as the synchronization semantics for static methods is different (lock on the class instead the object). This is limitation with the current implementation. I have no issues with adding the warning method, but I think it makes more sense to add it outside (where we set the static/synchronized irep flags) such that we don't have to pass around the message handler reference.

Yes, makes sense.
In that case use a PRECONDITION in instrument_synchronized_code to ensure it won't be called with a static synchronized method, and do the warning in this method.

cesaro · 2018-06-11T12:38:11Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+  }
+}
+
+/// Transforms the codet stored in in the value field of \p symbol. This


Nit: value field of \p symbol --> field \c symbol.value

cesaro · 2018-06-11T12:45:19Z

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+}
+
+/// Transforms the codet stored in in the value field of \p symbol. This
+/// expected to be a codet that needs to be synchronized, the transformation


This expected to be ... -> 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.

cesaro · 2018-06-11T12:52:57Z

jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc

+--
+Checks all possible paths to ensure a synchronized method does not end in an illegal monitor state.
+
+This is currently not working as explicit throws have been removed from the underlying model due to performance considerations.


I'm not sure this is a known bug. The code in the .java file should be supported without problem by this PR. What this phrase refers to is the lack of throwing a runtime exception in our model of monitorenter/exit when there are reasons to throw such exceptions (i.e, synchronizing on a null object or calling monitorexit when the counter is 0), but no such conditions are triggered in this test. Therefore this should work.

Am I missing something?

Yes this, test actually works without the exceptions. fixing.

cesaro · 2018-06-11T12:54:40Z

jbmc/regression/jbmc-concurrency/synchronized-methods/A.java

+  {
+    shared++;
+  }
+}


Add a new test with a static synchronized method and declare it as KNOWNBUG

allredj

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

Degiorgio · 2018-06-22T15:36:23Z

@peterschrammel https://github.com/diffblue/test-gen/pull/1908 is passing this can be merged.

cesaro · 2018-06-23T10:57:28Z

Rebased to to latest develop after merges these last days. TG bump also rebased to latest develop. Will merge in some hours if all CIs pass.

allredj

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

tautschnig · 2018-06-23T18:30:19Z

In #2415 I have done some sort of emergency fix of the coreModels test. You will thus need to rebase to resolve the conflict, but I note that #2388 has yet another change proposal to this very same test. @cesaro @peterschrammel please synchronise on this.

peterschrammel · 2018-06-23T18:35:24Z

@cesaro, the java models library label cbmc-5.9 should work with the current cbmc version. HEAD should work with this PR.

cesaro · 2018-06-23T18:41:42Z

@peterschrammel I agree with your reasoning in the message of the commit that fixes the coreModels test in #2388. Now that @tautschnig has temporarily fixed the thing I will just remove my fix here.

Pointing to a specific label of the java core library is orthogonal to this PR, which as you remark, will work with both HEAD and that label in the core library repo.

allredj

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

allredj

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

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.

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

@lock

'@lock' field (fixes diffblue#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.

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.

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

allredj

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

@lock

7c1de91 Merge pull request diffblue#2465 from tautschnig/vs-criteria 9480092 Merge pull request diffblue#2437 from tautschnig/vs-empty a025add Merge pull request diffblue#2463 from tautschnig/vs-xref 0f3d345 Remove unused parameter criteria cdb7e52 Merge pull request diffblue#2453 from tautschnig/vs-deprected-uint bb7607d Merge pull request diffblue#2451 from tautschnig/c++-parser a07639d Merge pull request diffblue#2447 from tautschnig/cpp-regression-tests bdac907 Merge pull request diffblue#2459 from tautschnig/cmake-cleanup 261e883 Merge pull request diffblue#2461 from tautschnig/vs-auto 8acbc6c Merge pull request diffblue#2457 from tautschnig/vs-goto-convert bd2547a Merge pull request diffblue#2458 from tautschnig/vs-long-long fbc56db Remove unnecessarily inlined implementations to otherwise empty cpp file 6adcebc Merge pull request diffblue#2456 from tautschnig/vs-reserve a905ac0 Replace lambda by member function reference to silence Visual Studio ce6a297 Use auto to avoid unnecessary signed/unsigned conversion 79ef045 Deprecate get_unsigned_int c528c25 Remove no-longer-existent-files from exclusion lists in CMake files 4c6fc61 Use long-long integer constant as the left-hand side is long long 7dbf60a Remove unused parameters in goto_convert 0482889 Use reserve instead of generating blank strings 5e5e264 Merge pull request diffblue#2441 from tautschnig/vs-concur 8b03ac1 Merge pull request diffblue#2404 from tautschnig/vs-zero-2 18a3070 Merge pull request diffblue#2454 from tautschnig/vs-code-typet 062a886 Merge pull request diffblue#2408 from tautschnig/vs-set-map ccfc4e0 Merge pull request diffblue#2417 from tautschnig/vs-missing-arg 2bf4097 Merge pull request diffblue#2419 from tautschnig/vs-loc-num 7308bf6 Avoid deprecated code_typet() constructor c2a8fb8 Do not use count() when returning a bool 62ec461 Merge pull request diffblue#2360 from smowton/smowton/fix/dont-deref-null-for-class-identifier-v2 5e1f365 C++ parser: actually use parameters dca5b76 Merge pull request diffblue#2413 from tautschnig/vs-cpp-fix ee2421a Test passes 0cf27c6 type_traits requires C++ 11 660ae90 Remove unused parameter from cpp_destructor and fix types 0784f77 Merge pull request diffblue#2125 from smowton/smowton/feature/symex-ignore-null-derefs 001fca0 Merge pull request diffblue#2280 from cesaro/java-concurrency-synchronization 2369df3 Add message handler to remove_instanceof and _exceptions 419bc1b Java instanceof: avoid dereferencing null pointer 9fd3434 Use local-safe-pointers analysis to improve Symex pointer resolution 8078569 Add local-safe-pointers analysis 0062a9c Merge pull request diffblue#2444 from tautschnig/vs-value-set 68ac566 JBMC: Regression tests for synchronized methods c0ee316 JBMC: Support for synchronized methods 7efa7bf JBMC: Regression tests for multi-threaded java programs 4d91aa5 JBMC: Modified the instrumentation of monitorexit/enter instructions 0691f03 JBMC: Zero-initialized 'cproverMonitorCount' component and removed '@lock' field (fixes diffblue#2307) 0b90c17 JBMC: Moved format_classpath.sh to scripts/format_classpath.sh 2a0d2f9 AppVeyor fix: remove existing clones of the java models library. 0c5a497 Merge pull request diffblue#2446 from tautschnig/vs-unlink f4cb6a9 Merge pull request diffblue#2442 from tautschnig/vs-side 5b12b25 Merge pull request diffblue#2445 from tautschnig/vs-simpl 53e35c2 Move side effect out of conditional aab593b Use C++ standard library function instead of POSIX function f5b465d Simplify code to avoid Visual Studio warnings 7621a86 Remove unused parameter in value_set_analysis d50cec0 Remove unused parameter from concurrency_instrumentationt::instrument 475fe20 Merge pull request diffblue#2393 from tautschnig/git-info-cmake-fixes 5cd87c1 Merge pull request diffblue#2436 from tautschnig/vs-zero b4c0e22 Merge pull request diffblue#2410 from tautschnig/vs-deref-type 662d256 Merge pull request diffblue#2431 from tautschnig/vs-with 1aceb6c Merge pull request diffblue#2391 from diffblue/compilation-instructions 7c894e7 Merge pull request diffblue#2402 from tautschnig/vs-no-dummy 822de57 Merge pull request diffblue#2432 from tautschnig/vs-slice a3fe43b Merge pull request diffblue#2427 from tautschnig/vs-read-bin 0ab38e5 Merge pull request diffblue#2433 from tautschnig/vs-is-zero 95396bc Merge pull request diffblue#2438 from tautschnig/vs-partial 551ab81 Merge pull request diffblue#2411 from tautschnig/vs-message-handler 7464904 Merge pull request diffblue#2424 from tautschnig/vs-template 1feaa94 Merge pull request diffblue#2407 from tautschnig/vs-linker 82c7e48 Remove dummy implementations from propt 209d459 Partial-order concurrency: Remove unused parameter 0e3958a Zero-length array warning is C4200 in Visual Studio ed2cf6a Remove unused parameter from float_bvt::is_zero cb54ae5 Remove unused, empty function a5ecfb4 Remove unused parameters in convert_with_* 373636e Remove parameters that read_bin_goto_object_v3 does not use d6bdee6 Merge pull request diffblue#2369 from polgreen/disconnect_unreachable 0498da9 Merge pull request diffblue#2400 from tautschnig/vs-return-type 2eb9156 Merge pull request diffblue#2406 from tautschnig/vs-sizet1 d5ea06f Merge pull request diffblue#2422 from tautschnig/vs-thread-id 609c934 Merge pull request diffblue#2414 from tautschnig/vs-want 9263e43 Merge pull request diffblue#2403 from tautschnig/vs-zero-1 e638f72 CBMC_VERSION: Use generated include files instead of command-line defines 1360f7f CMake refers to Clang on a Mac as AppleClang f27e724 Merge pull request diffblue#2421 from tautschnig/vs-bound ed98fd7 Merge pull request diffblue#2412 from tautschnig/vs-build 16fa26d Merge pull request diffblue#2405 from diffblue/aws-codebuild-jbmc d7dd598 build jbmc on AWS codebuild 001f684 fix compilation instructions 040fd91 Remove unused parameter dereference_type 6ee60cd Do not unnecessarily convert mp_integer to bounded type d605d56 goto-program instruction's location_number is unsigned 9305ebd Remove unused parameter message_handler 4361cc4 goto-instrument/wmm: add missing argument 6256290 Fix return type of nodes_empty 8c2f6e1 Use std::set instead of map as value is never used bd4faad Use std::size_t instead of int to match types at callsites d07d418 Templatize architecture_string to avoid type conversion 9c72f61 Fix type of thread_id to match goto-trace fb512f0 Remove unused paramter in cpp_typecheck_resolvet 2afa919 Explicitly compare int to zero to avoid Visual Studio warning a1be6c8 Remove unused parameter from local_bitvector_analysist::build 4b5677d Bound the number of attempts my_mkstemps tries to compute a file name b8743fa Merge pull request diffblue#2415 from tautschnig/fix-models d7ef0bc Fix coreModels test to match latest java models library 90c56b3 Merge pull request diffblue#2396 from tautschnig/vs-constructor a45e777 Merge pull request diffblue#2397 from tautschnig/vs-indent 38c7889 Merge pull request diffblue#2399 from tautschnig/vs-defined 8324386 Merge pull request diffblue#2401 from tautschnig/vs-make-constant-rec 1c1562e Merge pull request diffblue#2398 from tautschnig/vs-remove-adjust 2bf9de7 Remove empty function make_constant_rec cdb4075 Use defined(...) when testing for defined-ness of macros bef9866 Remove unused function adjust_lhs_object f0ceaf7 expr2c: indent output of code_deadt 576c0a6 Remove constructor declaration that has no implementation 8f6dab8 Merge pull request diffblue#2261 from thk123/bugfix/TG-3652/wrong-generic-type-two-params 262affb Merge pull request diffblue#2350 from thk123/feature/TG-3813/load-specified-methods 122108a Merge pull request diffblue#2387 from diffblue/fix-dist-scripts 1d461c4 version numbers are now followed by git tag 8f93163 increased version number in preparation for release 5.9 8bc9ecf Merge pull request diffblue#2386 from tautschnig/make-version 7b4b8fe Make's file function is only available from 4.2 onwards ca982a5 Merge pull request diffblue#2373 from tautschnig/git-version-output af880a4 Merge pull request diffblue#2382 from tautschnig/missing-dest e149397 Merge pull request diffblue#2384 from tautschnig/quiet-vs 4b124c8 add centered git version to CBMC banner 718e926 Build .release_info files containing the version string 6416372 windowsify compiler options 23455af Print git revision with all --version outputs 7ca835b Added CBMC_VERSION defines to CMake configuration 783fcea Extend lazy-methods-extra-entry-point to support regex methods 1e55404 CI lazy methods take vector of method loaders 2fb9e21 Add utility for checking two vectors are equal without caring about order e1398bc Add tests for generic type erasure 0c874bf Don't have generic type variables as a comment 1f9a5c4 Adding test about the type bd907a4 Diversified the test for multiple fields 6f98511 Merge pull request diffblue#2335 from thk123/bugfix/load-classes-from-opaque-calls ae1535f Do not print version info when linking using Visual Studio 7e7619c Add missing virtual destructor c0dd633 Merge pull request diffblue#2376 from diffblue/gcc_attributes5_KNOWNBUG 3423e44 gcc/clang treat __attribute__((aligned())) differently c509ece Merge pull request diffblue#2379 from tautschnig/fix-bswap e95f59d Don't instantiate abstract types when they are returned from stubs d7d5f63 Disable lazy loading opaque return for symex driven loading 409d892 Don't forcibly instantiate abstract classes a718893 Adding test to ensure methods on return type of opaque function 20645c9 Add classes to needed classes for parameters and returns for opaque calls 9d42bc8 Move method for gathering all instantiated types into ci_lazy_methods_needed b67ae26 Add can_cast_type for symbol_typet 9981fab Correct doxygen documentation 67c056b Unit test for disconnecting unreachable nodes eca3366 Disconnect unreachable nodes in a graph 3126dea Fix bswap_exprt constructor ac02bbc Merge pull request diffblue#2243 from diffblue/no-warning-ptr-array 0ef77c7 Merge pull request diffblue#2377 from diffblue/fix-tests3 b603a63 make test independent of index type 5ca7410 ignore size of arrays on ptr-to-array conversions git-subtree-dir: cbmc git-subtree-split: 7c1de91

Degiorgio requested review from cesaro, kroening, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners June 5, 2018 14:12

tautschnig reviewed Jun 5, 2018

View reviewed changes

tautschnig mentioned this pull request Jun 6, 2018

add Java monitorenter/exit symbols #2286

Closed

romainbrenguier reviewed Jun 6, 2018

View reviewed changes

Degiorgio force-pushed the java-concurrency-synchronization branch 4 times, most recently from e33c4f1 to ee358d9 Compare June 7, 2018 15:14

Degiorgio changed the title ~~Java concurrency synchronization~~ Java concurrency, support for synchronization Jun 7, 2018

Degiorgio mentioned this pull request Jun 7, 2018

Crash when using core models and comparing two inputs #2307

Closed

cesaro suggested changes Jun 8, 2018

View reviewed changes

Degiorgio force-pushed the java-concurrency-synchronization branch from ee358d9 to e00d56b Compare June 8, 2018 17:03

Degiorgio mentioned this pull request Jun 11, 2018

Add org.cprover.MustNotThrow method attribute #2308

Merged

Degiorgio force-pushed the java-concurrency-synchronization branch 2 times, most recently from 49375de to 5e80f47 Compare June 11, 2018 10:08

cesaro reviewed Jun 11, 2018

View reviewed changes

cesaro suggested changes Jun 11, 2018

View reviewed changes

peterschrammel added the do not merge label Jun 18, 2018

peterschrammel changed the title ~~Java concurrency, support for synchronization~~ [DO NOT MERGE] Java concurrency, support for synchronization Jun 18, 2018

Degiorgio force-pushed the java-concurrency-synchronization branch from 2dc4dc8 to d42722c Compare June 21, 2018 11:58

allredj reviewed Jun 21, 2018

View reviewed changes

Degiorgio changed the title ~~[DO NOT MERGE] Java concurrency, support for synchronization~~ Java concurrency, support for synchronization Jun 22, 2018

cesaro force-pushed the java-concurrency-synchronization branch from d42722c to 86b25dc Compare June 23, 2018 10:32

cesaro force-pushed the java-concurrency-synchronization branch 2 times, most recently from e52abcb to 488bce6 Compare June 23, 2018 15:26

allredj reviewed Jun 23, 2018

View reviewed changes

cesaro mentioned this pull request Jun 23, 2018

Use submodule to download java-models-library #2426

Merged

cesaro force-pushed the java-concurrency-synchronization branch from 488bce6 to d770bb9 Compare June 23, 2018 18:45

allredj reviewed Jun 23, 2018

View reviewed changes

cesaro force-pushed the java-concurrency-synchronization branch from d770bb9 to ce2e85e Compare June 24, 2018 13:16

allredj reviewed Jun 24, 2018

View reviewed changes

Degiorgio and others added 7 commits June 24, 2018 15:35

JBMC: Regression tests for multi-threaded java programs

7efa7bf

JBMC: Regression tests for synchronized methods

68ac566

Degiorgio force-pushed the java-concurrency-synchronization branch from ce2e85e to 68ac566 Compare June 24, 2018 14:35

allredj reviewed Jun 24, 2018

View reviewed changes

cesaro merged commit 001fca0 into diffblue:develop Jun 24, 2018

Java concurrency, support for synchronization #2280

Java concurrency, support for synchronization #2280

Conversation

Degiorgio commented Jun 5, 2018 • edited Loading

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jun 7, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jun 6, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jun 6, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Jun 6, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio commented Jun 7, 2018 • edited Loading

thk123 commented Jun 8, 2018

cesaro left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cesaro left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cesaro left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cesaro Jun 11, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio commented Jun 5, 2018 •

edited

Loading

Degiorgio Jun 7, 2018 •

edited

Loading

Degiorgio Jun 6, 2018 •

edited

Loading

Degiorgio Jun 6, 2018 •

edited

Loading

Degiorgio Jun 6, 2018 •

edited

Loading

Degiorgio commented Jun 7, 2018 •

edited

Loading

cesaro Jun 11, 2018 •

edited

Loading