Browse files

Refactoring, add new arguments to control how agressive SmartCheck is.

  • Loading branch information...
1 parent 7e121eb commit 7c4adcdab482129cb8d38f86af4ab55bec906d2e @leepike committed Sep 18, 2012
View
17 src/Test/SmartCheck.hs
@@ -25,15 +25,20 @@ import Generics.Deriving
smartCheck :: forall a b. ( Read a, Q.Arbitrary a, SubTypes a
, Generic a, ConNames (Rep a), Q.Testable b )
=> ScArgs -> (a -> b) -> IO ()
-smartCheck args propT = smartCheck' prop []
+smartCheck args propT = do
+ smartPrtLn ("If any stage takes too long to reduce, try reducing the standard\n"
+ ++ "arguments (see Types.hs).")
+ smartCheck' prop []
where
prop a = Q.property $ propT a
smartCheck' :: (a -> Q.Property) -> [a] -> IO ()
smartCheck' prop' ds = do
- -- Run standard QuickCheck.
- res <- runQC (qcArgs args) prop'
+ -- Run standard QuickCheck or read in value.
+ res <- if qc args then runQC (qcArgs args) prop'
+ else do smartPrtLn "Input value to SmartCheck:"
+ getLine >>= return . read
case res of
Nothing -> smartPrtLn "No value to smart-shrink; done."
Just r -> go r
@@ -62,8 +67,8 @@ smartCheck args propT = smartCheck' prop []
else smartPrtLn "Could not extrapolate a new value."
-- Ask the user if she wants to try again.
- putStrLn $ "Attempt to find a new counterexample?"
- ++ " ('Enter' to continue;"
+ putStrLn $ "Attempt to find a new counterexample?\n"
+ ++ " ('Enter' to continue;"
++ " any character then 'Enter' to quit.)"
s <- getLine
if (s == "")
@@ -82,7 +87,7 @@ smartCheck args propT = smartCheck' prop []
nonEmpty d vs cs = vsIdxs || csIdxs
where
vsIdxs = case vs of
- Just (idxs, _) -> (not $ matchesShapes d ds idxs)
+ Just (idxs, _) -> (not $ matchesShapes args d ds idxs)
&& (not $ null idxs)
Nothing -> False
csIdxs = case cs of
View
19 src/Test/SmartCheck/ConstructorGen.hs
@@ -9,6 +9,7 @@ import Test.SmartCheck.DataToTree
import Test.SmartCheck.SmartGen
import Test.SmartCheck.Render
+import Prelude hiding (max)
import Generics.Deriving
import qualified Data.Set as S
import Data.List
@@ -53,7 +54,8 @@ constrsGen args d prop vs = do
-- | Return True if we can generalize; False otherwise.
extrapolateConstrs :: (SubTypes a, Generic a, ConNames (Rep a))
=> ScArgs -> a -> Idx -> (a -> Q.Property) -> IO Bool
-extrapolateConstrs args a idx prop = recConstrs (S.singleton $ subConstr a idx)
+extrapolateConstrs args a idx prop =
+ recConstrs (S.singleton $ subConstr a idx (maxDepth args))
where
notProp = Q.expectFailure . prop
@@ -66,9 +68,11 @@ extrapolateConstrs args a idx prop = recConstrs (S.singleton $ subConstr a idx)
then return True
else do v <- arbSubset args a idx notProp constrs
case v of
- Result x -> recConstrs (subConstr x idx `S.insert` constrs)
+ Result x -> recConstrs (newConstr x)
FailedPreCond -> return False
FailedProp -> return False
+ where
+ newConstr x = subConstr x idx (maxDepth args) `S.insert` constrs
---------------------------------------------------------------------------------
@@ -83,19 +87,20 @@ arbSubset :: (SubTypes a, Generic a, ConNames (Rep a))
arbSubset args a idx prop constrs =
-- Because we're looking for some failure that passes the precondition, we
-- use maxDiscard.
- iterateArb a idx (maxFailure args) (Q.maxSize $ qcArgs args) prop'
+ iterateArbIdx a (idx, maxDepth args)
+ (maxSuccess args) (maxSize args) prop'
>>= return
where
prop' b = newConstr b Q.==> prop b
-- Make sure b's constructor is a new one.
- newConstr b = not $ subConstr b idx `S.member` constrs
+ newConstr b = not $ subConstr b idx (maxDepth args) `S.member` constrs
---------------------------------------------------------------------------------
-subConstr :: SubTypes a => a -> Idx -> String
-subConstr x idx =
- case getAtIdx x idx of
+subConstr :: SubTypes a => a -> Idx -> Maybe Int -> String
+subConstr x idx max =
+ case getAtIdx x idx max of
Nothing -> errorMsg "constrs'"
Just x' -> subTconstr x'
View
8 src/Test/SmartCheck/DataToTree.hs
@@ -90,10 +90,12 @@ getIdxForest forest idx =
getAtIdx :: SubTypes a
=> a -- ^ Parent value
-> Idx -- ^ Index of hole to replace
+ -> Maybe Int -- ^ Maximum depth we want to extract
-> Maybe SubT
-getAtIdx d Idx { level = l
- , column = c }
- = if length lev > c then Just (lev !! c) else Nothing
+getAtIdx d Idx { level = l, column = c } maxLevel
+ | maybe False ((>) l) maxLevel = Nothing
+ | length lev > c = Just (lev !! c)
+ | otherwise = Nothing
where
lev = getLevel (subTypes d) l
View
18 src/Test/SmartCheck/Extrapolate.hs
@@ -43,14 +43,14 @@ extrapolate args d origProp ds = do
forest = mkSubstForest d True
iter' = iter d test next origProp
prop idxs newProp a =
- (not $ matchesShapes a (d : ds) idxs) Q.==> newProp a
+ (not $ matchesShapes args a (d : ds) idxs) Q.==> newProp a
-- In this call to iterateArb, we want to claim we can extrapolate iff at
-- least one test passes a precondition, and for every test in which the
-- precondition is passed, it fails. We test values of all possible sizes, up
-- to Q.maxSize.
- test _ idx = iterateArb d idx (Q.maxSuccess $ qcArgs args)
- (Q.maxSize $ qcArgs args) origProp
+ test _ idx = iterateArbIdx d (idx, maxDepth args) (maxSuccess args)
+ (maxSize args) origProp
-- Control-flow.
next _ res forest' idx idxs =
@@ -68,26 +68,26 @@ extrapolate args d origProp ds = do
-- | Finds any two distinct values that match. INVARIANT: the ds are all
-- unequal, and d /= any ds.
-matchesShapes :: SubTypes a => a -> [a] -> [Idx] -> Bool
-matchesShapes d ds idxs = foldl' f False ds
+matchesShapes :: SubTypes a => ScArgs -> a -> [a] -> [Idx] -> Bool
+matchesShapes args d ds idxs = foldl' f False ds
where
f True _ = True
- f False d' = matchesShape d d' idxs
+ f False d' = matchesShape args d d' idxs
-- | Are the value's constructors the same (for algebraic constructors only
-- (e.g., omits Int)), and all the direct children constructors the same (for
-- algebraic constructors only, while ignoring differences in all values at
-- holes indexed by the indexes.
-matchesShape :: SubTypes a => a -> a -> [Idx] -> Bool
-matchesShape a b idxs = test (subT a, subT b) && repIdxs
+matchesShape :: SubTypes a => ScArgs -> a -> a -> [Idx] -> Bool
+matchesShape args a b idxs = test (subT a, subT b) && repIdxs
where
repIdxs = case foldl' f (Just b) idxs of
Nothing -> False
Just b' -> and . map test $ zip (nextLevel a) (nextLevel b')
f mb idx = do
b' <- mb
- v <- getAtIdx a idx
+ v <- getAtIdx a idx (maxDepth args)
replace b' idx v
nextLevel x = map rootLabel (subTypes x)
View
51 src/Test/SmartCheck/Reduce.hs
@@ -24,7 +24,7 @@ import Data.Maybe
smartRun :: SubTypes a => ScArgs -> a -> (a -> Q.Property) -> IO a
smartRun args res prop = do
putStrLn ""
- smartPrtLn "Smart Shrinking ... "
+ smartPrtLn "Smart Shrinking ..."
new <- smartShrink args res prop
smartPrtLn "Smart-shrunk value:"
print new
@@ -67,32 +67,41 @@ smartShrink args d prop =
-- idx.
test :: a -> Idx -> IO (Maybe a)
test x idx = do
- hole <- testHole (getAtIdx x idx)
- if isJust hole then return hole
- else do r <- iterateArb x idx (maxFailure args) (maxSize x idx) notProp
- return $ case r of
- Result a -> Just a
- FailedPreCond -> Nothing
- FailedProp -> Nothing
+ let vm = getAtIdx x idx (maxDepth args)
+ case vm of
+ Nothing -> errorMsg "smartShrink0"
+ Just v -> do
+ hole <- testHole v
+ if isJust hole then return hole
+ else do r <- iterateArb x v idx (maxFailure args)
+ -- Maximum size of values to generate; the minimum of
+ -- the value at the current index and the maxSize
+ -- parameter.
+ (min (subValSize x idx) (maxSize args))
+ notProp
+ return $ resultToMaybe r
where
-- -- XXX debuging
-- sh (Just SubT { unSubT = v }) = show v
- testHole :: Maybe SubT -> IO (Maybe a)
- testHole Nothing = return Nothing
- testHole (Just SubT { unSubT = v }) =
+ testHole :: SubT -> IO (Maybe a)
+ testHole SubT { unSubT = v } =
case cast v :: Maybe a of
Just v' -> extractAndTest v'
Nothing -> return Nothing
where
extractAndTest :: a -> IO (Maybe a)
extractAndTest y = do
res <- resultify notProp y
- return $ case res of
- FailedPreCond -> Nothing
- FailedProp -> Nothing
- Result n -> Just n
+ return $ resultToMaybe res
+
+resultToMaybe :: Result a -> Maybe a
+resultToMaybe res =
+ case res of
+ FailedPreCond -> Nothing
+ FailedProp -> Nothing
+ Result n -> Just n
---------------------------------------------------------------------------------
@@ -104,14 +113,14 @@ smartShrink args d prop =
-- (:) C
-- (:) C []
--- At (Idx 0 0) in v, we're at C, so maxSize v (Idx 0 0) == 0.
--- At (Idx 0 1) in v, we're at (C : C : []), so maxSize v (Idx 0 1) == 2, since
+-- At (Idx 0 0) in v, we're at C, so subValSize v (Idx 0 0) == 0.
+-- At (Idx 0 1) in v, we're at (C : C : []), so subValSize v (Idx 0 1) == 2, since
-- we have the constructors :, C (or :, []) in the longest path underneath.
--- Base-types have maxSize 0. So maxSize [1,2,3] idx == 0 for any idx.
--- Note that if we have maxSize d idx == 0, then it is impossible to construct a
+-- Base-types have subValSize 0. So subValSize [1,2,3] idx == 0 for any idx.
+-- Note that if we have subValSize d idx == 0, then it is impossible to construct a
-- *structurally* smaller value at hole idx.
-maxSize :: SubTypes a => a -> Idx -> Int
-maxSize d idx = maybe 0 id (fmap depth forestIdx)
+subValSize :: SubTypes a => a -> Idx -> Int
+subValSize d idx = maybe 0 id (fmap depth forestIdx)
where
forestIdx :: Maybe [Tree Bool]
forestIdx = fmap subForest $ getIdxForest (mkSubstForest d True) idx
View
52 src/Test/SmartCheck/SmartGen.hs
@@ -1,7 +1,8 @@
{-# LANGUAGE ScopedTypeVariables #-}
module Test.SmartCheck.SmartGen
- ( iterateArb
+ ( iterateArbIdx
+ , iterateArb
, resultify
, replace
, iter
@@ -14,11 +15,21 @@ import qualified Test.QuickCheck.Gen as Q
import qualified Test.QuickCheck as Q hiding (Result)
import qualified Test.QuickCheck.Property as Q
+import Prelude hiding (max)
import System.Random
import Data.Tree hiding (levels)
---------------------------------------------------------------------------------
+-- | Driver for iterateArb.
+iterateArbIdx :: SubTypes a
+ => a -> (Idx, Maybe Int) -> Int -> Int
+ -> (a -> Q.Property) -> IO (Result a)
+iterateArbIdx d (idx, max) tries sz prop =
+ case getAtIdx d idx max of
+ Nothing -> errorMsg "iterateArb 0"
+ Just ext -> iterateArb d ext idx tries sz prop
+
-- | Replace the hole in d indexed by idx with a bunch of random values, and
-- test the new d against the property. Returns the first new d (the full d but
-- with the hole replaced) that succeeds. "Succeeds" is determined by the call
@@ -29,28 +40,25 @@ import Data.Tree hiding (levels)
-- (Thus, there's an implied linear order on the Result type: FailedPreCond <
-- FailedProp < Result a.)
iterateArb :: forall a. SubTypes a
- => a -> Idx -> Int -> Int -> (a -> Q.Property) -> IO (Result a)
-iterateArb d idx tries maxSize prop = do
+ => a -> SubT -> Idx -> Int -> Int
+ -> (a -> Q.Property) -> IO (Result a)
+iterateArb d ext idx tries max prop = do
g <- newStdGen
iterateArb' FailedPreCond g 0 0
where
- ext :: SubT
- ext = case getAtIdx d idx of
- Just v -> v
- Nothing -> errorMsg "iterateArb 0"
-
- newMax SubT { unSubT = v } = maxDepth v
+ newMax SubT { unSubT = v } = valDepth v
-- Main loop. We break out if we ever satisfy the property. Otherwise, we
-- return the latest value.
iterateArb' :: Result a -> StdGen -> Int -> Int -> IO (Result a)
iterateArb' res g try currMax
-- We've exhausted the number of iterations.
| try >= tries = return res
- -- Values are now too big. Start again with size at 0.
- | newMax s >= maxSize = iterateArb' res g0 (try + 1) 0
- | otherwise =
+ -- The generated random value is too big. Start again sampling again with
+ -- size at 0.
+ | newMax s >= max = iterateArb' res g0 (try + 1) 0
+ | otherwise = --trace ("iter: " ++ show try ++ show s) $
case replace d idx s of
Nothing -> errorMsg "iterateArb 1"
Just d' -> do
@@ -65,13 +73,15 @@ iterateArb d idx tries maxSize prop = do
s = sample ext g size
sample SubT { unSubT = v } = newVal v
rec res' = iterateArb' res' g0 (try + 1)
- (currMax * 2) -- XXX what ratio is right to increase size of
- -- values? This gives us exponentail growth, but
- -- remember we're randomly chosing within the
- -- range of [0, max], so many values are
- -- significantly smaller than the max. Plus we
- -- reset the size whenever we get a value that's
- -- too big.
+ ((currMax + 1) * 2) -- XXX what ratio is right to increase size
+ -- of values? This gives us exponentail
+ -- growth, but remember we're randomly
+ -- chosing within the range of [0, max], so
+ -- many values are significantly smaller
+ -- than the max. Plus we reset the size
+ -- whenever we get a value that's too big.
+ -- Note the need for (+ 1), since we seed
+ -- with 0.
---------------------------------------------------------------------------------
@@ -149,7 +159,7 @@ iter d test nxt prop forest idx idxs
-- | Get the maximum depth of a value, where depth is measured in the maximum
-- depth of the tree representation, not counting base types (defined in
-- Types.hs).
-maxDepth :: SubTypes a => a -> Int
-maxDepth d = depth (mkSubstForest d True)
+valDepth :: SubTypes a => a -> Int
+valDepth d = depth (mkSubstForest d True)
---------------------------------------------------------------------------------
View
34 src/Test/SmartCheck/Types.hs
@@ -50,21 +50,39 @@ data Format = PrintTree | PrintString
data ScArgs =
ScArgs { treeShow :: Format -- ^ How to show extrapolated formula
, qcArgs :: Q.Args -- ^ QuickCheck arguments
- , maxFailure :: Int -- ^ How hard to look for failure
+ --------------
+ , qc :: Bool -- ^ Should we run QuickCheck? (If not, you
+ -- are expected to pass in data to analyze.)
, extrap :: Bool -- ^ Should we extrapolate?
, constrGen :: Bool -- ^ Should we try to generalize constructors?
+ --------------
+ , maxSuccess :: Int -- ^ How hard (number of rounds) to look for
+ -- failures durbing the extrapolation and
+ -- constructor generalization stages.
+ , maxFailure :: Int -- ^ How hard (number of rounds) to look for
+ -- failure in the reduction stage.
+ , maxSize :: Int -- ^ Maximum size of data to generate, in terms
+ -- of the size parameter of QuickCheck's
+ -- Arbitrary instance for your data.
+ , maxDepth :: Maybe Int -- ^ How levels into the structure of the
+ -- failed value should we descend when
+ -- reducing or generalizing? Nothing
+ -- means we go down to base types.
}
deriving (Show, Read)
scStdArgs :: ScArgs
scStdArgs = ScArgs { treeShow = PrintTree
- -- Let's let us fail at least 100 times to pass the
- -- precondition, then maxSuccess more to try to find a
- -- failure.
- , maxFailure = 100 + Q.maxSuccess Q.stdArgs
, qcArgs = Q.stdArgs
+ --------------
+ , qc = True
, extrap = True
, constrGen = True
+ --------------
+ , maxSuccess = 100
+ , maxFailure = 100
+ , maxSize = 10
+ , maxDepth = Nothing
}
---------------------------------------------------------------------------------
@@ -73,10 +91,10 @@ scStdArgs = ScArgs { treeShow = PrintTree
-- | Possible results of iterateArb.
data Result a = FailedPreCond -- ^ Couldn't satisfy the precondition of a
- -- QuickCheck property
+ -- QuickCheck property
| FailedProp -- ^ Failed the property---either we expect
- -- failure and it passes or we expect to pass it
- -- and we fail.
+ -- failure and it passes or we expect to pass it
+ -- and we fail.
| Result a -- ^ Satisfied it, with the satisfying value
deriving (Show, Read, Eq)

0 comments on commit 7c4adcd

Please sign in to comment.