WIP

flake.nix

@@ -49,10 +49,10 @@
 
         hevm = pkgs.haskell.lib.dontCheck (
           pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
-            owner = "elopez";
+            owner = "ethereum";
             repo = "hevm";
-            rev = "release/0.51.3-plus-ghc-9.4-support";
-            sha256 = "sha256-gJMFYfsPqf5XZyyPDGJLqr9q9RpXkemGeUQUvFT6V0E";
+            rev = "release/0.52.0";
+            sha256 = "sha256-LCv3m6AbLr9mV7pHj7r08dzsg1UVpQDn0zyJXbzRS2Q=";
         }) { secp256k1 = pkgs.secp256k1; });
 
         # FIXME: figure out solc situation, it conflicts with the one from
@@ -141,6 +141,7 @@
             shellHook = "hpack";
             buildInputs = [
               solc
+              slither-analyzer
               haskellPackages.hlint
               haskellPackages.cabal-install
               haskellPackages.haskell-language-server

lib/Echidna.hs

@@ -27,6 +27,8 @@ import Echidna.Types.Signature
 import Echidna.Types.Solidity
 import Echidna.Types.Tx
 import Echidna.Types.World
+import Control.Monad.ST (RealWorld)
+import Echidna.Types.Buffer (forceLitAddr)
 
 -- | This function is used to prepare, process, compile and initialize smart contracts for testing.
 -- It takes:
@@ -45,7 +47,7 @@ prepareContract
   -> NonEmpty FilePath
   -> Maybe ContractName
   -> Seed
-  -> IO (VM, World, GenDict)
+  -> IO (VM RealWorld, World, GenDict)
 prepareContract env contracts solFiles specifiedContract seed = do
   let solConf = env.cfg.solConf
 
@@ -64,13 +66,13 @@ prepareContract env contracts solFiles specifiedContract seed = do
     echidnaTests = createTests solConf.testMode
                                solConf.testDestruction
                                testNames
-                               vm.state.contract
+                               (forceLitAddr vm.state.contract)
                                funs
 
     eventMap = Map.unions $ map (.eventMap) contracts
     world = mkWorld solConf eventMap signatureMap specifiedContract slitherInfo
 
-    deployedAddresses = Set.fromList $ AbiAddress <$> Map.keys vm.env.contracts
+    deployedAddresses = Set.fromList $ AbiAddress . forceLitAddr <$> Map.keys vm.env.contracts
     constants = enhanceConstants slitherInfo
                 <> timeConstants
                 <> extremeConstants
@@ -79,7 +81,7 @@ prepareContract env contracts solFiles specifiedContract seed = do
 
     dict = mkGenDict env.cfg.campaignConf.dictFreq
                      -- make sure we don't use cheat codes to form fuzzing call sequences
-                     (Set.delete (AbiAddress cheatCode) constants)
+                     (Set.delete (AbiAddress $ forceLitAddr cheatCode) constants)
                      Set.empty
                      seed
                      (returnTypes contracts)

lib/Echidna/Campaign.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
 
 module Echidna.Campaign where
 
@@ -18,7 +19,7 @@ import Data.ByteString.Lazy qualified as LBS
 import Data.IORef (readIORef, writeIORef, atomicModifyIORef')
 import Data.Map qualified as Map
 import Data.Map (Map, (\\))
-import Data.Maybe (isJust, mapMaybe, fromMaybe)
+import Data.Maybe (isJust, mapMaybe, fromMaybe, fromJust)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text)
@@ -36,7 +37,7 @@ import Echidna.Shrink (shrinkTest)
 import Echidna.Test
 import Echidna.Transaction
 import Echidna.Types (Gas)
-import Echidna.Types.Buffer (forceBuf)
+import Echidna.Types.Buffer (forceBuf, forceLitAddr)
 import Echidna.Types.Campaign
 import Echidna.Types.Corpus (Corpus, corpusSize)
 import Echidna.Types.Coverage (scoveragePoints)
@@ -47,6 +48,7 @@ import Echidna.Types.Test qualified as Test
 import Echidna.Types.Tx (TxCall(..), Tx(..), call)
 import Echidna.Types.World (World)
 import Echidna.Utility (getTimestamp)
+import Control.Monad.ST (RealWorld)
 
 instance MonadThrow m => MonadThrow (RandT g m) where
   throwM = lift . throwM
@@ -62,7 +64,7 @@ isSuccessful =
 -- contain minized corpus without sequences that didn't increase the coverage.
 replayCorpus
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM     -- ^ VM to start replaying from
+  => VM RealWorld -- ^ VM to start replaying from
   -> [[Tx]] -- ^ corpus to replay
   -> m ()
 replayCorpus vm txSeqs =
@@ -77,7 +79,7 @@ runWorker
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m)
   => StateT WorkerState m ()
   -- ^ Callback to run after each state update (for instrumentation)
