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

Sanjoy Das via llvm-dev llvm-dev at lists.llvm.org
Tue May 3 22:34:14 PDT 2016

```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
```