Data.SBV.Examples.CodeGeneration.Fibonacci

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.

A naive implementation

fib0 :: SWord64 -> SWord64

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.)

Using a recursion depth, and accumulating parameters

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.

fib1 :: SWord64 -> SWord64 -> SWord64

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

genFib1 :: SWord64 -> IO ()

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;
}

Generating a look-up table

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.

fib2 :: SWord64 -> SWord64 -> SWord64

Compute the fibonacci numbers statically at code-generation time and put them in a table, accessed by the select call.

genFib2 :: SWord64 -> IO ()

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;
}