-  -> VM      -- ^ Initial VM state
+  -> VM RealWorld -- ^ Initial VM state
   -> World   -- ^ Initial world state
   -> GenDict -- ^ Generation dictionary
   -> Int     -- ^ Worker id starting from 0
@@ -88,7 +90,8 @@ runWorker callback vm world dict workerId initialCorpus testLimit = do
   metaCacheRef <- asks (.metadataCache)
   fetchContractCacheRef <- asks (.fetchContractCache)
   external <- liftIO $ Map.mapMaybe id <$> readIORef fetchContractCacheRef
-  liftIO $ writeIORef metaCacheRef (mkMemo (vm.env.contracts <> external))
+  let concretizeKeys = Map.foldrWithKey (Map.insert . forceLitAddr) mempty
+  liftIO $ writeIORef metaCacheRef (mkMemo (concretizeKeys vm.env.contracts <> external))
 
   let
     effectiveSeed = dict.defSeed + workerId
@@ -150,13 +153,13 @@ runWorker callback vm world dict workerId initialCorpus testLimit = do
 
   continue = runUpdate (shrinkTest vm) >> lift callback >> run
 
-  mkMemo = makeBytecodeCache . map (forceBuf . (^. bytecode)) . Map.elems
+  mkMemo = makeBytecodeCache . map (forceBuf . fromJust . (^. bytecode)) . Map.elems
 
 -- | Generate a new sequences of transactions, either using the corpus or with
 -- randomly created transactions
 randseq
   :: (MonadRandom m, MonadReader Env m, MonadState WorkerState m, MonadIO m)
