For some reason we were very conservative in our support or abstract
operations over the processor state in the RegisterUse analysis.
In particular, we were failing to process code such as:
r23 := (bv_and r21 (0xfffffffffffffff0 :: [64]))
whose goal is to align the value in r21 at a 16-byte boundary.
This resulted in us failing to analyze some code that was realigning its
stack pointer. With this change, the same code succeeds at propagating
the abstract stack pointer offset forward.
For some reason we were very conservative in our support or abstract operations over the processor state in the
RegisterUse
analysis.In particular, we were failing to process code such as:
r23 := (bv_and r21 (0xfffffffffffffff0 :: [64]))
whose goal is to align the value in r21 at a 16-byte boundary.
This resulted in us failing to analyze some code that was realigning its stack pointer. With this change, the same code succeeds at propagating the abstract stack pointer offset forward.