Byte extract lowering: support extracting non-byte-aligned arrays

[tautschnig]

Alignment to bytes may be true for ANSI C, but isn't the case for our C front-end (which supports arrays of single bits), and not true for the overall framework in general. This required fixing alignment assumptions both in unpack_array_vector (which turns an arbitrary type into an array of bytes) as well as lower_byte_extract_array_vector (which picks an array/vector of arbitrary subtype from an array of bytes as prepared by unpack_array_vector).

Depends on #6486, which is the first commit in here. Only the second commit is new.

• 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.

[codecov]

Codecov Report

Patch coverage: 97.27% and no project coverage change.

Comparison is base (6f3c16c) 79.00% compared to head (c8b7465) 79.01%.
Report is 2 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #6488   +/-   ##
========================================
  Coverage    79.00%   79.01%           
========================================
  Files         1697     1697           
  Lines       195369   195442   +73     
========================================
+ Hits        154350   154421   +71     
- Misses       41019    41021    +2     

Files Changed	Coverage Δ
src/util/lower_byte_operators.cpp	92.09% <96.87%> (+0.22%)	⬆️
unit/util/lower_byte_operators.cpp	100.00% <100.00%> (ø)

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[martin-cs]

I see why this is needed and why it is useful and I cannot see anything wrong with it. However, this kind of code is very prone to "off by one" type errors and is a nightmare to diagnose and fix. So... please can we have a high degree of test coverage? I realise you probably can't measure that until #6486 is merged but when you can, some test cases, maybe a union of an array of bits and a struct of some kind?

[martin-cs]

I vaguely recall some hero going around and replacing all of the (appropriate) instances of 8 with CHAR_BITS. Should we call on him again?

[kroening]

I am reluctant to add more functionality to byte_extract/byte_update, given that these are already the most complicated expressions we have (maybe floating-point stuff can compete).

Would it make sense to separate the aspect of "extract some bytes from byte-aligned memory" from "map some non-byte-aligned encoding to a byte-aligned memory layout"? This might also help with the fat pointers.

[tautschnig]

I am reluctant to add more functionality to byte_extract/byte_update, given that these are already the most complicated expressions we have (maybe floating-point stuff can compete).

I hear you, but I would like to clarify that this PR really only adds functionality to lowering; the propositional back-end will already get this case right (though perhaps has an easier time doing so). It's been a while that I prepared this PR, but I think the reasons it came up were attempts to support more cases of non-det pointers, which just meant that cases that I previously was too lazy to implement were now triggered.

Would it make sense to separate the aspect of "extract some bytes from byte-aligned memory" from "map some non-byte-aligned encoding to a byte-aligned memory layout"? This might also help with the fat pointers.

The architecture of the lowering implementation is of such nature, although it might not help that it's all baked into a single file. Any byte-extract or byte-update will first turn the underlying object into a byte array, and will then do all further operations on such a an array of bytes.

[kroening]

I am still not convinced of the use-case: there shouldn't be pointers into bit-arrays.

[peterschrammel]

Isn't this in conflict with #7298?