content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE OverloadedStrings #-}
  
  -- |
  -- This provides functionality for converting the
  -- architecture-independent components of @FnReop@ functions into LLVM.
  --
  -- It exports a fairly large set of capabilities so that all
  -- architecture-specific functionality can be implemented on top of this
  -- layer.
  module Reopt.CFG.LLVM (
    moduleForFunctions,
    LLVMGenOptions (..),
  
    -- * Internals for implement architecture specific functions
    LLVMArchSpecificOps (..),
    LLVMArchConstraints,
    LLVMLogEvent (..),
    LLVMLogEventInfo (..),
    LLVMBitCastInfo (..),
    llvmLogEventHeader,
    llvmLogEventToStrings,
    logEvent,
    HasValue,
    functionTypeToLLVM,
    Intrinsic,
    intrinsic,
    FunLLVMContext (archFns, funLLVMGenOptions, withArchConstraints),
    BBLLVM,
    typeToLLVMType,
    setAssignIdValue,
    padUndef,
    arithop,
    selectVal,
    convop,
    bitcast,
    band,
    bor,
    shl,
    icmpop,
    fcmpop,
    cmpsxFromSize,
    llvmAsPtr,
    llvmTrunc,
    llvmBitCast,
    extractValue,
    insertValue,
    call,
    call_,
    mkLLVMValue,
    ret,
    effect,
    AsmAttrs,
    noSideEffect,
    sideEffect,
    callAsm,
    callAsm_,
    llvmITypeNat,
    getInferredTypeBBLLVM,
    runGetInferredType,
  ) where
  
  import Control.Lens
  import Control.Monad
  import Control.Monad.Except
  import Control.Monad.Reader hiding (Reader)
  import Control.Monad.State.Strict
  import Data.Bifunctor (first)
  import Data.ByteString.Char8 qualified as BSC
  import Data.Foldable
  import Data.Int
  import Data.List
  import Data.Map.Strict (Map)
  import Data.Map.Strict qualified as Map
  import Data.Maybe (fromMaybe)
  import Data.Parameterized.Classes
  import Data.Parameterized.List qualified as PL
  import Data.Parameterized.NatRepr (widthVal, intValue)
  import Data.Parameterized.Some
  import Data.Parameterized.TraversableF
  import Data.Proxy
  import Data.Text qualified as Text
  import Data.Vector qualified as V
  import Effectful
  import Effectful.Reader.Static qualified as R
  import Data.Word
  import GHC.Stack
  import GHC.TypeLits
  
  -- NOTE: 902 means 9.2
  #if __GLASGOW_HASKELL__ < 902
  import           Numeric.Natural (Natural)
  #endif
  import Prettyprinter qualified as PP
  import Text.LLVM qualified as L
  import Text.LLVM.PP qualified as L
  import Text.LLVM.Triple.AST qualified as L
  import Text.PrettyPrint.HughesPJ qualified as HPJ
  import Text.Printf
  
  import Data.Macaw.Analysis.RegisterUse (BoundLoc (..))
  import Data.Macaw.CFG
  import Data.Macaw.Types
  import Data.Macaw.X86 (ArchitectureInfo, X86BlockPrecond (..), X86Reg (..), X86_64, archAddrWidth)
  
  import Data.Bits (testBit)
  import Reopt.CFG.FnRep
  import Reopt.Events (FunId, funId)
  import Reopt.TypeInference.ConstraintGen (
    FunctionTypeTyVars (..),
    ModuleConstraints (..),
    asFullyResolvedFunctionType,
    resolveFunctionType,
   )
  import Reopt.TypeInference.Solver (
    FTy,
    TyVar,
    tyToLLVMType,
    pattern FConflictTy,
    pattern FFunPtrTy,
    pattern FNumTy,
    pattern FPreFunPtrTy,
    pattern FPtrTy,
    pattern FUnknownFunPtrTy,
    pattern FUnknownTy,
    pattern FTupleTy,
    pattern FVecTy,
    pattern FVoidTy,
   )
  import Reopt.VCG.Annotations qualified as Ann
  import Debug.Trace (trace)
  
  data LLVMBitCastInfo = LLVMBitCastInfo
    { llvmBitCastSrcType :: L.Type
    , llvmBitCastDstType :: L.Type
    }
    deriving (Show)
  
  data LLVMLogEventInfo
    = LogInfoBitCast LLVMBitCastInfo
    | LogInfoTrunc LLVMBitCastInfo
    | LogInfoIntToPtr LLVMBitCastInfo
    | LogInfoPtrToInt LLVMBitCastInfo
    deriving (Show)
  
  data LLVMLogEvent = LLVMLogEvent
    { rLogEventContext :: String
    , rLogEventInfo :: LLVMLogEventInfo
    }
    deriving (Show)
  
  -- | Textual info acting as a "header" for the info generated by @logEventToStrings@.
  llvmLogEventHeader :: [String]
  llvmLogEventHeader = ["Reopt Source Context", "LLVM Operation", "Source LLVM Type", "Destination LLVM Type"]
  
  -- | Render a log event as segments of textual info (amicable to, e.g., CSV rendering).
  llvmLogEventToStrings :: (?config :: L.Config) => LLVMLogEvent -> [String]
  llvmLogEventToStrings e = rLogEventContext e : llvmLogInfoToStrings (rLogEventInfo e)
  
  llvmLogInfoToStrings :: (?config :: L.Config) => LLVMLogEventInfo -> [String]
  llvmLogInfoToStrings info =
    case info of
      LogInfoBitCast i -> "bitcast" : renderCastInfo i
      LogInfoTrunc i -> "trunc" : renderCastInfo i
      LogInfoIntToPtr i -> "inttoptr" : renderCastInfo i
      LogInfoPtrToInt i -> "ptrtoint" : renderCastInfo i
   where
    renderCastInfo :: LLVMBitCastInfo -> [String]
    renderCastInfo (LLVMBitCastInfo src dst) = [HPJ.render $ L.ppType src, HPJ.render $ L.ppType dst]
  
  -- | Return a LLVM type for a integer with the given width.
  llvmITypeNat :: Natural -> L.Type
  llvmITypeNat w
    | w <= fromIntegral (maxBound :: Word32) = L.PrimType (L.Integer wn)
    | otherwise = error $ "llvmITypeNat given bad width " ++ show w
   where
    wn :: Word32
    wn = fromIntegral w
  
  natReprToLLVMType :: NatRepr n -> L.Type
  natReprToLLVMType = llvmITypeNat . natValue
  
  ------------------------------------------------------------------------
  -- HasValue
  
  class HasValue v where
    valueOf :: v -> L.Typed L.Value
  
  instance HasValue (L.Typed L.Value) where
    valueOf = id
  
  ------------------------------------------------------------------------
  -- Intrinsic
  
  -- | An LLVM intrinsic
  data Intrinsic = Intrinsic
    { intrinsicName :: !L.Symbol
    , intrinsicRes :: L.Type
    , intrinsicArgs :: [L.Type]
    , intrinsicAttrs :: [L.FunAttr]
    }
  
  instance HasValue Intrinsic where
    valueOf i = L.Typed tp (L.ValSymbol (intrinsicName i))
     where
      tp = L.ptrT $ L.FunTy (intrinsicRes i) (intrinsicArgs i) False
  
  -- | Define an intrinsic that has no special attributes
  intrinsic :: String -> L.Type -> [L.Type] -> Intrinsic
  intrinsic name res args = intrinsic' name res args []
  
  -- | Define an intrinsic that has no special attributes
  intrinsic' :: String -> L.Type -> [L.Type] -> [L.FunAttr] -> Intrinsic
  intrinsic' name res args attrs =
    Intrinsic
      { intrinsicName = L.Symbol name
      , intrinsicRes = res
      , intrinsicArgs = args
      , intrinsicAttrs = attrs
      }
  
  --------------------------------------------------------------------------------
  -- LLVM intrinsics
  --------------------------------------------------------------------------------
  
  -- | LLVM arithmetic with overflow intrinsic.
  overflowOp :: (?config :: L.Config) => String -> L.Type -> Intrinsic
  overflowOp bop in_typ =
    intrinsic
      ("llvm." ++ bop ++ ".with.overflow." ++ show (L.ppType in_typ))
      (L.Struct [in_typ, L.iT 1])
      [in_typ, in_typ]
  
  type VectorLength = Word64
  
  -- | @llvm.masked.load.*@ intrinsic
  llvmMaskedLoad ::
    -- | Number of vector elements
    VectorLength ->
    -- | Type name (e.g. i32)
    String ->
    -- | Element type (should match string)
    L.Type ->
    Intrinsic
  llvmMaskedLoad n tp tpv = do
    let
      vstr = "v" ++ show n ++ tp
      mnem = "llvm.masked.load." ++ vstr ++ ".p0" ++ vstr
      args = [L.PtrTo (L.Vector n tpv), L.iT 32, L.Vector n (L.iT 1), L.Vector n tpv]
     in
      intrinsic mnem (L.Vector n tpv) args
  
  -- | @llvm.masked.store.*@ intrinsic
  llvmMaskedStore ::
    -- | Number of vector elements
    VectorLength ->
    -- | Type name (e.g. i32)
    String ->
    -- | Element type (should match string)
    L.Type ->
    Intrinsic
  llvmMaskedStore n tp tpv = do
    let
      vstr = "v" ++ show n ++ tp
      mnem = "llvm.masked.store." ++ vstr ++ ".p0" ++ vstr
      args = [L.PtrTo (L.Vector n tpv), L.iT 32, L.Vector n (L.iT 1), L.Vector n tpv]
     in
      intrinsic mnem (L.Vector n tpv) args
  
  llvmIntrinsics :: (?config :: L.Config) => [Intrinsic]
  llvmIntrinsics =
    [ overflowOp bop in_typ
    | bop <- ["uadd", "sadd", "usub", "ssub"]
    , in_typ <- map L.iT [4, 8, 16, 32, 64]
    ]
      ++ [ intrinsic ("llvm." ++ uop ++ "." ++ show (L.ppType typ)) typ [typ, L.iT 1]
         | uop <- ["cttz", "ctlz"]
         , typ <- map L.iT [8, 16, 32, 64]
         ]
  
  --------------------------------------------------------------------------------
  -- conversion to LLVM
  --------------------------------------------------------------------------------
  
  -- The type of FP arguments and results.  We actually want fp128, but
  -- it looks like llvm (at least as of version 3.6.2) doesn't put fp128
  -- into xmm0 on a return, whereas it does for <2 x double>
  
  llvmFloatType :: FloatInfoRepr flt -> L.FloatType
  llvmFloatType flt =
    case flt of
      HalfFloatRepr -> L.Half
      SingleFloatRepr -> L.Float
      DoubleFloatRepr -> L.Double
      QuadFloatRepr -> L.Fp128
      X86_80FloatRepr -> L.X86_fp80
  
  typeToLLVMType :: TypeRepr tp -> L.Type
  typeToLLVMType BoolTypeRepr = L.iT 1
  typeToLLVMType (BVTypeRepr n) = llvmITypeNat (natValue n)
  typeToLLVMType (FloatTypeRepr flt) = L.PrimType $ L.FloatType $ llvmFloatType flt
  typeToLLVMType (TupleTypeRepr s) = L.Struct (toListFC typeToLLVMType s)
  typeToLLVMType (VecTypeRepr w tp)
    | toInteger (natValue w) <= toInteger (maxBound :: Int32) =
        L.Vector (fromIntegral (natValue w)) (typeToLLVMType tp)
    | otherwise = error $ "Vector width of " ++ show w ++ " is too large."
  
  -- | This is a special label used for switch statement defaults.
  --
  -- We should never actually reach these blocks, and with some
  -- additional analysis we can probably eliminate the need for ever
  -- generating them, however at the moment we use them.
  switchFailLabel :: String
  switchFailLabel = "failure"
  
  -- | Block for fail label.
  failBlock :: L.BasicBlock
  failBlock =
    L.BasicBlock
      { L.bbLabel = Just $ L.Named $ L.Ident switchFailLabel
      , L.bbStmts = [L.Effect L.Unreachable []]
      }
  
  ------------------------------------------------------------------------
  -- Return handing
  
  -- | Get LLVM type for a function that returns the given values.
  llvmFunctionReturnType :: FunctionType arch -> L.Type
  llvmFunctionReturnType ftp =
    case fnReturnType ftp of
      Nothing -> L.PrimType L.Void
      Just (Some rtp) -> typeToLLVMType rtp
  
  ------------------------------------------------------------------------
  
  functionTypeToLLVM :: FunctionType arch -> L.Type
  functionTypeToLLVM ft =
    L.ptrT $
      L.FunTy
        (llvmFunctionReturnType ft)
        (viewSome typeToLLVMType <$> fnArgTypes ft)
        (fnVarArgs ft)
  
  -- FIXME
  functionTypeToLLVM' ::
    forall arch.
    LLVMArchConstraints arch =>
    FunctionType arch ->
    [Maybe FTy] ->
    Maybe (Maybe FTy) ->
    L.Type
  functionTypeToLLVM' ft args m_ret =
    L.ptrT $
      L.FunTy
        (fromMaybe (L.PrimType L.Void) m_ret')
        (zipWith mkTy (viewSome typeToLLVMType <$> fnArgTypes ft) args)
        (fnVarArgs ft)
   where
    m_ret' = mkTy <$> (viewSome typeToLLVMType <$> fnReturnType ft) <*> m_ret
  
    mkTy lty = maybe lty (tyToLLVMType ptrWidth)
    ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
  
  declareFunction ::
    FunctionDecl arch ->
    L.Declare
  declareFunction d =
    let ftp = funDeclType d
     in L.Declare
          { L.decLinkage = Nothing
          , L.decVisibility = Nothing
          , L.decRetType = llvmFunctionReturnType ftp
          , L.decName = L.Symbol (BSC.unpack (funDeclName d))
          , L.decArgs = viewSome typeToLLVMType <$> fnArgTypes ftp
          , L.decVarArgs = fnVarArgs ftp
          , L.decAttrs = []
          , L.decComdat = Nothing
          }
  
  -- Pads the given list of values to be the target lenght using undefs
  padUndef :: L.Type -> Int -> [L.Typed L.Value] -> [L.Typed L.Value]
  padUndef typ len xs = xs ++ replicate (len - length xs) (L.Typed typ L.ValUndef)
  
  -- | Result obtained by printing a block to LLVM
  data LLVMBlockResult arch = LLVMBlockResult
    { fnBlock :: !(FnBlock arch)
    -- ^ Fn block to create this.
    , llvmPhiVars :: !(V.Vector (PhiBinding arch))
    -- ^ Vector phi variables
    , finalBBState :: !(BBLLVMState arch)
    }
  
  -- | Maps each block label to the number of times a value should be repeated and the value.
  --
  -- The number of repetitions should be positive and needed because LLVM needs a separate phi
  -- value for each incoming edge even if they are from the same block.  Edges from the same block
  -- must have the same value.
  type PhiValues = Map L.BlockLabel (Int, L.Value)
  
  -- | A vector with an element for each phi variable in a block.
  type BlockPhiAssignment = V.Vector PhiValues
  
  -- | Maps LLVM blocks to the phi assignment for them.
  type ResolvePhiMap w = Map (FnBlockLabel w) BlockPhiAssignment
  
  -- | Create an initial phi map from the function.
  --
  -- This does not propagate values.
  initResolvePhiMap :: Function arch -> ResolvePhiMap (ArchAddrWidth arch)
  initResolvePhiMap f =
    Map.fromList
      [ (fbLabel b, V.replicate phiCnt Map.empty)
      | b <- fnBlocks f
      , let phiCnt = V.length (fbPhiVars b)
      ]
  
  -- | Return the phi assignment associated with the given target label.
  --
  -- Note. This needs the expected number of phi variables in case
  -- the phi variables have not yet been initialized.
  phiAssignmentForBlock ::
    ResolvePhiMap w ->
    FnBlockLabel w ->
    BlockPhiAssignment
  phiAssignmentForBlock m l =
    Map.findWithDefault (error emsg) l m
   where
    emsg = "Could not find phi assignment."
  
  -- | This is used for resolving type mismatch due to subtyping when
  -- doing a block transfer.
  type PhiMap arch = Map (FnBlockLabel (ArchAddrWidth arch)) (V.Vector (Some (FnPhiVar arch)))
  
  phiMapFromFunction :: Function arch -> PhiMap arch
  phiMapFromFunction f = Map.fromList [(fbLabel b, fbPhiVars b) | b <- fnBlocks f]
  
  ------------------------------------------------------------------------
  -- IntrinsicMap
  
  -- | Map from intrinsic name to intrinsic seen so far
  --
  -- Globally maintained when translating model so that we know which
  -- definitions to include.
  type IntrinsicMap = Map L.Symbol Intrinsic
  
  ------------------------------------------------------------------------
  -- FunStateAnn
  
  -- | Map from assign ID to LLVM value
  type AssignValMap = Map FnAssignId (L.Typed L.Value)
  
  -- | State relative to a function.
  data FunState arch = FunState
    { nmCounter :: !Int
    -- ^ Counter for generating new identifiers
    , funIntrinsicMap :: !IntrinsicMap
    -- ^ Collection used for tracking which intrinsics we need.
    , needSwitchFailLabel :: !Bool
    -- ^ Flag that indicates if we need the fail block for a
    -- switch statement.
    , funBlockPhiMap :: !(ResolvePhiMap (ArchAddrWidth arch))
    -- ^ Maps blocks to the phi nodes for that block.
    }
  
  funIntrinsicMapLens :: Simple Lens (FunState arch) IntrinsicMap
  funIntrinsicMapLens = lens funIntrinsicMap (\s v -> s{funIntrinsicMap = v})
  
  funBlockPhiMapLens :: Lens' (FunState arch) (ResolvePhiMap (ArchAddrWidth arch))
  funBlockPhiMapLens = lens funBlockPhiMap (\s v -> s{funBlockPhiMap = v})
  
  ------------------------------------------------------------------------
  -- Functions for creating LLVM identifiers.
  
  tempIdent :: Int -> L.Ident
  tempIdent c = L.Ident ('t' : show c)
  
  ------------------------------------------------------------------------
  -- LLVMGEneration options
  
  -- | Options for generating LLVM
  newtype LLVMGenOptions = LLVMGenOptions
    { mcExceptionIsUB :: Bool
    -- ^ Code with side effects is allowed to result in
    -- LLVM undefined behavior if machine code would
    -- have raised an exception.
    }
  
  ------------------------------------------------------------------------
  -- BBLLVM
  
  -- | Architecture-specific operations for generating LLVM
  data LLVMArchSpecificOps arch = LLVMArchSpecificOps
    { archEndianness :: !Endianness
    -- ^ Endianness of architecture
    --
    -- Some architectures allow endianness to change dynamically,
    -- Macaw does not support this.
    , archFnCallback ::
        !( forall tp.
           ArchFn arch (FnValue arch) tp ->
           BBLLVM arch (L.Typed L.Value)
         )
    -- ^ Callback for architecture-specific functions
    , archStmtCallback :: !(FnArchStmt arch (FnValue arch) -> BBLLVM arch ())
    -- ^ Callback for architecture-specific statements
    , popCountCallback ::
        !( forall w.
           NatRepr w ->
           FnValue arch (BVType w) ->
           BBLLVM arch (L.Typed L.Value)
         )
    -- ^ Callback for emitting a popcount instruction
    --
    -- This is architecture-specific so that we can choose machine code.
    }
  
  type LLVMArchConstraints arch =
    ( FnArchConstraints arch
    , ShowF (ArchReg arch)
    , OrdF (ArchReg arch)
    , IsArchStmt (FnArchStmt arch)
    , Eq (FunctionType arch)
    )
  
  -- | Information used to generate LLVM for a specific function.
  --
  -- This information is the same for all blocks within the function.
  data FunLLVMContext arch = FunLLVMContext
    { archInfo :: !(ArchitectureInfo arch)
    , archFns :: !(LLVMArchSpecificOps arch)
    -- ^ Architecture-specific functions
    , funLLVMGenOptions :: !LLVMGenOptions
    -- ^ Options for generating LLVM
    , funAddr :: ArchSegmentOff arch
    , funName :: BSC.ByteString
    , funArgs :: !(V.Vector (L.Typed L.Value))
    -- ^ Arguments to this function.
    , funRetType :: !(Maybe (Maybe FTy))
    -- ^ Return for this function
    , funAllocaCount :: !Int
    , moduleConstraints :: ModuleConstraints arch
    , funBlockPhis :: !(PhiMap arch)
    -- ^ Typing constraints inferred for the module
    , withArchConstraints :: forall a. (LLVMArchConstraints arch => a) -> a
    }
  
  -- | State specific to translating a single basic block.
  data BBLLVMState arch = BBLLVMState
    { bbThisLabel :: !L.BlockLabel
    -- ^ The label for the block we are translating
    , bbAssignValMap :: !AssignValMap
    -- ^ Map assignment ids created in this block to the LLVM value.
    , bbStmts :: ![L.Stmt]
    -- ^ Statements added so far with last statement at head of list.
    , bbLLVMLogEvents :: ![LLVMLogEvent]
    }
  
  data BBLLVMPair arch = BBLLVMPair
    { funState :: !(FunState arch)
    , bbLLVMState :: !(BBLLVMState arch)
    }
  
  funStateLens :: Simple Lens (BBLLVMPair arch) (FunState arch)
  funStateLens = lens funState (\s v -> s{funState = v})
  
  newtype BBLLVM arch a = BBLLVM {unBBLLVM :: ReaderT (FunLLVMContext arch) (State (BBLLVMPair arch)) a}
    deriving
      ( Functor
      , Applicative
      , Monad
      , MonadReader (FunLLVMContext arch)
      )
  
  instance MonadState (BBLLVMState arch) (BBLLVM arch) where
    get = BBLLVM $ bbLLVMState <$> get
    put s = BBLLVM $ modify $ \t -> t{bbLLVMState = s}
  
  logEvent :: LLVMLogEvent -> BBLLVM arch ()
  logEvent e = modify' $ \bs -> bs{bbLLVMLogEvents = e : bbLLVMLogEvents bs}
  
  -- | Generate a fresh identifier with the name 'rX'
  freshName :: BBLLVM arch L.Ident
  freshName = BBLLVM $ do
    c <- uses funStateLens nmCounter
    modify' $ funStateLens %~ \fs -> fs{nmCounter = c + 1}
    pure $! tempIdent c
  
  addIntrinsic :: Intrinsic -> BBLLVM arch ()
  addIntrinsic i = BBLLVM $ do
    m <- use $ funStateLens . funIntrinsicMapLens
    when (Map.notMember (intrinsicName i) m) $ do
      funStateLens . funIntrinsicMapLens .= Map.insert (intrinsicName i) i m
  
  markNeedSwitchFailLabel :: BBLLVM arch ()
  markNeedSwitchFailLabel = BBLLVM $ do
    funStateLens %= \s -> s{needSwitchFailLabel = True}
  
  -- | Append a statement to the list of statements
  emitStmt :: L.Stmt -> BBLLVM arch ()
  emitStmt stmt = seq stmt $ do
    s <- get
    put $! s{bbStmts = stmt : bbStmts s}
  
  -- | Evaluate an instruction and return the result.
  evalInstr :: L.Instr -> BBLLVM arch L.Value
  evalInstr i = do
    nm <- freshName
    emitStmt $! L.Result nm i []
    pure $! L.ValIdent nm
  
  -- | Emit an instruction as an effect
  effect :: L.Instr -> BBLLVM arch ()
  effect i = emitStmt $ L.Effect i []
  
  -- | Add a comment instruction
  comment :: String -> BBLLVM arch ()
  comment msg = effect (L.Comment msg)
  
  ret :: L.Typed L.Value -> BBLLVM arch ()
  ret = effect . L.Ret
  
  -- | Conditional expression, i.e. a series of if-then pairs
  -- and a final else/default value if no test is true.
  selectVal ::
    -- | Overall result type.
    L.Type ->
    -- | Test expressions and associated results.
    [(L.Typed L.Value, L.Typed L.Value)] ->
    -- | If no test expressions evaluate to true, return this value.
    L.Typed L.Value ->
    BBLLVM arch (L.Typed L.Value)
  selectVal resTy ifThens elseVal = do
    L.Typed resTy <$> foldM addClause (L.typedValue elseVal) ifThens
   where
    addClause acc (test, res) = evalInstr $ L.Select test res acc
  
  unimplementedInstr' :: L.Type -> String -> BBLLVM arch (L.Typed L.Value)
  unimplementedInstr' typ reason = do
    comment ("UNIMPLEMENTED: " ++ reason)
    return (L.Typed typ L.ValUndef)
  
  -- | Sets the value of the function assign id.
  setAssignIdValue ::
    HasCallStack =>
    FnAssignId ->
    L.Typed L.Value ->
    BBLLVM arch ()
  setAssignIdValue fid v = do
    m <- gets bbAssignValMap
    case Map.lookup fid m of
      Just{} -> error $ "internal: Assign id " ++ show (PP.pretty fid) ++ " already assigned."
      Nothing -> pure ()
    modify' $ \s -> s{bbAssignValMap = Map.insert fid v (bbAssignValMap s)}
  
  ------------------------------------------------------------------------
  -- Convert a value to LLVM
  
  -- | Map a function value to a LLVM value with no change.
  valueToLLVM ::
    forall arch tp.
    HasCallStack =>
    -- | Context
    FunLLVMContext arch ->
    -- | Map from assignment ids to value.
    AssignValMap ->
    FnValue arch tp ->
    BBLLVM arch (L.Typed L.Value)
  valueToLLVM ctx avmap val = withArchConstraints ctx $ do
    aInfo <- asks archInfo
    let ptrWidth = addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
    case val of
      -- A value that is actually undefined, like a non-argument register at
      -- the start of a function.
      FnUndefined typ -> pure $ L.Typed (typeToLLVMType typ) L.ValUndef
      FnConstantBool b -> pure $ L.Typed (L.iT 1) $ L.integer (if b then 1 else 0)
      -- ptr sized things are handled elsewhere (FnAddrWidthConstant)
      FnConstantValue sz n -> pure $ L.Typed (natReprToLLVMType sz) $ L.integer n
      -- Value from an assignment statement.
      FnAssignedValue (FnAssignment lhs _rhs) ->
        case Map.lookup lhs avmap of
          Just v -> pure v
          Nothing ->
            error $ "Could not find assignment value " ++ show (PP.pretty lhs)
      -- Value from a phi node
      FnPhiValue phiVar -> do
        case Map.lookup (unFnPhiVar phiVar) avmap of
          Just v -> pure v
          Nothing ->
            error $ "Could not find phi value " ++ show (unFnPhiVar phiVar)
      -- A value returned by a function call (rax/xmm0)
      FnReturn (FnReturnVar lhs _tp) ->
        case Map.lookup lhs avmap of
          Just v -> pure v
          Nothing ->
            error $ "Could not find return variable " ++ show (PP.pretty lhs)
      -- The entry pointer to a function.  We do the cast as a const expr as
      -- function addresses appear as constants in e.g. phi nodes
      FnFunctionEntryValue ftp nm -> do
        let typ = natReprToLLVMType ptrWidth
        let
          fptr :: L.Typed L.Value
          fptr = L.Typed (functionTypeToLLVM ftp) (L.ValSymbol (L.Symbol (BSC.unpack nm)))
        logEvent $
          LLVMLogEvent "FnFunctionEntryValue" $
            LogInfoPtrToInt $
              LLVMBitCastInfo (L.typedType fptr) typ
        pure $ L.Typed typ $ L.ValConstExpr (L.ConstConv L.PtrToInt fptr typ)
      -- Value is an argument passed via a register.
      FnArg i _tp
        | 0 <= i, i < V.length (funArgs ctx) -> pure $ funArgs ctx V.! i
        | otherwise -> error $ "Illegal argument index " ++ show i
      FnCodePointer addr -> do
        let
          ty =
            L.ptrT $
              L.FunTy
                L.Opaque -- TODO
                [] -- TODO
                False
          -- FIXME: should use the base and the offset
          value =
            L.ValConstExpr $
              L.ConstConv
                L.IntToPtr
                ( L.Typed
                    (L.PrimType (L.Integer (fromInteger (8 * toInteger (addrWidthReprByteCount (archAddrWidth aInfo))))))
                    (L.ValInteger (toInteger (segoffOffset addr)))
                )
                ty
        return $ L.Typed ty value
      FnTypedCodePointer addr fty -> do
        let
          ty = functionTypeToLLVM fty
          -- FIXME: should use the base and the offset
          value =
            L.ValConstExpr $
              L.ConstConv
                L.IntToPtr
                ( L.Typed
                    (L.PrimType (L.Integer (fromInteger (8 * toInteger (addrWidthReprByteCount (archAddrWidth aInfo))))))
                    (L.ValInteger (toInteger (addrOffset addr)))
                )
                ty
        return $ L.Typed ty value
  
  mkLLVMValue ::
    HasCallStack =>
    FnValue arch tp ->
    BBLLVM arch (L.Typed L.Value)
  mkLLVMValue val = do
    ctx <- ask
    m <- gets bbAssignValMap
    valueToLLVM ctx m val
  
  arithop :: L.ArithOp -> L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  arithop f val s = L.Typed (L.typedType val) <$> evalInstr (L.Arith f val s)
  
  bitop :: L.BitOp -> L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  bitop f val s = L.Typed (L.typedType val) <$> evalInstr (L.Bit f val s)
  
  -- | Conversion operation
  convop :: L.ConvOp -> L.Typed L.Value -> L.Type -> BBLLVM arch (L.Typed L.Value)
  convop f val tp = L.Typed tp <$> evalInstr (L.Conv f val tp)
  
  -- | Compare two LLVM integer values using the given operator.
  icmpop :: L.ICmpOp -> L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  icmpop f val s = do
    L.Typed (L.iT 1) <$> evalInstr (L.ICmp f val s)
  
  -- | Compare two LLVM float values using the given operator.
  fcmpop :: L.FCmpOp -> L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  fcmpop f val s = do
    L.Typed (L.iT 1) <$> evalInstr (L.FCmp f val s)
  
  -- | Given a byte size, return the appropriate mnemonic, i.e.,
  -- one of `cmpsb` (1), `cmpsw` (2), `cmpsd` (4), or `cmpsq` (8).
  cmpsxFromSize :: Integer -> Maybe String
  cmpsxFromSize 1 = Just "cmpsb"
  cmpsxFromSize 2 = Just "cmpsw"
  cmpsxFromSize 4 = Just "cmpsd"
  cmpsxFromSize 8 = Just "cmpsq"
  cmpsxFromSize _ = Nothing
  
  -- | Extract a value from a struct
  extractValue :: L.Typed L.Value -> Int32 -> BBLLVM arch (L.Typed L.Value)
  extractValue ta i = do
    let etp = case L.typedType ta of
          L.Struct fl -> fl !! fromIntegral i
          L.Array _l etp' -> etp'
          _ -> error "extractValue not given a struct or array."
    L.Typed etp <$> evalInstr (L.ExtractValue ta [i])
  
  -- | Insert a valiue into an aggregate
  insertValue ::
    -- | Aggregate
    L.Typed L.Value ->
    -- | Value to insert
    L.Typed L.Value ->
    -- | Index to insert
    Int32 ->
    BBLLVM arch (L.Typed L.Value)
  insertValue ta tv i =
    L.Typed (L.typedType ta) <$> evalInstr (L.InsertValue ta tv [i])
  
  -- | Do a bitcast
  bitcast :: L.Typed L.Value -> L.Type -> BBLLVM arch (L.Typed L.Value)
  bitcast = convop L.BitCast
  
  -- | Unsigned extension
  zext :: L.Typed L.Value -> L.Type -> BBLLVM arch (L.Typed L.Value)
  zext = convop L.ZExt
  
  band :: L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  band = bitop L.And
  
  -- | Bitwise inclusive  or
  bor :: L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  bor = bitop L.Or
  
  bxor :: L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  bxor = bitop L.Xor
  
  shl :: L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  shl = bitop (L.Shl False False)
  
  ashr :: L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  ashr = bitop (L.Ashr False)
  
  lshr :: L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)
  lshr = bitop (L.Lshr False)
  
  -- | Generate a non-tail call that returns a value
  call ::
    (HasCallStack, HasValue v) =>
    v ->
    [L.Typed L.Value] ->
    BBLLVM arch (L.Typed L.Value)
  call (valueOf -> f) args =
    case L.typedType f of
      L.PtrTo (L.FunTy res _argTypes _varArgs) -> do
        case res of
          L.PrimType L.Void ->
            error "call: expected to return a value, but returns void."
          _ ->
            L.Typed res <$> evalInstr (L.Call False res (L.typedValue f) args)
      _ -> error $ "call: given non-function pointer argument:\n" ++ show f
  
  -- | Generate a non-tail call that does not return a value
  call_ :: HasValue v => v -> [L.Typed L.Value] -> BBLLVM arch ()
  call_ (valueOf -> f) args =
    case L.typedType f of
      L.PtrTo (L.FunTy (L.PrimType L.Void) _argTypes _varArgs) -> do
        effect $ L.Call False (L.typedType f) (L.typedValue f) args
      _ -> error $ "call_: given non-function pointer argument\n" ++ show f
  
  -- | Sign extend a boolean value to the given width.
  carryValue ::
    (HasCallStack, 1 <= w) =>
    NatRepr w ->
    FnValue arch BoolType ->
    BBLLVM arch (L.Typed L.Value)
  carryValue w x = do
    val <- mkLLVMValue x
    if natValue w == 1
      then pure val
      else zext val (llvmITypeNat (natValue w))
  
  -- | Handle an intrinsic overflows
  intrinsicOverflows ::
    HasCallStack =>
    (?config :: L.Config) =>
    1 <= w =>
    String ->
    FnValue arch (BVType w) ->
    FnValue arch (BVType w) ->
    FnValue arch BoolType ->
    BBLLVM arch (L.Typed L.Value)
  -- Special case where carry/borrow flag is 0.
  intrinsicOverflows bop x y (FnConstantBool False) = do
    x' <- mkLLVMValue x
    y' <- mkLLVMValue y
    let in_typ = L.typedType x'
    r_tuple <- call (overflowOp bop in_typ) [x', y']
    extractValue r_tuple 1
  -- General case involves two calls
  intrinsicOverflows bop x y c = bbArchConstraints $ do
    x' <- mkLLVMValue x
    y' <- mkLLVMValue y
    let in_typ = L.typedType x'
    r_tuple <- call (overflowOp bop in_typ) [x', y']
    r <- extractValue r_tuple 0
    overflows <- extractValue r_tuple 1
    -- Check for overflow in carry flag
    c' <- carryValue (typeWidth x) c
    r_tuple' <- call (overflowOp bop in_typ) [r, c']
    overflows' <- extractValue r_tuple' 1
    bor overflows (L.typedValue overflows')
  
  appToLLVM ::
    forall arch tp.
    (?config :: L.Config) =>
    HasCallStack =>
    -- | Value being assigned
    FnAssignId ->
    App (FnValue arch) tp ->
    BBLLVM arch (L.Typed L.Value)
  appToLLVM lhs app = bbArchConstraints $ do
    let typ = typeToLLVMType $ typeRepr app
    let
      binop ::
        (L.Typed L.Value -> L.Value -> BBLLVM arch (L.Typed L.Value)) ->
        FnValue arch utp ->
        FnValue arch utp ->
        BBLLVM arch (L.Typed L.Value)
      binop f x y = do
        x' <- mkLLVMValue x
        y' <- mkLLVMValue y
        f x' (L.typedValue y')
    case app of
      Eq x y -> binop (icmpop L.Ieq) x y
      Mux _tp c t f -> do
        l_c <- mkLLVMValue c
        l_t <- mkLLVMValue t
        l_f <- mkLLVMValue f
        fmap (L.Typed (L.typedType l_t)) $ evalInstr $ L.Select l_c l_t (L.typedValue l_f)
      AndApp x y -> binop band x y
      OrApp x y -> binop bor x y
      NotApp x -> do
        -- x = 0 == complement x, according to LLVM manual.
        llvmX <- mkLLVMValue x
        icmpop L.Ieq llvmX (L.ValInteger 0)
      XorApp x y -> binop bxor x y
      -- Construct a tuple from fields.
      MkTuple fieldTypes fields -> do
        let structType = L.Struct (toListFC typeToLLVMType fieldTypes)
        let initUndef = L.Typed structType L.ValUndef
        let
          f ::
            forall utp.
            FnValue arch utp ->
            (Int32 -> L.Typed L.Value -> BBLLVM arch (L.Typed L.Value)) ->
            (Int32 -> L.Typed L.Value -> BBLLVM arch (L.Typed L.Value))
          f fld c i s = do
            llvmFieldValue <- mkLLVMValue fld
            s' <- insertValue s llvmFieldValue i
            c (i + 1) s'
        foldrFC f (\_ r -> pure r) fields 0 initUndef
      -- :: !(P.List TypeRepr l) -> !(f (TupleType l)) -> !(P.Index l r) -> App f r
      TupleField _fieldTypes macawStruct idx -> do
        -- Make a struct
        llvmStruct <- mkLLVMValue macawStruct
        -- Get index as an Int32
        let
          idxVal :: Integer
          idxVal = PL.indexValue idx
        when (idxVal >= toInteger (maxBound :: Int32)) $
          error $
            "Index out of range " ++ show idxVal ++ "."
        -- Extract a value
        extractValue llvmStruct (fromInteger idxVal :: Int32)
      ExtractElement fldType vec idx -> do
        let llvmFldType = typeToLLVMType fldType
        llvmVec <- mkLLVMValue vec
        let llvmIdx = L.ValInteger (toInteger idx)
        L.Typed llvmFldType <$> evalInstr (L.ExtractElt llvmVec llvmIdx)
      InsertElement vecType vec idx val -> do
        let llvmVecType = typeToLLVMType vecType
        llvmVec <- mkLLVMValue vec
        llvmVal <- mkLLVMValue val
        let llvmIdx = L.ValInteger (toInteger idx)
        L.Typed llvmVecType <$> evalInstr (L.InsertElt llvmVec llvmVal llvmIdx)
      Trunc v sz -> mkLLVMValue v >>= \u -> llvmTrunc "appToLLVM" u (natReprToLLVMType sz)
      SExt v sz -> mkLLVMValue v >>= \u -> convop L.SExt u (natReprToLLVMType sz)
      UExt v sz -> mkLLVMValue v >>= \u -> convop L.ZExt u (natReprToLLVMType sz)
      Bitcast x tp -> do
        llvmVal <- mkLLVMValue x
        llvmBitCast "appToLLVM" llvmVal (typeToLLVMType (widthEqTarget tp))
      BVAdd _sz x y -> do
        typeOfResult <- getInferredTypeForAssignIdBBLLVM lhs
        tx <- getInferredTypeBBLLVM x
        ty <- getInferredTypeBBLLVM y
        ptrWidth <- getPtrWidth'
  
        case (typeOfResult, tx, ty) of
          (_, Just (FPtrTy _), Just (FPtrTy _)) ->
            error "Inferred a pointer type for both addends, this suggests a bug in the constraint generation/solving!"
          (Just lhsty@(FPtrTy _), Just FPtrTy{}, Just FNumTy{})
            | FnAssignedValue FnAssignment{fnAssignRhs = FnAddrWidthConstant o} <- y ->
                bvAddPtrOffset (tyToLLVMType ptrWidth lhsty) x o
            | otherwise -> bvAddPtrSymbolic (tyToLLVMType ptrWidth lhsty) x y
          (Just lhsty@(FPtrTy _), Just FNumTy{}, Just FPtrTy{})
            | FnAssignedValue FnAssignment{fnAssignRhs = FnAddrWidthConstant o} <- x ->
                bvAddPtrOffset (tyToLLVMType ptrWidth lhsty) y o
            | otherwise -> bvAddPtrSymbolic (tyToLLVMType ptrWidth lhsty) y x
          (_, Just FPtrTy{}, _) -> error "BUG: Expecting a ptr return ty"
          (_, _, Just FPtrTy{}) -> error "BUG: Expecting a ptr return ty"
          -- If the result ought to be a pointer, but we have no idea which of the
          -- two arguments is the pointer, we must perform a bitvector add, but
          -- then cast the result into the appropriate pointer type that will be
          -- expected by the rest of the code.
          (Just (FPtrTy pointee), _, _) -> do
            result <- binop (arithop (L.Add False False)) x y
            let pty = L.PtrTo (tyToLLVMType ptrWidth pointee)
            logEvent $
              LLVMLogEvent "BVAdd(ptr_result)" $
                LogInfoIntToPtr $
                  LLVMBitCastInfo (L.typedType result) pty
            convop L.IntToPtr result pty
          _ -> binop (arithop (L.Add False False)) x y
      BVAdc _sz x y (FnConstantBool False) -> do
        binop (arithop (L.Add False False)) x y
      BVAdc _sz x y c -> do
        r <- binop (arithop (L.Add False False)) x y
        arithop (L.Add False False) r . L.typedValue =<< carryValue (typeWidth x) c
      BVSub _sz x y -> do
        typeOfResult <- getInferredTypeForAssignIdBBLLVM lhs
        tx <- getInferredTypeBBLLVM x
        ty <- getInferredTypeBBLLVM y
        ptrWidth <- getPtrWidth'
  
        case (typeOfResult, tx, ty) of
          (_, Just (FPtrTy _), Just (FPtrTy _)) -> bvSubPtrPtr x y
          (Just (FPtrTy lhsty), Just FPtrTy{}, Just FNumTy{}) ->
            bvSubPtrNum (tyToLLVMType ptrWidth lhsty) x . L.typedValue =<< mkLLVMValue y
          _ -> binop (arithop (L.Sub False False)) x y
      BVSbb _sz x y (FnConstantBool False) -> do
        binop (arithop (L.Sub False False)) x y
      BVSbb _sz x y b -> do
        d <- binop (arithop (L.Sub False False)) x y
        arithop (L.Sub False False) d . L.typedValue =<< carryValue (typeWidth x) b
      BVMul _sz x y -> binop (arithop (L.Mul False False)) x y
      BVUnsignedLt x y -> binop (icmpop L.Iult) x y
      BVUnsignedLe x y -> binop (icmpop L.Iule) x y
      BVSignedLt x y -> binop (icmpop L.Islt) x y
      BVSignedLe x y -> binop (icmpop L.Isle) x y
      BVTestBit v n -> do
        -- TODO: Test this it had a FIX comment with no details.
        llvm_v <- mkLLVMValue v
        let in_typ = L.typedType llvm_v
        n' <- mkLLVMValue n
        n_ext <-
          case compareF (typeWidth v) (typeWidth n) of
            LTF -> error "BVTestBit expected second argument to be at least first"
            EQF -> pure n'
            GTF -> zext n' in_typ
        mask <- shl (L.Typed in_typ (L.ValInteger 1)) (L.typedValue n_ext)
        r <- bitop L.And llvm_v (L.typedValue mask)
        icmpop L.Ine r (L.ValInteger 0)
      BVComplement _sz v -> do
        -- xor x -1 == complement x, according to LLVM manual.
        llvm_v <- mkLLVMValue v
        bitop L.Xor llvm_v (L.ValInteger (-1))
      BVAnd _sz x y -> binop band x y
      BVOr _sz x y -> binop bor x y
      BVXor _sz x y -> binop bxor x y
      BVShl _sz x y -> binop shl x y
      BVSar _sz x y -> binop ashr x y
      BVShr _sz x y -> binop lshr x y
      PopCount (w :: NatRepr n) v -> do
        let popCountCallbackInst ops = popCountCallback ops @n
        fn <- asks $ popCountCallbackInst . archFns
        fn w v
      ReverseBytes{} -> unimplementedInstr' typ "ReverseBytes"
      UadcOverflows x y c -> intrinsicOverflows "uadd" x y c
      SadcOverflows x y c -> intrinsicOverflows "sadd" x y c
      UsbbOverflows x y c -> intrinsicOverflows "usub" x y c
      SsbbOverflows x y c -> intrinsicOverflows "ssub" x y c
      Bsf _sz v -> do
        let cttz = intrinsic ("llvm.cttz." ++ show (L.ppType typ)) typ [typ, L.iT 1]
        v' <- mkLLVMValue v
        call cttz [v', L.iT 1 L.-: L.int 1]
      Bsr _sz v -> do
        let ctlz = intrinsic ("llvm.ctlz." ++ show (L.ppType typ)) typ [typ, L.iT 1]
        v' <- mkLLVMValue v
        call ctlz [v', L.iT 1 L.-: L.int 1]
  
  -- | Evaluate a value as a pointer (log if we need to perform a non-constant
  -- inttoptr cast).
  llvmAsPtr ::
    HasCallStack =>
    -- | Context calling this helper (for logging purposes)
    String ->
    -- | Type of value pointed to
    L.Type ->
    -- | Value to evaluate
    L.Typed L.Value -> -- FnValue arch (BVType (ArchAddrWidth arch))
    BBLLVM arch (L.Typed L.Value)
  llvmAsPtr ctx pointeeType ptrbv = do
    let pointerType = L.PtrTo pointeeType
    logEvent $
      LLVMLogEvent ctx $
        LogInfoIntToPtr $
          LLVMBitCastInfo (L.typedType ptrbv) pointerType
    convop L.IntToPtr ptrbv pointerType
  
  -- | Evaluate a value as a pointer (log if we need to perform a non-constant
  -- inttoptr cast).
  llvmPtrAsBV ::
    HasCallStack =>
    -- | Context calling this helper (for logging purposes)
    String ->
    -- | Value to evaluate
    L.Typed L.Value -> -- FnValue arch (BVType (ArchAddrWidth arch))
    BBLLVM arch (L.Typed L.Value)
  llvmPtrAsBV ctx llvmPtr = do
    ptrWidth <- getPtrWidth'
    let bvTy = L.iT (fromIntegral ptrWidth)
    logEvent $
      LLVMLogEvent ctx $
        LogInfoPtrToInt $
          LLVMBitCastInfo bvTy (L.typedType llvmPtr)
    convop L.PtrToInt llvmPtr bvTy
  
  -- | We have a bvadd which is actually taking the address of a sub-field of a structure.
  bvAddPtrOffset ::
    L.Type ->
    FnValue arch tp ->
    Integer ->
    BBLLVM arch (L.Typed L.Value)
  bvAddPtrOffset _lhsty x 0 = mkLLVMValue x
  bvAddPtrOffset lhsty x off = do
    ptrWidth <- getPtrWidth'
    if testBit off (ptrWidth - 1)
      then bvSubPtrNum lhsty x (L.integer (2 ^ ptrWidth - off))
      else ptrCase
   where
    xty' = L.PtrTo (L.Struct [L.Vector (fromInteger off) (L.iT 8), lhsty])
  
    -- We cast make x :: { <N x i8>, rhs } * so we can use a gep to get a pointer to it.
    ptrCase = do
      xV <- mkLLVMValue x
      x' <- llvmBitCast "bvAddPtrOffset" xV xty'
      llvmGEPFromPtr lhsty 1 x'
  
  -- Not much we can do here but convert to/from a bv.  We know that x
  -- is a pointer, y a number.
  bvAddPtrSymbolic ::
    L.Type ->
    FnValue arch tp ->
    FnValue arch tp' ->
    BBLLVM arch (L.Typed L.Value)
  bvAddPtrSymbolic lhsty x y = do
    x' <- llvmPtrAsBV "bvAddPtrSymbolic" =<< mkLLVMValue x
    r <- arithop (L.Add False False) x' . L.typedValue =<< mkLLVMValue y
    llvmAsPtr "bvAddPtrSymbolic" lhsty r
  
  -- | There isn't much we can do when we have ptrs, except to cast.
  bvSubPtrNum ::
    L.Type ->
    FnValue arch tp ->
    L.Value ->
    BBLLVM arch (L.Typed L.Value)
  bvSubPtrNum lhsty x rhs = do
    x' <- llvmPtrAsBV "bvAddPtrSymbolic" =<< mkLLVMValue x
    r <- arithop (L.Sub False False) x' rhs
    llvmAsPtr "bvAddPtrSymbolic" lhsty r
  
  bvSubPtrPtr ::
    FnValue arch tp ->
    FnValue arch tp' ->
    BBLLVM arch (L.Typed L.Value)
  bvSubPtrPtr x y = do
    x' <- llvmPtrAsBV "bvAddPtrSymbolic" =<< mkLLVMValue x
    y' <- llvmPtrAsBV "bvAddPtrSymbolic" =<< mkLLVMValue y
    arithop (L.Sub False False) x' (L.typedValue y')
  
  -- | This emits a getElementPointer in the special case where the value argument is a pointer.
  llvmGEPFromPtr ::
    HasCallStack =>
    L.Type ->
    Int ->
    L.Typed L.Value ->
    BBLLVM arch (L.Typed L.Value)
  llvmGEPFromPtr returnType ofs ptrV = do
    let
      pointeeType =
        case L.typedType ptrV of
          L.PtrTo ty -> ty
          ty -> error $ "llvmGEPFromPtr: expecter pointer type, got: " <> show ty
      zeroV = L.Typed (L.iT 32) (L.int 0)
      ofsV = L.Typed (L.iT 32) (L.int ofs)
    -- https://llvm.org/docs/GetElementPtr.html#what-is-the-first-index-of-the-gep-instruction
    L.Typed returnType <$> evalInstr (L.GEP False pointeeType ptrV [zeroV, ofsV])
  
  -- | Truncate and log.
  llvmTrunc ::
    forall arch.
    -- | Context truncation is being generated in.
    String ->
    L.Typed L.Value ->
    L.Type ->
    BBLLVM arch (L.Typed L.Value)
  llvmTrunc ctx lhs rhs = do
    logEvent $
      LLVMLogEvent ctx $
        LogInfoTrunc $
          LLVMBitCastInfo (L.typedType lhs) rhs
    convop L.Trunc lhs rhs
  
  -- | Bitcast and log.
  llvmBitCast ::
    forall arch.
    -- | Context truncation is being generated in.
    String ->
    L.Typed L.Value ->
    L.Type ->
    BBLLVM arch (L.Typed L.Value)
  llvmBitCast ctx lhs rhs = do
    logEvent $
      LLVMLogEvent ctx $
        LogInfoBitCast $
          LLVMBitCastInfo (L.typedType lhs) rhs
    convop L.BitCast lhs rhs
  
  -- | Create a singleton vector from a value.
  singletonVector :: L.Typed L.Value -> BBLLVM arch (L.Typed L.Value)
  singletonVector val = do
    let eltType = L.typedType val
    let arrayType = L.Vector 1 eltType
    let vec0 = L.Typed arrayType L.ValUndef
    L.Typed arrayType
      <$> evalInstr (L.InsertElt vec0 val (L.ValInteger 0))
  
  checkEndian :: Endianness -> BBLLVM arch ()
  checkEndian end = do
    req <- asks $ archEndianness . archFns
    when (end /= req) $
      error $
        "Memory accesses must have byte order " ++ show req
  
  llvmFloatName :: FloatInfoRepr flt -> String
  llvmFloatName flt =
    case flt of
      HalfFloatRepr -> "f16"
      SingleFloatRepr -> "f32"
      DoubleFloatRepr -> "f64"
      QuadFloatRepr -> "f128"
      X86_80FloatRepr -> "f80"
  
  -- | Given a `MemRepr`, return the name of the type for annotating
  -- intrinsics and the type itself.
  resolveLoadNameAndType :: MemRepr tp -> BBLLVM arch (String, L.Type)
  resolveLoadNameAndType memRep =
    case memRep of
      BVMemRepr w end -> do
        checkEndian end
        let bvw = 8 * natValue w
        pure ("i" ++ show bvw, llvmITypeNat bvw)
      FloatMemRepr f end -> do
        checkEndian end
        pure (llvmFloatName f, L.PrimType (L.FloatType (llvmFloatType f)))
      PackedVecMemRepr n eltRep -> do
        (eltName, eltType) <- resolveLoadNameAndType eltRep
        unless (toInteger (natValue n) <= toInteger (maxBound :: Int32)) $ do
          error $ "Vector width of " ++ show n ++ " is too large."
        pure ("v" ++ show n ++ eltName, L.Vector (fromIntegral (natValue n)) eltType)
  
  -- | The type inference will infer a pointer-to-struct type for the pointer (or a conflict type if
  -- one is detected).  This will do a GEP or cast as required.
  pointerForMemOp ::
    forall arch.
    FnArchConstraints arch =>
    -- | Reason if we need to cast
    String ->
    -- | Value to evaluate
    FnValue arch (BVType (ArchAddrWidth arch)) ->
    -- | Type of value pointed to
    L.Type ->
    BBLLVM arch (L.Typed L.Value)
  pointerForMemOp ctx ptr pointeeType = do
    ptrV <- mkLLVMValue ptr
    getInferredTypeBBLLVM ptr >>= \case
      Just FPtrTy{} -> llvmGEPFromPtr pointeeType 0 ptrV
      Just FConflictTy{} -> llvmAsPtr ctx pointeeType ptrV
      Just t -> error $ "Unexpected type at pointerForMemOp: " ++ show (PP.pretty t)
      Nothing -> return ptrV
        -- error $ "No inferred type for " ++ show (PP.pretty ptr)
  
  -- | Convert an assignment to a llvm expression
  rhsToLLVM ::
    forall arch tp.
    (?config :: L.Config) =>
    FnArchConstraints arch =>
    HasCallStack =>
    -- | Value being assigned.
    FnAssignId ->
    FnAssignRhs arch (FnValue arch) tp ->
    BBLLVM arch ()
  rhsToLLVM lhs rhs =
    case rhs of
      FnEvalApp app -> do
        llvmRhs <- appToLLVM lhs app
        setAssignIdValue lhs llvmRhs
      FnSetUndefined tp -> do
        setAssignIdValue lhs (L.Typed (typeToLLVMType tp) L.ValUndef)
      FnReadMem ptr _typ -> do
        typeOfResult <- fromMaybe FUnknownTy <$> getInferredTypeForAssignIdBBLLVM lhs
        let ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
        let typeOfResult' = tyToLLVMType ptrWidth typeOfResult
        p <- pointerForMemOp "rhsToLLVM(FnReadMem)" ptr typeOfResult'
        v <- evalInstr (L.Load typeOfResult' p Nothing Nothing)
        setAssignIdValue lhs (L.Typed typeOfResult' v)
      FnCondReadMem memRepr cond ptr passthru -> do
        (loadName, eltType) <- resolveLoadNameAndType memRepr
        let intr = llvmMaskedLoad 1 loadName eltType
        addIntrinsic intr
  
        -- Copied from above
        typeOfResult <- fromMaybe FUnknownTy <$> getInferredTypeForAssignIdBBLLVM lhs
        let ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
        let typeOfResult' = tyToLLVMType ptrWidth typeOfResult
        p <- pointerForMemOp "rhsToLLVM(FnReadMem)" ptr typeOfResult'
  
        -- cast as a vec so we can call the conditional read intrinsic
        llvmAddr <- llvmBitCast "rhsToLLVM(FnCondReadMem)" p (L.PtrTo (L.Vector 1 eltType))
        let llvmAlign = L.Typed (L.iT 32) (L.ValInteger 0)
        llvmCond <- singletonVector =<< mkLLVMValue cond
        llvmPassthru <- singletonVector =<< mkLLVMValue passthru
        rv <- call intr [llvmAddr, llvmAlign, llvmCond, llvmPassthru]
        r <- evalInstr $ L.ExtractElt rv (L.ValInteger 0)
        setAssignIdValue lhs (L.Typed eltType r)
      FnEvalArchFn f -> do
        let archFnCallbackInst ops = archFnCallback ops @tp
        fn <- asks $ archFnCallbackInst . archFns
        setAssignIdValue lhs =<< fn f
      FnAddrWidthConstant i -> do
        let ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
        -- FIXME: this should always return a type, not Maybe
        typeOfResult <- fromMaybe FUnknownTy <$> getInferredTypeForAssignIdBBLLVM lhs
        let ty = tyToLLVMType ptrWidth typeOfResult
        let llvmRhs = case typeOfResult of
              FPtrTy ty'
                | i == 0 -> L.nullPtr (tyToLLVMType ptrWidth ty')
                | otherwise ->
                    L.Typed ty $
                      L.ValConstExpr (L.ConstConv L.IntToPtr (L.Typed (L.iT (fromIntegral ptrWidth)) (L.integer i)) ty)
              _ -> L.Typed ty $ L.integer i
        setAssignIdValue lhs llvmRhs
  
  resolveFunctionEntry ::
    FnValue arch (BVType (ArchAddrWidth arch)) ->
    BBLLVM
      arch
      ( L.Typed L.Value
      , [Maybe FTy]
      , Maybe (Maybe FTy)
      )
  resolveFunctionEntry dest =
    case dest of
      FnFunctionEntryValue dest_ftp nm -> do
        ctx <- ask
        withArchConstraints ctx $ do
          let sym = L.Symbol (BSC.unpack nm)
          constraints <- asks moduleConstraints
          let fty =
                fromMaybe
                  (error "fnTypes 1")
                  (Map.lookup nm (mcExtFunTypes constraints))
          let (args, retTy) = resolveFunctionType constraints fty
          return
            ( L.Typed (functionTypeToLLVM' dest_ftp args retTy) (L.ValSymbol sym)
            , args
            , retTy
            )
      _ -> do
        error "Do not support indirect calls."
  
  {-# INLINE bbArchConstraints #-}
  bbArchConstraints :: (LLVMArchConstraints arch => BBLLVM arch a) -> BBLLVM arch a
  bbArchConstraints m = do
    ctx <- ask
    withArchConstraints ctx m
  
  stmtToLLVM ::
    forall arch.
    (?config :: L.Config) =>
    HasCallStack =>
    FnStmt arch ->
    BBLLVM arch ()
  stmtToLLVM stmt = bbArchConstraints $ do
    -- This prints the FnStmt alongside the LLVM code, for debugging purposes
    -- comment (show $ PP.pretty stmt)
    case stmt of
      FnComment _ -> return ()
      FnAssignStmt (FnAssignment lhs rhs) -> do
        rhsToLLVM lhs rhs
      FnWriteMem addr v -> do
        vty <- fromMaybe FUnknownTy <$> getInferredTypeBBLLVM v
        let ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
        let vty' = tyToLLVMType ptrWidth vty
        llvmPtr <- pointerForMemOp "rhsToLLVM(FnWriteMem)" addr vty'
        llvmVal <- mkLLVMValue v
        effect $ L.Store llvmVal llvmPtr Nothing Nothing
      FnCondWriteMem cond addr v memRepr -> do
        -- Obtain llvm.masked.store intrinsic and ensure it will be declared.
        (loadName, eltType) <- resolveLoadNameAndType memRepr
        let intr = llvmMaskedStore 1 loadName eltType
        addIntrinsic intr
        -- Compute value to write
        llvmValue <- singletonVector =<< mkLLVMValue v
        -- Convert addr to appropriate pointer.
        vty <- fromMaybe FUnknownTy <$> getInferredTypeBBLLVM v
        let ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
        let vty' = tyToLLVMType ptrWidth vty
        p <- pointerForMemOp "rhsToLLVM(FnCondWriteMem)" addr vty'
        llvmAddr <- llvmBitCast "rhsToLLVM(FnCondWriteMem)" p (L.PtrTo (L.Vector 1 eltType))
        -- Just use zero alignment
        let llvmAlign = L.Typed (L.iT 32) (L.ValInteger 0)
        -- Construct mask
        llvmMask <- singletonVector =<< mkLLVMValue cond
        -- Call llvmn.masked.store intrinsic
        call_ intr [llvmValue, llvmAddr, llvmAlign, llvmMask]
      FnCall dest args mretv -> do
        (llvmFn, args', retty') <- resolveFunctionEntry dest
        let goSubtype (Some v) = mkLLVMSubtypeValue v
        llvmArgs <- zipWithM goSubtype args args'
        -- Assign return values
        case mretv of
          Nothing -> do
            call_ llvmFn llvmArgs
          Just (Some rvar) -> do
            retv <- call llvmFn llvmArgs
            rvarty <- getInferredTypeForAssignIdBBLLVM (frAssignId rvar)
            retv' <- coerceForSubtype (fromMaybe (error "Missing return type") retty') rvarty retv
            setAssignIdValue (frAssignId rvar) retv'
      FnArchStmt astmt -> do
        fn <- asks $ archStmtCallback . archFns
        fn astmt
  
  llvmBlockLabel :: FnBlockLabel w -> L.BlockLabel
  llvmBlockLabel = L.Named . L.Ident . fnBlockLabelString
  
  getPtrWidth :: forall arch. BBLLVM arch (NatRepr (ArchAddrWidth arch))
  getPtrWidth =
    asks
      ( \ctx ->
          withArchConstraints ctx $
            addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
      )
  
  getPtrWidth' :: BBLLVM arch Int
  getPtrWidth' = widthVal <$> getPtrWidth
  
  -- | @coerceForSubtype mty1 mty2 v@ takes a value `v` with some potential actual
  -- type `mty1` and some potential expected type `mty2` in some context, and
  -- tries to create a value with the appropriate expected type, if possible.  For
  -- instance, we may have been able to figure out that something is a pointer in
  -- some context, but passed it to a context where things got conflicted, so that
  -- we must present it as a numeric type instead.
  -- Another example is values that have been understood as function pointers, but
  -- whose arity was not deducible in some context.  This may be alleviated with
  -- better constraint generation.
  coerceForSubtype ::
    Maybe FTy ->
    Maybe FTy ->
    L.Typed L.Value ->
    BBLLVM arch (L.Typed L.Value)
  coerceForSubtype m_vTy m_tgtTy v = do
    ptrWidth <- getPtrWidth'
    case (fromMaybe FUnknownTy m_vTy, fromMaybe FUnknownTy m_tgtTy) of
      (t, t') | tyToLLVMType ptrWidth t == tyToLLVMType ptrWidth t' -> pure v
      (FPtrTy{}, FPtrTy tr) ->
        llvmBitCast "coerceForSubtype" v (L.PtrTo (tyToLLVMType ptrWidth tr))
      -- We are casting from a ptr to a non-ptr, probably due to a
      -- limitation in the type inference (e.g. during cycle detection)
      (FPtrTy{}, _) -> llvmPtrAsBV "coerceForSubtype" v
      (_, FPtrTy ty) ->
        llvmAsPtr "coerceForSubtype" (tyToLLVMType ptrWidth ty) v
      (FUnknownTy, FFunPtrTy{}) -> pure v -- TODO (val) ?
      (FUnknownTy, FUnknownFunPtrTy{}) -> pure v -- TODO (val) ?
      (FFunPtrTy argsL _retL, FPreFunPtrTy argsR FUnknownTy)
        | length argsR <= length argsL -> pure v
      (t, t') -> do
        thisLabel <- gets bbThisLabel :: BBLLVM arch L.BlockLabel
        error $
          show $
            "Type mismatch at "
              <> PP.viaShow thisLabel
              <> ": "
              <> PP.pretty t
              <> " and "
              <> PP.pretty t'
  
  mkLLVMSubtypeValue ::
    forall arch tp.
    MemWidth (ArchAddrWidth arch) =>
    FnValue arch tp ->
    Maybe FTy ->
    BBLLVM arch (L.Typed L.Value)
  mkLLVMSubtypeValue v m_tgtTy = do
    m_vTy <- getInferredTypeBBLLVM v
    coerceForSubtype m_vTy m_tgtTy =<< mkLLVMValue v
  
  -- | Add Phi values for target block
  addTargetPhiValues ::
    forall arch.
    MemWidth (ArchAddrWidth arch) =>
    FnJumpTarget arch -> BBLLVM arch ()
  addTargetPhiValues tgt = do
    thisLabel <- gets bbThisLabel :: BBLLVM arch L.BlockLabel
    let
      tgtLbl :: FnBlockLabel (ArchAddrWidth arch)
      tgtLbl = fnJumpLabel tgt
    tgtPhis <- asks (fromMaybe (error "Missing block") . Map.lookup tgtLbl . funBlockPhis)
  
    let doSubtype (Some v) (Some phiv) =
          mkLLVMSubtypeValue v =<< getInferredTypeForAssignIdBBLLVM (unFnPhiVar phiv)
    values <- V.zipWithM doSubtype (fnJumpPhiValues tgt) tgtPhis
  
    -- Add this block value to phi assignment
    let
      updateVar ::
        Map L.BlockLabel (Int, L.Value) ->
        L.Typed L.Value ->
        BBLLVM arch (Map L.BlockLabel (Int, L.Value))
      -- updateVar prevVars (Some v@(FnPhiValue phiVar)) = do
      -- constraints <- asks moduleConstraints
      -- fn <- asks funName
      -- let tyV = mcAssignTyVars constraints Map.! fn Map.! unFnPhiVar phiVar
      -- let inferredType = mcTypeMap constraints Map.! tyV
      -- thisVal <- mkLLVMValue v
      -- pure $! Map.insertWith (const (first (+ 1))) thisLabel (1, L.typedValue thisVal) prevVars
      updateVar prevVars v = do
        pure $! Map.insertWith (const (first (+ 1))) thisLabel (1, L.typedValue v) prevVars
    m <- BBLLVM $ use $ funStateLens . funBlockPhiMapLens
    let curEntries = phiAssignmentForBlock m tgtLbl
    newEntries <- V.zipWithM updateVar curEntries values
    BBLLVM $ funStateLens . funBlockPhiMapLens .= Map.insert tgtLbl newEntries m
  
  termStmtToLLVM ::
    HasCallStack =>
    MemWidth (ArchAddrWidth arch) =>
    FnTermStmt arch ->
    BBLLVM arch ()
  termStmtToLLVM tm =
    case tm of
      FnJump tgt -> do
        addTargetPhiValues tgt
        let lbl = llvmBlockLabel $ fnJumpLabel tgt
        effect $ L.Jump lbl
      FnBranch macawCond ttgt ftgt -> do
        llvmCond <- mkLLVMValue macawCond
        addTargetPhiValues ttgt
        addTargetPhiValues ftgt
        let tlbl = llvmBlockLabel $ fnJumpLabel ttgt
        let flbl = llvmBlockLabel $ fnJumpLabel ftgt
        effect $ L.Br llvmCond tlbl flbl
      FnLookupTable idx vec -> do
        idx' <- mkLLVMValue idx
        traverse_ addTargetPhiValues vec
        let dests = V.toList $ llvmBlockLabel . fnJumpLabel <$> vec
        markNeedSwitchFailLabel
        effect $ L.Switch idx' (L.Named (L.Ident switchFailLabel)) (zip [0 ..] dests)
      FnRet mret -> do
        ftp <- asks funRetType
        case (ftp, mret) of
          (Nothing, Nothing) -> effect L.RetVoid
          (Just _, Nothing) -> error ("Expected return value when none found '" ++ show ftp ++ "'")
          (Nothing, Just _) -> error "Unexpected return value."
          (Just _rtp, Just (Some rval)) -> ret =<< mkLLVMValue rval
      FnTailCall dest args -> do
        (callTarget, args', retty') <- resolveFunctionEntry dest
        let goSubtype (Some v) = mkLLVMSubtypeValue v
        llvmArgs <- zipWithM goSubtype args args'
        fret <- asks funRetType
        let callTargetType = L.typedType callTarget
        let callTargetValue = L.typedValue callTarget
        case callTargetType of
          L.PtrTo (L.FunTy res _argTypes _varArgs) ->
            case res of
              L.PrimType L.Void -> do
                effect $ L.Call False callTargetType callTargetValue llvmArgs
                effect L.RetVoid
              _ -> do
                retv <- evalInstr $ L.Call False callTargetType callTargetValue llvmArgs
                -- FIXME: clean this up
                retv' <-
                  coerceForSubtype
                    (fromMaybe (error "Missing return type") retty')
                    (fromMaybe (error "Missing return type") fret)
                    (L.Typed res retv)
                ret retv'
          _ -> do
            error "Expected function type to tail call target."
  
  resolvePhiStmt ::
    forall arch.
    FnArchConstraints arch =>
    ModuleConstraints arch ->
    BSC.ByteString ->
    PhiValues ->
    PhiBinding arch ->
    [L.Stmt]
  resolvePhiStmt constraints function phiValues b =
    let
      ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
      phiAssignId = viewSome unFnPhiVar (phiFnRepVar b)
      lnm = L.Ident (phiLLVMIdent b)
      -- If we inferred a type for the phi variable by constraint solving, it
      -- takes precedence over the type we inferred at recovery time.
      llvmType :: L.Type
      llvmType =
        case getKnownInferredType function constraints phiAssignId of
          Just inferredType -> tyToLLVMType ptrWidth inferredType
          Nothing -> viewSome (typeToLLVMType . fnPhiVarType) (phiFnRepVar b)
      llvmPhiValues :: [(L.Value, L.BlockLabel)]
      llvmPhiValues =
        [ binding
        | (lbl, (llvmCnt, llvmVal)) <- Map.toList phiValues
        , binding <- replicate llvmCnt (llvmVal, lbl)
        ]
      showPhiAssignIdsInComments = True
     in
      [L.Effect (L.Comment (show phiAssignId)) [] | showPhiAssignIdsInComments]
        ++ [L.Result lnm (L.Phi llvmType llvmPhiValues) []]
  
  -- | Construct a basic block from a block result
  toBasicBlock ::
    HasCallStack =>
    LLVMArchConstraints arch =>
    ModuleConstraints arch ->
    BSC.ByteString ->
    ResolvePhiMap (ArchAddrWidth arch) ->
    -- | This block
    LLVMBlockResult arch ->
    L.BasicBlock
  toBasicBlock constraints function phiMap res
    | V.length phiVars /= V.length phiAssignment =
        error "Phi variables length does not match phi assignment."
    | otherwise =
        L.BasicBlock
          { L.bbLabel = Just lbl
          , L.bbStmts = phiStmts ++ reverse (bbStmts finalState)
          }
   where
    b = fnBlock res
    phiVars = llvmPhiVars res
    phiAssignment = phiAssignmentForBlock phiMap (fbLabel b)
    lbl = L.Named (L.Ident (fnBlockLabelString (fbLabel b)))
    phiStmts = join . V.toList $ V.zipWith (resolvePhiStmt constraints function) phiAssignment phiVars
    finalState = finalBBState res
  
  -- | Information relating a Macaw funcation variable and LLVM identifier.
  data PhiBinding arch = PhiBinding
    { phiFnRepVar :: !(Some (FnPhiVar arch))
    -- ^ Function representation variable.
    , phiLLVMIdent :: !String
    -- ^ LLVM identifier for Phi variable
    }
  
  -- | Add a phi var with the node info so that we have a ident to
  -- reference it by and queue up work to assign the value later.
  addPhiBinding ::
    HasCallStack =>
    Some (FnPhiVar arch) ->
    BBLLVM arch (PhiBinding arch)
  addPhiBinding (Some phiVar) = do
    L.Ident nm <- freshName
    ptrWidth <- getPtrWidth'
    m_fty <- getInferredTypeForAssignIdBBLLVM (unFnPhiVar phiVar)
    let llvmType =
          maybe (typeToLLVMType (fnPhiVarType phiVar)) (tyToLLVMType ptrWidth) m_fty
    setAssignIdValue (unFnPhiVar phiVar) (L.Typed llvmType (L.ValIdent (L.Ident nm)))
    pure $!
      PhiBinding
        { phiFnRepVar = Some phiVar
        , phiLLVMIdent = nm
        }
  
  addLLVMBlock ::
    forall arch.
    (?config :: L.Config) =>
    MemWidth (ArchAddrWidth arch) =>
    -- | Context for block
    FunLLVMContext arch ->
    FunState arch ->
    -- | Block to generate
    FnBlock arch ->
    (FunState arch, LLVMBlockResult arch)
  addLLVMBlock ctx fs b = (finFS, res)
   where
    s0 =
      BBLLVMState
        { bbThisLabel = llvmBlockLabel (fbLabel b)
        , bbAssignValMap = Map.empty
        , bbStmts = []
        , bbLLVMLogEvents = []
        }
    go :: BBLLVM arch (V.Vector (PhiBinding arch))
    go = do
      -- Add statements for Phi nodes
      bindings <- traverse addPhiBinding (fbPhiVars b)
      -- Add statements
      mapM_ stmtToLLVM (fbStmts b)
      -- Add term statement
      termStmtToLLVM (fbTerm b)
      -- Results
      pure bindings
    (phiBindings, BBLLVMPair finFS s) =
      runState (runReaderT (unBBLLVM go) ctx) (BBLLVMPair fs s0)
  
    res =
      LLVMBlockResult
        { fnBlock = b
        , llvmPhiVars = phiBindings
        , finalBBState = s
        }
  
  ------------------------------------------------------------------------
  -- Inline assembly
  
  -- | Attributes to annote inline assembly.
  newtype AsmAttrs = AsmAttrs {asmSideeffect :: Bool}
  
  -- | Indicates all side effects  of inline assembly are captured in the constraint list.
  noSideEffect :: AsmAttrs
  noSideEffect = AsmAttrs{asmSideeffect = False}
  
  -- | Indicates asm may have side effects that are not captured in the
  -- constraint list.
  sideEffect :: AsmAttrs
  sideEffect = AsmAttrs{asmSideeffect = True}
  
  -- | Call some inline assembly
  callAsm ::
    -- | Asm attrs
    AsmAttrs ->
    -- | Return type
    L.Type ->
    -- | Code
    String ->
    -- | Args code
    String ->
    -- | Arguments
    [L.Typed L.Value] ->
    BBLLVM arch (L.Typed L.Value)
  callAsm attrs resType asmCode asmArgs args = do
    let
      argTypes = L.typedType <$> args
      ftp = L.PtrTo (L.FunTy resType argTypes False)
      f = L.ValAsm (asmSideeffect attrs) False asmCode asmArgs
    L.Typed resType <$> evalInstr (L.Call False ftp f args)
  
  -- | Call some inline assembly that does not return a value.
  callAsm_ ::
    -- | Asm attrs
    AsmAttrs ->
    -- | Code
    String ->
    -- | Args code
    String ->
    -- | Arguments
    [L.Typed L.Value] ->
    BBLLVM arch ()
  callAsm_ attrs asmCode asmArgs args = do
    let argTypes = L.typedType <$> args
    let ftp = L.PtrTo (L.FunTy (L.PrimType L.Void) argTypes False)
    let
      f :: L.Value
      f = L.ValAsm (asmSideeffect attrs) False asmCode asmArgs
    call_ (L.Typed ftp f) args
  
  ------------------------------------------------------------------------
  -- Translating functions
  
  data LLVMTransState = LLVMTransState
    { llvmTransIntrinsicMap :: !IntrinsicMap
    , llvmTransLogEvents :: ![LLVMLogEvent]
    }
  
  -- | The LLVM translate monad records all the intrinsics detected when
  -- adding LLVM.
  newtype LLVMTrans a = LLVMTrans (State LLVMTransState a)
    deriving (Functor, Applicative, Monad, MonadState LLVMTransState)
  
  -- | Run the translation returning result and intrinsics.
  runLLVMTrans :: LLVMTrans a -> ([Intrinsic], [LLVMLogEvent], a)
  runLLVMTrans (LLVMTrans action) =
    let (r, LLVMTransState m events) = runState action (LLVMTransState Map.empty [])
     in (Map.elems m, events, r)
  
  argIdent :: Int -> L.Ident
  argIdent i = L.Ident ("arg" ++ show i)
  
  memAnn :: Ann.MCAddr -> (Word64, FnMemAccessType) -> Ann.MCMemoryEvent
  memAnn a (o, tp) =
    Ann.MCMemoryEvent
      { Ann.eventAddr = fromIntegral a + fromIntegral o
      , Ann.eventInfo =
          case tp of
            HeapAccess -> Ann.HeapAccess
            StackAccess -> Ann.BinaryOnlyAccess
      }
  
  mkStackExpr :: Integer -> Ann.Expr Ann.BlockVar
  mkStackExpr o
    | o < 0 =
        let oExpr = Ann.BVDecimal (fromInteger (negate o)) 64
         in Ann.BVSub (Ann.Var Ann.StackHigh) oExpr
    | o == 0 = Ann.Var Ann.StackHigh
    | otherwise =
        let
          oExpr :: Ann.Expr Ann.BlockVar
          oExpr = Ann.BVDecimal (fromInteger o) 64
         in
          Ann.BVAdd (Ann.Var Ann.StackHigh) oExpr
  
  newtype BlockAnnGen a = BlockAnnGen (Except String a)
    deriving (Functor, Applicative, Monad, MonadError String)
  
  runBlockAnnGen :: BSC.ByteString -> Ann.MCAddr -> BlockAnnGen a -> Either String a
  runBlockAnnGen fnm a (BlockAnnGen m) =
    case runExcept m of
      Left e -> Left $ printf "Missing annotation generation feature in %s(%s): %s" (BSC.unpack fnm) (show a) e
      Right r -> Right r
  
  -- | Create an annotation from a bound location.
  mkBoundLocExpr :: HasCallStack => BoundLoc X86Reg tp -> BlockAnnGen (Ann.Expr Ann.BlockVar)
  mkBoundLocExpr (RegLoc xr) =
    case xr of
      X86_GP r ->
        pure $! Ann.Var (Ann.InitGPReg64 r)
      X86_FlagReg r ->
        pure $! Ann.Var (Ann.InitFlagReg r)
      _ ->
        throwError $ "Do not support register " ++ show xr
  mkBoundLocExpr (StackOffLoc o tp) =
    if o < 0
      then case tp of
        BVMemRepr byteCount LittleEndian -> do
          let
            stackExpr = mkStackExpr (toInteger o)
            bitCount = 8 * natValue byteCount
          pure $! Ann.Var (Ann.MCStack stackExpr bitCount)
        _ ->
          throwError $ "Do not support stack references with type " ++ show tp
      else throwError "Do not support positive stack offsets."
  
  -- | Generate preconditions for a phi variable to associate LLVM phi
  -- variables with machine code.
  addPhiPrecond :: PhiBinding X86_64 -> [Ann.Expr Ann.BlockVar] -> BlockAnnGen [Ann.Expr Ann.BlockVar]
  addPhiPrecond b prev0 =
    case phiFnRepVar b of
      Some phiVar -> do
        -- Get expression representing LLVM value.
        let
          phiExpr :: Ann.Expr Ann.BlockVar
          phiExpr = Ann.Var (Ann.LLVMVar (Text.pack (phiLLVMIdent b)))
          -- Assert pfi expression is equal to each machine location.
          vars = fnPhiVarRep phiVar : fnPhiVarLocations phiVar
        let fn v prev = seq prev $ do
              e <- mkBoundLocExpr v
              let expr = Ann.Eq phiExpr e
              seq expr $ pure (expr : prev)
        foldrM fn prev0 vars
  
  -- | Create assertions from block preconditions.
  mkInvPrecond :: FnBlockInvariant X86_64 -> BlockAnnGen (Ann.Expr Ann.BlockVar)
  mkInvPrecond (FnCalleeSavedReg r x) = do
    xExpr <- mkBoundLocExpr x
    regExpr <-
      case r of
        X86_GP rgp -> pure $! Ann.Var (Ann.FnStartGPReg64 rgp)
        _ -> throwError "Only general purpose registers are supported."
    pure $! Ann.Eq xExpr regExpr
  mkInvPrecond (FnEqualLocs x y) =
    Ann.Eq <$> mkBoundLocExpr x <*> mkBoundLocExpr y
  mkInvPrecond (FnStackOff o x) =
    Ann.Eq <$> mkBoundLocExpr x <*> pure (mkStackExpr (toInteger o))
  
  -- | Generate pair containing block label in LLVM and annotations from
  -- block.
  getBlockAnn ::
    -- | Name of function
    BSC.ByteString ->
    LLVMBlockResult X86_64 ->
    Either String (String, Ann.BlockAnn)
  getBlockAnn fnm blockRes = do
    let b = fnBlock blockRes
    let lbl = fbLabel b
    let addr = fromIntegral $ addrOffset $ segoffAddr $ fnBlockLabelAddr lbl
    runBlockAnnGen fnm addr $ do
      let pr = fbPrecond b
      invPreconds <- mapM mkInvPrecond (fbInvariants b)
  
      -- Preconditions that relate phi variable with Macaw location.
      preconds <- foldrM addPhiPrecond invPreconds (llvmPhiVars blockRes)
  
      let isTail = case fbTerm b of
            FnTailCall{} -> True
            _ -> False
  
      -- Generate memory event annotation given base address, offset and address type.
      let ann =
            Ann.ReachableBlockAnn
              { Ann.blockAddr = addr
              , Ann.blockCodeSize = fbSize b
              , Ann.blockX87Top = blockInitX87TopReg pr
              , Ann.blockDFFlag = blockInitDF pr
              , Ann.blockPreconditions = preconds
              , Ann.blockAllocas = Map.empty
              , Ann.mcMemoryEvents = V.toList $ memAnn addr <$> fbMemInsnAddrs b
              , Ann.isTailCall = isTail
              }
      pure (fnBlockLabelString lbl, Ann.ReachableBlock ann)
  
  -- | This translates the function to LLVM and returns the define.
  --
  -- We have each function return all possible results, although only
  -- the ones that are actually used (we use undef for the others).
  -- This makes the LLVM conversion slightly simpler.
  --
  -- Users should declare intrinsics via 'declareIntrinsics' before
  -- using this function.  They should also add any referenced
  -- functions.
  defineFunction ::
    forall arch.
    (?config :: L.Config) =>
    (LLVMArchConstraints arch, arch ~ X86_64) =>
    ArchitectureInfo arch ->
    -- | Architecture specific operations
    LLVMArchSpecificOps arch ->
    -- | Options for generating LLVM
    LLVMGenOptions ->
    -- | Types inferred from constraint-solving
    ModuleConstraints arch ->
    -- | Function to translate
    Function arch ->
    LLVMTrans (L.Define, Either String Ann.FunctionAnn)
  defineFunction aInfo archOps genOpts constraints f = do
    let ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
    let
      mkInputReg :: (Some TypeRepr, TyVar) -> Int -> L.Typed L.Ident
      mkInputReg (Some tp, tyv) i =
        case Map.lookup tyv (mcTypeMap constraints) of
          Just (FPtrTy pointee) -> L.Typed (L.PtrTo (tyToLLVMType ptrWidth pointee)) (argIdent i)
          _ -> L.Typed (typeToLLVMType tp) (argIdent i)
  
    let fty = fromMaybe (error "fty") (Map.lookup (fnName f) (mcExtFunTypes constraints))
    let argsWithTyVars = zip (fnArgTypes (fnType f)) (fttvArgs fty)
  
    let
      inputArgs :: [L.Typed L.Ident]
      inputArgs = zipWith mkInputReg argsWithTyVars [0 ..]
  
    let fret = fmap (\tv -> Map.lookup tv (mcTypeMap constraints)) (fttvRet fty)
  
    let
      -- Needed for GHC >= 9
      id' :: (LLVMArchConstraints arch => a) -> a
      id' a = a
  
    let
      ctx :: FunLLVMContext arch
      ctx =
        FunLLVMContext
          { archInfo = aInfo
          , archFns = archOps
          , funLLVMGenOptions = genOpts
          , funAddr = fnAddr f
          , funName = fnName f
          , funArgs = V.fromList $ fmap L.ValIdent <$> inputArgs
          , funRetType = fret
          , funAllocaCount = 0
          , moduleConstraints = constraints
          , funBlockPhis = phiMapFromFunction f
          , withArchConstraints = id'
          }
  
    -- Create ordinary blocks
    m0 <- gets llvmTransIntrinsicMap
    let
      initFunState :: FunState arch
      initFunState =
        FunState
          { nmCounter = 0
          , funIntrinsicMap = m0
          , needSwitchFailLabel = False
          , funBlockPhiMap = initResolvePhiMap f
          }
    let (postEntryFunState, entryBlockRes) =
          addLLVMBlock ctx initFunState (fnEntryBlock f)
  
    let (finalFunState, finalBlocks) =
          mapAccumL (addLLVMBlock ctx) postEntryFunState (fnRestBlocks f)
  
    -- Update intrins map and log events
    modify' $ \s ->
      s
        { llvmTransIntrinsicMap = funIntrinsicMap finalFunState
        , llvmTransLogEvents =
            bbLLVMLogEvents (finalBBState entryBlockRes)
              ++ concatMap (bbLLVMLogEvents . finalBBState) finalBlocks
              ++ llvmTransLogEvents s
        }
  
    let
      entryLLVMBlock :: L.BasicBlock
      entryLLVMBlock = toBasicBlock constraints (fnName f) (funBlockPhiMap finalFunState) entryBlockRes
  
    let
      blocks :: [L.BasicBlock]
      blocks = toBasicBlock constraints (fnName f) (funBlockPhiMap finalFunState) <$> finalBlocks
  
    let finBlocks
          | needSwitchFailLabel finalFunState = entryLLVMBlock : (blocks ++ [failBlock])
          | otherwise = entryLLVMBlock : blocks
    let funDef =
          L.Define
            { L.defLinkage = Nothing
            , L.defVisibility = Nothing
            , L.defRetType = llvmFunctionReturnType (fnType f)
            , L.defName = L.Symbol (BSC.unpack (fnName f))
            , L.defArgs = inputArgs
            , L.defVarArgs = False
            , L.defAttrs = []
            , L.defSection = Nothing
            , L.defGC = Nothing
            , L.defBody = finBlocks
            , L.defMetadata = Map.empty
            , L.defComdat = Nothing
            }
    let
      funAnn :: Either String Ann.FunctionAnn
      funAnn = do
        blockAnnEntries <- mapM (getBlockAnn (fnName f)) (V.fromList (entryBlockRes : finalBlocks))
        let finBlockAnnMap
              | needSwitchFailLabel finalFunState =
                  V.snoc blockAnnEntries (switchFailLabel, Ann.UnreachableBlock)
              | otherwise =
                  blockAnnEntries
        let blockObjMap = uncurry Ann.blockAnnToJSON <$> finBlockAnnMap
        let addr = fromIntegral $ addrOffset $ segoffAddr $ fnAddr f
        pure $!
          Ann.FunctionAnn
            { Ann.llvmFunName = BSC.unpack (fnName f)
            , Ann.faStartAddr = addr
            , Ann.blocks = blockObjMap
            }
    pure (funDef, funAnn)
  
  -- | Create function annotation from declaration.
  mkExternalFunctionAnn ::
    FunctionDecl arch ->
    Ann.ExternalFunctionAnn
  mkExternalFunctionAnn d =
    let
      -- Name of function as string
      nm = BSC.unpack $ funDeclName d
      -- Address of function
      a = memWordValue $ addrOffset $ segoffAddr $ funDeclAddr d
     in
      Ann.ExternalFunctionAnn
        { Ann.efaLlvmFunName = nm
        , Ann.efaStartAddr = fromIntegral a
        , Ann.efaIsNoReturn = funDeclNoReturn d
        }
  
  ------------------------------------------------------------------------
  -- Other
  
  declareIntrinsic :: Intrinsic -> L.Declare
  declareIntrinsic i =
    L.Declare
      { L.decLinkage = Nothing
      , L.decVisibility = Nothing
      , L.decRetType = intrinsicRes i
      , L.decName = intrinsicName i
      , L.decArgs = intrinsicArgs i
      , L.decVarArgs = False
      , L.decAttrs = intrinsicAttrs i
      , L.decComdat = Nothing
      }
  
  -- | Generate LLVM module from a list of functions describing the
  -- behavior.
  moduleForFunctions ::
    forall arch.
    (?config :: L.Config) =>
    arch ~ X86_64 =>
    FoldableF (FnArchStmt arch) =>
    FoldableFC (ArchFn arch) =>
    LLVMArchConstraints arch =>
    Show (FunctionType arch) =>
    ArchitectureInfo arch ->
    -- | Architecture specific functions
    LLVMArchSpecificOps arch ->
    -- | Options for generating LLVM
    LLVMGenOptions ->
    -- | Module to generate
    RecoveredModule arch ->
    ModuleConstraints arch ->
    ( L.Module
    , [(FunId, Either String Ann.FunctionAnn)]
    , [Ann.ExternalFunctionAnn]
    , [LLVMLogEvent]
    )
  moduleForFunctions aInfo archOps genOpts recMod constraints =
    let
      (dynIntrinsics, logEvents, definesAndAnn) = runLLVMTrans $
        forM (recoveredDefs recMod) $ \f -> do
          let fId = funId (fnAddr f) (Just (fnName f))
          (d, ma) <- defineFunction aInfo archOps genOpts constraints f
          pure (d, (fId, ma))
      -- FIXME: this is repeated in a bunch of places
      ptrWidth = widthVal $ addrWidthNatRepr (addrWidthRepr (Proxy :: Proxy (ArchAddrWidth arch)))
      namedTypes =
        [ L.TypeDecl (L.Ident s) (tyToLLVMType ptrWidth ty)
        | (s, ty) <- mcNamedTypes constraints
        ]
      llvmMod =
        L.Module
          { L.modSourceName = Nothing
          , L.modDataLayout = []
          , L.modTypes = namedTypes
          , L.modNamedMd = []
          , L.modUnnamedMd = []
          , L.modGlobals = []
          , L.modDeclares =
              fmap declareIntrinsic llvmIntrinsics
                ++ fmap declareIntrinsic dynIntrinsics
                ++ fmap declareFunction (recoveredDecls recMod)
          , L.modDefines = fst <$> definesAndAnn
          , L.modInlineAsm = []
          , L.modAliases = []
          , L.modComdat = Map.empty
          , L.modTriple =
              L.TargetTriple
                { L.ttArch = L.X86_64
                , L.ttSubArch = L.NoSubArch
                , L.ttVendor = L.UnknownVendor
                , L.ttOS = L.Linux
                , L.ttEnv = L.GNU
                , L.ttObjFmt = L.UnknownObjectFormat
                }
          }
      annDecls = mkExternalFunctionAnn <$> recoveredDecls recMod
     in
      (llvmMod, snd <$> definesAndAnn, annDecls, logEvents)
  
  type GetInferredTypeEffects arch es =
    ( R.Reader BSC.ByteString :> es
    , R.Reader (ModuleConstraints arch) :> es
    )
  
  macawTypeToFTy :: Some TypeRepr -> FTy
  macawTypeToFTy = viewSome go
   where
    go :: TypeRepr ty -> FTy
    go BoolTypeRepr = FNumTy 1
    go (BVTypeRepr n) = FNumTy (fromInteger (intValue n))
    go (FloatTypeRepr _flt) = error "TODO: support float in type inference"
    go (TupleTypeRepr s) = FTupleTy $ toListFC go s
    go (VecTypeRepr w tp) = FVecTy (fromInteger (intValue w)) (go tp)
  
  functionTypeToFTy :: FunctionType arch -> FTy
  functionTypeToFTy fty | fnVarArgs fty = error "functionTypeToFTy: varargs"
  functionTypeToFTy fty =
    FFunPtrTy (mkArg <$> fnArgTypes fty) (mkRet $ fnReturnType fty)
    where
      mkArg :: Some TypeRepr -> FTy
      mkArg = macawTypeToFTy
      mkRet :: Maybe (Some TypeRepr) -> FTy
      mkRet Nothing = FVoidTy
      mkRet (Just tau) = macawTypeToFTy tau
  
  -- | Returns the type that was inferred for the given value via constraint solving, if any.
  getInferredType ::
    forall arch es tp.
    GetInferredTypeEffects arch es =>
    MemWidth (ArchAddrWidth arch) =>
    Proxy arch ->
    FnValue arch tp ->
    Eff es (Maybe FTy)
  getInferredType _ FnUndefined{} = pure Nothing
  getInferredType _ (FnConstantValue sz _) = pure (Just (FNumTy (widthVal sz)))
  getInferredType _ FnConstantBool{} = pure Nothing
  getInferredType _ (FnFunctionEntryValue fty nm) = do
    -- NOTE: This is where we must ignore the Macaw type of the function symbol,
    -- as it is less precise than the types we obtain through constraint solving.
    -- Namely, function pointers will just have a numeric type in Macaw.
    mc <- R.ask @(ModuleConstraints arch)
    case Map.lookup nm (mcExtFunTypes mc) of
      Nothing ->
        trace ("Warning: defaulting to Macaw type because we could not find type for " <> show nm)
          $ pure $ Just $ functionTypeToFTy fty
      Just ftyv ->
        case asFullyResolvedFunctionType mc ftyv of
          Nothing ->
            trace ("Warning: defaulting to Macaw type because we could not instantiate type variables for " <> show nm)
              $ pure $ Just $ functionTypeToFTy fty
          Just resolved -> pure $ Just resolved
    -- pure $ Just $ functionTypeToFTy fty
  getInferredType pxy (FnAssignedValue (FnAssignment aId _)) = getInferredTypeForAssignId pxy aId
  getInferredType pxy (FnPhiValue phiVar) = getInferredTypeForAssignId pxy (unFnPhiVar phiVar)
  getInferredType pxy (FnReturn (FnReturnVar retVar _)) = getInferredTypeForAssignId pxy retVar
  getInferredType pxy (FnArg arg _typ) = do
    fn <- R.ask @BSC.ByteString
    getInferredFunctionArgType pxy fn arg
  getInferredType _ (FnCodePointer fn) = do
    mc <- R.ask @(ModuleConstraints arch)
    case Map.lookup fn (mcFunTypes mc) of
      Nothing -> return Nothing
      Just fty ->
        case asFullyResolvedFunctionType mc fty of
          Just ty -> return $ Just ty
          Nothing -> error $ "getInferredType: could not resolve " <> show fty
  getInferredType _ (FnTypedCodePointer _args _ret) = error "TODO" -- TODO
  
  -- | Run `getInferredType`, passing the necessary information explicitly.
  runGetInferredType ::
    MemWidth (ArchAddrWidth arch) =>
    BSC.ByteString -> ModuleConstraints arch -> Proxy arch -> FnValue arch tp -> Maybe FTy
  runGetInferredType bs mc pa fv =
    runPureEff
      . R.runReader bs
      . R.runReader mc
      $ getInferredType pa fv
  
  -- | Runs `getInferredType` in a `BBLLVM` monadic context, where all the
  -- information needed is available.
  getInferredTypeBBLLVM ::
    forall arch tp.
    MemWidth (ArchAddrWidth arch) =>
    FnValue arch tp -> BBLLVM arch (Maybe FTy)
  getInferredTypeBBLLVM fv = do
    fn <- asks funName
    mc <- asks moduleConstraints
    return $ runGetInferredType fn mc (Proxy @arch) fv
  
  getInferredFunctionArgType ::
    forall arch es.
    GetInferredTypeEffects arch es =>
    Proxy arch ->
    BSC.ByteString ->
    Int ->
    Eff es (Maybe FTy)
  getInferredFunctionArgType _ fn arg = do
    constraints <- R.ask @(ModuleConstraints arch)
    let fnTypes =
          fromMaybe
            (error "fnTypes 1")
            (Map.lookup fn (mcExtFunTypes constraints))
    let argTyVar = fttvArgs fnTypes !! arg
    return (Map.lookup argTyVar (mcTypeMap constraints))
  
  getInferredTypeForAssignIdBBLLVM :: FnAssignId -> BBLLVM arch (Maybe FTy)
  getInferredTypeForAssignIdBBLLVM aId =
    do
      fn <- asks funName
      mc <- asks moduleConstraints
      return $ runGetInferredTypeForAssignId fn mc aId
  
  runGetInferredTypeForAssignId ::
    forall arch.
    BSC.ByteString -> ModuleConstraints arch -> FnAssignId -> Maybe FTy
  runGetInferredTypeForAssignId fn mc aId =
    runPureEff
      . R.runReader fn
      . R.runReader mc
      $ getInferredTypeForAssignId (Proxy @arch) aId
  
  getInferredTypeForAssignId ::
    forall arch es.
    GetInferredTypeEffects arch es =>
    Proxy arch ->
    FnAssignId ->
    Eff es (Maybe FTy)
  getInferredTypeForAssignId _ aId = do
    fn <- R.ask
    constraints <- R.ask @(ModuleConstraints arch)
    let fnTypes =
          fromMaybe
            (error ("Missing function key in mcAssignTyVars: " <> show fn))
            (Map.lookup fn (mcAssignTyVars constraints))
    return $ do
      valTyVar <- Map.lookup aId fnTypes
      Map.lookup valTyVar (mcTypeMap constraints)
  
  getKnownInferredType ::
    forall arch.
    BSC.ByteString ->
    ModuleConstraints arch ->
    FnAssignId ->
    Maybe FTy
  getKnownInferredType fn constraints aId =
    case runGetInferredTypeForAssignId fn constraints aId of
      Nothing -> Nothing
      Just FUnknownTy -> Nothing
      Just t -> Just t
  