TopArchive

Posts tagged "quickcheck":

13 Oct 2026

QuickCheck: shrinking like tuples, writing like applicative

The QuickCheck documentation for Arbitrary says that

There is no generic arbitrary implementation included because we don't know how to make a high-quality one.

Though in practice I've found that very often it suffices to write one that uses the fact that Gen is an Applicative. For instance, this type 

data Foo = Foo
    { tata :: Int
    , titi :: Double
    }

would get an implementation that looks like this 

instance Arbitrary Foo where
    arbitrary = Foo <$> arbitrary <*> arbitrary

When it comes to writing the function for shrinking Foo it is possible to rely on a generic function and the documentation says that

The default implementation returns the empty list, so will not try to shrink the value. If your data type has no special invariants, you can enable shrinking by defining shrink = genericShrink, but by customising the behaviour of shrink you can often get simpler counterexamples.

Based on some manual testing it seems that genericShrink generates something like this for the type Foo above 

instance Arbitrary Foo where
    shrink (Foo tata_ titi_) = Foo <$> shrink tata_ <*> shrink titi_

which means that if shrink tata_ generates a list of m elements and shrink titi_ generates a list of n elements, then shrink foo will generate a list of m×n elements. It's clear that the size can become problematic with more fields. It also means that it's very easy to get an empty list – if shrink v results in an empty list, then shrink foo is also empty. Oh, and shrink Nothing is []!

A colleague pointed out that tuples have a rather efficient implementation of shrink that grows linearly with the number of elements and doesn't reduce to the empty list as easily. I could use it for Foo like this 

instance Arbitrary Foo where
    shrink (Foo tata_ titi_) = uncurry Foo <$> shrink (tata_, titi_)

However, that doesn't scale that well to more fields. Up to a point I can use list comprehensions, but it gets a bit difficult to read, I find. On top of that, the largest tuple with an Arbitrary instance has 10 elements, and then I'll have to either define more or use inner tuples.

Wouldn't it be nice to write shrink in something that looks Applicative, but behaves like tuples?

Here's one approach to this.

First a type to hold information about what's being shrunk, or in this case waned 

data Wane a = Wane a [a]
    deriving (Generic, Show)

instance Functor Wane where
    fmap f (Wane a as) = Wane (f a) (f <$> as)

Then a couple of functions to bring values in and out, unWane to get the list of values out and wane to wrap a value in Wane 

unWane :: Wane a -> [a]
unWane (Wane _ as) = as

wane :: (Arbitrary a) => a -> Wane a
wane a = Wane a (shrink a)

Finally a way to combine two Wane values is needed, and here I was inspired by the implementation of Arbitrary for (a,b) 

infixl 4 \*/

(\*/) ::  Wane (a -> b) -> Wane a -> Wane b
(\*/) (Wane f fs) (Wane a as) =  Wane (f a) ([f a' | a' <- as] <> [f' a| f' <- fs])

It's now possible to write shrink for Foo like this 

instance Arbitrary Foo where
    shrink (Foo tata_ titi_) = unWane $ Foo <$> wane tata_ \*/ wane titi_

That scales to more fields just as nicely as applicative style, and the result matches what the variant using tuples produces (same elements, but the order is different).

Tags: haskell quickcheck
15 Jun 2015

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 

/**
 * Create a stack.
 */
void *create();

/**
 * Push a value onto an existing stack.
 */
void push (void *, int);

/**
 * Pop a value off an existing stack.
 */
int pop(void *);

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

{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}

module CApi
    where

import qualified Language.C.Inline as C
import Foreign.Ptr

C.include "stack.h"

create :: IO (Ptr ())
create = [C.exp| void * { create() } |]

push :: Ptr () -> C.CInt -> IO ()
push s i = [C.exp| void { push($(void *s), $(int i)) } |]

pop :: Ptr () -> IO C.CInt
pop s = [C.exp| int { pop($(void *s)) } |]

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: 