-  => Map Addr Contract
+  => Map (Expr 'EAddr) Contract
   -> World
   -> m [Tx]
 randseq deployedContracts world = do
@@ -187,9 +190,9 @@ randseq deployedContracts world = do
 -- minimized. Stores any useful data in the campaign state if coverage increased.
 callseq
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM
+  => VM RealWorld
   -> [Tx]
-  -> m VM
+  -> m (VM RealWorld)
 callseq vm txSeq = do
   env <- ask
   -- First, we figure out whether we need to execute with or without coverage
@@ -224,7 +227,7 @@ callseq vm txSeq = do
       -- compute the addresses not present in the old VM via set difference
       newAddrs = Map.keys $ vm'.env.contracts \\ vm.env.contracts
       -- and construct a set to union to the constants table
-      diffs = Map.fromList [(AbiAddressType, Set.fromList $ AbiAddress <$> newAddrs)]
+      diffs = Map.fromList [(AbiAddressType, Set.fromList $ AbiAddress . forceLitAddr <$> newAddrs)]
       -- Now we try to parse the return values as solidity constants, and add them to 'GenDict'
       resultMap = returnValues (map (\(t, (vr, _)) -> (t, vr)) results) workerState.genDict.rTypes
       -- union the return results with the new addresses
@@ -257,7 +260,7 @@ callseq vm txSeq = do
   -- know the return type for each function called. If yes, tries to parse the
   -- return value as a value of that type. Returns a 'GenDict' style Map.
   returnValues
-    :: [(Tx, VMResult)]
+    :: [(Tx, VMResult RealWorld)]
     -> (FunctionName -> Maybe AbiType)
     -> Map AbiType (Set AbiValue)
   returnValues txResults returnTypeOf =
@@ -270,13 +273,13 @@ callseq vm txSeq = do
           type' <- returnTypeOf fname
           case runGetOrFail (getAbi type') (LBS.fromStrict buf) of
             -- make sure we don't use cheat codes to form fuzzing call sequences
-            Right (_, _, abiValue) | abiValue /= AbiAddress cheatCode ->
+            Right (_, _, abiValue) | abiValue /= AbiAddress (forceLitAddr cheatCode) ->
               Just (type', Set.singleton abiValue)
             _ -> Nothing
         _ -> Nothing
 
   -- | Add transactions to the corpus discarding reverted ones
-  addToCorpus :: Int -> [(Tx, (VMResult, Gas))] -> Corpus -> Corpus
+  addToCorpus :: Int -> [(Tx, (VMResult RealWorld, Gas))] -> Corpus -> Corpus
   addToCorpus n res corpus =
     if null rtxs then corpus else Set.insert (n, rtxs) corpus
     where rtxs = fst <$> res
@@ -285,8 +288,8 @@ callseq vm txSeq = do
 -- executed, saving the transaction if it finds new coverage.
 execTxOptC
   :: (MonadIO m, MonadReader Env m, MonadState WorkerState m, MonadThrow m)
-  => VM -> Tx
-  -> m ((VMResult, Gas), VM)
+  => VM RealWorld -> Tx
+  -> m ((VMResult RealWorld, Gas), VM RealWorld)
 execTxOptC vm tx = do
   ((res, grew), vm') <- runStateT (execTxWithCov tx) vm
   when grew $ do
@@ -301,7 +304,7 @@ execTxOptC vm tx = do
 -- | Given current `gasInfo` and a sequence of executed transactions, updates
 -- information on highest gas usage for each call
 updateGasInfo
-  :: [(Tx, (VMResult, Gas))]
+  :: [(Tx, (VMResult RealWorld, Gas))]
   -> [Tx]
   -> Map Text (Gas, [Tx])
   -> Map Text (Gas, [Tx])
@@ -322,10 +325,10 @@ updateGasInfo ((t, _):ts) tseq gi = updateGasInfo ts (t:tseq) gi
 -- known solves.
 evalSeq
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM -- ^ Initial VM
-  -> (VM -> Tx -> m (result, VM))
+  => VM RealWorld -- ^ Initial VM
+  -> (VM RealWorld -> Tx -> m (result, VM RealWorld))
   -> [Tx]
-  -> m ([(Tx, result)], VM)
+  -> m ([(Tx, result)], VM RealWorld)
 evalSeq vm0 execFunc = go vm0 [] where
   go vm executedSoFar toExecute = do
     -- NOTE: we do reverse here because we build up this list by prepending,
@@ -365,8 +368,8 @@ runUpdate f = do
 -- Then update accordingly, keeping track of how many times we've tried to solve or shrink.
 updateTest
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
-  => VM
-  -> (VM, [Tx])
+  => VM RealWorld
+  -> (VM RealWorld, [Tx])
   -> EchidnaTest
   -> m (Maybe EchidnaTest)
 updateTest vmForShrink (vm, xs) test = do

lib/Echidna/Deploy.hs

@@ -19,21 +19,22 @@ import Echidna.Events (extractEvents)
 import Echidna.Types.Config (Env(..))
 import Echidna.Types.Solidity (SolException(..))
 import Echidna.Types.Tx (createTx, unlimitedGasPerBlock)
+import Control.Monad.ST (RealWorld)
 
 deployContracts
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, SolcContract)]
   -> Addr
-  -> VM
-  -> m VM
+  -> VM RealWorld
+  -> m (VM RealWorld)
 deployContracts cs = deployBytecodes' $ map (\(a, c) -> (a, c.creationCode)) cs
 
 deployBytecodes
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, Text)]
   -> Addr
