hevm 0.42 (#511)

* hevm-0.41.x

* Buffer.hs

* fix some non-exhaustive patterns

* actually implement viewBuffer lol

* disable gas price usage until hevm fixes its issue

* upgrade to hevm-0.42 and fix tests

* fixed test + default value

* fixed test + default value

* upgrade to sbv 8.8

Co-authored-by: ggrieco-tob <gustavo.grieco@trailofbits.com>

examples/solidity/basic/default.yaml

@@ -8,7 +8,7 @@ propMaxGas: 8000030
 #testMaxGas is a gas limit; does not cause failure, but terminates sequence
 testMaxGas: 8000030
 #maxGasprice is the maximum gas price
-maxGasprice: 100000000000
+maxGasprice: 0
 #testLimit is the number of test sequences to run
 testLimit: 50000
 #stopOnFail makes echidna terminate as soon as any property fails and has been shrunk

examples/solidity/basic/gasprice.yaml

@@ -0,0 +1 @@
+maxGasprice: 10000000

lib/Echidna.hs

@@ -5,7 +5,6 @@ module Echidna where
 import Control.Lens (view, (^.), to)
 import Data.Has (Has(..))
 import Control.Monad.Catch (MonadCatch(..))
-import Control.Monad.Fail  (MonadFail(..))
 import Control.Monad.Reader (MonadReader, MonadIO, liftIO)
 import Control.Monad.Random (MonadRandom)
 import Data.Map.Strict (keys)

lib/Echidna/Campaign.hs

@@ -26,10 +26,9 @@ import Data.Maybe (fromMaybe, isJust, mapMaybe)
 import Data.Ord (comparing)
 import Data.Has (Has(..))
 import Data.Text (Text)
-import Data.Traversable (traverse)
 import EVM
 import EVM.ABI (getAbi, AbiType(AbiAddressType), AbiValue(AbiAddress))
-import EVM.Types (Addr)
+import EVM.Types (Addr, Buffer(..))
 import System.Random (mkStdGen)
 
 import qualified Data.HashMap.Strict as H
@@ -248,8 +247,10 @@ callseq v w ql = do
     -- type for each function called, and if we do, tries to parse the return value as a value of that
     -- type. It returns a 'GenDict' style HashMap.
     parse l rt = H.fromList . flip mapMaybe l $ \(x, r) -> case (rt =<< x ^? call . _SolCall . _1, r) of
-      (Just ty, VMSuccess b) -> (ty, ) . S.fromList . pure <$> runGetOrFail (getAbi ty) (b ^. lazy) ^? _Right . _3
-      _                      -> Nothing
+      (Just ty, VMSuccess (ConcreteBuffer b)) ->
+        (ty, ) . S.fromList . pure <$> runGetOrFail (getAbi ty) (b ^. lazy) ^? _Right . _3
+      _                                       ->
+        Nothing
 
 -- | Run a fuzzing campaign given an initial universe state, some tests, and an optional dictionary
 -- to generate calls with. Return the 'Campaign' state once we can't solve or shrink anything.

lib/Echidna/Config.hs

@@ -16,7 +16,6 @@ import Control.Monad.State (StateT(..), runStateT)
 import Control.Monad.Trans (lift)
 import Data.Bool (bool)
 import Data.Aeson
-import Data.Functor ((<&>))
 import Data.Has (Has(..))
 import Data.HashMap.Strict (keys)
 import Data.HashSet (HashSet, fromList, insert, difference)
@@ -108,7 +107,7 @@ instance FromJSON EConfigWithUsage where
                 getWord s d = C Dull . fromIntegral <$> v ..:? s ..!= (d :: Integer)
                 xc = TxConf <$> getWord "propMaxGas" maxGasPerBlock
                             <*> getWord "testMaxGas" maxGasPerBlock
-                            <*> getWord "maxGasprice" 100000000000
+                            <*> getWord "maxGasprice" 0
                             <*> getWord "maxTimeDelay" defaultTimeDelay     
                             <*> getWord "maxBlockDelay" defaultBlockDelay
                             <*> getWord "maxValue" 100000000000000000000 -- 100 eth

lib/Echidna/Exec.hs

@@ -18,6 +18,8 @@ import EVM
 import EVM.Op (Op(..))
 import EVM.Exec (exec, vmForEthrunCreation)
 import EVM.Solidity (stripBytecodeMetadata)
+import EVM.Types (Buffer(..))
+import EVM.Symbolic (litWord)
 
 import qualified Data.ByteString as BS
 import qualified Data.Map as M
@@ -79,7 +81,7 @@ execTxWith h m t = do
       hasLens . state . calldata .= cd
       hasLens . result ?= f
     (VMFailure x, _) -> h x
-    (VMSuccess bc, SolCreate _) ->
+    (VMSuccess (ConcreteBuffer bc), SolCreate _) ->
       (hasLens %=) . execState $ do
         env . contracts . at (t ^. dst) . _Just . contractcode .= InitCode ""
         replaceCodeOfSelf (RuntimeCode bc)
@@ -125,6 +127,6 @@ traceCoverage = do
   hasLens <>= [readOp (BS.index c $ v ^. state . pc) c]
 
 initialVM :: VM
-initialVM = vmForEthrunCreation mempty & block . timestamp .~ initialTimestamp
+initialVM = vmForEthrunCreation mempty & block . timestamp .~ litWord initialTimestamp
                                        & block . number .~ initialBlockNumber
                                        & env . contracts .~ fromList []       -- fixes weird nonce issues

lib/Echidna/Mutator.hs

@@ -3,7 +3,6 @@
 module Echidna.Mutator where
 
 import Control.Monad.Random.Strict (fromList, MonadRandom, getRandomR)
-import Data.Maybe (maybe)
 
 import qualified Data.ListLike as LL
 

lib/Echidna/RPC.hs

@@ -18,13 +18,12 @@ import Data.Aeson (FromJSON(..), (.:), withObject, eitherDecodeFileStrict)
 import Data.Binary.Get (runGetOrFail)
 import Data.ByteString.Char8 (ByteString)
 import Data.Has (Has(..))
-import Data.Maybe (maybe)
 import Data.Text.Encoding (encodeUtf8)
 import EVM
 import EVM.ABI (AbiType(..), getAbi)
 import EVM.Concrete (w256)
 import EVM.Exec (exec)
-import EVM.Types (Addr, W256)
+import EVM.Types (Addr, Buffer(..), W256)
 import Text.Read (readMaybe)
 
 import qualified Control.Monad.Fail as M (MonadFail(..))
@@ -105,7 +104,7 @@ execEthenoTxs ts addr et = do
   case (res, et) of
        (Reversion,   _)               -> throwM $ EthenoException "Encountered reversion while setting up Etheno transactions"
        (VMFailure x, _)               -> vmExcept x >> M.fail "impossible"
-       (VMSuccess bc,
+       (VMSuccess (ConcreteBuffer bc),
         ContractCreated _ ca _ _ _ _) -> do
           hasLens . env . contracts . at ca . _Just . contractcode .= InitCode ""
           liftSH (replaceCodeOfSelf (RuntimeCode bc) >> loadContract ca)
@@ -121,7 +120,7 @@ execEthenoTxs ts addr et = do
                               -- execute x and check if it returned something of the correct type
                               go (x:xs) = setupTx x >> liftSH exec >>= \case
                                 -- executing the test function succeeded
-                                VMSuccess r -> do
+                                VMSuccess (ConcreteBuffer r) -> do
                                   put og
                                   case runGetOrFail (getAbi . AbiTupleType . V.fromList $ [AbiBoolType]) (r ^. lazy) ^? _Right . _3 of
                                        -- correct type ==> check the rest of the tests

lib/Echidna/Solidity.hs

@@ -12,7 +12,6 @@ import Control.Exception          (Exception)
 import Control.Monad              (liftM2, when, unless, void)
 import Control.Monad.Catch        (MonadThrow(..))
 import Control.Monad.IO.Class     (MonadIO(..))
-import Control.Monad.Fail         (MonadFail)
 import Control.Monad.Reader       (MonadReader)
 import Control.Monad.State.Strict (execStateT)
 import Data.Aeson                 (Value(..))
@@ -24,7 +23,6 @@ import Data.List                  (find, nub, partition)
 import Data.List.Lens             (prefixed, suffixed)
 import Data.Map                   (elems)
 import Data.Maybe                 (isJust, isNothing, catMaybes)
-import Data.Monoid                ((<>))
 import Data.Text                  (Text, isPrefixOf, isSuffixOf, append)
 import Data.Text.Lens             (unpacked)
 import Data.Text.Read             (decimal)
@@ -40,7 +38,7 @@ import Echidna.Types.Tx           (TxConf, TxCall(..), Tx(..), unlimitedGasPerBl
 import Echidna.Types.World        (World(..))
 import Echidna.Processor
 
-import EVM hiding (contracts)
+import EVM hiding (contracts, path)
 import qualified EVM (contracts)
 import EVM.ABI
 import EVM.Solidity

lib/Echidna/Test.hs

@@ -25,6 +25,7 @@ import Echidna.ABI
 import Echidna.Exec
 import Echidna.Solidity
 import Echidna.Transaction
+import Echidna.Types.Buffer (viewBuffer)
 import Echidna.Types.Tx (TxCall(..), Tx(..), TxConf, propGas, src)
 
 -- | Configuration for evaluating Echidna tests.
@@ -41,9 +42,9 @@ data CallRes = ResFalse | ResTrue | ResRevert | ResOther deriving (Eq, Show)
 
 -- | Given a 'VMResult', classify it assuming it was the result of a call to an Echidna test.
 classifyRes :: VMResult -> CallRes
-classifyRes (VMSuccess b) | b == encodeAbiValue (AbiBool True)  = ResTrue
-                          | b == encodeAbiValue (AbiBool False) = ResFalse
-                          | otherwise                           = ResOther
+classifyRes (VMSuccess b) | viewBuffer b == Just (encodeAbiValue (AbiBool True))  = ResTrue
+                          | viewBuffer b == Just (encodeAbiValue (AbiBool False)) = ResFalse
+                          | otherwise                                             = ResOther
 
 classifyRes Reversion = ResRevert
 classifyRes _ = ResOther
@@ -60,13 +61,15 @@ checkETest t = do
   --   * matchC[alldata] checks if we just executed the function we thought we did, based on calldata
   let matchR (Just (VMFailure (UnrecognizedOpcode 0xfe))) = False
       matchR _                                            = True
-      matchC sig = not . (BS.isPrefixOf . BS.take 4 $ abiCalldata (encodeSig sig) mempty)
+      matchC sig b = case viewBuffer b of
+        Just cd -> not . BS.isPrefixOf (BS.take 4 (abiCalldata (encodeSig sig) mempty)) $ cd
+        Nothing -> False
   res <- case t of
     -- If our test is a regular user-defined test, we exec it and check the result
     Left  (f, a) -> execTx (Tx (SolCall (f, [])) (s a) a g 0 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)
+                         <*> fmap (matchC sig) (use $ hasLens . state . calldata . _1)
   put vm -- restore EVM state
   pure res
 

lib/Echidna/Transaction.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -20,11 +21,13 @@ import Data.Has (Has(..))
 import Data.Hashable (hash)
 import Data.Map (Map, toList)
 import Data.Maybe (catMaybes)
-import EVM hiding (value)
+import Data.SBV (SWord, literal)
+import EVM hiding (value, path)
 import EVM.ABI (abiCalldata, abiValueType)
 import EVM.Concrete (Word(..), w256)
 import EVM.Solidity (stripBytecodeMetadata)
-import EVM.Types (Addr)
+import EVM.Symbolic ( litWord, litAddr)
+import EVM.Types (Addr, Buffer(..))
 
 import qualified System.Directory as SD
 import qualified Data.ByteString as BS
@@ -84,12 +87,12 @@ genTxM :: (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has Gen
   => Map Addr Contract
   -> m Tx
 genTxM m = do
-  TxConf _ g maxGp t b mv <- view hasLens
+  TxConf _ g gp t b mv <- view hasLens
   genTxWith
     m
     rElem rElem                                                                -- src and dst
     (const $ genInteractionsM . snd)                                           -- call itself
-    (pure g) (inRange maxGp) mv                                                -- gas, gasprice, value
+    (pure g) (pure gp) mv                                                      -- gas, gasprice, value
     (level <$> liftM2 (,) (inRange t) (inRange b))                             -- delay
   where inRange hi = w256 . fromIntegral <$> getRandomR (0 :: Integer, fromIntegral hi)
 
@@ -145,16 +148,20 @@ liftSH = stateST . runState . zoom hasLens
 setupTx :: (MonadState x m, Has VM x) => Tx -> m ()
 setupTx (Tx c s r g gp v (t, b)) = liftSH . sequence_ $
   [ result .= Nothing, state . pc .= 0, state . stack .= mempty, state . memory .= mempty, state . gas .= g
-  , tx . gasprice .= gp, tx . origin .= s, state . caller .= s, state . callvalue .= v
-  , block . timestamp += t, block . number += b, setup] where
+  , tx . gasprice .= gp, tx . origin .= s, state . caller .= litAddr s, state . callvalue .= litWord v
+  , block . timestamp += litWord t, block . number += b, setup] where
     setup = case c of
       SolCreate bc   -> assign (env . contracts . at r) (Just $ initialContract (InitCode bc) & set balance v) >> loadContract r >> state . code .= bc
-      SolCall cd     -> incrementBalance >> loadContract r >> state . calldata .= encode cd
-      SolCalldata cd -> incrementBalance >> loadContract r >> state . calldata .= cd
+      SolCall cd     -> incrementBalance >> loadContract r >> state . calldata .= concreteCalldata (encode cd)
+      SolCalldata cd -> incrementBalance >> loadContract r >> state . calldata .= concreteCalldata cd
     incrementBalance = (env . contracts . ix r . balance) += v
     encode (n, vs) = abiCalldata
       (encodeSig (n, abiValueType <$> vs)) $ V.fromList vs
 
+
+concreteCalldata :: BS.ByteString -> (Buffer, SWord 32)
+concreteCalldata cd = (ConcreteBuffer cd, literal . fromIntegral . BS.length $ cd)
+
 saveTxs :: Maybe FilePath -> [[Tx]] -> IO ()
 saveTxs (Just d) txs = mapM_ saveTx txs where
   saveTx v = do let fn = d ++ "/" ++ (show . hash . show) v ++ ".txt"

lib/Echidna/Types/Buffer.hs

@@ -0,0 +1,9 @@
+module Echidna.Types.Buffer where
+
+import Data.ByteString (ByteString)
+import EVM.Types (Buffer(..))
+import EVM.Symbolic (maybeLitBytes)
+
+viewBuffer :: Buffer -> Maybe ByteString
+viewBuffer (ConcreteBuffer b) = Just b
+viewBuffer (SymbolicBuffer b) = maybeLitBytes b

lib/Echidna/Types/Tx.hs

@@ -71,7 +71,11 @@ data TxResult = Success
               | ErrorInvalidMemoryAccess
               | ErrorCallDepthLimitReached
               | ErrorMaxCodeSizeExceeded
-              | ErrorPrecompileFailure      deriving (Eq, Ord, Show)
+              | ErrorPrecompileFailure
+              | ErrorUnexpectedSymbolic
+              | ErrorDeadPath
+              | ErrorChoose -- not entirely sure what this is
+  deriving (Eq, Ord, Show)
 $(deriveJSON defaultOptions ''TxResult)
 
 data TxConf = TxConf { _propGas       :: Word
@@ -88,7 +92,6 @@ data TxConf = TxConf { _propGas       :: Word
                      -- ^ Maximum value to use in transactions  
                      }
 makeLenses 'TxConf
-
 -- | Transform a VMResult into a more hash friendly sum type
 getResult :: VMResult -> TxResult
 getResult (VMSuccess _)                         = Success
@@ -109,3 +112,6 @@ getResult (VMFailure InvalidMemoryAccess)       = ErrorInvalidMemoryAccess
 getResult (VMFailure CallDepthLimitReached)     = ErrorCallDepthLimitReached
 getResult (VMFailure (MaxCodeSizeExceeded _ _)) = ErrorMaxCodeSizeExceeded
 getResult (VMFailure PrecompileFailure)         = ErrorPrecompileFailure
+getResult (VMFailure UnexpectedSymbolicArg)     = ErrorUnexpectedSymbolic
+getResult (VMFailure DeadPath)                  = ErrorDeadPath
+getResult (VMFailure (Choose _))                = ErrorChoose -- not entirely sure what this is

lib/Echidna/UI.hs

@@ -111,7 +111,9 @@ ui v w ts d txs = do
           Just _ -> liftIO $ updateUI CampaignUpdated
         )
         (const $ liftIO $ killThread ticker)
-      app <- customMain (mkVty vtyConfig) (Just bc) <$> monitor
+      let vty = mkVty vtyConfig
+      initialVty <- liftIO vty
+      app <- customMain initialVty vty (Just bc) <$> monitor
       liftIO $ void $ app (defaultCampaign, Uninitialized)
       final <- liftIO $ readIORef ref
       liftIO . putStrLn =<< ppCampaign final

lib/Echidna/UI/Report.hs

@@ -8,7 +8,7 @@ import Control.Monad.Reader (MonadReader)
 import Data.Has (Has(..))
 import Data.List (intercalate, nub, sortOn)
 import Data.Map (toList)
-import Data.Maybe (catMaybes, maybe)
+import Data.Maybe (catMaybes)
 import Data.Text (Text, unpack)
 import EVM.Types (Addr)
 

lib/Echidna/UI/Widgets.hs

@@ -11,7 +11,6 @@ import Control.Lens
 import Control.Monad.Reader (MonadReader)
 import Data.Has (Has(..))
 import Data.List (nub, intersperse)
-import Data.Maybe (maybe)
 import Data.Version (showVersion)
 import Text.Printf (printf)
 

package.yaml

@@ -13,7 +13,7 @@ dependencies:
   - ansi-terminal
   - base16-bytestring
   - binary
-  - brick                <= 0.46
+  - brick
   - base16-bytestring
   - bytestring
   - containers
@@ -35,6 +35,7 @@ dependencies:
   - optparse-applicative
   - process
   - random
+  - sbv
   - stm
   - temporary
   - text

src/test/Tests/Integration.hs

@@ -106,7 +106,7 @@ integrationTests = testGroup "Solidity Integration Testing"
       [ ("echidna_now passed",                     solved      "echidna_now") ]
   , testContract "basic/construct.sol"    Nothing
       [ ("echidna_construct passed",               solved      "echidna_construct") ]
-  , testContract "basic/gasprice.sol"     Nothing
+  , testContract "basic/gasprice.sol"     (Just "basic/gasprice.yaml")
       [ ("echidna_state passed",                   solved      "echidna_state") ]
   , let fp = "basic_multicontract/contracts/Foo.sol"; cfg = Just "basic_multicontract/echidna_config.yaml" in
       testCase fp $

stack.yaml

@@ -1,26 +1,23 @@
-resolver: lts-14.27
+resolver: lts-16.11
 
 packages:
 - '.'
 
 extra-deps:
 - git: https://github.com/dapphub/dapptools.git
-  commit: af84e2ee0a0654fdaa91186384233cf1731ee7ce
+  commit: 150dddc67b6cbad75fd4ae5a689452892f55ea26
   subdirs:
   - src/hevm
 
-- brick-0.46
 - ghci-pretty-0.0.2
-- multiset-0.3.4.1
+- HSH-2.1.3
+- monoidal-containers-0.6.0.1
 - restless-git-0.7
-- rosezipper-0.2
 - s-cargot-0.1.4.0
 - text-format-0.3.2
+- these-1.0.1
 - tree-view-0.5
-- HSH-2.1.3
-- ipprint-0.6
-- sr-extra-1.46.3.2
-- Unixutils-1.54.1
+- sbv-8.8
 - witherable-0.3.5
 - witherable-class-0
 - github: dmjio/semver-range