在 IA32 中计算 64 位除法的逆向分析
最近逆向 Haswell 的 MRC 代码的时候发现里面有一段 64 位除法的子程序，虽然稍作分析可以认出它是做 64 位除法的，但是当时还是没搞明白细节。这几天再对它进行了证明，终于搞明白这个算法。
因为 IA32 中没有 64 位除法运算，所以需要用 32 位的除法模拟。IA32 中可以用两个 32 位寄存器 EDX:EAX 保存一个 64 位的无符号被除数，再用一个 32 位寄存器或内存中的整数保存一个 32 位的无符号除数，然后用 DIV 指令完成除法，如果商可以用 32 位无符号整数表示，那么就将商存在 EAX，余数存在 EDX，从而完成除法，否则则发生除法溢出，触发异常。
首先考虑简单的情形，如果除数高 32 位都是 0，那么可以直接做除法，为了防止溢出，可以用除数分别除被除数的高低 32 位来计算最后的商。如果除数的高 32 位不小于被除数的高 32 位，那么商就是 0 或者 1，只要再看看低 32 位就行了。最后我们再考虑最复杂的情况，就是被除数高 32 位大于除数高 32 位，并且除数高 32 位不为 0. 以下设被除数位 u，除数为 d，处理器寄存器宽度为 w 位，在 IA32 中 w = 32.
我逆向的这个算法是这么做的。首先右移被除数和除数，直到除数成为 32 位整数，我们记右移的位数为 s. 移位后就可以进行 32 位除法，设移位后被除数和除数成为 u', d', 得到的商和余数为 q', r', 那么 u' = q'd' + r', 0 <= r' <= d' - 1.
接下来就是要计算最终的商和 q' 的关系了。从反汇编的代码看，商是 q' 或者 (q' - 1)，我们首先证明这个性质。
因为 u / d < (u' + 1) / d' = q' + (r' + 1) / d' <= q' + 1, 所以 u / d 的商小于 q' + 1，即商不大于 q'.
另一方面，u - (q' - 1)d >= d + u - q'd = d + u - q'(d'(2^s) + LO_s(d)) >= d - q'LO_s(d) 这里 2^s 指 2 的 s 次方，一个数乘 2^s 相当于它左移 s 位. LO_s(d) 指 d 的最低 s 位。 由于 q' <= u' / d' = (u >> s) / d' < (2^(2w-s)) / (2^(w-1)) = 2^(w-s+1), LO_s(d) < 2^s, 从而 q'LO_s(d) < 2^(w+1) 如果 d >= 2^(w+1), 则 u - (q'-1)d >= 0, 如果 d < 2^(w+1), 由此前的假设，d > 2^w, 从而 d 是个 w+1 位的数，s = 1, 从而 LO_s(d) <= 1, q'LO_s(d) <= q' < 2^w, 从而 d - q'LO_s(d) > 0. 总之，u - (q'-1)d >= 0 成立，因此 u/d >= q'-1, 即 u/d 的商不小于 q'-1.
于是我们证明了 u / d 的商是 q' 或 (q' - 1). 那么剩下的工作是要计算商是哪个值，为此我们计算 u - q'd 来看它是否不小于 0，如果小于 0，则商为 q'-1，否则商为 q'.
u - q'd = u - q'(d'(2^s) + LO_s(d)) = u - (u'-r')(2^s) - q'LO_s(d) = LO_s(u) + r'(2^s) - q'LO_s(d)
这个值不好算，因为提取 u 和 d 的低 s 位有点麻烦，但是如果把一个数左移 (w-s) 位，那么这个数的低 s 位就可以顶到 w 位整数的最高位，高位的数都在左移的过程中丢弃。根据反汇编的代码，我们计算 (r'(2^s) - q'LO_s(d)) << (w-s) = r'(2^w) - q'(d<<(w-s)), 设 q'(d<<(w-s)) = t, HI_w(t) 和 LO_w(t) 为 t 的高 w 位和低 w 位，而 HI_w(r'(2^w)) 恰好就是 r'.
如果 r' > HI_w(t), 那么 (r'(2^s) - q'LO_s(d)) << (w-s) 大于 0, 从而 r'(2^s) - q'LO_s(d) > 0, u - q'd > 0. 如果 r' < HI_w(t), 则 t - r'(2^w) >= 2^w, 而 (LO_s(u) << (w-s)) < 2^w, 从而 ((u - q'd) << (w-s)) = ((LO_s(u) << (w-s)) + r'(2^w) - t) <= -(2^w - (LO_s(u) << (w-s))) < 0, 所以 u - q'd < 0. 如果 r' = HI_w(t), 则 ((u - q'd) << (w - s)) = (LO_s(u) << (w - s)) - LO_w(t) = LO_w(u << (w - s)) - LO_w(t). 只要比较 LO_w(u << (w-s)) 和 LO_w(t) 即可。