byte_extract lowering for complex_typet [blocks: #2068]

[tautschnig]

It may have worked before via the fallback to flattening of the entire
expression to a bitvector, but let's be on the safe side and construct
appropriate expressions.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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: 5906993).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101421654

[romainbrenguier]

use move instead

[tautschnig]

How should I use move here given that I need to append to a vector? (The first insert of course should use move as you suggest.)

[romainbrenguier]

std::move(sub_imag.operands().begin(), sub_imag.operands().end(), std::back_inserter(byte_operands));

[tautschnig]

I'm now using std::make_move_iterator as the std::back_inserter would result in repeated reallocations. I hope that's ok as well.

[romainbrenguier]

Yes I think that's fine, otherwise you would have to do a reserve beforehand.

[tautschnig]

@romainbrenguier @smowton All comments addressed.

[smowton]

Looks good except that all the test code is commented. Happy to commit if there's an immediately-following PR that brings the tests in; otherwise suggest doing some interim check that this code is at least exercised.

[tautschnig]

I had to add two small extra commits, but with those we now actually have a successful live test, and not a commented-out one.