Java object factory: initialize AbstractStringBuilder-derived types correctly #2472
Conversation
This file contains hidden or 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
smowton
requested review from
cesaro,
mgudemann,
peterschrammel and
thk123
as code owners
allredj
reviewed
Jun 25, 2018
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 643e9f1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77258251
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
|
Linking my PR as related to the same type, but I think these are fundamentally different problems. #2479 |
|
Yeah that's different |
smowton
force-pushed
the
smowton/fix/nondet-stringbuilders
branch
from
643e9f1 to
b6fce21
Compare
smowton
force-pushed
the
smowton/fix/nondet-stringbuilders
branch
from
b6fce21 to
4a2013c
Compare
allredj
reviewed
Jun 27, 2018
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 4a2013c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77439595
mgudemann
reviewed
Jun 27, 2018
| --function Test.testme | ||
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| -- |
There was a problem hiding this comment.
test on successful verification?
| /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | ||
| /// Check if a structure is a nondeterministic String structure, and if it is | ||
| /// initialize its length and data fields. | ||
| /// \param struct_expr: struct that we may initialize |
There was a problem hiding this comment.
maybe mark as out parameter
| to_struct_expr(zero_object), ns, symbol_typet(qualified_clsid)); | ||
| to_struct_expr(initial_object), ns, symbol_typet(qualified_clsid)); | ||
|
|
||
| // If the initialised type is a special-cased String type, try to set up |
There was a problem hiding this comment.
maybe elaborate more on what special-cased means here
allredj
approved these changes
Jun 27, 2018
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| -- | ||
| type mismatch |
There was a problem hiding this comment.
I'm not sure I understand what this tests. What was the previous behaviour? The other tests makes sense to me however so I'm still happy.
…orrectly
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.
smowton
force-pushed
the
smowton/fix/nondet-stringbuilders
branch
from
4a2013c to
8e7b6e7
Compare
|
@allredj yep, added a comment. @mgudemann applied your comments. |
allredj
reviewed
Jun 27, 2018
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 8e7b6e7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77490650
mgudemann
approved these changes
Jun 28, 2018
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Aug 22, 2018
6fd77f4 Merge pull request diffblue#2472 from smowton/smowton/fix/nondet-stringbuilders 5423ea4 Merge pull request diffblue#2488 from polgreen/common_call_graph_funcs a2a5662 Merge pull request diffblue#2263 from JohnDumbell/bugfix/nondet_direct_return bbf0d02 Merge pull request diffblue#2482 from antlechner/antonia/direct-children-of-class c982c21 Merge pull request diffblue#2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix 8e7b6e7 Java object factory: initialize AbstractStringBuilder-derived types correctly 9af7ef1 Add tests for new class_hierarchy_grapht functions 79cad15 Fix existing class hierarchy test syntax dbac316 Add documentation to class_hierarchyt 3ecac30 Move non-graph function below graph functions 4badd8f Add useful functions to class_hierarchy_grapht 610467e Merge pull request diffblue#2480 from smowton/smowton/admin/graph-unit-tests 2431ac0 Doxygen formatting for dependence_graph test includes 19a1ceb factor out common call graph unit test functions into header deff59d Add tests for grapht::make_chordal and grapht::connected_subgraphs e94208f Merge pull request diffblue#2428 from tautschnig/vs-ref d00d833 Fix: several grapht functions were uncompilable if ever called b9014de Merge pull request diffblue#2381 from polgreen/depth_limited_search 7c767ab Merge pull request diffblue#2485 from tautschnig/vs-unreachable da76500 JBMC: Fixed asymmetry between synchronized blocks and methods. 5918640 Merge pull request diffblue#2487 from JohnDumbell/bugfix/add_java_load_class d65c655 Merge pull request diffblue#2484 from tautschnig/vs-printf 91e8b89 Fix for nondet replacement on a direct return (pre-remove returns) 904132d unit tests for depth limited search on call graph 2c76d0d call graph helper interface to depth limited search 64fdb9b depht limited search for grapht e708bfb Adds --java-load-class to tests that require it 6665c69 Remove unreachable instructions 6e4d5a7 printf does not and should not have a left-hand side 2111f7c Merge pull request diffblue#2475 from tautschnig/vs-wmm 6566d10 Merge pull request diffblue#2469 from tautschnig/vs-string2 3703974 Merge pull request diffblue#2477 from tautschnig/vs-string-abstraction cf797da Merge pull request diffblue#2473 from tautschnig/vs-update c07a09b Merge pull request diffblue#2476 from tautschnig/vs-cex e504e80 Remove unused parameter in string abstraction 4d88b98 Remove unused parameter in counterexample beautification 888f168 Remove unused parameter from update_scores 461754d Remove unused parameters in goto-instrument/wmm 93300aa Use string2unsigned when reading/expecting an unsigned 1a7033a String refinement: Take a reference to avoid copy git-subtree-dir: cbmc git-subtree-split: 6fd77f4
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.
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_fieldsare 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.
Note to reviewers: this is way easier to review with whitespace changes ignored