Skip to content

Commit

Permalink
Improve Tx destructuring (#966)
Browse files Browse the repository at this point in the history
  • Loading branch information
arcz authored Mar 3, 2023
1 parent 6dd6197 commit 54d8964
Show file tree
Hide file tree
Showing 4 changed files with 104 additions and 73 deletions.
2 changes: 1 addition & 1 deletion lib/Echidna/Campaign.hs
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ evalSeq vmForShrink e = go [] where
-- gas usage for each call
updateGasInfo :: [(Tx, (VMResult, Gas))] -> [Tx] -> Map Text (Gas, [Tx]) -> Map Text (Gas, [Tx])
updateGasInfo [] _ gi = gi
updateGasInfo ((tx@(Tx (SolCall (f, _)) _ _ _ _ _ _), (_, used')):txs) tseq gi =
updateGasInfo ((tx@(Tx { call = SolCall (f, _) }), (_, used')):txs) tseq gi =
case mused of
Nothing -> rec
Just (used, _) | used' > used -> rec
Expand Down
23 changes: 16 additions & 7 deletions lib/Echidna/Transaction.hs
Original file line number Diff line number Diff line change
Expand Up @@ -90,14 +90,14 @@ genValue mv ds ps sc =

-- | Check if a 'Transaction' is as \"small\" (simple) as possible (using ad-hoc heuristics).
canShrinkTx :: Tx -> Bool
canShrinkTx (Tx solcall _ _ _ 0 0 (0, 0)) =
case solcall of
canShrinkTx Tx { call, gasprice = 0, value = 0, delay = (0, 0) } =
case call of
SolCall (_, l) -> any canShrinkAbiValue l
_ -> False
canShrinkTx _ = True

removeCallTx :: Tx -> Tx
removeCallTx (Tx _ _ r _ _ _ d) = Tx NoCall 0 r 0 0 0 d
removeCallTx t = Tx NoCall 0 t.src 0 0 0 t.delay

-- | Given a 'Transaction', generate a random \"smaller\" 'Transaction', preserving origin,
-- destination, value, and call signature.
Expand All @@ -123,7 +123,7 @@ shrinkTx tx' = let
in join $ usuallyRarely (join (uniform possibilities)) (pure $ removeCallTx tx')

mutateTx :: (MonadRandom m) => Tx -> m Tx
mutateTx t@(Tx (SolCall c) _ _ _ _ _ _) = do
mutateTx t@(Tx { call = SolCall c }) = do
f <- oftenUsually skip mutate
f c
where mutate z = mutateAbiCall z >>= \c' -> pure $ t { call = SolCall c' }
Expand All @@ -142,9 +142,18 @@ setupTx (Tx c s r g gp v (t, b)) = fromEVM . sequence_ $
, tx . gasprice .= gp, tx . origin .= s, state . caller .= Lit (fromIntegral s), state . callvalue .= Lit v
, block . timestamp %= (\x -> Lit (forceLit x + t)), block . number += b, setup] where
setup = case c of
SolCreate bc -> assign (env . contracts . at r) (Just $ initialContract (InitCode bc mempty) & set balance v) >> loadContract r >> state . code .= RuntimeCode (ConcreteRuntimeCode bc)
SolCall cd -> incrementBalance >> loadContract r >> state . calldata .= ConcreteBuf (encode cd)
SolCalldata cd -> incrementBalance >> loadContract r >> state . calldata .= ConcreteBuf cd
SolCreate bc -> do
assign (env . contracts . at r) (Just $ initialContract (InitCode bc mempty) & set balance v)
loadContract r
state . code .= RuntimeCode (ConcreteRuntimeCode bc)
SolCall cd -> do
incrementBalance
loadContract r
state . calldata .= ConcreteBuf (encode cd)
SolCalldata cd -> do
incrementBalance
loadContract r
state . calldata .= ConcreteBuf cd
incrementBalance = (env . contracts . ix r . balance) += v
encode (n, vs) = abiCalldata
(encodeSig (n, abiValueType <$> vs)) $ V.fromList vs
2 changes: 1 addition & 1 deletion lib/Echidna/Types/Config.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ data UIConf = UIConf { maxTime :: Maybe Int
}

-- | An address involved with a 'Transaction' is either the sender, the recipient, or neither of those things.
data Role = Sender | Receiver | Ambiguous
data Role = Sender | Receiver

-- | Rules for pretty-printing addresses based on their role in a transaction.
type Names = Role -> Addr -> String
Expand Down
150 changes: 86 additions & 64 deletions lib/Echidna/UI/Report.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,115 +18,137 @@ import Echidna.Types.Test (testEvents, testState, TestState(..), testType, TestT
import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..))
import Echidna.Types.Config

-- | Given a number of boxes checked and a number of total boxes, pretty-print progress in box-checking.
progress :: Int -> Int -> String
progress n m = "(" ++ show n ++ "/" ++ show m ++ ")"
import EVM.Types (W256)

-- | Given rules for pretty-printing associated address, and whether to print them, pretty-print a 'Transaction'.
ppTx :: (MonadReader EConfig m) => Bool -> Tx -> m String
ppTx _ (Tx NoCall _ _ _ _ _ (t, b)) =
return $ "*wait*" ++ (if t == 0 then "" else " Time delay: " ++ show (toInteger t) ++ " seconds")
++ (if b == 0 then "" else " Block delay: " ++ show (toInteger b))
ppCampaign :: MonadReader EConfig m => Campaign -> m String
ppCampaign campaign = do
testsPrinted <- ppTests campaign
gasInfoPrinted <- ppGasInfo campaign
let coveragePrinted = ppCoverage campaign._coverage
corpusPrinted = "\n" <> ppCorpus campaign._corpus
seedPrinted = "\nSeed: " <> show campaign._genDict.defSeed
pure $
testsPrinted
<> gasInfoPrinted
<> coveragePrinted
<> corpusPrinted
<> seedPrinted

ppTx pn (Tx c s r g gp v (t, b)) = let sOf = ppTxCall in do
-- | Given rules for pretty-printing associated address, and whether to print them, pretty-print a 'Transaction'.
ppTx :: MonadReader EConfig m => Bool -> Tx -> m String
ppTx _ Tx { call = NoCall, delay } =
pure $ "*wait*" <> ppDelay delay
ppTx printName tx = do
names <- asks (.namesConf)
tGas <- asks (.txConf.txGas)
return $ sOf c ++ (if not pn then "" else names Sender s ++ names Receiver r)
++ (if g == tGas then "" else " Gas: " ++ show g)
++ (if gp == 0 then "" else " Gas price: " ++ show gp)
++ (if v == 0 then "" else " Value: " ++ show v)
++ (if t == 0 then "" else " Time delay: " ++ show (toInteger t) ++ " seconds")
++ (if b == 0 then "" else " Block delay: " ++ show (toInteger b))
pure $
ppTxCall tx.call
<> (if not printName then "" else names Sender tx.src <> names Receiver tx.dst)
<> (if tx.gas == tGas then "" else " Gas: " <> show tx.gas)
<> (if tx.gasprice == 0 then "" else " Gas price: " <> show tx.gasprice)
<> (if tx.value == 0 then "" else " Value: " <> show tx.value)
<> ppDelay tx.delay

ppDelay :: (W256, W256) -> [Char]
ppDelay (time, block) =
(if time == 0 then "" else " Time delay: " <> show (toInteger time) <> " seconds")
<> (if block == 0 then "" else " Block delay: " <> show (toInteger block))

-- | Pretty-print the coverage a 'Campaign' has obtained.
ppCoverage :: CoverageMap -> String
ppCoverage s = "Unique instructions: " ++ show (scoveragePoints s)
++ "\nUnique codehashes: " ++ show (length s)
ppCoverage s = "Unique instructions: " <> show (scoveragePoints s)
<> "\nUnique codehashes: " <> show (length s)

-- | Pretty-print the corpus a 'Campaign' has obtained.
ppCorpus :: Corpus -> String
ppCorpus c = "Corpus size: " ++ show (corpusSize c)
ppCorpus c = "Corpus size: " <> show (corpusSize c)

-- | Pretty-print the gas usage information a 'Campaign' has obtained.
ppGasInfo :: MonadReader EConfig m => Campaign -> m String
ppGasInfo Campaign { _gasInfo } | _gasInfo == mempty = pure ""
ppGasInfo Campaign { _gasInfo } = do
items <- mapM ppGasOne $ sortOn (\(_, (n, _)) -> n) $ toList _gasInfo
pure $ intercalate "" items

-- | Pretty-print the gas usage for a function.
ppGasOne :: MonadReader EConfig m => (Text, (Gas, [Tx])) -> m String
ppGasOne ("", _) = pure ""
ppGasOne (f, (g, xs)) = let pxs = mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs in
(("\n" ++ unpack f ++ " used a maximum of " ++ show g ++ " gas\n Call sequence:\n") ++) . unlines . fmap (" " ++) <$> pxs

-- | Pretty-print the gas usage information a 'Campaign' has obtained.
ppGasInfo :: MonadReader EConfig m => Campaign -> m String
ppGasInfo Campaign { _gasInfo = gi } | gi == mempty = pure ""
ppGasInfo Campaign { _gasInfo = gi } = (fmap $ intercalate "") (mapM ppGasOne $ sortOn (\(_, (n, _)) -> n) $ toList gi)
ppGasOne (func, (gas, txs)) = do
let header = "\n" <> unpack func <> " used a maximum of " <> show gas <> " gas\n"
<> " Call sequence:\n"
prettyTxs <- mapM (ppTx $ length (nub $ (.src) <$> txs) /= 1) txs
pure $ header <> unlines ((" " <>) <$> prettyTxs)

-- | Pretty-print the status of a solved test.
ppFail :: MonadReader EConfig m => Maybe (Int, Int) -> Events -> [Tx] -> m String
ppFail _ _ [] = pure "failed with no transactions made ⁉️ "
ppFail b es xs = let status = case b of
Nothing -> ""
Just (n,m) -> ", shrinking " ++ progress n m
pxs = mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs in
do s <- (("failed!💥 \n Call sequence" ++ status ++ ":\n") ++) . unlines . fmap (" " ++) <$> pxs
return (s ++ "\n" ++ ppEvents es)
ppFail b es xs = do
let status = case b of
Nothing -> ""
Just (n,m) -> ", shrinking " <> progress n m
prettyTxs <- mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs
pure $ "failed!💥 \n Call sequence" <> status <> ":\n"
<> unlines ((" " <>) <$> prettyTxs) <> "\n"
<> ppEvents es

ppEvents :: Events -> String
ppEvents es = if null es then "" else "Event sequence: " ++ T.unpack (T.intercalate ", " es)
ppEvents es = if null es then "" else "Event sequence: " <> T.unpack (T.intercalate ", " es)

-- | Pretty-print the status of a test.

ppTS :: MonadReader EConfig m => TestState -> Events -> [Tx] -> m String
ppTS (Failed e) _ _ = pure $ "could not evaluate ☣\n " ++ show e
ppTS (Failed e) _ _ = pure $ "could not evaluate ☣\n " <> show e
ppTS Solved es l = ppFail Nothing es l
ppTS Passed _ _ = pure " passed! 🎉"
ppTS (Open i) es [] = do
t <- asks (.campaignConf.testLimit)
if i >= t then ppTS Passed es [] else pure $ " fuzzing " ++ progress i t
if i >= t then ppTS Passed es [] else pure $ " fuzzing " <> progress i t
ppTS (Open _) es r = ppFail Nothing es r
ppTS (Large n) es l = do
m <- asks (.campaignConf.shrinkLimit)
ppFail (if n < m then Just (n, m) else Nothing) es l


ppOPT :: MonadReader EConfig m => TestState -> Events -> [Tx] -> m String
ppOPT (Failed e) _ _ = pure $ "could not evaluate ☣\n " ++ show e
ppOPT (Failed e) _ _ = pure $ "could not evaluate ☣\n " <> show e
ppOPT Solved es l = ppOptimized Nothing es l
ppOPT Passed _ _ = pure " passed! 🎉"
ppOPT (Open _) es r = ppOptimized Nothing es r
ppOPT (Large n) es l = do
m <- asks (.campaignConf.shrinkLimit)
ppOptimized (if n < m then Just (n, m) else Nothing) es l


-- | Pretty-print the status of a optimized test.
ppOptimized :: MonadReader EConfig m => Maybe (Int, Int) -> Events -> [Tx] -> m String
ppOptimized _ _ [] = pure "Call sequence:\n(no transactions)"
ppOptimized b es xs = let status = case b of
Nothing -> ""
Just (n,m) -> ", shrinking " ++ progress n m
pxs = mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs in
do s <- (("\n Call sequence" ++ status ++ ":\n") ++) . unlines . fmap (" " ++) <$> pxs
return (s ++ "\n" ++ ppEvents es)

ppOptimized b es xs = do
let status = case b of
Nothing -> ""
Just (n,m) -> ", shrinking " <> progress n m
prettyTxs <- mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs
pure $ "\n Call sequence" <> status <> ":\n"
<> unlines ((" " <>) <$> prettyTxs) <> "\n"
<> ppEvents es

-- | Pretty-print the status of all 'SolTest's in a 'Campaign'.
ppTests :: MonadReader EConfig m => Campaign -> m String
ppTests Campaign { _tests = ts } = unlines . catMaybes <$> mapM pp ts where
pp t = case t.testType of
PropertyTest n _ -> Just . ((T.unpack n ++ ": ") ++) <$> ppTS t.testState t.testEvents t.testReproducer
CallTest n _ -> Just . ((T.unpack n ++ ": ") ++) <$> ppTS t.testState t.testEvents t.testReproducer
AssertionTest _ s _ -> Just . ((T.unpack (encodeSig s) ++ ": ") ++) <$> ppTS t.testState t.testEvents t.testReproducer
OptimizationTest n _ -> Just . ((T.unpack n ++ ": max value: " ++ show t.testValue ++ "\n") ++) <$> ppOPT t.testState t.testEvents t.testReproducer
Exploration -> return Nothing
ppTests Campaign { _tests = ts } = unlines . catMaybes <$> mapM pp ts
where
pp t =
case t.testType of
PropertyTest n _ -> do
status <- ppTS t.testState t.testEvents t.testReproducer
pure $ Just (T.unpack n <> ": " <> status)
CallTest n _ -> do
status <- ppTS t.testState t.testEvents t.testReproducer
pure $ Just (T.unpack n <> ": " <> status)
AssertionTest _ s _ -> do
status <- ppTS t.testState t.testEvents t.testReproducer
pure $ Just (T.unpack (encodeSig s) <> ": " <> status)
OptimizationTest n _ -> do
status <- ppOPT t.testState t.testEvents t.testReproducer
pure $ Just (T.unpack n <> ": max value: " <> show t.testValue <> "\n" <> status)
Exploration -> pure Nothing

ppCampaign :: MonadReader EConfig m => Campaign -> m String
ppCampaign c = do
testsPrinted <- ppTests c
gasInfoPrinted <- ppGasInfo c
let coveragePrinted = ppCoverage c._coverage
corpusPrinted = "\n" ++ ppCorpus c._corpus
seedPrinted = "\nSeed: " ++ show c._genDict.defSeed
pure $
testsPrinted
++ gasInfoPrinted
++ coveragePrinted
++ corpusPrinted
++ seedPrinted
-- | Given a number of boxes checked and a number of total boxes, pretty-print progress in box-checking.
progress :: Int -> Int -> String
progress n m = "(" <> show n <> "/" <> show m <> ")"

0 comments on commit 54d8964

Please sign in to comment.