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

[ailrst]

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.

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.

The analysis should be possible with a congruence and interval domain after the region transform. Possibly just the sasi domain.