forked from crytic/echidna
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Exec.hs
146 lines (119 loc) · 5.29 KB
/
Exec.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleContexts, KindSignatures, LambdaCase, StrictData #-}
module Echidna.Exec (
VMState(..)
, VMAction(..)
, checkTest
, checkBoolExpTest
, checkRevertTest
, checkTrueOrRevertTest
, checkFalseOrRevertTest
, eCommand
, eCommandUsing
, ePropertySeq
, ePropertyUsing
, execCall
, execCallUsing
, module Echidna.Internal.Runner
, module Echidna.Internal.JsonRunner
) where
import Control.Lens ((&), (^.), (.=), (?~))
import Control.Monad.Catch (MonadCatch)
import Control.Monad.State.Strict (MonadState, evalState, execState, get, put)
import Control.Monad.Reader (MonadReader, runReaderT, ask)
import Data.List (intercalate)
import Data.Text (Text)
import Data.Typeable (Typeable)
import Data.Vector (fromList)
import Hedgehog
import Hedgehog.Gen (sequential)
import Hedgehog.Internal.State (Action(..))
import Hedgehog.Internal.Property (PropertyConfig(..), mapConfig)
import Hedgehog.Range (linear)
import EVM
import EVM.ABI (AbiValue(..), abiCalldata, abiValueType, encodeAbiValue)
import EVM.Concrete (Blob(..))
import EVM.Exec (exec)
import Echidna.ABI (SolCall, SolSignature, displayAbiCall, encodeSig, genInteractions)
import Echidna.Config (Config(..), testLimit, range, shrinkLimit)
import Echidna.Internal.Runner
import Echidna.Internal.JsonRunner
import Echidna.Property (PropertyType(..))
-------------------------------------------------------------------
-- Fuzzing and Hedgehog Init
execCall :: MonadState VM m => SolCall -> m VMResult
execCall = execCallUsing exec
execCallUsing :: MonadState VM m => m VMResult -> SolCall -> m VMResult
execCallUsing m (t,vs) = do og <- get
cleanUp
state . calldata .= cd
m >>= \case x@VMFailure{} -> put (og & result ?~ x) >> return x
x@VMSuccess{} -> return x
where cd = B . abiCalldata (encodeSig t $ abiValueType <$> vs) $ fromList vs
cleanUp = sequence_ [result .= Nothing, state . pc .= 0, state . stack .= mempty]
checkTest :: PropertyType -> VM -> Text -> Bool
checkTest ShouldReturnTrue = checkBoolExpTest True
checkTest ShouldReturnFalse = checkBoolExpTest False
checkTest ShouldRevert = checkRevertTest
checkTest ShouldReturnFalseRevert = checkFalseOrRevertTest
checkBoolExpTest :: Bool -> VM -> Text -> Bool
checkBoolExpTest b v t = case evalState (execCall (t, [])) v of
VMSuccess (B s) -> s == encodeAbiValue (AbiBool b)
_ -> False
checkRevertTest :: VM -> Text -> Bool
checkRevertTest v t = case evalState (execCall (t, [])) v of
(VMFailure Revert) -> True
_ -> False
checkTrueOrRevertTest :: VM -> Text -> Bool
checkTrueOrRevertTest v t = case evalState (execCall (t, [])) v of
(VMSuccess (B s)) -> s == encodeAbiValue (AbiBool True)
(VMFailure Revert) -> True
_ -> False
checkFalseOrRevertTest :: VM -> Text -> Bool
checkFalseOrRevertTest v t = case evalState (execCall (t, [])) v of
(VMSuccess (B s)) -> s == encodeAbiValue (AbiBool False)
(VMFailure Revert) -> True
_ -> False
newtype VMState (v :: * -> *) =
VMState VM
instance Show (VMState v) where
show (VMState v) = "EVM state, current result: " ++ show (v ^. result)
newtype VMAction (v :: * -> *) =
Call SolCall
instance Show (VMAction v) where
show (Call c) = displayAbiCall c
instance HTraversable VMAction where
htraverse _ (Call b) = pure $ Call b
eCommandUsing :: (MonadGen n, MonadTest m, Typeable a)
=> n SolCall
-> (VMAction Concrete -> m a)
-> (VM -> Bool)
-> Command n m VMState
eCommandUsing gen ex p = Command (\_ -> pure $ Call <$> gen) ex
[ Ensure $ \_ (VMState v) _ _ -> assert $ p v
, Update $ \(VMState v) (Call c) _ -> VMState $ execState (execCall c) v
]
eCommand :: (MonadGen n, MonadTest m) => n SolCall -> (VM -> Bool) -> Command n m VMState
eCommand = flip eCommandUsing (\ _ -> pure ())
configProperty :: Config -> PropertyConfig -> PropertyConfig
configProperty config x = x { propertyTestLimit = config ^. testLimit
, propertyShrinkLimit = config ^. shrinkLimit
}
ePropertyUsing :: (MonadCatch m, MonadTest m, MonadReader Config n)
=> [Command Gen m VMState]
-> (m () -> PropertyT IO ())
-> VM
-> n Property
ePropertyUsing cs f v = do
config <- ask
return $ mapConfig (configProperty config) . property $
f . executeSequential (VMState v) =<< forAllWith printCallSeq
(sequential (linear 1 (config ^. range)) (VMState v) cs)
where printCallSeq = ("Call sequence: " ++) . intercalate "\n " .
map showCall . sequentialActions
showCall (Action i _ _ _ _ _) = show i ++ ";"
ePropertySeq :: (MonadReader Config m)
=> (VM -> Bool) -- Predicate to fuzz for violations of
-> [SolSignature] -- Type signatures to fuzz
-> VM -- Initial state
-> m Property
ePropertySeq p ts vm = ask >>= \c -> ePropertyUsing [eCommand (runReaderT (genInteractions ts) c) p] id vm