Catch: A User Manual

by Neil Mitchell

Catch is a tool for checking that a piece of Haskell code does not have any inexhaustive pattern matches, and will not fail at runtime with a pattern match error. For the purposes of Catch, the includes things like passing the empty list to head, or division by zero.

This document proceeds as follows:

Obtaining and Installing Catch
A Walkthrough of Risers
Running Your Example
Reading Constraints
Flag Reference
Limitations

Acknowledgements

Thanks to Colin Runciman, Malcolm Wallace, Matt Naylor, Tom Shackell and everyone in PLASMA for useful feedback.

Obtaining and Installing Catch

Installing Yhc

Catch has Yhc as a dependency, so before installing Catch you must first install Yhc. See this page for details of installation. Once you have installed Yhc, add it to your search path so that the yhc command is available and can compile files.

If you aren't able to compile Yhc in its entirity, then the following is sufficient:

scons build yhc
scons build libraries

Installing Catch

Take a Catch tarball, and unpack. Then invoke the standard Cabal magic:

runhaskell Setup configure
runhaskell Setup build
runhaskell Setup install

A Walkthrough of Risers

This section describes how to run the example Risers program.

Open the command line and type:

catch Risers

Note that it goes through various stages, and comes to the answer at the end

Answer: _

Think of this answer as a pattern match, _ means that regardless of the inputs to Risers, it will not crash.

Running Your Example

This is intended to be a basic overview of the recommended best practice for trying a new example with Catch.

First find your code, something under 500 lines is probably best - start small (10 lines) and work your way up. Remember that even a 2 line program may pull in 1000's of lines of libraries, so do not think of program size as an absolute.

Your code should either be a program with a main function, or a library with an export list (restricted to one module deep names currently). If you wish to check a fragment which does not have main :: IO (), then name the module something else.

Next check that Yhc is able to compile your code, if it cannot then fix either the code or Yhc until you have success.

Now check the program by typing catch testname. To take a program such as HsColour, we would get:

Checking [1/5]: Language.Haskell.HsColour.Classify: Pattern match failure in fun
ction at 56:1-63:26.
Partial: "Language.Haskell.HsColour.Classify.nestcomment.4"
Partial: "Language.Haskell.HsColour.Classify.nestcomment"
Partial: "Language.Haskell.HsColour.Classify.nestcomment.5"
Answer: _
Checking [2/5]: PreludeList.foldr1: empty list
Partial: "Prelude.fold$292"
Answer: _
Checking [3/5]: PreludeList.head: empty list
Partial: "Prelude.head"
Partial: "Language.Haskell.HsColour.Classify.chunk.6"
Partial: "Main.Main.Prelude.319.useDefault$269.1"
Partial: "Main.Main.Prelude.319.useDefault$710.1"
Answer: _
Checking [4/5]: PreludeList.last: empty list
Partial: "Prelude.last"
Partial: "Main.Main.Prelude.313.writeResult$283.1"
Answer: _
Checking [5/5]: PreludeList.tail: empty list
Partial: "Prelude.tail"
Partial: "Language.Haskell.HsColour.Classify.chunk.6"
Answer: _
Checking whole program
Answer: _

Each "Checking" output corresponds to the error message the user would see at runtime if this pattern was invoked. For example, the second would give an error message about foldr1 being on an empty list - which clearly shows where the problem is. Functions often have specialised variants generated, Prelude.fold$30 is one of these - which comes from foldr originally.

Another example is the third error message. Here the function head has transmitted a precondition to useDefault, which is defined in module Main. The precondition extends no further than this though, so will never occur in practice.

We can examine the useDefault function more closely, we can find its original definition in HsColour:

useDefault d f list | null list = d
                    | otherwise = f (head list)

And if we turn on the --dcore flag to Catch, we can take a look at ycr/HsColour.6.ShortCtors.txt, which gives the functions relating to useDefault just before analysis. Another option is to look at the LetElim file, which is a close match to the original code:

