{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module MemoryReference
( prop_sequential
, prop_runSavedCommands
, prop_parallel
, prop_parallel'
, prop_nparallel
, prop_precondition
, prop_existsCommands
, Bug(..)
, prop_pairs_shrink_parallel_equivalence
, prop_pairs_shrinkAndValidate_equivalence
, prop_pairs_shrink_parallel
)
where
import Control.Concurrent
(threadDelay)
import Data.Functor.Classes
(Eq1)
import Data.IORef
(IORef, atomicModifyIORef', newIORef, readIORef,
writeIORef)
import GHC.Generics
(Generic, Generic1)
import Prelude
import System.Random
(randomIO, randomRIO)
import Test.QuickCheck
(Gen, Property, arbitrary, elements, frequency,
once, shrink, (===))
import Test.QuickCheck.Monadic
(monadicIO)
import Test.StateMachine
import Test.StateMachine.Parallel
(shrinkAndValidateNParallel,
shrinkAndValidateParallel, shrinkCommands',
shrinkNParallelCommands, shrinkParallelCommands)
import Test.StateMachine.Sequential
(ShouldShrink(..))
import Test.StateMachine.Types
(Commands(Commands), Reference(..), Symbolic(..),
Var(Var))
import qualified Test.StateMachine.Types as Types
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.StateMachine.Utils
(Shrunk(..), shrinkListS, shrinkListS'',
shrinkPairS, shrinkPairS')
import Test.StateMachine.Z
------------------------------------------------------------------------
data Command r
= Create
| Read (Reference (Opaque (IORef Int)) r)
| Write (Reference (Opaque (IORef Int)) r) Int
| Increment (Reference (Opaque (IORef Int)) r)
deriving stock (Eq, Generic1)
deriving anyclass (Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
deriving stock instance Show (Command Symbolic)
deriving stock instance Read (Command Symbolic)
deriving stock instance Show (Command Concrete)
data Response r
= Created (Reference (Opaque (IORef Int)) r)
| ReadValue Int
| Written
| Incremented
deriving stock (Eq, Generic1)
deriving anyclass Rank2.Foldable
deriving stock instance Show (Response Symbolic)
deriving stock instance Read (Response Symbolic)
deriving stock instance Show (Response Concrete)
newtype Model r = Model [(Reference (Opaque (IORef Int)) r, Int)]
deriving stock (Generic, Show)
instance ToExpr (Model Symbolic)
instance ToExpr (Model Concrete)
initModel :: Model r
initModel = Model empty
transition :: Eq1 r => Model r -> Command r -> Response r -> Model r
transition m@(Model model) cmd resp = case (cmd, resp) of
(Create, Created ref) -> Model ((ref, 0) : model)
(Read _, ReadValue _) -> m
(Write ref x, Written) -> Model (update ref x model)
(Increment ref, Incremented) -> case lookup ref model of
Just i -> Model (update ref (succ i) model)
Nothing -> error "transition: increment"
_ -> error "transition: impossible."
update :: Eq a => a -> b -> [(a, b)] -> [(a, b)]
update ref i m = (ref, i) : filter ((/= ref) . fst) m
precondition :: Model Symbolic -> Command Symbolic -> Logic
precondition (Model m) cmd = case cmd of
Create -> Top
Read ref -> ref `member` domain m
Write ref _ -> ref `member` domain m
Increment ref -> ref `member` domain m
postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postcondition (Model m) cmd resp = case (cmd, resp) of
(Create, Created ref) -> m' ! ref .== 0 .// "Create"
where
Model m' = transition (Model m) cmd resp
(Read ref, ReadValue v) -> v .== m ! ref .// "Read"
(Write _ref _x, Written) -> Top
(Increment _ref, Incremented) -> Top
_ -> Bot
data Bug
= None
| Logic
| Race
| Crash
| CrashAndLogic
deriving stock Eq
semantics :: Bug -> Command Concrete -> IO (Response Concrete)
semantics bug cmd = case cmd of
Create -> Created <$> (reference . Opaque <$> newIORef 0)
Read ref -> ReadValue <$> readIORef (opaque ref)
Write ref i ->
case bug of
-- One of the problems is a bug that writes a wrong value to the
-- reference.
Logic | i `elem` [5..10] -> Written <$ writeIORef (opaque ref) (i + 1)
-- There's also the possibility that the program gets killed or crashes.
Crash -> do
bool <- randomIO
if bool
then
error "Crash before writing!"
-- Written <$ writeIORef (opaque ref) i
else do
writeIORef (opaque ref) i
error "Crash after writing!"
CrashAndLogic -> do
writeIORef (opaque ref) (i + 1)
error "Crash after writing!"
_otherwise -> Written <$ writeIORef (opaque ref) i
Increment ref -> do
-- Another problem is that we introduce a possible race condition
-- when incrementing.
if bug == Race
then do
i <- readIORef (opaque ref)
threadDelay =<< randomRIO (0, 5000)
writeIORef (opaque ref) (i + 1)
else
atomicModifyIORef' (opaque ref) (\i -> (i + 1, ()))
return Incremented
mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
mock (Model m) cmd = case cmd of
Create -> Created <$> genSym
Read ref -> ReadValue <$> pure (m ! ref)
Write _ _ -> pure Written
Increment _ -> pure Incremented
generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
generator m@(Model []) = Just (genCreate m)
generator m = Just $ frequency
[ (1, genCreate m)
, (4, genWrite m)
, (4, genRead m)
, (4, genIncr m)
]
genCreate, genRead, genWrite, genIncr :: Model Symbolic -> Gen (Command Symbolic)
genCreate _model = return Create
genRead (Model model) = Read <$> elements (domain model)
genWrite (Model model) = Write <$> elements (domain model) <*> arbitrary
genIncr (Model model) = Increment <$> elements (domain model)
shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
shrinker _ (Write ref i) = [ Write ref i' | i' <- shrink i ]
shrinker _ _ = []
sm :: Bug -> StateMachine Model Command IO Response
sm bug = StateMachine initModel transition precondition postcondition
Nothing generator shrinker (semantics bug) mock noCleanup
prop_sequential :: Bug -> Property
prop_sequential bug = forAllCommands sm' Nothing $ \cmds -> monadicIO $ do
(hist, _model, res) <- runCommands sm' cmds
prettyCommands sm' hist (saveCommands "/tmp" cmds
(coverCommandNames cmds $ checkCommandNames cmds (res === Ok)))
where
sm' = sm bug
prop_runSavedCommands :: Bug -> FilePath -> Property
prop_runSavedCommands bug fp = monadicIO $ do
(_cmds, hist, _model, res) <- runSavedCommands (sm bug) fp
prettyCommands (sm bug) hist (res === Ok)
prop_parallel :: Bug -> Property
prop_parallel bug = forAllParallelCommands sm' Nothing $
\cmds -> checkCommandNamesParallel cmds $ monadicIO $
prettyParallelCommands cmds =<< runParallelCommands sm' cmds
where
sm' = sm bug
prop_parallel' :: Bug -> Property
prop_parallel' bug = forAllParallelCommands sm' Nothing $ \cmds -> monadicIO $ do
prettyParallelCommands cmds =<< runParallelCommands' (pure sm') complete cmds
where
sm' = sm bug
complete :: Command Concrete -> Response Concrete
complete Create = Created (error "This reference will never be used.")
complete Read {} = ReadValue 0 -- Doesn't matter what value we read.
complete Write {} = Written
complete Increment {} = Incremented
prop_nparallel :: Bug -> Int -> Property
prop_nparallel bug np = forAllNParallelCommands sm' np $ \cmds ->
checkCommandNamesParallel cmds $ coverCommandNamesParallel cmds $ monadicIO $ do
prettyNParallelCommands cmds =<< runNParallelCommands sm' cmds
where
sm' = sm bug
prop_precondition :: Property
prop_precondition = once $ monadicIO $ do
(hist, _model, res) <- runCommands sm' cmds
prettyCommands sm' hist
(res === PreconditionFailed "PredicateC (NotMember (Reference (Symbolic (Var 0))) [])")
where
sm' = sm None
cmds = Commands
[ Types.Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) [] ]
prop_existsCommands :: Property
prop_existsCommands = existsCommands sm' gens $ \cmds -> monadicIO $ do
(hist, _model, res) <- runCommands sm' cmds
prettyCommands sm' hist (checkCommandNames cmds (res === Ok))
where
sm' = sm None
gens =
[ genCreate
, genWrite
, genIncr
, genRead
]
{-------------------------------------------------------------------------------
Meta properties which test the testing framework.
-------------------------------------------------------------------------------}
prop_pairs_shrink_parallel_equivalence :: Property
prop_pairs_shrink_parallel_equivalence =
forAllParallelCommands (sm None) Nothing $ \pairCmds ->
let pairShrunk = shrinkParallelCommands (sm None) pairCmds
listCmds = Types.fromPair' pairCmds
listShrunk = shrinkNParallelCommands (sm None) listCmds
listShrunkPair = Types.toPairUnsafe' <$> listShrunk
in listShrunkPair === pairShrunk
prop_pairs_shrinkAndValidate_equivalence :: Property
prop_pairs_shrinkAndValidate_equivalence =
forAllParallelCommands (sm None) Nothing $ \pairCmds ->
let pairShrunk' = shrinkAndValidateParallel (sm None) DontShrink pairCmds
listCmds = Types.fromPair' pairCmds
listShrunk' = shrinkAndValidateNParallel (sm None) DontShrink listCmds
listShrunkPair' = Types.toPairUnsafe' <$> listShrunk'
in listShrunkPair' === pairShrunk'
prop_pairs_shrink_parallel :: Property
prop_pairs_shrink_parallel =
forAllParallelCommands (sm None) Nothing $ \cmds@(Types.ParallelCommands prefix suffixes) ->
let pair =
[ Shrunk s (Types.ParallelCommands prefix' (map Types.toPair suffixes'))
| Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' (shrinkListS (shrinkPairS' shrinkCommands'))
(prefix, map Types.fromPair suffixes)]
(Types.ParallelCommands _ listSuffixes) = Types.fromPair' cmds
list =
[ Shrunk s $ Types.toPairUnsafe' (Types.ParallelCommands prefix' suffixes')
| Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' (shrinkListS (shrinkListS'' shrinkCommands'))
(prefix, listSuffixes)]
in list == pair