newtype Program a = P [a]
    deriving (Eq, Foldable, Functor, Show, Traversable)

Then each of the C API functions can be represented with 

data Statement = Create | Push Int | Pop
    deriving (Eq, Show)

Arbitrary for Statement

My implementation of Arbitrary for Statement is very simple: 

instance Arbitrary Statement where
    arbitrary = oneof [return Create, return Pop, liftM Push arbitrary]
    shrink (Push i) = Push <$> shrink i
    shrink _ = []

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: 

type ModelContext = [R.r| { created :: Bool, pop :: Maybe Int, stack :: [Int] } |]

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

preCond :: ModelContext -> Statement -> Bool
preCond ctx Create = not $ RL.view [R.l| created |] ctx
preCond ctx (Push _) = RL.view [R.l| created |] ctx
preCond ctx Pop = RL.view [R.l| created |] ctx

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: 

modelRunStatement :: ModelContext -> Statement -> ModelContext
modelRunStatement ctx Create = RL.set [R.l| created |] True ctx
modelRunStatement ctx (Push i) = RL.over [R.l| stack |] (i :) ctx
modelRunStatement ctx Pop = [R.r| { created = c, pop = headMay s, stack = tail s } |]
    where
        c = RL.view [R.l| created |] ctx
        s = RL.view [R.l| stack |] ctx

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

instance Arbitrary (Program Statement) where
    arbitrary = liftM P $ ar baseModelCtx
        where
            ar m = do
                push <- liftM Push arbitrary
                let possible = filter (preCond m) [Create, Pop, push]
                if null possible
                    then return []
                    else do
                        s <- oneof (map return possible)
                        let m' = modelRunStatement m s
                        frequency [(499, liftM2 (:) (return s) (ar m')), (1, return [])]

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: 

shrink (P p) = filter allowed $ map P (shrink p)
    where
        allowed = and . snd . mapAccumL go baseModelCtx
            where
                go ctx s = (modelRunStatement ctx s, preCond ctx s)

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 

class S a where
    type Ctx a :: *

    baseCtx :: Ctx a
    preCond :: Ctx a -> a -> Bool
    ...

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 

type RealContext = [r| { o :: Ptr (), pop :: Maybe Int } |]

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

realRunStatement :: RealContext -> Statement -> IO RealContext
realRunStatement ctx Create = CApi.create >>= \ ptr -> return $ RL.set [R.l| o |] ptr ctx
realRunStatement ctx (Push i) = CApi.push o (toEnum i) >> return ctx
    where
        o = RL.view [R.l| o |] ctx
realRunStatement ctx Pop = CApi.pop o >>= \ v -> return $ RL.set [R.l| pop |] (Just (fromEnum v)) ctx
    where
        o = RL.view [R.l| o |] ctx

Comparing states

Comparing a ModelContext and a RealContext is easily done: 

compCtx :: ModelContext -> RealContext -> Bool
compCtx mc rc = mcC == rcC && mcP == rcP
    where
        mcC = RL.view [R.l| created |] mc
        rcC = RL.view [R.l| o |] rc /= nullPtr
        mcP = RL.view [R.l| pop|] mc
        rcP = RL.view [R.l| pop|] rc

Verifying a Program Statement

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

validProgram :: Program Statement -> IO Bool
validProgram p = and <$> snd <$> mapAccumM go (baseModelCtx, baseRealContext) p
    where
        runSingleStatement mc rc s = realRunStatement rc s >>= \ rc' -> return (modelRunStatement mc s, rc')

        go (mc, rc) s = do
            ctxs@(mc', rc') <- runSingleStatement mc rc s
            return (ctxs, compCtx mc' rc')

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

The property, finally!

To wrap this all up I then define the property 

prop_program :: Program Statement -> Property
prop_program p = monadicIO $ run (validProgram p) >>= assert

and a main function 

main :: IO ()
main = quickCheck prop_program

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

Tags: haskell quickcheck testing
Other posts