Java generic bounded types in method signatures #2232
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
owen-mc-diffblue
requested review from
cesaro,
chrisr-diffblue,
kroening,
mgudemann,
peterschrammel,
smowton,
tautschnig and
thk123
as code owners
owen-mc-diffblue
changed the title
owen-mc-diffblue
changed the title
smowton
approved these changes
May 24, 2018
owen-mc-diffblue
force-pushed
the
owen-jones-diffblue/generic-bounded-types
branch
from
8c2f7e2 to
4551084
Compare
|
I've rebased now #2231 has been merged and updated the TG bump |
peterschrammel
requested changes
May 24, 2018
| const typet ¶m_type = param.type(); | ||
| REQUIRE(param_type.id() == ID_pointer); | ||
| REQUIRE(param_type.subtype().id() == ID_symbol); | ||
| // REQUIRE( |
There was a problem hiding this comment.
remove commented code or use #if 0 AND add a comment why you deactivate the code (several occurrences)
owen-mc-diffblue
force-pushed
the
owen-jones-diffblue/generic-bounded-types
branch
from
4551084 to
274ebfc
Compare
majakusber
reviewed
May 24, 2018
There was a problem hiding this comment.
This could use a bit more clarification - is it true that before, when seeing bounds, we would keep the function/argument generic but set the bound to Object (which is not correct)? And now, by reverting back to descriptor, we make it non-generic and set it's type to the bound (correct but conservative)? This is a correction but not yet a solution to parsing bounds, so I would refer to the relevant ticket in comments.
| // Not currently working as the bound on type variable is ignored | ||
| REQUIRE( | ||
| id2string(to_symbol_type(param_type.subtype()).get_identifier()) == | ||
| "java::java.lang.Number"); |
There was a problem hiding this comment.
Shouldn't this work? By using descriptor rather than signature, the function is non-generic with argument x of type Number (the method_name above suggests so too). Before your changes, x was a generic parameter T with bound Object. In the ideal (future) case, when we do parse bounds, x will be generic parameter T with bound Number. Do I understand this correctly?
This applies to the other tests too.
There was a problem hiding this comment.
In this case it doesn't work because the generic type and its bound are defined on the class , not on the method, so the changes I've made don't affect it, and it uses the method signature rather than the method descriptor. Apart from that your understanding is correct.
| const typet ¶m_type = param.type(); | ||
| REQUIRE(param_type.id() == ID_pointer); | ||
| REQUIRE(param_type.subtype().id() == ID_symbol); | ||
| #if 0 |
There was a problem hiding this comment.
Rather than if 0, I would just add a comment with a TODO referring to the relevant ticket number that should fix the bounds - TG-1286 perhaps. Similarly in the other tests.
There was a problem hiding this comment.
Okay. I was trying to save someone time in future working out what tests to write when TG-1286 is fixed.
owen-mc-diffblue
force-pushed
the
owen-jones-diffblue/generic-bounded-types
branch
from
274ebfc to
ef4b528
Compare
Bounds on generic type variables are not currently parsed. Previously we were assuming a bound of java.lang.Object. This caused inconsistent types in goto programs. When we find a bounded type variable in a function signature we now give up on trying to parse the generic types and fall back to using the descriptor, which knows about the bounds and gives us type consistency. The problem still occurs when the bounded type variable is defined in a class signature.
owen-mc-diffblue
force-pushed
the
owen-jones-diffblue/generic-bounded-types
branch
from
ef4b528 to
fabbd04
Compare
|
@svorenova, @peterschrammel please re-review. |
|
TG bump has passed, so this can be merged when it has enough reviews |
peterschrammel
approved these changes
May 25, 2018
There was a problem hiding this comment.
Maybe @thk123 has an idea whether there is a 'knownbug' mechanism in catch.
|
There is ( |
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Aug 22, 2018
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is based on top of #2231. I will rebase when that PR is merged.
When we find generic bounded types in method signatures we give up and fall back to using the type from the descriptor. This means we get the bound correct.
@smowton and @thk123 please review.