News aggregator

Magnus Therning: Using QuickCheck to test C APIs

Planet Haskell - Sun, 06/14/2015 - 6:00pm

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.

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.

Categories: Offsite Blogs

How do apply conditional transformations

Haskell on Reddit - Sun, 06/14/2015 - 3:58pm

I often find this pattern and I would like to know the best haskelly way to write it. The problem is to apply a set of optional transformations to a value . For example a start and end dates might be given and the goal is to filter to filter what's between the date or not. The imperative way would like :

filterByDate :: HasDate a => Maybe Date -> Maybe Date -> [a] -> [a] filterByDate startM endM as = let as' = case startM of Nothing -> as Just start -> filter (\a -> date a >= startDate) as as'' = case endM of Nothing -> as' Just end -> filter (\a -> date a <- endDate) as' in as''

Of course, we could have more than 2 "filters".

submitted by maxigit
[link] [11 comments]
Categories: Incoming News

[Beginner] Why are function definitions written this way?

Haskell on Reddit - Sun, 06/14/2015 - 1:40pm

I'm wondering why round is defined as: round :: (RealFrac a, Integral b) => a -> b and not as: round :: RealFrac -> Integral

submitted by eviltofu
[link] [15 comments]
Categories: Incoming News

Make Semigroup a superclass of Monoid?

Haskell on Reddit - Sun, 06/14/2015 - 12:44pm

God knows this is one that's been debated enough over the years, I'm only curious whether there's any will in the community in these annīs AMP to revisit making Semigroup a superclass of Monoid. How strong is this will?

submitted by AaronRoth
[link] [64 comments]
Categories: Incoming News

Why I gave up on Haskell

Haskell on Reddit - Sun, 06/14/2015 - 12:31pm

This post is meant as constructive criticism.

I'm a Windows programmer who is used to GUIs and powerful IDEs which do almost anything you may desire from really advanced auto-completion to sophisticated refactoring. These IDEs understand your code!

This doesn't mean that I've never used simple editors. Indeed I started programming in Basic on a Commodore 64.

When I was 8 I had all the time in the world to experiment and a little trial and error was almost welcome. But now I can only try new things (like Haskell) in my spare time so any problem becomes a nuisance.

Another difference from when I was young is that now I know many programming languages so I try new things only when there are clear advantages in doing so.

Since I already know Scala, an expressive language with a powerful type system on a par with that of Haskell, curiosity is the only thing that motivates me to learn Haskell.

I graduated (in CS) magna cum laude so please don't assume this is just the whining of a mediocre coder or of a dumb person.

I really tried to set up a comfortable environment to work with Haskell, but I couldn't. I came across dozens of bugs. Since neither EclipseFP nor IntelliJ plugins worked, I even installed Ubuntu in a VM. I managed to get IntelliJ to work with Haskell, but I wasn't satisfied with it (too slow) so I tried EclipseFP but I couldn't install some external tools.

All the bugs I found are well-known but some workarounds need deep knowledge of how cabal and the Haskell ecosystem work.

If you really want to promote Haskell, you need to provide a complete installer/package with language + tools perfectly working! You can't ask a beginner (in Haskell) to spend hours on google trying to install the damn thing!

I think I'm going to give Haskell another chance in a year or so because functional programming and powerful type systems really fascinate me.

submitted by Kiuhnm
[link] [126 comments]
Categories: Incoming News

New gtk2hs 0.12.4 release

gtk2hs - Wed, 11/21/2012 - 12:56pm

Thanks to John Lato and Duncan Coutts for the latest bugfix release! The latest packages should be buildable on GHC 7.6, and the cairo package should behave a bit nicer in ghci on Windows. Thanks to all!


Categories: Incoming News