fixed state machine example

remotes/origin/dev-fix-int-generation
JP Smith 7 years ago
parent 3a44fac19e
commit e03bd91971
  1. 131
      examples/state-machine/StateMachine.hs
  2. 2
      lib/Echidna/Exec.hs
  3. 2
      solidity/turnstile.sol

@ -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 ()

@ -2,8 +2,10 @@
module Echidna.Exec (
checkETest
, cleanUp
, eCommand
, ePropertySeq
, execCall
, fuzz
) where

@ -12,7 +12,7 @@ contract Turnstile {
return(false);
} else {
locked = true;
return(true)
return(true);
}
}
}

Loading…
Cancel
Save