packages feed

quickcheck-lockstep 0.1.0 → 0.2.0

raw patch · 8 files changed

+225/−59 lines, 8 filesdep +constraintsdep ~base

Dependencies added: constraints

Dependency ranges changed: base

Files

CHANGELOG.md view
@@ -1,5 +1,14 @@ # Revision history for quickcheck-lockstep +## 0.2.0 -- 2022-11-11++* Relax bounds on `base` (support up to ghc 9.4)+* Show real/mock response in addition to observable response+  (see `showRealResponse`)+* Add `labelActions` function+* Generalise `runActionsBracket` (Joris Dral)+* Expose getter for the model in `Lockstep` (Joris Dral)+ ## 0.1.0 -- 2022-10-11  * First release
quickcheck-lockstep.cabal view
@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               quickcheck-lockstep-version:            0.1.0+version:            0.2.0 license:            BSD-3-Clause license-file:       LICENSE author:             Edsko de Vries@@ -32,6 +32,7 @@       RankNTypes       ScopedTypeVariables       StandaloneDeriving+      TupleSections       TypeApplications       TypeFamilies   other-extensions:@@ -57,7 +58,8 @@       Test.QuickCheck.StateModel.Lockstep.Op   build-depends:       -- quickcheck-dynamic requires ghc 8.10 minimum-      base               >= 4.14 && < 4.15+      base               >= 4.14 && < 4.18+    , constraints        >= 0.13 && < 0.14     , mtl                >= 2.2  && < 2.3     , containers         >= 0.6  && < 0.7     , QuickCheck         >= 2.14 && < 2.15@@ -84,6 +86,7 @@   build-depends:       -- Version bounds determined by main lib       base+    , constraints     , containers     , directory     , filepath
src/Test/QuickCheck/StateModel/Lockstep.hs view
@@ -13,6 +13,7 @@ module Test.QuickCheck.StateModel.Lockstep (     -- * Main abstraction     Lockstep -- opaque+  , getModel   , InLockstep(..)   , RunLockstep(..)     -- ** Convenience aliases
src/Test/QuickCheck/StateModel/Lockstep/API.hs view
@@ -4,6 +4,7 @@ module Test.QuickCheck.StateModel.Lockstep.API (     -- * State     Lockstep(..)+  , getModel     -- * Main abstraction   , InLockstep(..)   , RunLockstep(..)@@ -14,6 +15,7 @@   , ModelVar   ) where +import Data.Constraint (Dict(..)) import Data.Kind import Data.Typeable @@ -55,6 +57,10 @@ instance Show state => Show (Lockstep state) where   show = show . lockstepModel +-- | Inspect the model that resides inside the Lockstep state+getModel :: Lockstep state -> state+getModel = lockstepModel+ {-------------------------------------------------------------------------------   Main lockstep abstraction -------------------------------------------------------------------------------}@@ -147,6 +153,16 @@   observeReal ::        Proxy m     -> LockstepAction state a -> Realized m a -> Observable state a++  -- | Show responses from the real system+  --+  -- This method does not need to be implemented, but if it is, counter-examples+  -- can include the real response in addition to the observable response.+  showRealResponse ::+       Proxy m+    -> LockstepAction state a+    -> Maybe (Dict (Show (Realized m a)))+  showRealResponse _ _ = Nothing  {-------------------------------------------------------------------------------   Convenience aliases
src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs view
@@ -17,6 +17,7 @@  import Prelude hiding (init) +import Data.Constraint (Dict(..)) import Data.Maybe (isNothing) import Data.Typeable @@ -137,19 +138,32 @@   => 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)+    compareEquality+      (a         , observeReal p action a)+      (modelResp , 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 [+    compareEquality ::+         (Realized m a, Observable state a)+      -> (ModelValue state a, Observable state a) -> Maybe String+    compareEquality (realResp, obsRealResp) (mockResp, obsMockResp)+      | obsRealResp == obsMockResp = Nothing+      | otherwise                  = Just $ concat [             "System under test returned: "-          , show real+          , case showRealResponse (Proxy @m) action of+              Nothing   -> show obsRealResp+              Just Dict -> concat [+                  show obsRealResp+                , " ("+                , show realResp+                , ")"+                ]           , "\nbut model returned:         "-          , show mock+          , show obsMockResp+          , " ("+          , show mockResp+          , ")"           ]-
src/Test/QuickCheck/StateModel/Lockstep/Run.hs view
@@ -6,6 +6,7 @@ module Test.QuickCheck.StateModel.Lockstep.Run (     -- * Finding labelled examples     tagActions+  , labelActions     -- * Run tests   , runActions   , runActionsBracket@@ -51,14 +52,17 @@ -- executed against the model /only/. tagActions :: forall state.      InLockstep state-  => Proxy state-  -> Actions (Lockstep state)-  -> Property-tagActions _p (Actions steps) =+  => Proxy state -> Actions (Lockstep state) -> Property+tagActions _p actions = QC.label ("Tags: " ++ show (labelActions actions)) True++labelActions :: forall state.+     InLockstep state+  => Actions (Lockstep state) -> [String]+labelActions (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 :: Set String -> Lockstep state -> [Step (Lockstep state)] -> [String]+    go tags _st []            = Set.toList tags     go tags  st ((v:=a) : ss) = go' tags st v a ss      go' :: forall a.@@ -68,7 +72,7 @@       -> Var a                      -- variable for the result of this action       -> Action (Lockstep state) a  -- action to execute       -> [Step (Lockstep state)]    -- remaining steps to execute-      -> Property+      -> [String]     go' tags (Lockstep before env) var action ss =         go (Set.union (Set.fromList tags') tags) st' ss       where@@ -94,16 +98,21 @@  -- | Convenience runner with support for state initialization ----- This is less general than 'Test.QuickCheck.StateModel.runActions', but--- will be useful in many scenarios.+-- This is less general than 'Test.QuickCheck.StateModel.runActions', but will+-- be useful in many scenarios.+--+-- For most lockstep-style tests, a suitable monad to run the tests in is+-- @'ReaderT' r 'IO'@. In this case, using @'runReaderT'@ as the runner argument+-- is a reasonable choice. runActionsBracket ::-     RunLockstep state (ReaderT st IO)+     RunLockstep state m   => Proxy state   -> IO st         -- ^ Initialisation   -> (st -> IO ()) -- ^ Cleanup+  -> (m Property -> st -> IO Property) -- ^ Runner   -> Actions (Lockstep state) -> Property-runActionsBracket _ init cleanup actions =-    monadicBracketIO init cleanup $+runActionsBracket _ init cleanup runner actions =+    monadicBracketIO init cleanup runner $       void $ StateModel.runActions actions  {-------------------------------------------------------------------------------@@ -114,22 +123,24 @@      Testable a   => IO st   -> (st -> IO ())-  -> ReaderT st IO a+  -> (m a -> st -> IO a)+  -> m a   -> Property-ioPropertyBracket init cleanup (ReaderT prop) = do+ioPropertyBracket init cleanup runner prop =     QC.ioProperty $ mask $ \restore -> do       st <- init-      a  <- restore (prop st) `onException` cleanup st+      a <- restore (runner prop st) `onException` cleanup st       cleanup st       return a  -- | Variation on 'monadicIO' that allows for state initialisation/cleanup-monadicBracketIO :: forall st a.-     Testable a+monadicBracketIO :: forall st a m.+     (Monad m, Testable a)   => IO st   -> (st -> IO ())-  -> (PropertyM (ReaderT st IO) a)+  -> (m Property -> st -> IO Property)+  -> PropertyM m a   -> Property-monadicBracketIO init cleanup =-    monadic (ioPropertyBracket init cleanup)+monadicBracketIO init cleanup runner =+    monadic (ioPropertyBracket init cleanup runner)
test/Test/IORef.hs view
@@ -1,42 +1,77 @@+{-# LANGUAGE RecordWildCards #-}+ {-# OPTIONS_GHC -Wno-orphans #-}  module Test.IORef (tests) where +import Control.Monad.Reader import Data.Bifunctor+import Data.Constraint (Dict(..)) 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.HUnit import Test.Tasty.QuickCheck (testProperty) +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.Run qualified as Lockstep+import Test.QuickCheck.StateModel.Lockstep.Run (labelActions)  {-------------------------------------------------------------------------------   Model "M" -------------------------------------------------------------------------------}  type MRef = Int-type M    = Map MRef Int +data M = M {+      -- | Value of every var+      mValues :: Map MRef Int++      -- | Often did we write each value to each var?+      --+      -- This is used for tagging.+    , mWrites :: Map (MRef, Int) Int+    }+  deriving (Show)+ initModel :: M-initModel = Map.empty+initModel = M {+      mValues = Map.empty+    , mWrites = Map.empty+    }  modelNew :: M -> (MRef, M)-modelNew m = (mockRef, Map.insert mockRef 0 m)+modelNew M{..} = (+      mockRef+    , M { mValues = Map.insert mockRef 0 mValues+        , mWrites = mWrites+        }+    )   where     mockRef :: MRef-    mockRef = Map.size m+    mockRef = Map.size mValues -modelWrite :: MRef -> Int -> M -> ((), M)-modelWrite v x m = ((), Map.insert v x m)+modelWrite :: MRef -> Int -> M -> (Int, M)+modelWrite v x M{..} = (+      x+    , M { mValues = Map.insert v x mValues+        , mWrites = Map.alter recordWrite (v, x) mWrites+        }+    )+  where+    recordWrite :: Maybe Int -> Maybe Int+    recordWrite Nothing  = Just 1 -- First write+    recordWrite (Just n) = Just (n + 1)  modelRead :: MRef -> M -> (Int, M)-modelRead v m = (m Map.! v, m)+modelRead v m@M{..} = (mValues Map.! v, m)  {-------------------------------------------------------------------------------   Instances@@ -48,10 +83,13 @@     New :: Action (Lockstep M) (IORef Int)      -- | Write value to IORef+    --+    -- The value is specified either as a concrete value or by reference+    -- to a previous write.     Write ::          ModelVar M (IORef Int)-      -> Int-      -> Action (Lockstep M) ()+      -> Either Int (ModelVar M Int)+      -> Action (Lockstep M) Int      -- | Read IORef     Read ::@@ -64,15 +102,14 @@   arbitraryAction = Lockstep.arbitraryAction   shrinkAction    = Lockstep.shrinkAction -instance RunModel (Lockstep M) IO where+instance RunModel (Lockstep M) RealMonad where   perform       = \_state -> runIO   postcondition = Lockstep.postcondition-  monitoring    = Lockstep.monitoring (Proxy @IO)+  monitoring    = Lockstep.monitoring (Proxy @RealMonad)  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@@ -80,12 +117,12 @@     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]+  usedVars New                  = []+  usedVars (Write v (Left _))   = [SomeGVar v]+  usedVars (Write v (Right v')) = [SomeGVar v, SomeGVar v']+  usedVars (Read  v)            = [SomeGVar v]    modelNextState = runModel @@ -103,17 +140,40 @@            Gen (ModelVar M (IORef Int))         -> [Gen (Any (LockstepAction M))]       withVars genVar = [-            fmap Some $ Write <$> genVar <*> arbitrary+            fmap Some $ Write <$> genVar <*> (Left <$> choose (0, 10))           , fmap Some $ Read  <$> genVar           ] -instance RunLockstep M IO where+  shrinkWithVars findVars _mock = \case+      New               -> []+      Write v (Left x)  -> concat [+                               Some . Write v . Left  <$> shrink x+                             , Some . Write v . Right <$> findVars (Proxy @Int)+                             ]+      Write _ (Right _) -> []+      Read  _           -> []++  tagStep (_stBefore, stAfter) _action _result = concat [+        [ "WriteSameVarTwice"+        | not+        . Map.null+        . Map.filter (\numWrites -> numWrites > 1)+        $ mWrites stAfter+        ]+      ]++instance RunLockstep M RealMonad where   observeReal _ action result =       case (action, result) of         (New     , _) -> ORef         (Write{} , x) -> OId x         (Read{}  , x) -> OId x +  showRealResponse _ = \case+    New{}   -> Nothing+    Write{} -> Just Dict+    Read{}  -> Just Dict+ deriving instance Show (Action (Lockstep M) a) deriving instance Show (Observable M a) deriving instance Show (ModelValue M a)@@ -126,37 +186,88 @@   Interpreters against the real system and against the model -------------------------------------------------------------------------------} -runIO :: Action (Lockstep M) a -> LookUp IO -> IO a-runIO action lookUp =+data Buggy = Buggy | NotBuggy+  deriving (Show, Eq)++instance Arbitrary Buggy where+  arbitrary = elements [Buggy, NotBuggy]++  shrink Buggy    = [NotBuggy]+  shrink NotBuggy = []++-- | We trigger a bug if we write the /same/ value to the /same/ variable+type BrokenRef = [(IORef Int, Int)]++type RealMonad = ReaderT (Buggy, IORef BrokenRef) IO++runIO :: Action (Lockstep M) a -> LookUp RealMonad -> RealMonad a+runIO action lookUp = ReaderT $ \(buggy, brokenRef) ->     case action of       New       -> newIORef 0-      Write v x -> writeIORef (lookUpRef v) x-      Read  v   -> readIORef  (lookUpRef v)+      Write v x -> brokenWrite buggy brokenRef (lookUpRef v) (lookUpInt x)+      Read  v   -> readIORef (lookUpRef v)   where     lookUpRef :: ModelVar M (IORef Int) -> IORef Int-    lookUpRef = lookUpGVar (Proxy @IO) lookUp+    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp +    lookUpInt :: Either Int (ModelVar M Int) -> Int+    lookUpInt (Left  x) = x+    lookUpInt (Right v) = lookUpGVar (Proxy @RealMonad) lookUp v++-- | The second write to the same variable will be broken+brokenWrite :: Buggy -> IORef BrokenRef -> IORef Int -> Int -> IO Int+brokenWrite NotBuggy _         v x = writeIORef v x >> return x+brokenWrite Buggy    brokenRef v x = do+    broken <- readIORef brokenRef+    if (v, x) `elem` broken then+      writeIORef v 123456789+    else+      writeIORef v x+    modifyIORef brokenRef ((v, x) :)+    return x+ 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)+      New       -> first MRef . modelNew+      Write v x -> first MInt . modelWrite (lookUpRef v) (lookUpInt x)+      Read  v   -> first MInt . modelRead  (lookUpRef v)   where     lookUpRef :: ModelVar M (IORef Int) -> MRef     lookUpRef var = case lookUp var of MRef r -> r +    lookUpInt :: Either Int (ModelVar M Int) -> Int+    lookUpInt (Left  x) = x+    lookUpInt (Right v) = case lookUp v of MInt x -> x+ {-------------------------------------------------------------------------------   Top-level tests -------------------------------------------------------------------------------} -propIORef :: Actions (Lockstep M) -> Property-propIORef = Lockstep.runActions (Proxy @M)+propIORef :: Buggy -> Actions (Lockstep M) -> Property+propIORef buggy actions =+      (if triggersBug then expectFailure  else id)+    $ Lockstep.runActionsBracket+        (Proxy @M)+        initBroken+        (\_ -> return ())+        runReaderT+        actions+  where+    triggersBug :: Bool+    triggersBug =+           buggy == Buggy+        && "WriteSameVarTwice" `elem` labelActions actions +    initBroken :: IO (Buggy, IORef BrokenRef)+    initBroken = (buggy,) <$> newIORef []+ tests :: TestTree tests = testGroup "Test.IORef" [-      testProperty "runActions" propIORef+      testCase "labelledExamples" $+        QC.labelledExamples $ Lockstep.tagActions (Proxy @M)+    , testProperty "runActions" propIORef     ]
test/Test/MockFS.hs view
@@ -369,6 +369,7 @@         Lockstep.runActionsBracket (Proxy @FsState)           (createTempDirectory tmpDir "QSM")           removeDirectoryRecursive+          runReaderT     ]   where     -- TODO: tmpDir should really be a parameter to the test suite