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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.CodeGeneration.Fibonacci
-- Copyright : (c) Lee Pike
-- Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Computing Fibonacci numbers and generating C code. Inspired by Lee Pike's
-- original implementation, modified for inclusion in the package. It illustrates
-- symbolic termination issues one can have when working with recursive algorithms
-- and how to deal with such, eventually generating good C code.
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.CodeGeneration.Fibonacci where
import Data.SBV
import Data.SBV.Tools.CodeGen
-----------------------------------------------------------------------------
-- * A naive implementation
-----------------------------------------------------------------------------
-- | This is a naive implementation of fibonacci, and will work fine (albeit slow)
-- for concrete inputs:
--
-- >>> map fib0 [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
-- However, it is not suitable for doing proofs or generating code, as it is not
-- symbolically terminating when it is called with a symbolic value @n@. When we
-- recursively call @fib0@ on @n-1@ (or @n-2@), the test against @0@ will always
-- explore both branches since the result will be symbolic, hence will not
-- terminate. (An integrated theorem prover can establish termination
-- after a certain number of unrollings, but this would be quite expensive to
-- implement, and would be impractical.)
fib0 :: SWord64 -> SWord64
fib0 n = ite (n .== 0 .|| n .== 1)
n
(fib0 (n-1) + fib0 (n-2))
-----------------------------------------------------------------------------
-- * Using a recursion depth, and accumulating parameters
-----------------------------------------------------------------------------
{- $genLookup
One way to deal with symbolic termination is to limit the number of recursive
calls. In this version, we impose a limit on the index to the function, working
correctly upto that limit. If we use a compile-time constant, then SBV's code generator
can produce code as the unrolling will eventually stop.
-}
-- | The recursion-depth limited version of fibonacci. Limiting the maximum number to be 20, we can say:
--
-- >>> map (fib1 20) [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
-- The function will work correctly, so long as the index we query is at most @top@, and otherwise
-- will return the value at @top@. Note that we also use accumulating parameters here for efficiency,
-- although this is orthogonal to the termination concern.
--
-- A note on modular arithmetic: The 64-bit word we use to represent the values will of course
-- eventually overflow, beware! Fibonacci is a fast growing function..
fib1 :: SWord64 -> SWord64 -> SWord64
fib1 top n = fib' 0 1 0
where fib' :: SWord64 -> SWord64 -> SWord64 -> SWord64
fib' prev' prev m = ite (m .== top .|| m .== n) -- did we reach recursion depth, or the index we're looking for
prev' -- stop and return the result
(fib' prev (prev' + prev) (m+1)) -- otherwise recurse
-- | We can generate code for 'fib1' using the 'genFib1' action. Note that the
-- generated code will grow larger as we pick larger values of @top@, but only linearly,
-- thanks to the accumulating parameter trick used by 'fib1'. The following is an excerpt
-- from the code generated for the call @genFib1 10@, where the code will work correctly
-- for indexes up to 10:
--
-- > SWord64 fib1(const SWord64 x)
-- > {
-- > const SWord64 s0 = x;
-- > const SBool s2 = s0 == 0x0000000000000000ULL;
-- > const SBool s4 = s0 == 0x0000000000000001ULL;
-- > const SBool s6 = s0 == 0x0000000000000002ULL;
-- > const SBool s8 = s0 == 0x0000000000000003ULL;
-- > const SBool s10 = s0 == 0x0000000000000004ULL;
-- > const SBool s12 = s0 == 0x0000000000000005ULL;
-- > const SBool s14 = s0 == 0x0000000000000006ULL;
-- > const SBool s17 = s0 == 0x0000000000000007ULL;
-- > const SBool s19 = s0 == 0x0000000000000008ULL;
-- > const SBool s22 = s0 == 0x0000000000000009ULL;
-- > const SWord64 s25 = s22 ? 0x0000000000000022ULL : 0x0000000000000037ULL;
-- > const SWord64 s26 = s19 ? 0x0000000000000015ULL : s25;
-- > const SWord64 s27 = s17 ? 0x000000000000000dULL : s26;
-- > const SWord64 s28 = s14 ? 0x0000000000000008ULL : s27;
-- > const SWord64 s29 = s12 ? 0x0000000000000005ULL : s28;
-- > const SWord64 s30 = s10 ? 0x0000000000000003ULL : s29;
-- > const SWord64 s31 = s8 ? 0x0000000000000002ULL : s30;
-- > const SWord64 s32 = s6 ? 0x0000000000000001ULL : s31;
-- > const SWord64 s33 = s4 ? 0x0000000000000001ULL : s32;
-- > const SWord64 s34 = s2 ? 0x0000000000000000ULL : s33;
-- >
-- > return s34;
-- > }
genFib1 :: SWord64 -> IO ()
genFib1 top = compileToC Nothing "fib1" $ do
x <- cgInput "x"
cgReturn $ fib1 top x
-----------------------------------------------------------------------------
-- * Generating a look-up table
-----------------------------------------------------------------------------
{- $genLookup
While 'fib1' generates good C code, we can do much better by taking
advantage of the inherent partial-evaluation capabilities of SBV to generate
a look-up table, as follows.
-}
-- | Compute the fibonacci numbers statically at /code-generation/ time and
-- put them in a table, accessed by the 'select' call.
fib2 :: SWord64 -> SWord64 -> SWord64
fib2 top = select table 0
where table = map (fib1 top) [0 .. top]
-- | Once we have 'fib2', we can generate the C code straightforwardly. Below
-- is an excerpt from the code that SBV generates for the call @genFib2 64@. Note
-- that this code is a constant-time look-up table implementation of fibonacci,
-- with no run-time overhead. The index can be made arbitrarily large,
-- naturally. (Note that this function returns @0@ if the index is larger
-- than 64, as specified by the call to 'select' with default @0@.)
--
-- > SWord64 fibLookup(const SWord64 x)
-- > {
-- > const SWord64 s0 = x;
-- > static const SWord64 table0[] = {
-- > 0x0000000000000000ULL, 0x0000000000000001ULL,
-- > 0x0000000000000001ULL, 0x0000000000000002ULL,
-- > 0x0000000000000003ULL, 0x0000000000000005ULL,
-- > 0x0000000000000008ULL, 0x000000000000000dULL,
-- > 0x0000000000000015ULL, 0x0000000000000022ULL,
-- > 0x0000000000000037ULL, 0x0000000000000059ULL,
-- > 0x0000000000000090ULL, 0x00000000000000e9ULL,
-- > 0x0000000000000179ULL, 0x0000000000000262ULL,
-- > 0x00000000000003dbULL, 0x000000000000063dULL,
-- > 0x0000000000000a18ULL, 0x0000000000001055ULL,
-- > 0x0000000000001a6dULL, 0x0000000000002ac2ULL,
-- > 0x000000000000452fULL, 0x0000000000006ff1ULL,
-- > 0x000000000000b520ULL, 0x0000000000012511ULL,
-- > 0x000000000001da31ULL, 0x000000000002ff42ULL,
-- > 0x000000000004d973ULL, 0x000000000007d8b5ULL,
-- > 0x00000000000cb228ULL, 0x0000000000148addULL,
-- > 0x0000000000213d05ULL, 0x000000000035c7e2ULL,
-- > 0x00000000005704e7ULL, 0x00000000008cccc9ULL,
-- > 0x0000000000e3d1b0ULL, 0x0000000001709e79ULL,
-- > 0x0000000002547029ULL, 0x0000000003c50ea2ULL,
-- > 0x0000000006197ecbULL, 0x0000000009de8d6dULL,
-- > 0x000000000ff80c38ULL, 0x0000000019d699a5ULL,
-- > 0x0000000029cea5ddULL, 0x0000000043a53f82ULL,
-- > 0x000000006d73e55fULL, 0x00000000b11924e1ULL,
-- > 0x000000011e8d0a40ULL, 0x00000001cfa62f21ULL,
-- > 0x00000002ee333961ULL, 0x00000004bdd96882ULL,
-- > 0x00000007ac0ca1e3ULL, 0x0000000c69e60a65ULL,
-- > 0x0000001415f2ac48ULL, 0x000000207fd8b6adULL,
-- > 0x0000003495cb62f5ULL, 0x0000005515a419a2ULL,
-- > 0x00000089ab6f7c97ULL, 0x000000dec1139639ULL,
-- > 0x000001686c8312d0ULL, 0x000002472d96a909ULL,
-- > 0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL
-- > };
-- > const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];
-- >
-- > return s65;
-- > }
genFib2 :: SWord64 -> IO ()
genFib2 top = compileToC Nothing "fibLookup" $ do
cgPerformRTCs True -- protect against potential overflow, our table is not big enough
x <- cgInput "x"
cgReturn $ fib2 top x
|
