String preprocessing: don't re-initialise objects that already exist #3545
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,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
allredj
reviewed
Dec 7, 2018
| @@ -826,24 +826,37 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( | |||
| const exprt &lhs, | |||
| const exprt &rhs_array, | |||
| const exprt &rhs_length, | |||
| const symbol_table_baset &symbol_table) | |||
| const symbol_table_baset &symbol_table, | |||
| bool is_constructor) | |||
| @@ -1083,14 +1097,14 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call( | |||
| const java_method_typet &type, | |||
| const source_locationt &loc, | |||
| symbol_table_baset &symbol_table, | |||
| bool ignore_first_arg) | |||
| bool is_constructor) | |||
| @@ -857,10 +870,11 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( | |||
| codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( | |||
| const exprt &lhs, | |||
| const refined_string_exprt &rhs, | |||
| const symbol_table_baset &symbol_table) | |||
| const symbol_table_baset &symbol_table, | |||
| bool is_constructor) | |||
| struct_rhs.copy_to_operands(rhs_array); | ||
| return code_assignt( | ||
| checked_dereference(lhs, lhs.type().subtype()), struct_rhs); | ||
| if(is_constructor) |
There was a problem hiding this comment.
Documenting the "why" would be useful.
smowton
force-pushed
the
smowton/fix/string-refinement-dont-reinit-object
branch
from
8322911 to
655a788
Compare
Just set their length and data fields, leaving the others alone; otherwise it will overwrite taint fields, as well as lock fields and anything else introduced to java.lang.Object.
smowton
force-pushed
the
smowton/fix/string-refinement-dont-reinit-object
branch
from
655a788 to
e6fca9b
Compare
allredj
reviewed
Dec 10, 2018
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: e6fca9b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94196111
|
@allredj take a look at |
peterschrammel
approved these changes
Dec 11, 2018
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.
Just set their length and data fields, leaving the others alone; otherwise it will overwrite any fields stored on java.lang.Object with their initialiser value.
This should not change any behaviour in cbmc / test-gen; it only has an effect when java.lang.Object has been augmented with extra fields, as we do to track taint, and I know the concurrency work has done to better model locks.