#if __GLASGOW_HASKELL__ >= 800
#endif
module Test.Tasty.DejaFu
(
testAuto
, testDejafu
, testDejafus
, testAuto'
, testDejafu'
, testDejafus'
, testAutoIO
, testDejafuIO
, testDejafusIO
, testAutoIO'
, testDejafuIO'
, testDejafusIO'
, Bounds(..)
, MemType(..)
) where
import Control.Monad.ST (runST)
import Data.Char (toUpper)
import Data.List (intercalate, intersperse)
import Data.Proxy (Proxy(..))
import Data.Tagged (Tagged(..))
import Data.Typeable (Typeable)
import Test.DejaFu
import qualified Test.DejaFu.SCT as SCT
import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.Options (OptionDescription(..), IsOption(..), lookupOption)
import Test.Tasty.Providers (IsTest(..), singleTest, testPassed, testFailed)
#if MIN_VERSION_dejafu(0,4,0)
import qualified Test.DejaFu.Conc as Conc
#else
import qualified Test.DejaFu.Deterministic as Conc
#endif
import Unsafe.Coerce (unsafeCoerce)
#if MIN_VERSION_dejafu(0,3,0)
type Trc = Conc.Trace Conc.ThreadId Conc.ThreadAction Conc.Lookahead
#else
type Trc = Conc.Trace
#endif
sctBoundST :: MemType -> Bounds -> (forall t. Conc.ConcST t a) -> [(Either Failure a, Trc)]
sctBoundIO :: MemType -> Bounds -> Conc.ConcIO a -> IO [(Either Failure a, Trc)]
#if MIN_VERSION_dejafu(0,4,0)
sctBoundST memtype cb conc = runST (SCT.sctBound memtype cb conc)
sctBoundIO = SCT.sctBound
#else
sctBoundST = SCT.sctBound
sctBoundIO = SCT.sctBoundIO
#endif
instance Typeable t => IsTest (Conc.ConcST t (Maybe String)) where
testOptions = Tagged concOptions
run options conc callback = do
let memtype = lookupOption options :: MemType
let bounds = lookupOption options :: Bounds
let sctBound' :: Conc.ConcST t (Maybe String) -> [(Either Failure (Maybe String), Trc)]
sctBound' = unsafeCoerce $ sctBoundST memtype bounds
let traces = sctBound' conc
run options (ConcTest traces assertableP) callback
instance IsTest (Conc.ConcIO (Maybe String)) where
testOptions = Tagged concOptions
run options conc callback = do
let memtype = lookupOption options
let bounds = lookupOption options
let traces = sctBoundIO memtype bounds conc
run options (ConcIOTest traces assertableP) callback
concOptions :: [OptionDescription]
concOptions =
[ Option (Proxy :: Proxy Bounds)
, Option (Proxy :: Proxy MemType)
]
assertableP :: Predicate (Maybe String)
assertableP = alwaysTrue $ \r -> case r of
Right (Just _) -> False
_ -> True
instance IsOption Bounds where
defaultValue = defaultBounds
parseValue = const Nothing
optionName = Tagged "schedule-bounds"
optionHelp = Tagged "The schedule bounds to use. This cannot be set on the command line."
instance IsOption MemType where
defaultValue = defaultMemType
parseValue str = shortName (map toUpper str) 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\"."
testAuto :: (Eq a, Show a)
=> (forall t. Conc.ConcST t a)
-> TestTree
testAuto = testAuto' defaultMemType
testAuto' :: (Eq a, Show a)
=> MemType
-> (forall t. Conc.ConcST t a)
-> TestTree
testAuto' memtype conc = testDejafus' memtype defaultBounds conc autocheckCases
testAutoIO :: (Eq a, Show a) => Conc.ConcIO a -> TestTree
testAutoIO = testAutoIO' defaultMemType
testAutoIO' :: (Eq a, Show a) => MemType -> Conc.ConcIO a -> TestTree
testAutoIO' memtype concio = testDejafusIO' memtype defaultBounds concio autocheckCases
autocheckCases :: Eq a => [(TestName, Predicate a)]
autocheckCases =
[("Never Deadlocks", representative deadlocksNever)
, ("No Exceptions", representative exceptionsNever)
, ("Consistent Result", alwaysSame)
]
testDejafu :: Show a
=> (forall t. Conc.ConcST t a)
-> TestName
-> Predicate a
-> TestTree
testDejafu = testDejafu' defaultMemType defaultBounds
testDejafu' :: Show a
=> MemType
-> Bounds
-> (forall t. Conc.ConcST t a)
-> TestName
-> Predicate a
-> TestTree
testDejafu' memtype cb conc name p = testDejafus' memtype cb conc [(name, p)]
testDejafus :: Show a
=> (forall t. Conc.ConcST t a)
-> [(TestName, Predicate a)]
-> TestTree
testDejafus = testDejafus' defaultMemType defaultBounds
testDejafus' :: Show a
=> MemType
-> Bounds
-> (forall t. Conc.ConcST t a)
-> [(TestName, Predicate a)]
-> TestTree
testDejafus' = testst
testDejafuIO :: Show a => Conc.ConcIO a -> TestName -> Predicate a -> TestTree
testDejafuIO = testDejafuIO' defaultMemType defaultBounds
testDejafuIO' :: Show a => MemType -> Bounds -> Conc.ConcIO a -> TestName -> Predicate a -> TestTree
testDejafuIO' memtype cb concio name p = testDejafusIO' memtype cb concio [(name, p)]
testDejafusIO :: Show a => Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
testDejafusIO = testDejafusIO' defaultMemType defaultBounds
testDejafusIO' :: Show a => MemType -> Bounds -> Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
testDejafusIO' = testio
data ConcTest where
ConcTest :: Show a => [(Either Failure a, Trc)] -> Predicate a -> ConcTest
deriving Typeable
data ConcIOTest where
ConcIOTest :: Show a => IO [(Either Failure a, Trc)] -> Predicate a -> ConcIOTest
deriving Typeable
instance IsTest ConcTest where
testOptions = return []
run _ (ConcTest traces p) _ =
let err = showErr $ p traces
in return $ if null err then testPassed "" else testFailed err
instance IsTest ConcIOTest where
testOptions = return []
run _ (ConcIOTest iotraces p) _ = do
traces <- iotraces
let err = showErr $ p traces
return $ if null err then testPassed "" else testFailed err
testst :: Show a => MemType -> Bounds -> (forall t. Conc.ConcST t a) -> [(TestName, Predicate a)] -> TestTree
testst memtype cb conc tests = case map toTest tests of
[t] -> t
ts -> testGroup "Deja Fu Tests" ts
where
toTest (name, p) = singleTest name $ ConcTest traces p
traces = sctBoundST memtype cb conc
testio :: Show a => MemType -> Bounds -> Conc.ConcIO a -> [(TestName, Predicate a)] -> TestTree
testio memtype cb concio tests = case map toTest tests of
[t] -> t
ts -> testGroup "Deja Fu Tests" ts
where
toTest (name, p) = singleTest name $ ConcIOTest traces p
traces = sctBoundIO memtype cb concio
showErr :: Show a => Result a -> String
showErr res
| _pass res = ""
| otherwise = "Failed after " ++ show (_casesChecked res) ++ " cases:\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 (n1)
indent :: String -> String
indent = intercalate "\n" . map ('\t':) . lines