Clean member of #3901

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

thk123 merged 4 commits into diffblue:develop from thk123:clean-member-of

Jan 29, 2019

Contributor

thk123 commented Jan 23, 2019

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[n/a] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
[n/a] Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
[n/a] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@romainbrenguier @tautschnig I wasn't able to get the resolve_inherited_componentt to work because it relies on the symbols for the base fields existing, but seemingly they do not at this stage. In the mean time, I applied the clean up comments you two requested on the code that I hoped would be fixed by this.

thk123 requested review from cesaro, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton and tautschnig as code owners

January 23, 2019 17:37

thk123 requested a review from romainbrenguier

January 23, 2019 17:38

tautschnig approved these changes

View reviewed changes

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated

+              /// base class.
+              /// \param pointer: The expression to access the field on.
+              /// \param fieldref: A getfield/setfield instruction produced by the bytecode
+              /// parser.

Collaborator

tautschnig Jan 23, 2019

Nit pick: please indent

romainbrenguier approved these changes

View reviewed changes

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated

               /// parser.
               /// \param ns: Global namespace
               /// \return A member expression accessing the field, through base class
               /// components if necessary.
               static member_exprt
-              to_member(const exprt &pointer, const exprt &fieldref, const namespacet &ns)
+              to_member(const exprt &pointer, const exprt &field_instruction, const namespacet &ns)

Contributor

romainbrenguier Jan 24, 2019

Can we make the type of field_instruction more precise? Is it a member_designatort?
There seems to be some implicit assumption about the expression (for instance it has an ID_class).

Contributor Author

thk123 Jan 24, 2019

@smowton points out here field_instruction is a misleading name since it isn't an instruction - suggests calling it just field_reference, would you be happy with that @romainbrenguier (since you objected to fieldref)?)

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated

                 const exprt typed_pointer =
                   typecast_exprt::conditional_cast(pointer, java_reference_type(class_type));
-                const irep_idt &component_name = fieldref.get(ID_component_name);
+                const irep_idt &component_name = field_instruction.get(ID_component_name);

Contributor

romainbrenguier Jan 24, 2019

Is there a get_component_name that could be used instead?

Contributor Author

thk123 Jan 24, 2019

Thanks for persisting with this, I see there is a fieldref_exprt. To do it properly would take a little time, would you like to get this PR in first as a partial improvement and then I'll follow up with using fieldref_exprt more comprehensively.

Contributor

romainbrenguier Jan 24, 2019

either way is fine for me

thk123 force-pushed the clean-member-of branch from 7e95e1c to 63b1946 Compare

January 24, 2019 09:34

thk123 mentioned this pull request

Use fieldref exprt #3915

Merged

4 tasks

thk123 commented

View reviewed changes

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated Show resolved Hide resolved

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated

               /// parser.
               /// \param ns: Global namespace
               /// \return A member expression accessing the field, through base class
               /// components if necessary.
               static member_exprt
-              to_member(const exprt &pointer, const exprt &fieldref, const namespacet &ns)
+              to_member(const exprt &pointer, const exprt &field_instruction, const namespacet &ns)

Contributor Author

thk123 Jan 24, 2019

@smowton points out here field_instruction is a misleading name since it isn't an instruction - suggests calling it just field_reference, would you be happy with that @romainbrenguier (since you objected to fieldref)?)

thk123 force-pushed the clean-member-of branch from 63b1946 to de4b250 Compare

January 25, 2019 10:55

Contributor Author

thk123 commented Jan 25, 2019

CI failure was due to me being over-eager with a dangling reference. Remaining issues addressed

thk123 force-pushed the clean-member-of branch 2 times, most recently from 6eb4da3 to 56818d6 Compare

January 25, 2019 12:19

tautschnig reviewed

View reviewed changes

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp Outdated

+              /// Build a member exprt for accessing a specific field that may come from a
+              /// base class.
+              /// \param pointer: The expression to access the field on.
+              /// \param field_reference: A getfield/setfield instruction produced by the bytecode

Collaborator

tautschnig Jan 25, 2019

cpplint (rightfully) complains about an overly long line here.

tautschnig assigned thk123


          Add documentation to the member_of function

e4f215c

thk123 force-pushed the clean-member-of branch from ea42084 to 6396ca2 Compare

January 28, 2019 17:18

Contributor Author

thk123 commented Jan 28, 2019 •

edited

Loading

Gah I wish clang-format would reformat comments... Linting addressed)

thk123 added 3 commits

January 28, 2019 17:19


          Rename fieldref to clearer and lint-correct name

09213d3


          Refactor member_of to make while loop clearer

659cc0b


          Remove deprecated call to make_typecast

b863377

thk123 force-pushed the clean-member-of branch from 6396ca2 to b863377 Compare

January 28, 2019 17:20

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 6396ca2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98861766
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

🚫
This PR failed Diffblue compatibility checks (cbmc commit: b863377).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98863209
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

tautschnig unassigned thk123

tautschnig assigned smowton and peterschrammel

smowton reviewed

View reviewed changes

Contributor

smowton left a comment

Personally I'd say the old version was better -- keep the docs of course, but leave the loop the way it was; better to use a loop with a single exit point in the middle than to repeat ns.follow three times per loop just to force the break point to be at the top.

Contributor Author

thk123 commented Jan 29, 2019

@smowton I don't agree, for me the new loop reads more naturally ("while we can't find the component, iterate into the parent"). Do you think there are going to be real performance concerns here or are you happy to be outvoted (@romainbrenguier also prefers this version to the old one)

Contributor

smowton commented Jan 29, 2019

Performance unlikely to be an issue, it's usually bad to be repeating the same work though since at some point somebody will make some change to 2 of the 3 and miss the 3rd or something like that. Assignment in the condition is the usual way out of this sort of loop-and-a-half pattern in C, though here it's a bit verbose (hence previously being spread over a few lines):

while((const auto &accessed_type = type_of(accessed_object)).get_component(component_name).is_nil())

smowton approved these changes

View reviewed changes

Contributor

smowton left a comment

But also, let's not spend any more time thinking about this

thk123 merged commit 764bb42 into diffblue:develop

thk123 deleted the clean-member-of branch

January 29, 2019 17:05

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

tautschnig tautschnig approved these changes

romainbrenguier romainbrenguier approved these changes

allredj allredj left review comments

smowton smowton approved these changes

cesaro Awaiting requested review from cesaro

cristina-david Awaiting requested review from cristina-david

kroening Awaiting requested review from kroening kroening is a code owner

NathanJPhillips Awaiting requested review from NathanJPhillips

peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

pkesseli Awaiting requested review from pkesseli

Labels

None yet