{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Cleanup (
Bug (..)
, DoubleCleanup (..)
, FinalTest (..)
, prop_sequential_clean
, prop_parallel_clean
, prop_nparallel_clean
) where
import Control.Concurrent.MVar
import Control.Exception
import Control.Monad
import Control.Monad.IO.Class
import Data.Functor.Classes
(Ord1, Show1)
import Data.List
((\\))
import Data.Map.Strict
(Map)
import qualified Data.Map.Strict as Map
import GHC.Generics
(Generic, Generic1)
import Prelude
import System.Directory
import System.IO
import System.Random
import Test.QuickCheck
import Test.QuickCheck.Monadic
(monadicIO)
import Test.StateMachine
import qualified Test.StateMachine.Types as QSM (initModel)
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.StateMachine.Utils
(liftProperty, mkModel, whenFailM)
import Text.Show.Pretty
(ppShow)
{-----------------------------------------------------------------------------------
This example in mainly used to check how well cleanup of resources works. In our
case resources are files created on the @testDirectory@ (not open handles, just
files). So it is easy, by the end of the tests to test if there any any resources
which are not cleaned up, by the end of the tests.
We also test different scenarios, like injected exceptions in semantics
(before and after the resource is created). Tests also reveal what happens when
cleaning up a resource for the second time is not a no-op.
-----------------------------------------------------------------------------------}
data Command r
= Create String
| Delete (Reference (Opaque FileRef) r)
| Ls
| Write Int
| Increment
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 FileRef) r)
| Deleted
| Contents [String]
| ChangedValue Int
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)
data Model r = Model {
files :: Map (Reference (Opaque FileRef) r) String
, counter :: Int
, semanticsCounter :: Opaque (MVar Int)
, ref :: Opaque (MVar Int)
, value :: Int
, modelTestDir :: String
}
deriving stock (Generic, Show, Eq)
instance ToExpr (Model Symbolic)
instance ToExpr (Model Concrete)
initModel :: MVar Int -> MVar Int -> String -> Model r
initModel sc ref = Model Map.empty 0 (Opaque sc) (Opaque ref) 0
transition :: Ord1 r => Model r -> Command r -> Response r -> Model r
transition m@Model {..} cmd resp = case (cmd, resp) of
(Create p, Created rf) -> m {files = Map.insert rf p files, counter = counter + 1}
(Delete rf, Deleted) -> m {files = Map.delete rf files}
(Ls, Contents _) -> m
(Write n, ChangedValue _) -> m {value = n}
(Increment, ChangedValue _) -> m {value = value + 1}
_ -> error "transition impossible"
precondition :: Model Symbolic -> Command Symbolic -> Logic
precondition Model {..} cmd = case cmd of
Create p -> Boolean $ notElem p (Map.elems files)
Delete rf -> Boolean $ Map.member rf files
Ls -> Top
Write _ -> Top
Increment -> Top
sameElements :: Eq a => [a] -> [a] -> Bool
sameElements x y = null (x \\ y) && null (y \\ x)
postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postcondition Model{..} cmd resp = case (cmd, resp) of
(Create _, Created _) -> Top
(Delete _, Deleted) -> Top
(Ls, Contents ls) -> if sameElements ls (Map.elems files) then Top
else Annotate ("Not same elements between " ++ show ls ++ "and " ++ show (Map.elems files)) Bot
(Increment, ChangedValue _) -> Top
(Write n, ChangedValue m) -> m .== n
_ -> Bot
data MVarC a = MVarC (MVar a) Int
type FileRef = MVarC (String, Bool)
removeFileRef :: DoubleCleanup -> FileRef -> IO ()
removeFileRef dc (MVarC r _) = modifyMVar_ r $ \(file, isHere) -> do
case (isHere, dc) of
(_, ReDo) -> removeFile file
(True, _) -> removeFile file
(False, NoOp) -> return ()
return (file, False)
instance Eq (MVarC a) where
MVarC _ a == MVarC _ b = a == b
instance Ord (MVarC a) where
compare (MVarC _ a) (MVarC _ b) = compare a b
semantics :: MVar Int -> MVar Int -> String -> Bug -> Command Concrete -> IO (Response Concrete)
semantics counter ref tstDir bug cmd = case cmd of
Create f -> createFile f
`onException` removePathForcibly (makePath tstDir f)
Delete rf -> do
let MVarC lockedFile _ = unOpaque $ concrete rf
modifyMVar_ lockedFile $ \(file, _) -> do
removeFile file
return (file, False)
return Deleted
Ls -> do
ls <- listDirectory tstDir
return $ Contents ls
Write n ->
modifyMVar ref (\_ -> return (n, ChangedValue n))
Increment ->
modifyMVar ref (\m -> return (m + 1, ChangedValue $ m + 1))
where
createFile :: String -> IO (Response Concrete)
createFile f = do
let path = makePath tstDir f
c <- modifyMVar counter $ \n -> return (n + 1, n)
when (c > 3 && bug == Exception) $
throwIO $ userError "semantics injected bug"
withFile path WriteMode (\_ -> return ())
when (c > 3 && bug == ExcAfter) $
throwIO $ userError "semantics injected bug"
rf <- newMVar (path, True)
return $ Created $ reference $ Opaque $ MVarC rf c
mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
mock Model{..} cmd = case cmd of
Create _ -> Created <$> genSym
Delete _ -> return Deleted
Ls -> return $ Contents $ Map.elems files
Write n -> return $ ChangedValue n
Increment -> return $ ChangedValue $ value + 1
generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
generator Model{..} = Just $ do
n <- choose (1,10)
frequency
[ (7, return $ Create $ mkFileName counter)
, (if Map.null files then 0 else 3, Delete . fst <$> elements (Map.toList files))
, (1, return Ls)
, (1, return $ Write n)
, (1, return Increment)
]
shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
shrinker _ _ = []
cleanup :: DoubleCleanup -> Model Concrete -> IO ()
cleanup dc Model{..} = do
let cl = do
forM_ (Map.keys files) $ \rf ->
removeFileRef dc $ unOpaque $ concrete rf
modifyMVar_ (unOpaque semanticsCounter) (\_ -> return 0)
modifyMVar_ (unOpaque ref) (\_ -> return 0)
cl `finally` removePathForcibly modelTestDir
sm :: MVar Int -> MVar Int -> Bug -> DoubleCleanup -> IO (StateMachine Model Command IO Response)
sm counter ref bug dc = do
folderId :: Word <- randomIO
let testDir = testDirectoryBase ++ "-" ++ show folderId
exist <- doesDirectoryExist testDir
when exist $ removePathForcibly testDir
createDirectory testDir
pure $ StateMachine (initModel counter ref testDir) transition precondition postcondition
Nothing generator shrinker (semantics counter ref testDir bug) mock (cleanup dc)
smUnused :: StateMachine Model Command IO Response
smUnused = StateMachine (initModel f e "generator") transition precondition postcondition
Nothing generator shrinker (semantics e e e e) mock (cleanup e)
where
e = error "SUT must not be used"
f = error "SUT must not be useddd"
prop_sequential_clean :: FinalTest -> Bug -> DoubleCleanup -> Property
prop_sequential_clean testing bug dc = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do
counter <- liftIO $ newMVar 0
ref <- liftIO $ newMVar 0
let sm' = sm counter ref bug dc
(hist, model, res) <- runCommandsWithSetup sm' cmds
case testing of
Regular -> prettyCommands smUnused hist $ checkCommandNames cmds (res === Ok)
Files -> do
ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model)
(do
ls <- liftIO $ listDirectory $ modelTestDir model
printFiles ls) `whenFailM` ex
Eq _ -> liftProperty $ mkModel smUnused { QSM.initModel = initModel counter ref (modelTestDir model) } hist === model
prop_parallel_clean :: FinalTest -> Bug -> DoubleCleanup -> Property
prop_parallel_clean testing bug dc = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do
counter <- liftIO $ newMVar 0
ref <- liftIO $ newMVar 0
let sm' = sm counter ref bug dc
ret <- runParallelCommandsNTimesWithSetup 2 sm' cmds
case testing of
Regular -> prettyParallelCommands cmds ret
Files ->
mapM_ (\(_, model, _) -> do
ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model)
(do
ls <- liftIO $ listDirectory $ modelTestDir model
printFiles ls) `whenFailM` ex) ret
Eq bl -> do
let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> ret of
(x : y : _) -> (x,y)
_ -> error "expected at least two histories"
liftProperty $ printModels a b `whenFail`
property (modelEquivalence bl a b)
prop_nparallel_clean :: Int -> FinalTest -> Bug -> DoubleCleanup -> Property
prop_nparallel_clean np testing bug dc = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do
counter <- liftIO $ newMVar 0
ref <- liftIO $ newMVar 0
let sm' = sm counter ref bug dc
ret <- runNParallelCommandsNTimesWithSetup 2 sm' cmds -- This 2 is there just to have two histories later on!
case testing of
Regular -> prettyNParallelCommands cmds ret
Files ->
mapM_ (\(_, model, _) -> do
ex <- property . not <$> (liftIO $ doesDirectoryExist $ modelTestDir model)
(do
ls <- liftIO $ listDirectory $ modelTestDir model
printFiles ls) `whenFailM` ex) ret
Eq bl -> do
let (a, b) = case mkModel smUnused . (\(h, _, _) -> h) <$> ret of
(x : y : _) -> (x,y)
_ -> error "expected at least two histories"
liftProperty $ printModels a b `whenFail`
property (modelEquivalence bl a b)
printModels :: Show1 r => Model r -> Model r -> IO ()
printModels a b = do
putStrLn $ "Models are not equivalent: \n" ++ ppShow a ++ " \nand \n" ++ ppShow b
printFiles :: [String] -> IO ()
printFiles ls' =
putStrLn $ "Cleanup was not complete. Found files " ++ show ls'
data Bug = NoBug
| Exception
| ExcAfter
deriving stock (Eq, Show)
data DoubleCleanup = NoOp
| ReDo
deriving stock (Eq, Show)
data FinalTest = Regular
| Files
| Eq Bool
deriving stock (Eq, Show)
-- | This is meant to be used, in order to test equality of two
-- Models, created by two different executions of the same program.
-- Note that we don't test reference equality. This is because
-- different executions in the parallel case, may create references
-- with different order, so the counter assigned by the semantics
-- can be different.
modelEquivalence :: Bool -> Model Concrete -> Model Concrete -> Bool
modelEquivalence bl a b =
sameElements (Map.elems $ files a) (Map.elems $ files b)
&& counter a == counter b
&& (not bl || value a == value b)
makePath :: String -> String -> String
makePath tstDir file = tstDir ++ "/" ++ file
mkFileName :: Int -> String
mkFileName n = "file" ++ show n
testDirectoryBase :: String
testDirectoryBase = "cleanup-test-folder"