DL.hs

{-# LANGUAGE TemplateHaskell #-}

{-# OPTIONS_GHC -Wno-unused-do-bind #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Database.LSMTree.StateMachine.DL (
    tests
  ) where

import           Control.Monad (void)
import           Control.RefCount
import           Control.Tracer
import qualified Data.Map.Strict as Map
import           Data.Typeable (Typeable)
import qualified Data.Vector as V
import           Database.LSMTree as R
import qualified Database.LSMTree.Internal.Config as R (TableConfig (..))
import qualified Database.LSMTree.Model.Session as Model (fromSomeTable, tables)
import qualified Database.LSMTree.Model.Table as Model (values)
import           Prelude
import           SafeWildCards
import           System.FS.API.Types
import           System.FS.Sim.Error hiding (Blob)
import qualified System.FS.Sim.Stream as Stream
import           System.FS.Sim.Stream (Stream)
import           Test.Database.LSMTree.StateMachine hiding (tests)
import           Test.Database.LSMTree.StateMachine.Op
import           Test.QuickCheck as QC hiding (Some, label)
import           Test.QuickCheck.DynamicLogic
import qualified Test.QuickCheck.Gen as QC
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 qualified Test.Tasty.QuickCheck as QC
import           Test.Util.FS
import           Test.Util.PrettyProxy

tests :: TestTree
tests = testGroup "Test.Database.LSMTree.StateMachine.DL" [
      QC.testProperty "prop_example" prop_example
    , test_noSwallowedExceptions
    ]

instance DynLogicModel (Lockstep (ModelState IO R.Table))

-- | An example of how dynamic logic formulas can be run.
--
-- 'dl_example' is a manually created formula, but the same method of running a
-- formula also applies to counterexamples produced by a state machine property
-- test, such as 'propLockstep_RealImpl_RealFS_IO'. Such counterexamples are
-- (often almost) valid 'DL' expression. They can be copy-pasted into a Haskell
-- module with minor tweaks to make the compiler accept the copied code, and
-- then they can be run as any other 'DL' expression.
prop_example :: Property
prop_example =
    -- Run the example ...
    forAllDL dl_example $
    -- ... with the given lockstep property
    propLockstep_RealImpl_MockFS_IO tr CheckCleanup CheckFS CheckRefs (QC.Fixed 17)
  where
    -- To enable tracing, use something like @show `contramap` stdoutTracer@
    -- instead
    tr = nullTracer

-- | Create an initial "large" table
dl_example :: Typeable m => DL (Lockstep (ModelState m R.Table)) ()
dl_example = do
    -- Create an initial table and fill it with some inserts
    var3 <- action $ Action Nothing $ NewTableWith (PrettyProxy @((Key, Value, Blob))) (R.TableConfig {
          confMergePolicy = LazyLevelling
        , confSizeRatio = Four
        , confWriteBufferAlloc = AllocNumEntries 4
        , confBloomFilterAlloc = AllocFixed 10
        , confFencePointerIndex = OrdinaryIndex
        , confDiskCachePolicy = DiskCacheNone
        , confMergeSchedule = OneShot
        , confMergeBatchSize = MergeBatchSize 4
        })
    let kvs :: Map.Map Key Value
        kvs = Map.fromList $
              QC.unGen (QC.vectorOf 37 $ (,) <$> QC.arbitrary <*> QC.arbitrary)
                       (QC.mkQCGen 42) 30
        ups :: V.Vector (Key, Update Value Blob)
        ups = V.fromList
            . map (\(k,v) -> (k, Insert v Nothing))
            . Map.toList $ kvs
    action $ Action Nothing $ Updates ups (unsafeMkGVar var3 (OpFromRight `OpComp` OpId))
    -- 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.
    assertModel "table size" $ \s ->
        let (ModelState s' _) = getModel s in
        case Map.elems (Model.tables s') of
          [(_, smTbl)]
            | Just tbl <- (Model.fromSomeTable @Key @Value @Blob smTbl)
            -> Map.size (Model.values tbl) == Map.size kvs
          _ -> False

{-------------------------------------------------------------------------------
  Swallowed exceptions
-------------------------------------------------------------------------------}

-- | See 'prop_noSwallowedExceptions'.
--
-- Forgotten reference checks are disabled completely, because we allow bugs
-- (like forgotten references) in exception unsafe code where we inject disk
-- faults.
test_noSwallowedExceptions :: TestTree
test_noSwallowedExceptions =
    withResource
      (checkForgottenRefs >> disableForgottenRefChecks)
      (\_ -> enableForgottenRefChecks) $ \ !_ ->
      QC.testProperty "prop_noSwallowedExceptions" prop_noSwallowedExceptions

-- | Test that the @lsm-tree@ library does not swallow exceptions.
--
-- A functional requirement for the @lsm-tree@ library is that all exceptions
-- are properly communicated to the user. An alternative way of stating this
-- requirement is that no exceptions should be /swallowed/ by the library. We
-- test this requirement by running the state machine test with injected disk
-- errors using @fs-sim@, and asserting that no exceptions are swallowed.
--
-- The state machine test compares the SUT against a model by checking that
-- their responses to @lsm-tree@ actions are the same. As of writing this
-- property, not all of these actions on the SUT are guaranteed to be fully
-- exception safe. As a result, an exception might leave the database (i.e.,
-- session, tables, cursors) in an inconsistent state. The results of subsequent
-- operations on the inconsistent database should be considered undefined. As
-- such, it is highly likely that the SUT and model will thereafter disagree,
-- leading to a failing property.
--
-- Still, we want to run the swallowed error assertion on /all/ operations,
-- regardless of whether they are exception safe. We overcome this problem by
-- /definitely/ injecting errors (and running a swallowed error assertion) for
-- the last action in a sequence of actions. This may leave the final database
-- state inconsistent, but that is okay. However, we'll also have to disable
-- sanity checks like 'NoCheckCleanup', 'NoCheckFS', and 'NoCheckRefs', because
-- they are likely to fail if the database is an inconsistent state.
--
-- TODO: running only one swallowed exception assertion per action sequence is
-- restrictive, but this automatically improves as we make more actions
-- exceptions safe. When we generate injected errors for these errors by default
-- (in @arbitraryWithVars@), the swallowed exception assertion automatically
-- runs for those actions as well.
prop_noSwallowedExceptions :: QC.Fixed Salt -> Property
prop_noSwallowedExceptions salt = forAllDL dl_noSwallowExceptions runner
  where
    -- disable all file system and reference checks
    runner = propLockstep_RealImpl_MockFS_IO tr NoCheckCleanup NoCheckFS NoCheckRefs salt
    tr = nullTracer

-- | Run any number of actions using the default actions generator, and finally
-- run a single action with errors *definitely* enabled.
dl_noSwallowExceptions :: Typeable m => DL (Lockstep (ModelState m R.Table)) ()
dl_noSwallowExceptions = do
    -- Run any number of actions as normal
    anyActions_

    -- Generate a single action as normal
    varCtx <- getVarContextDL
    st <- getModelStateDL
    let
      gen = QLS.arbitraryAction varCtx st
      predicate (Some a) = QLS.precondition st a
      shr (Some a) = QLS.shrinkAction varCtx st a
    Some a <- forAllQ $ withGenQ gen predicate shr

    -- Overwrite the maybe errors of the generated action with *definitely* just
    -- errors.
    case a of
      Action _merrs a' -> do
        HasNoVariables errs <-
          forAllQ $ hasNoVariablesQ $ withGenQ arbitraryErrors (\_ -> True) shrinkErrors
        -- Run the modified action
        void $ action $ Action (Just errs) a'

-- | Generate an 'Errors' with arbitrary probabilities of exceptions.
--
-- The default 'genErrors' from @fs-sim@ generates streams of 'Maybe' exceptions
-- with a fixed probability for a 'Just' or 'Nothing'. The version here
-- generates an arbitrary probability for each stream, which should generate a
-- larger variety of 'Errors' structures.
--
-- TODO: upstream to @fs-sim@ to replace the default 'genErrors'?
arbitraryErrors :: Gen Errors
arbitraryErrors = do
    dumpStateE                <- genStream arbitrary
    hCloseE                   <- genStream arbitrary
    hTruncateE                <- genStream arbitrary
    doesDirectoryExistE       <- genStream arbitrary
    doesFileExistE            <- genStream arbitrary
    hOpenE                    <- genStream arbitrary
    hSeekE                    <- genStream arbitrary
    hGetSomeE                 <- genErrorStreamGetSome
    hGetSomeAtE               <- genErrorStreamGetSome
    hPutSomeE                 <- genErrorStreamPutSome
    hGetSizeE                 <- genStream arbitrary
    createDirectoryE          <- genStream arbitrary
    createDirectoryIfMissingE <- genStream arbitrary
    listDirectoryE            <- genStream arbitrary
    removeDirectoryRecursiveE <- genStream arbitrary
    removeFileE               <- genStream arbitrary
    renameFileE               <- genStream arbitrary
    hGetBufSomeE              <- genErrorStreamGetSome
    hGetBufSomeAtE            <- genErrorStreamGetSome
    hPutBufSomeE              <- genErrorStreamPutSome
    hPutBufSomeAtE            <- genErrorStreamPutSome
    pure $ filterErrors Errors {..}
  where
    -- Generate a stream using 'genLikelihoods' for its 'Maybe' elements.
    genStream :: forall a. Gen a -> Gen (Stream a)
    genStream genA = do
        (pNothing, pJust) <- genLikelihoods
        Stream.genInfinite $ Stream.genMaybe pNothing pJust genA

    -- Generate two integer likelihoods for 'Nothing' and 'Just' constructors.
    genLikelihoods :: Gen (Int, Int)
    genLikelihoods = do
      NonNegative pNothing <- arbitrary
      NonNegative pJust <- arbitrary
      if pNothing == 0 then
        pure (0, 1)
      else if pJust == 0 then
        pure (1, 0)
      else
        pure (pNothing, pJust)

    genErrorStreamGetSome :: Gen ErrorStreamGetSome
    genErrorStreamGetSome = genStream $ liftArbitrary2 arbitrary arbitrary

    genErrorStreamPutSome :: Gen ErrorStreamPutSome
    genErrorStreamPutSome = genStream $ flip liftArbitrary2 arbitrary $ do
        errorType <- arbitrary
        maybePutCorruption <- liftArbitrary genPutCorruption
        pure (errorType, maybePutCorruption)

    genPutCorruption :: Gen PutCorruption
    genPutCorruption = oneof [
          PartialWrite <$> arbitrary
        , SubstituteWithJunk <$> arbitrary
        ]
      where
        _coveredAllCases x = case x of
          PartialWrite{}       -> pure ()
          SubstituteWithJunk{} -> pure ()

    -- TODO: there is one case where an 'FsReachEOF' error is swallowed. Is that
    -- valid behaviour, or should we change it?
    filterErrors errs = errs {
          hGetBufSomeE = Stream.filter (not . isFsReachedEOFError) (hGetBufSomeE errs)
        }

    isFsReachedEOFError = maybe False (either isFsReachedEOF (const False))

-- | Shrink each error stream and all error stream elements.
--
-- The default 'shrink' from @fs-sim@ shrinks only the stream structure, but not
-- the elements contained in those streams.
--
-- TODO: upstream to @fs-sim@ to replace the default 'shrink'?
shrinkErrors :: Errors -> [Errors]
shrinkErrors err@($(fields 'Errors))
    | allNull err = []
    | otherwise = emptyErrors : concatMap (filter (not . allNull))
        [ (\s' -> err { dumpStateE = s' })                <$> Stream.liftShrinkStream shrink dumpStateE
        , (\s' -> err { hOpenE = s' })                    <$> Stream.liftShrinkStream shrink hOpenE
        , (\s' -> err { hCloseE = s' })                   <$> Stream.liftShrinkStream shrink hCloseE
        , (\s' -> err { hSeekE = s' })                    <$> Stream.liftShrinkStream shrink hSeekE
        , (\s' -> err { hGetSomeE = s' })                 <$> Stream.liftShrinkStream shrink hGetSomeE
        , (\s' -> err { hGetSomeAtE = s' })               <$> Stream.liftShrinkStream shrink hGetSomeAtE
        , (\s' -> err { hPutSomeE = s' })                 <$> Stream.liftShrinkStream shrink hPutSomeE
        , (\s' -> err { hTruncateE = s' })                <$> Stream.liftShrinkStream shrink hTruncateE
        , (\s' -> err { hGetSizeE = s' })                 <$> Stream.liftShrinkStream shrink hGetSizeE
        , (\s' -> err { createDirectoryE = s' })          <$> Stream.liftShrinkStream shrink createDirectoryE
        , (\s' -> err { createDirectoryIfMissingE = s' }) <$> Stream.liftShrinkStream shrink createDirectoryIfMissingE
        , (\s' -> err { listDirectoryE = s' })            <$> Stream.liftShrinkStream shrink listDirectoryE
        , (\s' -> err { doesDirectoryExistE = s' })       <$> Stream.liftShrinkStream shrink doesDirectoryExistE
        , (\s' -> err { doesFileExistE = s' })            <$> Stream.liftShrinkStream shrink doesFileExistE
        , (\s' -> err { removeDirectoryRecursiveE = s' }) <$> Stream.liftShrinkStream shrink removeDirectoryRecursiveE
        , (\s' -> err { removeFileE = s' })               <$> Stream.liftShrinkStream shrink removeFileE
        , (\s' -> err { renameFileE = s' })               <$> Stream.liftShrinkStream shrink renameFileE
        , (\s' -> err { hGetBufSomeE = s' })              <$> Stream.liftShrinkStream shrink hGetBufSomeE
        , (\s' -> err { hGetBufSomeAtE = s' })            <$> Stream.liftShrinkStream shrink hGetBufSomeAtE
        , (\s' -> err { hPutBufSomeE = s' })              <$> Stream.liftShrinkStream shrink hPutBufSomeE
        , (\s' -> err { hPutBufSomeAtE = s' })            <$> Stream.liftShrinkStream shrink hPutBufSomeAtE
        ]

deriving stock instance Enum FsErrorType
deriving stock instance Bounded FsErrorType

instance Arbitrary FsErrorType where
  arbitrary = arbitraryBoundedEnum
  shrink = shrinkBoundedEnum