1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
-----------------------------------------------------------------------------
-- |
-- 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
-- | Simple function that returns add/sum of args
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
-- ${CC} ${CCFLAGS} -c $< -o $@
-- <BLANKLINE>
-- addSub_driver: addSub.o addSub_driver.o
-- ${CC} ${CCFLAGS} $^ -o $@
-- <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 __addSub__HEADER_INCLUDED__
-- #define __addSub__HEADER_INCLUDED__
-- <BLANKLINE>
-- #include <stdio.h>
-- #include <stdlib.h>
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include <stdbool.h>
-- #include <string.h>
-- #include <math.h>
-- <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 /* __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 sum;
-- SWord8 dif;
-- <BLANKLINE>
-- addSub(132, 241, &sum, &dif);
-- <BLANKLINE>
-- printf("addSub(132, 241, &sum, &dif) ->\n");
-- printf(" sum = %"PRIu8"\n", sum);
-- printf(" dif = %"PRIu8"\n", dif);
-- <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>
-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
-- SWord8 *dif)
-- {
-- const SWord8 s0 = x;
-- const SWord8 s1 = y;
-- const SWord8 s2 = s0 + s1;
-- const SWord8 s3 = s0 - s1;
-- <BLANKLINE>
-- *sum = s2;
-- *dif = s3;
-- }
-- == END: "addSub.c" ==================
--
genAddSub :: IO ()
genAddSub = compileToC outDir "addSub" $ do
x <- cgInput "x"
y <- cgInput "y"
-- leave the cgDriverVals 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
|
