content: -- Main file of the hevm CLI program
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE OverloadedStrings #-}
  
  module Main where
  
  import Control.Monad (when, forM_, unless)
  import Control.Monad.State.Strict (runStateT)
  import Control.Monad.ST (RealWorld, stToIO)
  import Control.Monad.IO.Unlift
  import Control.Exception (try, IOException)
  import Data.ByteString (ByteString)
  import qualified Data.ByteString.Lazy as BS
  import Data.ByteString.Builder (toLazyByteString)
  import qualified Data.ByteString.Char8 as BC
  import Data.DoubleWord (Word256)
  import Data.List (intersperse, intercalate)
  import Data.Maybe (fromMaybe, mapMaybe, fromJust, isNothing, isJust)
  import Data.Text qualified as T
  import Data.Text.IO qualified as T
  import Data.Version (showVersion)
  import Data.Word (Word64)
  import GHC.Conc (getNumProcessors)
  import Numeric.Natural (Natural)
  import Optics.Core ((&), set)
  import Witch (unsafeInto)
  import Options.Generic as OptionsGeneric
  import Options.Applicative as Options
  import Paths_hevm qualified as Paths
  import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist, makeAbsolute)
  import System.FilePath ((</>))
  import System.Exit (exitFailure, exitWith, ExitCode(..))
  import Data.List.Split (splitOn)
  import Text.Read (readMaybe)
  import JSONL (jsonlBuilder, jsonLine)
  
  import EVM (initialContract, abstractContract, makeVm)
  import EVM.ABI (Sig(..))
  import EVM.Dapp (dappInfo, DappInfo, emptyDapp)
  import EVM.Expr qualified as Expr
  import EVM.Concrete qualified as Concrete
  import GitHash
  import EVM.FeeSchedule (feeSchedule)
  import EVM.Fetch qualified as Fetch
  import EVM.Format (hexByteString, strip0x, formatExpr)
  import EVM.Solidity
  import EVM.Solvers
  import EVM.Stepper qualified
  import EVM.SymExec
  import EVM.Transaction qualified
  import EVM.Types hiding (word, Env, Symbolic)
  import EVM.Types qualified
  import EVM.UnitTest
  import EVM.Effects
  import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
  import EVM.Tracing (interpretWithTrace, VMTraceStepResult(..))
  
  data AssertionType = DSTest | Forge
    deriving (Eq, Show, Read)
  
  projectTypeParser :: Parser ProjectType
  projectTypeParser = option auto (long "project-type" <> showDefault <> value Foundry <> help "Is this a CombinedJSON or Foundry project")
  
  sigParser :: Parser (Maybe Text)
  sigParser = (optional $ strOption $ long "sig" <> help "Signature of types to decode/encode")
  
  argParser :: Parser [String]
  argParser = (many $ strOption $ long "arg" <> help "Value(s) to encode. Can be given multiple times, once for each argument")
  
  createParser :: Parser Bool
  createParser = switch $ long "create" <> help "Tx: creation"
  
  rpcParser :: Parser (Maybe URL)
  rpcParser = (optional $ strOption $ long "rpc" <> help "Fetch state from a remote node")
  
  data CommonOptions = CommonOptions
    { askSmtIterations ::Integer
    , loopDetectionHeuristic ::LoopHeuristic
    , noDecompose   ::Bool
    , solver        ::Text
    , debug         ::Bool
    , calldata      ::Maybe ByteString
    , trace         ::Bool
    , verb          ::Int
    , root          ::Maybe String
    , assertionType ::AssertionType
    , solverThreads ::Natural
    , smttimeout    ::Natural
    , smtdebug      ::Bool
    , dumpUnsolved  ::Maybe String
    , numSolvers    ::Maybe Natural
    , maxIterations ::Integer
    , promiseNoReent::Bool
    , maxBufSize    ::Int
    , maxWidth      ::Int
    , maxDepth      ::Maybe Int
    , noSimplify    ::Bool
    , onlyDeployed  ::Bool
    }
  
  commonOptions :: Parser CommonOptions
  commonOptions = CommonOptions
    <$> option auto ( long "ask-smt-iterations" <> value 1 <>
      help "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability")
    <*> option auto (long "loop-detection-heuristic" <> showDefault <> value StackBased <>
      help "Which heuristic should be used to determine if we are in a loop: StackBased or Naive")
    <*> (switch $ long "no-decompose"         <> help "Don't decompose storage slots into separate arrays")
    <*> (strOption $ long "solver"            <> value "z3" <> help "Used SMT solver: z3, cvc5, or bitwuzla")
    <*> (switch $ long "debug"                <> help "Debug printing of internal behaviour, and dump internal expressions")
    <*> (optional $ strOption $ long "calldata" <> help "Tx: calldata")
    <*> (switch $ long "trace"                <> help "Dump trace")
    <*> (option auto $ long "verb"            <> showDefault <> value 1 <> help "Append call trace: {1} failures {2} all")
    <*> (optional $ strOption $ long "root"   <> help "Path to  project root directory")
    <*> (option auto $ long "assertion-type"  <> showDefault <> value Forge <> help "Assertions as per Forge or DSTest")
    <*> (option auto $ long "solver-threads"  <> showDefault <> value 1 <> help "Number of threads for each solver instance. Only respected for Z3")
    <*> (option auto $ long "smttimeout"      <> value 300 <> help "Timeout given to SMT solver in seconds")
    <*> (switch $ long "smtdebug"             <> help "Print smt queries sent to the solver")
    <*> (optional $ strOption $ long "dump-unsolved" <> help "Dump unsolved SMT queries to this (relative) path")
    <*> (optional $ option auto $ long "num-solvers" <> help "Number of solver instances to use (default: number of cpu cores)")
    <*> (option auto $ long "max-iterations"  <> showDefault <> value 5 <> help "Number of times we may revisit a particular branching point. For no bound, set -1")
    <*> (switch $ long "promise-no-reent"     <> help "Promise no reentrancy is possible into the contract(s) being examined")
    <*> (option auto $ long "max-buf-size"    <> value 64 <> help "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)")
    <*> (option auto $ long "max-width"      <> showDefault <> value 100 <> help "Max number of concrete values to explore when encountering a symbolic value. This is a form of branch width limitation per symbolic value")
    <*> (optional $ option auto $ long "max-depth" <> help "Limit maximum depth of branching during exploration (default: unlimited)")
    <*> (switch $ long "no-simplify" <> help "Don't perform simplification of expressions")
    <*> (switch $ long "only-deployed" <> help "When trying to resolve unknown addresses, only use addresses of deployed contracts")
  
  data CommonExecOptions = CommonExecOptions
    { address       ::Maybe Addr
    , caller        ::Maybe Addr
    , origin        ::Maybe Addr
    , coinbase      ::Maybe Addr
    , value         ::Maybe W256
    , nonce         ::Maybe Word64
    , gas           ::Maybe Word64
    , number        ::Maybe W256
    , timestamp     ::Maybe W256
    , basefee       ::Maybe W256
    , priorityFee   ::Maybe W256
    , gaslimit      ::Maybe Word64
    , gasprice      ::Maybe W256
    , maxcodesize   ::Maybe W256
    , prevRandao    ::Maybe W256
    , chainid       ::Maybe W256
    , rpc           ::Maybe URL
    , block         ::Maybe W256
  }
  
  commonExecOptions :: Parser CommonExecOptions
  commonExecOptions = CommonExecOptions
    <$> (optional $ option auto $ long "address"       <> help "Tx: address")
    <*> (optional $ option auto $ long "caller"        <> help "Tx: caller")
    <*> (optional $ option auto $ long "origin"        <> help "Tx: origin")
    <*> (optional $ option auto $ long "coinbase"      <> help "Block: coinbase")
    <*> (optional $ option auto $ long "value"         <> help "Tx: Eth amount")
    <*> (optional $ option auto $ long "nonce"         <> help "Nonce of origin")
    <*> (optional $ option auto $ long "gas"           <> help "Tx: gas amount")
    <*> (optional $ option auto $ long "number"        <> help "Block: number")
    <*> (optional $ option auto $ long "timestamp"     <> help "Block: timestamp")
    <*> (optional $ option auto $ long "basefee"       <> help "Block: base fee")
    <*> (optional $ option auto $ long "priority-fee"  <> help "Tx: priority fee")
    <*> (optional $ option auto $ long "gaslimit"      <> help "Tx: gas limit")
    <*> (optional $ option auto $ long "gasprice"      <> help "Tx: gas price")
    <*> (optional $ option auto $ long "maxcodesize"   <> help "Block: max code size")
    <*> (optional $ option auto $ long "prev-randao"   <> help "Block: prevRandao")
    <*> (optional $ option auto $ long "chainid"       <> help "Env: chainId")
    <*> rpcParser
    <*> (optional $ option auto $ long "block"         <> help "Block state is be fetched from")
  
  data CommonFileOptions = CommonFileOptions
   { code        ::Maybe ByteString
   , codeFile    ::Maybe String
   }
  
  commonFileOptions :: Parser CommonFileOptions
  commonFileOptions = CommonFileOptions
    <$> (optional $ strOption $ long "code" <> help "Program bytecode")
    <*> (optional $ strOption $ long "code-file" <> help "Program bytecode in a file")
  
  data TestOptions = TestOptions
    { projectType   ::ProjectType
    , rpc           ::Maybe URL
    , number        ::Maybe W256
    , coverage      ::Bool
    , match         ::Maybe String
    , prefix        ::String
    , ffi           ::Bool
    , mockFile      ::Maybe String
    }
  
  testOptions :: Parser TestOptions
  testOptions = TestOptions
    <$> projectTypeParser
    <*> rpcParser
    <*> (optional $ option auto $ long "number" <> help "Block: number")
    <*> (switch $ long "coverage" <> help "Coverage analysis")
    <*> (optional $ strOption $ long "match" <> help "Test case filter - only run methods matching regex")
    <*> (strOption $ long "prefix"  <> showDefault <> value "prove" <> help "Prefix for test cases to prove")
    <*> (switch $ long "ffi" <> help "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)")
    <*> (optional $ strOption $ long "mock-file" <> help "Read mocked RPC response data from JSON file")
  
  
  data EqOptions = EqOptions
    { codeA         ::Maybe ByteString
    , codeB         ::Maybe ByteString
    , codeAFile     ::Maybe String
    , codeBFile     ::Maybe String
    , sig           ::Maybe Text
    , arg           ::[String]
    , create        ::Bool
    }
  
  eqOptions :: Parser EqOptions
  eqOptions = EqOptions
    <$> (optional $ strOption $ long "code-a"      <> help "Bytecode of the first program")
    <*> (optional $ strOption $ long "code-b"      <> help "Bytecode of the second program")
    <*> (optional $ strOption $ long "code-a-file" <> help "First program's bytecode in a file")
    <*> (optional $ strOption $ long "code-b-file" <> help "Second program's bytecode in a file")
    <*> sigParser
    <*> argParser
    <*> createParser
  
  data SymbolicOptions = SymbolicOptions
    { projectType       ::ProjectType
    , initialStorage    ::Maybe InitialStorage
    , getModels         ::Bool
    , showTree          ::Bool
    , showReachableTree ::Bool
    , assertions        ::Maybe String
    , sig               ::Maybe Text
    , arg               ::[String]
    , create            ::Bool
    }
  
  symbolicOptions :: Parser SymbolicOptions
  symbolicOptions = SymbolicOptions
    <$> projectTypeParser
    <*> (optional $ option auto $ long "initial-storage" <> help "Starting state for storage: Empty, Abstract (default Abstract)")
    <*> (switch $ long "get-models" <> help "Print example testcase for each execution path")
    <*> (switch $ long "show-tree" <> help "Print branches explored in tree view")
    <*> (switch $ long "show-reachable-tree" <> showDefault <> help "Print only reachable branches explored in tree view")
    <*> (optional $ strOption $ long "assertions" <> help "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)")
    <*> sigParser
    <*> argParser
    <*> createParser
  
  data ExecOptions = ExecOptions
    { projectType :: ProjectType
    , create :: Bool
    , jsonTrace :: Bool
    }
  execOptions :: Parser ExecOptions
  execOptions = ExecOptions
    <$> projectTypeParser
    <*> createParser
    <*> (switch $ long "json-trace" <> help "Output a geth compatible json trace")
  
  -- Combined options data type
  data Command
    = Symbolic   CommonFileOptions SymbolicOptions CommonExecOptions CommonOptions
    | Equal      EqOptions CommonOptions
    | Test       TestOptions  CommonOptions
    | Exec       CommonFileOptions ExecOptions CommonExecOptions CommonOptions
    | Version
  
  -- Parser for the subcommands
  commandParser :: Parser Command
  commandParser = subparser
    ( command "test"
        (info (Test <$> testOptions <*> commonOptions <**> helper)
          (progDesc "Prove Foundry unit tests prefixed with `prove` by default"
          <> footer "For more help: https://hevm.dev/std-test-tutorial.html" ))
    <> command "equivalence"
        (info (Equal <$> eqOptions <*> commonOptions <**> helper)
          (progDesc "Prove equivalence between two programs"
          <> footer "For more help: https://hevm.dev/equivalence-checking-tutorial.html" ))
    <> command "symbolic"
        (info (Symbolic <$> commonFileOptions <*> symbolicOptions <*> commonExecOptions <*> commonOptions <**> helper)
          (progDesc "Symbolically explore an abstract program"
          <> footer "For more help, see: https://hevm.dev/symbolic-execution-tutorial.html" ))
    <> command "exec"
        (info (Exec <$> commonFileOptions <*> execOptions <*> commonExecOptions <*> commonOptions <**> helper)
          (progDesc "Concretely execute a given program"
          <> footer "For more help, see https://hevm.dev/exec.html" ))
    <> command "version"
        (info (pure Version)
          (progDesc "Show the version of the tool"))
    )
  
  type URL = Text
  
  deriving instance OptionsGeneric.ParseField Word256
  deriving instance OptionsGeneric.ParseField [Word256]
  
  data InitialStorage
    = Empty
    | Abstract
    deriving (Show, Read, OptionsGeneric.ParseField)
  
  getFullVersion :: [Char]
  getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"
    where
      gitInfo = $$tGitInfoCwdTry
      gitVersion = case gitInfo of
        Right val -> "git rev " <> giBranch val <>  "@" <> giHash val
        Left _ -> "no git revision present"
  
  main :: IO ()
  main = do
    cmd <- execParser $ info (commandParser <**> helper)
      ( Options.fullDesc
      <> progDesc "hevm, a symbolic and concrete EVM bytecode execution framework"
      <> footer "See https://hevm.dev for more information"
      )
  
    case cmd of
      Symbolic cFileOpts symbOpts cExecOpts cOpts -> do
        env <- makeEnv cOpts
        root <- getRoot cOpts
        withCurrentDirectory root $ runEnv env $ symbCheck cFileOpts symbOpts cExecOpts cOpts
      Equal eqOpts cOpts -> do
        env <- makeEnv cOpts
        runEnv env $ equivalence eqOpts cOpts
      Test testOpts cOpts -> do
        env <- makeEnv cOpts
        root <- getRoot cOpts
        solver <- getSolver cOpts.solver
        cores <- liftIO $ unsafeInto <$> getNumProcessors
        let solverCount = fromMaybe cores cOpts.numSolvers
        runEnv env $ withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do
          buildOut <- readBuildOutput root testOpts.projectType
          case buildOut of
            Left e -> liftIO $ do
              putStrLn $ "Error: " <> e
              exitFailure
            Right out -> do
              -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?
              unitTestOpts <- unitTestOptions testOpts cOpts solvers (Just out)
              res <- unitTest unitTestOpts out
              liftIO $ unless (uncurry (&&) res) exitFailure
      Exec cFileOpts execOpts cExecOpts cOpts-> do
        env <- makeEnv cOpts
        runEnv env $ launchExec cFileOpts execOpts cExecOpts cOpts
      Version {} ->putStrLn getFullVersion
    where
      makeEnv :: CommonOptions -> IO Env
      makeEnv cOpts = do
        when (cOpts.maxBufSize > 64) $ do
          putStrLn "Error: maxBufSize must be less than or equal to 64. That limits buffers to a size of 2^64, which is more than enough for practical purposes"
          exitFailure
        when (cOpts.maxBufSize < 0) $ do
          putStrLn "Error: maxBufSize must be at least 0. Negative values do not make sense. A value of zero means at most 1 byte long buffers"
          exitFailure
        pure Env { config = defaultConfig
          { dumpQueries = cOpts.smtdebug
          , dumpUnsolved = cOpts.dumpUnsolved
          , debug = cOpts.debug
          , dumpEndStates = cOpts.debug
          , dumpExprs = cOpts.debug
          , dumpTrace = cOpts.trace
          , decomposeStorage = Prelude.not cOpts.noDecompose
          , promiseNoReent = cOpts.promiseNoReent
          , maxBufSize = cOpts.maxBufSize
          , maxWidth = cOpts.maxWidth
          , maxDepth = cOpts.maxDepth
          , verb = cOpts.verb
          , simp = Prelude.not cOpts.noSimplify
          , onlyDeployed = cOpts.onlyDeployed
          } }
  
  
  getCode :: App m => Maybe String -> Maybe ByteString -> m (Maybe ByteString)
  getCode fname code = liftIO $ do
    when (isJust fname && isJust code) $ do
      putStrLn "Error: Cannot provide both a file and code"
      exitFailure
    case fname of
      Nothing -> pure $ fmap strip code
      Just f -> do
        result <- try (BS.readFile f) :: IO (Either IOException BS.ByteString)
        case result of
          Left e -> do
            putStrLn $ "Error reading file: " <> show e
            exitFailure
          Right content -> do
            pure $ Just $ strip (BS.toStrict content)
    where
      strip = BC.filter (\c -> c /= ' ' && c /= '\n' && c /= '\r' && c /= '\t' && c /= '"')
  
  equivalence :: App m => EqOptions -> CommonOptions -> m ()
  equivalence eqOpts cOpts = do
    bytecodeA' <- getCode eqOpts.codeAFile eqOpts.codeA
    bytecodeB' <- getCode eqOpts.codeBFile eqOpts.codeB
    let bytecodeA = decipher bytecodeA'
    let bytecodeB = decipher bytecodeB'
    when (isNothing bytecodeA) $ liftIO $ do
      putStrLn "Error: invalid or no bytecode for program A. Provide a valid one with --code-a or --code-a-file"
      exitFailure
    when (isNothing bytecodeB) $ liftIO $ do
      putStrLn "Error: invalid or no bytecode for program B. Provide a valid one with --code-b or --code-b-file"
      exitFailure
    let veriOpts = VeriOpts { iterConf = IterConfig {
                              maxIter = parseMaxIters cOpts.maxIterations
                              , askSmtIters = cOpts.askSmtIterations
                              , loopHeuristic = cOpts.loopDetectionHeuristic
                              }
                            , rpcInfo = mempty
                            }
    calldata <- buildCalldata cOpts eqOpts.sig eqOpts.arg
    solver <- liftIO $ getSolver cOpts.solver
    cores <- liftIO $ unsafeInto <$> getNumProcessors
    let solverCount = fromMaybe cores cOpts.numSolvers
    withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \s -> do
      eq <- equivalenceCheck s (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata eqOpts.create
      let anyIssues =  not (null eq.partials) || any (isUnknown . fst) eq.res  || any (isError . fst) eq.res
      liftIO $ case (any (isCex . fst) eq.res, anyIssues) of
        (False, False) -> putStrLn "   \x1b[32m[PASS]\x1b[0m Contracts behave equivalently"
        (True, _)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts do not behave equivalently"
        (_, True)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts may not behave equivalently"
      liftIO $ printWarnings Nothing eq.partials (map fst eq.res) "the contracts under test"
      case any (isCex . fst) eq.res of
        False -> liftIO $ do
          when anyIssues exitFailure
          putStrLn "No discrepancies found"
        True -> liftIO $ do
          let cexes = mapMaybe getCexP eq.res
          T.putStrLn . T.unlines $
            [ "Not equivalent. The following inputs result in differing behaviours:"
            , "" , "-----", ""
            ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap formatCexes cexes)
          exitFailure
    where
      decipher = maybe Nothing (hexByteString . strip0x)
      getCexP :: (ProofResult a b, String) -> Maybe (a, String)
      getCexP (Cex c, reason) = Just (c, reason)
      getCexP _ = Nothing
      formatCexes (cex, reason) = formatCex (AbstractBuf "txdata") Nothing cex <> "Difference: " <> T.pack reason
  
  getSolver :: Text -> IO Solver
  getSolver s = case T.unpack s of
    "z3" -> pure Z3
    "cvc5" -> pure CVC5
    "bitwuzla" -> pure Bitwuzla
    "empty" -> pure EmptySolver
    input -> do
      putStrLn $ "unrecognised solver: " <> input
      exitFailure
  
  getSrcInfo :: App m => ExecOptions -> CommonOptions -> m DappInfo
  getSrcInfo execOpts cOpts = do
    root <- liftIO $ getRoot cOpts
    conf <- readConfig
    liftIO $ withCurrentDirectory root $ do
      outExists <- doesDirectoryExist (root System.FilePath.</> "out")
      if outExists
      then do
        buildOutput <- runEnv Env {config = conf} $ readBuildOutput root execOpts.projectType
        case buildOutput of
          Left _ -> pure emptyDapp
          Right o -> pure $ dappInfo root o
      else pure emptyDapp
  
  getRoot :: CommonOptions -> IO FilePath
  getRoot cmd = maybe getCurrentDirectory makeAbsolute cmd.root
  
  parseMaxIters :: Integer -> Maybe Integer
  parseMaxIters num = if num < 0 then Nothing else Just num
  
  -- | Builds a buffer representing calldata based on the given cli arguments
  buildCalldata :: App m => CommonOptions -> Maybe Text -> [String] -> m (Expr Buf, [Prop])
  buildCalldata cOpts sig arg = case (cOpts.calldata, sig) of
    -- fully abstract calldata
    (Nothing, Nothing) -> mkCalldata Nothing []
    -- fully concrete calldata
    (Just c, Nothing) -> do
      let val = hexByteString $ strip0x c
      if (isNothing val) then liftIO $ do
        putStrLn $ "Error, invalid calldata: " <>  show c
        exitFailure
      else pure (ConcreteBuf (fromJust val), [])
    -- calldata according to given abi with possible specializations from the `arg` list
    (Nothing, Just sig') -> do
      method' <- liftIO $ functionAbi sig'
      mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) arg
    -- both args provided
    (_, _) -> liftIO $ do
      putStrLn "incompatible options provided: --calldata and --sig"
      exitFailure
  
  
  -- If function signatures are known, they should always be given for best results.
  symbCheck :: App m => CommonFileOptions -> SymbolicOptions -> CommonExecOptions -> CommonOptions -> m ()
  symbCheck cFileOpts sOpts cExecOpts cOpts = do
    let block' = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
        blockUrlInfo = (,) block' <$> cExecOpts.rpc
    sess <- Fetch.mkSession
    calldata <- buildCalldata cOpts sOpts.sig sOpts.arg
    preState <- symvmFromCommand cExecOpts sOpts cFileOpts sess calldata
    errCodes <- case sOpts.assertions of
      Nothing -> pure defaultPanicCodes
      Just s -> case (mapM readMaybe $ splitOn "," s) of
        Nothing -> liftIO $ do
          putStrLn $ "Error: invalid assertion codes: " <> s
          exitFailure
        Just codes -> pure codes
    when (cOpts.verb > 0) $ liftIO $ putStrLn $ "Using assertion code(s): " <> intercalate "," (map show errCodes)
    cores <- liftIO $ unsafeInto <$> getNumProcessors
    let solverCount = fromMaybe cores cOpts.numSolvers
    solver <- liftIO $ getSolver cOpts.solver
    withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do
      let veriOpts = VeriOpts { iterConf = IterConfig {
                                maxIter = parseMaxIters cOpts.maxIterations
                                , askSmtIters = cOpts.askSmtIterations
                                , loopHeuristic = cOpts.loopDetectionHeuristic
                                }
                              , rpcInfo = mempty {Fetch.blockNumURL = blockUrlInfo}
                              }
      let fetcher = Fetch.oracle solvers (Just sess) veriOpts.rpcInfo
      (expr, res) <- verify solvers fetcher veriOpts preState (Just $ checkAssertions errCodes)
      case res of
        [Qed] -> do
          liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
          showExtras solvers sOpts calldata expr
        _ -> do
          let cexs = snd <$> mapMaybe getCex res
              counterexamples
                | null cexs = []
                | otherwise =
                   [ ""
                   , ("Discovered the following " <> (T.pack $ show (length cexs)) <> " counterexample(s):")
                   , ""
                   ] <> fmap (formatCex (fst calldata) Nothing) cexs
          liftIO $ T.putStrLn $ T.unlines counterexamples
          liftIO $ printWarnings Nothing [expr] res "symbolically"
          showExtras solvers sOpts calldata expr
          liftIO exitFailure
  
  showExtras :: App m => SolverGroup ->SymbolicOptions -> (Expr Buf, [Prop]) -> Expr End -> m ()
  showExtras solvers sOpts calldata expr = do
    when sOpts.showTree $ liftIO $ do
      putStrLn "=== Expression ===\n"
      T.putStrLn $ formatExpr $ Expr.simplify expr
      putStrLn ""
    when sOpts.showReachableTree $ do
      reached <- reachable solvers expr
      liftIO $ do
        putStrLn "=== Potentially Reachable Expression ===\n"
        T.putStrLn (formatExpr . Expr.simplify $ reached)
        putStrLn ""
    when sOpts.getModels $ do
      liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ==="
      ms <- produceModels solvers expr
      liftIO $ forM_ ms (showModel (fst calldata))
  
  isTestOrLib :: Text -> Bool
  isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file
  
  areAnyPrefixOf :: [Text] -> Text -> Bool
  areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes
  
  launchExec :: App m => CommonFileOptions -> ExecOptions -> CommonExecOptions -> CommonOptions -> m ()
  launchExec cFileOpts execOpts cExecOpts cOpts = do
    dapp <- getSrcInfo execOpts cOpts
    sess <- Fetch.mkSession
    vm <- vmFromCommand cOpts cExecOpts cFileOpts execOpts sess
    let
      block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
      blockUrlInfo = (,) block <$> cExecOpts.rpc
      rpcDat :: Fetch.RpcInfo = mempty { Fetch.blockNumURL = blockUrlInfo }
  
    -- TODO: we shouldn't need solvers to execute this code
    withSolvers Z3 0 1 Nothing $ \solvers -> do
      let fetcher = Fetch.oracle solvers (Just sess) rpcDat
      vm' <- if execOpts.jsonTrace
             then do
               (vm', (_, traces)) <- runStateT (interpretWithTrace fetcher EVM.Stepper.runFully) (vm, [])
               liftIO $ do
                 let ret = case vm'.result of
                             Just (VMSuccess (ConcreteBuf r)) -> ByteStringS r
                             Just (VMFailure (Revert (ConcreteBuf r))) -> ByteStringS r
                             _ -> ByteStringS ""
                 let res = VMTraceStepResult ret (vm.state.gas - vm'.state.gas)
                 let jsonl = toLazyByteString $ jsonlBuilder traces <> jsonLine res
                 let file = "hevm-trace.jsonl"
                 BS.writeFile file jsonl
                 putStrLn $ "Wrote json trace to " <> show file
               pure vm'
             else EVM.Stepper.interpret fetcher vm EVM.Stepper.runFully
      writeTraceDapp dapp vm'
      case vm'.result of
        Just (VMFailure (Revert msg)) -> liftIO $ do
          let res = case msg of
                      ConcreteBuf bs -> bs
                      _ -> "<symbolic>"
          putStrLn $ "Revert: " <> (show $ ByteStringS res)
          exitWith (ExitFailure 2)
        Just (VMFailure err) -> liftIO $ do
          putStrLn $ "Error: " <> show err
          exitWith (ExitFailure 2)
        Just (VMSuccess buf) -> liftIO $ do
          let msg = case buf of
                ConcreteBuf msg' -> msg'
                _ -> "<symbolic>"
          print $ "Return: " <> (show $ ByteStringS msg)
        _ ->
          internalError "no EVM result"
  
  -- | Creates a (concrete) VM from command line options
  vmFromCommand :: App m => CommonOptions -> CommonExecOptions -> CommonFileOptions -> ExecOptions -> Fetch.Session -> m (VM Concrete RealWorld)
  vmFromCommand cOpts cExecOpts cFileOpts execOpts sess = do
    conf <- readConfig
    (miner,ts,baseFee,blockNum,prevRan) <- case cExecOpts.rpc of
      Nothing -> pure (LitAddr 0,Lit 0,0,Lit 0,0)
      Just url -> liftIO $ Fetch.fetchBlockWithSession conf sess block url >>= \case
        Nothing -> do
          putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url
          exitFailure
        Just Block{..} -> pure ( coinbase
                               , timestamp
                               , baseFee
                               , number
                               , prevRandao
                               )
  
    codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code
    contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of
      (Just url, Just addr', Just c) -> liftIO $ do
        let code = hexByteString $ strip0x c
        if isNothing code then do
          putStrLn $ "Error, invalid code: " <> show c
          exitFailure
        else
          Fetch.fetchContractWithSession conf sess block url addr' >>= \case
            Nothing -> do
              putStrLn $ "Error: contract not found: " <> show address
              exitFailure
            Just contract ->
              -- if both code and url is given,
              -- fetch the contract and overwrite the code
              pure $ initialContract (mkCode $ fromJust code)
                  & set #balance  (contract.balance)
                  & set #nonce    (contract.nonce)
                  & set #external (contract.external)
  
      (Just url, Just addr', Nothing) ->
        liftIO $ Fetch.fetchContractWithSession conf sess block url addr' >>= \case
          Nothing -> do
            putStrLn $ "Error, contract not found: " <> show address
            exitFailure
          Just contract -> pure contract
  
      (_, _, Just c)  -> do
        let code = hexByteString $ strip0x c
        if (isNothing code) then liftIO $ do
          putStrLn $ "Error, invalid code: " <> show c
          exitFailure
        else pure $ initialContract (mkCode $ fromJust code)
  
      (_, _, Nothing) -> liftIO $ do
        putStrLn "Error, must provide at least (rpc + address) or code"
        exitFailure
  
    let ts' = case maybeLitWordSimp ts of
          Just t -> t
          Nothing -> internalError "unexpected symbolic timestamp when executing vm test"
  
    if (isNothing bsCallData) then liftIO $ do
      putStrLn $ "Error, invalid calldata: " <> show calldata
      exitFailure
    else liftIO $ do
      vm <- stToIO $ vm0 baseFee miner ts' blockNum prevRan contract
      pure $ EVM.Transaction.initTx vm
    where
          bsCallData = bytes (.calldata) (pure "")
          block   = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
          val     = word (.value) 0
          caller  = addr (.caller) (LitAddr 0)
          origin  = addr (.origin) (LitAddr 0)
          calldata = ConcreteBuf $ fromJust bsCallData
          decipher = hexByteString . strip0x
          mkCode bs = if execOpts.create
                      then InitCode bs mempty
                      else RuntimeCode (ConcreteRuntimeCode bs)
          address = if execOpts.create
                    then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddrSimp origin) (W64 $ word64 (.nonce) 0))
                    else addr (.address) (LitAddr 0xacab)
  
          vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts
            { contract       = c
            , otherContracts = []
            , calldata       = (calldata, [])
            , value          = Lit val
            , address        = address
            , caller         = caller
            , origin         = origin
            , gas            = word64 (.gas) 0xffffffffffffffff
            , baseFee        = baseFee
            , priorityFee    = word (.priorityFee) 0
            , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff
            , coinbase       = addr (.coinbase) miner
            , number         = maybe blockNum Lit cExecOpts.number
            , timestamp      = Lit $ word (.timestamp) ts
            , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff
            , gasprice       = word (.gasprice) 0
            , maxCodeSize    = word (.maxcodesize) 0xffffffff
            , prevRandao     = word (.prevRandao) prevRan
            , schedule       = feeSchedule
            , chainId        = word (.chainid) 1
            , create         = (.create) execOpts
            , baseState      = EmptyBase
            , txAccessList   = mempty -- TODO: support me soon
            , allowFFI       = False
            , freshAddresses = 0
            , beaconRoot     = 0
            }
          word f def = fromMaybe def (f cExecOpts)
          word64 f def = fromMaybe def (f cExecOpts)
          addr f def = maybe def LitAddr (f cExecOpts)
          bytes f def = maybe def decipher (f cOpts)
  
  symvmFromCommand :: App m =>
    CommonExecOptions -> SymbolicOptions -> CommonFileOptions -> Fetch.Session ->
    (Expr Buf, [Prop]) -> m (VM EVM.Types.Symbolic RealWorld)
  symvmFromCommand cExecOpts sOpts cFileOpts sess calldata = do
    conf <- readConfig
    (miner,blockNum,baseFee,prevRan) <- case cExecOpts.rpc of
      Nothing -> pure (SymAddr "miner",Lit 0,0,0)
      Just url -> liftIO $ Fetch.fetchBlockWithSession conf sess block url >>= \case
        Nothing -> do
          putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url
          exitFailure
        Just Block{..} -> pure ( coinbase
                               , number
                               , baseFee
                               , prevRandao
                               )
  
    let
      caller = maybe (SymAddr "caller") LitAddr cExecOpts.caller
      ts = maybe Timestamp Lit cExecOpts.timestamp
      callvalue = maybe TxValue Lit cExecOpts.value
      storageBase = maybe AbstractBase parseInitialStorage (sOpts.initialStorage)
  
    codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code
    contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of
      (Just url, Just addr', _) ->
        liftIO $ Fetch.fetchContractWithSession conf sess block url addr' >>= \case
          Nothing -> do
            putStrLn "Error, contract not found."
            exitFailure
          Just contract' -> case codeWrapped of
                Nothing -> pure contract'
                -- if both code and url is given,
                -- fetch the contract and overwrite the code
                Just c -> do
                  let c' = decipher c
                  if isNothing c' then do
                    putStrLn $ "Error, invalid code: " <> show c
                    exitFailure
                  else pure $ do
                    initialContract (mkCode $ fromJust c')
                          & set #origStorage (contract'.origStorage)
                          & set #balance     (contract'.balance)
                          & set #nonce       (contract'.nonce)
                          & set #external    (contract'.external)
  
      (_, _, Just c) -> liftIO $ do
        let c' = decipher c
        if isNothing c' then do
          putStrLn $ "Error, invalid code: " <> show c
          exitFailure
        else case storageBase of
          EmptyBase -> pure (initialContract . mkCode $ fromJust c')
          AbstractBase -> pure ((`abstractContract` address) . mkCode $ fromJust c')
  
      (_, _, Nothing) -> liftIO $ do
        putStrLn "Error, must provide at least (rpc + address) or code"
        exitFailure
  
    vm <- liftIO $ stToIO $ vm0 baseFee miner ts blockNum prevRan calldata callvalue caller contract storageBase
    pure $ EVM.Transaction.initTx vm
  
    where
      decipher = hexByteString . strip0x
      block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
      origin = eaddr (.origin) (SymAddr "origin")
      mkCode bs = if sOpts.create
                     then InitCode bs mempty
                     else RuntimeCode (ConcreteRuntimeCode bs)
      address = eaddr (.address) (SymAddr "entrypoint")
      originAddr = eaddr (.origin) (SymAddr "origin")
      originContr = abstractContract (RuntimeCode (SymbolicRuntimeCode mempty)) originAddr
      vm0 baseFee miner ts blockNum prevRan cd callvalue caller c baseState = makeVm $ VMOpts
        { contract       = c
        , otherContracts = [(originAddr, originContr)]
        , calldata       = cd
        , value          = callvalue
        , address        = address
        , caller         = caller
        , origin         = origin
        , gas            = ()
        , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff
        , baseFee        = baseFee
        , priorityFee    = word (.priorityFee) 0
        , coinbase       = eaddr (.coinbase) miner
        , number         = maybe blockNum Lit cExecOpts.number
        , timestamp      = ts
        , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff
        , gasprice       = word (.gasprice) 0
        , maxCodeSize    = word (.maxcodesize) 0xffffffff
        , prevRandao     = word (.prevRandao) prevRan
        , schedule       = feeSchedule
        , chainId        = word (.chainid) 1
        , create         = (.create) sOpts
        , baseState      = baseState
        , txAccessList   = mempty
        , allowFFI       = False
        , freshAddresses = 0
        , beaconRoot     = 0
        }
      word f def = fromMaybe def (f cExecOpts)
      word64 f def = fromMaybe def (f cExecOpts)
      eaddr f def = maybe def LitAddr (f cExecOpts)
  
  unitTestOptions :: App m => TestOptions -> CommonOptions -> SolverGroup -> Maybe BuildOutput -> m (UnitTestOptions RealWorld)
  unitTestOptions testOpts cOpts solvers buildOutput = do
    root <- liftIO $ getRoot cOpts
    mockData <- if isJust testOpts.mockFile then liftIO $ do
        ret <- Fetch.readMockData (fromJust testOpts.mockFile)
        case ret of
          Left err -> do
            putStrLn $ "Error reading mock file: " <> err
            exitFailure
          Right md -> pure md
      else pure mempty
  
    let srcInfo = maybe emptyDapp (dappInfo root) buildOutput
    let blockUrlInfo = case (testOpts.number, testOpts.rpc) of
            (Just block, Just url) -> Just (Fetch.BlockNumber block, url)
            (Nothing, Just url) -> Just (Fetch.Latest, url)
            _ -> Nothing
        rpcDat = Fetch.mkRpcInfo blockUrlInfo mockData
    sess <- Fetch.mkSession
    params <- paramsFromRpc rpcDat sess
    let testn = params.number
        block' = if 0 == testn
         then Fetch.Latest
         else Fetch.BlockNumber testn
    pure UnitTestOptions
      { solvers = solvers
      , sess = sess
      , rpcInfo = let i = case testOpts.rpc of
                       Just url -> Just (block', url)
                       Nothing  -> Nothing
                  in rpcDat { Fetch.blockNumURL = i }
      , maxIter = parseMaxIters cOpts.maxIterations
      , askSmtIters = cOpts.askSmtIterations
      , smtTimeout = Just cOpts.smttimeout
      , match = T.pack $ fromMaybe ".*" testOpts.match
      , prefix = T.pack testOpts.prefix
      , testParams = params
      , dapp = srcInfo
      , ffiAllowed = testOpts.ffi
      , checkFailBit = cOpts.assertionType == DSTest
      , loopHeuristic = cOpts.loopDetectionHeuristic
      }
  parseInitialStorage :: InitialStorage -> BaseState
  parseInitialStorage Empty = EmptyBase
  parseInitialStorage Abstract = AbstractBase
  