{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Test.Tasty.DejaFu
(
testAuto
, testDejafu
, testDejafus
, testAutoWay
, testDejafuWay
, testDejafusWay
, testAutoWithSettings
, testDejafuWithSettings
, testDejafusWithSettings
, Predicate
, ProPredicate(..)
, module Test.DejaFu.Settings
, testProperty
, testPropertyFor
, R.Sig(..)
, R.RefinementProperty
, R.Testable(..)
, R.Listable(..)
, R.expectFailure
, R.refines, (R.=>=)
, R.strictlyRefines, (R.->-)
, R.equivalentTo, (R.===)
, testDejafuDiscard
, testDejafusDiscard
) where
import Data.Char (toUpper)
import qualified Data.Foldable as F
import Data.List (intercalate, intersperse)
import Data.Proxy (Proxy(..))
import Data.Tagged (Tagged(..))
import Data.Typeable (Typeable)
import System.Random (mkStdGen)
import Test.DejaFu hiding (Testable(..))
import qualified Test.DejaFu.Conc as Conc
import qualified Test.DejaFu.Refinement as R
import qualified Test.DejaFu.SCT as SCT
import qualified Test.DejaFu.Settings
import qualified Test.DejaFu.Types as D
import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.Options (IsOption(..), OptionDescription(..),
lookupOption)
import Test.Tasty.Providers (IsTest(..), singleTest, testFailed,
testPassed)
instance IsTest (Conc.ConcIO (Maybe String)) where
testOptions = Tagged concOptions
run options conc callback = do
let memtype = lookupOption options
let way = lookupOption options
let traces = SCT.runSCTWithSettings (set ldiscard (Just (pdiscard assertableP)) (fromWayAndMemType way memtype)) conc
run options (ConcTest traces (peval assertableP)) callback
concOptions :: [OptionDescription]
concOptions =
[ Option (Proxy :: Proxy MemType)
, Option (Proxy :: Proxy Way)
]
assertableP :: Predicate (Maybe String)
assertableP = alwaysTrue $ \case
Right (Just _) -> False
_ -> True
instance IsOption MemType where
defaultValue = defaultMemType
parseValue = shortName . map toUpper where
shortName "SC" = Just SequentialConsistency
shortName "TSO" = Just TotalStoreOrder
shortName "PSO" = Just PartialStoreOrder
shortName _ = Nothing
optionName = Tagged "memory-model"
optionHelp = Tagged "The memory model to use. This should be one of \"sc\", \"tso\", or \"pso\"."
instance IsOption Way where
defaultValue = defaultWay
parseValue = shortName . map toUpper where
shortName "SYSTEMATICALLY" = Just (systematically defaultBounds)
shortName "RANDOMLY" = Just (randomly (mkStdGen 42) 100)
shortName _ = Nothing
optionName = Tagged "way"
optionHelp = Tagged "The execution method to use. This should be one of \"systematically\" or \"randomly\"."
testAuto :: (Eq a, Show a)
=> Conc.ConcIO a
-> TestTree
testAuto = testAutoWithSettings defaultSettings
testAutoWay :: (Eq a, Show a)
=> Way
-> MemType
-> Conc.ConcIO a
-> TestTree
testAutoWay way = testAutoWithSettings . fromWayAndMemType way
testAutoWithSettings :: (Eq a, Show a)
=> Settings IO a
-> Conc.ConcIO a
-> TestTree
testAutoWithSettings settings = testDejafusWithSettings settings
[("Never Deadlocks", representative deadlocksNever)
, ("No Exceptions", representative exceptionsNever)
, ("Consistent Result", alwaysSame)
]
testDejafu :: Show b
=> TestName
-> ProPredicate a b
-> Conc.ConcIO a
-> TestTree
testDejafu = testDejafuWithSettings defaultSettings
testDejafuWay :: Show b
=> Way
-> MemType
-> TestName
-> ProPredicate a b
-> Conc.ConcIO a
-> TestTree
testDejafuWay way = testDejafuWithSettings . fromWayAndMemType way
testDejafuWithSettings :: Show b
=> Settings IO a
-> TestName
-> ProPredicate a b
-> Conc.ConcIO a
-> TestTree
testDejafuWithSettings settings name p = testDejafusWithSettings settings [(name, p)]
testDejafuDiscard :: Show b
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> String
-> ProPredicate a b
-> Conc.ConcIO a
-> TestTree
testDejafuDiscard discard way =
testDejafuWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED testDejafuDiscard "Use testDejafuWithSettings instead" #-}
testDejafus :: Show b
=> [(TestName, ProPredicate a b)]
-> Conc.ConcIO a
-> TestTree
testDejafus = testDejafusWithSettings defaultSettings
testDejafusWay :: Show b
=> Way
-> MemType
-> [(TestName, ProPredicate a b)]
-> Conc.ConcIO a
-> TestTree
testDejafusWay way = testDejafusWithSettings . fromWayAndMemType way
testDejafusWithSettings :: Show b
=> Settings IO a
-> [(TestName, ProPredicate a b)]
-> Conc.ConcIO a
-> TestTree
testDejafusWithSettings = testconc
testDejafusDiscard :: Show b
=> (Either Failure a -> Maybe Discard)
-> Way
-> MemType
-> [(TestName, ProPredicate a b)]
-> Conc.ConcIO a
-> TestTree
testDejafusDiscard discard way =
testDejafusWithSettings . set ldiscard (Just discard) . fromWayAndMemType way
{-# DEPRECATED testDejafusDiscard "Use testDejafusWithSettings instead" #-}
testProperty :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
=> TestName
-> p
-> TestTree
testProperty = testPropertyFor 10 100
testPropertyFor :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
=> Int
-> Int
-> TestName
-> p
-> TestTree
testPropertyFor = testprop
data ConcTest where
ConcTest :: Show b => IO [(Either Failure a, Conc.Trace)] -> ([(Either Failure a, Conc.Trace)] -> Result b) -> ConcTest
deriving Typeable
data PropTest where
PropTest :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p)) => Int -> Int -> p -> PropTest
deriving Typeable
instance IsTest ConcTest where
testOptions = pure []
run _ (ConcTest iotraces p) _ = do
traces <- iotraces
let err = showErr $ p traces
pure (if null err then testPassed "" else testFailed err)
instance IsTest PropTest where
testOptions = pure []
run _ (PropTest sn vn p) _ = do
ce <- R.checkFor sn vn p
pure $ case ce of
Just c -> testFailed . init $ unlines
[ "*** Failure: " ++
(if null (R.failingArgs c) then "" else unwords (R.failingArgs c) ++ " ") ++
"(seed " ++ show (R.failingSeed c) ++ ")"
, " left: " ++ show (F.toList $ R.leftResults c)
, " right: " ++ show (F.toList $ R.rightResults c)
]
Nothing -> testPassed ""
testconc :: Show b
=> Settings IO a
-> [(TestName, ProPredicate a b)]
-> Conc.ConcIO a
-> TestTree
testconc settings tests concio = case map toTest tests of
[t] -> t
ts -> testGroup "Deja Fu Tests" ts
where
toTest (name, p) =
let discarder = maybe id D.strengthenDiscard (get ldiscard settings) (pdiscard p)
traces = SCT.runSCTWithSettings (set ldiscard (Just discarder) settings) concio
in singleTest name $ ConcTest traces (peval p)
testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
=> Int -> Int -> TestName -> p -> TestTree
testprop sn vn name = singleTest name . PropTest sn vn
showErr :: Show a => Result a -> String
showErr res
| _pass res = ""
| otherwise = "Failed:\n" ++ msg ++ unlines failures ++ rest where
msg = if null (_failureMsg res) then "" else _failureMsg res ++ "\n"
failures = intersperse "" . map (\(r, t) -> indent $ either Conc.showFail show r ++ " " ++ Conc.showTrace t) . take 5 $ _failures res
rest = if moreThan (_failures res) 5 then "\n\t..." else ""
moreThan :: [a] -> Int -> Bool
moreThan [] n = n < 0
moreThan _ 0 = True
moreThan (_:xs) n = moreThan xs (n-1)
indent :: String -> String
indent = intercalate "\n" . map ('\t':) . lines