Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic

07/18/2022
by   David Monniaux, et al.
0

Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point and fixed-bitwidth integer computations, using the Coq proof assistant and successfully integrated it into the CompCert formally verified compiler.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset