Byte-operator lowering: Add support for byte-extracting unions

[tautschnig]

We already had support for structs, arrays, vectors in place; add unions
following the same approach. This is required for some SV-COMP device
driver benchmarks, including
ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--scsi--qla2xxx--tcm_qla2xxx.ko-entry_point.cil.out.i

• 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: 9384d50).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113362951

[smowton]

Also tests please, including one with multiple like-sized components (e.g. union { double d; uint64_t ul; })

[tautschnig]

Also tests please, including one with multiple like-sized components (e.g. union { double d; uint64_t ul; })

Test added, but note that this code will only be reached when none of the members as a known non-zero size.

[smowton]

Hmm, are you really sure we want to do lifting to the first component if it's the wrong size, rather than just abandoning conversion and doing whatever we did before this code existed?

[tautschnig]

Hmm, are you really sure we want to do lifting to the first component if it's the wrong size, rather than just abandoning conversion and doing whatever we did before this code existed?

No, I'm not sure :-) - but what we did before this code existed is running into a failing invariant that said that this case is unsupported.

[smowton]

Perhaps it would be better to have an invariant that if we're trying to turn a bv[N] into a union { T1 e1; T2 e2; ... } then at least one of T1 ... Tn has the correct size, then we'll know when this code is doing something nonsensical and can address that particular case?

[codecov]

Codecov Report

Base: 78.26% // Head: 78.26% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (7032a1f) compared to base (557624c).
Patch coverage: 100.00% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #4717   +/-   ##
========================================
  Coverage    78.26%   78.26%           
========================================
  Files         1642     1642           
  Lines       189830   189834    +4     
========================================
+ Hits        148568   148575    +7     
+ Misses       41262    41259    -3     

Impacted Files	Coverage Δ
src/solvers/lowering/byte_operators.cpp	92.76% <100.00%> (+0.02%)	⬆️
src/solvers/flattening/boolbv.cpp	87.46% <0.00%> (+0.29%)	⬆️
src/solvers/flattening/arrays.cpp	80.37% <0.00%> (+0.53%)	⬆️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[martin-cs]

Approve but please do have a look at the comments.