Merge remote-tracking branch 'origin/master' into dev-abi2

Hopefully this doesn't break anything
pull/284/head
Will Song 5 years ago
commit 3d1d9189fd
  1. 4
      Dockerfile
  2. 4
      examples/solidity/basic/default.yaml
  3. 17
      examples/solidity/basic/time.sol
  4. 2
      examples/solidity/basic/time.yaml
  5. 9
      lib/Echidna/Config.hs
  6. 15
      lib/Echidna/Solidity.hs
  7. 2
      lib/Echidna/Test.hs
  8. 79
      lib/Echidna/Transaction.hs
  9. 10
      lib/Echidna/UI.hs
  10. 4
      src/test/Spec.hs

@ -4,10 +4,10 @@ RUN apt-get install -y sudo cmake curl wget libgmp-dev libssl-dev libbz2-dev lib
RUN apt-get update
RUN wget https://github.com/ethereum/solidity/releases/download/v0.4.25/solc-static-linux
RUN chmod +x solc-static-linux
RUN mv solc-static-linux /usr/bin/solc
RUN mv solc-static-linux /usr/bin/solc-0.4.25
RUN wget https://github.com/ethereum/solidity/releases/download/v0.5.7/solc-static-linux
RUN chmod +x solc-static-linux
RUN mv solc-static-linux /usr/bin/solc-0.5.7
RUN mv solc-static-linux /usr/bin/solc
RUN curl -sSL https://get.haskellstack.org/ | sh
COPY . /echidna/
WORKDIR /echidna

@ -34,3 +34,7 @@ quiet: False
#dashboard determines if output is just text or an AFL-like display
dashboard: true
#seed not defined by default, is the random seed
maxTimeDelay: 604800
#maximum time between generated txs; default is one week
maxBlockDelay: 60480
#maximum number of blocks elapsed between generated txs; default is expected increment in one week

@ -0,0 +1,17 @@
contract Time {
uint start;
uint marked;
constructor() public {
start = now;
marked = now;
}
function mark() public {
marked = now;
}
function echidna_timepassed() public returns (bool) {
return(start == marked);
}
}

@ -0,0 +1,2 @@
maxTimeDelay: 1000
maxBlockDelay: 5

@ -8,7 +8,7 @@
module Echidna.Config where
import Control.Lens
import Control.Monad (liftM2)
import Control.Monad (liftM2, liftM4)
import Control.Monad.Catch (MonadThrow)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Reader (Reader, ReaderT(..), runReader)
@ -65,9 +65,9 @@ instance FromJSON EConfig where
let goal fname = if (fprefix <> "revert_") `isPrefixOf` fname then ResRevert else ResTrue
return $ TestConf (\fname -> (== goal fname) . maybe ResOther classifyRes . view result)
(const psender)
xc = liftM2 TxConf
(C Dull . fromIntegral <$> v .:? "propMaxGas" .!= (8000030 :: Integer))
(C Dull . fromIntegral <$> v .:? "testMaxGas" .!= (0xffffffff :: Integer))
getWord s d = C Dull . fromIntegral <$> v .:? s .!= (d :: Integer)
xc = liftM4 TxConf (getWord "propMaxGas" 8000030) (getWord "testMaxGas" 0xffffffff)
(getWord "maxTimeDelay" 604800) (getWord "maxBlockDelay" 60480)
cc = CampaignConf <$> v .:? "testLimit" .!= 50000
<*> v .:? "seqLen" .!= 100
<*> v .:? "shrinkLimit" .!= 5000
@ -94,6 +94,7 @@ instance FromJSON EConfig where
<*> v .:? "balanceAddr" .!= 0xffffffff
<*> v .:? "balanceContract".!= 0
<*> v .:? "prefix" .!= "echidna_"
<*> v .:? "cryticArgs" .!= []
<*> v .:? "solcArgs" .!= ""
<*> v .:? "solcLibs" .!= []
<*> v .:? "quiet" .!= False

