VMOpts: add option for freshAddresses initialization (#536)

* VMOpts: add option for freshAddresses initialization

* Changelog

* Update CHANGELOG.md

---------

Co-authored-by: Mate Soos @ Ethereum Foundation <[email protected]>

CHANGELOG.md

@@ -25,6 +25,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Symbolic ABI encoding for tuples, fuzzer for encoder
 - Printing `Addrs` when running `symbolic` for counterexamples and reachable end states
 - Improved symbolic execution tutorial
+- Add `freshAddresses` filed in `VMOpts` so that initial fresh address can be given as input
+- Add `freshAddresses` field in `VMOpts` so that initial fresh address can be given as input
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing

cli/cli.hs

@@ -496,6 +496,7 @@ vmFromCommand cmd = do
           , baseState      = EmptyBase
           , txAccessList   = mempty -- TODO: support me soon
           , allowFFI       = False
+          , freshAddresses = 0
           }
         word f def = fromMaybe def (f cmd)
         word64 f def = fromMaybe def (f cmd)
@@ -580,6 +581,7 @@ symvmFromCommand cmd calldata = do
       , baseState      = baseState
       , txAccessList   = mempty
       , allowFFI       = False
+      , freshAddresses = 0
       }
     word f def = fromMaybe def (f cmd)
     word64 f def = fromMaybe def (f cmd)

src/EVM.hs

@@ -157,7 +157,7 @@ makeVm o = do
     env = Env
       { chainId = o.chainId
       , contracts = Map.fromList ((o.address,o.contract):o.otherContracts)
-      , freshAddresses = 0
+      , freshAddresses = o.freshAddresses
       , freshGasVals = 0
       }
     block = Block

src/EVM/Exec.hs

@@ -41,6 +41,7 @@ vmForEthrunCreation creationCode =
     , create = False
     , txAccessList = mempty
     , allowFFI = False
+    , freshAddresses = 0
     }) <&> set (#env % #contracts % at (LitAddr ethrunAddress))
              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))
 

src/EVM/SymExec.hs

@@ -244,6 +244,7 @@ loadSymVM x callvalue cd create =
     , create = create
     , txAccessList = mempty
     , allowFFI = False
+    , freshAddresses = 0
     })
 
 -- | Interpreter which explores all paths at branching points. Returns an

src/EVM/Types.hs

@@ -940,6 +940,7 @@ data VMOpts (t :: VMType) = VMOpts
   , create :: Bool
   , txAccessList :: Map (Expr EAddr) [W256]
   , allowFFI :: Bool
+  , freshAddresses :: Int
   }
 
 deriving instance Show (VMOpts Symbolic)

src/EVM/UnitTest.hs

@@ -450,6 +450,7 @@ initialUnitTestVm (UnitTestOptions {..}) theContract = do
            , baseState = EmptyBase
            , txAccessList = mempty -- TODO: support unit test access lists???
            , allowFFI = ffiAllowed
+           , freshAddresses = 0
            }
   let creator =
         initialContract (RuntimeCode (ConcreteRuntimeCode ""))

test/EVM/Test/BlockchainTests.hs

@@ -414,6 +414,7 @@ fromBlockchainCase' block tx preState postState =
          , create         = isCreate
          , txAccessList   = Map.mapKeys LitAddr (txAccessMap tx)
          , allowFFI       = False
+         , freshAddresses = 0
          })
         checkState
         postState

test/EVM/Test/Tracing.hs

@@ -467,6 +467,7 @@ vmForRuntimeCode runtimecode calldata' evmToolEnv alloc txn fromAddr toAddress =
     , create = False
     , txAccessList = mempty
     , allowFFI = False
+    , freshAddresses = 0
     }) <&> set (#env % #contracts % at (LitAddr ethrunAddress))
              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode BS.empty))))
        <&> set (#state % #calldata) calldata'

test/rpc.hs

@@ -156,6 +156,7 @@ vmFromRpc blockNum calldata callvalue caller address = do
     , baseState      = EmptyBase
     , txAccessList   = mempty
     , allowFFI       = False
+    , freshAddresses = 0
     }) <&> set (#cache % #fetched % at address) (Just ctrct)
 
 testRpc :: Text