-  -> VM
-  -> m VM
+  -> VM RealWorld
+  -> m (VM RealWorld)
 deployBytecodes cs = deployBytecodes' $
   (\(a, bc) ->
     (a, fromRight (error ("invalid b16 decoding of: " ++ show bc)) $ BS16.decode $ encodeUtf8 bc)
@@ -44,8 +45,8 @@ deployBytecodes'
   :: (MonadIO m, MonadReader Env m, MonadThrow m)
   => [(Addr, ByteString)]
   -> Addr
-  -> VM
-  -> m VM
+  -> VM RealWorld
+  -> m (VM RealWorld)
 deployBytecodes' cs src initialVM = foldM deployOne initialVM cs
   where
   deployOne vm (dst, bytecode) = do

lib/Echidna/Etheno.hs

@@ -11,7 +11,7 @@ import Control.Exception (Exception)
 import Control.Monad (void)
 import Control.Monad.Catch (MonadThrow, throwM)
 import Control.Monad.Fail qualified as M (MonadFail(..))
-import Control.Monad.State.Strict (MonadState, get, put, execStateT, gets, modify', execState)
+import Control.Monad.State.Strict (MonadIO, MonadState, get, gets, put, execStateT)
 import Data.Aeson (FromJSON(..), (.:), withObject, eitherDecodeFileStrict)
 import Data.ByteString.Base16 qualified as BS16 (decode)
 import Data.ByteString.Char8 (ByteString)
@@ -35,6 +35,7 @@ import Echidna.ABI (encodeSig)
 import Echidna.Types (fromEVM)
 import Echidna.Types.Tx (TxCall(..), Tx(..), makeSingleTx, createTxWithValue, unlimitedGasPerBlock)
 import Data.Set (Set)
+import Control.Monad.ST (RealWorld, stToIO)
 
 -- | During initialization we can either call a function or create an account or contract
 data Etheno
@@ -120,38 +121,39 @@ matchSignatureAndCreateTx _ _ = []
 
 -- | Main function: takes a filepath where the initialization sequence lives and returns
 -- | the initialized VM along with a list of Addr's to put in GenConf
-loadEthenoBatch :: Bool -> FilePath -> IO VM
+loadEthenoBatch :: Bool -> FilePath -> IO (VM RealWorld)
 loadEthenoBatch ffi fp = do
   bs <- eitherDecodeFileStrict fp
   case bs of
     Left e -> throwM $ EthenoException e
     Right (ethenoInit :: [Etheno]) -> do
       -- Execute contract creations and initial transactions,
       let initVM = mapM execEthenoTxs ethenoInit
-      execStateT initVM (initialVM ffi)
+      vm <- stToIO $ initialVM ffi
+      execStateT initVM vm
 
-initAddress :: MonadState VM m => Addr -> m ()
+initAddress :: MonadState (VM s) m => Addr -> m ()
 initAddress addr = do
   cs <- gets (.env.contracts)
-  if addr `member` cs then pure ()
-  else #env % #contracts % at addr .= Just account
+  if LitAddr addr `member` cs then pure ()
+  else #env % #contracts % at (LitAddr addr) .= Just account
   where
     account =
       initialContract (RuntimeCode (ConcreteRuntimeCode mempty))
-        & set #nonce 0
-        & set #balance 100000000000000000000 -- default balance for EOAs in etheno
+        & set #nonce (Just 0)
+        & set #balance (Lit 100000000000000000000) -- default balance for EOAs in etheno
 
 crashWithQueryError
-  :: (MonadState VM m, MonadFail m, MonadThrow m)
-  => Query
+  :: (MonadState (VM s) m, MonadFail m, MonadThrow m)
+  => Query s
   -> Etheno
   -> m ()
 crashWithQueryError q et =
   case (q, et) of
-    (PleaseFetchContract addr _, FunctionCall f t _ _ _ _) ->
+    (PleaseFetchContract addr _ _, FunctionCall f t _ _ _ _) ->
       error $ "Address " ++ show addr ++ " was used during function call from "
                 ++ show f ++ " to " ++ show t ++ " but it was never defined as EOA or deployed as a contract"
-    (PleaseFetchContract addr _, ContractCreated f t _ _ _ _) ->
+    (PleaseFetchContract addr _ _, ContractCreated f t _ _ _ _) ->
       error $ "Address " ++ show addr ++ " was used during the contract creation of "
                 ++ show t ++ " from " ++ show f ++ " but it was never defined as EOA or deployed as a contract"
     (PleaseFetchSlot slot _ _, FunctionCall f t _ _ _ _) ->
@@ -164,7 +166,7 @@ crashWithQueryError q et =
 
 -- | Takes a list of Etheno transactions and loads them into the VM, returning the
 -- | address containing echidna tests
-execEthenoTxs :: (MonadState VM m, MonadFail m, MonadThrow m) => Etheno -> m ()
+execEthenoTxs :: (MonadIO m, MonadState (VM RealWorld) m, MonadFail m, MonadThrow m) => Etheno -> m ()
 execEthenoTxs et = do
   setupEthenoTx et
   vm <- get
@@ -179,20 +181,20 @@ execEthenoTxs et = do
         -- NOTE: this is not a real SMT query, we know it is concrete and can
         -- resume right away. It is done this way to support iterations counting
         -- in hevm.
-        modify' $ execState (continue (Case (c > 0)))
+        fromEVM (continue (Case (c > 0)))
         runFully vm
       (HandleEffect (Query q), _)    -> crashWithQueryError q et
       (VMFailure x, _)               -> vmExcept x >> M.fail "impossible"
       (VMSuccess (ConcreteBuf bc),
        ContractCreated _ ca _ _ _ _) -> do
-        #env % #contracts % at ca % _Just % #contractcode .= InitCode mempty mempty
+        #env % #contracts % at (LitAddr ca) % _Just % #code .= InitCode mempty mempty
         fromEVM $ do
           replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bc))
