MemoryReference.hs

{-# 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' 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