Automatically producing fast smallnum functions
The CakeML source language has arbitrary precision integers as the main integer type. These are implemented dynamically as either smallnums or bignums. A smallnum is used in case the value fits within a tagged machine word (32-bit or 64-bit depending on target architecture). The bignum representation is only used when the value doesn't fit a smallnum. A bignum is represented as a pointer to a vector of machine words on the heap containning the large number.
The consquence of this generality is that each arithmetic operation has to check whether it has a smallnum (unboxed value) or a bignum (pointer). The checking code is tuned to be very fast. However, it still comes at a cost -- not least in that the each bignum operation is a call to a library routine for doing the bignum operation. The prescence of such subroutine calls, even if they are seldomly used, disrupt the register allocation around each arithmetic operation.
This issue is about adding a new compiler optimisation that notices when a recursive function will from this point onwards have a smallnum only in one or more of its arguments and then jump to code that is optimised under this assumption.
Example:
The following function is a typical function used in the bootstrapped CakeML compiler implementation. Optimising such functions might improve the speed of the compiler itself.
The original function is:
genlist f n aux =
if n = 0 then aux else
let n = n - 1 in genlist n (f n :: aux)
This would be transformed into two functions:
genlist f n aux =
if is_small_num n /\ 0 <= n then genlist' f n aux else
if n = 0 then aux else
let n = n - 1 in genlist n (f n :: aux)
genlist' f n aux =
if n = 0 then aux else
let n = smallnum_minus n 1 in genlist' n (f n :: aux)
General case:
In general the optimisation should look for numbers that can only get smaller in a loop. If it finds such, then it makes a copy of the function and replaces all arithmetic operations that operate on the smallnum by smallnum versions.
Since this optimisation duplicates code, it must be possibly for the user of the compiler to control when it is applied. The simplest thing would be to have an on-off switch, but there could be more fine-grained controls too.
MSc project:
This issue is suitable as a MSc project on compiler verification. This optimisation would most naturally fit around the BVI intermediate language.