Fast Division on GCC/ARM

x SAR 31 is 0xffffffff (-1) for negative values of x, and 0x00000000 for positive values.

So the rsbis subtracting -1 from the result (which is the same as adding 1) if the dividend was negative.

Let's say your dividend is -60. With just the multiply and shift you'd get the result -7, so it subtracts -1 to get the expected result of -6.

After that, however, it subtracted (dividend/2^31) from the result.

Actually, it subtracts dividend >> 31, which is -1 for negative dividend, and 0 for non-negative dividend, when right-shifting negative integers is arithmetic right-shift (and int is 32 bits wide).

0x6666667 = (2^34 + 6)/10

So for x < 0, we have, writing x = 10*k + r with -10 < r <= 0,

0x66666667 * (10*k+r) = (2^34+6)*k + (2^34 + 6)*r/10 = 2^34*k + 6*k + (2^34+6)*r/10

Now, arithmetic right shift of negative integers yields the floor of v / 2^n, so

(0x66666667 * x) >> 34

results in

k + floor((6*k + (2^34+6)*r/10) / 2^34)

So we need to see that

-2^34 < 6*k + (2^34+6)*r/10 < 0

The right inequality is easy, both k and r are non-positive, and not both are 0.

For the left inequality, a bit more analysis is needed.

r >= -9

so the absolute value of (2^34+6)*r/10 is at most 2^34+6 - (2^34+6)/10.

|k| <= 2^31/10,

so |6*k| <= 3*2^31/5.

And it remains to verify that

6 + 3*2^31/5 < (2^34+6)/10
1288490194   < 1717986919

Yup, true.