00000000 sub_0:
00000000 mov r0, #0xff000000
00000004 lsr r0, r0, #0x20 {0xff000000}
00000008 bx lr
bytes: ff04a0e32000a0e11eff2fe1
For the above code, our PVS believes the result of r0 is 0xff000000. But on real armv7 hardware it become 0x0 because 0x20 (32) is wider than the input operand.
The cause is rather obscure -- the armv7 lifting is fine, but in the core PVS we always mask such shifts according to the way x86 works. (Coincidentally it also works for arm64, bc there is no instruction that does 1- or 2- byte right shift on arm64, otherwise it will also be broken)
bytes:
ff04a0e32000a0e11eff2fe1For the above code, our PVS believes the result of
r0is 0xff000000. But on real armv7 hardware it become 0x0 because 0x20 (32) is wider than the input operand.The cause is rather obscure -- the armv7 lifting is fine, but in the core PVS we always mask such shifts according to the way x86 works. (Coincidentally it also works for arm64, bc there is no instruction that does 1- or 2- byte right shift on arm64, otherwise it will also be broken)