ocaml-batteries-team/batteries-included — pull request #583 by cakeplus (2014-09-14 22:57:00+00:00)
Title: Int.safe int.mul fix

`BatInt.Safe_int.mul` doesn't catch overflows in certain cases. For example, on x86-64:
```
# BatInt.Safe_int.mul 3_000_000_000 3_000_000_000;;
- : int = -223372036854775808
```
Bummer.

Actually, the comment inside the implementation warns about the bug:
``` ocaml
(*This function used to assume that in case of overflow the result would be
different when computing in 31 bits (resp 63 bits) and in 32 bits (resp 64
bits). This trick turned out to be *wrong* on 64-bit machines, where
[Nativeint.mul 2432902008176640000n 21n] and [2432902008176640000 * 21]
yield the same result, [-4249290049419214848]. *)
```

The implementation itself is some crazy bit-twiddling voodoo magic. I couldn't fully understand why is it supposed to work, what is the "trick" mentioned in the comment, let alone how to fix it and prove it to be correct. So I tried to come up with a different solution.

The popular CERT C Coding Standard mentions a [simple implementation](https://www.securecoding.cert.org/confluence/display/seccode/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow) of the integer multiplication overflow detection algorithm, which seems to be portable to OCaml, since it wouldn't trigger undefined behavior. I have implemented the algorithm in OCaml, as well as checked carefully that it handles all the corner cases correctly. The proposed implementation is easy to understand and verify, thus robust. Still, it would be better if at least one more person looked through it carefully.