content: {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE FlexibleInstances #-}
  
  module EVM.SymExec where
  
  import Prelude hiding (Foldable(..))
  
  import Control.Arrow ((>>>))
  import Control.Concurrent.Async (concurrently, mapConcurrently)
  import Control.Concurrent.Spawn (parMapIO, pool)
  import Control.Monad (when, forM_, forM)
  import Control.Monad.IO.Unlift
  import Control.Monad.Operational qualified as Operational
  import Control.Monad.ST (RealWorld, stToIO, ST)
  import Control.Monad.State.Strict (runStateT)
  import Data.ByteString (ByteString)
  import Data.ByteString qualified as BS
  import Data.Containers.ListUtils (nubOrd)
  import Data.DoubleWord (Word256)
  import Data.Foldable (Foldable(..))
  import Data.List (sortBy, sort)
  import Data.List.NonEmpty qualified as NE
  import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
  import Data.Map.Strict (Map)
  import Data.Map.Strict qualified as Map
  import Data.Map.Merge.Strict qualified as Map
  import Data.Set (Set)
  import Data.Set qualified as Set
  import Data.Text (Text)
  import Data.Text qualified as T
  import Data.Text.IO qualified as T
  import Data.Tree.Zipper qualified as Zipper
  import Data.Tuple (swap)
  import Data.Vector qualified as V
  import Data.Vector.Storable qualified as VS
  import Data.Vector.Storable.ByteString (vectorToByteString)
  
  import EVM (makeVm, abstractContract, initialContract, getCodeLocation, isValidJumpDest)
  import EVM.Exec
  import EVM.Fetch qualified as Fetch
  import EVM.ABI
  import EVM.Effects
  import EVM.Expr qualified as Expr
  import EVM.FeeSchedule (feeSchedule)
  import EVM.Format (formatExpr, formatPartial, formatPartialDetailed, showVal, indent, formatBinary, formatProp, formatState, formatError)
  import EVM.SMT qualified as SMT
  import EVM.Solvers
  import EVM.Stepper (Stepper)
  import EVM.Stepper qualified as Stepper
  import EVM.Traversals
  import EVM.Types hiding (Comp)
  import EVM.Types qualified
  import EVM.Expr (maybeConcStoreSimp)
  import GHC.Conc (getNumProcessors)
  import GHC.Generics (Generic)
  import Optics.Core
  import Options.Generic (ParseField, ParseFields, ParseRecord)
  import Text.Printf (printf)
  import Witch (into, unsafeInto)
  import Data.Text.Encoding (encodeUtf8)
  import EVM.Solidity (WarningData (..))
  
  data LoopHeuristic
    = Naive
    | StackBased
    deriving (Eq, Show, Read, ParseField, ParseFields, ParseRecord, Generic)
  
  groupIssues :: forall a b . GetUnknownStr b => [ProofResult a b] -> [(Integer, String)]
  groupIssues results = map (\g -> (into (length g), NE.head g)) grouped
    where
      getIssue :: ProofResult a b -> Maybe String
      getIssue (Error k) = Just k
      getIssue (Unknown reason) = Just $ "SMT solver says: " <> getUnknownStr reason
      getIssue _ = Nothing
      grouped = NE.group $ sort $ mapMaybe getIssue results
  
  groupPartials :: Maybe (WarningData s t) -> [Expr End] -> [(Integer, String)]
  groupPartials warnData e = map (\g -> (into (length g), NE.head g)) grouped
    where
      getPartial :: Expr End -> Maybe String
      getPartial (Partial _ _ reason) = Just $ T.unpack $ formatPartialDetailed warnData reason
      getPartial _ = Nothing
      grouped = NE.group $ sort $ mapMaybe getPartial e
  
  data IterConfig = IterConfig
    { maxIter :: Maybe Integer
    , askSmtIters :: Integer
    , loopHeuristic :: LoopHeuristic
    }
    deriving (Eq, Show)
  
  defaultIterConf :: IterConfig
  defaultIterConf = IterConfig
    { maxIter = Nothing
    , askSmtIters = 1
    , loopHeuristic = StackBased
    }
  
  data VeriOpts = VeriOpts
    { iterConf :: IterConfig
    , rpcInfo :: Fetch.RpcInfo
    }
    deriving (Show)
  
  defaultVeriOpts :: VeriOpts
  defaultVeriOpts = VeriOpts
    { iterConf = defaultIterConf
    , rpcInfo = mempty
    }
  
  rpcVeriOpts :: (Fetch.BlockNumber, Text) -> VeriOpts
  rpcVeriOpts info = defaultVeriOpts { rpcInfo  = mempty { Fetch.blockNumURL = Just info }}
  
  extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
  extractCex (Cex c) = Just c
  extractCex _ = Nothing
  
  
  -- | Abstract calldata argument generation
  symAbiArg :: Text -> AbiType -> CalldataFragment
  symAbiArg name = \case
    AbiUIntType n ->
      if n `mod` 8 == 0 && n <= 256
      then St [] v
      else internalError "bad type"
    AbiIntType n ->
      if n `mod` 8 == 0 && n <= 256
      then St [] v
      else internalError "bad type"
    AbiBoolType -> St [] v
    AbiAddressType -> St [] (WAddr (SymAddr name))
    AbiBytesType n ->
      if n > 0 && n <= 32
      then St [] v
      else internalError "bad type"
    AbiArrayType sz tps -> do
      Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-a-" <> i) tp) $ (V.replicate sz tps)
    AbiTupleType tps ->
      Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-t-" <> i) tp) $ tps
    t -> internalError $ "TODO: symbolic abi encoding for " <> show t
    where
      v = Var name
  
  data CalldataFragment
    = St [Prop] (Expr EWord)
    | Dy [Prop] (Expr EWord) (Expr Buf)
    | Comp [CalldataFragment]
    deriving (Show, Eq)
  
  -- | Generates calldata matching given type signature, optionally specialized
  -- with concrete arguments.
  -- Any argument given as "<symbolic>" or omitted at the tail of the list are
  -- kept symbolic.
  symCalldata :: App m => Text -> [AbiType] -> [String] -> Expr Buf -> m (Expr Buf, [Prop])
  symCalldata sig typesignature concreteArgs base = do
    conf <- readConfig
    let
      args = concreteArgs <> replicate (length typesignature - length concreteArgs) "<symbolic>"
      mkArg :: AbiType -> String -> Int -> CalldataFragment
      mkArg typ "<symbolic>" n = symAbiArg (T.pack $ "arg" <> show n) typ
      mkArg typ arg _ =
        case makeAbiValue typ arg of
          AbiUInt _ w -> St [] . Lit . into $ w
          AbiInt _ w -> St [] . Lit . unsafeInto $ w
          AbiAddress w -> St [] . Lit . into $ w
          AbiBool w -> St [] . Lit $ if w then 1 else 0
          _ -> internalError "TODO"
      calldatas = zipWith3 mkArg typesignature args [1..]
      (cdBuf, props) = combineFragments calldatas base
      withSelector = writeSelector cdBuf sig
      sizeConstraints
        = (Expr.bufLength withSelector .>= cdLen calldatas)
        .&& (Expr.bufLength withSelector .< (Lit (2 ^ conf.maxBufSize)))
    pure (withSelector, sizeConstraints : props)
  
  cdLen :: [CalldataFragment] -> Expr EWord
  cdLen = go (Lit 4)
    where
      go acc = \case
        [] -> acc
        (hd:tl) -> case hd of
                     St _ _ -> go (Expr.add acc (Lit 32)) tl
                     Comp xs | all isSt xs -> go acc (xs <> tl)
                     _ -> internalError "unsupported"
  
  writeSelector :: Expr Buf -> Text -> Expr Buf
  writeSelector buf sig =
    writeSel (Lit 0) $ writeSel (Lit 1) $ writeSel (Lit 2) $ writeSel (Lit 3) buf
    where
      sel = ConcreteBuf $ selector sig
      writeSel idx = Expr.writeByte idx (Expr.readByte idx sel)
  
  combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop])
  combineFragments fragments base = go (Lit 4) fragments (base, [])
    where
      go :: Expr EWord -> [CalldataFragment] -> (Expr Buf, [Prop]) -> (Expr Buf, [Prop])
      go _ [] acc = acc
      go idx (f:rest) (buf, ps) =
        case f of
          -- static fragments get written as a word in place
          St p w -> go (Expr.add idx (Lit 32)) rest (Expr.writeWord idx w buf, p <> ps)
          -- compound fragments that contain only static fragments get written in place
          Comp xs | all isSt xs -> go idx (xs <> rest) (buf,ps)
          -- dynamic fragments are not yet supported... :/
          s -> internalError $ "unsupported cd fragment: " <> show s
  
  isSt :: CalldataFragment -> Bool
  isSt (St {}) = True
  isSt (Comp fs) = all isSt fs
  isSt _ = False
  
  
  abstractVM
    :: (Expr Buf, [Prop])
    -> ByteString
    -> Maybe (Precondition s)
    -> Bool
    -> ST s (VM Symbolic s)
  abstractVM cd contractCode maybepre create = do
    let value = TxValue
    let code = if create then InitCode contractCode (fst cd) else RuntimeCode (ConcreteRuntimeCode contractCode)
    vm <- loadSymVM code value (if create then mempty else cd) create
    let precond = case maybepre of
                  Nothing -> []
                  Just p -> [p vm]
    pure $ vm & over #constraints (<> precond)
  
  -- Creates symbolic VM with empty storage, not symbolic storage like loadSymVM
  loadEmptySymVM
    :: ContractCode
    -> Expr EWord
    -> (Expr Buf, [Prop])
    -> ST s (VM Symbolic s)
  loadEmptySymVM x callvalue cd =
    (makeVm $ VMOpts
      { contract = initialContract x
      , otherContracts = []
      , calldata = cd
      , value = callvalue
      , baseState = EmptyBase
      , address = SymAddr "entrypoint"
      , caller = SymAddr "caller"
      , origin = SymAddr "origin"
      , coinbase = SymAddr "coinbase"
      , number = Lit 0
      , timestamp = Lit 0
      , blockGaslimit = 0
      , gasprice = 0
      , prevRandao = 42069
      , gas = ()
      , gaslimit = 0xffffffffffffffff
      , baseFee = 0
      , priorityFee = 0
      , maxCodeSize = 0xffffffff
      , schedule = feeSchedule
      , chainId = 1
      , create = False
      , txAccessList = mempty
      , allowFFI = False
      , freshAddresses = 0
      , beaconRoot = 0
      })
  
  -- Creates a symbolic VM that has symbolic storage, unlike loadEmptySymVM
  loadSymVM
    :: ContractCode
    -> Expr EWord
    -> (Expr Buf, [Prop])
    -> Bool
    -> ST s (VM Symbolic s)
  loadSymVM x callvalue cd create =
    (makeVm $ VMOpts
      { contract = if create then initialContract x else abstractContract x (SymAddr "entrypoint")
      , otherContracts = []
      , calldata = cd
      , value = callvalue
      , baseState = AbstractBase
      , address = SymAddr "entrypoint"
      , caller = SymAddr "caller"
      , origin = SymAddr "origin"
      , coinbase = SymAddr "coinbase"
      , number = Lit 0
      , timestamp = Lit 0
      , blockGaslimit = 0
      , gasprice = 0
      , prevRandao = 42069
      , gas = ()
      , gaslimit = 0xffffffffffffffff
      , baseFee = 0
      , priorityFee = 0
      , maxCodeSize = 0xffffffff
      , schedule = feeSchedule
      , chainId = 1
      , create = create
      , txAccessList = mempty
      , allowFFI = False
      , freshAddresses = 0
      , beaconRoot = 0
      })
  
  -- freezes any mutable refs, making it safe to share between threads
  freezeVM :: VM Symbolic RealWorld -> ST RealWorld (VM Symbolic RealWorld)
  freezeVM vm = do
      state' <- do
        mem' <- freeze (vm.state.memory)
        pure $ vm.state { memory = mem' }
      frames' <- forM (vm.frames :: [Frame Symbolic RealWorld]) $ \frame -> do
        mem' <- freeze frame.state.memory
        pure $ (frame :: Frame Symbolic RealWorld) { state = frame.state { memory = mem' } }
  
      pure (vm :: VM Symbolic RealWorld)
        { state = state'
        , frames = frames'
        }
    where
      freeze = \case
        ConcreteMemory m -> SymbolicMemory . ConcreteBuf . vectorToByteString <$> VS.freeze m
        m@(SymbolicMemory _) -> pure m
  
  -- | Interpreter which explores all paths at branching points. Returns an
  -- 'Expr End' representing the possible executions.
  interpret
    :: forall m . App m
    => Fetch.Fetcher Symbolic m RealWorld
    -> IterConfig
    -> VM Symbolic RealWorld
    -> Stepper Symbolic RealWorld (Expr End)
    -> m (Expr End)
  interpret fetcher iterConf vm =
    eval . Operational.view
    where
    eval :: Operational.ProgramView (Stepper.Action Symbolic RealWorld) (Expr End) -> m (Expr End)
    eval (Operational.Return x) = pure x
    eval (action Operational.:>>= k) =
      case action of
        Stepper.Exec -> do
          conf <- readConfig
          (r, vm') <- liftIO $ stToIO $ runStateT (exec conf) vm
          interpret fetcher iterConf vm' (k r)
        Stepper.EVM m -> do
          (r, vm') <- liftIO $ stToIO $ runStateT m vm
          interpret fetcher iterConf vm' (k r)
        Stepper.ForkMany (PleaseRunAll expr vals continue) -> do
          when (length vals < 2) $ internalError "PleaseRunAll requires at least 2 branches"
          frozen <- liftIO $ stToIO $ freezeVM vm
          let newDepth = vm.exploreDepth+1
          ends <- withRunInIO $ \runInIO -> mapConcurrently (runInIO . runOne frozen newDepth) vals
          pure $ goITE (zip vals ends)
          where
            goITE :: [(Expr EWord, Expr End)] -> Expr End
            goITE [] = internalError "goITE: empty list"
            goITE [(_, end)] = end
            goITE ((val,end):ps) = ITE (Eq expr val) end (goITE ps)
            runOne :: App m => VM 'Symbolic RealWorld -> Int -> Expr EWord -> m (Expr 'End)
            runOne frozen newDepth v = do
              (ra, vma) <- liftIO $ stToIO $ runStateT (continue v) frozen { result = Nothing, exploreDepth = newDepth }
              interpret fetcher iterConf vma (k ra)
        Stepper.Fork (PleaseRunBoth cond continue) -> do
          frozen <- liftIO $ stToIO $ freezeVM vm
          let newDepth = vm.exploreDepth+1
          evalLeft <- toIO $ do
            (ra, vma) <- liftIO $ stToIO $ runStateT (continue True) frozen { result = Nothing, exploreDepth = newDepth }
            interpret fetcher iterConf vma (k ra)
          evalRight <- toIO $ do
            (rb, vmb) <- liftIO $ stToIO $ runStateT (continue False) frozen { result = Nothing, exploreDepth = newDepth }
            interpret fetcher iterConf vmb (k rb)
          (a, b) <- liftIO $ concurrently evalLeft evalRight
          pure $ ITE cond a b
        Stepper.Wait q -> do
          let performQuery = do
                m <- fetcher q
                (r, vm') <- liftIO$ stToIO $ runStateT m vm
                interpret fetcher iterConf vm' (k r)
  
          case q of
            PleaseAskSMT cond preconds continue -> do
              case Expr.concKeccakSimpExpr cond of
                -- is the condition concrete?
                Lit c ->
                  -- have we reached max iterations, are we inside a loop?
                  case (maxIterationsReached vm iterConf.maxIter, isLoopHead iterConf.loopHeuristic vm) of
                    -- Yes. return a partial leaf
                    (Just _, Just True) ->
                      pure $ Partial [] (TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels) $ MaxIterationsReached vm.state.pc vm.state.contract
                    -- No. keep executing
                    _ -> do
                      (r, vm') <- liftIO $ stToIO $ runStateT (continue (Case (c > 0))) vm
                      interpret fetcher iterConf vm' (k r)
  
                -- the condition is symbolic
                _ ->
                  -- are in we a loop, have we hit maxIters, have we hit askSmtIters?
                  case (isLoopHead iterConf.loopHeuristic vm, askSmtItersReached vm iterConf.askSmtIters, maxIterationsReached vm iterConf.maxIter) of
                    -- we're in a loop and maxIters has been reached
                    (Just True, _, Just n) -> do
                      -- continue execution down the opposite branch than the one that
                      -- got us to this point and return a partial leaf for the other side
                      (r, vm') <- liftIO $ stToIO $ runStateT (continue (Case $ not n)) vm
                      a <- interpret fetcher iterConf vm' (k r)
                      pure $ ITE cond a (Partial [] (TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels) (MaxIterationsReached vm.state.pc vm.state.contract))
                    -- we're in a loop and askSmtIters has been reached
                    (Just True, True, _) ->
                      -- ask the smt solver about the loop condition
                      performQuery
                    _ -> do
                      let simpProps = Expr.concKeccakSimpProps ((cond ./= Lit 0):preconds)
                      (r, vm') <- case simpProps of
                        [PBool False] -> liftIO $ stToIO $ runStateT (continue (Case False)) vm
                        [] -> liftIO $ stToIO $ runStateT (continue (Case True)) vm
                        _ -> liftIO $ stToIO $ runStateT (continue UnknownBranch) vm
                      interpret fetcher iterConf vm' (k r)
            _ -> performQuery
  
  maxIterationsReached :: VM Symbolic s -> Maybe Integer -> Maybe Bool
  maxIterationsReached _ Nothing = Nothing
  maxIterationsReached vm (Just maxIter) =
    let codelocation = getCodeLocation vm
        (iters, _) = view (at codelocation % non (0, [])) vm.iterations
    in if unsafeInto maxIter <= iters
       then Map.lookup (codelocation, iters - 1) vm.pathsVisited
       else Nothing
  
  askSmtItersReached :: VM Symbolic s -> Integer -> Bool
  askSmtItersReached vm askSmtIters = let
      codelocation = getCodeLocation vm
      (iters, _) = view (at codelocation % non (0, [])) vm.iterations
    in askSmtIters <= into iters
  
  {- | Loop head detection heuristic
  
   The main thing we wish to differentiate between, are actual loop heads, and branch points inside of internal functions that are called multiple times.
  
   One way to do this is to observe that for internal functions, the compiler must always store a stack item representing the location that it must jump back to. If we compare the stack at the time of the previous visit, and the time of the current visit, and notice that this location has changed, then we can guess that the location is a jump point within an internal function instead of a loop (where such locations should be constant between iterations).
  
   This heuristic is not perfect, and can certainly be tricked, but should generally be good enough for most compiler generated and non pathological user generated loops.
   -}
  isLoopHead :: LoopHeuristic -> VM Symbolic s -> Maybe Bool
  isLoopHead Naive _ = Just True
  isLoopHead StackBased vm = let
      loc = getCodeLocation vm
      oldIters = Map.lookup loc vm.iterations
      isValid (Lit wrd) = wrd <= unsafeInto (maxBound :: Int) && isValidJumpDest vm (unsafeInto wrd)
      isValid _ = False
    in case oldIters of
         Just (_, oldStack) -> Just $ filter isValid oldStack == filter isValid vm.state.stack
         Nothing -> Nothing
  
  type Precondition s = VM Symbolic s -> Prop
  type Postcondition s = VM Symbolic s -> Expr End -> Prop
  
  -- Used only in testing
  checkAssert
    :: App m
    => SolverGroup
    -> [Word256]
    -> ByteString
    -> Maybe Sig
    -> [String]
    -> VeriOpts
    -> m (Expr End, [VerifyResult])
  checkAssert solvers errs c signature' concreteArgs opts = do
    checkAssertWithSession solvers Nothing errs c signature' concreteArgs opts
  
  -- Used only in testing
  checkAssertWithSession
    :: App m
    => SolverGroup
    -> Maybe Fetch.Session
    -> [Word256]
    -> ByteString
    -> Maybe Sig
    -> [String]
    -> VeriOpts
    -> m (Expr End, [VerifyResult])
  checkAssertWithSession solvers sess errs c signature' concreteArgs opts = do
    verifyContractWithSession solvers sess c signature' concreteArgs opts Nothing (Just $ checkAssertions errs)
  
  -- Used only in testing
  getExprEmptyStore
    :: App m
    => SolverGroup
    -> ByteString
    -> Maybe Sig
    -> [String]
    -> VeriOpts
    -> m (Expr End)
  getExprEmptyStore solvers c signature' concreteArgs opts = do
    conf <- readConfig
    calldata <- mkCalldata signature' concreteArgs
    preState <- liftIO $ stToIO $ loadEmptySymVM (RuntimeCode (ConcreteRuntimeCode c)) (Lit 0) calldata
    exprInter <- interpret (Fetch.oracle solvers Nothing opts.rpcInfo) opts.iterConf preState runExpr
    if conf.simp then (pure $ Expr.simplify exprInter) else pure exprInter
  
  -- Used only in testing
  getExpr
    :: App m
    => SolverGroup
    -> ByteString
    -> Maybe Sig
    -> [String]
    -> VeriOpts
    -> m (Expr End)
  getExpr solvers c signature' concreteArgs opts = do
    conf <- readConfig
    calldata <- mkCalldata signature' concreteArgs
    preState <- liftIO $ stToIO $ abstractVM calldata c Nothing False
    exprInter <- interpret (Fetch.oracle solvers Nothing opts.rpcInfo) opts.iterConf preState runExpr
    if conf.simp then (pure $ Expr.simplify exprInter) else pure exprInter
  
  {- | Checks if an assertion violation has been encountered
  
    hevm recognises the following as an assertion violation:
  
    1. the invalid opcode (0xfe) (solc < 0.8)
    2. a revert with a reason of the form `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of the following (solc >= 0.8):
      - 0x00: Used for generic compiler inserted panics.
      - 0x01: If you call assert with an argument that evaluates to false.
      - 0x11: If an arithmetic operation results in underflow or overflow outside of an unchecked { ... } block.
      - 0x12; If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0).
      - 0x21: If you convert a value that is too big or negative into an enum type.
      - 0x22: If you access a storage byte array that is incorrectly encoded.
      - 0x31: If you call .pop() on an empty array.
      - 0x32: If you access an array, bytesN or an array slice at an out-of-bounds or negative index (i.e. x[i] where i >= x.length or i < 0).
      - 0x41: If you allocate too much memory or create an array that is too large.
      - 0x51: If you call a zero-initialized variable of internal function type.
  
    see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require
    NOTE: does not deal with e.g. `assertEq()`
  -}
  checkAssertions :: [Word256] -> Postcondition s
  checkAssertions errs _ = \case
    Failure _ _ (UnrecognizedOpcode 0xfe)  -> PBool False
    Failure _ _ (Revert (ConcreteBuf msg)) -> PBool $ msg `notElem` (fmap panicMsg errs)
    Failure _ _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)
    _ -> PBool True
  
  -- | By default hevm only checks for user-defined assertions
  defaultPanicCodes :: [Word256]
  defaultPanicCodes = [0x01]
  
  allPanicCodes :: [Word256]
  allPanicCodes = [0x00, 0x01, 0x11, 0x12, 0x21, 0x22, 0x31, 0x32, 0x41, 0x51]
  
  -- | Produces the revert message for solc >=0.8 assertion violations
  panicMsg :: Word256 -> ByteString
  panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
  
  -- | Builds a buffer representing calldata from the provided method description
  -- and concrete arguments
  mkCalldata :: App m => Maybe Sig -> [String] -> m (Expr Buf, [Prop])
  mkCalldata Nothing _ = do
    conf <- readConfig
    pure ( AbstractBuf "txdata"
         -- assert that the length of the calldata is never more than 2^64
         -- this is way larger than would ever be allowed by the gas limit
         -- and avoids spurious counterexamples during abi decoding
         -- TODO: can we encode calldata as an array with a smaller length?
         , [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ conf.maxBufSize))]
         )
  mkCalldata (Just (Sig name types)) args =
    symCalldata name types args (AbstractBuf "txdata")
  
  -- Used only in testing
  verifyContract :: forall m . App m
    => SolverGroup
    -> ByteString
    -> Maybe Sig
    -> [String]
    -> VeriOpts
    -> Maybe (Precondition RealWorld)
    -> Maybe (Postcondition RealWorld)
    -> m (Expr End, [VerifyResult])
  verifyContract solvers theCode signature' concreteArgs opts maybepre maybepost = do
    verifyContractWithSession solvers Nothing theCode signature' concreteArgs opts maybepre maybepost
  
  -- Used only in testing
  verifyContractWithSession :: forall m . App m
    => SolverGroup
    -> Maybe Fetch.Session
    -> ByteString
    -> Maybe Sig
    -> [String]
    -> VeriOpts
    -> Maybe (Precondition RealWorld)
    -> Maybe (Postcondition RealWorld)
    -> m (Expr End, [VerifyResult])
  verifyContractWithSession solvers sess theCode signature' concreteArgs opts maybepre maybepost = do
    calldata <- mkCalldata signature' concreteArgs
    preState <- liftIO $ stToIO $ abstractVM calldata theCode maybepre False
    let fetcher = Fetch.oracle solvers sess opts.rpcInfo
    verify solvers fetcher opts preState maybepost
  
  -- | Stepper that parses the result of Stepper.runFully into an Expr End
  runExpr :: Stepper.Stepper Symbolic RealWorld (Expr End)
  runExpr = do
    vm <- Stepper.runFully
    let traces = TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels
    pure $ case vm.result of
      Just (VMSuccess buf) -> Success vm.constraints traces buf (fmap toEContract vm.env.contracts)
      Just (VMFailure e)   -> Failure vm.constraints traces e
      Just (Unfinished p)  -> Partial vm.constraints traces p
      _ -> internalError "vm in intermediate state after call to runFully"
  
  toEContract :: Contract -> Expr EContract
  toEContract c = C c.code c.storage c.tStorage c.balance c.nonce
  
  -- | Converts a given top level expr into a list of final states and the
  -- associated path conditions for each state.
  flattenExpr :: Expr End -> [Expr End]
  flattenExpr = go []
    where
      go :: [Prop] -> Expr End -> [Expr End]
      go pcs = \case
        ITE c t f -> go (PNeg ((PEq (Lit 0) c)) : pcs) t <> go (PEq (Lit 0) c : pcs) f
        Success ps trace msg store -> [Success (nubOrd $ ps <> pcs) trace msg store]
        Failure ps trace e -> [Failure (nubOrd $ ps <> pcs) trace e]
        Partial ps trace p -> [Partial (nubOrd $ ps <> pcs) trace p]
        GVar _ -> internalError "cannot flatten an Expr containing a GVar"
  
  -- | Strips unreachable branches from a given expr
  -- Returns a list of executed SMT queries alongside the reduced expression for debugging purposes
  -- Note that the reduced expression loses information relative to the original
  -- one if jump conditions are removed. This restriction can be removed once
  -- Expr supports attaching knowledge to AST nodes.
  -- Although this algorithm currently parallelizes nicely, it does not exploit
  -- the incremental nature of the task at hand. Introducing support for
  -- incremental queries might let us go even faster here.
  -- TODO: handle errors properly
  reachable :: App m => SolverGroup -> Expr End -> m (Expr End)
  reachable solvers e = do
    res <- go [] e
    pure $ fromMaybe (internalError "no reachable paths found") res
    where
      {-
         Walk down the tree and collect pcs.
         Dispatch a reachability query at each leaf.
         If reachable return the expr wrapped in a Just. If not return Nothing.
         When walking back up the tree drop unreachable subbranches.
      -}
      go :: (App m, MonadUnliftIO m) => [Prop] -> Expr End -> m (Maybe (Expr End))
      go pcs = \case
        ITE c t f -> do
          (tres, fres) <- withRunInIO $ \env -> concurrently
            (env $ go (PEq (Lit 1) c : pcs) t)
            (env $ go (PEq (Lit 0) c : pcs) f)
          let subexpr = case (tres, fres) of
                (Just t', Just f') -> Just $ ITE c t' f'
                (Just t', Nothing) -> Just t'
                (Nothing, Just f') -> Just f'
                (Nothing, Nothing) -> Nothing
          pure subexpr
        leaf -> do
          res <- checkSatWithProps solvers pcs
          case res of
            Qed -> pure Nothing
            Cex _ -> pure (Just leaf)
            -- if we get an error, we don't know if the leaf is reachable or not, so
            -- we assume it could be reachable
            _ -> pure (Just leaf)
  
  -- | Extract constraints stored in Expr End nodes
  extractProps :: Expr End -> [Prop]
  extractProps = \case
    ITE _ _ _ -> []
    Success asserts _ _ _ -> asserts
    Failure asserts _ _ -> asserts
    Partial asserts _ _ -> asserts
    GVar _ -> internalError "cannot extract props from a GVar"
  
  extractEndStates :: Expr End -> Map (Expr EAddr) (Expr EContract)
  extractEndStates = \case
    ITE {} -> mempty
    Success _ _ _ contr -> contr
    Failure {} -> mempty
    Partial  {} -> mempty
    GVar _ -> internalError "cannot extract props from a GVar"
  
  isPartial :: Expr a -> Bool
  isPartial (Partial _ _ _) = True
  isPartial _ = False
  
  printPartialIssues :: [Expr End] -> String -> IO ()
  printPartialIssues flattened call =
    when (any isPartial flattened) $ do
      T.putStrLn $ indent 3 "\x1b[33m[WARNING]\x1b[0m: hevm was only able to partially explore "
                  <> T.pack call <> " due to the following issue(s):"
      T.putStr . T.unlines . fmap (indent 5 . ("- " <>)) . fmap formatPartial . (map fst) . getPartials $ flattened
  
  getPartials :: [Expr End] -> [(PartialExec, Expr End)]
  getPartials = mapMaybe go
    where
      go :: Expr End -> Maybe (PartialExec, Expr End)
      go = \case
        e@(Partial _ _ p) -> Just (p, e)
        _ -> Nothing
  
  -- | Symbolically execute the VM and check all endstates against the
  -- postcondition, if available.
  verify :: App m
    => SolverGroup
    -> Fetch.Fetcher Symbolic m RealWorld
    -> VeriOpts
    -> VM Symbolic RealWorld
    -> Maybe (Postcondition RealWorld)
    -> m (Expr End, [VerifyResult])
  verify solvers fetcher opts preState maybepost = do
    (expr, res, _) <- verifyInputs solvers opts fetcher preState maybepost
    pure $ verifyResults preState expr res
  
  verifyResults :: VM Symbolic RealWorld -> Expr End -> [(SMTResult, Expr End)] -> (Expr End, [VerifyResult])
  verifyResults preState expr cexs = if null cexs then (expr, [Qed]) else (expr, fmap toVRes cexs)
    where
      toVRes :: (SMTResult, Expr End) -> VerifyResult
      toVRes (res, leaf) = case res of
        Cex model -> Cex (leaf, expandCex preState model)
        Unknown reason -> Unknown (reason, leaf)
        Error e -> Error e
        Qed -> Qed
  
  -- | Symbolically execute the VM and find possible inputs given the
  -- postcondition, if available.
  verifyInputs
    :: App m
    => SolverGroup
    -> VeriOpts
    -> Fetch.Fetcher Symbolic m RealWorld
    -> VM Symbolic RealWorld
    -> Maybe (Postcondition RealWorld)
    -> m (Expr End, [(SMTResult, Expr End)], [(PartialExec, Expr End)])
  verifyInputs solvers opts fetcher preState maybepost = do
    conf <- readConfig
    let call = mconcat ["prefix 0x", getCallPrefix preState.state.calldata]
    when conf.debug $ liftIO $ putStrLn $ "   Exploring call " <> call
  
    expr <- interpret fetcher opts.iterConf preState runExpr
    when conf.dumpExprs $ liftIO $ T.writeFile "unsimplified.expr" (formatExpr expr)
    let flattened = flattenExpr expr
    when (conf.dumpExprs && conf.simp) $ liftIO $ do
      let exprSimplified = Expr.simplify expr
      T.writeFile "simplified.expr" (formatExpr exprSimplified)
      T.writeFile "simplified-conc.expr" (formatExpr $ Expr.simplify $ mapExpr Expr.concKeccakOnePass exprSimplified)
  
    let partials = getPartials flattened
    when conf.debug $ liftIO $ do
      putStrLn "   Flattening expression"
      printPartialIssues flattened ("the call " <> call)
      putStrLn $ "   Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
      putStrLn $ "   Keccak preimages in state: " <> (show $ length preState.keccakPreImgs)
    case maybepost of
      Nothing -> pure (expr, [(Qed, expr)], partials)
      Just post -> do
        let
          -- Filter out any leaves from `flattened` that can be statically shown to be safe
          tocheck = flip map flattened $ \leaf -> (toProps leaf preState post, leaf)
          withQueries = filter canBeSat tocheck
        when conf.debug $ liftIO $ putStrLn $ "   Checking for reachability of " <> show (length withQueries)
          <> " potential property violation(s) in call " <> call
  
        -- Dispatch the remaining branches to the solver to check for violations
        results <- withRunInIO $ \env -> flip mapConcurrently withQueries $ \(query, leaf) -> do
          res <- env $ checkSatWithProps solvers query
          when conf.debug $ putStrLn $ "   SMT result: " <> show res
          pure (res, leaf)
        let cexs = filter (\(res, _) -> not . isQed $ res) results
        when conf.debug $ liftIO $
          putStrLn $ "   Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
        pure (expr, cexs, partials)
    where
      getCallPrefix :: Expr Buf -> String
      getCallPrefix (WriteByte (Lit 0) (LitByte a) (WriteByte (Lit 1) (LitByte b) (WriteByte (Lit 2) (LitByte c) (WriteByte (Lit 3) (LitByte d) _)))) = mconcat $ map (printf "%02x") [a,b,c,d]
      getCallPrefix _ = "unknown"
      toProps leaf vm post = let
        postCondition = post preState leaf
        keccakConstraints = map (\(bs, k)-> PEq (Keccak (ConcreteBuf bs)) (Lit k)) (Set.toList vm.keccakPreImgs)
       in case postCondition of
        PBool True -> [PBool False]
        _ -> PNeg postCondition : vm.constraints <> extractProps leaf <> keccakConstraints
  
      canBeSat (a, _) = case a of
          [PBool False] -> False
          _ -> True
  
  expandCex :: VM Symbolic s -> SMTCex -> SMTCex
  expandCex prestate c = c { store = Map.union c.store concretePreStore }
    where
      concretePreStore = Map.mapMaybe (maybeConcStoreSimp . (.storage))
                       . Map.filter (\v -> Expr.containsNode isConcreteStore v.storage)
                       $ (prestate.env.contracts)
      isConcreteStore = \case
        ConcreteStore _ -> True
        _ -> False
  
  data EqIssues = EqIssues
    { res :: [(EquivResult, String)]
      , partials :: [Expr End]
    }
    deriving (Show, Eq)
  
  instance Monoid EqIssues where
    mempty = EqIssues mempty mempty
  
  instance Semigroup EqIssues where
    EqIssues a1 b1 <> EqIssues a2 b2 = EqIssues (a1 <> a2) (b1 <> b2)
  
  -- | Compares two contract runtimes for trace equivalence by running two VMs
  -- and comparing the end states.
  --
  -- We do this by asking the solver to find a common input for each pair of
  -- endstates that satisfies the path conditions for both sides and produces a
  -- differing output. If we can find such an input, then we have a clear
  -- equivalence break, and since we run this check for every pair of end states,
  -- the check is exhaustive.
  equivalenceCheck
    :: forall m . App m
    => SolverGroup
    -> ByteString
    -> ByteString
    -> VeriOpts
    -> (Expr Buf, [Prop])
    -> Bool
    -> m EqIssues
  equivalenceCheck solvers bytecodeA bytecodeB opts calldata create = do
    conf <- readConfig
    case bytecodeA == bytecodeB of
      True -> liftIO $ do
        putStrLn "bytecodeA and bytecodeB are identical"
        pure mempty
      False -> do
        when conf.debug $ liftIO $ do
          putStrLn "bytecodeA and bytecodeB are different, checking for equivalence"
        branchesAorig <- getBranches bytecodeA
        branchesBorig <- getBranches bytecodeB
        when conf.debug $ liftIO $ do
          liftIO $ putStrLn $ "branchesA props: " <> show (map extractProps branchesAorig)
          liftIO $ putStrLn $ "branchesB props: " <> show (map extractProps branchesBorig)
          liftIO $ putStrLn ""
          liftIO $ putStrLn $ "branchesA endstates: " <> show (map extractEndStates branchesAorig)
  
          liftIO $ putStrLn $ "branchesB endstates: " <> show (map extractEndStates branchesBorig)
        let branchesA = rewriteFresh "A-" branchesAorig
            branchesB = rewriteFresh "B-" branchesBorig
        let partialIssues = EqIssues mempty (filter isPartial branchesA <> filter isPartial branchesB)
        issues <- equivalenceCheck' solvers branchesA branchesB create
        pure $ oneQedOrNoQed issues <> partialIssues
    where
      -- decompiles the given bytecode into a list of branches
      getBranches :: App m => ByteString -> m [Expr End]
      getBranches bs = do
        conf <- readConfig
        let bytecode = if BS.null bs then BS.pack [0] else bs
        prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing create
        expr <- interpret (Fetch.oracle solvers Nothing mempty) opts.iterConf prestate runExpr
        let simpl = if conf.simp then Expr.simplify expr else expr
        pure $ flattenExpr simpl
      oneQedOrNoQed :: EqIssues -> EqIssues
      oneQedOrNoQed (EqIssues res partials) =
        let allQed = all (\(r, _) -> isQed r) res
        in if allQed then EqIssues [(Qed, "")] partials
            else EqIssues (filter (\(r, _) -> not $ isQed r) res) partials
  
  
  rewriteFresh :: Text -> [Expr a] -> [Expr a]
  rewriteFresh prefix exprs = fmap (mapExpr mymap) exprs
    where
      mymap :: Expr a -> Expr a
      mymap = \case
        Gas p x -> Gas (prefix <> p) x
        Var name | ("-fresh-" `T.isInfixOf` name) -> Var $ prefix <> name
        AbstractBuf name | ("-fresh-" `T.isInfixOf` name) -> AbstractBuf $ prefix <> name
        x -> x
  
  equivalenceCheck'
    :: forall m . App m
    => SolverGroup -> [Expr End] -> [Expr End] -> Bool -> m EqIssues
  equivalenceCheck' solvers branchesA branchesB create = do
        conf <- readConfig
        when conf.debug $ do
          liftIO $ printPartialIssues branchesA "codeA"
          liftIO $ printPartialIssues branchesB "codeB"
  
        let allPairs = [(a,b) | a <- branchesA, b <- branchesB]
        liftIO $ putStrLn $ "Found " <> show (length allPairs) <> " total pairs of endstates"
  
        when conf.dumpEndStates $ liftIO $
          putStrLn $ "endstates in bytecodeA: " <> show (length branchesA)
                     <> "\nendstates in bytecodeB: " <> show (length branchesB)
  
        ps <- forM allPairs $ uncurry distinct
        let differingEndStates = sortBySize $ mapMaybe (view _1) ps
        let knownIssues = foldr ((<>) . (view _2)) mempty ps
        liftIO $ putStrLn $ "Asking the SMT solver for " <> (show $ length differingEndStates) <> " pairs"
        when conf.dumpEndStates $ forM_ (zip differingEndStates [(1::Integer)..]) (\(x, i) ->
          liftIO $ T.writeFile ("prop-checked-" <> show i <> ".prop") (T.pack $ show x))
  
        procs <- liftIO getNumProcessors
        newDifferences <- checkAll differingEndStates procs
        let additionalIssues = EqIssues newDifferences mempty
        pure $ knownIssues <> additionalIssues
  
    where
      -- we order the sets by size because this gives us more UNSAT cache hits when
      -- running our queries later on (since we rely on a subset check)
      sortBySize :: [(Set a, b)] -> [(Set a, b)]
      sortBySize = sortBy (\(a, _) (b, _) -> compare (Set.size a) (Set.size b))
  
      -- Allows us to run the queries in parallel. Note that this (seems to) run it
      -- from left-to-right, and with a max of K threads. This is in contrast to
      -- mapConcurrently which would spawn as many threads as there are jobs, and
      -- run them in a random order. We ordered them correctly, though so that'd be bad
      checkAll :: (App m, MonadUnliftIO m) => [(Set Prop, String)] -> Int -> m [(EquivResult, String)]
      checkAll input numproc = withRunInIO $ \env -> do
         wrap <- pool numproc
         parMapIO (runOne env wrap) input
         where
           runOne env wrap (props, meaning) = do
             res <- wrap (env $ checkSatWithProps solvers (Set.toList props))
             pure (res, meaning)
  
      -- Takes two branches and returns a set of props that will need to be
      -- satisfied for the two branches to violate the equivalence check. i.e.
      -- for a given pair of branches, equivalence is violated if there exists an
      -- input that satisfies the branch conditions from both sides and produces
      -- a differing result in each branch
      distinct :: App m => Expr End -> Expr End -> m (Maybe (Set Prop, String), EqIssues)
      distinct aEnd bEnd = do
        (requireToDiff, issues) <- resultsDiffer aEnd bEnd
        let newIssues = EqIssues [] (filter isPartial [aEnd, bEnd])
        pure (collectReqs requireToDiff, issues <> newIssues)
        where
          collectReqs (Just (reqToDiff, meaning)) = Just (Set.fromList $ Expr.simplifyProps (reqToDiff : extractProps aEnd <> extractProps bEnd), meaning)
          collectReqs Nothing  = Nothing
  
      -- Note that the a==b and similar checks are ONLY syntactic checks. If they are true,
      -- then they are surely equivalent. But if not, we need to check via SMT
      resultsDiffer :: App m => Expr End -> Expr End -> m (Maybe (Prop, String), EqIssues)
      resultsDiffer aEnd bEnd = do
        let deployText :: String = if create then "Undeployed contracts. " else "Deployed contracts. "
        case (aEnd, bEnd) of
          (Success aProps _ aOut aState, Success bProps _ bOut bState) ->
            case (aOut == bOut, aState == bState, create) of
              (True, True, _) -> pure (Nothing, mempty)
              (_, _, True) -> do
                -- Either the deployed code doesn't behave the same, or they start with a different
                -- starting state
                deployedContractIssues <- deployedCodeDiffer aOut bOut aProps bProps
                let deployedStateDiffer = (statesDiffer aState bState,
                      deployText <> "Both end in Successful code deployment, but starting states differ. " <>
                      "\nRet of A: " <> T.unpack (formatExpr aOut) <>
                      "\nState of A: " <> T.unpack (formatState aState) <>
                      "\nRet of B: " <> T.unpack (formatExpr bOut) <>
                      "\nState of B: " <> T.unpack (formatState bState))
                pure (Just deployedStateDiffer, deployedContractIssues)
              (_, _, False) -> do
                pure (Just ((aOut ./= bOut) .|| (statesDiffer aState bState),
                  deployText <> "Both end in Success, but return values or end state differ. " <>
                  "\nRet of A: " <> T.unpack (formatExpr aOut) <>
                  "\nState of A: " <> T.unpack (formatState aState) <>
                  "\nRet of B: " <> T.unpack (formatExpr bOut) <>
                  "\nState of B: " <> T.unpack (formatState bState)), mempty)
          (Failure _ _ a, Failure _ _ b) -> pure (Just (differentError a b,
                    deployText <> "Both end in Failure but different EVM error." <>
                    "\nA err: " <> T.unpack (formatError a) <>
                    "\nB err: " <> T.unpack (formatError b)), mempty)
          ((Failure _ _ a), (Success _ _ b _)) -> pure (Just (PBool True,
            deployText <> "Failure vs Success end states" <>
            "\nA err: " <> T.unpack (formatError a) <>
            "\nB ret: " <> T.unpack (formatExpr b)), mempty)
          ((Success _ _ a _), (Failure _ _ b)) -> pure (Just (PBool True,
            deployText <> "Success vs Failure end states" <>
            "\nA ret: " <> T.unpack (formatExpr a) <>
            "\nB err: " <> T.unpack (formatError b)), mempty)
          -- partial end states can't be compared to actual end states, so we always ignore them
          (Partial {}, _) -> pure (Nothing, mempty)
          (_, Partial {}) -> pure (Nothing, mempty)
          (ITE _ _ _, _) -> internalError "Expressions must be flattened"
          (_, ITE _ _ _) -> internalError "Expressions must be flattened"
          (GVar _, _) -> internalError "GVar in equivalence check"
          (_, GVar _) -> internalError "GVar in equivalence check"
  
          where
            -- All EVM errors that cannot be syntactically compared are compared semantically: BalanceTooLow, Revert, and MaxInitCodeSizeExceeded
            differentError :: EvmError ->EvmError -> Prop
            differentError a b =  case (a, b) of
              (BalanceTooLow a1Word a2Word, BalanceTooLow b1Word b2Word) -> (a1Word ./= b1Word) .|| (a2Word ./= b2Word)
              (Revert aBuf, Revert bBuf) -> aBuf ./= bBuf
              (MaxInitCodeSizeExceeded l1 aWord, MaxInitCodeSizeExceeded l2 bWord) -> (PBool (l1 /= l2)) .|| (aWord ./= bWord)
              (x, y) | x == y -> PBool False
                     | otherwise -> PBool True
  
      -- If the original check was for create (i.e. undeployed code), then we must also check that the deployed
      -- code is equivalent. The constraints from the undeployed code (aProps,bProps) influence this check.
      deployedCodeDiffer :: Expr Buf -> Expr Buf -> [Prop] -> [Prop] -> m EqIssues
      deployedCodeDiffer aOut bOut aProps bProps = do
        let simpA = Expr.simplify aOut
            simpB = Expr.simplify bOut
        conf <- readConfig
        case (simpA, simpB) of
          (ConcreteBuf codeA, ConcreteBuf codeB) -> do
            -- TODO: use aProps/bProps to constrain the deployed code
            --       since symbolic code (with constructors taking arguments) is not supported,
            --       this is currently not necessary
            when conf.debug $ liftIO $ do
              liftIO $ putStrLn $ "create deployed code A: " <> bsToHex codeA
                <> " with constraints: " <> (T.unpack . T.unlines $ map formatProp aProps)
              liftIO $ putStrLn $ "create deployed code B: " <> bsToHex codeB
                <> " with constraints: " <> (T.unpack . T.unlines $ map formatProp bProps)
            calldata <- mkCalldata Nothing []
            equivalenceCheck solvers codeA codeB defaultVeriOpts calldata False
          _ -> internalError $ "Symbolic code returned from constructor." <> " A: " <> show simpA <> " B: " <> show simpB
  
      statesDiffer :: Map (Expr EAddr) (Expr EContract) -> Map (Expr EAddr) (Expr EContract) -> Prop
      statesDiffer aState bState =
        case aState == bState of
          True -> PBool False
          False ->  if Set.fromList (Map.keys aState) /= Set.fromList (Map.keys bState)
            -- TODO: consider possibility of aliased symbolic addresses
            then PBool True
            else let
              merged = (Map.merge Map.dropMissing Map.dropMissing (Map.zipWithMatched (\_ x y -> (x,y))) aState bState)
            in Map.foldl' (\a (ac, bc) -> a .|| contractsDiffer ac bc) (PBool False) merged
  
      contractsDiffer :: Expr EContract -> Expr EContract -> Prop
      contractsDiffer ac bc = let
          balsDiffer = case (ac.balance, bc.balance) of
            (Lit ab, Lit bb) -> PBool $ ab /= bb
            (ab, bb) -> if ab == bb then PBool False else ab ./= bb
          -- TODO: is this sound? do we need a more sophisticated nonce representation?
          noncesDiffer = PBool (ac.nonce /= bc.nonce)
          storesDiffer = case (ac.storage, bc.storage) of
            (ConcreteStore as, ConcreteStore bs) | not (as == Map.empty || bs == Map.empty) -> PBool $ as /= bs
            (as, bs) -> if as == bs then PBool False else as ./= bs
        in balsDiffer .|| storesDiffer .|| noncesDiffer
  
  
  both' :: (a -> b) -> (a, a) -> (b, b)
  both' f (x, y) = (f x, f y)
  
  produceModels :: App m => SolverGroup -> Expr End -> m [(Expr End, SMTResult)]
  produceModels solvers expr = do
    let flattened = flattenExpr expr
        withQueries = fmap (\e -> (extractProps e, e)) flattened
    results <- withRunInIO $ \runInIO -> (flip mapConcurrently) withQueries $ \(query, leaf) -> do
      res <- runInIO $ checkSatWithProps solvers query
      pure (res, leaf)
    pure $ fmap swap $ filter (\(res, _) -> not . isQed $ res) results
  
  showModel :: Expr Buf -> (Expr End, SMTResult) -> IO ()
  showModel cd (expr, res) = do
    case res of
      Qed -> pure () -- ignore unreachable branches
      Error e -> do
        putStrLn ""
        putStrLn "--- Branch ---"
        putStrLn $ "Error during SMT solving, cannot check branch " <> e
      Unknown reason -> do
        putStrLn ""
        putStrLn "--- Branch ---"
        putStrLn $ "Unable to produce a model for the following end state due to '" <> reason <> "' :"
        T.putStrLn $ indent 2 $ formatExpr expr
        putStrLn ""
      Cex cex -> do
        putStrLn ""
        putStrLn "--- Branch ---"
        putStrLn "Inputs:"
        T.putStrLn $ indent 2 $ formatCex cd Nothing cex
        putStrLn "End State:"
        T.putStrLn $ indent 2 $ formatExpr expr
  
  showBuffer :: (Expr Buf) -> SMTCex -> Text
  showBuffer buf cex = case Map.lookup buf cex.buffers of
    Nothing -> internalError "buffer missing in the counterexample"
    Just buffer -> case SMT.collapse buffer of
      Nothing -> T.pack $ show buffer
      Just (Flat bs) -> T.pack $ show bs
      Just (EVM.Types.Comp _) -> internalError "CompressedBuf returned from collapse"
  
  formatCex :: Expr Buf -> Maybe Sig -> SMTCex -> Text
  formatCex cd sig m@(SMTCex _ addrs _ store blockContext txContext) = T.unlines $
    [ "Calldata:", indent 2 cd' ]
    <> storeCex
    <> txCtx
    <> blockCtx
    <> addrsCex
    where
      -- we attempt to produce a model for calldata by substituting all variables
      -- and buffers provided by the model into the original calldata expression.
      -- If we have a concrete result then we display it, otherwise we display
      -- `Any`. This is a little bit of a hack (and maybe unsound?), but we need
      -- it for branches that do not refer to calldata at all (e.g. the top level
      -- callvalue check inserted by solidity in contracts that don't have any
      -- payable functions).
      cd' = case sig of
        Nothing -> case (defaultSymbolicValues $ subModel m cd) of
          Right k -> prettyBuf $ Expr.concKeccakSimpExpr k
          Left err -> T.pack err
        Just (Sig n ts) -> prettyCalldata m cd n ts
  
      storeCex :: [Text]
      storeCex
        | Map.null store = []
        | otherwise =
            [ "Storage:"
            , indent 2 $ T.unlines $ Map.foldrWithKey (\key val acc ->
                ("Addr " <> (T.pack . show $ key)
                  <> ": " <> (T.pack $ show (Map.toList val))) : acc
              ) mempty store
            ]
  
      txCtx :: [Text]
      txCtx
        | Map.null txContext = []
        | otherwise =
          [ "Transaction Context:"
          , indent 2 $ T.unlines $ Map.foldrWithKey (\key val acc ->
              (showTxCtx key <> ": " <> (T.pack $ show val)) : acc
            ) mempty (filterSubCtx txContext)
          ]
  
      addrsCex :: [Text]
      addrsCex
        | Map.null addrs = []
        | otherwise =
            [ "Addrs:"
            , indent 2 $ T.unlines $ Map.foldrWithKey (\key val acc ->
                ((T.pack . show $ key) <> ": " <> (T.pack $ show val)) : acc
              ) mempty addrs
            ]
  
      -- strips the frame arg from frame context vars to make them easier to read
      showTxCtx :: Expr EWord -> Text
      showTxCtx (TxValue) = "TxValue"
      showTxCtx x = T.pack $ show x
  
      -- strips all frame context that doesn't come from the top frame
      filterSubCtx :: Map (Expr EWord) W256 -> Map (Expr EWord) W256
      filterSubCtx = Map.filterWithKey go
        where
          go :: Expr EWord -> W256 -> Bool
          go (TxValue) _ = True
          go (Balance {}) _ = internalError "TODO: BALANCE"
          go (Gas {}) _ = internalError "TODO: Gas"
          go _ _ = False
  
      blockCtx :: [Text]
      blockCtx
        | Map.null blockContext = []
        | otherwise =
          [ "Block Context:"
          , indent 2 $ T.unlines $ Map.foldrWithKey (\key val acc ->
              (T.pack $ show key <> ": " <> show val) : acc
            ) mempty txContext
          ]
  
  prettyBuf :: Expr Buf -> Text
  prettyBuf (ConcreteBuf "") = "Empty"
  prettyBuf (ConcreteBuf bs) = formatBinary bs
  prettyBuf b = internalError $ "Unexpected symbolic buffer:\n" <> T.unpack (formatExpr b)
  
  calldataFromCex :: App m => SMTCex -> Expr Buf -> Sig -> m (Err ByteString)
  calldataFromCex cex buf sig = do
    let sigKeccak = keccakSig $ encodeUtf8 (callSig sig)
    pure $ (sigKeccak <>) <$> body
    where
      cd = defaultSymbolicValues $ subModel cex buf
      argdata = case cd of
        Right cd' -> Right $ Expr.drop 4 (Expr.simplify cd')
        Left e -> Left e
      body = forceConcrete =<< argdata
      forceConcrete :: (Expr Buf) -> Err ByteString
      forceConcrete (ConcreteBuf k) = Right k
      forceConcrete _ = Left "Symbolic buffer in calldata, cannot produce concrete model"
      keccakSig :: ByteString -> ByteString
      keccakSig = keccakBytes >>> BS.take 4
  
  prettyCalldata :: SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
  prettyCalldata cex buf sig types = headErr errSig (T.splitOn "(" sig) <> "(" <> body <> ")" <> T.pack finalErr
    where
      cd = defaultSymbolicValues $ subModel cex buf
      argdata :: Err (Expr Buf) = case cd of
        Right cd' -> Right $ Expr.drop 4 (Expr.simplify cd')
        Left e -> Left e
      (body, finalErr) = case argdata of
        Right argdata' -> case decodeBuf types argdata' of
          (CAbi v, "") -> (T.intercalate "," (fmap showVal v), "")
          (CAbi v, err) -> (T.intercalate "," (fmap showVal v), dash <> err)
          (NoVals, err) -> case argdata' of
              ConcreteBuf c -> (T.pack $ "ABI decode failed. hex calldata: 0x" <> (bsToHex c), dash <> err)
              _ -> (T.pack defaultText, dash <> err)
          (SAbi _, err) -> (T.pack defaultText, dash <> err)
        Left err -> (T.pack err, "")
      headErr e l = fromMaybe (T.pack e) $ listToMaybe l
      dash = " -- "
      defaultText = "Error: unable to produce a concrete model for calldata: " <> show buf
      errSig = "Error unable to split sig: " <> show sig
  
  -- | If the expression contains any symbolic values, default them to some
  -- concrete value The intuition here is that if we still have symbolic values
  -- in our calldata expression after substituting in our cex, then they can have
  -- any value and we can safely pick a random value. This is a bit unsatisfying,
  -- we should really be doing smth like: https://github.com/argotorg/hevm/issues/334
  -- but it's probably good enough for now
  defaultSymbolicValues :: Err (Expr a) -> Err (Expr a)
  defaultSymbolicValues = \case
      Right e -> subBufs (foldTerm symbufs mempty e)
                 . subVars (foldTerm symwords mempty e)
                 . subAddrs (foldTerm symaddrs mempty e) $ e
      Left err -> Left err
    where
      symaddrs :: Expr a -> Map (Expr EAddr) Addr
      symaddrs = \case
        a@(SymAddr _) -> Map.singleton a (Addr 0x1312)
        _ -> mempty
      symbufs :: Expr a -> Map (Expr Buf) BufModel
      symbufs = \case
        a@(AbstractBuf _) -> Map.singleton a (Flat BS.empty)
        _ -> mempty
      symwords :: Expr a -> Map (Expr EWord) W256
      symwords = \case
        a@(Var _) -> Map.singleton a 0
        a@Origin -> Map.singleton a 0
        a@Coinbase -> Map.singleton a 0
        a@Timestamp -> Map.singleton a 0
        a@BlockNumber -> Map.singleton a 0
        a@PrevRandao -> Map.singleton a 0
        a@GasLimit -> Map.singleton a 0
        a@ChainId -> Map.singleton a 0
        a@BaseFee -> Map.singleton a 0
        _ -> mempty
  
  -- | Takes an expression and a Cex and replaces all abstract values in the buf with
  -- concrete ones from the Cex.
  subModel :: SMTCex -> Expr a -> Err (Expr a)
  subModel c
    = subBufs c.buffers
    . subStores c.store
    . subVars c.vars
    . subVars c.blockContext
    . subVars c.txContext
    . subAddrs c.addrs
  
  subVars :: Map (Expr EWord) W256 -> Expr a -> Expr a
  subVars model b = Map.foldlWithKey subVar b model
    where
      subVar :: Expr a -> Expr EWord -> W256 -> Expr a
      subVar a var val = mapExpr go a
        where
          go :: Expr a -> Expr a
          go = \case
            v@(Var _) -> if v == var
                        then Lit val
                        else v
            e -> e
  
  subAddrs :: Map (Expr EAddr) Addr -> Expr a -> Expr a
  subAddrs model b = Map.foldlWithKey subAddr b model
    where
      subAddr :: Expr a -> Expr EAddr -> Addr -> Expr a
      subAddr a var val = mapExpr go a
        where
          go :: Expr a -> Expr a
          go = \case
            v@(SymAddr _) -> if v == var
                        then LitAddr val
                        else v
            e -> e
  
  subBufs :: Map (Expr Buf) BufModel -> Expr a -> Err (Expr a)
  subBufs model b = Map.foldlWithKey subBuf (Right b) model
    where
      subBuf :: Err (Expr a) -> Expr Buf -> BufModel -> Err (Expr a)
      subBuf x var val = case x of
        Right x' -> mapExprM go x'
        Left err -> Left err
        where
          go :: Expr a -> Err (Expr a)
          go = \case
            c@(AbstractBuf _) -> case c == var of
              True -> case forceFlattened val of
                Right bs -> Right $ ConcreteBuf bs
                Left err -> Left $ show c <> " --- cannot flatten buffer: " <> err
              False -> Right c
            e -> Right e
          forceFlattened :: BufModel -> Err ByteString
          forceFlattened (Flat bs) = Right bs
          forceFlattened buf@(EVM.Types.Comp _) =  case SMT.collapse buf of
            Just k -> forceFlattened k
            Nothing -> Left $ show buf
  
  subStores :: Map (Expr EAddr) (Map W256 W256) -> Expr a -> Expr a
  subStores model b = Map.foldlWithKey subStore b model
    where
      subStore :: Expr a -> Expr EAddr -> Map W256 W256 -> Expr a
      subStore x var val = mapExpr go x
        where
          go :: Expr a -> Expr a
          go = \case
            v@(AbstractStore a _)
              -> if a == var
                 then ConcreteStore val
                 else v
            e -> e
  
  getCex :: ProofResult a b -> Maybe a
  getCex (Cex c) = Just c
  getCex _ = Nothing
  