diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for quickcheck-lockstep + +## 0.1.0 -- 2022-10-11 + +* First release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2022, Edsko de Vries + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Edsko de Vries nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/quickcheck-lockstep.cabal b/quickcheck-lockstep.cabal new file mode 100644 --- /dev/null +++ b/quickcheck-lockstep.cabal @@ -0,0 +1,97 @@ +cabal-version: 2.4 +name: quickcheck-lockstep +version: 0.1.0 +license: BSD-3-Clause +license-file: LICENSE +author: Edsko de Vries +maintainer: edsko@well-typed.com +extra-source-files: CHANGELOG.md +category: Testing +synopsis: Library for lockstep-style testing with 'quickcheck-dynamic' +description: Lockstep-style testing is a particular approach for blackbox + testing of stateful APIs: we generate a random sequence of + APIs calls, then execute them both against the system under + test and against a model, and compare responses up to some + notion of observability. + +source-repository head + type: git + location: https://github.com/well-typed/quickcheck-lockstep + +common lang + default-language: + Haskell2010 + default-extensions: + FlexibleContexts + FlexibleInstances + GADTs + ImportQualifiedPost + LambdaCase + MultiParamTypeClasses + QuantifiedConstraints + RankNTypes + ScopedTypeVariables + StandaloneDeriving + TypeApplications + TypeFamilies + other-extensions: + UndecidableInstances + ghc-options: + -Wall + -Wprepositive-qualified-module + -Wredundant-constraints + +library + import: + lang + exposed-modules: + Test.QuickCheck.StateModel.Lockstep + Test.QuickCheck.StateModel.Lockstep.Defaults + Test.QuickCheck.StateModel.Lockstep.Op.Identity + Test.QuickCheck.StateModel.Lockstep.Op.SumProd + Test.QuickCheck.StateModel.Lockstep.Run + other-modules: + Test.QuickCheck.StateModel.Lockstep.API + Test.QuickCheck.StateModel.Lockstep.EnvF + Test.QuickCheck.StateModel.Lockstep.GVar + Test.QuickCheck.StateModel.Lockstep.Op + build-depends: + -- quickcheck-dynamic requires ghc 8.10 minimum + base >= 4.14 && < 4.15 + , mtl >= 2.2 && < 2.3 + , containers >= 0.6 && < 0.7 + , QuickCheck >= 2.14 && < 2.15 + , quickcheck-dynamic >= 2.0 && < 2.1 + hs-source-dirs: + src + +test-suite test-quickcheck-lockstep + import: + lang + type: + exitcode-stdio-1.0 + hs-source-dirs: + test + main-is: + Main.hs + other-modules: + Test.MockFS + Test.MockFS.Mock + Test.IORef + default-extensions: + DeriveGeneric + EmptyCase + build-depends: + -- Version bounds determined by main lib + base + , containers + , directory + , filepath + , mtl + , QuickCheck + , quickcheck-dynamic + , quickcheck-lockstep + , tasty + , tasty-hunit + , tasty-quickcheck + , temporary diff --git a/src/Test/QuickCheck/StateModel/Lockstep.hs b/src/Test/QuickCheck/StateModel/Lockstep.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep.hs @@ -0,0 +1,37 @@ +-- | Lockstep-style testing using @quickcheck-dynamic@ +-- +-- See +-- for a tutorial. +-- +-- This module is intended for unqualified import alongside imports of +-- "Test.QuickCheck.StateModel". +-- +-- > import Test.QuickCheck.StateModel +-- > import Test.QuickCheck.StateModel.Lockstep +-- > import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep +-- > import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep +module Test.QuickCheck.StateModel.Lockstep ( + -- * Main abstraction + Lockstep -- opaque + , InLockstep(..) + , RunLockstep(..) + -- ** Convenience aliases + , LockstepAction + , ModelFindVariables + , ModelLookUp + , ModelVar + -- * Variables + , GVar -- opaque + , AnyGVar(..) + , lookUpGVar + , mapGVar + -- ** Operations + , Operation(..) + , InterpretOp(..) + ) where + +import Prelude hiding (init) + +import Test.QuickCheck.StateModel.Lockstep.API +import Test.QuickCheck.StateModel.Lockstep.Op +import Test.QuickCheck.StateModel.Lockstep.GVar diff --git a/src/Test/QuickCheck/StateModel/Lockstep/API.hs b/src/Test/QuickCheck/StateModel/Lockstep/API.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/API.hs @@ -0,0 +1,174 @@ +-- | Public API +-- +-- This is re-exported through "Test.QuickCheck.StateModel.Lockstep". +module Test.QuickCheck.StateModel.Lockstep.API ( + -- * State + Lockstep(..) + -- * Main abstraction + , InLockstep(..) + , RunLockstep(..) + -- * Convenience aliases + , LockstepAction + , ModelFindVariables + , ModelLookUp + , ModelVar + ) where + +import Data.Kind +import Data.Typeable + +import Test.QuickCheck (Gen) +import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action) + +import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF) +import Test.QuickCheck.StateModel.Lockstep.GVar (GVar, AnyGVar(..)) +import Test.QuickCheck.StateModel.Lockstep.Op +import Test.QuickCheck.StateModel.Lockstep.Op.Identity qualified as Identity + +{------------------------------------------------------------------------------- + Lockstep state + + @quickcheck-dynamic@ takes care of keeping track of the responses of the + system under test, but not the model. We do that here. + + Implementation note: the 'RunModel' class in @quickcheck-dynamic@ uses a type + family 'Realized': for an @Action state a@, the response from the real system + is expected to be of type @Realized m a@. This allows the same tests to be run + against different "test execution backends"; for example, we could run the + tests in the real IO monad, or using an IO monad simulator. + + This is an orthogonal generalization to what Lockstep provides: no matter the + test execution backend, the /model/ will always be the same. We could perhaps + piggy-back on the same abstraction if we introduced a separate monad parameter + @n@ for the model, and then use @Realized n a@ instead of @ModelValue a@. This + might work, but it's less clear how to then also that for 'Observable'. + Overall, it seems cleaner to reserve 'Realized' exclusively for the + parameterization over test execution backends. +-------------------------------------------------------------------------------} + +data Lockstep state = Lockstep { + lockstepModel :: state + , lockstepEnv :: EnvF (ModelValue state) + } + +-- | The 'Show' instance does not show the internal environment +instance Show state => Show (Lockstep state) where + show = show . lockstepModel + +{------------------------------------------------------------------------------- + Main lockstep abstraction +-------------------------------------------------------------------------------} + +class + ( StateModel (Lockstep state) + , Typeable state + , InterpretOp (ModelOp state) (ModelValue state) + , forall a. Show (ModelValue state a) + , forall a. Eq (Observable state a) + , forall a. Show (Observable state a) + ) + => InLockstep state where + -- | Values in the mock environment + -- + -- 'ModelValue' witnesses the relation between values returned by the real + -- system and values returned by the model. + -- + -- In most cases, we expect the real system and the model to return the + -- /same/ value. However, for some things we must allow them to diverge: + -- consider file handles for example. + data ModelValue state a + + -- | Observable responses + -- + -- The real system returns values of type @a@, and the model returns values + -- of type @MockValue a@. @Observable a@ defines the parts of those results + -- that expect to be the /same/ for both. + data Observable state a + + -- | Type of operations required on the results of actions + -- + -- Whenever an action has a result of type @a@, but we later need a variable + -- of type @b@, we need a constructor + -- + -- > GetB :: ModelOp state a b + -- + -- in the 'ModelOp' type. For many tests, the standard 'Op' type will + -- suffice, but not always. + type ModelOp state :: Type -> Type -> Type + type ModelOp state = Identity.Op + + -- | Extract the observable part of a response from the model + observeModel :: ModelValue state a-> Observable state a + + -- | All variables required by a command + usedVars :: LockstepAction state a -> [AnyGVar (ModelOp state)] + + -- | Step the model + -- + -- The order of the arguments mimicks 'perform'. + modelNextState :: + LockstepAction state a + -> ModelLookUp state + -> state + -> (ModelValue state a, state) + + -- | Generate an arbitrary action, given a way to find variables + arbitraryWithVars :: + ModelFindVariables state + -> state + -> Gen (Any (LockstepAction state)) + + -- | Shrink an action, given a way to find variables + -- + -- This is optional; without an implementation of 'shrinkWithVars', lists of + -- actions will still be pruned, but /individual/ actions will not be shrunk. + shrinkWithVars :: + ModelFindVariables state + -> state + -> LockstepAction state a + -> [Any (LockstepAction state)] + shrinkWithVars _ _ _ = [] + + -- | Tag actions + -- + -- Tagging is optional, but can help understand your test input data as + -- well as your shrinker (see 'tagActions'). + tagStep :: + (state, state) + -> LockstepAction state a + -> ModelValue state a + -> [String] + tagStep _ _ _ = [] + +class ( InLockstep state + , RunModel (Lockstep state) m + ) => RunLockstep state m where + -- See also 'Observable' + observeReal :: + Proxy m + -> LockstepAction state a -> Realized m a -> Observable state a + +{------------------------------------------------------------------------------- + Convenience aliases +-------------------------------------------------------------------------------} + +-- | An action in the lock-step model +type LockstepAction state = Action (Lockstep state) + +-- | Look up a variable for model execution +-- +-- The type of the variable is the type in the /real/ system. +type ModelLookUp state = forall a. ModelVar state a -> ModelValue state a + +-- | Find variables of the appropriate type +-- +-- The type you pass must be the result type of (previously executed) actions. +-- If you want to change the type of the variable, see +-- 'StateModel.Lockstep.GVar.map'. +type ModelFindVariables state = forall a. + Typeable a + => Proxy a -> [GVar (ModelOp state) a] + +-- | Variables with a "functor-esque" instance +type ModelVar state = GVar (ModelOp state) + diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs b/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs @@ -0,0 +1,155 @@ +-- | Default implementations for the @quickcheck-dynamic@ class methods +-- +-- Intended for qualified import. +-- +-- > import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep +module Test.QuickCheck.StateModel.Lockstep.Defaults ( + -- * Default implementations for methods of 'StateModel' + initialState + , nextState + , precondition + , arbitraryAction + , shrinkAction + -- * Default implementations for methods of 'RunModel' + , postcondition + , monitoring + ) where + +import Prelude hiding (init) + +import Data.Maybe (isNothing) +import Data.Typeable + +import Test.QuickCheck (Gen, Property) +import Test.QuickCheck qualified as QC +import Test.QuickCheck.StateModel (Var, Any(..), LookUp, Realized) + +import Test.QuickCheck.StateModel.Lockstep.API +import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF) +import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF +import Test.QuickCheck.StateModel.Lockstep.GVar + +{------------------------------------------------------------------------------- + Default implementations for members of 'StateModel' +-------------------------------------------------------------------------------} + +-- | Default implementation for 'Test.QuickCheck.StateModel.initialState' +initialState :: state -> Lockstep state +initialState state = Lockstep { + lockstepModel = state + , lockstepEnv = EnvF.empty + } + +-- | Default implementation for 'Test.QuickCheck.StateModel.nextState' +nextState :: forall state a. + (InLockstep state, Typeable a) + => Lockstep state + -> LockstepAction state a + -> Var a + -> Lockstep state +nextState (Lockstep state env) action var = + Lockstep state' $ EnvF.insert var modelResp env + where + modelResp :: ModelValue state a + state' :: state + (modelResp, state') = modelNextState action (lookUpEnvF env) state + +-- | Default implementation for 'Test.QuickCheck.StateModel.precondition' +-- +-- The default precondition only checks that all variables have a value +-- and that the operations on them are defined. +precondition :: + InLockstep state + => Lockstep state -> LockstepAction state a -> Bool +precondition (Lockstep _ env) = + all (\(SomeGVar var) -> definedInEnvF env var) . usedVars + +-- | Default implementation for 'Test.QuickCheck.StateModel.arbitraryAction' +arbitraryAction :: + InLockstep state + => Lockstep state -> Gen (Any (LockstepAction state)) +arbitraryAction (Lockstep state env) = + arbitraryWithVars (varsOfType env) state + +-- | Default implementation for 'Test.QuickCheck.StateModel.shrinkAction' +shrinkAction :: + InLockstep state + => Lockstep state + -> LockstepAction state a -> [Any (LockstepAction state)] +shrinkAction (Lockstep state env) = + shrinkWithVars (varsOfType env) state + +{------------------------------------------------------------------------------- + Default implementations for methods of 'RunModel' +-------------------------------------------------------------------------------} + +-- | Default implementation for 'Test.QuickCheck.StateModel.postcondition' +-- +-- The default postcondition verifies that the real system and the model +-- return the same results, up to " observability ". +postcondition :: forall m state a. + RunLockstep state m + => (Lockstep state, Lockstep state) + -> LockstepAction state a + -> LookUp m + -> Realized m a + -> m Bool +postcondition (before, _after) action _lookUp a = + pure $ isNothing $ checkResponse (Proxy @m) before action a + +monitoring :: forall m state a. + RunLockstep state m + => Proxy m + -> (Lockstep state, Lockstep state) + -> LockstepAction state a + -> LookUp m + -> Realized m a + -> Property -> Property +monitoring p (before, after) action _lookUp realResp = + QC.counterexample ("State: " ++ show after) + . maybe id QC.counterexample (checkResponse p before action realResp) + . QC.tabulate "Tags" tags + where + tags :: [String] + tags = tagStep (lockstepModel before, lockstepModel after) action modelResp + + modelResp :: ModelValue state a + modelResp = fst $ modelNextState + action + (lookUpEnvF $ lockstepEnv before) + (lockstepModel before) + +{------------------------------------------------------------------------------- + Internal auxiliary +-------------------------------------------------------------------------------} + +varsOfType :: + InLockstep state + => EnvF (ModelValue state) -> ModelFindVariables state +varsOfType env _ = map fromVar $ EnvF.keysOfType env + +-- | Check the response of the system under test against the model +-- +-- This is used in 'postcondition', where we can however only return a 'Bool', +-- and in 'monitoring', to give the user more detailed feedback. +checkResponse :: forall m state a. + RunLockstep state m + => Proxy m + -> Lockstep state -> LockstepAction state a -> Realized m a -> Maybe String +checkResponse p (Lockstep state env) action a = + compareEquality (observeReal p action a) (observeModel modelResp) + where + modelResp :: ModelValue state a + modelResp = fst $ modelNextState action (lookUpEnvF env) state + + compareEquality :: Observable state a -> Observable state a -> Maybe String + compareEquality real mock + | real == mock = Nothing + | otherwise = Just $ concat [ + "System under test returned: " + , show real + , "\nbut model returned: " + , show mock + ] + + diff --git a/src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs b/src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs @@ -0,0 +1,59 @@ +-- | Environment parameterised by functor @f@ +-- +-- Intended for qualified import: +-- +-- > import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF) +-- > import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF +module Test.QuickCheck.StateModel.Lockstep.EnvF ( + EnvF -- opaque + -- * Construction + , empty + , insert + -- * Query + , lookup + , keysOfType + ) where + +import Prelude hiding (lookup) + +import Control.Monad +import Data.Foldable (asum) +import Data.Maybe (mapMaybe) +import Data.Typeable + +import Test.QuickCheck.StateModel (Var(..)) + +{------------------------------------------------------------------------------- + Types +-------------------------------------------------------------------------------} + +data EnvEntry f where + EnvEntry :: Typeable a => Var a -> f a -> EnvEntry f + +newtype EnvF f = EnvF [EnvEntry f] + +{------------------------------------------------------------------------------- + Construction +-------------------------------------------------------------------------------} + +empty :: EnvF f +empty = EnvF [] + +insert :: Typeable a => Var a -> f a -> EnvF f -> EnvF f +insert x fa (EnvF env) = EnvF (EnvEntry x fa : env) + +{------------------------------------------------------------------------------- + Query +-------------------------------------------------------------------------------} + +lookup :: forall f a. (Typeable f, Typeable a) => Var a -> EnvF f -> Maybe (f a) +lookup = \var (EnvF env) -> + asum $ map (\(EnvEntry var' fa') -> aux var var' fa') env + where + aux :: Typeable a' => Var a -> Var a' -> f a' -> Maybe (f a) + aux (Var x) (Var y) fa' = do + guard (x == y) + cast fa' + +keysOfType :: Typeable a => EnvF f -> [Var a] +keysOfType (EnvF env) = mapMaybe (\(EnvEntry var _) -> cast var) env diff --git a/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs b/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | Generalized variables +-- +-- Intended for unqualified import. +module Test.QuickCheck.StateModel.Lockstep.GVar ( + GVar -- opaque + , AnyGVar(..) + -- * Construction + , fromVar + , mapGVar + -- * Interop with 'Env' + , lookUpGVar + -- * Interop with 'EnvF' + , lookUpEnvF + , definedInEnvF + ) where + +import Prelude hiding (map) + +import Data.Maybe (isJust, fromJust) +import Data.Typeable + +import Test.QuickCheck.StateModel (Var(..), LookUp, Realized) + +import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF) +import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF +import Test.QuickCheck.StateModel.Lockstep.Op + +{------------------------------------------------------------------------------- + Main type +-------------------------------------------------------------------------------} + +-- | Generalized variables +-- +-- The key difference between 'GVar' and the standard 'Var' type is that +-- 'GVar' have a functor-esque structure: see 'map'. +data GVar op f where + GVar :: Typeable x => Var x -> op x y -> GVar op y + +data AnyGVar op where + SomeGVar :: GVar op y -> AnyGVar op + +deriving instance (forall x. Show (op x a)) => Show (GVar op a) + +instance (forall x. Eq (op x a)) => Eq (GVar op a) where + (==) = \(GVar x op) (GVar x' op') -> aux x x' op op' + where + aux :: forall x x'. + (Typeable x, Typeable x') + => Var x -> Var x' -> op x a -> op x' a -> Bool + aux x x' op op' = + case eqT @x @x' of + Nothing -> False + Just Refl -> (x, op) == (x', op') + +{------------------------------------------------------------------------------- + Construction +-------------------------------------------------------------------------------} + +fromVar :: (Operation op, Typeable a) => Var a -> GVar op a +fromVar var = GVar var opIdentity + +mapGVar :: (forall x. op x a -> op x b) -> GVar op a -> GVar op b +mapGVar f (GVar var op) = GVar var (f op) + +{------------------------------------------------------------------------------- + Interop with 'Env' +-------------------------------------------------------------------------------} + +lookUpWrapped :: Typeable a => Proxy m -> LookUp m -> Var a -> WrapRealized m a +lookUpWrapped _ m v = WrapRealized (m v) + +-- | Lookup 'GVar' given a lookup function for 'Var' +-- +-- The variable must be in the environment and evaluation must succeed. +-- This is normally guaranteed by the default test 'precondition'. +lookUpGVar :: + InterpretOp op (WrapRealized m) + => Proxy m -> LookUp m -> GVar op a -> Realized m a +lookUpGVar p lookUp (GVar var op) = + unwrapRealized $ fromJust $ intOp op (lookUpWrapped p lookUp var) + +{------------------------------------------------------------------------------- + Interop with EnvF +-------------------------------------------------------------------------------} + +-- | Lookup 'GVar' +-- +-- The variable must be in the environment and evaluation must succeed. +-- This is normally guaranteed by the default test 'precondition'. +lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> f a +lookUpEnvF env (GVar var op) = fromJust $ + EnvF.lookup var env >>= intOp op + +-- | Check if the variable is well-defined and evaluation will succeed. +definedInEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Bool +definedInEnvF env (GVar var op) = isJust $ + EnvF.lookup var env >>= intOp op diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Op.hs b/src/Test/QuickCheck/StateModel/Lockstep/Op.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/Op.hs @@ -0,0 +1,46 @@ +module Test.QuickCheck.StateModel.Lockstep.Op ( + Operation(..) + , InterpretOp(..) + , WrapRealized(..) + , intOpRealizedId + ) where + +import Test.QuickCheck.StateModel (Realized) +import Data.Coerce + +{------------------------------------------------------------------------------- + Operations + + This is basically reified functions. We reify them for two reasons: + + 1. It means we can define proper Show/Eq instances for 'GVar' + 2. It allows us to give separate interpretations of 'Op' for mock values + and for real values. +-------------------------------------------------------------------------------} + +class Operation op where + opIdentity :: op a a + +class Operation op => InterpretOp op f where + intOp :: op a b -> f a -> Maybe (f b) + +{------------------------------------------------------------------------------- + Interop with 'Realized' + + We want to execute operations against 'Realized' values, but since that is + a newtype, we need to wrap and unwrap in order to be able to give the + appropriate 'InterpretOp' instances. +-------------------------------------------------------------------------------} + +newtype WrapRealized m a = WrapRealized { + unwrapRealized :: Realized m a + } + +-- | Convenience function for defining 'InterpretOp' instances +-- +-- This can be used for monads like @IO@ where @Realized m a@ is just @a@. +intOpRealizedId :: + (Realized m a ~ a, Realized m b ~ b) + => (op a b -> a -> Maybe b) + -> op a b -> WrapRealized m a -> Maybe (WrapRealized m b) +intOpRealizedId = coerce diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Op/Identity.hs b/src/Test/QuickCheck/StateModel/Lockstep/Op/Identity.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/Op/Identity.hs @@ -0,0 +1,18 @@ +module Test.QuickCheck.StateModel.Lockstep.Op.Identity (Op(..)) where + +import Test.QuickCheck.StateModel.Lockstep.Op + +-- | Very simple operation type that supports identity only +-- +-- This can be used by tests that don't need to map over variables. That is, +-- where variables always refer to the /exact/ result of previously executed +-- commands. Such tests will not need to define any 'InterpretOp' instances. +data Op a b where + OpId :: Op a a + +deriving instance Show (Op a b) +deriving instance Eq (Op a b) + +instance Operation Op where opIdentity = OpId +instance InterpretOp Op f where intOp OpId = Just + diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs b/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE TypeOperators #-} +module Test.QuickCheck.StateModel.Lockstep.Op.SumProd (Op(..)) where + +import Control.Monad.Reader (ReaderT) +import Control.Monad.State +import GHC.Show (appPrec) + +import Test.QuickCheck.StateModel.Lockstep.Op + +{------------------------------------------------------------------------------- + Example (but very useful) 'Operation' example + + Because this is designed for testing where we want everything to be 'Show'able + and 'Typeable', matching on 'Op' might reveal some additonal constrants. + This is useful in 'OpComp' where we have an existential variable (@b@), but + it's also useful for example in 'OpRight': the caller might have a constraint + @Show (Either a b)@, but that doesn't give them a way to obtain a constraint + @Show a@; the implication only goes one way. + + (These are the same constraints that 'Any' imposes.) +-------------------------------------------------------------------------------} + +-- | Operations with support for products (pairs) and sums ('Either') +data Op a b where + OpId :: Op a a + OpFst :: Op (a, b) a + OpSnd :: Op (b, a) a + OpLeft :: Op (Either a b) a + OpRight :: Op (Either b a) a + OpComp :: Op b c -> Op a b -> Op a c + +intOpId :: Op a b -> a -> Maybe b +intOpId OpId = Just +intOpId OpFst = Just . fst +intOpId OpSnd = Just . snd +intOpId OpLeft = either Just (const Nothing) +intOpId OpRight = either (const Nothing) Just +intOpId (OpComp g f) = intOpId g <=< intOpId f + +{------------------------------------------------------------------------------- + 'InterpretOp' instances +-------------------------------------------------------------------------------} + +instance Operation Op where + opIdentity = OpId + +instance InterpretOp Op (WrapRealized IO) where + intOp = intOpRealizedId intOpId + +instance InterpretOp Op (WrapRealized (ReaderT r IO)) where + intOp = intOpRealizedId intOpId + +instance InterpretOp Op (WrapRealized (StateT s IO)) where + intOp = intOpRealizedId intOpId + +{------------------------------------------------------------------------------- + 'Show' and 'Eq' instances +-------------------------------------------------------------------------------} + +sameOp :: Op a b -> Op c d -> Bool +sameOp = go + where + go :: Op a b -> Op c d -> Bool + go OpId OpId = True + go OpFst OpFst = True + go OpSnd OpSnd = True + go OpLeft OpLeft = True + go OpRight OpRight = True + go (OpComp g f) (OpComp g' f') = go g g' && go f f' + go _ _ = False + + _coveredAllCases :: Op a b -> () + _coveredAllCases = \case + OpId -> () + OpFst -> () + OpSnd -> () + OpLeft -> () + OpRight -> () + OpComp{} -> () + +instance Eq (Op a b) where + (==) = sameOp + +instance Show (Op a b) where + showsPrec p = \op -> case op of + OpComp{} -> showParen (p > appPrec) (go op) + _ -> go op + where + go :: Op x y -> String -> String + go OpId = showString "id" + go OpFst = showString "fst" + go OpSnd = showString "snd" + go OpLeft = showString "fromLeft" + go OpRight = showString "fromRight" + go (OpComp g f) = go g . showString " . " . go f + diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Run.hs b/src/Test/QuickCheck/StateModel/Lockstep/Run.hs new file mode 100644 --- /dev/null +++ b/src/Test/QuickCheck/StateModel/Lockstep/Run.hs @@ -0,0 +1,135 @@ +-- | Run lockstep tests +-- +-- Intended for qualified import. +-- +-- > import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep +module Test.QuickCheck.StateModel.Lockstep.Run ( + -- * Finding labelled examples + tagActions + -- * Run tests + , runActions + , runActionsBracket + ) where + +import Prelude hiding (init) + +import Control.Exception +import Control.Monad.Reader +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Typeable +import Test.QuickCheck.Monadic + +import Test.QuickCheck (Property, Testable) +import Test.QuickCheck qualified as QC +import Test.QuickCheck.StateModel hiding (runActions) +import Test.QuickCheck.StateModel qualified as StateModel + +import Test.QuickCheck.StateModel.Lockstep.API +import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF +import Test.QuickCheck.StateModel.Lockstep.GVar + +{------------------------------------------------------------------------------- + Finding labelled examples + + Implementation note: the 'monitoring' hook from 'StateModel' cannot be used + for finding labelled examples. This hook is called many times during test + execution (once per action); this means that we cannot call 'label' inside + 'monitoring', but must instead use 'tabulate'. However, 'tabulate' is not + supported by 'labelledExamples'. In 'tagActions' we therefore run over all + actions, collecting tags as we go, and then do a /single/ call to 'label' + at the end. +-------------------------------------------------------------------------------} + +-- | Tag a list of actions +-- +-- This can be used together with QuickCheck's 'labelledExamples' to test your +-- tagging code as well as your shrinker (QuickCheck will try to produce +-- /minimal/ labelled examples). +-- +-- Unlike 'runActions', this does not require a 'RunModel' instance; this is +-- executed against the model /only/. +tagActions :: forall state. + InLockstep state + => Proxy state + -> Actions (Lockstep state) + -> Property +tagActions _p (Actions steps) = + go Set.empty Test.QuickCheck.StateModel.initialState steps + where + go :: Set String -> Lockstep state -> [Step (Lockstep state)] -> Property + go tags _st [] = QC.label ("Tags: " ++ show (Set.toList tags)) True + go tags st ((v:=a) : ss) = go' tags st v a ss + + go' :: forall a. + Typeable a + => Set String -- accumulated set of tags + -> Lockstep state -- current state + -> Var a -- variable for the result of this action + -> Action (Lockstep state) a -- action to execute + -> [Step (Lockstep state)] -- remaining steps to execute + -> Property + go' tags (Lockstep before env) var action ss = + go (Set.union (Set.fromList tags') tags) st' ss + where + st' :: Lockstep state + st' = Lockstep after (EnvF.insert var modelResp env) + + modelResp :: ModelValue state a + after :: state + (modelResp, after) = modelNextState action (lookUpEnvF env) before + + tags' :: [String] + tags' = tagStep (before, after) action modelResp + +{------------------------------------------------------------------------------- + Run tests +-------------------------------------------------------------------------------} + +runActions :: + RunLockstep state IO + => Proxy state + -> Actions (Lockstep state) -> Property +runActions _ actions = monadicIO $ void $ StateModel.runActions actions + +-- | Convenience runner with support for state initialization +-- +-- This is less general than 'Test.QuickCheck.StateModel.runActions', but +-- will be useful in many scenarios. +runActionsBracket :: + RunLockstep state (ReaderT st IO) + => Proxy state + -> IO st -- ^ Initialisation + -> (st -> IO ()) -- ^ Cleanup + -> Actions (Lockstep state) -> Property +runActionsBracket _ init cleanup actions = + monadicBracketIO init cleanup $ + void $ StateModel.runActions actions + +{------------------------------------------------------------------------------- + Internal auxiliary +-------------------------------------------------------------------------------} + +ioPropertyBracket :: + Testable a + => IO st + -> (st -> IO ()) + -> ReaderT st IO a + -> Property +ioPropertyBracket init cleanup (ReaderT prop) = do + QC.ioProperty $ mask $ \restore -> do + st <- init + a <- restore (prop st) `onException` cleanup st + cleanup st + return a + +-- | Variation on 'monadicIO' that allows for state initialisation/cleanup +monadicBracketIO :: forall st a. + Testable a + => IO st + -> (st -> IO ()) + -> (PropertyM (ReaderT st IO) a) + -> Property +monadicBracketIO init cleanup = + monadic (ioPropertyBracket init cleanup) + diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,12 @@ +module Main (main) where + +import Test.Tasty + +import Test.IORef qualified +import Test.MockFS qualified + +main :: IO () +main = defaultMain $ testGroup "quickcheck-lockstep" [ + Test.IORef.tests + , Test.MockFS.tests + ] diff --git a/test/Test/IORef.hs b/test/Test/IORef.hs new file mode 100644 --- /dev/null +++ b/test/Test/IORef.hs @@ -0,0 +1,162 @@ +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.IORef (tests) where + +import Data.Bifunctor +import Data.IORef +import Data.Map (Map) +import Data.Map qualified as Map +import Data.Proxy +import Test.QuickCheck +import Test.Tasty +import Test.Tasty.QuickCheck (testProperty) + +import Test.QuickCheck.StateModel +import Test.QuickCheck.StateModel.Lockstep +import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep +import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep + +{------------------------------------------------------------------------------- + Model "M" +-------------------------------------------------------------------------------} + +type MRef = Int +type M = Map MRef Int + +initModel :: M +initModel = Map.empty + +modelNew :: M -> (MRef, M) +modelNew m = (mockRef, Map.insert mockRef 0 m) + where + mockRef :: MRef + mockRef = Map.size m + +modelWrite :: MRef -> Int -> M -> ((), M) +modelWrite v x m = ((), Map.insert v x m) + +modelRead :: MRef -> M -> (Int, M) +modelRead v m = (m Map.! v, m) + +{------------------------------------------------------------------------------- + Instances +-------------------------------------------------------------------------------} + +instance StateModel (Lockstep M) where + data Action (Lockstep M) a where + -- | Create new IORef + New :: Action (Lockstep M) (IORef Int) + + -- | Write value to IORef + Write :: + ModelVar M (IORef Int) + -> Int + -> Action (Lockstep M) () + + -- | Read IORef + Read :: + ModelVar M (IORef Int) + -> Action (Lockstep M) Int + + initialState = Lockstep.initialState initModel + nextState = Lockstep.nextState + precondition = Lockstep.precondition + arbitraryAction = Lockstep.arbitraryAction + shrinkAction = Lockstep.shrinkAction + +instance RunModel (Lockstep M) IO where + perform = \_state -> runIO + postcondition = Lockstep.postcondition + monitoring = Lockstep.monitoring (Proxy @IO) + +instance InLockstep M where + data ModelValue M a where + MRef :: MRef -> ModelValue M (IORef Int) + MUnit :: () -> ModelValue M () + MInt :: Int -> ModelValue M Int + + data Observable M a where + ORef :: Observable M (IORef Int) + OId :: (Show a, Eq a) => a -> Observable M a + + observeModel (MRef _) = ORef + observeModel (MUnit x) = OId x + observeModel (MInt x) = OId x + + usedVars New = [] + usedVars (Write v _) = [SomeGVar v] + usedVars (Read v) = [SomeGVar v] + + modelNextState = runModel + + arbitraryWithVars findVars _mock = oneof $ concat [ + withoutVars + , case findVars (Proxy @(IORef Int)) of + [] -> [] + vars -> withVars (elements vars) + ] + where + withoutVars :: [Gen (Any (LockstepAction M))] + withoutVars = [return $ Some New] + + withVars :: + Gen (ModelVar M (IORef Int)) + -> [Gen (Any (LockstepAction M))] + withVars genVar = [ + fmap Some $ Write <$> genVar <*> arbitrary + , fmap Some $ Read <$> genVar + ] + +instance RunLockstep M IO where + observeReal _ action result = + case (action, result) of + (New , _) -> ORef + (Write{} , x) -> OId x + (Read{} , x) -> OId x + +deriving instance Show (Action (Lockstep M) a) +deriving instance Show (Observable M a) +deriving instance Show (ModelValue M a) + +deriving instance Eq (Action (Lockstep M) a) +deriving instance Eq (Observable M a) +deriving instance Eq (ModelValue M a) + +{------------------------------------------------------------------------------- + Interpreters against the real system and against the model +-------------------------------------------------------------------------------} + +runIO :: Action (Lockstep M) a -> LookUp IO -> IO a +runIO action lookUp = + case action of + New -> newIORef 0 + Write v x -> writeIORef (lookUpRef v) x + Read v -> readIORef (lookUpRef v) + where + lookUpRef :: ModelVar M (IORef Int) -> IORef Int + lookUpRef = lookUpGVar (Proxy @IO) lookUp + +runModel :: + Action (Lockstep M) a + -> ModelLookUp M + -> M -> (ModelValue M a, M) +runModel action lookUp = + case action of + New -> first MRef . modelNew + Write v x -> first MUnit . modelWrite (lookUpRef v) x + Read v -> first MInt . modelRead (lookUpRef v) + where + lookUpRef :: ModelVar M (IORef Int) -> MRef + lookUpRef var = case lookUp var of MRef r -> r + +{------------------------------------------------------------------------------- + Top-level tests +-------------------------------------------------------------------------------} + +propIORef :: Actions (Lockstep M) -> Property +propIORef = Lockstep.runActions (Proxy @M) + +tests :: TestTree +tests = testGroup "Test.IORef" [ + testProperty "runActions" propIORef + ] diff --git a/test/Test/MockFS.hs b/test/Test/MockFS.hs new file mode 100644 --- /dev/null +++ b/test/Test/MockFS.hs @@ -0,0 +1,376 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +module Test.MockFS (tests) where + +import Prelude hiding (init) + +import Control.Exception (catch, throwIO) +import Control.Monad +import Control.Monad.Reader +import Data.Bifunctor +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Typeable +import System.Directory (removeDirectoryRecursive) +import System.Directory qualified as IO +import System.IO qualified as IO +import System.IO.Temp (createTempDirectory) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit +import Test.Tasty.QuickCheck (testProperty) + +import Test.QuickCheck (Gen) +import Test.QuickCheck qualified as QC +import Test.QuickCheck.StateModel + +import Test.QuickCheck.StateModel.Lockstep +import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep +import Test.QuickCheck.StateModel.Lockstep.Op.SumProd +import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep + +import Test.MockFS.Mock (Mock, Dir(..), File(..), Err) +import Test.MockFS.Mock qualified as Mock + +{------------------------------------------------------------------------------- + Model state +-------------------------------------------------------------------------------} + +data FsState = FsState { + fsStateMock :: Mock + , fsStateStats :: Stats + } + deriving (Show) + +initState :: FsState +initState = FsState { + fsStateMock = Mock.emptyMock + , fsStateStats = initStats + } + +{------------------------------------------------------------------------------- + StateModel and 'RunModel' instances +-------------------------------------------------------------------------------} + +type RealMonad = ReaderT FilePath IO + +type FsVar a = ModelVar FsState a +type FsAct a = Action (Lockstep FsState) (Either Err a) + +instance StateModel (Lockstep FsState) where + data Action (Lockstep FsState) a where + MkDir :: Dir -> FsAct () + Open :: File -> FsAct (IO.Handle, File) + Write :: FsVar IO.Handle -> String -> FsAct () + Close :: FsVar IO.Handle -> FsAct () + Read :: Either (FsVar File) File -> FsAct String + + initialState = Lockstep.initialState initState + nextState = Lockstep.nextState + precondition = Lockstep.precondition + arbitraryAction = Lockstep.arbitraryAction + shrinkAction = Lockstep.shrinkAction + +instance RunModel (Lockstep FsState) RealMonad where + perform = \_st -> runIO + postcondition = Lockstep.postcondition + monitoring = Lockstep.monitoring (Proxy @RealMonad) + +deriving instance Show (Action (Lockstep FsState) a) +deriving instance Eq (Action (Lockstep FsState) a) + +{------------------------------------------------------------------------------- + InLockstep instance +-------------------------------------------------------------------------------} + +type FsVal a = ModelValue FsState a +type FsObs a = Observable FsState a + +instance InLockstep FsState where + + -- + -- Model values + -- + -- For model values, we must be sure that if we have a value of type + -- + -- > FsVal IO.Handle + -- + -- that it is a in fact mock handle. This means that here we cannot define + -- + -- > ModelId :: a -> FsVal a + -- + -- unlike in 'FsObs'. + + data ModelValue FsState a where + MHandle :: Mock.MHandle -> FsVal IO.Handle + + -- Rest is regular: + + MErr :: Err -> FsVal Err + MFile :: File -> FsVal File + MString :: String -> FsVal String + MUnit :: () -> FsVal () + + MEither :: Either (FsVal a) (FsVal b) -> FsVal (Either a b) + MPair :: (FsVal a, FsVal b) -> FsVal (a, b) + + -- + -- Observable results + -- + + data Observable FsState a where + OHandle :: FsObs IO.Handle + OId :: (Show a, Typeable a, Eq a) => a -> FsObs a + OEither :: Either (FsObs a) (FsObs b) -> FsObs (Either a b) + OPair :: (FsObs a, FsObs b) -> FsObs (a, b) + + observeModel :: FsVal a -> FsObs a + observeModel = \case + MEither x -> OEither $ bimap observeModel observeModel x + MPair x -> OPair $ bimap observeModel observeModel x + MErr x -> OId x + MString x -> OId x + MUnit x -> OId x + MFile x -> OId x + MHandle _ -> OHandle + + -- + -- Semantics + -- + + modelNextState :: forall a. + LockstepAction FsState a + -> ModelLookUp FsState + -> FsState -> (FsVal a, FsState) + modelNextState action lookUp (FsState mock stats) = + auxStats $ runMock lookUp action mock + where + auxStats :: (FsVal a, Mock) -> (FsVal a, FsState) + auxStats (result, state') = + (result, FsState state' $ updateStats action result stats) + + -- + -- Variables + -- + + type ModelOp FsState = Op + + usedVars :: LockstepAction FsState a -> [AnyGVar (ModelOp FsState)] + usedVars = \case + MkDir{} -> [] + Open{} -> [] + Write h _ -> [SomeGVar h] + Close h -> [SomeGVar h] + Read (Left h) -> [SomeGVar h] + Read (Right _) -> [] + + -- + -- Generation, shrinking and labelling + -- + + arbitraryWithVars findVars _mock = arbitraryFsAction findVars + shrinkWithVars findVars _mock = shrinkFsAction findVars + + tagStep (_, FsState _ after) act = map show . tagFsAction after act + +deriving instance Show (Observable FsState a) +deriving instance Eq (Observable FsState a) + +deriving instance Show (FsVal a) + +{------------------------------------------------------------------------------- + RunLockstep instance +-------------------------------------------------------------------------------} + +instance RunLockstep FsState RealMonad where + observeReal :: + Proxy RealMonad + -> LockstepAction FsState a -> Realized RealMonad a -> FsObs a + observeReal _ = \case + MkDir{} -> OEither . bimap OId OId + Open{} -> OEither . bimap OId (OPair . bimap (const OHandle) OId) + Write{} -> OEither . bimap OId OId + Close{} -> OEither . bimap OId OId + Read{} -> OEither . bimap OId OId + +{------------------------------------------------------------------------------- + Interpreter against the model +-------------------------------------------------------------------------------} + +runMock :: + ModelLookUp FsState + -> Action (Lockstep FsState) a + -> Mock -> (FsVal a, Mock) +runMock lookUp = \case + MkDir d -> wrap MUnit . Mock.mMkDir d + Open f -> wrap (mOpen f) . Mock.mOpen f + Write h s -> wrap MUnit . Mock.mWrite (getHandle $ lookUp h) s + Close h -> wrap MUnit . Mock.mClose (getHandle $ lookUp h) + Read f -> wrap MString . Mock.mRead (either (getFile . lookUp) id f) + where + wrap :: (a -> FsVal b) -> (Either Err a, Mock) -> (FsVal (Either Err b), Mock) + wrap f = first (MEither . bimap MErr f) + + mOpen :: File -> Mock.MHandle -> FsVal (IO.Handle, File) + mOpen f h = MPair (MHandle h, MFile f) + + getHandle :: ModelValue FsState IO.Handle -> Mock.MHandle + getFile :: ModelValue FsState File -> File + + getHandle (MHandle h) = h + getFile (MFile f) = f + +{------------------------------------------------------------------------------- + Generator and shrinking +-------------------------------------------------------------------------------} + +arbitraryFsAction :: + ModelFindVariables FsState + -> Gen (Any (LockstepAction FsState)) +arbitraryFsAction findVars = QC.oneof $ concat [ + withoutVars + , case findVars (Proxy @((Either Err (IO.Handle, File)))) of + [] -> [] + vars -> withVars (QC.elements vars) + ] + where + withoutVars :: [Gen (Any (LockstepAction FsState))] + withoutVars = [ + fmap Some $ MkDir <$> genDir + , fmap Some $ Open <$> genFile + , fmap Some $ Read <$> (Right <$> genFile) + ] + + withVars :: + Gen (FsVar (Either Err (IO.Handle, File))) + -> [Gen (Any (LockstepAction FsState))] + withVars genVar = [ + fmap Some $ Write <$> (handle <$> genVar) <*> genString + , fmap Some $ Close <$> (handle <$> genVar) + ] + where + handle :: GVar Op (Either Err (IO.Handle, File)) -> GVar Op IO.Handle + handle = mapGVar (\op -> OpFst `OpComp` OpRight `OpComp` op) + + genDir :: Gen Dir + genDir = do + n <- QC.choose (0, 3) + Dir <$> replicateM n (QC.elements ["x", "y", "z"]) + + genFile :: Gen File + genFile = File <$> genDir <*> QC.elements ["a", "b", "c"] + + genString :: Gen String + genString = QC.sized $ \n -> replicateM n (QC.elements "ABC") + +shrinkFsAction :: + ModelFindVariables FsState + -> Action (Lockstep FsState) a -> [Any (LockstepAction FsState)] +shrinkFsAction findVars = \case + Open (File (Dir []) ('t' : n)) -> + [openTemp n' | n' <- QC.shrink (read n)] + Open _ -> + [openTemp 100] + Read (Right _) -> + [ Some $ Read (Left $ mapGVar (\op -> OpSnd `OpComp` OpRight `OpComp` op) v) + | v <- findVars (Proxy @((Either Err (IO.Handle, File)))) + ] + _otherwise -> + [] + where + openTemp :: Int -> Any (LockstepAction FsState) + openTemp n = Some $ Open (File (Dir []) ('t' : show n)) + +{------------------------------------------------------------------------------- + Interpret 'Op' against 'ModelValue' +-------------------------------------------------------------------------------} + +instance InterpretOp Op (ModelValue FsState) where + intOp OpId = Just + intOp OpFst = \case MPair x -> Just (fst x) + intOp OpSnd = \case MPair x -> Just (snd x) + intOp OpLeft = \case MEither x -> either Just (const Nothing) x + intOp OpRight = \case MEither x -> either (const Nothing) Just x + intOp (OpComp g f) = intOp g <=< intOp f + +{------------------------------------------------------------------------------- + Interpreter for IO +-------------------------------------------------------------------------------} + +runIO :: LockstepAction FsState a -> LookUp RealMonad -> RealMonad (Realized RealMonad a) +runIO action lookUp = ReaderT $ \root -> aux root action + where + aux :: FilePath -> LockstepAction FsState a -> IO a + aux root = \case + MkDir d -> catchErr $ + IO.createDirectory (Mock.dirFP root d) + Open f -> catchErr $ + (,f) <$> IO.openFile (Mock.fileFP root f) IO.AppendMode + Write h s -> catchErr $ + IO.hPutStr (lookUp' h) s + Close h -> catchErr $ + IO.hClose (lookUp' h) + Read f -> catchErr $ + IO.readFile (Mock.fileFP root $ either lookUp' id f) + where + lookUp' :: FsVar x -> x + lookUp' = lookUpGVar (Proxy @RealMonad) lookUp + +catchErr :: forall a. IO a -> IO (Either Err a) +catchErr act = catch (Right <$> act) handler + where + handler :: IOError -> IO (Either Err h) + handler e = maybe (throwIO e) (return . Left) (Mock.fromIOError e) + +{------------------------------------------------------------------------------- + Statistics and tagging +-------------------------------------------------------------------------------} + +-- The only statistics we need to track for this example is the files we opened +type Stats = Set File + +initStats :: Stats +initStats = Set.empty + +updateStats :: LockstepAction FsState a -> FsVal a -> Stats -> Stats +updateStats action result = + case (action, result) of + (Open f, MEither (Right _)) -> Set.insert f + _otherwise -> id + +data Tag = OpenTwo | SuccessfulRead + deriving (Show) + +tagFsAction :: Stats -> LockstepAction FsState a -> FsVal a -> [Tag] +tagFsAction openedFiles = \case + Read _ -> \v -> [SuccessfulRead | MEither (Right _) <- [v]] + Open _ -> \_ -> [OpenTwo | Set.size openedFiles >= 2] + _ -> \_ -> [] + +{------------------------------------------------------------------------------- + Top-level test +-------------------------------------------------------------------------------} + +tests :: TestTree +tests = testGroup "Test.MockFS" [ + testCase "labelledExamples" $ + QC.labelledExamples $ Lockstep.tagActions (Proxy @FsState) + , testProperty "propLockstep" $ + Lockstep.runActionsBracket (Proxy @FsState) + (createTempDirectory tmpDir "QSM") + removeDirectoryRecursive + ] + where + -- TODO: tmpDir should really be a parameter to the test suite + tmpDir :: FilePath + tmpDir = "./tmp" diff --git a/test/Test/MockFS/Mock.hs b/test/Test/MockFS/Mock.hs new file mode 100644 --- /dev/null +++ b/test/Test/MockFS/Mock.hs @@ -0,0 +1,124 @@ +module Test.MockFS.Mock ( + -- * Paths + Dir(..) + , File(..) + , dirFP + , fileFP + -- * Errors + , Err(..) + , fromIOError + -- * Mock file system + , MHandle + , Mock(..) + , emptyMock + , mMkDir + , mOpen + , mWrite + , mClose + , mRead + ) where + +import Data.List qualified as List +import Data.Map (Map) +import Data.Map qualified as Map +import Data.Set (Set) +import Data.Set qualified as Set +import GHC.Generics (Generic) +import GHC.IO.Exception qualified as GHC +import System.FilePath (()) +import System.IO.Error + +{------------------------------------------------------------------------------- + Paths +-------------------------------------------------------------------------------} + +data Dir = Dir [String] + deriving (Show, Eq, Ord, Generic) + +parent :: Dir -> Dir +parent (Dir fp) = Dir (init fp) + +data File = File {dir :: Dir, name :: String} + deriving (Show, Eq, Ord, Generic) + +dirFP :: FilePath -> Dir -> FilePath +dirFP root (Dir d) = List.foldl' () root d + +fileFP :: FilePath -> File -> FilePath +fileFP root (File d f) = dirFP root d f + +{------------------------------------------------------------------------------- + Errors +-------------------------------------------------------------------------------} + +data Err = + AlreadyExists + | DoesNotExist + | HandleClosed + | Busy + deriving (Show, Eq) + + +fromIOError :: IOError -> Maybe Err +fromIOError e = + case ioeGetErrorType e of + GHC.AlreadyExists -> Just AlreadyExists + GHC.NoSuchThing -> Just DoesNotExist + GHC.ResourceBusy -> Just Busy + GHC.IllegalOperation -> Just HandleClosed + _otherwise -> Nothing + +{------------------------------------------------------------------------------- + Mock implementation +-------------------------------------------------------------------------------} + +type MHandle = Int + +data Mock = M { + dirs :: Set Dir + , files :: Map File String + , open :: Map MHandle File + , next :: MHandle + } + deriving (Show, Generic) + +emptyMock :: Mock +emptyMock = M (Set.singleton (Dir [])) Map.empty Map.empty 0 + +type MockOp a = Mock -> (Either Err a, Mock) + +mMkDir :: Dir -> MockOp () +mMkDir d m@(M ds fs hs n) + | d `Set.member` ds = (Left AlreadyExists, m) + | parent d `Set.notMember` ds = (Left DoesNotExist, m) + | otherwise = (Right (), M (Set.insert d ds) fs hs n) + +mOpen :: File -> MockOp MHandle +mOpen f m@(M ds fs hs n) + | alreadyOpen = (Left Busy, m) + | not dirExists = (Left DoesNotExist, m) + | fileExists = (Right n, M ds fs hs' n') + | otherwise = (Right n, M ds (Map.insert f "" fs) hs' n') + where + hs' = Map.insert n f hs + n' = succ n + + fileExists = f `Map.member` fs + dirExists = dir f `Set.member` ds + alreadyOpen = f `List.elem` Map.elems hs + +mWrite :: MHandle -> String -> MockOp () +mWrite h s m@(M ds fs hs n) + | Just f <- Map.lookup h hs = (Right (), M ds (Map.adjust (++ s) f fs) hs n) + | otherwise = (Left HandleClosed, m) + +mClose :: MHandle -> MockOp () +mClose h (M ds fs hs n) = (Right (), M ds fs (Map.delete h hs) n) + +mRead :: File -> MockOp String +mRead f m@(M _ fs hs _) + | alreadyOpen = (Left Busy , m) + | Just s <- Map.lookup f fs = (Right s , m) + | otherwise = (Left DoesNotExist , m) + where + alreadyOpen = f `List.elem` Map.elems hs