Skip to content

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

Merged
tautschnig merged 1 commit intodiffblue:developfrom
tautschnig:byte-op-strings
Feb 15, 2019
Merged

byte_extract lowering of string constants [blocks: #2068]#4186
tautschnig merged 1 commit intodiffblue:developfrom
tautschnig:byte-op-strings

Conversation

@tautschnig
Copy link
Copy Markdown
Collaborator

@tautschnig tautschnig commented Feb 14, 2019

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
Copy Markdown
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
array.copy_to_operands(op);
}
}
else if(src.id() == ID_string_constant)
Copy link
Copy Markdown
Contributor

@smowton smowton Feb 14, 2019

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
Copy Markdown
Collaborator Author

@tautschnig tautschnig Feb 14, 2019

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
Copy Markdown
Contributor

@smowton smowton Feb 14, 2019

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
Copy Markdown
Collaborator Author

@tautschnig tautschnig Feb 14, 2019

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
Copy Markdown
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

@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

2 more reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

Reviewers whose approvals may not affect merge requirements

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