[llvm-dev] Reasoning about known bits of the absolute value of a signed integer

[Sanjoy Das via llvm-dev]

Hi Carlos,

I made a notational mistake here, ABS everywhere should be NEG (i.e. negate).  To get ABS from Neg, you should be able 
to do:

ABS({A,B}) = if A.hasSignBitSet(): {A, B}  // positive
              else if B.hasSignBitSet(): NEG({A,B})  // negative
              else {
                {P, Q} = NEG({A, B})
                return {P & Q, Q & B}
              }

Or something better.

-- Sanjoy




>
> Giving:
>
> Let {A, B} denote the approximation KnownZero = A, KnownOne = B
>
> ApproxABS({A, B}) == ApproxIncrement(ApproxNot({A, B}))
>
> == ApproxIncrement(({B, A}))
>
> `ApproxIncrement` is a little trickier:
>
> Carry = 1; // since we're adding 1. This can be 0, 1 or unknown
> for i = 0 to wordSize-1:
> if KnownZero[i]:
> if Carry is 1:
> Result.KnownOne[i] = 1
> else if Carry is 0:
> Result.KnownZero[i] = 1
> Carry = 0
> continue // never any carry
> if KnownOne[i]:
> if Carry is 1:
> Result.KnownZero[i] = 1
> Carry = 1
> else if Carry is 0:
> Result.KnownOne[i] = 1
> Carry = 0
> else if Carry is unknown:
> Carry = unknown
> continue
> // if neither one or zero is known:
> if Carry == 1:
> Carry = unknown
>
> -- Sanjoy