shift+mask -> concat

[dmwit]

When reading from memory, the new memory model currently reassembles bytes by shifting and masking. If we use bitvector concatenation instead, that will more clearly indicate our intent -- and may lead to better rewrites in what4 and better performance from solvers.