PopulationCount.hs

-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.CodeGeneration.PopulationCount
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Computing population-counts (number of set bits) and automatically
-- generating C code.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.CodeGeneration.PopulationCount where

import Data.SBV
import Data.SBV.Tools.CodeGen

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV
#endif

-----------------------------------------------------------------------------
-- * 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:
--
-- >>> popCountSlow 0x0123456789ABCDEF
-- 32 :: SWord8
popCountSlow :: SWord64 -> SWord8
popCountSlow 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.
popCountFast :: SWord64 -> SWord8
popCountFast 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 (popCountSlow . literal) [0 .. 255]

-----------------------------------------------------------------------------
-- * Verification
-----------------------------------------------------------------------------

{- $VerificationIntro
We prove that `popCountFast` and `popCountSlow` are functionally equivalent.
This is essential as we will automatically generate C code from `popCountFast`,
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. Turns out Z3's default solver is rather slow
-- for this one, but there's a magic incantation to make it go fast.
-- See <http://github.com/Z3Prover/z3/issues/1150> for details.
--
-- >>> let cmd = "(check-sat-using (then (using-params ackermannize_bv :div0_ackermann_limit 1000000) simplify bit-blast sat))"
-- >>> proveWith z3{satCmd = cmd} fastPopCountIsCorrect
-- Q.E.D.
fastPopCountIsCorrect :: SWord64 -> SBool
fastPopCountIsCorrect x = popCountFast x .== popCountSlow 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 are the generated files for `popCountFast`:
--
-- >>> genPopCountInC
-- == BEGIN: "Makefile" ================
-- # Makefile for popCount. Automatically generated by SBV. Do not edit!
-- <BLANKLINE>
-- # include any user-defined .mk file in the current directory.
-- -include *.mk
-- <BLANKLINE>
-- CC?=gcc
-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
-- <BLANKLINE>
-- all: popCount_driver
-- <BLANKLINE>
-- popCount.o: popCount.c popCount.h
-- 	${CC} ${CCFLAGS} -c $< -o $@
-- <BLANKLINE>
-- popCount_driver.o: popCount_driver.c popCount.h
-- 	${CC} ${CCFLAGS} -c $< -o $@
-- <BLANKLINE>
-- popCount_driver: popCount.o popCount_driver.o
-- 	${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}
-- <BLANKLINE>
-- clean:
-- 	rm -f *.o
-- <BLANKLINE>
-- veryclean: clean
-- 	rm -f popCount_driver
-- == END: "Makefile" ==================
-- == BEGIN: "popCount.h" ================
-- /* Header file for popCount. Automatically generated by SBV. Do not edit! */
-- <BLANKLINE>
-- #ifndef SBV_GENERATED_popCount_HEADER_INCLUDED
-- #define SBV_GENERATED_popCount_HEADER_INCLUDED
-- <BLANKLINE>
-- <BLANKLINE>
-- #include <stdio.h>
-- #include <stdlib.h>
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include <stdbool.h>
-- #include <string.h>
-- #include <math.h>
-- <BLANKLINE>
-- /* Floating-point calling convention:
--  * Enter generated code in FE_TONEAREST (round-to-nearest, ties-to-even).
--  * Callbacks must preserve this mode before returning or re-entering.
--  * Generated code does not check or change the hardware rounding mode.
--  * Custom builds must disable implicit FP contraction, including at LTO link time.
--  */
-- <BLANKLINE>
-- /* The boolean type */
-- typedef bool SBool;
-- <BLANKLINE>
-- /* The float type */
-- typedef float SFloat;
-- <BLANKLINE>
-- /* The double type */
-- typedef double SDouble;
-- <BLANKLINE>
-- /* Unsigned bit-vectors */
-- typedef uint8_t  SWord8;
-- typedef uint16_t SWord16;
-- typedef uint32_t SWord32;
-- typedef uint64_t SWord64;
-- <BLANKLINE>
-- /* Signed bit-vectors */
-- typedef int8_t  SInt8;
-- typedef int16_t SInt16;
-- typedef int32_t SInt32;
-- typedef int64_t SInt64;
-- <BLANKLINE>
-- /* Entry point prototype: */
-- SWord8 popCount(const SWord64 x);
-- <BLANKLINE>
-- #endif /* SBV_GENERATED_popCount_HEADER_INCLUDED */
-- == END: "popCount.h" ==================
-- == BEGIN: "popCount_driver.c" ================
-- /* Example driver program for popCount. */
-- /* Automatically generated by SBV. Edit as you see fit! */
-- <BLANKLINE>
-- #include <stdio.h>
-- #include "popCount.h"
-- <BLANKLINE>
-- int main(void)
-- {
--   const SWord8 sbv_result = popCount(0x1b02e143e4f0e0e5ULL);
-- <BLANKLINE>
--   printf("popCount(0x1b02e143e4f0e0e5ULL) = %"PRIu8"\n", sbv_result);
-- <BLANKLINE>
--   return 0;
-- }
-- == END: "popCount_driver.c" ==================
-- == BEGIN: "popCount.c" ================
-- /* File: "popCount.c". Automatically generated by SBV. Do not edit! */
-- <BLANKLINE>
-- #include "popCount.h"
-- <BLANKLINE>
-- /* Exact bit-vector runtime. All arithmetic is modulo the declared width. */
-- #ifndef SBV_CGEN_UNUSED
-- #if defined(__GNUC__) || defined(__clang__)
-- #define SBV_CGEN_UNUSED __attribute__((unused))
-- #else
-- #define SBV_CGEN_UNUSED
-- #endif
-- #endif
-- <BLANKLINE>
-- static inline SBV_CGEN_UNUSED SWord64 sbv_bv_u64_shl(SWord64 a, SWord64 amount)
-- {
--   const uint64_t n = (uint64_t) (SWord64) amount;
--   const SWord64 result = n >= 64 ? (SWord64) 0 : (SWord64) ((uint64_t) (SWord64) a << n);
--   return result;
-- }
-- <BLANKLINE>
-- static inline SBV_CGEN_UNUSED SWord64 sbv_bv_u64_lshr(SWord64 a, SWord64 amount)
-- {
--   const uint64_t n = (uint64_t) (SWord64) amount;
--   return n >= 64 ? (SWord64) 0 : (SWord64) ((uint64_t) (SWord64) a >> n);
-- }
-- <BLANKLINE>
-- static inline SBV_CGEN_UNUSED SWord8 sbv_bv_u8_add(SWord8 a, SWord8 b)
-- {
--   const SWord8 bits = (SWord8) ((((uint64_t) (SWord8) a) + ((uint64_t) (SWord8) b)) & UINT64_C(0x00000000000000ff));
--   return (SWord8) bits;
-- }
-- <BLANKLINE>
-- <BLANKLINE>
-- SWord8 popCount(const SWord64 sbv_input_0)
-- {
--   const SWord64 s0 = sbv_input_0;
--   const SWord64 s11 = s0 & 0x00000000000000ffULL;
--   const SWord64 s14 = sbv_bv_u64_lshr(s0, 0x0000000000000008ULL);
--   const SWord64 s15 = 0x00000000000000ffULL & s14;
--   const SWord64 s18 = sbv_bv_u64_lshr(s14, 0x0000000000000008ULL);
--   const SWord64 s19 = 0x00000000000000ffULL & s18;
--   const SWord64 s22 = sbv_bv_u64_lshr(s18, 0x0000000000000008ULL);
--   const SWord64 s23 = 0x00000000000000ffULL & s22;
--   const SWord64 s26 = sbv_bv_u64_lshr(s22, 0x0000000000000008ULL);
--   const SWord64 s27 = 0x00000000000000ffULL & s26;
--   const SWord64 s30 = sbv_bv_u64_lshr(s26, 0x0000000000000008ULL);
--   const SWord64 s31 = 0x00000000000000ffULL & s30;
--   const SWord64 s34 = sbv_bv_u64_lshr(s30, 0x0000000000000008ULL);
--   const SWord64 s35 = 0x00000000000000ffULL & s34;
--   const SWord64 s38 = sbv_bv_u64_lshr(s34, 0x0000000000000008ULL);
--   const SWord64 s39 = 0x00000000000000ffULL & s38;
--         SWord8  s12;
--         SWord8  s16;
--         SWord8  s17;
--         SWord8  s20;
--         SWord8  s21;
--         SWord8  s24;
--         SWord8  s25;
--         SWord8  s28;
--         SWord8  s29;
--         SWord8  s32;
--         SWord8  s33;
--         SWord8  s36;
--         SWord8  s37;
--         SWord8  s40;
--         SWord8  s41;
--   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
--   };
--   s12 = table0[s11];
--   s16 = table0[s15];
--   s17 = sbv_bv_u8_add(s12, s16);
--   s20 = table0[s19];
--   s21 = sbv_bv_u8_add(s17, s20);
--   s24 = table0[s23];
--   s25 = sbv_bv_u8_add(s21, s24);
--   s28 = table0[s27];
--   s29 = sbv_bv_u8_add(s25, s28);
--   s32 = table0[s31];
--   s33 = sbv_bv_u8_add(s29, s32);
--   s36 = table0[s35];
--   s37 = sbv_bv_u8_add(s33, s36);
--   s40 = table0[s39];
--   s41 = sbv_bv_u8_add(s37, s40);
-- <BLANKLINE>
--   return s41;
-- }
-- == END: "popCount.c" ==================
genPopCountInC :: IO ()
genPopCountInC = compileToC Nothing "popCount" $ do
        cgSetDriverValues [0x1b02e143e4f0e0e5]  -- remove this line to get a random test value
        x <- cgInput "x"
        cgReturn $ popCountFast x