Conditions Analysis

[l-kent]

It would be useful to have an analysis that can provide more useful information about branch conditions. Branch conditions check the status register flags according to the following:

https://developer.arm.com/documentation/dui0801/l/Condition-Codes/Condition-code-suffixes-and-related-flags

It is then necessary to check how the relevant status register flags were set in order to determine what the condition is at a slightly higher level.

This should not be too complicate to implement - it should mostly be about identifying the patterns - typically there is a cmp instruction which sets the flags, followed by a b.cond instruction which branches on the results.

This pseudocode (slightly modified BIR with the arm assembly annotated) helps to explain the problem:

// cmp w0, #12
#4 := 31:0[R0] - 12
VF := extend:33[#4 + 1] <> extend:33[31:0[R0]] - 0xB
CF := pad:33[#4 + 1] <> pad:33[31:0[R0]] + 0xFFFFFFF5
ZF := #4 + 1 = 0
NF := 31:31[#4 + 1]
// b.hi
goto %0000042a, %00000439

%0000042a
assume (CF & ~ZF)
...

%00000439
assume !(CF & ~ZF)
...

Because this is a HI branch (checking if CF is set and ZF is clear), it means that it's doing an unsigned greater than comparison, so it's branching if R0 > 12 (since those were the values being compared).

It may potentially make more sense to handle this problem at the lifter level though, I'm not sure.