Main.Main.Prelude.311.useDefault$24 v1 v4 =
    Main.Main.Prelude.311.useDefault$24.1 (Prelude.null v4) v1 v4

Main.Main.Prelude.311.useDefault$24.1 v2 v1 v4 =
    case v2 of
        Prelude.True -> v1
        Prelude.False -> Prelude.head v4

Main.Main.Prelude.311.useDefault$93 v1 v2 v8 v9 v10 =
    Main.Main.Prelude.311.useDefault$93.1
      (Prelude.null v1)
      v10
      v2
      v8
      v9
      v1

Main.Main.Prelude.311.useDefault$93.1 v3 v10 v2 v8 v9 v1 =
    case v3 of
        Prelude.True -> Main.Main.Prelude.307.ttyInteract$94 v2 v8 v9 v10
        Prelude.False ->
            Main.Main.Prelude.306.fileInteract$262
              (Prelude.head v1)
              v2
              v8
              v9
              v10

Both versions have been specialised, with functional arguments frozen in - id for useDefault$24 and fileInteract for useDefault$93. Focusing on the simpler of these two ($24), we can see that useDefault$24.1 is potentially unsafe, as Catch told us. We can also see that its call is safe, as Catch also said.

When tracking down an error, I typically look at the partial list, find the first function in that list that should not be there, and go there to find where the error is likely to be.

Reading Constraints

Here are some sample constraints, and their meanings. This section could probably do with being expanded.

_ Anything is safe.
0 Nothing is safe.
{True} Must be the constructor True.
{[]} Must be the constructor [].
{Just {True}} | {Nothing} Must be Just True or Nothing.
{#2 _ {True}} The function takes 2 arguments, the second must be True.
{: _ * _} Must be the constructor (:). The first _ is the restriction on the head, the * is merely a separator, and the second _ is the restriction on all tails.
{: {True} * {: {True} | []}} | [] Must be a list of any size, with True for all elements.

Catch could probably do with writing its constraints in some human friendly way - although quite what form this would take is still unclear. Counter example generation is likely to be useful, and is on the todo list.

Command Line Reference

The command line structure for Catch interprets any argument begining with a - (hyphen) as an argument, and any others as a file. Arguments may occur in any order.

Specifying Files

You may specify any one of:

.hs/.lhs Treated as a Haskell file, and compiled using Yhc. If no extension is given, this extension is infered.
.txt A text file, listing files to analyse one per line.
Directory A directory of .hs/.lhs files, all which be analysed separately.

Files are searched for in the current directory and in %CATCH_BASE_PATH%/examples/*/. This allows the standard examples to be executed by Catch without worrying about directories etc.

Options

Standard options:
  -v           --version            show version number
  -h, -?       --help               show help message
  -q           --quiet              final results only
  -t[SECONDS]  --timeout[=SECONDS]  timeout per error, 0=inf
  -s N,M       --skip=N,M           list of errors to skip
  -y flags     --yhc=flags          extra flags to give to Yhc

Debug options:
               --dlog               ouptput property/precondition logs
               --dcore              output intermediate Yhc.Core files
               --dtime              display CPU time
               --dmemory            display memory useage
               --dprofile           run with profiling

Limitations

Catch is still very much alpha software, and may be delicate from time to time.

IO errors Several IO operations can raise "errors", which semantically are _|_, Catch will not detect these. Examples include readFile, getEnv, createDirectory etc.
Missing libraries Some programs may import libraries that Catch does not support. In actual fact, these are missing from Yhc which Catch requires - adding them to Yhc will fix your problem.
Firstifier non-terminates Some programs will not terminate in the firstifier. If the program has this behaviour, email it to me. There are a few known cases of this, which are being investigated.
Analysis takes forever This is unlikely, but it may well take a very long time. Adding either --skip or --timeout can be used to ignore this particular error.
Timeout does not work Not sure why, but I have very limited success with the timeout flag.

The larger the program, the more likely that Catch will run into one of these issues - however a large program in itself will not cause any issues.