Vector35 / Vector35/binaryninja-api
Incorrect PVS for armv7 logic right shift lsr
Open
@xusheng6 is already working on this.
Since Jul 30, 2026.
- Dominant language
- C++
- Stars
- 1.3k
- Forks
- 298
- Avg merge
- 5d 5h
- Merged PRs (30d)
- 19
Description
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)
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.