Skip to content

Object factory: permit null pointers within java.lang.Class #2202

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
Merged
merged 1 commit into from
May 23, 2018
Merged

Object factory: permit null pointers within java.lang.Class #2202

merged 1 commit into from
May 23, 2018

Conversation

smowton
Copy link
Contributor

@smowton smowton commented May 18, 2018

This is in fact required by the Deeptest models library, and is generally sensible if we don't
know whether or not a particular implementation of java.lang.Class should or should not be able
to store null in any particular field. If you're running an implementation that requires them
not null, add a cproverNondetInitialize function to that effect.

This was blocking using implementations that expect a null value from passing initialization.

@smowton
Copy link
Contributor Author

smowton commented May 18, 2018

Note: test-gen had been getting away with this as the special case was bypassed by pointer-type-selector. This was just luck however.

thk123
thk123 reviewed May 21, 2018
View reviewed changes
Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

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

I guess I am missing something here but only one of the two changes makes sense to me.

src/java_bytecode/java_entry_point.cpp Outdated
@@ -94,11 +94,6 @@ static void java_static_lifetime_init(
if(allow_null)
{
irep_idt nameid=sym.symbol_expr().get_identifier();
std::string namestr=id2string(nameid);
Copy link
Contributor

Choose a reason for hiding this comment

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

When can Foo.class field be null? If this is so, I don't think the above test demonstrates it as wasn't the assert already unreachable by the fact we assume Class.field is null (and we used to require it be non-null).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It can't. At some point this was initialising a java.lang.Class *, when the allow_null = false; made sense. Now it's initialising a java.lang.Class (i.e. not a pointer), so it's no longer relevant (the allow_null only has an effect on Class's fields, not the pointer itself, which is created as &java.lang.Integer@class_model (for example) as each reference site)

@thk123
Copy link
Contributor

thk123 commented May 21, 2018

Makes sense - could we get a TG bump when CI is passing here?

@smowton smowton force-pushed the smowton/fix/java-lang-class-fields branch 2 times, most recently from 061f4d5 to cdc9b56 Compare May 21, 2018 14:22
@smowton
Copy link
Contributor Author

smowton commented May 21, 2018

@thk123 done https://github.com/diffblue/test-gen/pull/1833

@smowton smowton force-pushed the smowton/fix/java-lang-class-fields branch from cdc9b56 to febd954 Compare May 22, 2018 14:10
peterschrammel
peterschrammel requested changes May 22, 2018
View reviewed changes
regression/cbmc-java/class-fields/Test.java Outdated
@@ -0,0 +1,10 @@
public class Test {
Copy link
Member

Choose a reason for hiding this comment

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

Move to jbmc/regression/jbmc

Copy link
Member

Choose a reason for hiding this comment

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

More clean up in this respect: #2228

@smowton
Object factory: permit null pointers within java.lang.Class
8a59f6f 
This is in fact required by the Deeptest models library, and is generally sensible if we don't
know whether or not a particular implementation of java.lang.Class should or should not be able
to store null in any particular field. If you're running an implementation that requires them
not null, add a cproverNondetInitialize function to that effect.

This was blocking using implementations that expect a null value from passing initialization.
@smowton smowton force-pushed the smowton/fix/java-lang-class-fields branch from febd954 to 8a59f6f Compare May 23, 2018 07:30
@smowton
Copy link
Contributor Author

smowton commented May 23, 2018

@peterschrammel done.

@smowton
Copy link
Contributor Author

smowton commented May 23, 2018

@thk123 done, looks good.

@smowton smowton merged commit af02973 into diffblue:develop May 23, 2018
NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this pull request Aug 22, 2018
Squashed 'cbmc/' changes from 31ef182..779fa71
aa3c92a 
779fa71 Merge pull request diffblue#2253 from peterschrammel/documentation/override2
40ecff8 Merge pull request diffblue#2250 from tautschnig/expr-iterator-deque
050b344 Re-enable enforcement of override without virtual
b5dec9c Get legalistic about use of override without virtual
b51e2a8 Merge pull request diffblue#2196 from peterschrammel/check-module-includes
d5eabdf expr_iterator: use a std::deque to implement the stack
fada0af Add module dependency definition files
a90ea44 Add module dependency check to CPP-LINT
88f8cfc Remove unnecessary includes
d6986d8 Fix relative include paths
0f9c202 Merge pull request diffblue#2242 from diffblue/section-name-warning
b7f5886 Merge pull request diffblue#2241 from diffblue/ld_mode
5c11eb7 Merge pull request diffblue#2245 from mgudemann/fix/warning/clang_self_assign
f7e5fb5 Merge pull request diffblue#2229 from diffblue/ssize_t
1a504c9 Merge pull request diffblue#2244 from diffblue/solver-Makefile-fix
4bb1bf0 Fix clang++'s warning about self-assign
9a0aa9c Merge pull request diffblue#2235 from thomasspriggs/test-pl-colour
4c2cb3a remove linker mode from gcc_mode
303908f add separate path for ld
524091f factor out creation of hybrid binaries
b9127f3 linker_script_merget now takes exactly one ELF + goto binary
cd967db update year + add Michael
0d95cc5 missing const method qualifiers
6f04d98 fix ordering problem in solvers/Makefile
8f6bae0 remove a warning about section names
8befd02 Merge pull request diffblue#2238 from owen-jones-diffblue/owen-jones-diffblue/doc/irep_id
34b0ac6 Merge pull request diffblue#2236 from diffblue/show-class-hierarchy
8e8e450 Merge pull request diffblue#2232 from owen-jones-diffblue/owen-jones-diffblue/generic-bounded-types
01dc76b Add section on irep_idt and dstringt
2f4c6ad Add and unify --show-class-hierarchy command line option
56256f1 Minor typos in irept documentation
3cf4e3a Merge pull request diffblue#2178 from thomasspriggs/remove_java_bytecode_parse_treet_swap
1a7235d use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJECT/OFFSET
a018e2f Add JSON output for class hierarchy
68c45ed Improve class hierarchy output
eeb732f Switch `push_back` to `emplace_back` when constructing `parse_trees`.
f154840 Delete copy constructor of `class java_bytecode_parse_treet`.
c5cbcec Fix instances where copying was being used instead of moving.
52a669f Remove `java_bytecode::swap` and return using `optionalt` instead.
fabbd04 Give up parsing generic method signature with bound
77f8162 Colour code tests passing vs failing.
e5e0897 Merge pull request diffblue#2126 from danpoe/refactor/sharing-map-small-nodes
f55bd96 Merge pull request diffblue#2231 from smowton/smowton/fix/jbmc-tests
af02973 Merge pull request diffblue#2202 from smowton/smowton/fix/java-lang-class-fields
42a78af JBMC tests: suffix logfiles when using symex-driven loading
af2defd Removed obsolete sharing map unit test
1d7fbd3 Refactor sharing map nodes to reduce memory consumption
5235938 Restore testing of jbmc
8a59f6f Object factory: permit null pointers within java.lang.Class
8412eb0 Merge pull request diffblue#2228 from peterschrammel/move-remaining-java-tests
369577a Move remaining java tests to jbmc/regression/
bfe3d3d Merge pull request diffblue#2226 from tautschnig/inline-get-str-cont
2b00973 Merge pull request diffblue#2227 from tautschnig/fptr-removal
3f7685f Merge pull request diffblue#2223 from diffblue/fp-builtins
3b3dc71 Distinct names of return-value symbols
4f7fade Cleanup: use symbolt::symbol_expr
8372862 function-pointer removal: Set the mode of a return symbol
272cde0 Inline get_string_container
72a0379 test __builtin_isinf, __builtin_isinf_sign, __builtin_isnormal
f156ef0 Merge pull request diffblue#2222 from tautschnig/attributes
a69c603 add __builtin_isnormal
83aeddd added __builtin_isinf_sign
87d467e fix return types of various __builtin_is* functions
61af061 added typecast_exprt::conditional_cast
e1b906a Support GCC's fallthrough attribute
d6d0a49 C front-end: support alias attributes on variables
376beab Merge pull request diffblue#2218 from diffblue/builtin_fpclassify
c3603e3 added a test for raw __builtin_fpclassify
52595bd add support for __builtin_fpclassify
50d1c79 Merge pull request diffblue#2214 from tautschnig/tg-only
3c59312 Remove unused substitute.{h,cpp}
d3e131c Revert "Set memory limit utility"
a4389fe Merge pull request diffblue#2210 from tautschnig/verbosity-cleanup
c250880 Merge pull request diffblue#2211 from tautschnig/travis-osx-cleanup
c8597a4 Merge pull request diffblue#2174 from romainbrenguier/bugfix/not_contains#TG-3150
b08ef94 Merge pull request diffblue#2216 from peterschrammel/update-codeowners
471ab0f Merge pull request diffblue#2207 from diffblue/remove-solvers-cvc
215cd69 Use enum entries instead of numeric values when comparing verbosity
6344b4f Warn if user-specified verbosity is out of range
bf04bcb Use a single implementation of eval_verbosity
b4731eb Do not redundantly set the message handler
42ec63a Clean up .gitignore
19200bf Update CODEOWNERS for /jbmc
0487376 Merge pull request diffblue#2173 from svorenova/gs_tg1121
6af2270 Update regression test that no longer throws an exception
bc17328 Enable previously failing regression tests
146bb29 Adding debug information to dereference type comparison
7b9a20a Allow pointers to be dereferenced to void types
108129c Merge pull request diffblue#2118 from diffblue/remove-jbmc
11411e4 Travis/OSX follow-up cleanup: remove unnecessary environment variables
386faa8 Test for String.contains and very large strings
9e73699 Refactor negation of not contains constraints
29a8818 Build jbmc on CI
f196e74 Update compilation instructions
1b7c84a Add JBMC README
03d6f5b Shorten goto-analyzer-taint-ansi-c tests to goto-analyzer-taint
8dc0d74 Remove obsolete jbmc-cover tests
f36da08 Move Java regression tests
b6742ca Move Java unit tests
e247458 Add JANALYZER tool
4588753 Add JDIFF tool
a20f2c1 Move java_bytecode, jbmc and miniz to jbmc/src
987106f Make unit test independent of java_bytecode
d945452 Adapt cpplint header guard check
28907b2 remove (pre-SMT-LIB) CVC interface

git-subtree-dir: cbmc
git-subtree-split: 779fa71
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@thk123 thk123 thk123 approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@mgudemann mgudemann Awaiting requested review from mgudemann

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening

@tautschnig tautschnig Awaiting requested review from tautschnig

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@smowton @thk123 @peterschrammel