Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
make worker type deterministic based on config and id; update events …
Browse files Browse the repository at this point in the history
…to reflect things that can happen with symbolic
samalws-tob committed Apr 8, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
1 parent 00e8bc2 commit c0c2be8
Showing 7 changed files with 51 additions and 26 deletions.
24 changes: 14 additions & 10 deletions lib/Echidna/Campaign.hs
Original file line number Diff line number Diff line change
@@ -5,7 +5,7 @@ module Echidna.Campaign where

import Control.Concurrent
import Control.DeepSeq (force)
import Control.Monad (replicateM, when, void, forM_)
import Control.Monad (replicateM, when, unless, void, forM_)
import Control.Monad.Catch (MonadThrow(..))
import Control.Monad.Random.Strict (MonadRandom, RandT, evalRandT)
import Control.Monad.Reader (MonadReader, asks, liftIO, ask)
@@ -122,7 +122,7 @@ runSymWorker callback vm dict workerId initialCorpus name cs = do
lift callback
void $ replayCorpus vm initialCorpus
listenerLoop listenerFunc chan nworkers
pure TestLimitReached
pure SymbolicDone

where

@@ -138,7 +138,7 @@ runSymWorker callback vm dict workerId initialCorpus name cs = do
, runningThreads = []
}

listenerFunc (_, WorkerEvent _ (NewCoverage {transactions})) = do
listenerFunc (_, WorkerEvent _ FuzzWorker (NewCoverage {transactions})) = do
void $ callseq vm transactions
symexecTxs transactions
listenerFunc _ = pure ()
@@ -156,7 +156,9 @@ runSymWorker callback vm dict workerId initialCorpus name cs = do
modify' (\ws -> ws { runningThreads = [] })
lift callback

mapM_ (\symTx -> void $ callseq vm' [symTx]) symTxs
newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm' [symTx]) symTxs

unless newCoverage (pushWorkerEvent SymNoNewCoverage)

-- | Run a fuzzing campaign given an initial universe state, some tests, and an
-- optional dictionary to generate calls with. Return the 'Campaign' state once
@@ -231,7 +233,7 @@ runFuzzWorker callback vm world dict workerId initialCorpus testLimit = do
| otherwise ->
lift callback >> pure TestLimitReached

fuzz = randseq vm.env.contracts world >>= callseq vm
fuzz = randseq vm.env.contracts world >>= fmap fst . callseq vm

continue = runUpdate (shrinkTest vm) >> lift callback >> run

@@ -268,11 +270,12 @@ randseq deployedContracts world = do

-- | Runs a transaction sequence and checks if any test got falsified or can be
-- minimized. Stores any useful data in the campaign state if coverage increased.
-- Returns resulting VM, as well as whether any new coverage was found.
callseq
:: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
=> VM Concrete RealWorld
-> [Tx]
-> m (VM Concrete RealWorld)
-> m (VM Concrete RealWorld, Bool)
callseq vm txSeq = do
env <- ask
-- First, we figure out whether we need to execute with or without coverage
@@ -337,7 +340,7 @@ callseq vm txSeq = do
, ncallseqs = workerState.ncallseqs + 1
}

