IORefPrePostConditionQuickCheck.hs

{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeFamilies               #-}

module IORefPrePostConditionQuickCheck where

import           Control.Lens            hiding (pre)
import           Control.Monad.Free
import           Control.Monad.Free.TH
import           Control.Monad.State
import           Data.IORef
import           Test.QuickCheck
import           Test.QuickCheck.Monadic

------------------------------------------------------------------------

newtype Ref = Ref Int
  deriving (Eq, Show, Read, Num, Ord)

makeWrapped ''Ref

data MemStepF ref
  = New
  | Read ref
  | Write ref Int
  deriving (Show, Eq, Read, Functor)

type MemStep = MemStepF Ref

newtype Mem = Mem [MemStep]
  deriving (Show, Eq, Monoid, Read)

makeWrapped ''Mem

------------------------------------------------------------------------

type Model = [Int]

new_pre :: Model -> Bool
new_pre _ = True

new_next :: Model -> () -> Ref -> Model
new_next m _ ref = m ++ [0]

new_post :: Model -> () -> Ref -> Bool
new_post _ _ _ = True


read_pre :: Model -> Bool
read_pre = not . null

read_next :: Model -> Ref -> Int -> Model
read_next m _ _ = m

read_post :: Model -> Ref -> Int -> Bool
read_post m ref r = m !! op Ref ref == r && read_next m ref r == m


write_pre :: Model -> Bool
write_pre = not . null

write_next :: Model -> (Ref, Int) -> () -> Model
write_next m (ref, i) _ = m & element (op Ref ref) .~ i

write_post :: Model -> (Ref, Int) -> () -> Bool
write_post m (ref, i) _ = write_next m (ref, i) () !! op Ref ref == i

------------------------------------------------------------------------

type OurMonad m = (MonadIO m, MonadState Env m)

type Env = [IORef Int]

data Type = RefT (IORef Int) | IntT Int | UnitT

semStep :: OurMonad m => MemStep -> m Type
semStep New              = do
  len <- length <$> get
  ref <- liftIO $ newIORef 0
  id %= (++ [ref])
  return $ RefT ref
semStep (Read ref)       = do
  e <- get
  i <- liftIO $ readIORef $ e !! op Ref ref
  return $ IntT i
semStep (Write ref i)    = do
  e <- get
  if i `elem` [5..10]
    -- Introduce a bug:
    then liftIO $ writeIORef (e !! op Ref ref) $ i + 1
    else liftIO $ writeIORef (e !! op Ref ref) $ i
  return UnitT

sem :: OurMonad m => Mem -> m ()
sem = foldM (\ih m -> semStep m >> return ih) () . op Mem

runMemm :: Mem -> IO ()
runMemm m = do
  putStrLn ""
  (t, env) <- flip runStateT [] $ sem m
  putStrLn ""
  forM_ (zip [0..] env) $ \(i, ref) -> do
    v <- readIORef ref
    putStrLn $ "$" ++ show i ++ ": " ++ show v
  return ()

------------------------------------------------------------------------

gen1 :: Model -> Gen (MemStep, Model)
gen1 m = frequency
  [ (if new_pre   m then 1 else 0, new_gen   m)
  , (if read_pre  m then 5 else 0, read_gen  m)
  , (if write_pre m then 5 else 0, write_gen m)
  ]
  where
  new_gen :: Model -> Gen (MemStep, Model)
  new_gen m = return (New, m ++ [0])

  read_gen :: Model -> Gen (MemStep, Model)
  read_gen m = do
    ref <- Ref <$> choose (0, length m - 1)
    return (Read ref, m) -- read_next m ref (m !! (op Ref ref)))

  write_gen :: Model -> Gen (MemStep, Model)
  write_gen m = do
    ref <- Ref <$> choose (0, length m - 1)
    i   <- arbitrary
    return (Write ref i, write_next m (ref, i) ())

genMem :: Gen Mem
genMem = sized $ go []
  where
  go :: Model -> Int -> Gen Mem
  go m 0 = return $ Mem []
  go m n = do
    (mem, m') <- gen1 m
    Mem ih    <- go m' (n - 1)
    return $ Mem $ mem : ih

------------------------------------------------------------------------

instance Arbitrary Mem where
  arbitrary = genMem
  shrink    = map Mem . shrinkMem . op Mem

shrinkMem :: [MemStep] -> [[MemStep]]
shrinkMem []                 = []
shrinkMem (New         : ms) =
  [ [] ]
  ++ [ map (fmap (\ref -> max 0 (ref - 1))) ms ]
  ++ [ New : ms' | ms' <- shrinkMem ms ]
shrinkMem (Read ref    : ms) =
  [ [] ]
  ++ [ ms ]
  ++ [ Read ref     : ms' | ms' <- shrinkMem ms ]
shrinkMem (Write ref i : ms) =
  [ [] ]
  ++ [ ms ]
  ++ [ Write ref i' : ms' | (i', Mem ms') <- shrink (i, Mem ms) ]

------------------------------------------------------------------------

monadicOur :: PropertyM (StateT Env IO) () -> Property
monadicOur = monadic $ ioProperty . flip evalStateT []

prop_safety :: Property
prop_safety = forAllShrink genMem shrink $ monadicOur . go [] . op Mem
  where
  go :: OurMonad m => Model -> [MemStep] -> PropertyM m ()
  go _ []                     = return ()
  go m (New : ms)             = do
    monitor $ collect "new"
    pre $ new_pre m
    r <- run $ semStep New
    case r of
      RefT ref -> do
        -- We don't have a model ref here.
        -- let r = undefined
        -- assert' "`new_post'" $ new_post m () r
        -- go (new_next m () r) ms
        go (m ++ [0]) ms
      _ -> fail "not ref"
  go m (Read ref : ms)        = do
    monitor $ collect "read"
    pre $ read_pre m
    r <- run $ semStep $ Read ref
    case r of
      IntT i -> do
        assert' ("`read_post': read " ++ show ref ++ " ["++ show i ++ "]")
            $ read_post m ref i
        go (read_next m ref i) ms
      _ -> fail "not int"
  go m (Write ref i : ms) = do
    monitor $ collect "write"
    pre $ write_pre m
    r <- run $ semStep $ Write ref i
    case r of
      UnitT -> do
        assert' "`write_post'" $ write_post m (ref, i) ()
        go (write_next m (ref, i) ()) ms
      _ -> fail "not unit"

assert' :: Monad m => String -> Bool -> PropertyM m ()
assert' msg True  = return ()
assert' msg False = fail $ msg ++ " failed"

testP :: IO ()
testP = verboseCheckWith stdArgs prop_safety

prop_shrink :: Property
prop_shrink = monadicIO $ do
  result <- run $ quickCheckWithResult (stdArgs {chatty = False}) prop_safety
  case result of
    Failure { output = output } -> do
      let lastLine = last $ lines output
      assert $ lastLine == "Mem [New,Write (Ref 0) 5,Read (Ref 0)]"
    _                           -> return ()

testS :: IO ()
testS = quickCheckWith (stdArgs { maxSuccess = 500 }) prop_shrink