leepike/smartcheck

A Smarter QuickCheck

smartcheck's Issues

Wrong generalization for the overflow example (PaperExample1)

This is perhaps related to issue #12.

For the motivating example of the SmartCheck paper, SmartCheck reports a correct counter-example,
but an incorrect generalization:

forall values x0 x1 x2 x3:

T x3 (: -21874 x0) x2 (: -12585 []) x1

It is too general and includes values that are not counter-examples:

> let x0 = [21874]; x1 = []; x2 = []; x3 = []
> prop (T x3 (-21874:x0) x2 (-12585:[]) x1)
True

I have run the example with the default parameters, maybe tuning it to test more could fix this.

Upload to Hackage

When can we expect to see smartcheck on Hackage? If you don't think it's ready, where does it need work and how can the rest of us help?

I've played with it a bit via cabal-dev, and it seems pretty great!

SmartCheck not compiling with GHC 8.0.2 or QuickCheck 2.10.*

Hello,

I think SmartCheck-0.2.2 does not compile under GHC 8.0.2 or with QuickCheck 2.10.*. Though this may be just my system misbehaving. I have tried the following.

Starting from a fresh home directory, I did:

$ cabal update
Downloading the latest package list from hackage.haskell.org
$ cabal install smartcheck
Resolving dependencies...
Downloading smartcheck-0.2.2...
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Failed to install smartcheck-0.2.2
Build log ( /home/testuser/.cabal/logs/smartcheck-0.2.2.log ):
cabal: Entering directory '/tmp/cabal-tmp-30973/smartcheck-0.2.2'
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Preprocessing library smartcheck-0.2.2...
<command line>: cannot satisfy -package-id QuickCheck-2.10.0.1-ALuGysu7txTB2VnkPyDuTq
    (use -v for more information)
cabal: Leaving directory '/tmp/cabal-tmp-30973/smartcheck-0.2.2'
cabal: Error: some packages failed to install:
smartcheck-0.2.2 failed during the building phase. The exception was:
ExitFailure 1

After some fiddling around, I installed the immediately previous version
of QuickCheck (2.9.2):

$ cabal install tf-random primitive random generic-deriving mtl --reinstall --force-reinstalls
...
$ cabal install QuickCheck-2.9.2
...
Installed QuickCheck-2.9.2

When I try to install install SmartCheck bound with QuickCheck-2.9.2, I get a compilation error message:

$ cabal install smartcheck --constraint 'QuickCheck <= 2.9.2'
Resolving dependencies...
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Failed to install smartcheck-0.2.2
Build log ( /home/testuser/.cabal/logs/smartcheck-0.2.2.log ):
cabal: Entering directory '/tmp/cabal-tmp-1490/smartcheck-0.2.2'
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Preprocessing library smartcheck-0.2.2...

src/Test/SmartCheck/Types.hs:6:14: warning:
    -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
[ 1 of 11] Compiling Test.SmartCheck.Types ( src/Test/SmartCheck/Types.hs, dist/build/Test/SmartCheck/Types.o )

src/Test/SmartCheck/Types.hs:256:10: error:
    • No instance for (Generic Char)
        arising from a use of ‘Test.SmartCheck.Types.$dmsubTypes’
    • In the expression: Test.SmartCheck.Types.$dmsubTypes @Char
      In an equation for ‘subTypes’:
          subTypes = Test.SmartCheck.Types.$dmsubTypes @Char
      In the instance declaration for ‘SubTypes Char’

...

src/Test/SmartCheck/Types.hs:259:10: error:
    • No instance for (Generic Int)
        arising from a use of ‘Test.SmartCheck.Types.$dmshowForest’
    • In the expression: Test.SmartCheck.Types.$dmshowForest @Int
      In an equation for ‘showForest’:
          showForest = Test.SmartCheck.Types.$dmshowForest @Int
      In the instance declaration for ‘SubTypes Int’
cabal: Leaving directory '/tmp/cabal-tmp-1490/smartcheck-0.2.2'
cabal: Error: some packages failed to install:
smartcheck-0.2.2 failed during the building phase. The exception was:
ExitFailure 1

This may be my system, but it seems this issue is related to the fact that
Generic instances have been removed from base types starting with GHC 8.0. See
comment number 7 from GHC ticket 10532. See also this issue from lens and
this issue from optparse.

I am using GHC 8.0.2, cabal-install 1.24.0.2 and Cabal 1.24.2.0.

I tried installing under GHC 7.10 and it worked fine.

Bug in SmartCheck pretty printer

While trying to run SmartCheck, I've bumped into some problems. I've tried
both vanilla scStdArgs (check prop = smartCheck scStdArgs) and this version here:

check prop = smartCheck scArgs prop
     where scArgs = scStdArgs { format      = PrintString
                              , scMaxForall = 100     -- 20
                              , scMinForall = 50      -- 10
                              , scMaxExists = 50      -- 20
                              , scMaxDepth  = Just 5  -- Nothing
                              , scMaxSize   = 20      -- 10
                              }

