Reach

Contents

• Introduction
• Reach by Example
• Papers and Presentations
• The Reach Tool
• Current Limitations
• Related Work

Introduction

Reach by Example

module CircLib where

import Reach

tree            :: (a -> a -> a) -> [a] -> a
tree f [x]      =  x
tree f (x:y:ys) =  tree f (ys ++ [f x y])

(/=/)   :: [Bool] -> [Bool] -> Bool
a /=/ b =  tree (&&) (zipWith (==) a b)

prop_eq a b = (a /=/ b) == (num a == num b)

num        :: [Bool] -> Int
num []     =  0
num (a:as) =  fromEnum a + 2 * num as

target :: a -> a

refute       :: Bool -> Bool
refute False =  target False
refute True  =  True

main a b = refute (prop_eq a b)

# yhc --linkcore CircLib.hs
Compiling Reach            ( Reach.hs )
Compiling CircLib          ( CircLib.hs )
Linking...

# reach CircLib.yca
main (True : (True : [])) (True : [])
main (False : (True : [])) (False : [])
main (True : []) (True : (True : []))
main (False : []) (False : (True : []))

prop_eq a b = length a == length b ==> (a /=/ b) == (num a == num b)

# reach CircLib.yca

# reach -r5 CircLib.yca

# reach --crash CircLib.yca
main [] []

prop_eq a b = not (null a) && not (null b) && length a == length b
                ==> (a /=/ b) == (num a == num b)

# reach --crash CircLib.yca

Ok, so what have we achieved? We could have just used QuickCheck or SmallCheck here, right? Well yes, but just take a look at the antecedent on the final version of prop_eq -- it's big, and quite restrictive. The problem is that many blindly generated inputs are not likely to satisfy it, and furthermore, antecedents even more restrictive than this one arise frequently in property-based verification. For fair testing, we really want to generate inputs that satisfy the antecedent -- we all know that property will hold when the antecedent is false!

Therefore, in QuickCheck or SmallCheck the developer might feel urged to define a custom data generator to generate input lists of the same size. In general, this means more work for the developer, and the possibility of introducing a bug when writing the generator. Using Reach, we needn't worry about this! Reach uses Lazy Narrowing to find targets, and as a result, solves antecedents directly, cutting out large regions of the input space that falsify it.

Let's check this final claim with a quick experiment.

A primary goal of Reach is to avoid having to write custom data generators. Let's look at some more evidence that Reach can help achieve this goal.

Example 2 Let's take another example from CircLib, a binary multiplexor.

unaryMux          :: [Bool] -> [[Bool]] -> [Bool]
unaryMux sel xs   =  map (tree (||))
                  $  transpose
                  $  zipWith (\s x -> map (s &&) x) sel xs

decode []         =  [True]
decode [x]        =  [not x,x]
decode (x:xs)     =  concatMap (\y -> [not x && y,x && y]) rest
  where
    rest          =  decode xs

binaryMux         :: [Bool] -> [[Bool]] -> [Bool]
binaryMux sel xs  =  unaryMux (decode sel) xs

Now let's check the correctness of binaryMux. Recall our claim that complex antecedents often arise in property-based testing. Well, here is an illustrative example.

prop_binMux sel xs = length xs == 2 ^ length sel
                       && all ((== length (head xs)) . length) xs)
                         ==> (binaryMux sel xs == xs !! num sel)

main sel xs = refute (prop_binMux sel xs)

Reach is unable to refute this property below depth 11. Now look at the timings compared to exhaustive testing.

The more restrictive the antecedent, the greater need to write a custom data generator, and the greater the benefit of Reach.

Example 3 Let's complement the CircLib library with a little behavioural description library, Flash. Flash provides a number of behavioural circuit abstractions, such as sequential and parallel composition, if statements and while loops.

Now suppose that we're adding a loop optimisation to Flash. To test our optimisation, we may wish to test the library with Flash programs that contain while loops that execute their bodies at least once. Normally one would have to write a custom data generator for this. But we can use Reach to generate such Flash programs very easily. First we make use of another abstraction over target which is exported from Reach.hs.

targetWhen         :: Bool -> a -> a
targetWhen True a  =  target a
targetWhen False a =  a

Now all we need to do is place a target at the point where while loops are treated, and express the constraint that the body gets executed.

circuit (While cond prog) start =  targetWhen
                                     (or (start <&> cond))
                                     (out, finish)
  where (out, finish')          =  circuit prog start'
        active                  =  start <|> finish'
        start'                  =  cond <&> active
        finish                  =  inv cond <&> active

Expressing the constraint is straigtforward, as all the information we need to constrain is in scope. In particular, we just want the start signal and condition signal to be true on at least one clock cycle. Furthermore, with a small change can strengthen the constraint so that only programs with terminating while loops are generated.

# reach Flash.yca
...

main (Wait :>> (Wait :>> (While (_469 : (_491 : (True : _511))) _444)))

Notice that the terms begining with _, such as _469, represent unbound variables -- they could be instantied to anything well-defined and the target would be reached. Notice also that the while loop's condition is true on the third clock cycle, coninciding with its start signal (Wait statements consume one clock cycle and :>> represents sequential composition).

So complex data generators can be rendered rather simple using Reach.

Summary Hopefully we have given a taste of Reach's capabilities, showing that it can often obviate the manual development of custom data generators, a potentially frequent time-consuming and error-prone programming task. For more examples, see our SCAM'07 paper, discussed next. Experimenting with Reach by applying it to more examples is an ongoing task.

Papers and Presentations about Reach

SCAM'07 paper: pdf

SCAM'07 slides: pdf

IFIP WG2.8 Meeting, 2007, slides (by Colin): pdf