Klee: a poor man’s QuickCheck…

Recently, I’ve been working on packaging the Klee symbolic interpreter for Debian and Ubuntu because I’d really like to see more folks using it to test their software. To that end, I’ve also begun working through some simple example tests to demonstrate how you might use it to test your own software. Thus, without further ado:

Suppose that you’ve been given the following reference implementation of the Fibonacci function:

int fibonacci_ref(int n)
{
  if      (n == 0) return 0;
  else if (n == 1) return 1;
  else             return fibonacci_ref(n-1) + fibonacci_ref(n-2);
}

and that you’ve been asked to speed it up, say, by replacing the naive recursion in the reference implementation with iteration, like so:

int fibonacci_opt(int n)
{
  if (n == 0)      return 0;
  else if (n == 1) return 1;
  else
  {
    int a, b, c;
    a = 0; b = 1; c = 1;
    for (int i = 1; i < n; i++)
    {
      a = b; b = c; c = a + b;
    }
    return c;
  }
}

Wouldn’t it be nice to know whether the reference implementation and the iteration-based implementation compute the same function?

Well, conveniently, here’s a test harness, fib.c, that we might use:

#include <klee.h>
#include <assert.h>

/* fibonacci_ref... */
/* fibonacci_opt... */

int main(int argc, char** argv)
{
  int n, a, b;
  klee_make_symbolic(&n, sizeof(n), "n");
  n &= 0x3F;
  a = fibonacci_ref(n);
  b = fibonacci_opt(n);
  klee_assert(a == b);
  return 0;
}

with the following Makefile:

all: fib.bc
    klee --max-time=5 --optimize --use-random-search --emit-all-errors --only-output-states-covering-new $<
    for f in $$(find klee-last/ -name '*.err'); do ktest-tool --write-ints $$(echo $$f | cut -f1 -d.).ktest; done

fib.bc: fib.c
    clang -O3 -o $@ -emit-llvm -c $<

.PHONY: all

to check some small random inputs.

(P.S. - Care to guess what the output is?)