The property described here are very simple but artificial, just to show, in the simplest form possible, issues I've seen.

Missing boolean on Counterexample

This property should fail for False *:

prop_booleans :: Bool -> Bool -> Bool
prop_booleans p q = p

But actually, SmartCheck reports failing for only False (it should be False False or False True). And it is not able to extrapolate:

> check prop_booleans
Failed! Falsifiable (after 1 test):
False
*** (If any stage takes too long, try modifying SmartCheck's standard arguments (see Args.hs).)

*** Smart Shrinking ...
*** Smart-shrunk value:
False

*** Extrapolating values ...

*** Extrapolating Constructors ...
*** Could not extrapolate a new value.

Attempt to find a new counterexample?
  ('Enter' to continue; any character then 'Enter' to quit.)

+++ OK, passed 100 tests.
*** No value to smart-shrink; done.

Of the counterexamples reported in other properties, I've noticed that the
first parameter is usually missing.

QuickCheck correctly reports the output:

> quickCheck prop_booleans
*** Failed! Falsifiable (after 5 tests and 1 shrink):
False
False

Lazy SmallCheck is able to report the partial counterexample:

> depthCheck 3 prop_booleans
LSC: Counterexample found after 3 tests.
Var 0: False
Var 1: _

Tuples of booleans

Another issue happens for a slightly different statement of the property above:

-- This should fail for "(False,*)"
prop_booleans2 :: (Bool,Bool) -> Bool
prop_booleans2 (p,q) = p

After running SmartCheck, it is able to correctly report a counterexample
(False,True), but it is not able to extrapolate that to (False,*).
SmartCheck is supposed to work that way in this case?

> check prop_booleans2
*** Failed! Falsifiable (after 1 test):
*** (If any stage takes too long, try modifying SmartCheck's standard arguments (see Args.hs).)

*** Smart Shrinking ...
*** Smart-shrunk value:
(False,True)

*** Extrapolating values ...

*** Extrapolating Constructors ...
*** Could not extrapolate a new value.

Attempt to find a new counterexample?
  ('Enter' to continue; any character then 'Enter' to quit.)

*** Gave up! Passed only 0 tests.
*** No value to smart-shrink; done.

Lazy SmallCheck is also able to report the partial counterexample:

> depthCheck 3 prop_booleans2
LSC: Counterexample found after 4 tests.
Var 0: (False,_)
*** Exception: ExitFailure 1

Nub on lists of integers

This property should fail for any list containing a repeated element:

prop_nub :: [Int] -> Bool
prop_nub xs = xs == nub xs

When running SmartCheck, it displays a (correct) counterexample, but extrapolates that to something invalid:

*** Failed! Falsifiable (after 7 tests):
*** (If any stage takes too long, try modifying SmartCheck's standard arguments (see Args.hs).)

*** Smart Shrinking ...
*** Smart-shrunk value:
[4,4]

*** Extrapolating values ...

*** Extrapolating Constructors ...

*** Extrapolated value:
forall values x0:

: 4 (: x0 [])

[4,*] is clearly not a correct extrapolation. A correct one would be
[4,4,*] or 4:4:*. Or am I misinterpreting the output?

Versions

I'm using HEAD SmartCheck (7c35ea3). My GHC is 7.8.2.

Support custom QuickCheck generators

It would be nice if SmartCheck supported custom generators, like QuickCheck does with forAll. For example, I want to use SmartCheck to test an interpreter I'm working on, but I need to be able generate expressions of a given type. I can probably work around it with the standard newtype trick though, for now.

Bug/regression: no counter-example for `\xs -> nub xs == (xs :: [Int])`

Hi,

I think I found a regression on SmartCheck-0.2.2 in relation to SmartCheck-0.2.1.

Consider the following minimal SmartChecking program:

import Test.SmartCheck
import Data.List (nub)

main :: IO ()
main = smartCheck scStdArgs{format = PrintString}
     $ \xs -> nub xs == (xs :: [Int])

0.2.1

When compiled and run against smartcheck-0.2.1, it produces:

$ ghc-7.10 -dynamic list.hs
$ yes | ./list
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 6 tests):  
*** Smart Shrinking ...
*** Smart-shrunk value:
[-2,-2]
*** Extrapolating values ...
*** Extrapolating Constructors ...
*** Extrapolated value:
forall values x0:
: -2 (: -2 x0)
*** Done.

So far so good. This is what I would expect. The tail of the list is generalized. The property fails regardless of the tail.

(Above, I have trimmed/summarized the output a bit.)

0.2.2

When compiled and run against smartcheck-0.2.2, it produces:

$ ghc-7.10 -dynamic list.hs
$ yes | list
*** Finding a counterexample with QuickCheck...
+++ OK, passed 1 tests.

*** Analyzing the first argument of the property with SmartCheck...
*** (If any stage takes too long, modify SmartCheck's arguments.)
*** No value to smart-shrink; done.

SmartCheck fails to report a counter-example and says it passes the property for just 1 test.

(Above, output is in full.)

Details

• smartcheck-0.2.1 was compiled against QuickCheck-2.7.6;
• smartcheck-0.2.2 was compiled against QuickCheck-2.9.2;
• In both cases I was using GHC 7.10.3;
• This is perhaps related to issue #5.

SmartCheck fails to compile against QuickCheck 2.8

The root of the problem seems to be that QuickCheck restructured its internal State type a bit.

Shrinking base types

Add a way to optionally shrink base types.

One way to do this would be to define a "shrink-like" class, and the user can define instances for types they want to shrink. Then during the reduction phase, it will additionally shrink according to the definition. I can't use QC's shrink directly, since shrink is defined by default for base types.

Note that simply using a newtype won't help, since base types inside of a new or data type isn't touched.

Only activate existential sub-value generalization when there is more than one constructor

This is more of a feature request than a bug itself.

When there is only one possible constructor, existential sub-value generalization does not produce a
very useful result.

Consider the following faulty sort implementation along with a property:

sort :: Ord a => [a] -> [a]
sort [] = []
sort (x:xs) = sort (filter (< x) xs)
           ++ [x]
           ++ sort (filter (> x) xs)

prop_sortCount :: Int -> [Int] -> Bool
prop_sortCount x xs = count x (sort xs) == count x xs
  where
  count x = length . filter (== x)

The property fails, as shown by QuickCheck:

> quickCheck prop_sortCount
*** Failed! Falsifiable (after 51 tests and 9 shrinks):
21
[21,21]

The generalization produced by SmartCheck is not very useful, see:

> smartCheck scStdArgs{format = PrintString} (prop_sortCount :: Int -> [Int] -> Bool)
*** Failed! Falsifiable (after 57 tests and 10 shrinks):
*** Non SmartChecked arguments:
[-10,-10]

*** Analyzing the first argument of the property with SmartCheck...
*** Smart-shrunk value:
-10

*** Extrapolated value:
forall constructors C0:
  there exist arguments x̅ s.t.

 C0

The existential sub-value generalization is correct: for all possible constructors (GHC.Int) there exists a value (-10) that falsifies the property. But that is obvious from the reported counter-example itself.

Perhaps existential sub-value generalization should only activate when there is more than one constructor that can be placed? (In which case it is really useful -- cf. divSubTerms example from SmartCheck's paper.)

Notes

If we set runExists = False, SmartCheck reports that it cannot extrapolate a
new value -- this is what I would intuitively expect in this case.

SmartCheck does work flawlessly if we uncurry the property (so it can
generalize the second argument as well):

> smartCheck scStdArgs{format = PrintString} $ uncurry prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 8 tests):
*** Smart-shrunk value:
(5,[5,5])

*** Extrapolated value:
forall values x0: (,) 5 (: 5 (: 5 x0))

The sort example is also used in issue #12.

Counter-example too general (includes incorrect counter-examples)

Consider the following faulty sort implementation along with a property:

sort :: Ord a => [a] -> [a]
sort [] = []
sort (x:xs) = sort (filter (< x) xs)
           ++ [x]
           ++ sort (filter (> x) xs)

prop_sortCount :: Int -> [Int] -> Bool
prop_sortCount x xs = count x (sort xs) == count x xs
  where
  count x = length . filter (== x)

SmartCheck does work flawlessly if we uncurry the property so it can generalize the second argument as well:

> smartCheck scStdArgs{format = PrintString} $ uncurry prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 8 tests):
*** Smart-shrunk value:
(5,[5,5])

*** Extrapolated value:
forall values x0: (,) 5 (: 5 (: 5 x0))

However, if we flip the property so that SmartCheck can generalize only the second argument, the reported generalization is incorrect:

*Main Test.QuickCheck> smartCheck scStdArgs{format = PrintString} $ flip prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 11 tests):
*** Non SmartChecked arguments:
0
*** Analyzing the first argument of the property with SmartCheck...
*** Smart-shrunk value:
[8,-10,9,0,0,-9,-3,4,-4]

*** Extrapolated value:
forall values x0:
: 8 x0

By incorrect, I mean it includes values that are not counter-examples, like 8:[] or 8:7:6:[]. Of course, it also includes correct counter-examples, like: 8:8:[].

I would expect it to report something like:

*** Extrapolated value:
forall values x0:
: 8 (: 9 (: 0 (: 0 x0)))

I understand this may be hard to fix because of the nature of the generalization algorithm that is being used. The algorithm is unsound in the general case anyway.

I have run this with default values. Maybe just changing the parameters may get rid of the incorrect generalization.

Notes

The sort example is also used in issue #11.