Skip to content

Commit

Permalink
Use trace printing from hevm (#1157)
Browse files Browse the repository at this point in the history
  • Loading branch information
arcz authored Jan 5, 2024
1 parent 0a34809 commit f6e8fbb
Show file tree
Hide file tree
Showing 10 changed files with 83 additions and 71 deletions.
5 changes: 1 addition & 4 deletions lib/Echidna/Campaign.hs
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,6 @@ import EVM.Types hiding (Env, Frame(state))

import Echidna.ABI
import Echidna.Exec
import Echidna.Events (extractEvents)
import Echidna.Mutator.Corpus
import Echidna.Shrink (shrinkTest)
import Echidna.Symbolic (forceBuf, forceAddr)
Expand Down Expand Up @@ -373,14 +372,12 @@ updateTest
-> EchidnaTest
-> m (Maybe EchidnaTest)
updateTest vmForShrink (vm, xs) test = do
dappInfo <- asks (.dapp)
case test.state of
Open -> do
(testValue, vm') <- checkETest test vm
let
events = extractEvents False dappInfo vm'
results = getResultFromVM vm'
test' = updateOpenTest test xs (testValue, events, results)
test' = updateOpenTest test xs (testValue, vm', results)
case test'.state of
Large _ -> do
pushEvent (TestFalsified test')
Expand Down
11 changes: 6 additions & 5 deletions lib/Echidna/Output/JSON.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,11 @@ import Data.Text.Encoding (decodeUtf8)
import Data.Vector.Unboxed qualified as VU
import Numeric (showHex)

import EVM.Dapp (DappInfo)
import EVM.Types (keccak')

import Echidna.ABI (ppAbiValue, GenDict(..))
import Echidna.Events (Events)
import Echidna.Events (Events, extractEvents)
import Echidna.Types (Gas)
import Echidna.Types.Campaign (WorkerState(..))
import Echidna.Types.Config (Env(..))
Expand Down Expand Up @@ -107,21 +108,21 @@ encodeCampaign env workerStates = do
pure $ encode Campaign
{ _success = True
, _error = Nothing
, _tests = mapTest <$> tests
, _tests = mapTest env.dapp <$> tests
, seed = worker0.genDict.defSeed
, coverage = Map.mapKeys (("0x" ++) . (`showHex` "") . keccak') $ VU.toList <$> frozenCov
, gasInfo = Map.toList $ Map.unionsWith max ((.gasInfo) <$> workerStates)
}

mapTest :: EchidnaTest -> Test
mapTest test =
mapTest :: DappInfo -> EchidnaTest -> Test
mapTest dappInfo test =
let (status, transactions, err) = mapTestState test.state test.reproducer
in Test
{ contract = "" -- TODO add when mapping is available https://github.com/crytic/echidna/issues/415
, name = "name" -- TODO add a proper name here
, status = status
, _error = err
, events = test.events
, events = maybe [] (extractEvents False dappInfo) test.vm
, testType = Property
, transactions = transactions
}
Expand Down
3 changes: 1 addition & 2 deletions lib/Echidna/Shrink.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ import Data.List qualified as List

import EVM.Types (VM)

import Echidna.Events (extractEvents)
import Echidna.Exec
import Echidna.Transaction
import Echidna.Types.Solidity (SolConf(..))
Expand All @@ -38,7 +37,7 @@ shrinkTest vm test = do
Just (txs, val, vm') -> do
Just test { state = Large (i + 1)
, reproducer = txs
, events = extractEvents False env.dapp vm'
, vm = Just vm'
, result = getResultFromVM vm'
, value = val }
Nothing ->
Expand Down
12 changes: 6 additions & 6 deletions lib/Echidna/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ getResultFromVM vm =
Nothing -> error "getResultFromVM failed"

createTest :: TestType -> EchidnaTest
createTest m = EchidnaTest Open m v [] Stop []
createTest m = EchidnaTest Open m v [] Stop Nothing
where v = case m of
PropertyTest _ _ -> BoolValue True
OptimizationTest _ _ -> IntValue minBound
Expand Down Expand Up @@ -114,17 +114,17 @@ createTests m td ts r ss = case m of
updateOpenTest
:: EchidnaTest
-> [Tx]
-> (TestValue, Events, TxResult)
-> (TestValue, VM RealWorld, TxResult)
-> EchidnaTest
updateOpenTest test txs (BoolValue False, es, r) =
test { Test.state = Large 0, reproducer = txs, events = es, result = r }
updateOpenTest test txs (BoolValue False, vm, r) =
test { Test.state = Large 0, reproducer = txs, vm = Just vm, result = r }
updateOpenTest test _ (BoolValue True, _, _) =
test
updateOpenTest test txs (IntValue v',es,r) =
updateOpenTest test txs (IntValue v', vm, r) =
if v' > v then
test { reproducer = txs
, value = IntValue v'
, events = es
, vm = Just vm
, result = r }
else
test
Expand Down
5 changes: 2 additions & 3 deletions lib/Echidna/Types/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ import Data.Text (Text)
import EVM.Dapp (DappInfo)
import EVM.Types (Addr, VM)

import Echidna.Events (Events)
import Echidna.Types (ExecException)
import Echidna.Types.Signature (SolSignature)
import Echidna.Types.Tx (Tx, TxResult)
Expand Down Expand Up @@ -85,8 +84,8 @@ data EchidnaTest = EchidnaTest
, value :: TestValue
, reproducer :: [Tx]
, result :: TxResult
, events :: Events
} deriving (Eq, Show)
, vm :: Maybe (VM RealWorld)
} deriving (Show)

isOptimizationTest :: EchidnaTest -> Bool
isOptimizationTest EchidnaTest{testType = OptimizationTest _ _} = True
Expand Down
64 changes: 32 additions & 32 deletions lib/Echidna/UI/Report.hs
Original file line number Diff line number Diff line change
@@ -1,28 +1,29 @@
module Echidna.UI.Report where

import Control.Monad.Reader (MonadReader, MonadIO (liftIO), asks)
import Control.Monad.ST (RealWorld)
import Data.IORef (readIORef)
import Data.List (intercalate, nub, sortOn)
import Data.Map (toList)
import Data.Maybe (catMaybes)
import Data.Map qualified as Map
import Data.Maybe (catMaybes, fromJust)
import Data.Text (Text, unpack)
import Data.Text qualified as T
import Data.Time (LocalTime)

import Echidna.ABI (GenDict(..), encodeSig)
import Echidna.Events (Events)
import Echidna.Pretty (ppTxCall)
import Echidna.Types (Gas)
import Echidna.Types.Campaign
import Echidna.Types.Config
import Echidna.Types.Corpus (corpusSize)
import Echidna.Types.Coverage (scoveragePoints)
import Echidna.Types.Test (EchidnaTest(..), TestState(..), TestType(..))
import Echidna.Types.Tx (Tx(..), TxCall(..), TxConf(..))
import Echidna.Types.Config

import EVM.Types (W256)
import Echidna.Types.Corpus (corpusSize)
import Echidna.Utility (timePrefix)
import qualified Data.Map as Map

import EVM.Format (showTraceTree)
import EVM.Types (W256, VM)

ppLogLine :: (Int, LocalTime, CampaignEvent) -> String
ppLogLine (workerId, time, event) =
Expand Down Expand Up @@ -96,71 +97,70 @@ ppGasOne (func, (gas, txs)) = do
pure $ header <> unlines ((" " <>) <$> prettyTxs)

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

ppEvents :: Events -> String
ppEvents es = if null es then "" else unlines $ "Event sequence:" : (T.unpack <$> es)
<> "Traces: \n" <> T.unpack (showTraceTree dappInfo vm)

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

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

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

-- | Pretty-print the status of a optimized test.
ppOptimized :: MonadReader Env m => Maybe (Int, Int) -> Events -> [Tx] -> m String
ppOptimized :: MonadReader Env m => Maybe (Int, Int) -> VM RealWorld -> [Tx] -> m String
ppOptimized _ _ [] = pure "Call sequence:\n(no transactions)"
ppOptimized b es xs = do
ppOptimized b vm xs = do
let status = case b of
Nothing -> ""
Just (n,m) -> ", shrinking " <> progress n m
prettyTxs <- mapM (ppTx $ length (nub $ (.src) <$> xs) /= 1) xs
dappInfo <- asks (.dapp)
pure $ "\n Call sequence" <> status <> ":\n"
<> unlines ((" " <>) <$> prettyTxs) <> "\n"
<> ppEvents es
<> "Traces: \n" <> T.unpack (showTraceTree dappInfo vm)

-- | Pretty-print the status of all 'SolTest's in a 'Campaign'.
ppTests :: (MonadReader Env m) => [EchidnaTest] -> m String
ppTests :: MonadReader Env m => [EchidnaTest] -> m String
ppTests tests = do
unlines . catMaybes <$> mapM pp tests
where
pp t =
case t.testType of
PropertyTest n _ -> do
status <- ppTS t.state t.events t.reproducer
status <- ppTS t.state (fromJust t.vm) t.reproducer
pure $ Just (T.unpack n <> ": " <> status)
CallTest n _ -> do
status <- ppTS t.state t.events t.reproducer
status <- ppTS t.state (fromJust t.vm) t.reproducer
pure $ Just (T.unpack n <> ": " <> status)
AssertionTest _ s _ -> do
status <- ppTS t.state t.events t.reproducer
status <- ppTS t.state (fromJust t.vm) t.reproducer
pure $ Just (T.unpack (encodeSig s) <> ": " <> status)
OptimizationTest n _ -> do
status <- ppOPT t.state t.events t.reproducer
status <- ppOPT t.state (fromJust t.vm) t.reproducer
pure $ Just (T.unpack n <> ": max value: " <> show t.value <> "\n" <> status)
Exploration -> pure Nothing

Expand Down
47 changes: 30 additions & 17 deletions lib/Echidna/UI/Widgets.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,15 @@ import Brick.Widgets.Border
import Brick.Widgets.Center
import Brick.Widgets.Dialog qualified as B
import Control.Monad.Reader (MonadReader, asks, ask)
import Control.Monad.ST (RealWorld)
import Data.List (nub, intersperse, sortBy)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe (fromMaybe, isJust)
import Data.Maybe (fromMaybe, isJust, fromJust)
import Data.Sequence (Seq)
import Data.Sequence qualified as Seq
import Data.String.AnsiEscapeCodes.Strip.Text (stripAnsiEscapeCodes)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Time (LocalTime, NominalDiffTime, formatTime, defaultTimeLocale, diffLocalTime)
import Data.Version (showVersion)
Expand All @@ -25,15 +28,15 @@ import Text.Printf (printf)
import Text.Wrap

import Echidna.ABI
import Echidna.Events (Events)
import Echidna.Types.Campaign
import Echidna.Types.Config
import Echidna.Types.Test
import Echidna.Types.Tx (Tx(..), TxResult(..))
import Echidna.UI.Report
import Echidna.Utility (timePrefix)

import EVM.Types (Addr, Contract, W256)
import EVM.Format (showTraceTree)
import EVM.Types (Addr, Contract, W256, VM(..))

data UIState = UIState
{ status :: UIStateStatus
Expand Down Expand Up @@ -276,36 +279,42 @@ tsWidget
-> EchidnaTest
-> m (Widget Name, Widget Name)
tsWidget (Failed e) _ = pure (str "could not evaluate", str $ show e)
tsWidget Solved t = failWidget Nothing t.reproducer t.events t.value t.result
tsWidget Solved t = failWidget Nothing t.reproducer (fromJust t.vm) t.value t.result
tsWidget Passed _ = pure (success $ str "PASSED!", emptyWidget)
tsWidget Open _ = pure (success $ str "passing", emptyWidget)
tsWidget (Large n) t = do
m <- asks (.cfg.campaignConf.shrinkLimit)
failWidget (if n < m then Just (n,m) else Nothing) t.reproducer t.events t.value t.result
failWidget (if n < m then Just (n,m) else Nothing) t.reproducer (fromJust t.vm) t.value t.result

titleWidget :: Widget n
titleWidget = str "Call sequence" <+> str ":"

eventWidget :: Events -> Widget n
eventWidget es =
if null es then str ""
else str "Event sequence" <+> str ":"
<=> strBreak (T.unpack $ T.intercalate "\n" es)
tracesWidget :: MonadReader Env m => VM RealWorld -> m (Widget n)
tracesWidget vm = do
dappInfo <- asks (.dapp)
-- TODO: showTraceTree does coloring with ANSI escape codes, we need to strip
-- those because they break the Brick TUI. Fix in hevm so we can display
-- colors here as well.
let traces = stripAnsiEscapeCodes $ showTraceTree dappInfo vm
pure $
if T.null traces then str ""
else str "Traces" <+> str ":" <=> (txtBreak traces)

failWidget
:: MonadReader Env m
=> Maybe (Int, Int)
-> [Tx]
-> Events
-> VM RealWorld
-> TestValue
-> TxResult
-> m (Widget Name, Widget Name)
failWidget _ [] _ _ _= pure (failureBadge, str "*no transactions made*")
failWidget b xs es _ r = do
failWidget b xs vm _ r = do
s <- seqWidget xs
traces <- tracesWidget vm
pure
( failureBadge <+> str (" with " ++ show r)
, status <=> titleWidget <=> s <=> eventWidget es
, status <=> titleWidget <=> s <=> str " " <=> traces
)
where
status = case b of
Expand All @@ -327,21 +336,22 @@ optWidget Open t =
"optimizing, max value: " ++ show t.value, emptyWidget)
optWidget (Large n) t = do
m <- asks (.cfg.campaignConf.shrinkLimit)
maxWidget (if n < m then Just (n,m) else Nothing) t.reproducer t.events t.value
maxWidget (if n < m then Just (n,m) else Nothing) t.reproducer (fromJust t.vm) t.value

maxWidget
:: MonadReader Env m
=> Maybe (Int, Int)
-> [Tx]
-> Events
-> VM RealWorld
-> TestValue
-> m (Widget Name, Widget Name)
maxWidget _ [] _ _ = pure (failureBadge, str "*no transactions made*")
maxWidget b xs es v = do
maxWidget b xs vm v = do
s <- seqWidget xs
traces <- tracesWidget vm
pure
( maximumBadge <+> str (" max value: " ++ show v)
, status <=> titleWidget <=> s <=> eventWidget es
, status <=> titleWidget <=> s <=> str " " <=> traces
)
where
status = case b of
Expand All @@ -367,4 +377,7 @@ maximumBadge = withAttr (attrName "maximum") $ str "OPTIMIZED!"
strBreak :: String -> Widget n
strBreak = strWrapWith $ defaultWrapSettings { breakLongWords = True }

txtBreak :: Text -> Widget n
txtBreak = txtWrapWith $ defaultWrapSettings { breakLongWords = True }

#endif
1 change: 1 addition & 0 deletions package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ dependencies:
- http-conduit
- html-conduit
- xml-conduit
- strip-ansi-escape

language: GHC2021

Expand Down
Loading

0 comments on commit f6e8fbb

Please sign in to comment.