Skip to content

Fix/bytecode args write from stack #951

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
merged 8 commits into from
Jun 18, 2017
Merged

Fix/bytecode args write from stack #951

merged 8 commits into from
Jun 18, 2017

Conversation

mgudemann
Copy link
Contributor

alternative to #931 ; as suggested by @smowton instead of adding temporary variables for load operations, this adds temporary variables on store, and also filters for types of operations and variable names.

@mgudemann mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from 84cc74b to b3e4296 Compare May 23, 2017 07:32
@mgudemann mgudemann requested review from smowton and tautschnig May 23, 2017 07:33
@mgudemann
Copy link
Contributor Author

still needs a regression test for ?astore

smowton
smowton approved these changes May 23, 2017
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Broadly looks good, a few specific suggestions, plus perhaps you could factor the stack backup routines into something like backup_stack_aliases (some_predicate) where the predicate differs by instruction type, looking for field or symbol or local variable references as appropriate?

regression/cbmc-java/LocalVarTable5/test.desc Outdated
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can use [0-9] for this

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

regression/cbmc-java/stack_var10/test.desc Outdated
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remove this (it will match any line)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably while. I certainly try not to introduce double casts, but there are probably still places where they get introduced.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might as well compare the member names like the symbol comparison above?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is done in the refactored code

@mgudemann mgudemann mentioned this pull request May 23, 2017
Closed
tautschnig
tautschnig requested changes May 24, 2017
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lots of mostly minor comments, but having repeated the very same comments 4-5 times makes me feel very uneasy about this. It seems a refactoring would be necessary.

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there any reason not to use a ranged for here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I refactored the code, please have a look

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As above

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Again: ranged for?

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As above: code_assignt assign(tmp_var, stack_entry);

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

code_assignt assign(var, toassign);

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Make that code more similar to the above by introducing a temporary variable, which will then also have the source location assigned.

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ranged for

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As above

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ranged for

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

code assignt assign(tmp_var, stack_entry);

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

@mgudemann mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from b3e4296 to ed0b3b1 Compare May 24, 2017 16:27
@mgudemann mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from ed0b3b1 to 8b4e2e9 Compare May 24, 2017 16:40
smowton
smowton approved these changes May 24, 2017
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

tautschnig
tautschnig reviewed May 25, 2017
View reviewed changes
src/java_bytecode/java_bytecode_convert_method.cpp Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use .get_component_name()

tautschnig
tautschnig approved these changes May 25, 2017
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just one minor API-usage suggestion, but otherwise looks good. Thanks a lot for all the refactoring!

Add temporary variables for values on stack for write operations
0ce085f 
concerned bytecode instructions:
 - iinc
 - pustatic
 - putfield
 - ?store
 - ?astore
@mgudemann mgudemann force-pushed the fix/bytecode_args_write_from_stack branch from 3e52f89 to 0ce085f Compare May 25, 2017 13:25
@mgudemann
Copy link
Contributor Author

all fixed

@tautschnig tautschnig mentioned this pull request May 26, 2017
Closed
@kroening kroening merged commit a71dfb5 into diffblue:master Jun 18, 2017
@mgudemann mgudemann deleted the fix/bytecode_args_write_from_stack branch July 1, 2018 08:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnig tautschnig tautschnig approved these changes

+1 more reviewer

@smowton smowton smowton approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@kroening kroening

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mgudemann @smowton @tautschnig @kroening