Portability | portable |
---|---|
Stability | experimental |
Maintainer | erkokl@gmail.com |
Computing population-counts (number of set bits) and autimatically generating C code.
- popCount_Slow :: SWord64 -> SWord8
- popCount :: SWord64 -> SWord8
- pop8 :: [SWord8]
- fastPopCountIsCorrect :: SWord64 -> SBool
- genPopCountInC :: IO ()
Reference: Slow but obviously correct
popCount_Slow :: SWord64 -> SWord8Source
Given a 64-bit quantity, the simplest (and obvious) way to count the number of bits that are set in it is to simply walk through all the bits and add 1 to a running count. This is slow, as it requires 64 iterations, but is simple and easy to convince yourself that it is correct. For instance:
>>>
popCount_Slow 0x0123456789ABCDEF
32 :: SWord8
Faster: Using a look-up table
popCount :: SWord64 -> SWord8Source
Faster version. This is essentially the same algorithm, except we go 8 bits at a time instead of one by one, by using a precomputed table of population-count values for each byte. This algorithm loops only 8 times, and hence is at least 8 times more efficient.
Look-up table, containing population counts for all possible 8-bit value, from 0 to 255. Note that we do not "hard-code" the values, but merely use the slow version to compute them.
Verification
We prove that popCount
and popCount_Slow
are functionally equivalent.
This is essential as we will automatically generate C code from popCount
,
and we would like to make sure that the fast version is correct with
respect to the slower reference version.
fastPopCountIsCorrect :: SWord64 -> SBoolSource
States the correctness of faster population-count algorithm, with respect to the reference slow version. We have:
>>>
prove fastPopCountIsCorrect
Q.E.D.
Code generation
Not only we can prove that faster version is correct, but we can also automatically generate C code to compute population-counts for us. This action will generate all the C files that you will need, including a driver program for test purposes.
Below is the generated header file for popCount
:
/* Header file for popCount. Automatically generated by SBV. Do not edit! */ #ifndef __popCount__HEADER_INCLUDED__ #define __popCount__HEADER_INCLUDED__ #include <inttypes.h> #include <stdint.h> /* Unsigned bit-vectors */ typedef uint8_t SBool ; typedef uint8_t SWord8 ; typedef uint16_t SWord16; typedef uint32_t SWord32; typedef uint64_t SWord64; /* Signed bit-vectors */ typedef int8_t SInt8 ; typedef int16_t SInt16; typedef int32_t SInt32; typedef int64_t SInt64; /* Entry point prototype: */ SWord8 popCount(const SWord64 x); #endif /* __popCount__HEADER_INCLUDED__ */
The generated C function. Note how the Haskell list pop8
is turned into a look-up
table automatically (see table0
below) in the C code.
/* File: "popCount.c". Automatically generated by SBV. Do not edit! */ #include <inttypes.h> #include <stdint.h> #include "popCount.h" SWord8 popCount(const SWord64 x) { const SWord64 s0 = x; static const SWord8 table0[] = { 0x00, 0x01, 0x01, 0x02, 0x01, 0x02, 0x02, 0x03, 0x01, 0x02, 0x02, 0x03, 0x02, 0x03, 0x03, 0x04, 0x01, 0x02, 0x02, 0x03, 0x02, 0x03, 0x03, 0x04, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x01, 0x02, 0x02, 0x03, 0x02, 0x03, 0x03, 0x04, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x01, 0x02, 0x02, 0x03, 0x02, 0x03, 0x03, 0x04, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x04, 0x05, 0x05, 0x06, 0x05, 0x06, 0x06, 0x07, 0x01, 0x02, 0x02, 0x03, 0x02, 0x03, 0x03, 0x04, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x04, 0x05, 0x05, 0x06, 0x05, 0x06, 0x06, 0x07, 0x02, 0x03, 0x03, 0x04, 0x03, 0x04, 0x04, 0x05, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x04, 0x05, 0x05, 0x06, 0x05, 0x06, 0x06, 0x07, 0x03, 0x04, 0x04, 0x05, 0x04, 0x05, 0x05, 0x06, 0x04, 0x05, 0x05, 0x06, 0x05, 0x06, 0x06, 0x07, 0x04, 0x05, 0x05, 0x06, 0x05, 0x06, 0x06, 0x07, 0x05, 0x06, 0x06, 0x07, 0x06, 0x07, 0x07, 0x08 }; const SWord64 s11 = s0 & 0x00000000000000ffULL; const SWord8 s12 = table0[s11]; const SWord64 s13 = s0 >> 8; const SWord64 s14 = 0x00000000000000ffULL & s13; const SWord8 s15 = table0[s14]; const SWord8 s16 = s12 + s15; const SWord64 s17 = s13 >> 8; const SWord64 s18 = 0x00000000000000ffULL & s17; const SWord8 s19 = table0[s18]; const SWord8 s20 = s16 + s19; const SWord64 s21 = s17 >> 8; const SWord64 s22 = 0x00000000000000ffULL & s21; const SWord8 s23 = table0[s22]; const SWord8 s24 = s20 + s23; const SWord64 s25 = s21 >> 8; const SWord64 s26 = 0x00000000000000ffULL & s25; const SWord8 s27 = table0[s26]; const SWord8 s28 = s24 + s27; const SWord64 s29 = s25 >> 8; const SWord64 s30 = 0x00000000000000ffULL & s29; const SWord8 s31 = table0[s30]; const SWord8 s32 = s28 + s31; const SWord64 s33 = s29 >> 8; const SWord64 s34 = 0x00000000000000ffULL & s33; const SWord8 s35 = table0[s34]; const SWord8 s36 = s32 + s35; const SWord64 s37 = s33 >> 8; const SWord64 s38 = 0x00000000000000ffULL & s37; const SWord8 s39 = table0[s38]; const SWord8 s40 = s36 + s39; return s40; }
SBV will also generate a driver program for test purposes. The driver will call
the generated function with random values. (It is also possible to instruct SBV
to use prescribed values, see the function compileToC'
.)
/* Example driver program for popCount. */ /* Automatically generated by SBV. Edit as you see fit! */ #include <inttypes.h> #include <stdint.h> #include <stdio.h> #include "popCount.h" int main(void) { const SWord8 pc = popCount(0x0123456789abcdefULL); printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", pc); return 0; }
And a Makefile
to simplify compilation:
# Makefile for popCount. Automatically generated by SBV. Do not edit! CC=gcc CCFLAGS=-Wall -O3 -DNDEBUG -fomit-frame-pointer all: popCount_driver popCount.o: popCount.c popCount.h ${CC} ${CCFLAGS} -c popCount.c -o popCount.o popCount_driver.o: popCount_driver.c ${CC} ${CCFLAGS} -c popCount_driver.c -o popCount_driver.o popCount_driver: popCount.o popCount_driver.o ${CC} ${CCFLAGS} popCount.o popCount_driver.o -o popCount_driver clean: rm -f popCount_driver.o popCount.o veryclean: clean rm -f popCount_driver