Analysis&transform to make region value type match the load/store to access size and alignment

[ailrst]

Description

When accesses to a region are aligned and always greater than a bitwidth greater than a byte we can increase the value size in the region maps to this width, e.g. we can have a region map bv32[bv64] if we only ever load/store bv32 from the region.

The analysis should be possible with a congruence and interval domain after the region transform. The known-bits domain would also work by showing that n low bits are known to be always zero, meaning the number is congruent to the 2^i, where i is the least-significant bit not known to be zero. SASI would also work.

Motivation

This helps along the CHC solver @aaronbembenek uses for invariant generation, and should also improve the performance in Boogie, as it seems to struggle to reason through the byte concatenation in loads and stores.