Simplify (some) big concats

[b-paul]

You may have seen expressions like the following (using boogie syntax):

bvor32(bvand32((((((((((((((((((((((((((((((((bvlshr32(#R19_1209[32:0], 31bv32)[1:0] ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]) ++ bvlshr32(#R19_1209[32:0], 31bv32)[1:0]), 4227858432bv32), bvand32(bvor32(bvand32(bvor32(bvlshr32(#R19_1209[32:0], 6bv32), bvshl32(#R19_1209[32:0], 26bv32)), 4294967295bv32), 0bv32), 67108863bv32))

This is taken from main in cntlm. If we look closely, this is just a concatenation of the same singular bit over and over again! We could just replace it with a repeat.

bvor32(bvand32(repeat32_1(bvlshr32(#R19_1209[32:0], 31bv32)[1:0]), 4227858432bv32), bvand32(bvor32(bvand32(bvor32(bvlshr32(#R19_1209[32:0], 6bv32), bvshl32(#R19_1209[32:0], 26bv32)), 4294967295bv32), 0bv32), 67108863bv32))

But if you think about it, a repeat of a one bit value is the same thing as a sign extend.

bvor32(bvand32(sign_extend31_1(bvlshr32(#R19_1209[32:0], 31bv32)[1:0]), 4227858432bv32), bvand32(bvor32(bvand32(bvor32(bvlshr32(#R19_1209[32:0], 6bv32), bvshl32(#R19_1209[32:0], 26bv32)), 4294967295bv32), 0bv32), 67108863bv32))

But if you think about it even more, we're doing a logical right shift by 31 then taking the first bit, and then sign extending... That's just an arithmetic right shift!

bvor32(bvand32(bvashr32(#R19_1209[32:0], 31bv32), 4227858432bv32), bvand32(bvor32(bvand32(bvor32(bvlshr32(#R19_1209[32:0], 6bv32), bvshl32(#R19_1209[32:0], 26bv32)), 4294967295bv32), 0bv32), 67108863bv32))

I suspect that these big concat chain comes from somewhere in the lifting pipeline not knowing how to handle 32 bit arithmetic shifts nicely. Hopefully the simplification helps somewhere!