diff --git a/cabal.project.release b/cabal.project.release index 4c3460cdd..bd7b30293 100644 --- a/cabal.project.release +++ b/cabal.project.release @@ -43,8 +43,8 @@ source-repository-package fs-api fs-sim --- quickcheck-lockstep with more verbose counterexamples +-- quickcheck-lockstep with shrinking for variables source-repository-package type: git location: https://github.com/well-typed/quickcheck-lockstep - tag: 845cd66d03d0410618c660dbcb21f58f66cf0931 + tag: b511080f0344ba788bb3af2fb834a41c74af4ded diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index 33abf8688..8ced00c7f 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -75,7 +75,6 @@ import Control.ActionRegistry (AbortActionRegistryError (..), import Control.Applicative (Alternative (..)) import Control.Concurrent.Class.MonadMVar.Strict import Control.Concurrent.Class.MonadSTM.Strict -import Control.Exception (assert) import qualified Control.Exception import Control.Monad (forM_, void, (<=<)) import Control.Monad.Class.MonadST @@ -92,6 +91,7 @@ import Control.Tracer (Tracer, nullTracer) import Data.Bifunctor (Bifunctor (..)) import Data.Constraint (Dict (..)) import Data.Either (partitionEithers) +import Data.Function ((&)) import Data.Kind (Type) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE @@ -132,23 +132,26 @@ import System.FS.Sim.MockFS (MockFS) import System.FS.Sim.Stream (Stream) import System.IO.Temp (createTempDirectory, getCanonicalTemporaryDirectory) -import Test.Database.LSMTree.StateMachine.Op (HasBlobRef (getBlobRef), - Op (..)) +import qualified Test.Database.LSMTree.StateMachine.Op as Op +import Test.Database.LSMTree.StateMachine.Op (Dep (..), + HasBlobRef (..), Op (..)) import qualified Test.QuickCheck as QC import Test.QuickCheck (Arbitrary, Gen, Property) import qualified Test.QuickCheck.Extras as QD import qualified Test.QuickCheck.Monadic as QC import Test.QuickCheck.Monadic (PropertyM) import qualified Test.QuickCheck.StateModel as QD -import Test.QuickCheck.StateModel hiding (Var) +import Test.QuickCheck.StateModel hiding (Var, shrinkVar) import Test.QuickCheck.StateModel.Lockstep import qualified Test.QuickCheck.StateModel.Lockstep.Defaults as Lockstep.Defaults +import qualified Test.QuickCheck.StateModel.Lockstep.Op as Op import qualified Test.QuickCheck.StateModel.Lockstep.Run as Lockstep.Run import Test.Tasty (TestTree, testGroup, withResource) import Test.Tasty.QuickCheck (testProperty) import Test.Util.FS (approximateEqStream, noRemoveDirectoryRecursiveE, propNoOpenHandles, propNumOpenHandles) import Test.Util.FS.Error +import Test.Util.Orphans () import Test.Util.PrettyProxy import Test.Util.QC (Choice) import qualified Test.Util.QLS as QLS @@ -670,6 +673,31 @@ type B a = ( -- | Common constraints for keys, values and blobs type C k v b = (K k, V v, B b) +{------------------------------------------------------------------------------- + Dependent shrinking +-------------------------------------------------------------------------------} + +type DepVar h a = Op.DepVar (ModelState h) a + +getDepVar :: forall h a. Proxy h -> DepVar h a -> Var h a +getDepVar _ = Op.getDepVar (Proxy @(ModelState h)) + +lookupDepVar :: forall h m a. + InterpretOp Op (Op.WrapRealized m) + => Proxy m + -> Proxy h + -> LookUp (RealMonad h m) + -> DepVar h a + -> Realized (RealMonad h m) a +lookupDepVar _ _ = Op.lookupDepVar (Proxy @(RealMonad h m)) (Proxy @(ModelState h)) + +shrinkDepVar :: + ModelVarContext (ModelState h) + -> [GVar Op (Dep a)] + -> DepVar h a + -> [DepVar h a] +shrinkDepVar = Op.shrinkDepVar + {------------------------------------------------------------------------------- StateModel -------------------------------------------------------------------------------} @@ -733,7 +761,7 @@ data Action' h a where NewCursor :: C k v b => Maybe k - -> Var h (WrapTable h IO k v b) + -> DepVar h (WrapTable h IO k v b) -> Act' h (WrapCursor h IO k v b) CloseCursor :: C k v b @@ -747,8 +775,9 @@ data Action' h a where -- Updates Updates :: C k v b - => V.Vector (k, R.Update v b) -> Var h (WrapTable h IO k v b) - -> Act' h () + => DepVar h (WrapTable h IO k v b) + -> V.Vector (k, R.Update v b) + -> Act' h (Dep (WrapTable h IO k v b)) Inserts :: C k v b => V.Vector (k, v, Maybe b) -> Var h (WrapTable h IO k v b) @@ -898,6 +927,8 @@ instance ( Eq (Class.TableConfig h) MBlobRef :: Class.C_ b => Model.BlobRef b -> Val h (WrapBlobRef h IO b) + MDep :: Dep (Val h a) -> Val h (Dep a) + MLookupResult :: (Class.C_ v, Class.C_ b) => LookupResult v (Val h (WrapBlobRef h IO b)) -> Val h (LookupResult v (WrapBlobRef h IO b)) @@ -921,12 +952,15 @@ instance ( Eq (Class.TableConfig h) OCursor :: Obs h (WrapCursor h IO k v b) OBlobRef :: Obs h (WrapBlobRef h IO b) + ODep :: Dep (Obs h a) -> Obs h (Dep a) + OLookupResult :: (Class.C_ v, Class.C_ b) => LookupResult v (Obs h (WrapBlobRef h IO b)) -> Obs h (LookupResult v (WrapBlobRef h IO b)) OQueryResult :: Class.C k v b => QueryResult k v (Obs h (WrapBlobRef h IO b)) -> Obs h (QueryResult k v (WrapBlobRef h IO b)) + OBlob :: (Show b, Typeable b, Eq b) => WrapBlob b -> Obs h (WrapBlob b) @@ -939,9 +973,10 @@ instance ( Eq (Class.TableConfig h) observeModel :: Val h a -> Obs h a observeModel = \case - MTable _ -> OTable + MTable _ -> OTable MCursor _ -> OCursor MBlobRef _ -> OBlobRef + MDep x -> ODep $ fmap observeModel x MLookupResult x -> OLookupResult $ fmap observeModel x MQueryResult x -> OQueryResult $ fmap observeModel x MSnapshotName x -> OId x @@ -972,10 +1007,10 @@ instance ( Eq (Class.TableConfig h) Close tableVar -> [SomeGVar tableVar] Lookups _ tableVar -> [SomeGVar tableVar] RangeLookup _ tableVar -> [SomeGVar tableVar] - NewCursor _ tableVar -> [SomeGVar tableVar] + NewCursor _ tableVar -> [either SomeGVar SomeGVar tableVar] CloseCursor cursorVar -> [SomeGVar cursorVar] ReadCursor _ cursorVar -> [SomeGVar cursorVar] - Updates _ tableVar -> [SomeGVar tableVar] + Updates tableVar _ -> [either SomeGVar SomeGVar tableVar] Inserts _ tableVar -> [SomeGVar tableVar] Deletes _ tableVar -> [SomeGVar tableVar] Mupserts _ tableVar -> [SomeGVar tableVar] @@ -1031,7 +1066,10 @@ instance Eq (Obs h a) where -- See also 'Model.runModelMWithInjectedErrors' and -- 'runRealWithInjectedErrors'. (OEither (Left (OId lhs)), OEither (Left (OId rhs))) - | Just (_ :: Model.Err) <- cast lhs + | Just (e :: Model.Err) <- cast lhs + , case e of + Model.ErrOther _ -> False + _ -> True , Just Model.DefaultErrDiskFault <- cast rhs -> True @@ -1047,6 +1085,7 @@ instance Eq (Obs h a) where (OTable, OTable) -> True (OCursor, OCursor) -> True (OBlobRef, OBlobRef) -> True + (ODep x, ODep y) -> x == y (OLookupResult x, OLookupResult y) -> x == y (OQueryResult x, OQueryResult y) -> x == y (OBlob x, OBlob y) -> x == y @@ -1062,6 +1101,7 @@ instance Eq (Obs h a) where OTable{} -> () OCursor{} -> () OBlobRef{} -> () + ODep{} -> () OLookupResult{} -> () OQueryResult{} -> () OBlob{} -> () @@ -1144,7 +1184,7 @@ instance ( Eq (Class.TableConfig h) CloseCursor{} -> OEither $ bimap OId OId result ReadCursor{} -> OEither $ bimap OId (OVector . fmap (OQueryResult . fmap (const OBlobRef))) result - Updates{} -> OEither $ bimap OId OId result + Updates{} -> OEither $ bimap OId (ODep . Dep . const OTable) result Inserts{} -> OEither $ bimap OId OId result Deletes{} -> OEither $ bimap OId OId result Mupserts{} -> OEither $ bimap OId OId result @@ -1169,7 +1209,7 @@ instance ( Eq (Class.TableConfig h) NewCursor{} -> Nothing CloseCursor{} -> Just Dict ReadCursor{} -> Nothing - Updates{} -> Just Dict + Updates{} -> Nothing Inserts{} -> Just Dict Deletes{} -> Just Dict Mupserts{} -> Just Dict @@ -1204,7 +1244,7 @@ instance ( Eq (Class.TableConfig h) CloseCursor{} -> OEither $ bimap OId OId result ReadCursor{} -> OEither $ bimap OId (OVector . fmap (OQueryResult . fmap (const OBlobRef))) result - Updates{} -> OEither $ bimap OId OId result + Updates{} -> OEither $ bimap OId (ODep . Dep . const OTable) result Inserts{} -> OEither $ bimap OId OId result Deletes{} -> OEither $ bimap OId OId result Mupserts{} -> OEither $ bimap OId OId result @@ -1229,7 +1269,7 @@ instance ( Eq (Class.TableConfig h) NewCursor{} -> Nothing CloseCursor{} -> Just Dict ReadCursor{} -> Nothing - Updates{} -> Just Dict + Updates{} -> Nothing Inserts{} -> Just Dict Deletes{} -> Just Dict Mupserts{} -> Just Dict @@ -1304,7 +1344,7 @@ runModel lookUp (Action merrs action') = case action' of NewCursor offset tableVar -> wrap MCursor . Model.runModelMWithInjectedErrors merrs - (Model.newCursor offset (getTable $ lookUp tableVar)) + (Model.newCursor offset (lookupDepTable tableVar)) (pure ()) -- TODO(err) CloseCursor cursorVar -> wrap MUnit @@ -1316,10 +1356,12 @@ runModel lookUp (Action merrs action') = case action' of . Model.runModelMWithInjectedErrors merrs (Model.readCursor n (getCursor $ lookUp cursorVar)) (pure ()) -- TODO(err) - Updates kups tableVar -> - wrap MUnit + Updates tableVar kups -> + wrap (MDep . Dep . MTable) . Model.runModelMWithInjectedErrors merrs - (Model.updates Model.getResolve kups (getTable $ lookUp tableVar)) + (do let t = lookupDepTable tableVar + Model.updates Model.getResolve kups t + pure t) (pure ()) -- TODO(err) Inserts kins tableVar -> wrap MUnit @@ -1378,11 +1420,24 @@ runModel lookUp (Action merrs action') = case action' of (Model.unions Model.getResolve (fmap (getTable . lookUp) tableVars)) (pure ()) -- TODO(err) where + lookupTable :: + Var h (WrapTable h IO k v b) + -> Model.Table k v b + lookupTable tableVar = lookUp tableVar & \case MTable t -> t + + -- TODO: replace by lookupTable getTable :: ModelValue (ModelState h) (WrapTable h IO k v b) -> Model.Table k v b getTable (MTable t) = t + lookupDepTable :: + DepVar h (WrapTable h IO k v b) + -> Model.Table k v b + lookupDepTable = \case + Left tableVar -> lookupTable tableVar + Right tableVar -> lookUp tableVar & \case MDep (Dep (MTable t)) -> t + getCursor :: ModelValue (ModelState h) (WrapCursor h IO k v b) -> Model.Cursor k v b @@ -1439,7 +1494,7 @@ runIO action lookUp = ReaderT $ \ !env -> do (\_ -> pure ()) -- TODO(err) NewCursor offset tableVar -> runRealWithInjectedErrors "NewCursor" env merrs - (WrapCursor <$> Class.newCursor offset (unwrapTable $ lookUp' tableVar)) + (WrapCursor <$> Class.newCursor offset (lookupDepTable tableVar)) (\_ -> pure ()) -- TODO(err) CloseCursor cursorVar -> runRealWithInjectedErrors "CloseCursor" env merrs @@ -1449,9 +1504,11 @@ runIO action lookUp = ReaderT $ \ !env -> do runRealWithInjectedErrors "ReadCursor" env merrs (fmap (fmap WrapBlobRef) <$> Class.readCursor (Proxy @h) n (unwrapCursor $ lookUp' cursorVar)) (\_ -> pure ()) -- TODO(err) - Updates kups tableVar -> + Updates tableVar kups -> runRealWithInjectedErrors "Updates" env merrs - (Class.updates (unwrapTable $ lookUp' tableVar) kups) + (do let t = lookupDepTable tableVar + Class.updates t kups + pure $ Dep $ WrapTable t) (\_ -> pure ()) -- TODO(err) Inserts kins tableVar -> runRealWithInjectedErrors "Inserts" env merrs @@ -1505,6 +1562,11 @@ runIO action lookUp = ReaderT $ \ !env -> do lookUp' :: Var h x -> Realized IO x lookUp' = lookUpGVar (Proxy @(RealMonad h IO)) lookUp + lookupDepTable :: + DepVar h (WrapTable h IO k v b) + -> h IO k v b + lookupDepTable = unwrapTable . lookupDepVar (Proxy @IO) (Proxy @h) lookUp + runIOSim :: forall s a h. Class.IsTable h => LockstepAction (ModelState h) a @@ -1536,7 +1598,7 @@ runIOSim action lookUp = ReaderT $ \ !env -> do (\_ -> pure ()) -- TODO(err) NewCursor offset tableVar -> runRealWithInjectedErrors "NewCursor" env merrs - (WrapCursor <$> Class.newCursor offset (unwrapTable $ lookUp' tableVar)) + (WrapCursor <$> Class.newCursor offset (lookupDepTable tableVar)) (\_ -> pure ()) -- TODO(err) CloseCursor cursorVar -> runRealWithInjectedErrors "CloseCursor" env merrs @@ -1546,9 +1608,11 @@ runIOSim action lookUp = ReaderT $ \ !env -> do runRealWithInjectedErrors "ReadCursor" env merrs (fmap (fmap WrapBlobRef) <$> Class.readCursor (Proxy @h) n (unwrapCursor $ lookUp' cursorVar)) (\_ -> pure ()) -- TODO(err) - Updates kups tableVar -> + Updates tableVar kups -> runRealWithInjectedErrors "Updates" env merrs - (Class.updates (unwrapTable $ lookUp' tableVar) kups) + (do let t = lookupDepTable tableVar + Class.updates t kups + pure $ Dep $ WrapTable t) (\_ -> pure ()) -- TODO(err) Inserts kins tableVar -> runRealWithInjectedErrors "Inserts" env merrs @@ -1602,6 +1666,11 @@ runIOSim action lookUp = ReaderT $ \ !env -> do lookUp' :: Var h x -> Realized (IOSim s) x lookUp' = lookUpGVar (Proxy @(RealMonad h (IOSim s))) lookUp + lookupDepTable :: + DepVar h (WrapTable h IO k v b) + -> h (IOSim s) k v b + lookupDepTable = unwrapTable . lookupDepVar (Proxy @(IOSim s)) (Proxy @h) lookUp + -- | @'runRealWithInjectedErrors' _ errsVar merrs action rollback@ runs @action@ -- with injected errors if available in @merrs@. -- @@ -1633,16 +1702,22 @@ runRealWithInjectedErrors s env merrs k rollback = case eith of Left (Model.ErrDiskFault _) -> do modifyMutVar faultsVar (InjectFaultInducedError s :) - assert (countNoisyErrors errsLog >= 1) $ pure () - pure eith + if (countNoisyErrors errsLog >= 1) then + pure eith + else + pure $ Left (Model.ErrOther "counter1") Left _ -> do - assert (countNoisyErrors errsLog == 0) $ pure () - pure eith + if (countNoisyErrors errsLog == 0) then + pure eith + else + pure $ Left (Model.ErrOther "counter2") Right x -> do modifyMutVar faultsVar (InjectFaultAccidentalSuccess s :) rollback x - assert (countNoisyErrors errsLog == 0) $ pure () - pure $ Left $ Model.ErrDiskFault ("dummy: " <> s) + if (countNoisyErrors errsLog == 0) then + pure $ Left $ Model.ErrDiskFault ("dummy: " <> s) + else + pure $ Left (Model.ErrOther "counter3") where errsVar = envErrors env logVar = envErrorsLog env @@ -1804,7 +1879,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = | let genErrors = pure Nothing -- TODO: generate errors ] ++ [ (10, fmap Some $ (Action <$> genErrors <*>) $ - Updates <$> genUpdates <*> genTableVar) + Updates <$> (Left <$> genTableVar) <*> genUpdates) | let genErrors = pure Nothing -- TODO: generate errors ] ++ [ (10, fmap Some $ (Action <$> genErrors <*>) $ @@ -1820,7 +1895,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = | let genErrors = pure Nothing -- TODO: generate errors ] ++ [ (3, fmap Some $ (Action <$> genErrors <*>) $ - NewCursor <$> QC.arbitrary <*> genTableVar) + NewCursor <$> QC.arbitrary <*> (Left <$> genTableVar)) | length cursorVars <= 5 -- no more than 5 cursors at once , let genErrors = pure Nothing -- TODO: generate errors ] @@ -1926,7 +2001,8 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = shrinkActionWithVars :: forall h a. ( - Eq (Class.TableConfig h) + Show (Class.TableConfig h) + , Eq (Class.TableConfig h) , Arbitrary (Class.TableConfig h) , Typeable h ) @@ -1973,6 +2049,7 @@ dictIsTypeable = \case shrinkAction'WithVars :: forall h a. ( Eq (Class.TableConfig h) + , Show (Class.TableConfig h) , Arbitrary (Class.TableConfig h) , Typeable h ) @@ -1980,38 +2057,60 @@ shrinkAction'WithVars :: -> ModelState h -> Action' h a -> [Any (Action' h)] -shrinkAction'WithVars _ctx _st a = case a of +shrinkAction'WithVars ctx _st a = case a of New p conf -> [ Some $ New p conf' | conf' <- QC.shrink conf ] + -- * Updates + -- Shrink inserts and deletes towards updates. - Updates upds tableVar -> [ - Some $ Updates upds' tableVar - | upds' <- QC.shrink upds + + Updates tableVar upds -> [ + Some $ Updates tableVar' upds' + | (upds', tableVar') <- + QC.liftShrink (shrinkDepVar ctx findDeps) (upds, tableVar) ] Inserts kvbs tableVar -> [ - Some $ Inserts kvbs' tableVar - | kvbs' <- QC.shrink kvbs - ] <> [ - Some $ Updates (V.map f kvbs) tableVar + Some $ Updates (Left tableVar) (V.map f kvbs) | let f (k, v, mb) = (k, R.Insert v mb) ] Deletes ks tableVar -> [ - Some $ Deletes ks' tableVar - | ks' <- QC.shrink ks - ] <> [ - Some $ Updates (V.map f ks) tableVar + Some $ Updates (Left tableVar) (V.map f ks) | let f k = (k, R.Delete) ] + Mupserts mups tableVar -> [ + Some $ Updates (Left tableVar) (V.map f mups) + | let f (k, v) = (k, R.Mupsert v) + ] Lookups ks tableVar -> [ - Some $ Lookups ks' tableVar - | ks' <- QC.shrink ks + Some $ Lookups ks' tableVar' + | (ks', tableVar') <- QC.liftShrink (shrinkVar ctx) (ks, tableVar) + ] + + -- * Cursor + + NewCursor kmay tableVar -> [ + Some $ NewCursor kmay' tableVar' + | (kmay', tableVar') <- + QC.liftShrink (shrinkDepVar ctx findDeps) (kmay, tableVar) + ] + + ReadCursor n cursorVar -> [ + Some $ ReadCursor n' cursorVar' + | (n', cursorVar') <- + QC.liftShrink2 + (\x -> [ x' | QC.NonNegative x' <- QC.shrink (QC.NonNegative x)]) + (shrinkVar ctx) (n, cursorVar) ] _ -> [] + where + findDeps :: forall k v b. C k v b => [GVar Op (Dep (WrapTable h IO k v b))] + findDeps = mapGVar (OpFromRight `OpComp`) <$> + findVars ctx (Proxy @(Either Model.Err (Dep (WrapTable h IO k v b)))) {------------------------------------------------------------------------------- Interpret 'Op' against 'ModelValue' @@ -2027,6 +2126,7 @@ instance InterpretOp Op (ModelValue (ModelState h)) where OpFromLeft -> \case MEither x -> either Just (const Nothing) x OpFromRight -> \case MEither x -> either (const Nothing) Just x OpComp g f -> intOp g <=< intOp f + OpUnDep -> \case MDep (Dep x) -> Just x OpLookupResults -> Just . MVector . V.mapMaybe (\case MLookupResult x -> getBlobRef x) . \case MVector x -> x @@ -2141,7 +2241,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result _ -> stats updNumUpdates stats = case (action', result) of - (Updates upds _, MEither (Right (MUnit ()))) -> stats { + (Updates _ upds, MEither (Right (MDep (Dep (MTable _))))) -> stats { numUpdates = countAll upds } (Inserts ins _, MEither (Right (MUnit ()))) -> stats { @@ -2199,8 +2299,8 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result -- distribution. Success / failure is detailed elsewhere. Lookups _ tableVar -> updateCount tableVar RangeLookup _ tableVar -> updateCount tableVar - NewCursor _ tableVar -> updateCount tableVar - Updates _ tableVar -> updateCount tableVar + NewCursor _ tableVar -> updateCount (getDepVar (Proxy @h) tableVar) + Updates tableVar _ -> updateCount (getDepVar (Proxy @h) tableVar) Inserts _ tableVar -> updateCount tableVar Deletes _ tableVar -> updateCount tableVar Mupserts _ tableVar -> updateCount tableVar @@ -2285,9 +2385,9 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result | not (null ks) -> updateLastActionLog tableVar RangeLookup r tableVar | not (emptyRange r) -> updateLastActionLog tableVar - NewCursor _ tableVar -> updateLastActionLog tableVar - Updates upds tableVar - | not (null upds) -> updateLastActionLog tableVar + NewCursor _ tableVar -> updateLastActionLog (getDepVar (Proxy @h) tableVar) + Updates tableVar upds + | not (null upds) -> updateLastActionLog (getDepVar (Proxy @h) tableVar) Inserts ins tableVar | not (null ins) -> updateLastActionLog tableVar Deletes ks tableVar diff --git a/test/Test/Database/LSMTree/StateMachine/DL.hs b/test/Test/Database/LSMTree/StateMachine/DL.hs index b18aa0f09..801f9c8d4 100644 --- a/test/Test/Database/LSMTree/StateMachine/DL.hs +++ b/test/Test/Database/LSMTree/StateMachine/DL.hs @@ -27,7 +27,7 @@ import qualified Test.QuickCheck.Random as QC import Test.QuickCheck.StateModel.Lockstep import qualified Test.QuickCheck.StateModel.Lockstep.Defaults as QLS import Test.QuickCheck.StateModel.Variables -import Test.Tasty (TestTree, testGroup, withResource) +import Test.Tasty (TestTree, localOption, testGroup, withResource) import qualified Test.Tasty.QuickCheck as QC import Test.Util.PrettyProxy @@ -36,7 +36,11 @@ tests = testGroup "Test.Database.LSMTree.StateMachine.DL" [ withResource checkForgottenRefs (\_ -> checkForgottenRefs) $ \_ -> QC.testProperty "prop_example" prop_example , withResource checkForgottenRefs (const ignoreForgottenRefs) $ \_ -> - QC.testProperty "prop_noSwallowedExceptions" prop_noSwallowedExceptions + localOption (QC.QuickCheckReplay (read "SMGen 601225290552401160 8241196702162822795",50)) -- TODO: remove + (QC.testProperty "prop_noSwallowedExceptions" $ + QC.expectFailure $ -- TODO: remove + QC.withMaxSuccess 1000 $ -- TODO: remove + prop_noSwallowedExceptions) ] instance DynLogicModel (Lockstep (ModelState R.Table)) @@ -80,7 +84,7 @@ dl_example = do ups = V.fromList . map (\(k,v) -> (k, Insert v Nothing)) . Map.toList $ kvs - action $ Action Nothing $ Updates ups (unsafeMkGVar var3 (OpFromRight `OpComp` OpId)) + action $ Action Nothing $ Updates (Left $ unsafeMkGVar var3 (OpFromRight `OpComp` OpId)) ups -- This is a rather ugly assertion, and could be improved using some helper -- function(s). However, it does serve its purpose as checking that the -- insertions we just did were successful. @@ -96,6 +100,16 @@ dl_example = do Swallowed exceptions -------------------------------------------------------------------------------} +{- +--quickcheck-replay="(SMGen 601225290552401160 8241196702162822795,50)" + +--quickcheck-replay="(SMGen 1262390567463183010 1470447921673677017,56)" + +--quickcheck-replay="(SMGen 1761811726072439171 16251490036421965979,69)" +-} + + + -- | Test that the @lsm-tree@ library does not swallow exceptions. -- -- A functional requirement for the @lsm-tree@ library is that all exceptions diff --git a/test/Test/Database/LSMTree/StateMachine/Op.hs b/test/Test/Database/LSMTree/StateMachine/Op.hs index 1bd1d73cc..7fc34fde9 100644 --- a/test/Test/Database/LSMTree/StateMachine/Op.hs +++ b/test/Test/Database/LSMTree/StateMachine/Op.hs @@ -1,9 +1,6 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -Wno-orphans #-} -- | SumProd Op extended with BlobRef extraction module Test.Database.LSMTree.StateMachine.Op ( @@ -12,19 +9,34 @@ module Test.Database.LSMTree.StateMachine.Op ( , intOpId -- * 'HasBlobRef' class , HasBlobRef (..) + -- * Dependent shrinking + , Dep (..) + , DepVar + , getDepVar + , lookupDepVar + , shrinkDepVar ) where +import Control.Concurrent.Class.MonadMVar (MonadMVar (..)) +import Control.Concurrent.Class.MonadSTM (MonadSTM (..)) +import qualified Control.Concurrent.MVar as Real +import qualified Control.Concurrent.STM as Real import Control.Monad ((<=<)) import Control.Monad.IOSim (IOSim) import Control.Monad.Reader (ReaderT) import Control.Monad.State (StateT) +import Data.Data (Proxy (Proxy)) +import Data.Kind (Type) import qualified Data.Vector as V +import Database.LSMTree (Cursor, LookupResult, QueryResult, Table) import qualified Database.LSMTree.Class as Class +import Database.LSMTree.Common (BlobRef) import GHC.Show (appPrec) -import Test.QuickCheck.StateModel.Lockstep (InterpretOp, Operation) +import Test.QuickCheck.StateModel (LookUp, Realized) +import Test.QuickCheck.StateModel.Lockstep import qualified Test.QuickCheck.StateModel.Lockstep.Op as Op -import Test.Util.Orphans () -import Test.Util.TypeFamilyWrappers (WrapBlobRef) +import Test.Util.TypeFamilyWrappers (WrapBlob (..), WrapBlobRef (..), + WrapCursor, WrapTable (..)) {------------------------------------------------------------------------------- 'Op' @@ -39,6 +51,7 @@ data Op a b where OpFromLeft :: Op (Either a b) a OpFromRight :: Op (Either a b) b OpComp :: Op b c -> Op a b -> Op a c + OpUnDep :: Op (Dep a) a OpLookupResults :: Op (V.Vector (Class.LookupResult v (WrapBlobRef h IO b))) (V.Vector (WrapBlobRef h IO b)) OpQueryResults :: Op (V.Vector (Class.QueryResult k v (WrapBlobRef h IO b))) (V.Vector (WrapBlobRef h IO b)) @@ -51,6 +64,7 @@ intOpId OpRight = Just . Right intOpId OpFromLeft = either Just (const Nothing) intOpId OpFromRight = either (const Nothing) Just intOpId (OpComp g f) = intOpId g <=< intOpId f +intOpId OpUnDep = Just . unDep intOpId OpLookupResults = Just . V.mapMaybe getBlobRef intOpId OpQueryResults = Just . V.mapMaybe getBlobRef @@ -90,7 +104,8 @@ instance InterpretOp Op (Op.WrapRealized (IOSim s)) where OpFromLeft -> either (Just . Op.WrapRealized) (const Nothing) . Op.unwrapRealized OpFromRight -> either (const Nothing) (Just . Op.WrapRealized) . Op.unwrapRealized OpComp g f -> Op.intOp g <=< Op.intOp f - OpLookupResults -> Just . Op.WrapRealized . V.mapMaybe getBlobRef . Op.unwrapRealized + OpUnDep -> Just . Op.WrapRealized . unDep . Op.unwrapRealized + OpLookupResults -> Just . Op.WrapRealized . V.mapMaybe getBlobRef . Op.unwrapRealized OpQueryResults -> Just . Op.WrapRealized . V.mapMaybe getBlobRef . Op.unwrapRealized {------------------------------------------------------------------------------- @@ -109,6 +124,7 @@ sameOp = go go OpFromLeft OpFromLeft = True go OpFromRight OpFromRight = True go (OpComp g f) (OpComp g' f') = go g g' && go f f' + go OpUnDep OpUnDep = True go OpLookupResults OpLookupResults = True go OpQueryResults OpQueryResults = True go _ _ = False @@ -123,6 +139,7 @@ sameOp = go OpFromLeft -> () OpFromRight -> () OpComp{} -> () + OpUnDep -> () OpLookupResults{} -> () OpQueryResults{} -> () @@ -146,9 +163,39 @@ instance Show (Op a b) where go OpFromLeft = showString "OpFromLeft" go OpFromRight = showString "OpFromRight" go (OpComp g f) = go g . showString " `OpComp` " . go f + go OpUnDep = showString "OpUnDep" go OpLookupResults = showString "OpLookupResults" go OpQueryResults = showString "OpQueryResults" +{------------------------------------------------------------------------------- + IOSim +-------------------------------------------------------------------------------} + +type instance Realized (IOSim s) a = RealizeIOSim s a + +type RealizeIOSim :: Type -> Type -> Type +type family RealizeIOSim s a where + -- io-classes + RealizeIOSim s (Real.TVar a) = TVar (IOSim s) a + RealizeIOSim s (Real.TMVar a) = TMVar (IOSim s) a + RealizeIOSim s (Real.MVar a) = MVar (IOSim s) a + -- lsm-tree + RealizeIOSim s (Table IO k v b) = Table (IOSim s) k v b + RealizeIOSim s (LookupResult v b) = LookupResult v (RealizeIOSim s b) + RealizeIOSim s (QueryResult k v b) = QueryResult k v (RealizeIOSim s b) + RealizeIOSim s (Cursor IO k v b) = Table (IOSim s) k v b + RealizeIOSim s (BlobRef IO b) = BlobRef (IOSim s) b + -- Type family wrappers + RealizeIOSim s (WrapTable h IO k v b) = WrapTable h (IOSim s) k v b + RealizeIOSim s (WrapCursor h IO k v b) = WrapCursor h (IOSim s) k v b + RealizeIOSim s (WrapBlobRef h IO b) = WrapBlobRef h (IOSim s) b + RealizeIOSim s (WrapBlob b) = WrapBlob b + -- Congruence + RealizeIOSim s (f a b) = f (RealizeIOSim s a) (RealizeIOSim s b) + RealizeIOSim s (f a) = f (RealizeIOSim s a) + -- Default + RealizeIOSim s a = a + {------------------------------------------------------------------------------- 'HasBlobRef' class -------------------------------------------------------------------------------} @@ -164,3 +211,39 @@ instance HasBlobRef (Class.LookupResult v) where instance HasBlobRef (Class.QueryResult k v) where getBlobRef Class.FoundInQuery{} = Nothing getBlobRef (Class.FoundInQueryWithBlob _ _ blobref) = Just blobref + +{------------------------------------------------------------------------------- + Dependent shrinking +-------------------------------------------------------------------------------} + +newtype Dep a = Dep { unDep :: a } + deriving stock (Show, Eq, Functor) + +type DepVar state a = + Either + (ModelVar state a) + (ModelVar state (Dep a)) + +getDepVar :: + ModelOp state ~ Op + => Proxy state + -> DepVar state a + -> ModelVar state a +getDepVar _ dvar = either id (mapGVar (OpUnDep `OpComp`)) dvar + +lookupDepVar :: + forall m state a. (ModelOp state ~ Op, InterpretOp Op (Op.WrapRealized m)) + => Proxy m -> Proxy state -> LookUp m -> DepVar state a -> Realized m a +lookupDepVar _ _ lookUp = lookUp' . getDepVar (Proxy @state) + where + lookUp' = lookUpGVar (Proxy @m) lookUp + +shrinkDepVar :: + ModelOp state ~ Op + => ModelVarContext state + -> [GVar Op (Dep a)] + -> DepVar state a + -> [DepVar state a] +shrinkDepVar ctx findDeps = \case + Left z -> (Left <$> shrinkVar ctx z) ++ (Right <$> findDeps) + Right z -> Right <$> shrinkVar ctx z diff --git a/test/Test/Util/Orphans.hs b/test/Test/Util/Orphans.hs index 6ee22d3c3..f5f0b7cc4 100644 --- a/test/Test/Util/Orphans.hs +++ b/test/Test/Util/Orphans.hs @@ -1,79 +1,17 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GeneralisedNewtypeDeriving #-} -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE StandaloneKindSignatures #-} -{-# LANGUAGE TypeFamilies #-} - {-# OPTIONS_GHC -Wno-orphans #-} module Test.Util.Orphans () where -import Control.Concurrent.Class.MonadMVar (MonadMVar (..)) -import Control.Concurrent.Class.MonadSTM (MonadSTM (..)) -import qualified Control.Concurrent.MVar as Real -import qualified Control.Concurrent.STM as Real -import Control.Monad ((<=<)) import Control.Monad.IOSim (IOSim) -import Data.Kind (Type) -import Database.LSMTree (Cursor, LookupResult, QueryResult, Table) -import Database.LSMTree.Common (BlobRef, IOLike, SerialiseValue) +import Database.LSMTree.Common (IOLike, SerialiseValue) import Database.LSMTree.Internal.Serialise (SerialiseKey) import Test.QuickCheck.Modifiers (Small (..)) -import Test.QuickCheck.StateModel (Realized) -import Test.QuickCheck.StateModel.Lockstep (InterpretOp) -import qualified Test.QuickCheck.StateModel.Lockstep.Op as Op -import qualified Test.QuickCheck.StateModel.Lockstep.Op.SumProd as SumProd -import Test.Util.TypeFamilyWrappers (WrapBlob (..), WrapBlobRef (..), - WrapCursor, WrapTable (..)) {------------------------------------------------------------------------------- IOSim -------------------------------------------------------------------------------} instance IOLike (IOSim s) - -type instance Realized (IOSim s) a = RealizeIOSim s a - -type RealizeIOSim :: Type -> Type -> Type -type family RealizeIOSim s a where - -- io-classes - RealizeIOSim s (Real.TVar a) = TVar (IOSim s) a - RealizeIOSim s (Real.TMVar a) = TMVar (IOSim s) a - RealizeIOSim s (Real.MVar a) = MVar (IOSim s) a - -- lsm-tree - RealizeIOSim s (Table IO k v b) = Table (IOSim s) k v b - RealizeIOSim s (LookupResult v b) = LookupResult v (RealizeIOSim s b) - RealizeIOSim s (QueryResult k v b) = QueryResult k v (RealizeIOSim s b) - RealizeIOSim s (Cursor IO k v b) = Table (IOSim s) k v b - RealizeIOSim s (BlobRef IO b) = BlobRef (IOSim s) b - -- Type family wrappers - RealizeIOSim s (WrapTable h IO k v b) = WrapTable h (IOSim s) k v b - RealizeIOSim s (WrapCursor h IO k v b) = WrapCursor h (IOSim s) k v b - RealizeIOSim s (WrapBlobRef h IO b) = WrapBlobRef h (IOSim s) b - RealizeIOSim s (WrapBlob b) = WrapBlob b - -- Congruence - RealizeIOSim s (f a b) = f (RealizeIOSim s a) (RealizeIOSim s b) - RealizeIOSim s (f a) = f (RealizeIOSim s a) - -- Default - RealizeIOSim s a = a - -instance InterpretOp SumProd.Op (Op.WrapRealized (IOSim s)) where - intOp :: - SumProd.Op a b - -> Op.WrapRealized (IOSim s) a - -> Maybe (Op.WrapRealized (IOSim s) b) - intOp = \case - SumProd.OpId -> Just - SumProd.OpFst -> Just . Op.WrapRealized . fst . Op.unwrapRealized - SumProd.OpSnd -> Just . Op.WrapRealized . snd . Op.unwrapRealized - SumProd.OpLeft -> either (Just . Op.WrapRealized) (const Nothing) . Op.unwrapRealized - SumProd.OpRight -> either (const Nothing) (Just . Op.WrapRealized) . Op.unwrapRealized - SumProd.OpComp g f -> Op.intOp g <=< Op.intOp f - {------------------------------------------------------------------------------- QuickCheck -------------------------------------------------------------------------------}