Data.SBV.Examples.CodeGeneration.PopulationCount

Computing population-counts (number of set bits) and autimatically generating C code.

Reference: Slow but obviously correct

popCount_Slow :: SWord64 -> SWord8

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 -> SWord8

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.

pop8 :: [SWord8]

Look-up table, containing population counts for all possible 8-bit value, from 0 to 255.

Verification

While we would like to use popCount instead of popCount_Slow, how can we be absolutely sure that we got the constants correctly computed and stored in pop8? It is entirely possible that one of the entries might be incorrect, causing a hard-to-detect bug. However, using SBV we can equivalence check that the faster version computes precisely the same answers as the slower reference version.

fastPopCountIsCorrect :: SWord64 -> SBool

States the correctness of faster population-count algorithm, with respect to the reference slow version. We have:

>>> prove fastPopCountIsCorrect
Q.E.D.

Code generation

genPopCountInC :: IO ()

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:

 /* 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[] = {
       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:

 /* 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