{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module Bookstore ( Bug(..) , prop_bookstore , cleanup , setup ) where import Control.Concurrent (threadDelay) import Control.Monad.Reader (ReaderT, ask, runReaderT) import Data.Int (Int64) import Data.Kind (Type) import Data.List (dropWhileEnd, group, inits, isInfixOf, sort, tails) import Data.Maybe (fromJust) import Database.PostgreSQL.Simple as PS (ConnectInfo, Connection, Query, close, connect, connectDatabase, connectHost, connectPassword, connectPort, connectUser, defaultConnectInfo, execute, execute_, query) import Database.PostgreSQL.Simple.Errors (ConstraintViolation(..), catchViolation) import Database.PostgreSQL.Simple.FromRow (FromRow(fromRow), field) import GHC.Generics (Generic, Generic1) import Network.Socket as Sock (AddrInfoFlag(AI_NUMERICHOST, AI_NUMERICSERV), Socket, SocketType(Stream), addrAddress, addrFamily, addrFlags, addrProtocol, addrSocketType, close, connect, defaultHints, getAddrInfo, socket) import Prelude import System.Process (callProcess, readProcess) import Test.QuickCheck (Arbitrary(arbitrary), Gen, Property, arbitraryPrintableChar, choose, elements, frequency, ioProperty, listOf, oneof, shrink, suchThat, vectorOf, (===)) import Test.QuickCheck.Monadic (monadic) import UnliftIO (IOException, bracket, catch, liftIO, onException, throwIO) import Test.StateMachine import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Z (codomain, domain) ------------------------------------------------------------------------ -- Based on Bookstore case study from: -- https://propertesting.com/book_case_study_stateful_properties_with_a_bookstore.html -- System under test: Parametrized SQL statements data Book = Book { isbn :: String , title :: String , author :: String , owned :: Int , avail :: Int } deriving stock (Eq, Show, Generic) instance ToExpr Book where instance FromRow Book where fromRow = Book <$> field <*> field <*> field <*> field <*> field handleViolations :: (Connection -> IO a) -> Connection -> IO (Maybe a) handleViolations fn cn = catchViolation catcher (Just <$> fn cn) where catcher _ (UniqueViolation _) = return Nothing catcher e _ = throwIO e setupTable :: Connection -> IO (Maybe Int64) setupTable = handleViolations $ \cn -> execute_ cn "CREATE TABLE books (\ \ isbn varchar(20) PRIMARY KEY,\ \ title varchar(256) NOT NULL,\ \ author varchar(256) NOT NULL,\ \ owned smallint DEFAULT 0,\ \ available smallint DEFAULT 0\ \ )" teardown :: Connection -> IO (Maybe Int64) teardown = handleViolations $ \cn -> execute_ cn "DROP TABLE books" addBook :: String -> String -> String -> Connection -> IO (Maybe Int64) addBook isbn_ title_ auth = handleViolations $ \cn -> execute cn templ (isbn_, title_, auth) where templ = "INSERT INTO books (isbn, title, author, owned, available)\ \ VALUES ( ?, ?, ?, 0, 0 )" update :: Query -> String -> Connection -> IO Int64 update prepStmt param cn = execute cn prepStmt [param] addCopy :: String -> Connection -> IO (Maybe Int64) addCopy isbn_ = handleViolations $ update templ isbn_ where templ = "UPDATE books SET\ \ owned = owned + 1,\ \ available = available + 1\ \ WHERE isbn = ?" borrowCopy :: String -> Connection -> IO (Maybe Int64) borrowCopy isbn_ = handleViolations (update templ isbn_) where templ = "UPDATE books SET available = available - 1 \ \ WHERE isbn = ? AND available > 0" returnCopy :: Bug -> String -> Connection -> IO (Maybe Int64) returnCopy bug isbn_ = handleViolations (update templ isbn_) where templ = if bug == Bug then "UPDATE books SET available = available + 1 WHERE isbn = ?;" else "UPDATE books SET available = available + 1\ \ WHERE isbn = ? AND available < owned;" select :: Query -> String -> Connection -> IO [Book] select prepStmt param cn = query cn prepStmt [param] findByAuthor, findByTitle :: Bug -> String -> Connection -> IO (Maybe [Book]) findByAuthor bug s = case bug of Injection -> handleViolations (select templ $ "%"++s++"%") _ -> handleViolations (select templ $ "%"++(sanitize s)++"%") where templ = "SELECT * FROM books WHERE author LIKE ?" findByTitle bug s = case bug of Injection -> handleViolations (select templ $ "%"++s++"%") _ -> handleViolations (select templ $ "%"++(sanitize s)++"%") where templ = "SELECT * FROM books WHERE title LIKE ?" findByIsbn :: String -> Connection -> IO (Maybe [Book]) findByIsbn s = handleViolations $ select "SELECT * FROM books WHERE isbn = ?" s -- XXX sanitize :: String -> String sanitize = concatMap (\c -> if c `elem` ['_', '%', '\\'] then '\\':[c] else [c]) withConnection :: ConnectInfo -> (Connection -> IO a) -> IO a withConnection connInfo = bracket (PS.connect connInfo) PS.close -- Modeling newtype Model r = Model [(Isbn, Book)] deriving stock (Generic, Show) instance ToExpr (Model Concrete) where initModel :: Model v initModel = Model [] newtype Isbn = Isbn { getString :: String } deriving stock (Eq, Show) instance ToExpr Isbn where toExpr = toExpr . show instance Arbitrary Isbn where arbitrary = oneof [isbn10, isbn13] where isbn10 = do gr <- isbnGroup t <- pubTitle (9 - length gr) c <- elements ('X':['0'..'9']) return $ Isbn (gr ++ "-" ++ t ++ "-" ++ [c]) isbn13 = do code <- elements ["978", "979"] Isbn x <- isbn10 return $ Isbn (code ++ "-" ++ x) isbnGroup :: Gen String isbnGroup = elements $ show <$> concat [ [0..5] :: [Integer] , [7] , [80..94] , [600..621] , [950..989] , [9926..9989] , [99901..99976] ] pubTitle :: Int -> Gen String pubTitle size = do i <- choose (1, size - 1) v1 <- vectorOf i $ choose ('0', '9') v2 <- vectorOf (size - i) $ choose ('0', '9') return $ v1 ++ "-" ++ v2 data Tag = New | Exist | Invalid | Avail | Unavail | Taken | Full deriving stock (Eq, Show) data Command (r :: Type -> Type) = NewBook Tag Isbn String String | AddCopy Tag Isbn | Borrow Tag Isbn | Return Tag Isbn | FindByAuthor Tag String | FindByTitle Tag String | FindByIsbn Tag Isbn deriving stock (Show, Generic1) instance Rank2.Foldable Command where instance Rank2.Functor Command where instance Rank2.Traversable Command where data Response (r :: Type -> Type) = Rows [Book] | Updated | Inserted | NotFound | UniqueError | OtherError deriving stock (Eq, Show, Generic1) instance Rank2.Foldable Response where generator :: Model Symbolic -> Maybe (Gen (Command Symbolic)) generator (Model m) = Just $ oneof $ [ NewBook New <$> newIsbn <*> stringGen <*> stringGen , AddCopy Invalid <$> newIsbn , Borrow Invalid <$> newIsbn , Return Invalid <$> newIsbn , FindByIsbn Invalid <$> newIsbn , FindByTitle Invalid <$> searchStringGen , FindByAuthor Invalid <$> searchStringGen ] ++ if null m then [] else [ NewBook Exist <$> existIsbn <*> stringGen <*> stringGen , AddCopy Exist <$> existIsbn , Borrow Avail <$> existIsbn , Borrow Unavail <$> existIsbn , Return Taken <$> existIsbn , Return Full <$> existIsbn , FindByIsbn Exist <$> existIsbn , FindByTitle Exist <$> genTitle , FindByAuthor Exist <$> genAuthor ] where newIsbn = arbitrary `suchThat` \x -> x `notElem` domain m existIsbn = elements $ domain m genTitle = elements $ (title <$> codomain m) >>= infixes genAuthor = elements $ (author <$> codomain m) >>= infixes stringGen :: Gen String stringGen = listOf arbitraryPrintableChar searchStringGen :: Gen String searchStringGen = listOf $ frequency [ (7, arbitraryPrintableChar) , (3, elements ['_', '%']) ] infixes :: Ord a => [a] -> [[a]] infixes l = map head . group . sort $ inits l >>= tails -- How to shrink Commands shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic] shrinker _ (NewBook tag key x y) = [ NewBook tag key x y' | y' <- shrink y ] ++ [ NewBook tag key x' y | x' <- shrink x ] shrinker _ (FindByAuthor tag a) = [ FindByAuthor tag a' | a' <- shrink a ] shrinker _ (FindByTitle tag t) = [ FindByTitle tag t' | t' <- shrink t ] shrinker _ _ = [] -- Pre-requisites and invariants preconditions :: Model Symbolic -> Command Symbolic -> Logic preconditions (Model m) cmd = case cmd of AddCopy Invalid key -> Not $ hasKey key Borrow Invalid key -> Not $ hasKey key Return Invalid key -> Not $ hasKey key FindByIsbn Invalid key -> Not $ hasKey key NewBook New key _ _ -> Not $ hasKey key NewBook Exist key _ _ -> hasKey key AddCopy Exist key -> hasKey key FindByIsbn Exist key -> hasKey key Borrow Avail key -> keyPred key (\b -> avail b .> 0) Borrow Unavail key -> keyPred key (\b -> avail b .== 0) Return Taken key -> keyPred key (\b -> owned b .> avail b) Return Full key -> keyPred key (\b -> owned b .== avail b) FindByAuthor Invalid x -> Not $ Exists values (Boolean . isInfixOf x . author) FindByTitle Invalid x -> Not $ Exists values (Boolean . isInfixOf x . title) FindByTitle Exist x -> Exists values (Boolean . isInfixOf x . title) _ -> Top where values = codomain m hasKey key = key `member` (domain m) keyPred key p = maybe Bot p (lookup key m) postconditions :: Model Concrete -> Command Concrete -> Response Concrete -> Logic postconditions (Model m) cmd resp = case cmd of NewBook Exist _ _ _ -> resp .== UniqueError NewBook New _ _ _ -> resp .== Inserted AddCopy Invalid _ -> resp .== NotFound Return Invalid _ -> resp .== NotFound Borrow Invalid _ -> resp .== NotFound Return Full _ -> resp .== NotFound Borrow Unavail _ -> resp .== NotFound Borrow Avail _ -> resp .== Updated AddCopy Exist _ -> resp .== Updated Return Taken _ -> resp .== Updated FindByIsbn Invalid _ -> resp .== Rows [] FindByAuthor Invalid _ -> resp .== Rows [] FindByTitle Invalid _ -> resp .== Rows [] FindByIsbn Exist key -> case lookup key m of Just x -> Rows [x] .== resp _ -> error "Should not happen" FindByAuthor Exist x -> case resp of Rows rs -> Forall rs (Boolean . isInfixOf x . author) .&& Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m) _ -> Bot .// "findByAuthor returned " ++ (show resp) FindByTitle Exist x -> case resp of Rows rs -> Forall rs (Boolean . isInfixOf x . title) .&& Forall rs (\b -> Just b .== lookup (Isbn $ isbn b) m) _ -> Bot .// "findByTitle returned " ++ (show resp) _ -> Bot -- Transitions of the state machine that models SUT transitions :: Model r -> Command r -> Response r -> Model r transitions (Model m) cmd _ = Model $ case cmd of NewBook New key t a -> (key, Book (getString key) t a 0 0):m AddCopy Exist key -> map (applyForKey key $ incOwned . incAvail) m Borrow Avail key -> map (applyForKey key decAvail) m Return Taken key -> map (applyForKey key incAvail) m _ -> m where applyForKey key fn (k, v) = (k, if k == key then fn v else v) incOwned row = row { owned = 1 + owned row } incAvail row = row { avail = 1 + avail row } decAvail row = row { avail = (avail row) - 1 } -- Semantics data Bug = Bug | NoBug | Injection deriving stock Eq semantics :: Bug -> Command Concrete -> ReaderT ConnectInfo IO (Response Concrete) semantics bug cmd = do connInfo <- ask liftIO $ withConnection connInfo $ \cn -> case cmd of NewBook _ (Isbn key) t a -> toResp insertRes <$> addBook key t a cn AddCopy _ (Isbn key) -> toResp updateRes <$> addCopy key cn Borrow _ (Isbn key) -> toResp updateRes <$> borrowCopy key cn Return _ (Isbn key) -> toResp updateRes <$> returnCopy bug key cn FindByAuthor _ x -> toResp Rows <$> findByAuthor bug x cn FindByTitle _ x -> toResp Rows <$> findByTitle bug x cn FindByIsbn _ (Isbn key) -> toResp Rows <$> findByIsbn key cn where toResp = maybe UniqueError updateRes 0 = NotFound updateRes 1 = Updated updateRes _ = OtherError insertRes 1 = Inserted insertRes _ = OtherError -- Mock is currently not used by the library mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic) mock (Model m) cmd = return $ case cmd of NewBook New _ _ _ -> Inserted NewBook Exist _ _ _ -> UniqueError AddCopy Invalid _ -> NotFound AddCopy Exist _ -> Updated Borrow Invalid _ -> NotFound Borrow Avail _ -> Updated Borrow Unavail _ -> NotFound Return Invalid _ -> NotFound Return Taken _ -> Updated Return Full _ -> NotFound FindByTitle Exist x -> Rows $ filter (isInfixOf x . title) (codomain m) FindByAuthor Exist x -> Rows $ filter (isInfixOf x . author) (codomain m) FindByIsbn Exist key -> Rows [fromJust (lookup key m)] FindByTitle Invalid _ -> Rows [] FindByIsbn Invalid _ -> Rows [] FindByAuthor Invalid _ -> Rows [] _ -> error $ (show cmd) ++ " should not happen" -- Property sm :: Bug -> StateMachine Model Command (ReaderT ConnectInfo IO) Response sm bug = StateMachine initModel transitions preconditions postconditions Nothing generator shrinker (semantics bug) mock noCleanup runner :: IO String -> ReaderT ConnectInfo IO Property -> IO Property runner io p = do dbIp <- io let connInfo = defaultConnectInfo { connectUser = "postgres" , connectPassword = "mysecretpassword" , connectDatabase = "postgres" , connectPort = 5432 , connectHost = dbIp } bracket (withConnection connInfo setupTable) (const (withConnection connInfo teardown)) (const (runReaderT p connInfo)) prop_bookstore :: Bug -> IO String -> Property prop_bookstore bug io = forAllCommands sm' Nothing $ \cmds -> monadic (ioProperty . runner io) $ do (hist, _, res) <- runCommands sm' cmds prettyCommands sm' hist $ res === Ok where sm' = sm bug -- Setup PostgreSQL db in Docker setup :: IO (String, String) setup = do pid <- trim <$> readProcess "docker" [ "run" , "-d" , "-e", "POSTGRES_PASSWORD=mysecretpassword" , "postgres:10.2" ] "" ip <- trim <$> readProcess "docker" [ "inspect" , pid , "--format" , "'{{range .NetworkSettings.Networks}}{{.IPAddress}}{{end}}'" ] "" healthyDb pid ip `onException` callProcess "docker" [ "rm", "-f", "-v", pid ] return (pid, ip) where trim :: String -> String trim = dropWhileEnd isGarbage . dropWhile isGarbage where isGarbage = flip elem ['\'', '\n'] healthyDb :: String -> String -> IO () healthyDb pid ip = do sock <- go 10 Sock.close sock where go :: Int -> IO Socket go 0 = error "healthyDb: db isn't healthy" go n = do let hints = defaultHints { addrFlags = [AI_NUMERICHOST , AI_NUMERICSERV] , addrSocketType = Stream } addr : _ <- getAddrInfo (Just hints) (Just ip) (Just "5432") sock <- socket (addrFamily addr) (addrSocketType addr) (addrProtocol addr) (Sock.connect sock (addrAddress addr) >> readProcess "docker" [ "exec" , "-u", "postgres" , pid , "psql", "-U", "postgres", "-d", "postgres", "-c", "SELECT 1 + 1" ] "" >> return sock) `catch` (\(_ :: IOException) -> do threadDelay 1000000 go (n - 1)) cleanup :: (String, String) -> IO () cleanup (pid, _) = callProcess "docker" [ "rm", "-f", "-v", pid ]