----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Examples.CodeGeneration.PopulationCount -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- Portability : portable -- -- Computing population-counts (number of set bits) and autimatically -- generating C code. ----------------------------------------------------------------------------- module Data.SBV.Examples.CodeGeneration.PopulationCount where import Data.SBV ----------------------------------------------------------------------------- -- * Reference: Slow but /obviously/ correct ----------------------------------------------------------------------------- -- | 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 popCount_Slow :: SWord64 -> SWord8 popCount_Slow inp = go inp 0 0 where go :: SWord64 -> Int -> SWord8 -> SWord8 go _ 64 c = c go x i c = go (x `shiftR` 1) (i+1) (ite (x .&. 1 .== 1) (c+1) c) ----------------------------------------------------------------------------- -- * Faster: Using a look-up table ----------------------------------------------------------------------------- -- | 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. popCount :: SWord64 -> SWord8 popCount inp = go inp 0 0 where go :: SWord64 -> Int -> SWord8 -> SWord8 go _ 8 c = c go x i c = go (x `shiftR` 8) (i+1) (c + select pop8 0 (x .&. 0xff)) -- | 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. pop8 :: [SWord8] pop8 = map popCount_Slow [0 .. 255] ----------------------------------------------------------------------------- -- * Verification ----------------------------------------------------------------------------- {- $VerificationIntro 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. -} -- | States the correctness of faster population-count algorithm, with respect -- to the reference slow version. We have: -- -- >>> prove fastPopCountIsCorrect -- Q.E.D. fastPopCountIsCorrect :: SWord64 -> SBool fastPopCountIsCorrect x = popCount x .== popCount_Slow x ----------------------------------------------------------------------------- -- * 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 -- > #include -- > -- > /* 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 -- > #include -- > #include "popCount.h" -- > -- > SWord8 popCount(const SWord64 x) -- > { -- > const SWord64 s0 = x; -- > static const SWord8 table0[] = { -- > 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3, -- > 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, -- > 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2, -- > 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, -- > 3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, -- > 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3, -- > 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, -- > 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, -- > 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4, -- > 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, -- > 5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5, -- > 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8 -- > }; -- > 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 -- > #include -- > #include -- > #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 genPopCountInC :: IO () genPopCountInC = compileToC False (Just "popCountC") "popCount" ["x", "pc"] popCount