@ -79,6 +79,7 @@ data SolConf = SolConf { _contractAddr :: Addr -- ^ Contract address to u
, _balanceAddr :: Integer -- ^ Initial balance of deployer and senders
, _balanceContract :: Integer -- ^ Initial balance of contract to test
, _prefix :: Text -- ^ Function name prefix used to denote tests
, _cryticArgs :: [String] -- ^ Args to pass to crytic
, _solcArgs :: String -- ^ Args to pass to @solc@
, _solcLibs :: [String] -- ^ List of libraries to load, in order.
, _quiet :: Bool -- ^ Suppress @solc@ output, errors, and warnings
@ -97,16 +98,17 @@ contracts fp = let usual = ["--solc-disable-warnings", "--export-format", "solc"
a <- view (hasLens . solcArgs)
q <- view (hasLens . quiet)
ls <- view (hasLens . solcLibs)
c <- view (hasLens . cryticArgs)
let solargs = a ++ linkLibraries ls & (usual ++) .
(\sa -> if null sa then [] else ["--solc-args", sa])
maybe (throwM CompileFailure) (pure . toList . fst) =<< liftIO (do
stderr <- if q then UseHandle <$> openFile "/dev/null" WriteMode else pure Inherit
_ <- readCreateProcess (proc "crytic-compile" $ solargs |> fp) {std_err = stderr} ""
_ <- readCreateProcess (proc "crytic-compile" $ (c ++ solargs) |> fp) {std_err = stderr} ""
readSolc2 "crytic-export/combined_solc.json")
addresses :: (MonadReader x m, Has SolConf x) => m [AbiValue2]
addresses = view hasLens <&> \(SolConf ca d ads _ _ _ _ _ _ _) ->
addresses = view hasLens <&> \(SolConf ca d ads _ _ _ _ _ _ _ _) ->
AbiAddress2 . fromIntegral <$> nub (ads ++ [ca, d, 0x0])
populateAddresses :: [Addr] -> Integer -> VM -> VM
@ -123,7 +125,7 @@ loadLibraries :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x)
=> [SolcContract2] -> Addr -> Addr -> VM -> m VM
loadLibraries [] _ _ vm = return vm
loadLibraries (l:ls) la d vm = loadLibraries ls (la + 1) d =<< loadRest
where loadRest = execStateT (execTx2 $ Tx2 (Right $ l ^. creationCode2) d la 0xffffffff 0) vm
where loadRest = execStateT (execTx2 $ Tx2 (Right $ l ^. creationCode2) d la 0xffffffff 0 (0,0)) vm
-- | Generate a string to use as argument in solc to link libraries starting from addrLibrary
linkLibraries :: [String] -> String
@ -148,7 +150,7 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
unless q . putStrLn $ "Analyzing contract: " <> c ^. contractName2 . unpacked
-- Local variables
(SolConf ca d ads bala balc pref _ libs _ ch) <- view hasLens
(SolConf ca d ads bala balc pref _ _ libs _ ch) <- view hasLens
let bc = c ^. creationCode2
blank = populateAddresses (ads |> d) bala (vmForEthrunCreation bc)
abi = liftM2 (,) (view methodName2) (fmap snd . view methodInputs2) <$> toList (c ^. abiMap2)
@ -164,8 +166,7 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
case find (not . null . snd) tests of
Just (t,_) -> throwM $ TestArgsFound t -- Test args check
Nothing -> loadLibraries ls addrLibrary d blank >>= fmap (, fallback : funs, fst <$> tests) .
execStateT (execTx2 $ Tx2 (Right bc) d ca 0xffffffff (w256 $ fromInteger balc))
execStateT (execTx2 $ Tx2 (Right bc) d ca 0xffffffff (w256 $ fromInteger balc) (0, 0))
where choose [] _ = throwM NoContracts
choose (c:_) Nothing = return c
@ -189,7 +190,7 @@ loadWithCryticCompile fp name = contracts fp >>= loadSpecified name
-- for running a 'Campaign' against the tests found.
prepareForTest :: (MonadReader x m, Has SolConf x)
=> (VM, [SolSignature2], [Text]) -> m (VM, World2, [SolTest])
prepareForTest (v, a, ts) = view hasLens <&> \(SolConf _ _ s _ _ _ _ _ _ ch) ->
prepareForTest (v, a, ts) = view hasLens <&> \(SolConf _ _ s _ _ _ _ _ _ _ ch) ->
(v, World2 s [(r, a)], fmap Left (zip ts $ repeat r) ++ if ch then Right <$> drop 1 a else []) where
r = v ^. state . contract

@ -60,7 +60,7 @@ checkETest t = asks getter >>= \(TestConf p s) -> view (hasLens . propGas) >>= \
matchC sig = not . (BS.isPrefixOf . BS.take 4 $ abiCalldata2 (encodeSig2 sig) mempty)
res <- case t of
-- If our test is a regular user-defined test, we exec it and check the result
Left (f, a) -> execTx2 (Tx2 (Left (f, [])) (s a) a g 0) >> gets (p f . getter)
Left (f, a) -> execTx2 (Tx2 (Left (f, [])) (s a) a g 0 (0, 0)) >> gets (p f . getter)
-- If our test is an auto-generated assertion test, we check if we failed an assert on that fn
Right sig -> (||) <$> fmap matchR (use $ hasLens . result)
<*> fmap (matchC sig) (use $ hasLens . state . calldata)

@ -2,7 +2,10 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
module Echidna.Transaction where
@ -13,7 +16,7 @@ import Control.Monad (join, liftM2, liftM3, liftM5)
import Control.Monad.Catch (MonadThrow)
import Control.Monad.Random.Strict (MonadRandom, getRandomR)
import Control.Monad.Reader.Class (MonadReader)
import Control.Monad.State.Strict (MonadState, State, runState)
import Control.Monad.State.Strict (MonadState, State, evalStateT, runState)
import Data.Aeson (ToJSON(..), object)
import Data.ByteString (ByteString)
import Data.Either (either, lefts)
@ -39,14 +42,19 @@ data Tx2 = Tx2 { _call2 :: Either SolCall2 ByteString -- | Either a call or cod
, _dst2 :: Addr -- | Destination
, _gas2' :: Word -- | Gas
, _value2 :: Word -- | Value
, _delay2 :: (Word, Word) -- | (Time, # of blocks since last call)
} deriving (Eq, Ord, Show)
makeLenses ''Tx2
data TxConf = TxConf { _propGas :: Word
data TxConf = TxConf { _propGas :: Word
-- ^ Gas to use evaluating echidna properties
, _txGas :: Word
, _txGas :: Word
-- ^ Gas to use in generated transactions
, _maxTimeDelay :: Word
-- ^ Maximum time delay between transactions (seconds)
, _maxBlockDelay :: Word
-- ^ Maximum block delay between transactions
}
makeLenses 'TxConf
@ -56,13 +64,21 @@ ppSolCall2 :: SolCall2 -> String
ppSolCall2 (t, vs) = (if t == "" then T.unpack "*fallback*" else T.unpack t) ++ "(" ++ intercalate "," (ppAbiValue2 <$> vs) ++ ")"
instance ToJSON Tx2 where
toJSON (Tx2 c s d g v) = object [ ("call", toJSON $ either ppSolCall2 (const "<CREATE>") c)
-- from/to are Strings, since JSON doesn't support hexadecimal notation
, ("from", toJSON $ show s)
, ("to", toJSON $ show d)
, ("value", toJSON $ show v)
, ("gas", toJSON $ show g)
]
toJSON (Tx2 c s d g v (t, b)) = object [ ("call", toJSON $ either ppSolCall2 (const "<CREATE>") c)
-- from/to are Strings, since JSON doesn't support hexadecimal notation
, ("from", toJSON $ show s)
, ("to", toJSON $ show d)
, ("value", toJSON $ show v)
, ("gas", toJSON $ show g)
, ("time delay", toJSON $ show t)
, ("block delay", toJSON $ show b)
]
-- | If half a tuple is zero, make both halves zero. Useful for generating delays, since block number
-- only goes up with timestamp
level :: (Num a, Eq a) => (a, a) -> (a, a)
level (elemOf each 0 -> True) = (0,0)
level x = x
-- | A contract is just an address with an ABI (for our purposes).
type ContractA2 = (Addr, [SolSignature2])
@ -82,41 +98,49 @@ genTxWith2 :: (MonadRandom m, MonadState x m, Has World2 x, MonadThrow m)
-> (Addr -> ContractA2 -> m SolCall2) -- ^ Call generator
-> m Word -- ^ Gas generator
-> (Addr -> ContractA2 -> SolCall2 -> m Word) -- ^ Value generator
-> m (Word, Word) -- ^ Delay generator
-> m Tx2
genTxWith2 s r c g v = use hasLens >>=
\case (World2 ss rs) -> let s' = s ss; r' = r rs; c' = join $ liftM2 c s' r' in
liftM5 Tx2 (Left <$> c') s' (fst <$> r') g =<< liftM3 v s' r' c'
genTxWith2 s r c g v t = use hasLens >>= \(World2 ss rs) ->
let s' = s ss; r' = r rs; c' = join $ liftM2 c s' r' in
(liftM5 Tx2 (Left <$> c') s' (fst <$> r') g =<< liftM3 v s' r' c') <*> t
-- | Synthesize a random 'Transaction', not using a dictionary.
genTx2 :: (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has World2 y, MonadThrow m) => m Tx2
genTx2 = view (hasLens . txGas) >>= \g -> genTxWith2 (rElem "sender list") (rElem "recipient list")
(const $ genInteractions2 . snd) (pure g) (\_ _ _ -> pure 0)
genTx2 :: forall m x y. (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has World2 y, MonadThrow m) => m Tx2
genTx2 = use (hasLens :: Lens' y World2) >>= evalStateT genTxM2 . (defaultDict2,)
--genTx2 = view (hasLens . txGas) >>= \g -> genTxWith2 (rElem "sender list") (rElem "recipient list")
-- (const $ genInteractions2 . snd) (pure g) (\_ _ _ -> pure 0)
-- | Generate a random 'Transaction' with either synthesis or mutation of dictionary entries.
genTxM2 :: (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has GenDict2 y, Has World2 y, MonadThrow m) => m Tx2
genTxM2 = view (hasLens . txGas) >>= \g -> genTxWith2 (rElem "sender list") (rElem "recipient list")
(const $ genInteractionsM2 . snd) (pure g) (\_ _ _ -> pure 0)
genTxM2 = view hasLens >>= \(TxConf _ g t b) -> genTxWith2
(rElem "sender list") (rElem "recipient list") -- src and dst
(const $ genInteractionsM2 . snd) -- call itself
(pure g) (\_ _ _ -> pure 0) (level <$> liftM2 (,) (inRange t) (inRange b)) -- gas, value, delay
where inRange hi = w256 . fromIntegral <$> getRandomR (0 :: Integer, fromIntegral hi)
-- | Check if a 'Transaction' is as \"small\" (simple) as possible (using ad-hoc heuristics).
canShrinkTx2 :: Tx2 -> Bool
canShrinkTx2 (Tx2 (Right _) _ _ _ 0) = False
canShrinkTx2 (Tx2 (Left (_,l)) _ _ _ 0) = any canShrinkAbiValue2 l
canShrinkTx2 _ = True
canShrinkTx2 (Tx2 (Right _) _ _ _ 0 (0, 0)) = False
canShrinkTx2 (Tx2 (Left (_,l)) _ _ _ 0 (0, 0)) = any canShrinkAbiValue2 l
canShrinkTx2 _ = True
-- | Given a 'Transaction', generate a random \"smaller\" 'Transaction', preserving origin,
-- destination, value, and call signature.
shrinkTx2 :: MonadRandom m => Tx2 -> m Tx2
shrinkTx2 (Tx2 c s d g (C _ v)) = let c' = either (fmap Left . shrinkAbiCall2) (fmap Right . pure) c in
liftM5 Tx2 c' (pure s) (pure d) (pure g) $ w256 . fromIntegral <$> getRandomR (0 :: Integer, fromIntegral v)
shrinkTx2 (Tx2 c s d g (C _ v) (C _ t, C _ b)) = let
c' = either (fmap Left . shrinkAbiCall2) (fmap Right . pure) c
lower x = w256 . fromIntegral <$> getRandomR (0 :: Integer, fromIntegral x) in
liftM5 Tx2 c' (pure s) (pure d) (pure g) (lower v) <*> fmap level (liftM2 (,) (lower t) (lower b))
-- | Given a 'Set' of 'Transaction's, generate a similar 'Transaction' at random.
spliceTxs2 :: (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has World2 y, MonadThrow m) => Set Tx2 -> m Tx2
spliceTxs2 ts = let l = S.toList ts; (cs, ss) = unzip $ (\(Tx2 c s _ _ _) -> (c,s)) <$> l in
spliceTxs2 ts = let l = S.toList ts; (cs, ss) = unzip $ (\(Tx2 c s _ _ _ _) -> (c,s)) <$> l in
view (hasLens . txGas) >>= \g ->
genTxWith2 (const . rElem "sender list" $ ss) (rElem "recipient list")
(\_ _ -> mutateAbiCall2 =<< rElem "past calls" (lefts cs)) (pure g)
(\ _ _ (n,_) -> let valOf (Tx2 c _ _ _ v) = if elem n $ c ^? _Left . _1 then v else 0
(\ _ _ (n,_) -> let valOf (Tx2 c _ _ _ v _) = if elem n $ c ^? _Left . _1 then v else 0
in rElem "values" $ valOf <$> l)
(pure (0, 0))
-- | Lift an action in the context of a component of some 'MonadState' to an action in the
-- 'MonadState' itself.
@ -126,9 +150,10 @@ liftSH = S.state . runState . zoom hasLens
-- | Given a 'Transaction', set up some 'VM' so it can be executed. Effectively, this just brings
-- 'Transaction's \"on-chain\".
setupTx2 :: (MonadState x m, Has VM x) => Tx2 -> m ()
setupTx2 (Tx2 c s r g v) = liftSH . sequence_ $
setupTx2 (Tx2 c s r g v (t, b)) = liftSH . sequence_ $
[ result .= Nothing, state . pc .= 0, state . stack .= mempty, state . memory .= mempty, state . gas .= g
, tx . origin .= s, state . caller .= s, state . callvalue .= v, setup] where
, tx . origin .= s, state . caller .= s, state . callvalue .= v
, block . timestamp += t, block . number += b, setup] where
setup = case c of
Left cd -> loadContract r >> state . calldata .= encode cd
Right bc -> assign (env . contracts . at r) (Just $ initialContract (RuntimeCode bc) & set balance v) >> loadContract r

@ -54,12 +54,14 @@ type Names = Role -> Addr -> String
-- | Given rules for pretty-printing associated address, and whether to print them, pretty-print a 'Transaction'.
ppTx :: (MonadReader x m, Has Names x, Has TxConf x) => Bool -> Tx2 -> m String
ppTx b (Tx2 c s r g v) = let sOf = either ppSolCall2 (const "<CREATE>") in do
ppTx pn (Tx2 c s r g v (t, b)) = let sOf = either ppSolCall2 (const "<CREATE>") in do
names <- view hasLens
tGas <- view $ hasLens . txGas
return $ sOf c ++ (if not b then "" else names Sender s ++ names Receiver r)
++ (if g == tGas then "" else " Gas: " ++ show g)
++ (if v == 0 then "" else " Value: " ++ show v)
return $ sOf c ++ (if not pn then "" else names Sender s ++ names Receiver r)
++ (if g == tGas then "" else " Gas: " ++ show g)
++ (if v == 0 then "" else " Value: " ++ show v)
++ (if t == 0 then "" else " Time delay: " ++ show t)
++ (if b == 0 then "" else " Block delay: " ++ show b)
-- | Given a number of boxes checked and a number of total boxes, pretty-print progress in box-checking.
progress :: Int -> Int -> String

@ -74,7 +74,7 @@ seedTests =
, testCase "same seeds" $ assertBool "results differ" =<< same 0 0
]
where cfg s = defaultConfig & sConf . quiet .~ True
& cConf .~ CampaignConf 600 5 0 Nothing (Just s)
& cConf .~ CampaignConf 600 20 0 Nothing (Just s)
gen s = view tests <$> runContract "basic/flags.sol" (cfg s)
same s t = liftM2 (==) (gen s) (gen t)
@ -147,6 +147,8 @@ integrationTests = testGroup "Solidity Integration Testing"
, testContract "basic/assert.sol" (Just "basic/assert.yaml")
[ ("echidna_set0 passed", solved "ASSERTION set0")
, ("echidna_set1 failed", passed "ASSERTION set1") ]
, testContract "basic/time.sol" (Just "basic/time.yaml")
[ ("echidna_timepassed passed", solved "echidna_timepassed") ]
]
testContract :: FilePath -> Maybe FilePath -> [(String, Campaign -> Bool)] -> TestTree

Loading…
Cancel
Save