-          loadContract ca
+          -- loadContract ca
       _ -> pure ()
 
 -- | For an etheno txn, set up VM to execute txn
-setupEthenoTx :: MonadState VM m => Etheno -> m ()
+setupEthenoTx :: (MonadIO m, MonadState (VM RealWorld) m) => Etheno -> m ()
 setupEthenoTx (AccountCreated f) =
   initAddress f -- TODO: improve etheno to include initial balance
 setupEthenoTx (ContractCreated f c _ _ d v) =

lib/Echidna/Events.hs

@@ -29,7 +29,7 @@ type Events = [Text]
 emptyEvents :: TreePos Empty a
 emptyEvents = fromForest []
 
-extractEvents :: Bool -> DappInfo -> VM -> Events
+extractEvents :: Bool -> DappInfo -> VM s -> Events
 extractEvents decodeErrors dappInfo vm =
   let forest = traceForest vm
   in maybeToList (decodeRevert decodeErrors vm)
@@ -76,7 +76,7 @@ maybeContractNameFromCodeHash info codeHash = contractToName <$> maybeContract
   where maybeContract = snd <$> Map.lookup codeHash info.solcByHash
         contractToName c = contractNamePart c.contractName
 
-decodeRevert :: Bool -> VM -> Maybe Text
+decodeRevert :: Bool -> VM s -> Maybe Text
 decodeRevert decodeErrors vm =
   case vm.result of
     Just (VMFailure (Revert (ConcreteBuf bs))) -> decodeRevertMsg decodeErrors bs