From e03bd91971f6fe7ed0f7421841f73ed27becde1c Mon Sep 17 00:00:00 2001 From: JP Smith Date: Wed, 28 Feb 2018 17:13:02 -0500 Subject: [PATCH] fixed state machine example --- examples/state-machine/StateMachine.hs | 131 ++++++++----------------- lib/Echidna/Exec.hs | 2 + solidity/turnstile.sol | 2 +- 3 files changed, 46 insertions(+), 89 deletions(-) diff --git a/examples/state-machine/StateMachine.hs b/examples/state-machine/StateMachine.hs index 5c34aa63..94da66d9 100644 --- a/examples/state-machine/StateMachine.hs +++ b/examples/state-machine/StateMachine.hs @@ -2,48 +2,19 @@ module Main where -import Control.Monad.IO.Class +import Control.Monad.State.Strict -import Data.IORef - - {- -import EVM -import EVM.ABI (AbiType, AbiValue(..), abiCalldata, abiValueType, encodeAbiValue) import Echidna.Exec import Echidna.Solidity - -} + +import EVM +import EVM.ABI +import EVM.Concrete import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range --- locked initially true --- coin() -> locked to false --- push() when locked -> false --- push() when unlocked -> true, locked now true - --- model of contract states -data TurnstileState = Locked - | Unlocked - deriving (Eq, Ord, Show) - -newtype Turnstile = Turnstile { - unTurnstile :: IORef TurnstileState - } - -newTurnstile :: IO Turnstile -newTurnstile = Turnstile <$> newIORef Locked - -insertCoin :: Turnstile -> IO () -insertCoin (Turnstile ref) = atomicModifyIORef' ref $ \_ -> (Unlocked, ()) - -pushTurnstile :: Turnstile -> IO Bool -pushTurnstile (Turnstile ref) = atomicModifyIORef' ref $ \s -> - case s of - Locked -> (Locked, False) - Unlocked -> (Locked, True) - --- model of contract transitions data ModelState (v :: * -> *) = TLocked | TUnlocked deriving (Eq, Ord, Show) @@ -51,11 +22,9 @@ data ModelState (v :: * -> *) = TLocked initialState :: ModelState v initialState = TLocked -data Coin (v :: * -> *) = Coin - deriving (Eq, Show) +data Coin (v :: * -> *) = Coin deriving (Eq, Show) -data Push (v :: * -> *) = Push - deriving (Eq, Show) +data Push (v :: * -> *) = Push deriving (Eq, Show) instance HTraversable Coin where htraverse _ Coin = pure Coin @@ -64,57 +33,43 @@ instance HTraversable Push where htraverse _ Push = pure Push -- commands representing state transitions that are passed to hedgehog -s_coin :: (Monad n, MonadIO m, MonadTest m) => Turnstile -> Command n m ModelState -s_coin ts = - let gen _ = Just $ pure Coin - execute Coin = liftIO (insertCoin ts) - in - Command gen execute [ Update $ \_ Coin _o -> TUnlocked - , Ensure $ \_ after Coin () -> do after === TUnlocked - ] - -s_push_locked :: (Monad n, MonadIO m, MonadTest m) => Turnstile -> Command n m ModelState -s_push_locked ts = - let gen state = case state of - TLocked -> Just $ pure Push - TUnlocked -> Nothing - execute Push = do liftIO $ pushTurnstile ts - in - Command gen execute [ Require $ \s Push -> s == TLocked - , Update $ \_ Push _o -> TLocked - , Ensure $ \before after Push b -> do - before === TLocked - assert (not b) - after === TLocked - ] - -s_push_unlocked :: (Monad n, MonadIO m, MonadTest m) => Turnstile -> Command n m ModelState -s_push_unlocked ts = - let gen state = case state of - TUnlocked -> Just $ pure Push - TLocked -> Nothing - execute Push = do liftIO $ pushTurnstile ts - in - Command gen execute [ Require $ \s Push -> s == TUnlocked - , Update $ \_ Push _o -> TLocked - , Ensure $ \before after Push b -> do - before === TUnlocked - assert b - after === TLocked - ] - --- the property, the actual hedgehog proposal +s_coin :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState +s_coin = Command (\_ -> Just $ pure Coin) + (\Coin -> cleanUp >> execCall ("coin", [])) + [ Update $ \_ Coin _ -> TUnlocked + , Ensure $ \_ s Coin _ -> s === TUnlocked + ] + +match :: VMResult -> Bool -> Bool +match (VMSuccess (B s)) b = s == encodeAbiValue (AbiBool b) +match _ _ = False + +s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState +s_push_locked = Command (\s -> if s == TUnlocked then Just $ pure Push else Nothing) + (\Push -> cleanUp >> execCall ("push", [])) + [ Require $ \s Push -> s == TLocked + , Update $ \_ Push _ -> TLocked + , Ensure $ \before after Push b -> do before === TLocked + assert (match b False) + after === TLocked + ] + +s_push_unlocked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState +s_push_unlocked = Command (\s -> if s == TLocked then Just $ pure Push else Nothing) + (\Push -> cleanUp >> execCall ("push", [])) + [ Require $ \s Push -> s == TUnlocked + , Update $ \_ Push _ -> TLocked + , Ensure $ \before after Push b -> do before === TUnlocked + assert (match b True) + after === TLocked + ] + prop_turnstile :: Property prop_turnstile = property $ do - t <- liftIO newTurnstile - ops <- forAll $ Gen.sequential (Range.linear 1 100) initialState [ - s_coin t - , s_push_locked t - , s_push_unlocked t - ] - executeSequential initialState ops + (v,_,_) <- loadSolidity "solidity/turnstile.sol" + actions <- forAll $ Gen.sequential (Range.linear 1 100) initialState + [s_coin, s_push_locked, s_push_unlocked] + evalStateT (executeSequential initialState actions) v main :: IO () -main = do - r <- check $ prop_turnstile - putStrLn $ show r +main = check prop_turnstile >> pure () diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs index a9e0a36b..941438ad 100644 --- a/lib/Echidna/Exec.hs +++ b/lib/Echidna/Exec.hs @@ -2,8 +2,10 @@ module Echidna.Exec ( checkETest + , cleanUp , eCommand , ePropertySeq + , execCall , fuzz ) where diff --git a/solidity/turnstile.sol b/solidity/turnstile.sol index 17d40870..e00b2d21 100644 --- a/solidity/turnstile.sol +++ b/solidity/turnstile.sol @@ -12,7 +12,7 @@ contract Turnstile { return(false); } else { locked = true; - return(true) + return(true); } } }