Skip to content

Commit

Permalink
Improved shrinking removing reverts from reproducers (#1250)
Browse files Browse the repository at this point in the history
* remove reverted sequences from reproducers

* fixes

* concat NoCalls

* clean useless no calls when delay is zero

* avoid reversing transaction sequence
  • Loading branch information
ggrieco-tob authored May 28, 2024
1 parent 80acdf5 commit 55a8091
Show file tree
Hide file tree
Showing 2 changed files with 65 additions and 21 deletions.
67 changes: 46 additions & 21 deletions lib/Echidna/Shrink.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,15 @@ import Control.Monad.State.Strict (MonadIO)
import Control.Monad.ST (RealWorld)
import Data.Set qualified as Set
import Data.List qualified as List
import Data.Maybe (mapMaybe)

import EVM.Types (VM, VMType(Concrete))
import EVM.Types (VM, VMType(..))

import Echidna.Exec
import Echidna.Transaction
import Echidna.Types.Solidity (SolConf(..))
import Echidna.Types.Test (TestValue(..), EchidnaTest(..), TestState(..), isOptimizationTest)
import Echidna.Types.Tx (Tx(..))
import Echidna.Types.Tx (Tx(..), hasReverted, isUselessNoCall, catNoCalls, TxCall(..))
import Echidna.Types.Config
import Echidna.Types.Campaign (CampaignConf(..))
import Echidna.Test (getResultFromVM, checkETest)
Expand All @@ -31,24 +32,47 @@ shrinkTest vm test = do
Large i | i >= env.cfg.campaignConf.shrinkLimit && not (isOptimizationTest test) ->
pure $ Just test { state = Solved }
Large i ->
if length test.reproducer > 1 || any canShrinkTx test.reproducer then do
maybeShrunk <- shrinkSeq vm (checkETest test) test.value test.reproducer
pure $ case maybeShrunk of
Just (txs, val, vm') -> do
Just test { state = Large (i + 1)
, reproducer = txs
, vm = Just vm'
, result = getResultFromVM vm'
, value = val }
Nothing ->
-- No success with shrinking this time, just bump trials
Just test { state = Large (i + 1) }
else
pure $ Just test { state = if isOptimizationTest test
then Large (i + 1)
else Solved }
do repro <- removeReverts vm test.reproducer
let rr = removeUselessNoCalls $ catNoCalls repro
if length rr > 1 || any canShrinkTx rr then do
maybeShrunk <- shrinkSeq vm (checkETest test) test.value rr
pure $ case maybeShrunk of
Just (txs, val, vm') -> do
Just test { state = Large (i + 1)
, reproducer = txs
, vm = Just vm'
, result = getResultFromVM vm'
, value = val }
Nothing ->
-- No success with shrinking this time, just bump trials
Just test { state = Large (i + 1), reproducer = rr}
else
pure $ Just test { state = if isOptimizationTest test
then Large (i + 1)
else Solved }
_ -> pure Nothing

replaceByNoCall :: Tx -> Tx
replaceByNoCall tx = tx { call = NoCall }

removeUselessNoCalls :: [Tx] -> [Tx]
removeUselessNoCalls = mapMaybe f
where f tx = if isUselessNoCall tx then Nothing else Just tx

removeReverts :: (MonadIO m, MonadReader Env m, MonadThrow m) => VM Concrete RealWorld -> [Tx] -> m [Tx]
removeReverts vm txs = do
let (itxs, le) = (init txs, last txs)
ftxs <- removeReverts' vm itxs []
return (ftxs ++ [le])

removeReverts' :: (MonadIO m, MonadReader Env m, MonadThrow m) => VM Concrete RealWorld -> [Tx] -> [Tx] -> m [Tx]
removeReverts' _ [] ftxs = return $ reverse ftxs
removeReverts' vm (t:txs) ftxs = do
(_, vm') <- execTx vm t
if hasReverted vm'
then removeReverts' vm' txs (replaceByNoCall t: ftxs)
else removeReverts' vm' txs (t:ftxs)

-- | Given a call sequence that solves some Echidna test, try to randomly
-- generate a smaller one that still solves that test.
shrinkSeq
Expand All @@ -60,11 +84,12 @@ shrinkSeq
-> m (Maybe ([Tx], TestValue, VM Concrete RealWorld))
shrinkSeq vm f v txs = do
txs' <- uniform =<< sequence [shorten, shrunk]
(value, vm') <- check txs' vm
let txs'' = removeUselessNoCalls txs'
(value, vm') <- check txs'' vm
-- if the test passed it means we didn't shrink successfully
pure $ case (value,v) of
(BoolValue False, _) -> Just (txs', value, vm')
(IntValue x, IntValue y) | x >= y -> Just (txs', value, vm')
(BoolValue False, _) -> Just (txs'', value, vm')
(IntValue x, IntValue y) | x >= y -> Just (txs'', value, vm')
_ -> Nothing
where
check [] vm' = f vm'
Expand Down
19 changes: 19 additions & 0 deletions lib/Echidna/Types/Tx.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ module Echidna.Types.Tx where
import Prelude hiding (Word)

import Control.Applicative ((<|>))
import Control.Monad.ST (RealWorld)
import Data.Aeson (FromJSON, ToJSON, parseJSON, toJSON, object, withObject, (.=), (.:))
import Data.Aeson.TH (deriveJSON, defaultOptions)
import Data.Aeson.Types (Parser)
Expand Down Expand Up @@ -199,6 +200,24 @@ data TxConf = TxConf
-- ^ Maximum value to use in transactions
}

hasReverted :: VM Concrete RealWorld -> Bool
hasReverted vm = let r = vm.result in
case r of
(Just (VMSuccess _)) -> False
_ -> True

isUselessNoCall :: Tx -> Bool
isUselessNoCall tx = tx.call == NoCall && tx.delay == (0, 0)

catNoCalls :: [Tx] -> [Tx]
catNoCalls [] = []
catNoCalls [tx] = [tx]
catNoCalls (tx1:tx2:xs) =
case (tx1.call, tx2.call) of
(NoCall, NoCall) -> catNoCalls (nc:xs)
_ -> tx1 : catNoCalls (tx2:xs)
where nc = tx1 { delay = (fst tx1.delay + fst tx2.delay, snd tx1.delay + snd tx2.delay) }

-- | Transform a VMResult into a more hash friendly sum type
getResult :: VMResult Concrete s -> TxResult
getResult = \case
Expand Down

0 comments on commit 55a8091

Please sign in to comment.