Fix stubbed String constructor special case #4495
Conversation
antlechner
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
| if(!is_sub && | ||
| !skip_classid && | ||
| update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) | ||
| // * Always if it has a string type (special case). |
There was a problem hiding this comment.
⛏️ I don't think (special case) is necessary here. Rather an explanation of why strings are a special case would be useful.
There was a problem hiding this comment.
I added a few more lines, with a reference to the function that initialises string fields. Any further documentation should probably go to that function.
| // * Always if it has a string type (special case). | ||
|
|
||
| const bool is_char_sequence = | ||
| java_string_library_preprocesst ::implements_java_char_sequence( |
There was a problem hiding this comment.
⛏️ ❓ Is it customary to have a space before the double colon?
There was a problem hiding this comment.
Huh, clang-format did this, not sure why! I'll fix it as CI is failing with a linting error anyway.
| @@ -801,12 +801,11 @@ void java_object_factoryt::gen_nondet_struct_init( | |||
| struct_type); | |||
| const bool has_length_and_data = | |||
| struct_type.has_component("length") && struct_type.has_component("data"); | |||
| const bool skip_special_string_fields = | |||
| is_char_sequence && has_length_and_data; | |||
| const bool is_string_type = is_char_sequence && has_length_and_data; | |||
There was a problem hiding this comment.
👍 Thanks for changing that. The name was really bad.
antlechner
force-pushed
the
antonia/stubbed-string-constructors
branch
from
f471fd7 to
c6e5552
Compare
For a given struct, the object factory previously checked if it was a string only in the case where skip_classid was set to false and the update strategy was NO_UPDATE_IN_PLACE or MAY_UPDATE_IN_PLACE. This missed some cases, for example the case where no model for String is loaded and the Java method includes a call to a string constructor that depends on a model. In this case the constructor is stubbed and skip_classid is set to true in java_simple_method_stubst. Before this fix, the object factory would go through the components of the string expression as if it was a regular object expression, and hit an invariant violation because the data component is stored as a pointer to an unsignedbv, contradicting the assumption that all pointers point to structs.
There are more decisions associated with this variable than whether or not to skip the length and data fields.
antlechner
force-pushed
the
antonia/stubbed-string-constructors
branch
from
c6e5552 to
9bc1a6e
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 9bc1a6e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107467585
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: c6e5552).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107467525
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
This PR fixes a bug that was caused/uncovered by #4483.
Generally JBMC should only be run on methods that include Strings if a model for String is loaded. However,
--show-propertiesshould work even without the model. After the changes in #4483, in the special case where the Java method includes a call to a String constructor and no model for it was loaded, we didn't check if the object had a string type, and a pointer to an unsignedbv ended up in the pointer case of the object factory, causing an invariant violation. This PR fixes the conditions in the struct case of the object factory so it always checks if the type is a String type, not only whenskip_classidis false.