pure vm'
pure (vm', newCoverage)

where
-- Given a list of transactions and a return typing rule, checks whether we
@@ -485,7 +488,8 @@ pushWorkerEvent
pushWorkerEvent event = do
workerId <- gets (.workerId)
env <- ask
liftIO $ pushCampaignEvent env (WorkerEvent workerId event)
let workerType = workerIDToType env.cfg.campaignConf workerId
liftIO $ pushCampaignEvent env (WorkerEvent workerId workerType event)

pushCampaignEvent :: Env -> CampaignEvent -> IO ()
pushCampaignEvent env event = do
@@ -530,5 +534,5 @@ listenerLoop handler chan !workersAlive =
event <- liftIO $ readChan chan
handler event
case event of
(_, WorkerEvent _ (WorkerStopped _)) -> listenerLoop handler chan (workersAlive - 1)
_ -> listenerLoop handler chan workersAlive
(_, WorkerEvent _ _ (WorkerStopped _)) -> listenerLoop handler chan (workersAlive - 1)
_ -> listenerLoop handler chan workersAlive
2 changes: 1 addition & 1 deletion lib/Echidna/Output/Corpus.hs
Original file line number Diff line number Diff line change
@@ -42,7 +42,7 @@ saveCorpusEvent env (_time, campaignEvent) = do
Just corpusDir -> saveEvent corpusDir campaignEvent
Nothing -> pure ()
where
saveEvent dir (WorkerEvent _workerId event) =
saveEvent dir (WorkerEvent _workerId _workerType event) =
maybe (pure ()) (saveFile dir) $ getEventInfo event
saveEvent _ _ = pure ()

12 changes: 9 additions & 3 deletions lib/Echidna/Server.hs
Original file line number Diff line number Diff line change
@@ -16,11 +16,16 @@ import Echidna.Types.Config (Env(..))
newtype SSE = SSE (LocalTime, CampaignEvent)

instance ToJSON SSE where
toJSON (SSE (time, WorkerEvent workerId event)) =
toJSON (SSE (time, WorkerEvent workerId workerType event)) =
object [ "worker" .= workerId
, "workerType" .= workerTypeString workerType
, "timestamp" .= time
, "data" .= event
]
where
workerTypeString :: WorkerType -> String
workerTypeString SymbolicWorker = "symbolic"
workerTypeString FuzzWorker = "fuzz"
toJSON (SSE (time, Failure reason)) =
object [ "timestamp" .= time
, "data" .= reason
@@ -38,17 +43,18 @@ runSSEServer serverStopVar env port nworkers = do
else do
event@(_, campaignEvent) <- readChan sseChan
let eventName = \case
WorkerEvent _ workerEvent ->
WorkerEvent _ _ workerEvent ->
case workerEvent of
TestFalsified _ -> "test_falsified"
TestOptimized _ -> "test_optimized"
NewCoverage {} -> "new_coverage"
SymNoNewCoverage -> "sym_no_new_coverage"
TxSequenceReplayed {} -> "tx_sequence_replayed"
TxSequenceReplayFailed {} -> "tx_sequence_replay_failed"
WorkerStopped _ -> "worker_stopped"
Failure _err -> "failure"
case campaignEvent of
WorkerEvent _ (WorkerStopped _) -> do
WorkerEvent _ _ (WorkerStopped _) -> do
aliveAfter <- atomicModifyIORef' aliveRef (\n -> (n-1, n-1))
when (aliveAfter == 0) $ putMVar serverStopVar ()
_ -> pure ()
16 changes: 13 additions & 3 deletions lib/Echidna/Types/Campaign.hs
Original file line number Diff line number Diff line change
@@ -54,25 +54,27 @@ data CampaignConf = CampaignConf
-- Only relevant if symExec is True
}

data WorkerType = FuzzWorker | SymbolicWorker
data WorkerType = FuzzWorker | SymbolicWorker deriving (Eq)

type WorkerId = Int

data CampaignEvent
= WorkerEvent WorkerId WorkerEvent
= WorkerEvent WorkerId WorkerType WorkerEvent
| Failure String

data WorkerEvent
= TestFalsified !EchidnaTest
| TestOptimized !EchidnaTest
| NewCoverage { points :: !Int, numCodehashes :: !Int, corpusSize :: !Int, transactions :: [Tx] }
| SymNoNewCoverage
| TxSequenceReplayed FilePath !Int !Int
| TxSequenceReplayFailed FilePath Tx
| WorkerStopped WorkerStopReason
-- ^ This is a terminal event. Worker exits and won't push any events after
-- this one
deriving Show

-- TODO
instance ToJSON WorkerEvent where
toJSON = \case
TestFalsified test -> toJSON test
@@ -87,6 +89,7 @@ instance ToJSON WorkerEvent where

data WorkerStopReason
= TestLimitReached
| SymbolicDone
| TimeLimitReached
| FastFailed
| Killed !String
@@ -95,7 +98,7 @@ data WorkerStopReason

ppCampaignEvent :: CampaignEvent -> String
ppCampaignEvent = \case
WorkerEvent _ e -> ppWorkerEvent e
WorkerEvent _ _ e -> ppWorkerEvent e
Failure err -> err

ppWorkerEvent :: WorkerEvent -> String
@@ -109,6 +112,8 @@ ppWorkerEvent = \case
"New coverage: " <> show points <> " instr, "
<> show numCodehashes <> " contracts, "
<> show corpusSize <> " seqs in corpus"
SymNoNewCoverage ->
"Symbolic execution finished with no new coverage."
TxSequenceReplayed file current total ->
"Sequence replayed from corpus file " <> file <> " (" <> show current <> "/" <> show total <> ")"
TxSequenceReplayFailed file tx ->
@@ -117,6 +122,8 @@ ppWorkerEvent = \case
"Remove the file or the transaction to fix the issue."
WorkerStopped TestLimitReached ->
"Test limit reached. Stopping."
WorkerStopped SymbolicDone ->
"Symbolic worker ran out of transactions to work on. Stopping."
WorkerStopped TimeLimitReached ->
"Time limit reached. Stopping."
WorkerStopped FastFailed ->
@@ -181,3 +188,6 @@ getNFuzzWorkers conf = fromIntegral (fromMaybe 1 (conf.workers))
-- | Number of workers, including SymExec worker if there is one
getNWorkers :: CampaignConf -> Int
getNWorkers conf = getNFuzzWorkers conf + (if conf.symExec then 1 else 0)

workerIDToType :: CampaignConf -> WorkerId -> WorkerType
workerIDToType conf wid = if conf.symExec && wid == (getNWorkers conf - 1) then SymbolicWorker else FuzzWorker
11 changes: 5 additions & 6 deletions lib/Echidna/UI.hs
Original file line number Diff line number Diff line change
@@ -222,12 +222,11 @@ ui vm world dict initialCorpus cliSelectedContract cs = do

threadId <- forkIO $ do
-- TODO: maybe figure this out with forkFinally?
let workerType = workerIDToType env.cfg.campaignConf workerId
stopReason <- catches (do
let
timeoutUsecs = maybe (-1) (*1_000_000) env.cfg.uiConf.maxTime
isSym = env.cfg.campaignConf.symExec && workerId == (getNWorkers env.cfg.campaignConf)-1
corpus = if isSym then initialCorpus else corpusChunk
workerType = if isSym then SymbolicWorker else FuzzWorker
corpus = if workerType == SymbolicWorker then initialCorpus else corpusChunk
maybeResult <- timeout timeoutUsecs $
runWorker workerType (get >>= writeIORef stateRef)
vm world dict workerId corpus testLimit cliSelectedContract cs
@@ -240,7 +239,7 @@ ui vm world dict initialCorpus cliSelectedContract cs = do
]

time <- liftIO getTimestamp
writeChan env.eventQueue (time, WorkerEvent workerId (WorkerStopped stopReason))
writeChan env.eventQueue (time, WorkerEvent workerId workerType (WorkerStopped stopReason))

pure (threadId, stateRef)

@@ -285,14 +284,14 @@ monitor = do
modify' $ \state -> state { events = state.events |> event }

case campaignEvent of
WorkerEvent _ (NewCoverage { points, numCodehashes, corpusSize }) ->
WorkerEvent _ _ (NewCoverage { points, numCodehashes, corpusSize }) ->
modify' $ \state ->
state { coverage = max state.coverage points -- max not really needed
, corpusSize
, numCodehashes
, lastNewCov = time
}
WorkerEvent _ (WorkerStopped _) ->
WorkerEvent _ _ (WorkerStopped _) ->
modify' $ \state ->
state { workersAlive = state.workersAlive - 1
, timeStopped = if state.workersAlive == 1
4 changes: 3 additions & 1 deletion lib/Echidna/UI/Report.hs
Original file line number Diff line number Diff line change
@@ -30,8 +30,10 @@ import EVM.Solidity (SolcContract(..))
import EVM.Types (W256, VM, VMType(Concrete), Addr, Expr (LitAddr))

ppLogLine :: (LocalTime, CampaignEvent) -> String
ppLogLine (time, event@(WorkerEvent workerId _)) =
ppLogLine (time, event@(WorkerEvent workerId FuzzWorker _)) =
timePrefix time <> "[Worker " <> show workerId <> "] " <> ppCampaignEvent event
ppLogLine (time, event@(WorkerEvent workerId SymbolicWorker _)) =
timePrefix time <> "[Worker " <> show workerId <> ", symbolic] " <> ppCampaignEvent event
ppLogLine (time, event) =
timePrefix time <> " " <> ppCampaignEvent event

8 changes: 6 additions & 2 deletions lib/Echidna/UI/Widgets.hs
Original file line number Diff line number Diff line change
@@ -146,9 +146,13 @@ logPane uiState =
foldl (<=>) emptyWidget (showLogLine <$> Seq.reverse uiState.events)

showLogLine :: (LocalTime, CampaignEvent) -> Widget Name
showLogLine (time, event@(WorkerEvent workerId _)) =
(withAttr (attrName "time") $ str $ (timePrefix time) <> "[Worker " <> show workerId <> "] ")
showLogLine (time, event@(WorkerEvent workerId workerType _)) =
(withAttr (attrName "time") $ str $ (timePrefix time) <> "[Worker " <> show workerId <> symSuffix <> "] ")
<+> strBreak (ppCampaignEvent event)
where
symSuffix = case workerType of
SymbolicWorker -> ", symbolic"
_ -> ""
showLogLine (time, event) =
(withAttr (attrName "time") $ str $ (timePrefix time) <> " ") <+> strBreak (ppCampaignEvent event)

0 comments on commit c0c2be8

Please sign in to comment.