quickcheck-lockstep 0.6.0 → 0.7.0
raw patch · 14 files changed
+613/−69 lines, 14 filesdep +tasty-goldendep ~QuickCheckdep ~basedep ~containers
Dependencies added: tasty-golden
Dependency ranges changed: QuickCheck, base, containers, mtl, quickcheck-dynamic
Files
- CHANGELOG.md +23/−0
- quickcheck-lockstep.cabal +38/−5
- src/Test/QuickCheck/StateModel/Lockstep.hs +4/−1
- src/Test/QuickCheck/StateModel/Lockstep/API.hs +45/−14
- src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs +48/−19
- src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs +14/−0
- src/Test/QuickCheck/StateModel/Lockstep/GVar.hs +25/−12
- test-internals/Main.hs +9/−0
- test-internals/Test/Test/QuickCheck/StateModel/Lockstep/GVar.hs +176/−0
- test/Main.hs +7/−5
- test/Test/Golden.hs +107/−0
- test/Test/IORef/Full.hs +2/−2
- test/Test/IORef/Simple.hs +1/−1
- test/Test/MockFS.hs +114/−10
CHANGELOG.md view
@@ -1,5 +1,28 @@ # Revision history for quickcheck-lockstep +## 0.7.0 -- 2025-05-09++* BREAKING: Rename `lookupGVar` to `realLookupVar`, and add a `RealLookup`+ convenience alias that is used in the type of `RealLookupVar`. The type of+ `realLookupVar` is slightly different than the type of `lookupGVar`, but only+ in the positions of universal quantification over types.+* NON-BREAKING: improved error messages for `realLookupVar` and `lookupVar`,+ which might throw an error when variables are ill-defined or unevaluable.+* PATCH: some documentation is moved from convenience aliases like+ `ModelFindVariables` to the functions have these aliases in their type, like+ `findVars`.+* BREAKING: Enable verbose counterexamples by default in the 'postcondition'+ function using 'postconditionWith'.+* NON-BREAKING: Add a new 'postconditionWith' function that can be configured to+ produce more verbose counterexamples. With verbosity disabled, all states of+ the model are printed in a counterexample. If verbosity is enabled, the+ counterexample will also include all responses from the real system and the+ model.+* NON-BREAKING: Add a new `shrinkVar` function and `ModelShrinkVar` type alias.+ Use `shrinkVar` to shrink variables to earlier variables of the same type.+* PATCH: allow building with `ghc-9.12`+* PATCH: support `containers-0.8`+ ## 0.6.0 -- 2024-12-03 * BREAKING: Generalise `ModelFindVariables` and `ModelLookup` to
quickcheck-lockstep.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: quickcheck-lockstep-version: 0.6.0+version: 0.7.0 license: BSD-3-Clause license-file: LICENSE author: Edsko de Vries@@ -21,7 +21,14 @@ notion of observability. tested-with:- GHC ==8.10 || ==9.0 || ==9.2 || ==9.4 || ==9.6 || ==9.8 || ==9.10+ GHC ==8.10+ || ==9.0+ || ==9.2+ || ==9.4+ || ==9.6+ || ==9.8+ || ==9.10+ || ==9.12 source-repository head type: git@@ -65,9 +72,9 @@ -- quickcheck-dynamic requires ghc 8.10 minimum build-depends:- , base >=4.14 && <4.21+ , base >=4.14 && <4.22 , constraints ^>=0.13 || ^>=0.14- , containers ^>=0.6 || ^>=0.7+ , containers ^>=0.6 || ^>=0.7 || ^>=0.8 , mtl ^>=2.2 || ^>=2.3 , QuickCheck ^>=2.14 || ^>=2.15 , quickcheck-dynamic ^>=3.4.1@@ -80,6 +87,7 @@ hs-source-dirs: test main-is: Main.hs other-modules:+ Test.Golden Test.IORef.Full Test.IORef.Simple Test.MockFS@@ -91,7 +99,7 @@ -- Version bounds determined by main lib build-depends:- , base+ , base < 5 , constraints , containers , directory@@ -101,6 +109,31 @@ , quickcheck-dynamic , quickcheck-lockstep , tasty+ , tasty-golden , tasty-hunit , tasty-quickcheck , temporary++test-suite test-internals+ import: lang+ type: exitcode-stdio-1.0+ hs-source-dirs: test-internals src+ main-is: Main.hs+ other-modules:+ Test.QuickCheck.StateModel.Lockstep.EnvF+ Test.QuickCheck.StateModel.Lockstep.GVar+ Test.QuickCheck.StateModel.Lockstep.Op+ Test.QuickCheck.StateModel.Lockstep.Op.SumProd+ Test.Test.QuickCheck.StateModel.Lockstep.GVar++ ghc-options:+ -Wno-prepositive-qualified-module++ -- Version bounds determined by main lib+ build-depends:+ , base < 5+ , quickcheck-dynamic+ , tasty+ , mtl+ , tasty-quickcheck+ , QuickCheck
src/Test/QuickCheck/StateModel/Lockstep.hs view
@@ -20,16 +20,19 @@ , LockstepAction , ModelFindVariables , ModelLookUp+ , ModelShrinkVar , ModelVar+ , RealLookUp -- * Variable context , ModelVarContext , lookupVar , findVars+ , shrinkVar+ , realLookupVar -- * Variables , GVar -- opaque , AnyGVar(..) , unsafeMkGVar- , lookUpGVar , mapGVar -- ** Operations , Operation(..)
src/Test/QuickCheck/StateModel/Lockstep/API.hs view
@@ -15,10 +15,14 @@ , ModelFindVariables , ModelLookUp , ModelVar+ , ModelShrinkVar+ , RealLookUp -- * Variable context , ModelVarContext , findVars , lookupVar+ , shrinkVar+ , realLookupVar ) where import Data.Constraint (Dict(..))@@ -26,7 +30,7 @@ import Data.Typeable import Test.QuickCheck (Gen)-import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action)+import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action, LookUp) import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF) import Test.QuickCheck.StateModel.Lockstep.GVar (GVar, AnyGVar(..), fromVar)@@ -179,20 +183,20 @@ -- | 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.+-- | See 'lookupVar'. 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'.+-- | See 'findVars'. type ModelFindVariables state = forall a. Typeable a => Proxy a -> [GVar (ModelOp state) a] +-- | See 'shrinkVar'.+type ModelShrinkVar state = forall a. ModelVar state a -> [ModelVar state a]++-- | See 'realLookupVar'.+type RealLookUp m op = forall a. Proxy m -> LookUp m -> GVar op a -> Realized m a+ -- | Variables with a "functor-esque" instance type ModelVar state = GVar (ModelOp state) @@ -203,18 +207,45 @@ -- | The environment of known variables and their (model) values. -- -- This environment can be queried for information about known variables through--- 'findVars' and 'lookupVar'. This environment is updated automically by the--- lockstep framework.+-- 'findVars', 'lookupVar', and 'shrinkVar'. This environment is updated+-- automically by the lockstep framework. type ModelVarContext state = EnvF (ModelValue state) --- | See 'ModelFindVariables'.+-- | 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 'EnvF.mapGVar'. findVars :: InLockstep state => ModelVarContext state -> ModelFindVariables state findVars env _ = map fromVar $ EnvF.keysOfType env --- | See 'ModelLookUp'.+-- | Look up a variable for execution of the model.+--+-- The type of the variable is the type in the /real/ system. lookupVar :: InLockstep state => ModelVarContext state -> ModelLookUp state-lookupVar env = EnvF.lookUpEnvF env+lookupVar env gvar = case EnvF.lookUpEnvF env gvar of+ Just x -> x+ Nothing -> error+ "lookupVar: the variable (ModelVar) must be well-defined and evaluable, \+ \but this requirement was violated. Normally, this is guaranteed by the \+ \default test 'precondition'."++-- | Shrink variables to /earlier/ variables of the same type.+shrinkVar ::+ (Typeable state, InterpretOp (ModelOp state) (ModelValue state))+ => ModelVarContext state -> ModelShrinkVar state+shrinkVar env var = EnvF.shrinkGVar env var++-- | Look up a variable for execution of the real system.+--+-- The type of the variable is the type in the /real/ system.+realLookupVar :: InterpretOp op (WrapRealized m) => RealLookUp m op+realLookupVar p lookUp gvar = case EnvF.lookUpGVar p lookUp gvar of+ Just x -> x+ Nothing -> error+ "realLookupVar: the variable (GVar) must be well-defined and evaluable, \+ \but this requirement was violated. Normally, this is guaranteed by the \+ \default test 'precondition'."
src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs view
@@ -14,6 +14,7 @@ , shrinkAction -- * Default implementations for methods of 'RunModel' , postcondition+ , postconditionWith , monitoring ) where @@ -99,10 +100,27 @@ -> LookUp m -> Realized m a -> PostconditionM m Bool-postcondition (before, _after) action _lookUp a =+postcondition = postconditionWith True++-- | Like 'postcondition', but with configurable verbosity.+--+-- By default, all states of the model are printed when a property+-- counterexample is printed. If verbose output is enabled, the counterexample+-- will also print all responses from the real system and the model.+postconditionWith :: forall m state a.+ RunLockstep state m+ => Bool -- ^ Verbose output+ -> (Lockstep state, Lockstep state)+ -> LockstepAction state a+ -> LookUp m+ -> Realized m a+ -> PostconditionM m Bool+postconditionWith verbose (before, _after) action _lookUp a = case checkResponse (Proxy @m) before action a of- Nothing -> pure True- Just s -> monitorPost (QC.counterexample s) >> pure False+ Right s+ | verbose -> monitorPost (QC.counterexample s) >> pure True+ | otherwise -> pure True+ Left s -> monitorPost (QC.counterexample s) >> pure False monitoring :: forall m state a. RunLockstep state m@@ -155,7 +173,7 @@ checkResponse :: forall m state a. RunLockstep state m => Proxy m- -> Lockstep state -> LockstepAction state a -> Realized m a -> Maybe String+ -> Lockstep state -> LockstepAction state a -> Realized m a -> Either String String checkResponse p (Lockstep state env) action a = compareEquality (a , observeReal p action a)@@ -166,23 +184,34 @@ compareEquality :: (Realized m a, Observable state a)- -> (ModelValue state a, Observable state a) -> Maybe String+ -> (ModelValue state a, Observable state a) -> Either String String compareEquality (realResp, obsRealResp) (mockResp, obsMockResp)- | obsRealResp == obsMockResp = Nothing- | otherwise = Just $ concat [+ | obsRealResp == obsMockResp = Right $ concat [ "System under test returned: "- , case showRealResponse (Proxy @m) action of- Nothing -> show obsRealResp- Just Dict -> concat [- show obsRealResp- , " ("- , show realResp- , ")"- ]+ , sutReturned+ , "\nModel returned: "+ , modelReturned+ ]+ | otherwise = Left $ concat [+ "System under test returned: "+ , sutReturned , "\nbut model returned: "- , show obsMockResp- , " ("- , show mockResp- , ")"+ , modelReturned ] + where+ sutReturned = case showRealResponse (Proxy @m) action of+ Nothing -> show obsRealResp+ Just Dict -> concat [+ show obsRealResp+ , " ("+ , show realResp+ , ")"+ ]++ modelReturned = concat [+ show obsMockResp+ , " ("+ , show mockResp+ , ")"+ ]
src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE PatternSynonyms #-}+ -- | Environment parameterised by functor @f@ -- -- Intended for qualified import:@@ -12,6 +14,10 @@ -- * Query , lookup , keysOfType+ , shrinkVar+ -- * Internal: exposed for testing+ , pattern EnvF+ , EnvEntry (..) ) where import Prelude hiding (lookup)@@ -57,3 +63,11 @@ keysOfType :: Typeable a => EnvF f -> [Var a] keysOfType (EnvF env) = mapMaybe (\(EnvEntry var _) -> cast var) env++-- | Shrink a variable to variables of the same type, but with a smaller+-- variable number.+--+-- The numbering of variables is according to their age, meaning that this+-- function shrinks a variable to /earlier/ variables.+shrinkVar :: Typeable a => EnvF f -> Var a -> [Var a]+shrinkVar envf v = [ v' | v' <- keysOfType envf, v' < v ]
src/Test/QuickCheck/StateModel/Lockstep/GVar.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE UndecidableInstances #-} -- | Generalized variables@@ -15,11 +16,14 @@ -- * Interop with 'EnvF' , lookUpEnvF , definedInEnvF+ , shrinkGVar+ -- * Internal: exposed for testing+ , pattern GVar ) where import Prelude hiding (map) -import Data.Maybe (isJust, fromJust)+import Data.Maybe (isJust) import Data.Typeable import GHC.Show@@ -37,7 +41,7 @@ -- | Generalized variables -- -- The key difference between 'GVar' and the standard 'Var' type is that--- 'GVar' have a functor-esque structure: see 'map'.+-- 'GVar' have a functor-esque structure: see 'mapGVar'. data GVar op f where GVar :: Typeable x => Var x -> op x y -> GVar op y @@ -92,13 +96,13 @@ -- | 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'.+-- The result is 'Just' if the variable is in the environment and evaluation+-- succeeds. This is normally guaranteed by the default test 'precondition'. lookUpGVar :: InterpretOp op (WrapRealized m)- => Proxy m -> LookUp m -> GVar op a -> Realized m a+ => Proxy m -> LookUp m -> GVar op a -> Maybe (Realized m a) lookUpGVar p lookUp (GVar var op) =- unwrapRealized $ fromJust $ intOp op (lookUpWrapped p lookUp var)+ unwrapRealized <$> intOp op (lookUpWrapped p lookUp var) {------------------------------------------------------------------------------- Interop with EnvF@@ -106,13 +110,22 @@ -- | 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 $+-- The result is 'Just' if the variable is in the environment and evaluation+-- succeeds. This is normally guaranteed by the default test 'precondition'.+lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Maybe (f a)+lookUpEnvF env (GVar var op) = 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+definedInEnvF env gvar = isJust (lookUpEnvF env gvar)++-- | Shrink a 'GVar' to earlier 'GVar's of the same type. It is guaranteed that+-- the shrunk variables are in the environment and that evaluation will succeed.+shrinkGVar :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> [GVar op a]+shrinkGVar env (GVar var op) =+ [ gvar'+ | var' <- EnvF.shrinkVar env var+ , let gvar' = GVar var' op+ , definedInEnvF env gvar'+ ]
+ test-internals/Main.hs view
@@ -0,0 +1,9 @@+module Main (main) where++import Test.Tasty+import qualified Test.Test.QuickCheck.StateModel.Lockstep.GVar++main :: IO ()+main = defaultMain $ testGroup "quickcheck-lockstep-internals" [+ Test.Test.QuickCheck.StateModel.Lockstep.GVar.tests+ ]
+ test-internals/Test/Test/QuickCheck/StateModel/Lockstep/GVar.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE DerivingStrategies #-}++{-# OPTIONS_GHC -Wno-orphans #-}++module Test.Test.QuickCheck.StateModel.Lockstep.GVar where++import Data.Data (eqT,+ (:~:) (Refl))+import Data.Functor.Identity+import Test.QuickCheck.StateModel.Lockstep.EnvF hiding+ (shrinkVar)+import Test.QuickCheck.StateModel.Lockstep.GVar+import Test.QuickCheck.StateModel.Lockstep.Op+import Test.QuickCheck.StateModel.Lockstep.Op.SumProd+import Test.QuickCheck.StateModel.Variables hiding+ (shrinkVar)+import Test.Tasty+import Test.Tasty.QuickCheck++tests :: TestTree+tests = testGroup "Test.Test.QuickCheck.StateModel.Lockstep.GVar" [+ testProperty "prop_shrinkGVar_wellDefined" $+ forAllShrinkShow genEnvironment shrinkEnvironment showEnvironment $ \env ->+ forAllShrink genGVar shrinkGVar' $ \gvar ->+ prop_shrinkGVar_wellDefinedAndEvaluable env gvar+ ]++{-------------------------------------------------------------------------------+ Well-defined and evaluable shrinks+-------------------------------------------------------------------------------}++-- | Verify that 'GVar's are only shrunk to 'GVar's that are well-defined and+-- evaluable wth respect to the environment.+prop_shrinkGVar_wellDefinedAndEvaluable :: EnvF Identity -> GVar Op Int -> Property+prop_shrinkGVar_wellDefinedAndEvaluable env gvar =+ -- It's not important for the test that the input GVar is well-defined, but+ -- we label the test case anyway to see that the input GVar is /sometimes/+ -- well-defined.+ tabulate "Input GVar is well-defined" [show (definedInEnvF env gvar)] $+ tabulate "Number of shrinks" [show (length shrinks)] $+ conjoin [ prop gvar' | gvar' <- shrinks]+ where+ shrinks = shrinkGVar env gvar++ prop gvar' =+ counterexample ("Shrunk GVar is not in the environment: " ++ show gvar')+ (definedInEnvF env gvar')++{-------------------------------------------------------------------------------+ Well-defined and evaluable shrinks: generators, shrinkers, printers+-------------------------------------------------------------------------------}++instance InterpretOp Op Identity where+ intOp op = traverse (intOpId op)++-- NOTE: both the environment and variables contain/are existential types, which+-- can get a little bit complicated when writing generators, shrinkers and+-- printers. Thus for simplicity, we take a dynamic typing approach that throws+-- errors once we encounter a type that we did not expect. It does make+-- functions partial and the code a little bit ugly, but it works well enough+-- for testing well-defined and evaluable shrinks.++-- With just two types of 'Var's, we can test most interesting cases of+-- (non-)well-defined and (non-)successful evaluation.+type T1 = Either Int Char+type T2 = Either Char Int++-- | Generate an environment that maps 'T1' and 'T2' variables to 'T1' and 'T2' values+-- respectively.+genEnvironment :: Gen (EnvF Identity)+genEnvironment = do+ NonNegative (Small n) <- arbitrary+ genInsert empty n+ where+ genInsert :: EnvF Identity -> Int -> Gen (EnvF Identity)+ genInsert acc 0 = pure acc+ genInsert acc n = do+ b <- elements [True, False]+ if b then do+ var <- genVar+ x <- genValue1+ genInsert (insert var (Identity x) acc) (n-1)+ else do+ var <- genVar+ x <- genValue2+ genInsert (insert var (Identity x) acc) (n-1)++shrinkEnvironment :: EnvF Identity -> [EnvF Identity]+shrinkEnvironment (EnvF xs) = EnvF <$> liftShrink shrinkEntry xs++-- | Shrink each entry individually, but also shrink T1 entries towards T2 entries+shrinkEntry :: EnvEntry Identity -> [EnvEntry Identity]+shrinkEntry (EnvEntry (var :: Var a) (Identity x))+ -- A T1 entry+ | Just Refl <- eqT @a @T1+ = -- Shrink either the variable, or shrink the value, or ...+ [ EnvEntry var' (Identity x')+ | (var', x') <- liftShrink2 shrinkVar shrinkValue1 (var, x)+ ] +++ -- ... shrink towards a T2 entry+ [ EnvEntry (unsafeCoerceVar var :: Var T2) (Identity x')+ | x' <- case x of+ Left y -> [Right y]+ Right{} -> []+ ]+ -- A T2 entry+ | Just Refl <- eqT @a @T2+ = -- Shrink either the variable, or shrink the value+ [ EnvEntry var' (Identity x')+ | (var', x') <- liftShrink2 shrinkVar shrinkValue2 (var, x)+ ]+ | otherwise+ = error "shrinkEntry"++showEnvironment :: EnvF Identity -> String+showEnvironment (EnvF xs) = "EnvF " ++ "[" ++ concatMap showEntry xs ++ "]"++showEntry :: EnvEntry Identity -> String+showEntry (EnvEntry (var :: Var a) x)+ | Just Refl <- eqT @a @T1+ = "EnvEntry " ++ show var ++ " (" ++ show x ++ ")"+ | Just Refl <- eqT @a @T2+ = "EnvEntry " ++ show var ++ " (" ++ show x ++ ")"+ | otherwise+ = error "showEntry"++-- | Generate a T1 or T2 variable+genGVar :: Gen (GVar Op Int)+genGVar = oneof [+ do var <- genVar+ pure (unsafeMkGVar (var :: Var T1) OpLeft)+ , do var <- genVar+ pure (unsafeMkGVar (var :: Var T2) OpRight)+ ]++shrinkGVar' :: GVar Op Int -> [GVar Op Int]+shrinkGVar' (GVar (var :: Var a) op)+ | Just Refl <- eqT @a @T1+ = [ unsafeMkGVar var' op+ | var' <- shrinkVar var+ ] ++ [+ unsafeMkGVar (unsafeCoerceVar var :: Var T2) OpRight+ ]+ | Just Refl <- eqT @a @T2+ = [ unsafeMkGVar var' op+ | var' <- shrinkVar var+ ]+ | otherwise+ = error "shrink'GVar"++genVar :: Gen (Var a)+genVar = mkVar <$> arbitrary++shrinkVar :: Var a -> [Var a]+shrinkVar var = [ mkVar x' | x' <- shrink x]+ where+ -- Hacky: the constructor for 'Var' is not exposed, but we can obtain the+ -- wrapped integer by reading it from the show output.+ --+ -- The show instance looks like:+ --+ -- > data Var = Var Int+ -- > show (Var x) = "var" ++ show x+ x = read (drop 3 (show var))++genValue1 :: Gen T1+genValue1 = arbitrary++shrinkValue1 :: T1 -> [T1]+shrinkValue1 = shrink++genValue2 :: Gen T2+genValue2 = arbitrary++shrinkValue2 :: T2 -> [T2]+shrinkValue2 = shrink
test/Main.hs view
@@ -1,14 +1,16 @@ module Main (main) where -import Test.Tasty+import Test.Tasty -import Test.IORef.Full qualified-import Test.IORef.Simple qualified-import Test.MockFS qualified+import Test.Golden+import Test.IORef.Full+import Test.IORef.Simple+import Test.MockFS main :: IO () main = defaultMain $ testGroup "quickcheck-lockstep" [- Test.IORef.Simple.tests+ Test.Golden.tests+ , Test.IORef.Simple.tests , Test.IORef.Full.tests , Test.MockFS.tests ]
+ test/Test/Golden.hs view
@@ -0,0 +1,107 @@+{- HLINT ignore "Use camelCase" -}++module Test.Golden where++import Control.Exception (bracket_)+import System.Directory+import System.FilePath+import Test.MockFS as MockFS+import Test.QuickCheck+import Test.QuickCheck.Random (mkQCGen)+import Test.Tasty+import Test.Tasty.Golden++tests :: TestTree+tests = testGroup "Test.Golden" [+ golden_success_propLockstep_MockFS+ , golden_failure_default_propLockstep_MockFS+ , golden_failure_nonVerbose_propLockstep_MockFS+ , golden_failure_verbose_propLockstep_MockFS+ ]++goldenDir :: FilePath+goldenDir = "test" </> "golden"++tmpDir :: FilePath+tmpDir = "_tmp"++-- | Golden test for a successful lockstep test+golden_success_propLockstep_MockFS :: TestTree+golden_success_propLockstep_MockFS =+ goldenVsFile testName goldenPath outputPath $ do+ createDirectoryIfMissing False tmpDir+ r <- quickCheckWithResult args MockFS.propLockstep+ writeFile outputPath (output r)+ where+ testName = "golden_success_propLockstep_MockFS"+ goldenPath = goldenDir </> testName <.> "golden"+ outputPath = tmpDir </> testName <.> "golden"++ args = stdArgs {+ replay = Just (mkQCGen 17, 32)+ , chatty = False+ }++-- | Golden test for a failing lockstep test that produces a counterexample+-- using the default postcondition.+golden_failure_default_propLockstep_MockFS :: TestTree+golden_failure_default_propLockstep_MockFS =+ goldenVsFile testName goldenPath outputPath $ do+ createDirectoryIfMissing False tmpDir+ r <-+ bracket_+ MockFS.setInduceFault+ MockFS.setNoInduceFault+ (quickCheckWithResult args MockFS.propLockstep)+ writeFile outputPath (output r)+ where+ testName = "golden_failure_default_propLockstep_MockFS"+ goldenPath = goldenDir </> testName <.> "golden"+ outputPath = tmpDir </> testName <.> "golden"++ args = stdArgs {+ replay = Just (mkQCGen 17, 32)+ , chatty = False+ }++-- | Golden test for a failing lockstep test that produces a /non-verbose/ counterexample+golden_failure_nonVerbose_propLockstep_MockFS :: TestTree+golden_failure_nonVerbose_propLockstep_MockFS =+ goldenVsFile testName goldenPath outputPath $ do+ createDirectoryIfMissing False tmpDir+ r <-+ bracket_+ (MockFS.setInduceFault >> MockFS.setPostconditionNonVerbose)+ (MockFS.setNoInduceFault >> MockFS.setPostconditionDefault)+ (quickCheckWithResult args MockFS.propLockstep)+ writeFile outputPath (output r)+ where+ testName = "golden_failure_nonVerbose_propLockstep_MockFS"+ goldenPath = goldenDir </> testName <.> "golden"+ outputPath = tmpDir </> testName <.> "golden"++ args = stdArgs {+ replay = Just (mkQCGen 17, 32)+ , chatty = False+ }++-- | Golden test for a failing lockstep test that produces a /verbose/ counterexample+golden_failure_verbose_propLockstep_MockFS :: TestTree+golden_failure_verbose_propLockstep_MockFS =+ goldenVsFile testName goldenPath outputPath $ do+ createDirectoryIfMissing False tmpDir+ r <-+ bracket_+ (MockFS.setInduceFault >> MockFS.setPostconditionVerbose)+ (MockFS.setNoInduceFault >> MockFS.setPostconditionDefault)+ (quickCheckWithResult args MockFS.propLockstep)+ writeFile outputPath (output r)+ where+ testName = "golden_failure_verbose_propLockstep_MockFS"+ goldenPath = goldenDir </> testName <.> "golden"+ outputPath = tmpDir </> testName <.> "golden"++ args = stdArgs {+ replay = Just (mkQCGen 17, 32)+ , chatty = False+ }
test/Test/IORef/Full.hs view
@@ -208,11 +208,11 @@ Read v -> readIORef (lookUpRef v) where lookUpRef :: ModelVar M (IORef Int) -> IORef Int- lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp+ lookUpRef = realLookupVar (Proxy @RealMonad) lookUp lookUpInt :: Either Int (ModelVar M Int) -> Int lookUpInt (Left x) = x- lookUpInt (Right v) = lookUpGVar (Proxy @RealMonad) lookUp v+ lookUpInt (Right v) = realLookupVar (Proxy @RealMonad) lookUp v -- | The second write to the same variable will be broken brokenWrite :: Buggy -> IORef BrokenRef -> IORef Int -> Int -> IO Int
test/Test/IORef/Simple.hs view
@@ -155,7 +155,7 @@ Read v -> readIORef (lookUpRef v) where lookUpRef :: ModelVar M (IORef Int) -> IORef Int- lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp+ lookUpRef = realLookupVar (Proxy @RealMonad) lookUp runModel :: Action (Lockstep M) a
test/Test/MockFS.hs view
@@ -11,14 +11,27 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -module Test.MockFS (tests) where+module Test.MockFS (+ tests+ , propLockstep+ -- * Unsafe: induce test failure+ , setInduceFault+ , setNoInduceFault+ -- * Unsafe: set postcondition+ , setPostconditionDefault+ , setPostconditionNonVerbose+ , setPostconditionVerbose+ ) where import Prelude hiding (init) import Control.Exception (catch, throwIO) import Control.Monad (replicateM, (<=<)) import Control.Monad.Reader (ReaderT (..))+import Control.Monad.Trans (lift) import Data.Bifunctor+import Data.Constraint+import Data.IORef import Data.Set (Set) import Data.Set qualified as Set import Data.Typeable@@ -26,6 +39,7 @@ import System.Directory qualified as IO import System.IO qualified as IO import System.IO.Temp (createTempDirectory, getCanonicalTemporaryDirectory)+import System.IO.Unsafe (unsafePerformIO) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit import Test.Tasty.QuickCheck (testProperty)@@ -83,7 +97,9 @@ instance RunModel (Lockstep FsState) RealMonad where perform = \_st -> runIO- postcondition = Lockstep.postcondition+ postcondition states action lookUp result = do+ pc <- lift $ lift getPostcondition+ runPostcondition pc states action lookUp result monitoring = Lockstep.monitoring (Proxy @RealMonad) deriving instance Show (Action (Lockstep FsState) a)@@ -203,6 +219,13 @@ Close{} -> OEither . bimap OId OId Read{} -> OEither . bimap OId OId + showRealResponse _ = \case+ MkDir{} -> Just Dict+ Open{} -> Nothing+ Write{} -> Just Dict+ Close{} -> Just Dict+ Read{} -> Just Dict+ {------------------------------------------------------------------------------- Interpreter against the model -------------------------------------------------------------------------------}@@ -320,11 +343,15 @@ IO.hPutStr (lookUp' h) s Close h -> catchErr $ IO.hClose (lookUp' h)- Read f -> catchErr $- IO.readFile (Mock.fileFP root $ either lookUp' id f)+ Read f -> catchErr $ do+ fault <- getFaultRef+ s <- IO.readFile (Mock.fileFP root $ either lookUp' id f)+ case fault of+ Fault | length s >= 3 -> pure ""+ _ -> pure s where lookUp' :: FsVar x -> x- lookUp' = lookUpGVar (Proxy @RealMonad) lookUp+ lookUp' = realLookupVar (Proxy @RealMonad) lookUp catchErr :: forall a. IO a -> IO (Either Err a) catchErr act = catch (Right <$> act) handler@@ -365,14 +392,91 @@ tests = testGroup "Test.MockFS" [ testCase "labelledExamples" $ QC.labelledExamples $ Lockstep.tagActions (Proxy @FsState)- , testProperty "propLockstep" $- Lockstep.runActionsBracket (Proxy @FsState)- (createSystemTempDirectory "QSM")- removeDirectoryRecursive- runReaderT+ , testProperty "propLockstep" propLockstep ] +propLockstep :: Actions (Lockstep FsState) -> QC.Property+propLockstep =+ Lockstep.runActionsBracket (Proxy @FsState)+ (createSystemTempDirectory "QSM")+ removeDirectoryRecursive+ runReaderT+ createSystemTempDirectory :: [Char] -> IO FilePath createSystemTempDirectory prefix = do systemTempDir <- getCanonicalTemporaryDirectory createTempDirectory systemTempDir prefix++{-------------------------------------------------------------------------------+ Unsafe: induce test failure+-------------------------------------------------------------------------------}++data Fault = Fault | NoFault+ deriving Eq++{-# NOINLINE faultRef #-}+-- | A mutable variable that can be set globally to induce test failures in+-- 'propLockstep'. This is used in "Test.Golden" to golden test counterexamples+-- as produced by the @quickcheck-lockstep@.+faultRef :: IORef Fault+faultRef = unsafePerformIO $ newIORef NoFault++{-# NOINLINE getFaultRef #-}+getFaultRef :: IO Fault+getFaultRef = readIORef faultRef++{-# NOINLINE setFaultRef #-}+setFaultRef :: Fault -> IO ()+setFaultRef = writeIORef faultRef++{-# NOINLINE setInduceFault #-}+setInduceFault :: IO ()+setInduceFault = setFaultRef Fault++{-# NOINLINE setNoInduceFault #-}+setNoInduceFault :: IO ()+setNoInduceFault = setFaultRef NoFault++{-------------------------------------------------------------------------------+ Unsafe: set postcondition+-------------------------------------------------------------------------------}++data Postcondition =+ DefaultPostcondition+ | NonVerbosePostcondition+ | VerbosePostcondition++runPostcondition ::+ Postcondition+ -> (Lockstep FsState, Lockstep FsState)+ -> Action (Lockstep FsState) a+ -> LookUp RealMonad+ -> Realized RealMonad a+ -> PostconditionM RealMonad Bool+runPostcondition DefaultPostcondition = Lockstep.postcondition+runPostcondition NonVerbosePostcondition = Lockstep.postconditionWith False+runPostcondition VerbosePostcondition = Lockstep.postconditionWith True++{-# NOINLINE postconditionRef #-}+postconditionRef :: IORef Postcondition+postconditionRef = unsafePerformIO $ newIORef DefaultPostcondition++{-# NOINLINE getPostcondition #-}+getPostcondition :: IO Postcondition+getPostcondition = readIORef postconditionRef++{-# NOINLINE setPostconditionDefault #-}+setPostconditionDefault :: IO ()+setPostconditionDefault = setPostcondition VerbosePostcondition++{-# NOINLINE setPostconditionVerbose #-}+setPostconditionVerbose :: IO ()+setPostconditionVerbose = setPostcondition VerbosePostcondition++{-# NOINLINE setPostconditionNonVerbose #-}+setPostconditionNonVerbose :: IO ()+setPostconditionNonVerbose = setPostcondition NonVerbosePostcondition++{-# NOINLINE setPostcondition #-}+setPostcondition :: Postcondition -> IO ()+setPostcondition = writeIORef postconditionRef