Byte extract lowering for vectors and array cleanup [blocks: #2068, #4187] #4124

tautschnig · 2019-02-07T17:47:14Z

Only the last three commits are new, the rest is borrowed from #4123.

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/
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.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

src/solvers/lowering/byte_operators.cpp

allredj

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

tautschnig · 2019-02-14T13:07:45Z

@smowton All comments addressed.

allredj

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

smowton

Looks good, thanks! One comment I think is wrong and a tiny nitpick -- one other thing: can we avoid the back-and-forth between constant_exprt and optional<mp_integer> that happens when we recurse into a member? That seems a little error-prone, as well as expensive.

src/solvers/lowering/byte_operators.cpp

smowton · 2019-02-14T15:17:21Z

src/solvers/lowering/byte_operators.cpp

@@ -111,7 +111,7 @@ static array_exprt unpack_array_vector(
    // recursively unpack each element until so that we eventually just have an
    // array of bytes left
    exprt sub =
-      unpack_rec(element, little_endian, nil_exprt(), max_bytes, ns, true);
+      unpack_rec(element, little_endian, nullopt, max_bytes, ns, true);


Usually {} rather than nullopt

We seem to have a small number of uses, but agreed that {} is more common and thus to be used.

Refactor the code used for arrays to make it re-usable for vectors and arrays.

We already limited extraction at an uppper bound, but when we know the offset we can also start as late as possible. For structs, for example, we now do not expand components that will be irrelevant to the final result.

No need to construct index_exprt when we can just pick the operand out of a vector.

This makes the unit of measurement explicit and thus should help avoid bits/bytes confusion.

This makes the interface much more explicit about what is or isn't supported at moment.

tautschnig · 2019-02-14T15:43:28Z

can we avoid the back-and-forth between constant_exprt and optional<mp_integer> that happens when we recurse into a member? That seems a little error-prone, as well as expensive.

Using optionalt<mp_integer> makes things again much simpler :-) - thanks!

allredj

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

tautschnig added bugfix blocker dependent - do not merge labels Feb 7, 2019

tautschnig requested review from chrisr-diffblue, forejtv, kroening, peterschrammel, smowton and thk123 as code owners February 7, 2019 17:47

tautschnig self-assigned this Feb 7, 2019

allredj reviewed Feb 7, 2019

View reviewed changes

tautschnig force-pushed the byte-op-5 branch from c21e390 to f62cfae Compare February 14, 2019 08:39

tautschnig mentioned this pull request Feb 14, 2019

byte_extract lowering of unions [blocks: #2068] #4187

Merged

3 tasks

smowton reviewed Feb 14, 2019

View reviewed changes

allredj reviewed Feb 14, 2019

View reviewed changes

tautschnig changed the title ~~Byte extract lowering for vectors and array cleanup [depends-on: #4123, blocks: #2068]~~ Byte extract lowering for vectors and array cleanup [blocks: #2068, #4187] Feb 14, 2019

tautschnig removed the dependent - do not merge label Feb 14, 2019

tautschnig force-pushed the byte-op-5 branch 2 times, most recently from ff981ee to 8836523 Compare February 14, 2019 13:07

tautschnig assigned smowton, kroening and peterschrammel and unassigned tautschnig Feb 14, 2019

allredj reviewed Feb 14, 2019

View reviewed changes

smowton approved these changes Feb 14, 2019

View reviewed changes

tautschnig added 4 commits February 14, 2019 15:24

byte_extract lowering of vectors and array cleanup

5c38606

Refactor the code used for arrays to make it re-usable for vectors and arrays.

byte_extract lowering: also use a lower bound

e2265db

We already limited extraction at an uppper bound, but when we know the offset we can also start as late as possible. For structs, for example, we now do not expand components that will be irrelevant to the final result.

byte_extract lowering of arrays: optimise for constant index

2bfaafc

No need to construct index_exprt when we can just pick the operand out of a vector.

byte-operator lowering: rename element_width to {element,component}_bits

445f38f

This makes the unit of measurement explicit and thus should help avoid bits/bytes confusion.

byte_extract lowering: Use optionalt<mp_integer> instead of nil_exprt

bd30790

This makes the interface much more explicit about what is or isn't supported at moment.

tautschnig force-pushed the byte-op-5 branch from 8836523 to bd30790 Compare February 14, 2019 15:43

tautschnig assigned tautschnig and unassigned smowton, kroening and peterschrammel Feb 14, 2019

allredj reviewed Feb 14, 2019

View reviewed changes

tautschnig merged commit e654aa7 into diffblue:develop Feb 14, 2019

tautschnig deleted the byte-op-5 branch February 14, 2019 17:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Byte extract lowering for vectors and array cleanup [blocks: #2068, #4187] #4124

Byte extract lowering for vectors and array cleanup [blocks: #2068, #4187] #4124

Uh oh!

tautschnig commented Feb 7, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Uh oh!

tautschnig commented Feb 14, 2019

Uh oh!

allredj left a comment

Uh oh!

smowton left a comment

Uh oh!

Uh oh!

smowton Feb 14, 2019

Uh oh!

tautschnig Feb 14, 2019

Uh oh!

tautschnig commented Feb 14, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Byte extract lowering for vectors and array cleanup [blocks: #2068, #4187] #4124

Byte extract lowering for vectors and array cleanup [blocks: #2068, #4187] #4124

Uh oh!

Conversation

tautschnig commented Feb 7, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 14, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

smowton Feb 14, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 14, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 14, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!