Skip to content

byte_extract lowering of string constants [blocks: #2068] #4186

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 1 commit into from
Feb 15, 2019
Merged

byte_extract lowering of string constants [blocks: #2068] #4186

merged 1 commit into from
Feb 15, 2019

Conversation

tautschnig
Copy link
Collaborator

These need to be handled like arrays of characters.

  • 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.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • 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).
  • 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.

smowton
smowton reviewed Feb 14, 2019
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.

AFAIK this is all C, not Java stuff, as particularly shown by the unit test which exhibits strings with char size = 8 (Java chars are 16-bit)

src/solvers/lowering/byte_operators.cpp
@@ -118,6 +119,26 @@ static exprt unpack_rec(
array.copy_to_operands(op);
}
}
else if(src.id() == ID_string_constant)
Copy link
Contributor

Choose a reason for hiding this comment

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

I might be wrong, but I think these are not used by Java, so the commit message may need amending

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Amended to not have that unnecessary restriction, but I do see results of git grep string_constantt in jbmc/ as well...

Copy link
Contributor

Choose a reason for hiding this comment

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

They are used for input and output steps only; the Java bytecode parser makes them to describe string literals, but those are later transformed into references to constant java.lang.String instances, so there are no free-floating constants in the same way as there are in C.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Ah, ok! I guess it must have been some C code where I had seen them in the wild.

@tautschnig tautschnig changed the title byte_extract lowering of (Java) strings [depends-on: #4124] byte_extract lowering of (Java) strings [depends-on: #4124, blocks: #2068] Feb 14, 2019
@tautschnig tautschnig changed the title byte_extract lowering of (Java) strings [depends-on: #4124, blocks: #2068] byte_extract lowering of (Java) strings [blocks: #2068] Feb 14, 2019
@tautschnig tautschnig removed their assignment Feb 14, 2019
@tautschnig tautschnig force-pushed the byte-op-strings branch 2 times, most recently from 4d4e564 to d532a45 Compare February 15, 2019 08:27
@smowton smowton changed the title byte_extract lowering of (Java) strings [blocks: #2068] byte_extract lowering of string constants [blocks: #2068] Feb 15, 2019
@tautschnig
Lowering of byte_extract over string constants
9a67ec4 
These need to be handled like arrays of characters.
allredj
allredj reviewed Feb 15, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 9a67ec4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101065754

@tautschnig tautschnig merged commit 99aabb4 into diffblue:develop Feb 15, 2019
@tautschnig tautschnig deleted the byte-op-strings branch February 15, 2019 10:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

Assignees

@tautschnig tautschnig

Labels
blocker
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@tautschnig @smowton @allredj @kroening @peterschrammel