Using QuickCheck to test C APIs

Last year at ICFP I attended the tutorial on QuickCheck with John Hughes. We got to use the Erlang implementation of QuickCheck to test a C API. Ever since I’ve been planning to do the same thing using Haskell. I’ve put it off for the better part of a year now, but then Francesco Mazzoli wrote about inline-c (Call C functions from Haskell without bindings and I found the motivation to actually start writing some code.

The general idea

Many C APIs are rather stateful beasts so to test it I

  1. generate a sequence of API calls (a program of sorts),
  2. run the sequence against a model,
  3. run the sequence against the real implementation, and
  4. compare the model against the real state each step of the way.

The C API

To begin with I hacked up a simple implementation of a stack in C. The “specification” is

Using inline-c to create bindings for it is amazingly simple:

In the code below I import this module qualified.

Representing a program

To represent a sequence of calls I first used a custom type, but later realised that there really was no reason at all to not use a wrapped list:

Then each of the C API functions can be represented with

Arbitrary for Statement

My implementation of Arbitrary for Statement is very simple:

That is, arbitrary just returns one of the constructors of Statement, and shrinking only returns anything for the one constructor that takes an argument, Push.

Prerequisites of Arbitrary for Program Statement

I want to ensure that all Program Statement are valid, which means I need to define the model for running the program and functions for checking the precondition of a statement as well as for updating the model (i.e. for running the Statement).

Based on the C API above it seems necessary to track creation, the contents of the stack, and even if it isn’t explicitly mentioned it’s probably a good idea to track the popped value. Using record (Record is imported as R, and Record.Lens as RL) I defined it like this:

Based on the rather informal specification I coded the pre-conditions for the three statements as

That is

  • Create requires that the stack hasn’t been created already.
  • Push i requires that the stack has been created.
  • Pop also requires that the stack has been created.

Furthermore the “specification” suggests the following definition of a function for running a statement:

(This definition assumes that the model satisfies the pre-conditions, as can be seen in the use of tail.)

Arbitrary for Program Statement

With this in place I can define Arbitrary for Program Statement as follows.

The idea is to, in each step, choose a valid statement given the provided model and cons it with the result of a recursive call with an updated model. The constant 499 is just an arbitrary one I chose after running arbitrary a few times to see how long the generated programs were.

For shrinking I take advantage of the already existing implementation for lists:

Some thoughts so far

I would love making an implementation of Arbitrary s, where s is something that implements a type class that contains preCond, modelRunStatement and anything else needed. I made an attempt using something like

However, when trying to use baseCtx in an implementation of arbitrary I ran into the issue of injectivity. I’m still not entirely sure what that means, or if there is something I can do to work around it. Hopefully someone reading this can offer a solution.

Running the C code

When running the sequence of Statement against the C code I catch the results in

Actually running a statement and capturing the output in a RealContext is easily done using inline-c and record:

Comparing states

Comparing a ModelContext and a RealContext is easily done:

Verifying a Program Statement

With all that in place I can finally write a function for checking the validity of a program:

(This uses mapAccumM from an earlier post of mine.)

The property, finally!

To wrap this all up I then define the property

and a main function


Edit 2015-07-17: Adjusted the description of the pre-conditions to match the code.

⟸ mapAccum in monad Systemd watchdog ⟹

Jesse McDonald

I believe the problem with baseCtx is that there could be two or more instances of S which have the same definition for Ctx a, which means that the compiler can’t infer a (and thus the instance to use) from Ctx a. One option would be to add a Proxy a parameter to baseCtx to select the instance. Another would be to make S a multi-parameter type class with a one-to-one functional dependency between the parameters, like so:

Magnus Therning

I should probably point out that I’m using version 0.3.1.2 of record.

The library seems to have seen dramatic changes as of version 0.4.0.0.

Leave a comment