Before we considered the `code_switch_caset` to belong to the target instruction
which lead to uncoverable goals of the form:
IF condition 1 then GOTO 1
...
1: GOTO 2
ASSERT false // uncoverable block
...
2:
If an enumeration type's values() method clones an array, we assume it is cloning the array of
enumeration values and therefore is bounded by the enumeration's size, similar to the existing
handling of enumeration static initializers.
This enables unwind handlers to use the calling context to decide when to unwind a particular loop,
the first use case being generic array clone methods called from enumeration type methods with known
bounds.
This currently breaks an assertion as described in the .desc file. It should be re-enabled
once string-refinement knows how to introduce sufficient indirection to overcome this.
The local-safe-pointers analysis can already inform symex that certain pointers
are known not to be null at particular program points. This strengthens the analysis
to spot more cases such that it can determine no null pointer is dereferenced in the
new regression test `jbmc/clean_derefs`, which exercises many common Java operations
including array accesses.
The specific improvements to local-safe-pointers:
* Look through typecasts. This was already done for GOTO instructions, but now works
for ASSUME as well.
* Search for not-null expressions using base_type_eq instead of just irept::operator<.
This means that when symex uses namespacet::follow to remove a symbol_typet that does
not prevent local-safe-pointers from noting it is not null in a particular context.
Drops the 'java' prefix from the most important
java command line options. The prefix is not
required anymore since JBMC and CBMC do not
share the same command line interface anymore.
These options are always required in practical
use cases. They can be disabled with --no-lazy-methods
and --no-refine-strings if needed for regression tests.
The symbol table was being passed by-value instead of by-reference to
'instrument_getCurrentThreadID', causing an assertion violation in symex
due to missing symbols. This function is responsible for converting
calls to 'CProver.getCurrentThreadID:()I' into the appropriate codet.
This bug was not detected by existing regression tests as in typical
scenarios the aforementioned function does not add new symbols.
These are currently initialized as if they are directly derived from Object, which causes a crash due to the
type inconsistency between StringBuilder { AbstractStringBuilder { Object { } } } and StringBuilder { Object { } }
With this change they are initialised more like normal types, which has the side-effect that any fields they possess
that are *not* special-cased by `initialize_nondet_string_fields` are nondet-initialized as for any other type.
I add a test verifying this new behaviour, and a simpler test checking that Builder and Buffer are usable as
nondet arguments at all.
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.
If remove returns hasn't been run and the nondet method call was a direct return - return nondetWithoutNull() - an assertion was hit because it couldn't find the destination assignment to add the nondet value too. This change just adds that particular situation in, saying if we can't find an assignment it's likely to be a return and then attempts to look for that.
The logic is also very slightly modified to replace the code of the target instruction instead of destroying it, creating a new one and inserting that directly afterwards.
Using "unsigned" is almost always wrong - the type is unrelated to both the
machine type the code is compiled on as well as the width of the platform we are
running an analysis for.
get_unsigned_int specifically was used inconsistently: the same entry (ID_width)
is set via APIs with a parameter of type size_t and several places already used
get_size_t.
Previously our code was of the form
tmp = x->@class_identifier
is_instanceof = x != null && tmp == "A" || tmp == "B" || ...
This was harmless as the value read from a null pointer was never used if it was null, but
would present a spurious dereference of a possibly-null pointer, introducing false uncertainty
about the vallue of `tmp`. Therefore we now generate:
if x == null:
is_instanceof = false
else:
tmp = x->@class_identifier
is_instanceof = tmp == "A" || tmp == "B" || ...
This uses local_safe_pointerst to determine when symex dereferences a pointer
that cannot be null. When it does the null result is excluded from the possible
values, and therefore a $invalid_object reference may be excluded from the result
of dereferencing such a pointer. This can improve constant propagation.
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'.
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.
'@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.
'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.
Also fixes a number of shortcomings of the earlier approach as far as CMake is
concerned:
- Adds --dirty to the git command line (as is done for Makefiles).
- Does not require a rebuild when there are no changes to the version string.
- CBMC release number updates will be reflected and trigger a rebuild (even when
no other changes have taken place).
Matthias Güdemann