fs-sim-0.5.0.0: test/Test/System/FS/StateMachine.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{- HLINT ignore "Use camelCase" -}
-- | Tests for our filesystem abstractions.
--
-- The blogpost [An in-depth look at __quickcheck-state-machine__](http://www.well-typed.com/blog/2019/01/qsm-in-depth/)
-- uses these tests of the file system abstraction as a case study and outlines the
-- general approach. Like all of the model based tests, this consists of
--
-- 1. A set of commands
-- 2. A model against which we execute those commands
-- 3. An interpreter of those commands against the real implementation
-- 4. A generator and a shrinker for sequences of these commands
-- 5. A way to /label/ generated sequences so that we can verify that the tests
-- are covering what we think they should be covering.
--
-- The sequences generated are then executed against both the model and the
-- implementation, and the results are compared.
--
-- In this particular case, the commands are file system operations such as
-- create a directory, open a file, write some bytes, etc. The model is a very
-- simple one: we simply model a file system as a tree of 'ByteString's (the raw
-- bytes in the files). The goal of the model, of course, is not to provide one
-- that mirrors the low-level details of the real implementation, but rather one
-- that abstracts over such details and provides a /specification/.
--
-- The file system abstraction however is a bit of an unusual test in that this
-- is really "reverse model testing": the tests compare the model to the real
-- file system, but we are of course not developing a file system. Instead, the
-- tests serve to make sure that we got the model right, which we can then use
-- in the tests of the rest of the consensus layer.
module Test.System.FS.StateMachine
( showLabelledExamples
, tests
) where
#if __GLASGOW_HASKELL__<910
import Data.Foldable (foldl')
#endif
import qualified Control.Exception as E
import Control.Monad
import Control.Monad.Primitive
import Control.Monad.ST.Strict (runST)
import Data.Bifoldable
import Data.Bifunctor
import qualified Data.Bifunctor.TH as TH
import Data.Bitraversable
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import Data.Functor.Classes
import Data.Int (Int64)
import qualified Data.List as L
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromJust)
import Data.Primitive (MutableByteArray, newPinnedByteArray)
import Data.Proxy
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as Text
import Data.Word (Word64)
import GHC.Generics
import GHC.Stack hiding (prettyCallStack)
import qualified Generics.SOP as SOP
import System.FS.API
import System.FS.CallStack
import System.FS.Condense
import System.FS.IO
import System.FS.Sim.FsTree (FsTree (..))
import System.FS.Sim.MockFS (HandleMock, MockFS)
import qualified System.FS.Sim.MockFS as Mock
import System.FS.Sim.Prim
import System.IO.Temp (withSystemTempDirectory)
import System.Posix.Types (ByteCount)
import System.Random (getStdRandom, randomR)
import Test.QuickCheck
import qualified Test.QuickCheck.Monadic as QC
import Test.QuickCheck.Random (mkQCGen)
import Test.StateMachine (Concrete, Symbolic)
import qualified Test.StateMachine as QSM
import qualified Test.StateMachine.Labelling as C
import qualified Test.StateMachine.Sequential as QSM
import Test.StateMachine.TreeDiff
import qualified Test.StateMachine.Types as QSM
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.Tasty (TestTree, localOption, testGroup)
import Test.Tasty.QuickCheck
import Test.Util.RefEnv (RefEnv)
import qualified Test.Util.RefEnv as RE
import Text.Read (readMaybe)
import Text.Show.Pretty (ppShow)
{-------------------------------------------------------------------------------
Path expressions
-------------------------------------------------------------------------------}
data PathExpr fp
= PExpPath FsPath
| PExpRef fp
| PExpParentOf fp
deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)
evalPathExpr :: PathExpr FsPath -> FsPath
evalPathExpr (PExpPath fp) = fp
evalPathExpr (PExpRef fp) = fp
evalPathExpr (PExpParentOf fp) = fsPathInit fp
{-------------------------------------------------------------------------------
Abstract model
-------------------------------------------------------------------------------}
-- | Commands
--
-- We will be interested in three different instantiations of @h@:
--
-- > Cmd HandleMock
-- > Cmd (Reference (Opaque (FsHandle IOFSE)) Concrete)
-- > Cmd (Reference (Opaque (FsHandle IOFSE)) Symbolic)
--
-- Key idea is that all this infrastructure will be applicable both to
-- the model and to the system under test.
--
-- TODO: Program such as "copy what you read" is currently not expressible
-- in our language. Does this matter?
data Cmd fp h
= Open (PathExpr fp) OpenMode
| Close h
| IsOpen h
| Seek h SeekMode Int64
| Get h Word64
| GetAt h Word64 AbsOffset
| GetBuf h ByteCount
| GetBufAt h ByteCount AbsOffset
| Put h ByteString
| PutBuf h ByteString ByteCount
| PutBufAt h ByteString ByteCount AbsOffset
| Truncate h Word64
| GetSize h
| CreateDir (PathExpr fp)
| CreateDirIfMissing Bool (PathExpr fp)
| ListDirectory (PathExpr fp)
| DoesDirectoryExist (PathExpr fp)
| DoesFileExist (PathExpr fp)
| RemoveDirRecursive (PathExpr fp)
| RemoveFile (PathExpr fp)
| RenameFile (PathExpr fp) (PathExpr fp)
deriving (Generic, Show, Functor, Foldable, Traversable)
deriving instance SOP.Generic (Cmd fp h)
deriving instance SOP.HasDatatypeInfo (Cmd fp h)
-- | Successful result
data Success fp h
= WHandle fp h
| RHandle h
| Unit ()
| Path fp ()
| Word64 Word64
| ByteString ByteString
| ByteCount ByteCount -- PutBuf, PutBufAt
| BCBS ByteCount ByteString -- GetBuf, GetBufAt
| Strings (Set String)
| Bool Bool
deriving (Eq, Show, Functor, Foldable)
-- | Successful semantics
run ::
forall m h.
(PrimMonad m, HasCallStack) =>
HasFS m h ->
Cmd FsPath (Handle h) ->
m (Success FsPath (Handle h))
run hasFS@HasFS{..} = go
where
go :: Cmd FsPath (Handle h) -> m (Success FsPath (Handle h))
go (Open pe mode) =
case mode of
ReadMode -> withPE pe (\_ -> RHandle) $ \fp -> hOpen fp mode
_otherwise -> withPE pe WHandle $ \fp -> hOpen fp mode
go (CreateDir pe) = withPE pe Path $ createDirectory
go (CreateDirIfMissing b pe) = withPE pe Path $ createDirectoryIfMissing b
go (IsOpen h) = Bool <$> hIsOpen h
go (Close h) = Unit <$> hClose h
go (Seek h mode sz) = Unit <$> hSeek h mode sz
-- Note: we're not using 'hGetSome', 'hGetSomeAt' and 'hPutSome' that may
-- produce partial reads/writes, but wrappers around them that handle
-- partial reads/writes, see #502.
go (Get h n) = ByteString <$> hGetSomeChecked hasFS h n
go (GetAt h n o) = ByteString <$> hGetSomeAtChecked hasFS h n o
go (GetBuf h n) = uncurry BCBS <$> hGetBufSomeChecked hasFS h n
go (GetBufAt h n o) = uncurry BCBS <$> hGetBufSomeAtChecked hasFS h n o
go (Put h bs) = Word64 <$> hPutSomeChecked hasFS h bs
go (PutBuf h bs n) = ByteCount <$> hPutBufSomeChecked hasFS h bs n
go (PutBufAt h bs n o) = ByteCount <$> hPutBufSomeAtChecked hasFS h bs n o
go (Truncate h sz) = Unit <$> hTruncate h sz
go (GetSize h) = Word64 <$> hGetSize h
go (ListDirectory pe) = withPE pe (const Strings) $ listDirectory
go (DoesDirectoryExist pe) = withPE pe (const Bool) $ doesDirectoryExist
go (DoesFileExist pe) = withPE pe (const Bool) $ doesFileExist
go (RemoveDirRecursive pe) = withPE pe (const Unit) $ removeDirectoryRecursive
go (RemoveFile pe) = withPE pe (const Unit) $ removeFile
go (RenameFile pe1 pe2) = withPEs pe1 pe2 (\_ _ -> Unit) $ renameFile
withPE ::
PathExpr FsPath ->
(FsPath -> a -> Success FsPath (Handle h)) ->
(FsPath -> m a) ->
m (Success FsPath (Handle h))
withPE pe r f = let fp = evalPathExpr pe in r fp <$> f fp
withPEs ::
PathExpr FsPath ->
PathExpr FsPath ->
(FsPath -> FsPath -> a -> Success FsPath (Handle h)) ->
(FsPath -> FsPath -> m a) ->
m (Success FsPath (Handle h))
withPEs pe1 pe2 r f =
let fp1 = evalPathExpr pe1
fp2 = evalPathExpr pe2
in r fp1 fp2 <$> f fp1 fp2
{-------------------------------------------------------------------------------
Detecting partial reads/writes of the tested IO implementation
-------------------------------------------------------------------------------}
{- Note [Checking for partial reads/writes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The functions 'hGetSome', 'hGetSomeAt' and 'hPutSome' might perform partial
reads/writes, depending on the underlying implementation, see
[ouroboros-network#277](https://github.com/IntersectMBO/ouroboros-network/issues/277).
While the model will always perform complete reads/writes, the real IO
implementation we are testing /might/ actually perform partial reads/writes.
This testsuite will fail when such a partial read or write is performed in the
real IO implementation, as these are undeterministic and the model will no
longer correspond to the real implementation. See
[ouroboros-network#502](https://github.com/IntersectMBO/ouroboros-network/issues/502)
were we tracked this issue.
So far, on all systems the tests have been run on, no partial reads/writes
have ever been noticed. However, we cannot be sure that the tests will never
be run on a system or file-system that might result in partial reads/writes.
Therefore, we use checked variants of 'hGetSome', 'hGetSomeAt' and 'hPutSome'
that detect partial reads/writes and that will signal an error so that the
developer noticing the failing test doesn't waste any time debugging the
implementation while the failing test was actually due to an unexpected
partial read/write.
For compound functions like 'hGetExactly' and 'hPutAll', this is not a good
solution. However, since we are only testing primitives, the solution is fine
for our purposes.
The problem with compound functions is that to run a single 'Cmd', we now have
to run multiple primitive 'HasFS' functions. Each of those primitive functions
might update the state of the model and the real world. Now when the second,
third, ..., or n-th primitive functions fails (while running a single 'Cmd'),
the whole 'Cmd' failed and the model is not updated. This means that we
continue with the model as it was /before/ running the 'Cmd'. However, these
primitive functions might have changed the model /and/ the state of the real
implementation. In that case, we can no longer guarantee that the model and
the real implementation are in sync.
-}
hGetSomeChecked ::
(Monad m, HasCallStack) =>
HasFS m h -> Handle h -> Word64 -> m ByteString
hGetSomeChecked HasFS{..} h n = do
bytes <- hGetSome h n
when (fromIntegral (BS.length bytes) /= n) $ do
moreBytes <- hGetSome h 1
-- If we can actually read more bytes, the last read was partial. If we
-- cannot, we really were at EOF.
unless (BS.null moreBytes) $
error "Unsupported partial read detected, see Note [Checking for partial reads/writes]"
return bytes
hGetSomeAtChecked ::
(Monad m, HasCallStack) =>
HasFS m h -> Handle h -> Word64 -> AbsOffset -> m ByteString
hGetSomeAtChecked HasFS{..} h n o = do
bytes <- hGetSomeAt h n o
when (fromIntegral (BS.length bytes) /= n) $ do
moreBytes <- hGetSomeAt h 1 $ o + fromIntegral (BS.length bytes)
-- If we can actually read more bytes, the last read was partial. If we
-- cannot, we really were at EOF.
unless (BS.null moreBytes) $
error "Unsupported partial read detected, see Note [Checking for partial reads/writes]"
return bytes
hPutSomeChecked ::
(Monad m, HasCallStack) =>
HasFS m h -> Handle h -> ByteString -> m Word64
hPutSomeChecked HasFS{..} h bytes = do
n <- hPutSome h bytes
if fromIntegral (BS.length bytes) /= n
then error "Unsupported partial write detected, see Note [Checking for partial reads/writes]"
else return n
hGetBufSomeChecked ::
(HasCallStack, PrimMonad m) =>
HasFS m h ->
Handle h ->
ByteCount ->
m (ByteCount, ByteString)
hGetBufSomeChecked HasFS{..} h n = do
allocaMutableByteArray (fromIntegral n) $ \buf -> do
n' <- hGetBufSome h buf 0 n
bs <- fromJust <$> Mock.fromBuffer buf 0 n'
when (n /= n') $ do
moreBytes <- hGetSome h 1
-- If we can actually read more bytes, the last read was partial. If we
-- cannot, we really were at EOF.
unless (BS.null moreBytes) $
error "Unsupported partial read detected, see #502"
pure (n', bs)
hGetBufSomeAtChecked ::
(HasCallStack, PrimMonad m) =>
HasFS m h ->
Handle h ->
ByteCount ->
AbsOffset ->
m (ByteCount, ByteString)
hGetBufSomeAtChecked HasFS{..} h n o = do
allocaMutableByteArray (fromIntegral n) $ \buf -> do
n' <- hGetBufSomeAt h buf 0 n o
bs <- fromJust <$> Mock.fromBuffer buf 0 n'
when (n /= n') $ do
moreBytes <- hGetSomeAt h 1 $ o + fromIntegral n'
-- If we can actually read more bytes, the last read was partial. If we
-- cannot, we really were at EOF.
unless (BS.null moreBytes) $
error "Unsupported partial read detected, see #502"
pure (n', bs)
hPutBufSomeChecked ::
(HasCallStack, PrimMonad m) =>
HasFS m h ->
Handle h ->
ByteString ->
ByteCount ->
m ByteCount
hPutBufSomeChecked HasFS{..} h bs n =
allocaMutableByteArray (min (fromIntegral n) (BS.length bs)) $ \buf -> do
void $ Mock.intoBuffer buf 0 (BS.take (fromIntegral n) bs)
n' <- hPutBufSome h buf 0 n
if n /= n'
then error "Unsupported partial write detected, see #502"
else return n
hPutBufSomeAtChecked ::
(HasCallStack, PrimMonad m) =>
HasFS m h ->
Handle h ->
ByteString ->
ByteCount ->
AbsOffset ->
m ByteCount
hPutBufSomeAtChecked HasFS{..} h bs n o =
allocaMutableByteArray (min (fromIntegral n) (BS.length bs)) $ \buf -> do
void $ Mock.intoBuffer buf 0 (BS.take (fromIntegral n) bs)
n' <- hPutBufSomeAt h buf 0 n o
if n /= n'
then error "Unsupported partial write detected, see #502"
else return n
allocaMutableByteArray :: PrimMonad m => Int -> (MutableByteArray (PrimState m) -> m a) -> m a
allocaMutableByteArray size action = newPinnedByteArray size >>= action
{-------------------------------------------------------------------------------
Instantiating the semantics
-------------------------------------------------------------------------------}
-- | For some error types, our mock FS implementation, which is based on
-- (Ubuntu) Linux might throw different errors than the actual file system. In
-- particular, this problem occurs when the file system under test is a Windows
-- or MacOS one. In these cases, the 'sameError' comparison function, which is
-- used to compare the 'FsError's that the mock throws against the 'FsError's
-- that the SUT throws, is more lenient than the default 'sameFsError'.
sameError :: FsError -> FsError -> Bool
#if defined(mingw32_HOST_OS)
-- For the following error types, our mock FS implementation (and the Posix
-- implementation) throw the same errors:
--
-- * 'FsReachedEOF'
-- * 'FsDeviceFull'
-- * 'FsResourceAlreadyInUse'
--
-- For other cases, Windows throws different errors than the mock FS
-- implementation.
sameError e1 e2 = fsErrorPath e1 == fsErrorPath e2
&& sameFsErrorType (fsErrorType e1) (fsErrorType e2)
where
sameFsErrorType ty1 ty2 = case (ty1, ty2) of
(FsReachedEOF, FsReachedEOF) -> True
(FsReachedEOF, _) -> False
(_, FsReachedEOF) -> False
(FsDeviceFull, FsDeviceFull) -> True
(FsDeviceFull, _) -> False
(_, FsDeviceFull) -> False
(FsResourceAlreadyInUse, FsResourceAlreadyInUse) -> True
(FsResourceAlreadyInUse, _) -> False
(_, FsResourceAlreadyInUse) -> False
(_, _) -> True
#elif defined(darwin_HOST_OS)
-- Check default implementation first using 'sameFsError', and otherwise permit
-- some combinations of error types that are not structurally equal.
sameError e1 e2 = sameFsError e1 e2
|| (fsErrorPath e1 == fsErrorPath e2
&& permitted (fsErrorType e1) (fsErrorType e2))
where
-- error types that are permitted to differ for technical reasons
permitted ty1 ty2 = case (ty1, ty2) of
(FsInsufficientPermissions , FsResourceInappropriateType) -> True
(FsResourceInappropriateType, FsInsufficientPermissions ) -> True
(_ , _ ) -> False
#else
-- treat every other distribution like it is (Ubuntu) Linux
sameError = sameFsError
#endif
-- | Responses are either successful termination or an error
newtype Resp fp h = Resp {getResp :: Either FsError (Success fp h)}
deriving (Show, Functor, Foldable)
-- | The 'Eq' instance for 'Resp' uses 'sameError'
instance (Eq fp, Eq h) => Eq (Resp fp h) where
Resp (Left e) == Resp (Left e') = sameError e e'
Resp (Right a) == Resp (Right a') = a == a'
_ == _ = False
runPure ::
Cmd FsPath (Handle HandleMock) ->
MockFS ->
(Resp FsPath (Handle HandleMock), MockFS)
runPure cmd mockFS =
aux $ runST $ runFSSimT (run primHasMockFS cmd) mockFS
where
aux ::
Either FsError (Success FsPath (Handle HandleMock), MockFS) ->
(Resp FsPath (Handle HandleMock), MockFS)
aux (Left e) = (Resp (Left e), mockFS)
aux (Right (r, mockFS')) = (Resp (Right r), mockFS')
runIO ::
HasFS IO HandleIO ->
Cmd FsPath (Handle HandleIO) ->
IO (Resp FsPath (Handle HandleIO))
runIO hfs cmd = Resp <$> E.try (run hfs cmd)
{-------------------------------------------------------------------------------
Bitraversable instances
-------------------------------------------------------------------------------}
TH.deriveBifunctor ''Cmd
TH.deriveBifoldable ''Cmd
TH.deriveBitraversable ''Cmd
TH.deriveBifunctor ''Success
TH.deriveBifoldable ''Success
TH.deriveBitraversable ''Success
TH.deriveBifunctor ''Resp
TH.deriveBifoldable ''Resp
TH.deriveBitraversable ''Resp
{-------------------------------------------------------------------------------
Collect arguments
-------------------------------------------------------------------------------}
paths :: Bitraversable t => t fp h -> [fp]
paths = bifoldMap (: []) (const [])
handles :: Bitraversable t => t fp h -> [h]
handles = bifoldMap (const []) (: [])
{-------------------------------------------------------------------------------
Model
-------------------------------------------------------------------------------}
-- | Concrete or symbolic reference to a path
type PathRef = QSM.Reference FsPath
-- | Concrete or symbolic reference to an IO file handle
type HandleRef = QSM.Reference (Handle HandleIO)
-- | Mapping between real IO file handles and mock file handles
type KnownHandles = RefEnv (Handle HandleIO) (Handle HandleMock)
-- | Mapping between path references and paths
type KnownPaths = RefEnv FsPath FsPath
resolvePathExpr :: Eq1 r => KnownPaths r -> PathExpr (PathRef r) -> FsPath
resolvePathExpr knownPaths = evalPathExpr . fmap (knownPaths RE.!)
-- | Execution model
data Model r = Model
{ mockFS :: MockFS
, knownPaths :: KnownPaths r
, knownHandles :: KnownHandles r
}
deriving (Show, Generic)
-- | Initial model
initModel :: Model r
initModel = Model Mock.empty RE.empty RE.empty
-- | Key property of the model is that we can go from real to mock responses
toMock ::
(Bifunctor t, Eq1 r) =>
Model r -> t :@ r -> t FsPath (Handle HandleMock)
toMock Model{..} (At r) = bimap (knownPaths RE.!) (knownHandles RE.!) r
-- | Step the mock semantics
--
-- We cannot step the whole Model here (see 'Event', below)
step ::
Eq1 r =>
Model r -> Cmd :@ r -> (Resp FsPath (Handle HandleMock), MockFS)
step model@Model{..} cmd = runPure (toMock model cmd) mockFS
-- | Open read handles
openHandles :: Model r -> [Handle HandleMock]
openHandles Model{..} =
filter isOpen (RE.elems knownHandles)
where
isOpen :: Handle HandleMock -> Bool
isOpen (Handle h _) = Mock.handleIsOpen mockFS h
{-------------------------------------------------------------------------------
Wrapping in quickcheck-state-machine references
-------------------------------------------------------------------------------}
-- | Instantiate functor @f@ to @f (PathRef r) (HandleRef r)@
--
-- > Cmd :@ Concrete ~ Cmd (PathRef Concrete) (HandleRef Concrete)
newtype At t r = At {unAt :: (t (PathRef r) (HandleRef r))}
deriving Generic
-- | Alias for 'At'
type (:@) t r = At t r
deriving instance Show1 r => Show (Cmd :@ r)
deriving instance Show1 r => Show (Resp :@ r)
deriving instance Eq1 r => Eq (Resp :@ r)
instance Bifoldable t => Rank2.Foldable (At t) where
foldMap = \f (At x) -> bifoldMap (app f) (app f) x
where
app :: (r x -> m) -> QSM.Reference x r -> m
app f (QSM.Reference x) = f x
instance Bifunctor t => Rank2.Functor (At t) where
fmap = \f (At x) -> At (bimap (app f) (app f) x)
where
app :: (r x -> r' x) -> QSM.Reference x r -> QSM.Reference x r'
app f (QSM.Reference x) = QSM.Reference (f x)
instance Bitraversable t => Rank2.Traversable (At t) where
traverse = \f (At x) -> At <$> bitraverse (app f) (app f) x
where
app ::
Functor f =>
(r x -> f (r' x)) -> QSM.Reference x r -> f (QSM.Reference x r')
app f (QSM.Reference x) = QSM.Reference <$> f x
{-------------------------------------------------------------------------------
Events
-------------------------------------------------------------------------------}
-- | An event records the model before and after a command along with the
-- command itself and its response
data Event r = Event
{ eventBefore :: Model r
, eventCmd :: Cmd :@ r
, eventAfter :: Model r
, eventMockResp :: Resp FsPath (Handle HandleMock)
}
deriving Show
eventMockCmd :: Eq1 r => Event r -> Cmd FsPath (Handle HandleMock)
eventMockCmd Event{..} = toMock eventBefore eventCmd
-- | Construct an event
--
-- When we execute both the model and the real implementation in lockstep,
-- we get two responses: this suffices to update the model.
lockstep ::
forall r.
(Show1 r, Ord1 r, HasCallStack) =>
Model r ->
Cmd :@ r ->
Resp :@ r ->
Event r
lockstep model@Model{..} cmd (At resp) =
Event
{ eventBefore = model
, eventCmd = cmd
, eventAfter =
Model
{ mockFS = mockFS'
, knownPaths = knownPaths `RE.union` newPaths
, knownHandles = knownHandles `RE.union` newHandles
}
, eventMockResp = resp'
}
where
(resp', mockFS') = step model cmd
newPaths = RE.fromList $ zip (paths resp) (paths resp')
newHandles = RE.fromList $ zip (handles resp) (handles resp')
{-------------------------------------------------------------------------------
Generator
-------------------------------------------------------------------------------}
generator :: Model Symbolic -> Gen (Cmd :@ Symbolic)
generator Model{..} =
oneof $
concat
[ withoutHandle
, if RE.null knownHandles then [] else withHandle
]
where
withoutHandle :: [Gen (Cmd :@ Symbolic)]
withoutHandle =
[ fmap At $ genOpen
, fmap At $ CreateDir <$> genPathExpr
, fmap At $ CreateDirIfMissing <$> arbitrary <*> genPathExpr
, fmap At $ ListDirectory <$> genPathExpr
, fmap At $ DoesDirectoryExist <$> genPathExpr
, fmap At $ DoesFileExist <$> genPathExpr
, fmap At $ RemoveDirRecursive <$> genPathExpr
, fmap At $ RemoveFile <$> genPathExpr
, fmap At $ RenameFile <$> genPathExpr <*> genPathExpr
]
withHandle :: [Gen (Cmd :@ Symbolic)]
withHandle =
[ fmap At $ Close <$> genHandle
, fmap At $ IsOpen <$> genHandle
, fmap At $ Seek <$> genHandle <*> genSeekMode <*> genOffset
, fmap At $ Get <$> genHandle <*> (getSmall <$> arbitrary)
, fmap At $ GetAt <$> genHandle <*> (getSmall <$> arbitrary) <*> arbitrary
, fmap At $ GetBuf <$> genHandle <*> (getSmall <$> arbitrary)
, fmap At $ GetBufAt <$> genHandle <*> (getSmall <$> arbitrary) <*> arbitrary
, fmap At $ Put <$> genHandle <*> (BS.pack <$> arbitrary)
, fmap At $ PutBuf <$> genHandle <*> (BS.pack <$> arbitrary) <*> (getSmall <$> arbitrary)
, fmap At $
PutBufAt <$> genHandle <*> (BS.pack <$> arbitrary) <*> (getSmall <$> arbitrary) <*> arbitrary
, fmap At $ Truncate <$> genHandle <*> (getSmall . getNonNegative <$> arbitrary)
, fmap At $ GetSize <$> genHandle
]
genOpen :: Gen (Cmd (PathRef Symbolic) (HandleRef Symbolic))
genOpen = do
path <- genPath
mode <- genMode $ elem path (RE.elems knownPaths)
return $ Open (PExpPath path) mode
-- Wrap path in a simple path expression
-- (References are generated during shrinking only)
genPathExpr :: Gen (PathExpr fp)
genPathExpr = PExpPath <$> genPath
-- We choose from a small list of names so that we reuse names often
-- We use the same set of files and directories so that we can test
-- things like trying to open a directory as if it were a file
genPath :: Gen FsPath
genPath = do
n <- choose (0, 3)
mkFsPath <$> replicateM n (elements ["x", "y", "z"])
genHandle :: Gen (HandleRef Symbolic)
genHandle = elements (RE.keys knownHandles)
genMode :: Bool -> Gen OpenMode
genMode fileExists =
frequency
[ (rf, return ReadMode)
, (wf, WriteMode <$> genAllowExisting)
, (wf, AppendMode <$> genAllowExisting)
, (wf, ReadWriteMode <$> genAllowExisting)
]
where
-- we try to avoid 'ReadMode' when the file does not exist.
(rf, wf) = if fileExists then (10, 3) else (1, 3)
genAllowExisting :: Gen AllowExisting
genAllowExisting = elements [AllowExisting, MustBeNew, MustExist]
genSeekMode :: Gen SeekMode
genSeekMode =
elements
[ AbsoluteSeek
, RelativeSeek
, SeekFromEnd
]
genOffset :: Gen Int64
genOffset =
oneof
[ return 0
, choose (1, 10)
, choose (-1, -10)
]
instance Arbitrary AbsOffset where
arbitrary = AbsOffset . getSmall <$> arbitrary
shrink ao = AbsOffset <$> shrink (unAbsOffset ao)
{-------------------------------------------------------------------------------
Temporary files (used in shrinking)
-------------------------------------------------------------------------------}
-- | Temp files are numbered from 1
newtype TempFile = TempFile Int
deriving Show
instance Condense TempFile where -- basically GNTD
condense (TempFile n) = condense n
tempToExpr :: TempFile -> PathExpr fp
tempToExpr (TempFile n) = PExpPath (mkFsPath ['t' : show n])
tempFromPath :: FsPath -> Maybe TempFile
tempFromPath fp =
case map Text.unpack (fsPathToList fp) of
['t' : suf] -> do
n <- readMaybe suf
guard (n >= 1)
return $ TempFile n
_otherwise -> Nothing
{-------------------------------------------------------------------------------
Shrinking
-------------------------------------------------------------------------------}
-- | When we replace one reference with another, we are careful to impose an
-- order so that we don't end up flipping between references. Since shrinking is
-- greedy this does mean that the choice of reference may influence how much we
-- can shrink later. This is hard to avoid in greedy algorithms.
shrinker :: Model Symbolic -> Cmd :@ Symbolic -> [Cmd :@ Symbolic]
shrinker Model{..} (At cmd) =
case cmd of
Open pe mode ->
concat
[ case tempFromPath fp of
Just n ->
map (\n' -> At $ Open (tempToExpr n') mode) $
shrinkTempFile n
Nothing ->
let mode' = case mode of
ReadMode -> ReadWriteMode AllowExisting
_otherwise -> mode
in [At $ Open (tempToExpr (TempFile numTempFiles)) mode']
, case mode of
ReadWriteMode ex ->
[ At $ Open pe ReadMode
, At $ Open pe (WriteMode ex)
]
_otherwise ->
[]
, map (\pe' -> At $ Open pe' mode) $
replaceWithRef pe (== fp) PExpRef
]
where
fp :: FsPath
fp = resolvePathExpr knownPaths pe
ListDirectory pe ->
concat
[ map (At . ListDirectory) $
replaceWithRef pe ((== fp) . fsPathInit) PExpParentOf
]
where
fp :: FsPath
fp = resolvePathExpr knownPaths pe
Get h n -> At . Get h <$> shrink n
GetAt h n o ->
At
<$> [GetAt h n o' | o' <- shrink o]
<> [GetAt h n' o | n' <- shrink n]
GetBuf h n ->
At
<$> [GetBuf h n' | n' <- shrink n]
GetBufAt h n o ->
At
<$> [GetBufAt h n' o | n' <- shrink n]
<> [GetBufAt h n o' | o' <- shrink o]
Put h bs -> At . Put h <$> shrinkBytes bs
PutBuf h bs n ->
At
<$> [PutBuf h bs' n | bs' <- BS.pack <$> shrink (BS.unpack bs)]
<> [PutBuf h bs n' | n' <- shrink n]
PutBufAt h bs n o ->
At
<$> [PutBufAt h bs' n o | bs' <- BS.pack <$> shrink (BS.unpack bs)]
<> [PutBufAt h bs n' o | n' <- shrink n]
<> [PutBufAt h bs n o' | o' <- shrink o]
Truncate h n -> At . Truncate h <$> shrink n
_otherwise ->
[]
where
-- Replace path with reference
--
-- If we are replacing one reference with another, be careful to impose
-- an ordering so that we don't end up toggling between references.
replaceWithRef ::
PathExpr (PathRef Symbolic) ->
-- current
(FsPath -> Bool) ->
-- evaluate candidate
(PathRef Symbolic -> PathExpr (PathRef Symbolic)) ->
-- construct replacement
[PathExpr (PathRef Symbolic)]
replaceWithRef pe p f =
filter (canReplace pe) $ map f $ RE.reverseLookup p knownPaths
where
canReplace ::
PathExpr (PathRef Symbolic) -> -- current
PathExpr (PathRef Symbolic) -> -- candidate
Bool
canReplace (PExpRef ref) (PExpRef ref') = ref' < ref
canReplace (PExpParentOf ref) (PExpParentOf ref') = ref' < ref
canReplace _ _ = True
shrinkTempFile :: TempFile -> [TempFile]
shrinkTempFile (TempFile n) = TempFile . getPositive <$> shrink (Positive n)
shrinkBytes :: ByteString -> [ByteString]
shrinkBytes = map BS.pack . shrink . BS.unpack
numTempFiles :: Int
numTempFiles = 100
{-------------------------------------------------------------------------------
Limitations/known bugs
-------------------------------------------------------------------------------}
-- | Known limitations/bugs that we don't want to test for
--
-- NOTE: Can assume all used handles are in known in the model.
knownLimitation :: Model Symbolic -> Cmd :@ Symbolic -> QSM.Logic
knownLimitation model cmd =
case getResp resp of
Left FsError{..} -> QSM.Boolean fsLimitation
_otherwise -> QSM.Bot
where
(resp, _mockFS') = step model cmd
{-------------------------------------------------------------------------------
The final state machine
-------------------------------------------------------------------------------}
-- | Mock a response
--
-- We do this by running the pure semantics and then generating mock
-- references for any new handles.
mock ::
Model Symbolic ->
Cmd :@ Symbolic ->
QSM.GenSym (Resp :@ Symbolic)
mock model cmd = At <$> bitraverse (const QSM.genSym) (const QSM.genSym) resp
where
(resp, _mockFS') = step model cmd
precondition :: Model Symbolic -> Cmd :@ Symbolic -> QSM.Logic
precondition m@Model{..} (At cmd) =
QSM.forAll (handles cmd) (`QSM.member` RE.keys knownHandles)
QSM.:&& QSM.Boolean (Mock.numOpenHandles mockFS < maxNumOpenHandles)
QSM.:&& QSM.Not (knownLimitation m (At cmd))
where
-- Limit number of open handles to avoid exceeding OS limits
maxNumOpenHandles = 100
-- | Step the model
--
-- NOTE: This function /must/ be polymorphic in @r@.
transition :: (Show1 r, Ord1 r) => Model r -> Cmd :@ r -> Resp :@ r -> Model r
transition model cmd = eventAfter . lockstep model cmd
postcondition ::
Model Concrete ->
Cmd :@ Concrete ->
Resp :@ Concrete ->
QSM.Logic
postcondition model cmd resp =
toMock (eventAfter ev) resp
QSM..== eventMockResp ev
QSM..&& errorHasMountPoint (getResp $ unAt resp)
where
ev = lockstep model cmd resp
errorHasMountPoint :: Either FsError a -> QSM.Logic
errorHasMountPoint (Right _) = QSM.Top
errorHasMountPoint (Left fsError) = QSM.Boolean $ hasMountPoint fsError
semantics :: HasFS IO HandleIO -> Cmd :@ Concrete -> IO (Resp :@ Concrete)
semantics hfs (At cmd) =
At . bimap QSM.reference QSM.reference
<$> runIO hfs (bimap QSM.concrete QSM.concrete cmd)
-- | The state machine proper
sm :: HasFS IO HandleIO -> QSM.StateMachine Model (At Cmd) IO (At Resp)
sm hfs =
QSM.StateMachine
{ initModel = initModel
, transition = transition
, precondition = precondition
, postcondition = postcondition
, generator = Just . generator
, shrinker = shrinker
, semantics = semantics hfs
, mock = mock
, cleanup = QSM.noCleanup
, invariant = Nothing
}
{-------------------------------------------------------------------------------
Labelling
-------------------------------------------------------------------------------}
data Tag
= -- | Create directory then list its parent
--
-- > CreateDir [x, .., y, z]
-- > ListDirectory [x, .., y]
TagCreateDirThenListDir
| -- | Create a directory with its parents, then list its parents
--
-- > CreateDirIfMissing True [x, .., y, z]
-- > ListDirectory [x, .., y]
--
-- Note that this implies all directories must have been created.
TagCreateDirWithParentsThenListDir
| -- | Have a least N open files
--
-- > Open ..
-- > .. --
-- > Open ..
--
-- (with not too many Close calls in between).
TagAtLeastNOpenFiles Int
| -- | Write, then truncate, then write again
--
-- > Put ..
-- > Truncate .. (deleting some but not all of the bytes already written)
-- > Put (write some different bytes)
--
-- Verifies that we correctly modify the file pointer.
TagPutTruncatePut
| -- | Concurrent writer and reader
--
-- > h1 <- Open fp WriteMode ..
-- > h2 <- Open fp ReadMode ..
-- > Put h1 ..
-- > Get h2 ..
TagConcurrentWriterReader
| -- > Get h2 ..
-- | Writing many times should append the bytes.
--
-- > h1 <- Open fp WriteMode .. | > h2 <- Open fp ReadMode ..
-- > Put h1 .. |
-- > Put h1 .. |
TagWriteWriteRead
| -- | Try to open a directory
--
-- > CreateDirectoryIfMissing True fp
-- > Open hp IO.WriteMode
TagOpenDirectory
| -- | Write to a file
--
-- > Put h1
TagWrite
| -- | Seek from end of a file
--
-- > Seek h IO.SeekFromEnd n (n<0)
TagSeekFromEnd
| -- | Create a directory
--
-- > CreateDirIfMissing True ..
TagCreateDirectory
| -- | DoesFileExistOK returns True
TagDoesFileExistOK
| -- | DoesFileExistOK returns False
TagDoesFileExistKO
| -- | DoesDirectoryExistOK returns True
TagDoesDirectoryExistOK
| -- | DoesDirectoryExistOK returns False
TagDoesDirectoryExistKO
| -- | Remove a directory recursively
--
-- > RemoveDirRecursively fe
-- > DoesFileExist fe
TagRemoveDirectoryRecursive
| -- | Remove a file
--
-- > RemoveFile fe
-- > DoesFileExist fe
TagRemoveFile
| -- | Rename a file
--
-- > _ <- Open fe1 WriteMode
-- > RenameFile fe2 fe2
TagRenameFile
| -- | Put truncate and Get
--
-- > Put ..
-- > Truncate ..
-- > Get ..
TagPutTruncateGet
| -- | Close a handle 2 times
--
-- > h <- Open ..
-- > close h
-- > close h
TagClosedTwice
| -- | Open an existing file with ReadMode and then with WriteMode
--
-- > open fp ReadMode
-- > open fp Write
TagOpenReadThenWrite
| -- | Open 2 Readers of a file.
--
-- > open fp ReadMode
-- > open fp ReadMode
TagOpenReadThenRead
| -- | ListDir on a non empty dirextory.
--
-- > CreateDirIfMissing True a/b
-- > ListDirectory a
TagCreateDirWithParentsThenListDirNotNull
| -- | Read from an AppendMode file
--
-- > h <- Open fp AppendMode
-- > Read h ..
TagReadInvalid
| -- | Write to a read only file
--
-- > h <- Open fp ReadMode
-- > Put h ..
TagWriteInvalid
| -- | Put Seek and Get
--
-- > Put ..
-- > Seek ..
-- > Get ..
TagPutSeekGet
| -- | Put Seek (negative) and Get
--
-- > Put ..
-- > Seek .. (negative)
-- > Get ..
TagPutSeekNegGet
| -- | Open with MustBeNew (O_EXCL flag), but the file already existed.
--
-- > h <- Open fp (AppendMode _)
-- > Close h
-- > Open fp (AppendMode MustBeNew)
TagExclusiveFail
| -- | Open a file in read mode successfully
--
-- > h <- Open fp (WriteMode _)
-- > Close h
-- > h <- Open fp ReadMode
TagReadModeMustExist
| -- | Open a file in read mode, but it fails because the file does not exist.
--
-- > h <- Open fp ReadMode
TagReadModeMustExistFail
| -- | Open a file in non-read mode with 'MustExist' successfully.
--
-- > h <- Open fp (_ MustBeNew)
-- > Close h
-- > h <- Open fp (_ MustExist)
TagFileMustExist
| -- | Open a file in non-read mode with 'MustExist', but it fails because the
-- files does not exist.
--
-- > h <- Open fp (_ MustExist)
TagFileMustExistFail
| -- | Reading returns an empty bytestring when EOF
--
-- > h <- open fp ReadMode
-- > Get h 1 == ""
TagReadEOF
| -- | GetAt
--
-- > GetAt ...
TagPread
| -- | Roundtrip for I/O with user-supplied buffers
--
-- > PutBuf h bs c
-- > GetBuf h c (==bs)
TagPutGetBuf
| -- | Roundtrip for I/O with user-supplied buffers
--
-- > PutBufAt h bs c o
-- > GetBufAt h c o (==bs)
TagPutGetBufAt
deriving (Show, Eq)
-- | Predicate on events
type EventPred = C.Predicate (Event Symbolic) Tag
-- | Convenience combinator for creating classifiers for successful commands
--
-- For convenience we pair handles with the paths they refer to
successful ::
( Event Symbolic ->
Success FsPath (Handle HandleMock) ->
Either Tag EventPred
) ->
EventPred
successful f = C.predicate $ \ev ->
case eventMockResp ev of
Resp (Left _) -> Right $ successful f
Resp (Right ok) -> f ev ok
-- | Tag commands
--
-- Tagging works on symbolic events, so that we can tag without doing real IO.
tag :: [Event Symbolic] -> [Tag]
tag =
C.classify
[ tagCreateDirThenListDir Set.empty
, tagCreateDirWithParentsThenListDir Set.empty
, tagAtLeastNOpenFiles 0
, tagPutTruncatePut Map.empty Map.empty Map.empty
, tagConcurrentWriterReader Map.empty
, tagWriteWriteRead Map.empty
, tagOpenDirectory Set.empty
, tagWrite
, tagSeekFromEnd
, tagCreateDirectory
, tagDoesFileExistOK
, tagDoesFileExistKO
, tagDoesDirectoryExistOK
, tagDoesDirectoryExistKO
, tagRemoveDirectoryRecursive Set.empty
, tagRemoveFile Set.empty
, tagRenameFile
, tagPutTruncateGet Map.empty Set.empty
, tagClosedTwice Set.empty
, tagOpenReadThenWrite Set.empty
, tagOpenReadThenRead Set.empty
, tagCreateDirWithParentsThenListDirNotNull Set.empty
, tagReadInvalid Set.empty
, tagWriteInvalid Set.empty
, tagPutSeekGet Set.empty Set.empty
, tagPutSeekNegGet Set.empty Set.empty
, tagExclusiveFail
, tagReadModeMustExist
, tagReadModeMustExistFail
, tagFileMustExist
, tagFileMustExistFail
, tagReadEOF
, tagPread
, tagPutGetBuf Set.empty
, tagPutGetBufAt Set.empty
]
where
tagCreateDirThenListDir :: Set FsPath -> EventPred
tagCreateDirThenListDir created = successful $ \ev _ ->
case eventMockCmd ev of
CreateDir fe ->
Right $ tagCreateDirThenListDir (Set.insert fp created)
where
fp = evalPathExpr fe
ListDirectory fe
| fp `Set.member` (Set.map fsPathInit created) ->
Left TagCreateDirThenListDir
where
fp = evalPathExpr fe
_otherwise ->
Right $ tagCreateDirThenListDir created
tagCreateDirWithParentsThenListDir :: Set FsPath -> EventPred
tagCreateDirWithParentsThenListDir created = successful $ \ev _ ->
case eventMockCmd ev of
CreateDirIfMissing True fe
| length (fsPathToList fp) > 1 ->
Right $ tagCreateDirWithParentsThenListDir (Set.insert fp created)
where
fp = evalPathExpr fe
ListDirectory fe
| fp `Set.member` (Set.map fsPathInit created) ->
Left TagCreateDirWithParentsThenListDir
where
fp = evalPathExpr fe
_otherwise ->
Right $ tagCreateDirWithParentsThenListDir created
tagCreateDirWithParentsThenListDirNotNull :: Set FsPath -> EventPred
tagCreateDirWithParentsThenListDirNotNull created = successful $ \ev suc ->
case (eventMockCmd ev, suc) of
(CreateDirIfMissing True fe, _)
| length (fsPathToList fp) > 1 ->
Right $ tagCreateDirWithParentsThenListDirNotNull (Set.insert fp created)
where
fp = evalPathExpr fe
(ListDirectory fe, Strings set)
| fp `Set.member` (Set.map fsPathInit created)
&& not (Set.null set) ->
Left TagCreateDirWithParentsThenListDirNotNull
where
fp = evalPathExpr fe
_otherwise ->
Right $ tagCreateDirWithParentsThenListDirNotNull created
-- TODO: It turns out we never hit the 10 (or higher) open handles case
-- Not sure if this is a problem or not.
tagAtLeastNOpenFiles :: Int -> EventPred
tagAtLeastNOpenFiles maxNumOpen =
C.Predicate
{ predApply = \ev ->
let maxNumOpen' = max maxNumOpen (countOpen (eventAfter ev))
in Right $ tagAtLeastNOpenFiles maxNumOpen'
, predFinish = case maxNumOpen of
0 -> Nothing
1 -> Just $ TagAtLeastNOpenFiles 1
2 -> Just $ TagAtLeastNOpenFiles 2
n | n < 10 -> Just $ TagAtLeastNOpenFiles 3
n -> Just $ TagAtLeastNOpenFiles (n `div` 10 * 10)
}
where
countOpen :: Model r -> Int
countOpen = Mock.numOpenHandles . mockFS
tagPutTruncateGet ::
Map (HandleMock, FsPath) Int ->
Set (HandleMock, FsPath) ->
EventPred
tagPutTruncateGet put truncated = successful $ \ev _ ->
case eventMockCmd ev of
Put (Handle h fp) bs
| BS.length bs /= 0 ->
let
f Nothing = Just $ BS.length bs
f (Just n) = Just $ (BS.length bs) + n
put' = Map.alter f (h, fp) put
in
Right $ tagPutTruncateGet put' truncated
Truncate (Handle h fp) sz | sz > 0 -> case Map.lookup (h, fp) put of
Just p
| fromIntegral sz < p ->
let truncated' = Set.insert (h, fp) truncated
in Right $ tagPutTruncateGet put truncated'
_otherwise -> Right $ tagPutTruncateGet put truncated
Get (Handle h fp) n
| n > 0
&& ( not $
Set.null $
Set.filter (\(hRead, fp') -> fp' == fp && not (hRead == h)) truncated
) ->
Left TagPutTruncateGet
GetAt (Handle h fp) n _
| n > 0
&& ( not $
Set.null $
Set.filter (\(hRead, fp') -> fp' == fp && not (hRead == h)) truncated
) ->
Left TagPutTruncateGet
_otherwise -> Right $ tagPutTruncateGet put truncated
tagPutTruncatePut ::
Map HandleMock ByteString ->
Map HandleMock ByteString ->
Map HandleMock ByteString ->
EventPred
tagPutTruncatePut before truncated after = successful $ \ev _ ->
case eventMockCmd ev of
Put (Handle h _) bs | BS.length bs /= 0 ->
case Map.lookup h truncated of
Nothing ->
-- not yet truncated
let before' = Map.alter (appTo bs) h before
in Right $ tagPutTruncatePut before' truncated after
Just deleted ->
let putAfter = Map.findWithDefault mempty h after <> bs
after' = Map.insert h putAfter after
in if deleted /= BS.take (BS.length deleted) putAfter
then Left $ TagPutTruncatePut
else Right $ tagPutTruncatePut before truncated after'
Truncate (Handle h _) sz
| sz > 0 ->
let putBefore = Map.findWithDefault mempty h before
(putBefore', deleted) = BS.splitAt (fromIntegral sz) putBefore
before' = Map.insert h putBefore' before
truncated' = Map.insert h deleted truncated
after' = Map.delete h after
in Right $ tagPutTruncatePut before' truncated' after'
_otherwise ->
Right $ tagPutTruncatePut before truncated after
where
appTo :: Monoid a => a -> Maybe a -> Maybe a
appTo b Nothing = Just b
appTo b (Just a) = Just (a <> b)
tagConcurrentWriterReader :: Map HandleMock (Set HandleMock) -> EventPred
tagConcurrentWriterReader put = successful $ \ev@Event{..} _ ->
case eventMockCmd ev of
Put (Handle h fp) bs
| BS.length bs > 0 ->
-- Remember the other handles to the same file open at this time
let readHs :: Set HandleMock
readHs =
Set.fromList $
map handleRaw $
filter (\(Handle h' fp') -> h /= h' && fp == fp') $
openHandles eventBefore
put' :: Map HandleMock (Set HandleMock)
put' = Map.alter (Just . maybe readHs (Set.union readHs)) h put
in Right $ tagConcurrentWriterReader put'
Close (Handle h _) ->
Right $ tagConcurrentWriterReader (Map.delete h put)
Get (Handle h _) n
| h `elem` Set.unions (Map.elems put)
, n > 0 ->
Left TagConcurrentWriterReader
GetAt (Handle h _) n _
| h `elem` Set.unions (Map.elems put)
, n > 0 ->
Left TagConcurrentWriterReader
_otherwise ->
Right $ tagConcurrentWriterReader put
tagOpenReadThenWrite :: Set FsPath -> EventPred
tagOpenReadThenWrite readOpen = successful $ \ev _ ->
case eventMockCmd ev of
Open (PExpPath fp) ReadMode ->
Right $ tagOpenReadThenWrite $ Set.insert fp readOpen
Open (PExpPath fp) (WriteMode _)
| Set.member fp readOpen ->
Left TagOpenReadThenWrite
_otherwise -> Right $ tagOpenReadThenWrite readOpen
tagOpenReadThenRead :: Set FsPath -> EventPred
tagOpenReadThenRead readOpen = successful $ \ev _ ->
case eventMockCmd ev of
Open (PExpPath fp) ReadMode
| Set.member fp readOpen ->
Left TagOpenReadThenRead
Open (PExpPath fp) ReadMode ->
Right $ tagOpenReadThenRead $ Set.insert fp readOpen
_otherwise -> Right $ tagOpenReadThenRead readOpen
tagWriteWriteRead :: Map (HandleMock, FsPath) Int -> EventPred
tagWriteWriteRead wr = successful $ \ev _ ->
case eventMockCmd ev of
Put (Handle h fp) bs
| BS.length bs > 0 ->
let f Nothing = Just 0
f (Just x) = Just $ x + 1
in Right $ tagWriteWriteRead $ Map.alter f (h, fp) wr
Get (Handle hRead fp) n
| n > 1 ->
if not $
Map.null $
Map.filterWithKey (\(hWrite, fp') times -> fp' == fp && times > 1 && not (hWrite == hRead)) wr
then Left TagWriteWriteRead
else Right $ tagWriteWriteRead wr
GetAt (Handle hRead fp) n _
| n > 1 ->
if not $
Map.null $
Map.filterWithKey (\(hWrite, fp') times -> fp' == fp && times > 1 && not (hWrite == hRead)) wr
then Left TagWriteWriteRead
else Right $ tagWriteWriteRead wr
_otherwise ->
Right $ tagWriteWriteRead wr
-- this never succeeds because of an fsLimitation
tagOpenDirectory :: Set FsPath -> EventPred
tagOpenDirectory created = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(CreateDir fe, Resp (Right _)) ->
Right $ tagOpenDirectory (Set.insert fp created)
where
fp = evalPathExpr fe
(CreateDirIfMissing True fe, Resp (Right _)) ->
Right $ tagOpenDirectory (Set.insert fp created)
where
fp = evalPathExpr fe
(Open fe _mode, _)
| Set.member (evalPathExpr fe) created ->
Left TagOpenDirectory
_otherwise ->
Right $ tagOpenDirectory created
tagWrite :: EventPred
tagWrite = successful $ \ev _ ->
case eventMockCmd ev of
Put _ bs
| BS.length bs > 0 ->
Left TagWrite
_otherwise -> Right tagWrite
tagSeekFromEnd :: EventPred
tagSeekFromEnd = successful $ \ev _ ->
case eventMockCmd ev of
Seek _ SeekFromEnd n | n < 0 -> Left TagSeekFromEnd
_otherwise -> Right tagSeekFromEnd
tagCreateDirectory :: EventPred
tagCreateDirectory = successful $ \ev _ ->
case eventMockCmd ev of
CreateDirIfMissing True (PExpPath fp)
| length (fsPathToList fp) > 1 ->
Left TagCreateDirectory
_otherwise ->
Right tagCreateDirectory
tagDoesFileExistOK :: EventPred
tagDoesFileExistOK = successful $ \ev suc ->
case (eventMockCmd ev, suc) of
(DoesFileExist _, Bool True) -> Left TagDoesFileExistOK
_otherwise -> Right tagDoesFileExistOK
tagDoesFileExistKO :: EventPred
tagDoesFileExistKO = successful $ \ev suc ->
case (eventMockCmd ev, suc) of
(DoesFileExist _, Bool False) -> Left TagDoesFileExistKO
_otherwise -> Right tagDoesFileExistKO
tagDoesDirectoryExistOK :: EventPred
tagDoesDirectoryExistOK = successful $ \ev suc ->
case (eventMockCmd ev, suc) of
(DoesDirectoryExist (PExpPath fp), Bool True)
| not (fp == mkFsPath ["/"]) ->
Left TagDoesDirectoryExistOK
_otherwise -> Right tagDoesDirectoryExistOK
tagDoesDirectoryExistKO :: EventPred
tagDoesDirectoryExistKO = successful $ \ev suc ->
case (eventMockCmd ev, suc) of
(DoesDirectoryExist _, Bool False) -> Left TagDoesDirectoryExistKO
_otherwise -> Right tagDoesDirectoryExistKO
tagRemoveDirectoryRecursive :: Set FsPath -> EventPred
tagRemoveDirectoryRecursive removed = successful $ \ev _suc ->
case eventMockCmd ev of
RemoveDirRecursive fe -> Right $ tagRemoveDirectoryRecursive $ Set.insert fp removed
where
fp = evalPathExpr fe
DoesFileExist fe ->
if Set.member fp removed
then Left TagRemoveDirectoryRecursive
else Right $ tagRemoveDirectoryRecursive removed
where
fp = evalPathExpr fe
_otherwise -> Right $ tagRemoveDirectoryRecursive removed
tagRemoveFile :: Set FsPath -> EventPred
tagRemoveFile removed = successful $ \ev _suc ->
case eventMockCmd ev of
RemoveFile fe -> Right $ tagRemoveFile $ Set.insert fp removed
where
fp = evalPathExpr fe
DoesFileExist fe ->
if Set.member fp removed
then Left TagRemoveFile
else Right $ tagRemoveFile removed
where
fp = evalPathExpr fe
_otherwise -> Right $ tagRemoveFile removed
tagRenameFile :: EventPred
tagRenameFile = successful $ \ev _suc ->
case eventMockCmd ev of
RenameFile{} -> Left TagRenameFile
_otherwise -> Right tagRenameFile
tagClosedTwice :: Set HandleMock -> EventPred
tagClosedTwice closed = successful $ \ev _suc ->
case eventMockCmd ev of
Close (Handle h _) | Set.member h closed -> Left TagClosedTwice
Close (Handle h _) -> Right $ tagClosedTwice $ Set.insert h closed
_otherwise -> Right $ tagClosedTwice closed
-- this never succeeds because of an fsLimitation
tagReadInvalid :: Set HandleMock -> EventPred
tagReadInvalid openAppend = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(Open _ (AppendMode _), Resp (Right (WHandle _ (Handle h _)))) ->
Right $ tagReadInvalid $ Set.insert h openAppend
(Close (Handle h _), Resp (Right _)) ->
Right $ tagReadInvalid $ Set.delete h openAppend
(Get (Handle h _) _, Resp (Left _))
| Set.member h openAppend ->
Left TagReadInvalid
(GetAt (Handle h _) _ _, Resp (Left _))
| Set.member h openAppend ->
Left TagReadInvalid
_otherwise -> Right $ tagReadInvalid openAppend
tagWriteInvalid :: Set HandleMock -> EventPred
tagWriteInvalid openRead = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(Open _ ReadMode, Resp (Right (RHandle (Handle h _)))) ->
Right $ tagWriteInvalid $ Set.insert h openRead
(Close (Handle h _), Resp (Right _)) ->
Right $ tagWriteInvalid $ Set.delete h openRead
(Put (Handle h _) _, _)
| Set.member h openRead ->
Left TagWriteInvalid
_otherwise -> Right $ tagWriteInvalid openRead
tagPutSeekGet :: Set HandleMock -> Set HandleMock -> EventPred
tagPutSeekGet put seek = successful $ \ev _suc ->
case eventMockCmd ev of
Put (Handle h _) bs
| BS.length bs > 0 ->
Right $ tagPutSeekGet (Set.insert h put) seek
Seek (Handle h _) RelativeSeek n
| n > 0 && Set.member h put ->
Right $ tagPutSeekGet put (Set.insert h seek)
Get (Handle h _) n
| n > 0 && Set.member h seek ->
Left TagPutSeekGet
GetAt (Handle h _) n _
| n > 0 && Set.member h seek ->
Left TagPutSeekGet
_otherwise -> Right $ tagPutSeekGet put seek
tagPutSeekNegGet :: Set HandleMock -> Set HandleMock -> EventPred
tagPutSeekNegGet put seek = successful $ \ev _suc ->
case eventMockCmd ev of
Put (Handle h _) bs
| BS.length bs > 0 ->
Right $ tagPutSeekNegGet (Set.insert h put) seek
Seek (Handle h _) RelativeSeek n
| n < 0 && Set.member h put ->
Right $ tagPutSeekNegGet put (Set.insert h seek)
Get (Handle h _) n
| n > 0 && Set.member h seek ->
Left TagPutSeekNegGet
GetAt (Handle h _) n _
| n > 0 && Set.member h seek ->
Left TagPutSeekNegGet
_otherwise -> Right $ tagPutSeekNegGet put seek
tagExclusiveFail :: EventPred
tagExclusiveFail = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(Open _ mode, Resp (Left fsError))
| MustBeNew <- allowExisting mode
, fsErrorType fsError == FsResourceAlreadyExist ->
Left TagExclusiveFail
_otherwise -> Right tagExclusiveFail
tagReadModeMustExist :: EventPred
tagReadModeMustExist = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(Open _ ReadMode, Resp (Right (RHandle _))) -> Left TagReadModeMustExist
_otherwise -> Right tagReadModeMustExist
tagReadModeMustExistFail :: EventPred
tagReadModeMustExistFail = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(Open _ ReadMode, Resp (Left fsError))
| fsErrorType fsError == FsResourceDoesNotExist ->
Left TagReadModeMustExistFail
_otherwise -> Right tagReadModeMustExistFail
tagFileMustExist :: EventPred
tagFileMustExist = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(Open _ mode, Resp (Right (WHandle _ _)))
| MustExist <- allowExisting mode
, mode /= ReadMode ->
Left TagFileMustExist
_otherwise -> Right tagFileMustExist
tagFileMustExistFail :: EventPred
tagFileMustExistFail = C.predicate $ \ev ->
case (eventMockCmd ev, eventMockResp ev) of
(Open _ mode, Resp (Left fsError))
| MustExist <- allowExisting mode
, mode /= ReadMode
, fsErrorType fsError == FsResourceDoesNotExist ->
Left TagFileMustExistFail
_otherwise -> Right tagFileMustExistFail
tagReadEOF :: EventPred
tagReadEOF = successful $ \ev suc ->
case (eventMockCmd ev, suc) of
(Get _ n, ByteString bl)
| n > 0, BS.null bl -> Left TagReadEOF
_otherwise -> Right tagReadEOF
tagPread :: EventPred
tagPread = successful $ \ev _ ->
case eventMockCmd ev of
GetAt{} -> Left TagPread
_otherwise -> Right tagPread
tagPutGetBufAt :: Set HandleMock -> EventPred
tagPutGetBufAt put = successful $ \ev _ ->
case eventMockCmd ev of
PutBufAt (Handle h _) bs c _
| BS.length bs > 0 && c > 0 ->
Right (tagPutGetBufAt (Set.insert h put))
GetBufAt _ c _
| c > 0 ->
Left TagPutGetBufAt
_otherwise ->
Right (tagPutGetBufAt put)
tagPutGetBuf :: Set HandleMock -> EventPred
tagPutGetBuf put = successful $ \ev _ ->
case eventMockCmd ev of
PutBuf (Handle h _) bs c
| BS.length bs > 0 && c > 0 ->
Right (tagPutGetBuf (Set.insert h put))
GetBuf _ c
| c > 0 ->
Left TagPutGetBuf
_otherwise ->
Right (tagPutGetBuf put)
-- | Step the model using a 'QSM.Command' (i.e., a command associated with
-- an explicit set of variables)
execCmd :: Model Symbolic -> QSM.Command (At Cmd) (At Resp) -> Event Symbolic
execCmd model (QSM.Command cmd resp _vars) = lockstep model cmd resp
-- | 'execCmds' is just the repeated form of 'execCmd'
execCmds :: QSM.Commands (At Cmd) (At Resp) -> [Event Symbolic]
execCmds = \(QSM.Commands cs) -> go initModel cs
where
go :: Model Symbolic -> [QSM.Command (At Cmd) (At Resp)] -> [Event Symbolic]
go _ [] = []
go m (c : cs) = let ev = execCmd m c in ev : go (eventAfter ev) cs
{-------------------------------------------------------------------------------
Required instances
The 'ToExpr' constraints come from "Data.TreeDiff".
-------------------------------------------------------------------------------}
constrInfo ::
SOP.HasDatatypeInfo a =>
proxy a ->
SOP.NP SOP.ConstructorInfo (SOP.Code a)
constrInfo = SOP.constructorInfo . SOP.datatypeInfo
constrName :: forall a. SOP.HasDatatypeInfo a => a -> String
constrName a =
SOP.hcollapse $ SOP.hliftA2 go (constrInfo p) (SOP.unSOP (SOP.from a))
where
go :: SOP.ConstructorInfo b -> SOP.NP SOP.I b -> SOP.K String b
go nfo _ = SOP.K $ SOP.constructorName nfo
p = Proxy @a
constrNames :: SOP.HasDatatypeInfo a => proxy a -> [String]
constrNames p =
SOP.hcollapse $ SOP.hmap go (constrInfo p)
where
go :: SOP.ConstructorInfo a -> SOP.K String a
go nfo = SOP.K $ SOP.constructorName nfo
instance QSM.CommandNames (At Cmd) where
cmdName (At cmd) = constrName cmd
cmdNames _ = constrNames (Proxy @(Cmd () ()))
deriving instance ToExpr a => ToExpr (FsTree a)
deriving instance ToExpr fp => ToExpr (PathExpr fp)
deriving instance ToExpr HandleMock
deriving instance ToExpr MockFS
deriving instance ToExpr Mock.HandleState
deriving instance ToExpr Mock.OpenHandleState
deriving instance ToExpr Mock.ClosedHandleState
deriving instance ToExpr Mock.FilePtr
deriving instance ToExpr FsPath
instance ToExpr (Handle h) where
toExpr = defaultExprViaShow
deriving instance ToExpr (Model Concrete)
{-------------------------------------------------------------------------------
Top-level tests
-------------------------------------------------------------------------------}
-- | Show minimal examples for each of the generated tags
--
-- TODO: The examples listed are not always minimal. I'm not entirely sure why.
showLabelledExamples' ::
-- | Seed
Maybe Int ->
-- | Number of tests to run to find examples
Int ->
-- | Tag filter (can be @const True@)
(Tag -> Bool) ->
IO ()
showLabelledExamples' mReplay numTests focus = do
replaySeed <- case mReplay of
Nothing -> getStdRandom (randomR (1, 999999))
Just seed -> return seed
labelledExamplesWith
( stdArgs
{ replay = Just (mkQCGen replaySeed, 0)
, maxSuccess = numTests
}
)
$ forAllShrinkShow
(QSM.generateCommands sm' Nothing)
(QSM.shrinkCommands sm')
pp
$ \cmds ->
collects (filter focus . tag . execCmds $ cmds) $
property True
putStrLn $ "Used replaySeed " ++ show replaySeed
where
sm' = sm unusedHasFS
pp = \x -> ppShow x ++ "\n" ++ condense x
collects :: Show a => [a] -> Property -> Property
collects = repeatedly collect
where
repeatedly :: (a -> b -> b) -> ([a] -> b -> b)
repeatedly = flip . foldl' . flip
showLabelledExamples :: IO ()
showLabelledExamples = showLabelledExamples' Nothing 1000 (const True)
prop_sequential :: Property
prop_sequential =
withMaxSuccess 1000 $
QSM.forAllCommands (sm unusedHasFS) Nothing $
runCmds
runCmds :: QSM.Commands (At Cmd) (At Resp) -> Property
runCmds cmds = QC.monadicIO $ do
(tstTmpDir, hist, res) <- QC.run $
withSystemTempDirectory "StateMachine" $ \tstTmpDir -> do
let mount = MountPoint tstTmpDir
hfs = ioHasFS mount
sm' = sm hfs
(hist, model, res) <- QSM.runCommands' sm' cmds
-- Close all open handles
forM_ (RE.keys (knownHandles model)) $ hClose hfs . QSM.concrete
return (tstTmpDir, hist, res)
QSM.prettyCommands (sm unusedHasFS) hist $
QSM.checkCommandNames cmds $
tabulate "Tags" (map show $ tag (execCmds cmds)) $
counterexample ("Mount point: " ++ tstTmpDir) $
res === QSM.Ok
tests :: TestTree
tests =
testGroup
"Test.System.FS.StateMachine"
[ testProperty "q-s-m" $ prop_sequential
, localOption (QuickCheckTests 1) $
testProperty "regression_removeFileOnDir" $
runCmds regression_removeFileOnDir
]
-- | Unused HasFS
--
-- 'forAllCommands' wants the entire state machine as argument, but we need the
-- HasFS only when /executing/ the commands in IO. We can therefore generate the
-- commands with a dummy HasFS, and then inside the property construct a
-- temporary directory which we can use for execution.
unusedHasFS :: HasFS m h
unusedHasFS = error "HasFS not used during command generation"
-- | The error numbers returned by Linux vs. MacOS differ when using
-- 'removeFile' on a directory. The model mainly mimicks Linux-style errors,
-- which results in an 'FsResourceInappropriateType' error, whereas on MacOS it
-- results in an 'FsInsufficientPermissions' error. The implementation of
-- 'F.sameError' was made more lenient for MacOS in fs-sim#41 to allow this
-- model-SUT discrepancy to occur without making the tests fail. We might revist
-- this /temporary/ fix in the future, see fs-sim#45.
regression_removeFileOnDir :: QSM.Commands (At Cmd) (At Resp)
regression_removeFileOnDir =
QSM.Commands
{ unCommands =
[ QSM.Command
( At
{ unAt =
CreateDirIfMissing
True
(PExpPath (mkFsPath ["x"]))
}
)
( At
{ unAt =
Resp
{ getResp =
Right (Path (QSM.Reference (QSM.Symbolic (QSM.Var 0))) ())
}
}
)
[QSM.Var 0]
, QSM.Command
( At
{ unAt =
RemoveFile
(PExpPath (mkFsPath ["x"]))
}
)
( At
{ unAt =
Resp
{ getResp =
Left
( FsError
{ fsErrorType = FsResourceInappropriateType
, fsErrorPath = FsErrorPath Nothing (mkFsPath ["x"])
, fsErrorString = "expected file"
, fsErrorNo = Nothing
, fsErrorStack = prettyCallStack
, fsLimitation = False
}
)
}
}
)
[]
]
}
{-------------------------------------------------------------------------------
Debugging
-------------------------------------------------------------------------------}
-- | Debugging: show @n@ levels of shrink steps (with some required tags)
--
-- This can be useful when debugging the shrinker
_showTaggedShrinks ::
-- | Required tags
([Tag] -> Bool) ->
-- | Number of shrink steps
Int ->
QSM.Commands (At Cmd) (At Resp) ->
IO ()
_showTaggedShrinks hasRequiredTags numLevels = go 0
where
go :: Int -> QSM.Commands (At Cmd) (At Resp) -> IO ()
go n _ | n == numLevels = return ()
go n cmds = do
if hasRequiredTags tags
then do
putStrLn $ replicate n '\t' ++ condense (cmds, tags)
forM_ shrinks $ go (n + 1)
else
return ()
where
tags = tag $ execCmds cmds
shrinks = QSM.shrinkCommands (sm unusedHasFS) cmds
{-------------------------------------------------------------------------------
Pretty-printing
-------------------------------------------------------------------------------}
instance Condense fp => Condense (PathExpr fp) where
condense (PExpPath fp) = condense fp
condense (PExpRef fp) = condense fp
condense (PExpParentOf fp) = condense fp ++ "/.."
instance (Condense fp, Condense h) => Condense (Cmd fp h) where
condense = L.intercalate " " . go
where
go (Open fp mode) = ["open", condense fp, condense mode]
go (Close h) = ["close", condense h]
go (IsOpen h) = ["isOpen", condense h]
go (Seek h mode o) = ["seek", condense h, condense mode, condense o]
go (Get h n) = ["get", condense h, condense n]
go (GetAt h n o) = ["getAt", condense h, condense n, condense o]
go (GetBuf h n) = ["getBuf", condense h, condense n]
go (GetBufAt h n o) = ["getBufAt", condense h, condense n, condense o]
go (Put h bs) = ["put", condense h, condense bs]
go (PutBuf h bs n) = ["putBuf", condense h, condense bs, condense n]
go (PutBufAt h bs n o) = ["putBufAt", condense h, condense bs, condense n, condense o]
go (Truncate h sz) = ["truncate", condense h, condense sz]
go (GetSize h) = ["getSize", condense h]
go (CreateDir fp) = ["createDir", condense fp]
go (CreateDirIfMissing p fp) = ["createDirIfMissing", condense p, condense fp]
go (ListDirectory fp) = ["listDirectory", condense fp]
go (DoesDirectoryExist fp) = ["doesDirectoryExist", condense fp]
go (DoesFileExist fp) = ["doesFileExist", condense fp]
go (RemoveDirRecursive fp) = ["removeDirectoryRecursive", condense fp]
go (RemoveFile fp) = ["removeFile", condense fp]
go (RenameFile fp1 fp2) = ["renameFile", condense fp1, condense fp2]
instance Condense1 r => Condense (Cmd :@ r) where
condense (At cmd) = condense cmd
instance Condense Tag where
condense = show
instance Condense AbsOffset where
condense = show
instance Condense ByteCount where
condense = show
{-------------------------------------------------------------------------------
(Orphan) condense instance for QSM types
-------------------------------------------------------------------------------}
instance Condense QSM.Var where
condense (QSM.Var i) = "x" ++ condense i
instance Condense1 Symbolic where
liftCondense _ (QSM.Symbolic a) = condense a
instance Condense (QSM.Opaque a) where
condense _ = "<>"
instance (Condense1 r, Condense a) => Condense (QSM.Reference a r) where
condense (QSM.Reference ra) = condense1 ra
instance Condense (cmd Symbolic) => Condense (QSM.Command cmd resp) where
condense = \(QSM.Command cmd _resp vars) ->
L.intercalate " " $ go cmd vars
where
go :: cmd Symbolic -> [QSM.Var] -> [String]
go cmd [] = [condense cmd]
go cmd xs = [condense xs, "<-", condense cmd]
instance Condense (cmd Symbolic) => Condense (QSM.Commands cmd resp) where
condense (QSM.Commands cmds) = unlines $ "do" : map (indent . condense) cmds
where
indent :: String -> String
indent = (" " ++)