AddSub.hs

-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.CodeGeneration.AddSub
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Simple code generation example.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.CodeGeneration.AddSub where

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

-- | Return the sum and difference of two unsigned 8-bit values, wrapping modulo 256.
addSub :: SWord8 -> SWord8 -> (SWord8, SWord8)
addSub x y = (x+y, x-y)

-- | Generate C code for addSub. Here's the output showing the generated C code:
--
-- >>> genAddSub
-- == BEGIN: "Makefile" ================
-- # Makefile for addSub. 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: addSub_driver
-- <BLANKLINE>
-- addSub.o: addSub.c addSub.h
-- 	${CC} ${CCFLAGS} -c $< -o $@
-- <BLANKLINE>
-- addSub_driver.o: addSub_driver.c addSub.h
-- 	${CC} ${CCFLAGS} -c $< -o $@
-- <BLANKLINE>
-- addSub_driver: addSub.o addSub_driver.o
-- 	${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}
-- <BLANKLINE>
-- clean:
-- 	rm -f *.o
-- <BLANKLINE>
-- veryclean: clean
-- 	rm -f addSub_driver
-- == END: "Makefile" ==================
-- == BEGIN: "addSub.h" ================
-- /* Header file for addSub. Automatically generated by SBV. Do not edit! */
-- <BLANKLINE>
-- #ifndef SBV_GENERATED_addSub_HEADER_INCLUDED
-- #define SBV_GENERATED_addSub_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: */
-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
--             SWord8 *dif);
-- <BLANKLINE>
-- #endif /* SBV_GENERATED_addSub_HEADER_INCLUDED */
-- == END: "addSub.h" ==================
-- == BEGIN: "addSub_driver.c" ================
-- /* Example driver program for addSub. */
-- /* Automatically generated by SBV. Edit as you see fit! */
-- <BLANKLINE>
-- #include <stdio.h>
-- #include "addSub.h"
-- <BLANKLINE>
-- int main(void)
-- {
--   SWord8 sbv_driver_output_0;
--   SWord8 sbv_driver_output_1;
-- <BLANKLINE>
--   addSub(132, 241, &sbv_driver_output_0, &sbv_driver_output_1);
-- <BLANKLINE>
--   printf("addSub(132, 241, &sum, &dif) ->\n");
--   printf("  sum = %"PRIu8"\n", sbv_driver_output_0);
--   printf("  dif = %"PRIu8"\n", sbv_driver_output_1);
-- <BLANKLINE>
--   return 0;
-- }
-- == END: "addSub_driver.c" ==================
-- == BEGIN: "addSub.c" ================
-- /* File: "addSub.c". Automatically generated by SBV. Do not edit! */
-- <BLANKLINE>
-- #include "addSub.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 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>
-- static inline SBV_CGEN_UNUSED SWord8 sbv_bv_u8_sub(SWord8 a, SWord8 b)
-- {
--   const SWord8 bits = (SWord8) ((((uint64_t) (SWord8) a) - ((uint64_t) (SWord8) b)) & UINT64_C(0x00000000000000ff));
--   return (SWord8) bits;
-- }
-- <BLANKLINE>
-- <BLANKLINE>
-- void addSub(const SWord8 sbv_input_0, const SWord8 sbv_input_1,
--             SWord8 *sbv_output_0, SWord8 *sbv_output_1)
-- {
--   const SWord8 s0 = sbv_input_0;
--   const SWord8 s1 = sbv_input_1;
--   const SWord8 s2 = sbv_bv_u8_add(s0, s1);
--   const SWord8 s3 = sbv_bv_u8_sub(s0, s1);
-- <BLANKLINE>
--   *sbv_output_0 = s2;
--   *sbv_output_1 = s3;
-- }
-- == END: "addSub.c" ==================
--
genAddSub :: IO ()
genAddSub = compileToC outDir "addSub" $ do
        x <- cgInput "x"
        y <- cgInput "y"
        -- leave the cgSetDriverValues call out for generating a driver with random values
        cgSetDriverValues [132, 241]
        let (s, d) = addSub x y
        cgOutput "sum" s
        cgOutput "dif" d
 where -- use Just "dirName" for putting the output to the named directory
       -- otherwise, it'll go to standard output
       outDir = Nothing