Skip to content

Crash when using core models and comparing two inputs #2307

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

Jump to bottom
Closed
thk123 opened this issue Jun 7, 2018 · 1 comment
Closed

Crash when using core models and comparing two inputs #2307

thk123 opened this issue Jun 7, 2018 · 1 comment
Labels
pending merge

Comments

@thk123
Copy link
Contributor

thk123 commented Jun 7, 2018

Given the following Java:

class Test2Class {
  static void test(Object a, Object b) {
    assert(a == b);
  }
}

When running jbmc with the core models: jbmc Test2Class.class --function Test2Class.test --classpath ../../../src/java_bytecode/library/core-models.jar:.

The following error is generated:

struct: component type does not match: signedbv
  * width: 32
  * #c_type: signed_int vs. 
terminate called after throwing an instance of 'int'
Aborted (core dumped)

The component that is specifically the wrong type is monitorCount from java.lang.Object model.
@Degiorgio
Copy link
Contributor

Degiorgio commented Jun 7, 2018 •
edited
Loading

The following PR when merged should fix this: #2280

Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 8, 2018
@Degiorgio
JBMC: Zero-initialized 'monitorCount' component (fixes diffblue#2307)
897b197 
The 'monitorCount' 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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 13, 2018
@Degiorgio
JBMC: Zero-initialized 'monitorCount' component (fixes diffblue#2307)
062b97a 
The 'monitorCount' 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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 13, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
621f02e 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 13, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
5d61696 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 14, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
49cb5b6 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 14, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
6f84969 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 14, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
ba86208 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 14, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
eee360f 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 15, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
d5987c1 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 15, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
8780176 
'@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.
Degiorgio added a commit to cesaro/cbmc that referenced this issue Jun 21, 2018
@Degiorgio
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
a2a7dfb 
'@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.
cesaro pushed a commit to cesaro/cbmc that referenced this issue Jun 23, 2018
@Degiorgio @cesaro
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
0b2ecbb 
'@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.
cesaro pushed a commit to cesaro/cbmc that referenced this issue Jun 23, 2018
@Degiorgio @cesaro
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
a0091a9 
'@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.
cesaro pushed a commit to cesaro/cbmc that referenced this issue Jun 23, 2018
@Degiorgio @cesaro
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
3ffc276 
'@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.
cesaro pushed a commit to cesaro/cbmc that referenced this issue Jun 24, 2018
@Degiorgio @cesaro
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
4a423f2 
'@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.
@cesaro cesaro closed this as completed in 0691f03 Jun 24, 2018
polgreen pushed a commit to polgreen/cbmc that referenced this issue Jul 5, 2018
@Degiorgio @polgreen
JBMC: Zero-initialized 'cproverMonitorCount' component and removed
6574a82 
'@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.
NathanJPhillips added a commit to NathanJPhillips/cbmc that referenced this issue Aug 22, 2018
@NathanJPhillips
Squashed 'cbmc/' changes from 8a7893c..7c1de91
04b23a8 
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@thk123 @tautschnig @Degiorgio