Trans.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}

module Mir.Trans(transCollection,transStatics,RustModule(..)
                , readMirRef
                , writeMirRef
                , subindexRef
                , evalBinOp
                , evalOperand
                , vectorCopy, aggregateCopy_constLen
                , ptrCopy, copyNonOverlapping
                , isNonOverlapping
                , evalRval
                , callExp
                , callHandle
                , doVirtCall
                , derefExp, readPlace, addrOfPlace
                , transmuteExp
                , extendUnsignedBV
                ) where

import Control.Monad
import Control.Monad.ST
import Control.Monad.Trans.Class

import Control.Lens hiding (op,(|>))
import qualified Control.Lens.Extras as Lens (is)
import Data.Foldable

import Data.Bits (shift, shiftL)
import qualified Data.ByteString as BS
import qualified Data.Char as Char
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Maybe as Maybe
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.STRef
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Traversable as Trav
import Data.String (fromString)
import Numeric
import Numeric.Natural()

import Prettyprinter (Pretty(..))
import qualified Prettyprinter as PP

import qualified Lang.Crucible.CFG.Generator as G
import qualified Lang.Crucible.FunctionHandle as FH
import qualified What4.ProgramLoc as PL
import qualified What4.FunctionName as FN
import qualified What4.Utils.StringLiteral as W4
import qualified Lang.Crucible.CFG.Reg as R
import qualified Lang.Crucible.CFG.SSAConversion as SSA
import qualified Lang.Crucible.CFG.Expr as E
import qualified Lang.Crucible.CFG.Core as Core
import qualified Lang.Crucible.Syntax as S
import qualified Lang.Crucible.Types as C
import Lang.Crucible.Panic


import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Classes
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Parameterized.Nonce (newSTNonceGenerator)

import Mir.Mir
import qualified Mir.Mir as M
import qualified Mir.DefId as M

import Mir.Intrinsics
import Mir.Generator
import Mir.GenericOps
import Mir.TransTy

import Mir.PP (fmt, fmtDoc)

import Debug.Trace



parsePosition :: Text.Text -> PL.Position
parsePosition posText =
  case Text.split (== ':') posText of
    [fname',line,col]
      | (l,[]):_ <- readDec (Text.unpack line)
      , (c,[]):_ <- readDec (Text.unpack col)
      -> PL.SourcePos fname' l c
    _ -> PL.OtherPos posText


setPosition :: Text.Text -> MirGenerator h s ret ()
setPosition = G.setPosition . parsePosition

--------------------------------------------------------------------------------------
-- ** Expressions

-- Expressions: variables and constants
--

transConstVal :: HasCallStack => M.Ty -> Some C.TypeRepr -> M.ConstVal -> MirGenerator h s ret (MirExp s)

-- Custom types
transConstVal (CTyBv _) (Some (C.BVRepr w)) (M.ConstStruct [M.ConstInt i, M.ConstStruct []]) = do
    val <- case M.fromIntegerLit i of
        0 -> return 0   -- Bv::ZERO
        1 -> return 1   -- Bv::ONE
        2 -> return $ (1 `shift` fromIntegral (intValue w)) - 1    -- Bv::MAX
        i' -> mirFail $ "unknown bitvector constant " ++ show i'
    return $ MirExp (C.BVRepr w) (S.app $ eBVLit w val)
transConstVal CTyMethodSpec _ _ = do
    mirFail "transConstVal: can't construct MethodSpec without an override"
transConstVal CTyMethodSpecBuilder _ _ = do
    mirFail "transConstVal: can't construct MethodSpecBuilder without an override"

transConstVal _ty (Some (C.BVRepr w)) (M.ConstInt i) =
    return $ MirExp (C.BVRepr w) (S.app $ eBVLit w (fromInteger (M.fromIntegerLit i)))
transConstVal _ty (Some (C.BoolRepr)) (M.ConstBool b) = return $ MirExp (C.BoolRepr) (S.litExpr b)
transConstVal _ty (Some (UsizeRepr)) (M.ConstInt i) =
    do let n = fromInteger (M.fromIntegerLit i)
       return $ MirExp UsizeRepr (S.app $ usizeLit n)
transConstVal _ty (Some (IsizeRepr)) (ConstInt i) =
      return $ MirExp IsizeRepr (S.app $ isizeLit (fromIntegerLit i))

--
-- This code handles slice references, both for ordinary array slices
-- and string slices. (These differ from ordinary references in having
-- a length.)  It needs to look up the definition ID, and then:
--    * extract the type from the global variable it finds
--      (note that it'll be a MirVectorRepr that it needs to unwrap)
--    * construct a reference to the global variable
--      (with globalMirRef rather than constMirRef, that's the point of
--      all this)
--    * apply subindexRef as above
--    * cons up the length
--    * call mkStruct
--    * cons up the final MirExp
--
-- staticSlicePlace does the first four of these actions; addrOfPlace
-- does the last two.
--
transConstVal (M.TyRef (M.TySlice ty) _) (Some MirSliceRepr) (M.ConstSliceRef defid len) = do
    Some tpr <- tyToReprM ty
    place <- staticSlicePlace len (Some tpr) defid
    addrOfPlace place
transConstVal (M.TyRef M.TyStr _) (Some MirSliceRepr) (M.ConstSliceRef defid len) = do
    let tpr = C.BVRepr $ knownNat @8
    place <- staticSlicePlace len (Some tpr) defid
    addrOfPlace place

transConstVal _ty (Some MirAggregateRepr) (M.ConstStrBody bs) = do
    let bytes = map (\b -> R.App (eBVLit (knownNat @8) (toInteger b))) (BS.unpack bs)
    ag <- mirAggregate_uninit_constSize (fromIntegral $ length bytes)
    -- TODO: hardcoded size=1
    ag' <- foldM
        (\ag' (i, b) -> mirAggregate_set i 1 knownRepr b ag')
        ag (zip [0..] bytes)
    return $ MirExp MirAggregateRepr ag'

transConstVal (M.TyArray ty _sz) (Some MirAggregateRepr) (M.ConstArray arr) = do
    Some tpr <- tyToReprM ty
    arr' <- Trav.for arr $ \e -> do
        MirExp tpr' e' <- transConstVal ty (Some tpr) e
        Refl <- testEqualityOrFail tpr tpr' $
            "transConstVal (ConstArray): returned wrong type: expected " ++
            show tpr ++ ", got " ++ show tpr'
        pure e'
    ag <- mirAggregate_uninit_constSize (fromIntegral $ length arr')
    -- TODO: hardcoded size=1
    ag' <- foldM
        (\ag' (i, x) -> mirAggregate_set i 1 tpr x ag')
        ag (zip [0..] arr')
    return $ MirExp MirAggregateRepr ag'

transConstVal _ty (Some (C.BVRepr w)) (M.ConstChar c) =
    do let i = toInteger (Char.ord c)
       return $ MirExp (C.BVRepr w) (S.app $ eBVLit w i)
transConstVal _ty (Some C.UnitRepr) (M.ConstFunction _did) =
    return $ MirExp C.UnitRepr $ S.app E.EmptyApp
transConstVal _ty (Some C.UnitRepr) (M.ConstTuple []) =
    return $ MirExp C.UnitRepr $ S.app E.EmptyApp
transConstVal (M.TyTuple tys) (Some MirAggregateRepr) (M.ConstTuple vals) =
    transConstTuple tys vals
transConstVal (M.TyClosure upvar_tys) (Some MirAggregateRepr) (M.ConstClosure upvar_vals) =
    transConstTuple upvar_tys upvar_vals

transConstVal _ty (Some (C.RealValRepr)) (M.ConstFloat (M.FloatLit _ str)) =
    case reads str of
      (d , _):_ -> let rat = toRational (d :: Double) in
                   return (MirExp C.RealValRepr (S.app $ E.RationalLit rat))
      []        -> mirFail $ "cannot parse float constant: " ++ show str

transConstVal _ty _ (ConstInitializer funid) =
    callExp funid []
transConstVal _ty _ (ConstStaticRef did) =
    staticPlace did >>= addrOfPlace
transConstVal ty _ ConstZST = initialValue ty >>= \case
    Just x -> return x
    Nothing -> mirFail $
        "failed to evaluate ZST constant of type " ++ show ty ++ " (initialValue failed)"
transConstVal _ty (Some MirReferenceRepr) (ConstRawPtr i) =
    MirExp MirReferenceRepr <$> integerToMirRef (R.App $ usizeLit i)
transConstVal ty@(M.TyAdt aname _ _) tpr (ConstStruct fields) = do
    adt <- findAdt aname
    col <- use $ cs . collection
    case findReprTransparentField col adt of
        Just idx ->
            transTransparentVal ty tpr adt fields idx
        Nothing -> do
            let fieldDefs = adt ^. adtvariants . ix 0 . vfields
            let fieldTys = map (\f -> f ^. fty) fieldDefs
            exps <- zipWithM (\val ty' -> tyToReprM ty' >>= \rpr -> transConstVal ty' rpr val) fields fieldTys
            buildStruct adt exps

transConstVal ty@(M.TyAdt aname _ _) tpr (ConstEnum variant fields) = do
    adt <- findAdt aname
    col <- use $ cs . collection
    case findReprTransparentField col adt of
        Just idx ->
            transTransparentVal ty tpr adt fields idx
        Nothing -> do
            let fieldDefs = adt ^. adtvariants . ix variant . vfields
            let fieldTys = map (\f -> f ^. fty) fieldDefs
            exps <- zipWithM (\val ty' -> tyToReprM ty' >>= \rpr -> transConstVal ty' rpr val) fields fieldTys
            buildEnum adt variant exps
transConstVal ty (Some MirReferenceRepr) cv = do
    let pointeeTy = M.typeOfProj M.Deref ty
    Some tpr <- tyToReprM pointeeTy
    MirExp tpr' val <- transConstVal pointeeTy (Some tpr) cv
    Refl <- testEqualityOrFail tpr tpr' $
        "transConstVal returned wrong type: expected " ++ show tpr ++ ", got " ++ show tpr'
    ref <- constMirRef tpr val
    return $ MirExp MirReferenceRepr ref
transConstVal _ty (Some tpr@(C.FunctionHandleRepr argTys retTy)) (ConstFnPtr did) = do
    mbHndl <- resolveFn did
    case mbHndl of
        Just (MirHandle _ _ hndl) -> do
            Refl <- testEqualityOrFail argTys (FH.handleArgTypes hndl) $ unlines
                [ "transConstVal (ConstFnPtr): argument types mismatch"
                , "expected: " ++ show argTys
                , "actual:   " ++ show (FH.handleArgTypes hndl)
                , "def id:   " ++ show did
                ]
            Refl <- testEqualityOrFail retTy (FH.handleReturnType hndl) $ unlines
                [ "transConstVal (ConstFnPtr): return type mismatch"
                , "expected: " ++ show retTy
                , "actual:   " ++ show (FH.handleReturnType hndl)
                , "def id:   " ++ show did
                ]
            return $ MirExp tpr $ R.App $ E.HandleLit hndl
        Nothing -> mirFail $
            "transConstVal (ConstFnPtr): Couldn't resolve function " ++ show did
transConstVal ty tp cv = mirFail $
    "fail or unimp constant: " ++ show ty ++ " (" ++ show tp ++ ") " ++ show cv

-- Translate a constant (non-empty) tuple or constant closure value.
transConstTuple :: [M.Ty] -> [ConstVal] -> MirGenerator h s ret (MirExp s)
transConstTuple tys vals = do
    exps <- forM (zip tys vals) $ \(ty, val) -> do
        Some tpr <- tyToReprM ty
        transConstVal ty (Some tpr) val
    buildTupleMaybeM tys (map Just exps)

-- Translate a struct or enum marked with repr(transparent).
transTransparentVal ::
  M.Ty {- The transparent struct or enum type (only used for error messages) -} ->
  Some C.TypeRepr {- The Crucible representation of the transparent struct or
                     enum type. -} ->
  Adt {- The transparent struct or enum's Adt description. -} ->
  [ConstVal] {- The field values of the transparent struct or enum variant.
                Really, it should only be a single field value, but we must
                check that this is actually the case. -} ->
  Int {- The index of the underlying field in the variant. -} ->
  MirGenerator h s ret (MirExp s)
transTransparentVal ty tpr adt fields idx = do
    ty' <- case adt ^? adtvariants . ix 0 . vfields . ix idx . fty of
        Just x -> return x
        Nothing -> mirFail $ "repr(transparent) field index " ++ show idx ++
            " out of range for " ++ show (pretty ty)
    constant <- case fields ^? ix idx of
        Just x -> return x
        Nothing -> mirFail $ "repr(transparent) field index " ++ show idx ++
            " out of range for " ++ show (pretty ty') ++ " initializer"
    transConstVal ty' tpr constant

typedVarInfo :: HasCallStack => Text -> C.TypeRepr tp -> MirGenerator h s ret (VarInfo s tp)
typedVarInfo name tpr = do
    optV <- use $ varMap . at name
    case optV of
        Nothing -> mirFail $
            "variable " ++ show name ++ " not found"
        Just (Some vi) -> do
            let tpr' = varInfoRepr vi
            Refl <- testEqualityOrFail tpr tpr' $
                "expected var " ++ show name ++ " to have type " ++ show tpr
                    ++ ", but it has type " ++ show tpr' ++ " instead"
            return vi

readVar :: C.TypeRepr tp -> VarInfo s tp -> MirGenerator h s ret (R.Expr MIR s tp)
readVar tpr vi = do
    case vi of
        VarRegister reg -> G.readReg reg
        VarReference _ reg -> G.readReg reg >>= readMirRef tpr
        VarAtom a -> return $ R.AtomExpr a

varExp :: HasCallStack => M.Var -> MirGenerator h s ret (MirExp s)
varExp (M.Var vname' _ vty _) = do
    Some tpr <- tyToReprM vty
    vi <- typedVarInfo vname' tpr
    x <- readVar tpr vi
    return $ MirExp tpr x

varPlace :: HasCallStack => M.Var -> MirGenerator h s ret (MirPlace s)
varPlace (M.Var vname' _ vty _) = do
    Some tpr <- tyToReprM vty
    vi <- typedVarInfo vname' tpr
    r <- case vi of
        VarReference _ reg -> G.readReg reg
        -- TODO: these cases won't be needed once immutable ref support is done
        -- - make them report an error instead
        VarRegister reg -> do
            x <- G.readReg reg
            r <- constMirRef tpr x
            return r
        VarAtom a -> do
            r <- constMirRef tpr $ R.AtomExpr a
            return r
    return $ MirPlace tpr r NoMeta

staticPlace :: HasCallStack => M.DefId -> MirGenerator h s ret (MirPlace s)
staticPlace did = do
    sm <- use $ cs.staticMap
    case Map.lookup did sm of
        Just (StaticVar gv) ->
            MirPlace (G.globalType gv) <$> globalMirRef gv <*> pure NoMeta
        Nothing -> mirFail $ "cannot find static variable " ++ fmt did

-- variant of staticPlace for slices
-- tpr is the element type; len is the length
staticSlicePlace ::
    HasCallStack =>
    Int ->
    Some C.TypeRepr ->
    M.DefId ->
    MirGenerator h s ret (MirPlace s)
staticSlicePlace len (Some tpr) did = do
    sm <- use $ cs.staticMap
    case Map.lookup did sm of
        Just (StaticVar gv) -> do
            let tpr_found = G.globalType gv
            -- TODO: why is `() <- ...` needed here?
            () <- case tpr_found of
                MirAggregateRepr -> return ()
                _ -> mirFail $
                    "staticSlicePlace: wrong type: expected vector, found " ++ show tpr_found
            ref <- globalMirRef gv
            ref' <- subindexRef tpr ref (R.App $ usizeLit 0)
            let len' = R.App $ usizeLit $ fromIntegral len
            return $ MirPlace tpr ref' (SliceMeta len')
        Nothing -> mirFail $ "cannot find static variable " ++ fmt did

-- NOTE: The return var in the MIR output is always "_0"
getReturnExp :: HasCallStack => C.TypeRepr ret -> MirGenerator h s ret (R.Expr MIR s ret)
getReturnExp tpr = do
    vi <- typedVarInfo "_0" tpr
    readVar tpr vi


-- ** Expressions: Operations and Aggregates

evalOperand :: HasCallStack => M.Operand -> MirGenerator h s ret (MirExp s)
evalOperand (M.Copy lv) = evalPlace lv >>= readPlace
evalOperand (M.Move lv) = evalPlace lv >>= readPlace
evalOperand (M.OpConstant (M.Constant conty constval)) = do
    Some tpr <- tyToReprM conty
    transConstVal conty (Some tpr) constval
evalOperand (M.Temp rv) = evalRval rv

-- | Dereference a `MirExp` (which must be `MirReferenceRepr` pointing to a
-- sized type), producing a `MirPlace`.
derefExp :: HasCallStack => M.Ty -> MirExp s -> MirGenerator h s ret (MirPlace s)
derefExp pointeeTy (MirExp MirReferenceRepr e) = do
    Some tpr <- tyToReprM pointeeTy
    return $ MirPlace tpr e NoMeta
derefExp _pointeeTy (MirExp tpr _) = mirFail $ "don't know how to deref " ++ show tpr

readPlace :: HasCallStack => MirPlace s -> MirGenerator h s ret (MirExp s)
readPlace (MirPlace tpr r NoMeta) = MirExp tpr <$> readMirRef tpr r
readPlace (MirPlace tpr _ meta) =
    mirFail $ "don't know how to read from place with metadata " ++ show meta
        ++ " (type " ++ show tpr ++ ")"

addrOfPlace :: HasCallStack => MirPlace s -> MirGenerator h s ret (MirExp s)
addrOfPlace (MirPlace _tpr r NoMeta) = return $ MirExp MirReferenceRepr r
addrOfPlace (MirPlace _tpr r (SliceMeta len)) =
    return $ MirExp MirSliceRepr $ mkSlice r len
addrOfPlace (MirPlace _tpr r (DynMeta vtable)) =
    return $ MirExp DynRefRepr $
      R.App $ E.MkStruct DynRefCtx $
      Ctx.Empty Ctx.:> r Ctx.:> vtable


-- Given two bitvectors, extend the length of the shorter one so that they
-- have the same length
-- Use the sign of the first bitvector to determine how to sign extend
extendToMax :: (1 <= n, 1 <= m) =>
               NatRepr n -> G.Expr MIR s (C.BVType n) ->
               NatRepr m -> G.Expr MIR s (C.BVType m) -> Maybe M.ArithType ->
   (forall n'. (1 <= n') => NatRepr n' -> G.Expr MIR s (C.BVType n') -> G.Expr MIR s (C.BVType n') -> a) -> a
extendToMax n e1 m e2 (Just arith) k =
   let extend :: (1 <= w, 1 <= r, w + 1 <= r) => (NatRepr r)
         -> (NatRepr w)
         -> (f (C.BVType w))
         -> E.App MIR f (C.BVType r)
       extend = case arith of
                  M.Signed   -> E.BVSext
                  M.Unsigned -> E.BVZext
   in case testEquality n m of
      Just Refl -> k n e1 e2
      Nothing   -> case testLeq (incNat n) m of
                      Just LeqProof ->
                         k m (S.app $ extend m n e1) e2
                      Nothing -> case testLeq (incNat m) n of
                          Just LeqProof ->
                              k n e1 (S.app $ extend n m e2)
                          Nothing -> error "impossible case"
extendToMax n e1 m e2 Nothing k =
   case testEquality n m of
      Just Refl -> k n e1 e2
      Nothing   -> error "don't know the sign"



transBinOp :: M.BinOp -> M.Operand -> M.Operand -> MirGenerator h s ret (MirExp s)
transBinOp bop op1 op2 = do
    me1 <- evalOperand  op1
    me2 <- evalOperand  op2
    let mat = M.arithType op1 `mplus` M.arithType op2
    case bop of
        Unchecked bop' -> do
            (res, overflow) <- evalBinOp bop' mat me1 me2
            G.assertExpr (S.notExpr overflow) $
              S.litExpr $
              "Binary operation (" <> Text.pack (show (pretty bop')) <>
              ") would overflow"
            pure res
        WithOverflow bop' -> do
            (res, overflow) <- evalBinOp bop' mat me1 me2
            buildTupleM [typeOf op1, TyBool] [res, MirExp C.BoolRepr overflow]
        _ -> fst <$> evalBinOp bop mat me1 me2

-- Evaluate a binop, returning both the result and an overflow flag.
evalBinOp :: forall h s ret. M.BinOp -> Maybe M.ArithType -> MirExp s -> MirExp s ->
    MirGenerator h s ret (MirExp s, R.Expr MIR s C.BoolType)
evalBinOp bop mat me1 me2 =
    case (me1, me2) of
      (MirExp ty1@(C.BVRepr na) e1a, MirExp ty2@C.NatRepr e2a) ->
         case (bop, mat) of
            (M.Shl, _) -> do
                let e2bv = S.app (E.IntegerToBV na (S.app (E.NatToInteger e2a)))
                return (MirExp (C.BVRepr na) (S.app $ E.BVShl na e1a e2bv),
                    shiftOverflowNat na e2a)
            (M.Shr, Just M.Unsigned) -> do
                let e2bv = S.app (E.IntegerToBV na (S.app (E.NatToInteger e2a)))
                return (MirExp (C.BVRepr na) (S.app $ E.BVLshr na e1a e2bv),
                    shiftOverflowNat na e2a)
            (M.Shr, Just M.Signed) -> do
                let e2bv = S.app (E.IntegerToBV na (S.app (E.NatToInteger e2a)))
                return (MirExp (C.BVRepr na) (S.app $ E.BVAshr na e1a e2bv),
                    shiftOverflowNat na e2a)

            _ -> mirFail $ "No translation for binop: " ++ show bop ++ " with " ++ show ty1 ++ " and " ++ show ty2
      (MirExp ty1@(C.BVRepr na) e1a, MirExp ty2@(C.BVRepr ma) e2a) ->
          -- In all cases except shifts, the inputs should already have the
          -- same width, and `extendToMax` is a no-op (except it provides the
          -- proof that `na` and `ma` are equal).  For shifts, the second input
          -- (shift amount) can have any width, so we pad one side or the other
          -- to make the widths match up.
          extendToMax na e1a ma e2a (mat) $ \ n e1 e2 ->
            case (bop, mat) of
              (M.Add, _) -> do
                let carry = case mat of
                        Just M.Unsigned -> E.BVCarry
                        Nothing -> E.BVCarry
                        Just M.Signed -> E.BVSCarry
                return (MirExp (C.BVRepr n) (S.app $ E.BVAdd n e1 e2), S.app $ carry n e1 e2)
              (M.Sub, _) -> do
                let borrow = case mat of
                        Just M.Unsigned -> E.BVUlt
                        Nothing -> E.BVUlt
                        Just M.Signed -> E.BVSBorrow
                return (MirExp (C.BVRepr n) (S.app $ E.BVSub n e1 e2), S.app $ borrow n e1 e2)
              (M.Mul, Just M.Unsigned) ->
                return (MirExp (C.BVRepr n) (S.app $ E.BVMul n e1 e2), umulOverflow n e1 e2)
              (M.Mul, Just M.Signed) ->
                return (MirExp (C.BVRepr n) (S.app $ E.BVMul n e1 e2), smulOverflow n e1 e2)
              (M.Div, Just M.Unsigned) ->
                return (MirExp (C.BVRepr n) (S.app $ E.BVUdiv n e1 e2), udivOverflow n e1 e2)
              (M.Div, Just M.Signed) ->
                return (MirExp (C.BVRepr n) (S.app $ E.BVSdiv n e1 e2), sdivOverflow n e1 e2)
              (M.Rem, Just M.Unsigned) ->
                return (MirExp (C.BVRepr n) (S.app $ E.BVUrem n e1 e2), udivOverflow n e1 e2)
              (M.Rem, Just M.Signed) ->
                return (MirExp (C.BVRepr n) (S.app $ E.BVSrem n e1 e2), sdivOverflow n e1 e2)
              -- Bitwise ops never overflow
              (M.BitXor, _) -> return (MirExp (C.BVRepr n) (S.app $ E.BVXor n e1 e2), noOverflow)
              (M.BitAnd, _) -> return (MirExp (C.BVRepr n) (S.app $ E.BVAnd n e1 e2), noOverflow)
              (M.BitOr, _) -> return (MirExp (C.BVRepr n) (S.app $ E.BVOr n e1 e2), noOverflow)
              -- Shift ops overflow when shift amount >= bit width
              -- If `extendToMax` padded the first argument, we need to
              -- truncate the result back down to its original width using
              -- `extendUnsignedBV`.
              --
              -- TODO: clean this up so it's more precise about how the
              -- operands get extended/truncated, instead of using the somewhat
              -- magical `extendToMax` / `extendUnsignedBV` functions.
              (M.Shl, _) -> do
                 res <- extendUnsignedBV (MirExp (C.BVRepr n) (S.app $ E.BVShl n e1 e2)) na
                 return (res, shiftOverflowBV na ma e2a)
              (M.Shr, Just M.Unsigned) -> do
                 res <- extendUnsignedBV (MirExp (C.BVRepr n) (S.app $ E.BVLshr n e1 e2)) na
                 return (res, shiftOverflowBV na ma e2a)
              (M.Shr, Nothing) -> do
                 res <- extendUnsignedBV (MirExp (C.BVRepr n) (S.app $ E.BVLshr n e1 e2)) na
                 return (res, shiftOverflowBV na ma e2a)
              (M.Shr, Just M.Signed) -> do
                 res <- extendSignedBV (MirExp (C.BVRepr n) (S.app $ E.BVAshr n e1 e2) ) na
                 return (res, shiftOverflowBV na ma e2a)
              -- Comparison ops never overflow
              (M.Lt, Just M.Unsigned) -> return (MirExp (C.BoolRepr) (S.app $ E.BVUlt n e1 e2), noOverflow)
              (M.Lt, Just M.Signed)   -> return (MirExp (C.BoolRepr) (S.app $ E.BVSlt n e1 e2), noOverflow)
              (M.Le, Just M.Unsigned) -> return (MirExp (C.BoolRepr) (S.app $ E.BVUle n e1 e2), noOverflow)
              (M.Le, Just M.Signed)   -> return (MirExp (C.BoolRepr) (S.app $ E.BVSle n e1 e2), noOverflow)

              (M.Gt, Just M.Unsigned) -> return (MirExp (C.BoolRepr) (S.app $ E.BVUlt n e2 e1), noOverflow)
              (M.Gt, Just M.Signed)   -> return (MirExp (C.BoolRepr) (S.app $ E.BVSlt n e2 e1), noOverflow)
              (M.Ge, Just M.Unsigned) -> return (MirExp (C.BoolRepr) (S.app $ E.BVUle n e2 e1), noOverflow)
              (M.Ge, Just M.Signed)   -> return (MirExp (C.BoolRepr) (S.app $ E.BVSle n e2 e1), noOverflow)

              (M.Ne, _) -> return (MirExp (C.BoolRepr) (S.app $ E.Not $ S.app $ E.BVEq n e1 e2), noOverflow)
              (M.Beq, _) -> return (MirExp (C.BoolRepr) (S.app $ E.BVEq n e1 e2), noOverflow)
              _ -> mirFail $ "No translation for binop: " ++ show bop ++ " " ++ show mat
                           ++ " for " ++ show ty1 ++ " and " ++ show ty2
      (MirExp C.BoolRepr e1, MirExp C.BoolRepr e2) ->
          case bop of
            M.BitAnd -> return (MirExp C.BoolRepr (S.app $ E.And e1 e2), noOverflow)
            M.BitXor -> return (MirExp C.BoolRepr (S.app $ E.BoolXor e1 e2), noOverflow)
            M.BitOr -> return (MirExp C.BoolRepr (S.app $ E.Or e1 e2), noOverflow)
            M.Beq -> return (MirExp C.BoolRepr (S.app $ E.Not $ S.app $ E.BoolXor e1 e2), noOverflow)
            M.Ne  -> return (MirExp C.BoolRepr (S.app $ E.BoolXor e1 e2), noOverflow)
            _ -> mirFail $ "No translation for bool binop: " ++ fmt bop
      (MirExp C.RealValRepr e1, MirExp C.RealValRepr e2) ->
          case bop of
            M.Beq -> return (MirExp C.BoolRepr (S.app $ E.RealEq e1 e2), noOverflow)
            M.Lt -> return (MirExp C.BoolRepr (S.app $ E.RealLt e1 e2), noOverflow)
            M.Le -> return (MirExp C.BoolRepr (S.app $ E.RealLe e1 e2), noOverflow)
            M.Gt -> return (MirExp C.BoolRepr (S.app $ E.RealLt e2 e1), noOverflow)
            M.Ge -> return (MirExp C.BoolRepr (S.app $ E.RealLe e2 e1), noOverflow)
            M.Ne -> return (MirExp C.BoolRepr (S.app $ E.Not $ S.app $ E.RealEq e1 e2), noOverflow)

            -- Binops on floats never set the overflow flag
            M.Add -> return (MirExp C.RealValRepr (S.app $ E.RealAdd e1 e2), noOverflow)
            M.Sub -> return (MirExp C.RealValRepr (S.app $ E.RealSub e1 e2), noOverflow)
            M.Mul -> return (MirExp C.RealValRepr (S.app $ E.RealMul e1 e2), noOverflow)
            M.Div -> return (MirExp C.RealValRepr (S.app $ E.RealDiv e1 e2), noOverflow)
            M.Rem -> return (MirExp C.RealValRepr (S.app $ E.RealMod e1 e2), noOverflow)

            _ -> mirFail $ "No translation for real number binop: " ++ fmt bop

      (MirExp MirReferenceRepr e1, MirExp MirReferenceRepr e2) ->
          case bop of
            M.Beq -> do
                eq <- mirRef_eq e1 e2
                return (MirExp C.BoolRepr eq, noOverflow)
            M.Ne -> do
                eq <- mirRef_eq e1 e2
                return (MirExp C.BoolRepr $ S.app $ E.Not eq, noOverflow)
            _ -> mirFail $ "No translation for pointer binop: " ++ fmt bop

      (MirExp MirReferenceRepr e1, MirExp UsizeRepr e2) -> do
          newRef <- mirRef_offsetWrap e1 e2
          return (MirExp MirReferenceRepr newRef, noOverflow)

      (_, _) -> mirFail $ "bad or unimplemented type: " ++ (fmt bop) ++ ", " ++ (show me1) ++ ", " ++ (show me2)

  where
    noOverflow :: R.Expr MIR s C.BoolType
    noOverflow = S.app $ E.BoolLit False

    -- Check whether unsigned multiplication of `e1 * e2` overflows `w` bits.
    -- If `zext e1 * zext e2 /= zext (e1 * e2)`, then overflow has occurred.
    mulOverflow :: forall w. (1 <= w, 1 <= w + w) =>
        NatRepr w ->
        (R.Expr MIR s (C.BVType w) -> R.Expr MIR s (C.BVType (w + w))) ->
        R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s C.BoolType
    mulOverflow w ext e1 e2 = S.app $ E.Not $ S.app $ E.BVEq w'
        (S.app $ E.BVMul w' (ext e1) (ext e2))
        (ext $ S.app $ E.BVMul w e1 e2)
      where w' = addNat w w

    umulOverflow :: forall w. (1 <= w) =>
        NatRepr w -> R.Expr MIR s (C.BVType w) -> R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s C.BoolType
    umulOverflow w e1 e2
      | LeqProof <- leqAdd2 (leqRefl w) (LeqProof @1 @w),
        LeqProof <- dblPosIsPos (LeqProof @1 @w) =
        mulOverflow w (S.app . E.BVZext (addNat w w) w) e1 e2
    smulOverflow :: forall w. (1 <= w) =>
        NatRepr w -> R.Expr MIR s (C.BVType w) -> R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s C.BoolType
    smulOverflow w e1 e2
      | LeqProof <- leqAdd2 (leqRefl w) (LeqProof @1 @w),
        LeqProof <- dblPosIsPos (LeqProof @1 @w) =
        mulOverflow w (S.app . E.BVSext (addNat w w) w) e1 e2

    -- Check that shift amount `e` is less than the input width `w`.
    shiftOverflowNat w e =
        let wLit = S.app $ E.NatLit $ natValue w
        in S.app $ E.Not $ S.app $ E.NatLt e wLit
    -- Check that shift amount `e` (whose width in `w'`) is less than the input
    -- width `w`.
    shiftOverflowBV :: (1 <= w') =>
        NatRepr w -> NatRepr w' -> R.Expr MIR s (C.BVType w') -> R.Expr MIR s C.BoolType
    shiftOverflowBV w w' e =
        let wLit = S.app $ eBVLit w' $ intValue w
        in S.app $ E.Not $ S.app $ E.BVUlt w' e wLit

    udivOverflow :: (1 <= w) =>
        NatRepr w ->
        R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s C.BoolType
    udivOverflow w _x y = S.app $ E.BVEq w y $ S.app $ eBVLit w 0

    sdivOverflow :: (1 <= w) =>
        NatRepr w ->
        R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s (C.BVType w) ->
        R.Expr MIR s C.BoolType
    sdivOverflow w x y =
        S.app $ E.Or (udivOverflow w x y) $
            -- Are we dividing INT_MIN by -1?  E.g. `x == -128 && y == -1`
            S.app $ E.And
                (S.app $ E.BVEq w x $ S.app $ eBVLit w (1 `shiftL` (w' - 1)))
                (S.app $ E.BVEq w y $ S.app $ eBVLit w ((1 `shiftL` w') - 1))
      where w' = fromIntegral $ intValue w

-- Nullary ops in rust are used for resource allocation, so are not interpreted
transNullaryOp ::  M.NullOp -> M.Ty -> MirGenerator h s ret (MirExp s)
transNullaryOp nop ty =
  case nop of
    M.AlignOf -> getLayoutFieldAsMirExp "AlignOf" layAlign ty
    M.SizeOf -> getLayoutFieldAsMirExp "SizeOf" laySize ty
    M.UbChecks -> do
      -- Disable undefined behavior checks.
      -- TODO: re-enable this later, and fix the tests that break
      -- (see https://github.com/GaloisInc/mir-json/issues/107)
      return $ MirExp C.BoolRepr $ R.App $ E.BoolLit False

transUnaryOp :: M.UnOp -> M.Operand -> MirGenerator h s ret (MirExp s)
transUnaryOp uop op = do
    mop <- evalOperand op
    case (uop, mop) of
      (M.Not, MirExp C.BoolRepr e) -> return $ MirExp C.BoolRepr $ S.app $ E.Not e
      (M.Not, MirExp (C.BVRepr n) e) -> return $ MirExp (C.BVRepr n) $ S.app $ E.BVNot n e
      (M.Neg, MirExp (C.BVRepr n) e) -> return $ MirExp (C.BVRepr n) (S.app $ E.BVSub n (S.app $ eBVLit n 0) e)
      (M.Neg, MirExp C.IntegerRepr e) -> return $ MirExp C.IntegerRepr $ S.app $ E.IntNeg e
      (M.Neg, MirExp C.RealValRepr e) -> return $ MirExp C.RealValRepr $ S.app $ E.RealNeg e
      (M.PtrMetadata, MirExp MirSliceRepr e) -> return $ MirExp UsizeRepr $ getSliceLen e
      (_ , MirExp ty _) -> mirFail $ "Unimplemented unary op `" ++ fmt uop ++ "' for " ++ show ty


-- a -> u -> [a;u]
buildRepeat :: M.Operand -> M.ConstUsize -> MirGenerator h s ret (MirExp s)
buildRepeat op size = do
    MirExp tpr e <- evalOperand op
    let n = fromInteger size
    -- TODO: hardcoded size=1
    ag <- mirAggregate_uninit_constSize n
    ag' <- foldM
        (\ag' i -> mirAggregate_set i 1 tpr e ag')
        ag (init [0 .. n])
    return $ MirExp MirAggregateRepr ag'




-- casts

-- | Make sure that the expression has exactly the bitwidth requested. If the BV is too short, extend. If too long, truncate.
extendUnsignedBV :: (1 <= w) => MirExp s -> NatRepr w -> MirGenerator h s ret (MirExp s)
extendUnsignedBV (MirExp tp e) w =
    case tp of
      (C.BVRepr n) | Just Refl <- testEquality w n ->
                return $ MirExp tp e
      (C.BVRepr n) | Just LeqProof <- testLeq (incNat w) n ->
                return $ MirExp (C.BVRepr w) (S.app $ E.BVTrunc w n e)
      (C.BVRepr n) | Just LeqProof <- testLeq (incNat n) w ->
                return $ MirExp (C.BVRepr w) (S.app $ E.BVZext w n e)
      _ -> mirFail ("unimplemented unsigned bvext: " ++ show tp ++ "  " ++ show w)

extendSignedBV :: (1 <= w) => MirExp s -> NatRepr w -> MirGenerator h s ret (MirExp s)
extendSignedBV (MirExp tp e) w =
    case tp of
      (C.BVRepr n) | Just Refl <- testEquality w n ->
                return $ MirExp tp e
      (C.BVRepr n) | Just LeqProof <- testLeq (incNat w) n ->
                return $ MirExp (C.BVRepr w) (S.app $ E.BVTrunc w n e)
      (C.BVRepr n) | Just LeqProof <- testLeq (incNat n) w ->
                return $ MirExp (C.BVRepr w) (S.app $ E.BVSext w n e)
      _ -> mirFail $ "unimplemented signed bvext " ++ show tp ++ " " ++ show w


evalCast' :: forall h s ret. HasCallStack => M.CastKind -> M.Ty -> MirExp s -> M.Ty -> MirGenerator h s ret (MirExp s)
evalCast' ck ty1 e ty2  = do
    col <- use $ cs . collection
    case (ck, ty1, ty2) of
      (M.Misc,a,b) | a == b -> return e

      (M.Misc, M.TyUint M.USize, M.TyInt M.USize)
       | MirExp UsizeRepr e0 <- e
       -> return $ MirExp IsizeRepr (usizeToIsize R.App e0)
      (M.Misc, M.TyInt M.USize, M.TyUint M.USize)
       | MirExp IsizeRepr e0 <- e
       -> return $ MirExp UsizeRepr (isizeToUsize R.App e0)

      (M.Misc, M.TyUint _, M.TyInt  M.USize)
       | MirExp (C.BVRepr sz) e0 <- e
       -> return $ MirExp IsizeRepr (bvToIsize sz R.App e0)

      (M.Misc, M.TyUint _, M.TyUint  M.USize)
       | MirExp (C.BVRepr sz) e0 <- e
       -> return $ MirExp UsizeRepr (bvToUsize sz R.App e0)

      (M.Misc, M.TyInt _, M.TyInt  M.USize)
       | MirExp (C.BVRepr sz) e0 <- e
       -> return $ MirExp IsizeRepr (sbvToIsize sz R.App e0)

      (M.Misc, M.TyInt _, M.TyUint  M.USize)
       | MirExp (C.BVRepr sz) e0 <- e
       -> return $ MirExp UsizeRepr (sbvToUsize sz R.App e0)

      (M.Misc, M.TyUint M.USize, M.TyUint bsz)
       | MirExp UsizeRepr e0 <- e
       -> baseSizeToNatCont bsz $ \w -> return $
         MirExp (C.BVRepr w) (usizeToBv w R.App e0)

      (M.Misc, M.TyInt M.USize, M.TyUint bsz)
       | MirExp IsizeRepr e0 <- e
       -> baseSizeToNatCont bsz $ \w -> return $
         MirExp (C.BVRepr w) (isizeToBv w R.App e0)

      (M.Misc, M.TyUint M.USize, M.TyInt bsz)
       | MirExp UsizeRepr e0 <- e
       -> baseSizeToNatCont bsz $ \w -> return $
         MirExp (C.BVRepr w) (usizeToBv w R.App e0)

      (M.Misc, M.TyInt M.USize, M.TyInt bsz)
       | MirExp IsizeRepr e0 <- e
       -> baseSizeToNatCont bsz $ \w -> return $
         MirExp (C.BVRepr w) (isizeToBv w R.App e0)

      (M.Misc, M.TyUint _, M.TyUint s) -> baseSizeToNatCont s $ extendUnsignedBV e
      (M.Misc, M.TyInt _,  M.TyInt s)  -> baseSizeToNatCont s $ extendSignedBV e

      -- unsigned to signed (nothing to do except fix sizes)
      (M.Misc, M.TyUint _, M.TyInt s)  -> baseSizeToNatCont s $ extendUnsignedBV e

      -- signed to unsigned.  Testing indicates that this sign-extends.
      (M.Misc, M.TyInt _,  M.TyUint s) -> baseSizeToNatCont s $ extendSignedBV e

       -- boolean to nat
      (M.Misc, TyBool, TyUint M.USize)
       | MirExp C.BoolRepr e0 <- e
       -> return $ MirExp UsizeRepr (R.App $ usizeIte e0 (R.App $ usizeLit 1) (R.App $ usizeLit 0))
      (M.Misc, TyBool, TyInt M.USize)

       -- boolean to integer
       | MirExp C.BoolRepr e0 <- e
       -> return $ MirExp IsizeRepr (R.App $ isizeIte e0 (R.App $ isizeLit 1) (R.App $ isizeLit 0))

      -- booleans to BVs
      (M.Misc, TyBool, TyUint bsz)
       | MirExp C.BoolRepr e0 <- e
       -> baseSizeToNatCont bsz $ \w ->
           return $ MirExp (C.BVRepr w) (R.App $ E.BVIte e0 w (R.App $ eBVLit w 1) (R.App $ eBVLit w 0))
      (M.Misc, TyBool, TyInt bsz)
       | MirExp C.BoolRepr e0 <- e
       -> baseSizeToNatCont bsz $ \w ->
           return $ MirExp (C.BVRepr w) (R.App $ E.BVIte e0 w (R.App $ eBVLit w 1) (R.App $ eBVLit w 0))

      -- char to usize
      (M.Misc, M.TyChar, M.TyUint  M.USize)
       | MirExp (C.BVRepr sz) e0 <- e
       -> return $ MirExp UsizeRepr (bvToUsize sz R.App e0)
      -- char to other uint
      (M.Misc, M.TyChar, M.TyUint s) -> baseSizeToNatCont s $ extendUnsignedBV e

      -- byte to char
      (M.Misc, M.TyUint B8, M.TyChar) -> baseSizeToNatCont M.B32 $ extendUnsignedBV e



{-      -- BV to Float
      (M.Misc, M.TyInt bsz, TyFloat fsz)
       | MirExp (C.BVRepr sz) e0 <- e
       -> return $ MirExp C.FloatRepr -}

      -- Not sure why this appears in generated MIR, but libcore has some no-op
      -- unsizes from `*const dyn Any` to `*const dyn Any`
      -- TODO: Remove this completely.
      (M.Unsize,a,b) | a == b -> return e

      -- ADT -> ADT unsizing is done via `CoerceUnsized`, and handled here.
      -- Reference-to-ADT -> reference-to-ADT casting is handled separately,
      -- below.
      (M.Unsize, M.TyAdt aname1 _ _, M.TyAdt aname2 _ _) ->
        coerceUnsized ck aname1 aname2 e
      (M.UnsizeVtable _, M.TyAdt aname1 _ _, M.TyAdt aname2 _ _) ->
        coerceUnsized ck aname1 aname2 e

      (M.Unsize, M.TyRef (M.TyArray tp sz) _, M.TyRef (M.TySlice tp') _) ->
        unsizeArray tp sz tp'
      (M.Unsize, M.TyRawPtr (M.TyArray tp sz) _, M.TyRawPtr (M.TySlice tp') _) ->
        unsizeArray tp sz tp'

      -- Trait object creation from a ref
      (M.UnsizeVtable vtbl, M.TyRef _ _,
        M.TyRef (M.TyDynamic traitName') _) ->
          mkTraitObject traitName' vtbl e
      (M.UnsizeVtable vtbl, M.TyRawPtr _ _,
        M.TyRawPtr (M.TyDynamic traitName') _) ->
          mkTraitObject traitName' vtbl e

      -- Casting between TyDynamics that vary only in their auto traits
      -- TODO: this should also normalize the TraitProjection predicates, to
      -- allow casting between equivalent descriptions of the same trait object
      (M.Unsize, M.TyRef (M.TyDynamic t1) _, M.TyRef (M.TyDynamic t2) _)
        | t1 == t2
        -> return e

      (M.Unsize, M.TyRef _ _, M.TyRef (M.TyDynamic _) _) ->
        mirFail $ unlines $
          [ "error when casting:"
          , "  ty: " <> show ty1
          , "  as: " <> show ty2
          , "expected `UnsizeVtable` cast kind, but saw `Unsize` cast kind" ]
      (M.Unsize, M.TyRawPtr _ _, M.TyRawPtr (M.TyDynamic _) _) ->
        mirFail $ unlines $
          [ "error when casting:"
          , "  ty: " <> show ty1
          , "  as: " <> show ty2
          , "expected `UnsizeVtable` cast kind, but saw `Unsize` cast kind" ]

      -- trait object cast down to underlying object reference (forgetting vtable)
      (M.Misc, M.TyRawPtr (M.TyDynamic _) _, M.TyRawPtr _ _)
        | Right (Some MirReferenceRepr) <- tyToRepr col ty2
        , MirExp DynRefRepr a <- e
        -> pure (MirExp MirReferenceRepr (R.App (E.GetStruct a dynRefDataIndex MirReferenceRepr)))

      -- Unsized casts from references to sized structs to references to DSTs.
      -- We defer to the provided cast kind to determine what kind of unsizing
      -- cast we expect to perform, i.e. what kind of metadata to include in the
      -- created fat pointer.
      (M.Unsize, M.TyRef (M.TyAdt an1 _ _) m1, M.TyRef (M.TyAdt an2 _ _) m2) ->
        unsizeAdtSlice M.TyRef an1 m1 an2 m2
      (M.Unsize, M.TyRawPtr (M.TyAdt an1 _ _) m1, M.TyRawPtr (M.TyAdt an2 _ _) m2) ->
        unsizeAdtSlice M.TyRawPtr an1 m1 an2 m2
      (M.UnsizeVtable vtable, M.TyRef (M.TyAdt an1 _ _) m1, M.TyRef (M.TyAdt an2 _ _) m2) ->
        unsizeAdtDyn vtable M.TyRef an1 m1 an2 m2
      (M.UnsizeVtable vtable, M.TyRawPtr (M.TyAdt an1 _ _) m1, M.TyRawPtr (M.TyAdt an2 _ _) m2) ->
        unsizeAdtDyn vtable M.TyRawPtr an1 m1 an2 m2

      -- C-style adts, casting an enum value to a TyInt
      (M.Misc, M.TyAdt aname _ _, M.TyInt sz) -> do
        adt <- findAdt aname
        discr <- enumDiscriminant adt e
        evalCast' M.Misc (M.TyInt M.USize) discr (M.TyInt sz)
      (M.Misc, M.TyAdt aname _ _, M.TyUint sz) -> do
        adt <- findAdt aname
        discr <- enumDiscriminant adt e
        evalCast' M.Misc (M.TyInt M.USize) discr (M.TyUint sz)

      -- References have the same representation as Raw pointers
      (M.Misc, M.TyRef ty1' mut1, M.TyRawPtr ty2' mut2)
         | ty1' == ty2' && mut1 == mut2 -> return e

      (M.MutToConstPointer, M.TyRawPtr ty1' M.Mut, M.TyRawPtr ty2' M.Immut)
         | ty1' == ty2' -> return e

      -- Integer-to-pointer casts.  Pointer-to-integer casts are not yet
      -- supported.
      (M.Misc, M.TyInt _, M.TyRawPtr _ _) -> transmuteExp e ty1 ty2
      (M.Misc, M.TyUint _, M.TyRawPtr _ _) -> transmuteExp e ty1 ty2

      --  *const [T] -> *T (discards the length and returns only the pointer)
      (M.Misc, M.TyRawPtr (M.TySlice t1) m1, M.TyRawPtr t2 m2)
        | t1 == t2, m1 == m2, MirExp MirSliceRepr e' <- e
        -> return $ MirExp MirReferenceRepr (getSlicePtr e')
      (M.Misc, M.TyRawPtr M.TyStr m1, M.TyRawPtr (M.TyUint M.B8) m2)
        | m1 == m2, MirExp MirSliceRepr e' <- e
        -> return $ MirExp MirReferenceRepr (getSlicePtr e')

      --  *const [T; N] -> *const T (get first element)
      (M.Misc, M.TyRawPtr (M.TyArray t1 _) m1, M.TyRawPtr t2 m2)
        | t1 == t2, m1 == m2, MirExp MirReferenceRepr e' <- e
        -> do
          Some tpr <- tyToReprM t1
          MirExp MirReferenceRepr <$> subindexRef tpr e' (R.App $ usizeLit 0)

      --  *const [u8] <-> *const str (no-ops)
      (M.Misc, M.TyRawPtr (M.TySlice (M.TyUint M.B8)) m1, M.TyRawPtr M.TyStr m2)
        | m1 == m2 -> return e
      (M.Misc, M.TyRawPtr M.TyStr m1, M.TyRawPtr (M.TySlice (M.TyUint M.B8)) m2)
        | m1 == m2 -> return e

      -- Arbitrary pointer-to-pointer casts are allowed as long as the source
      -- and destination types have the same Crucible representation.  This is
      -- similar to calling `transmute`.
      (M.Misc, M.TyRawPtr _ _, M.TyRawPtr _ _)
         | ty1 == ty2 -> return e
         | tyToRepr col ty1 == tyToRepr col ty2 -> return e

      (M.ReifyFnPointer, M.TyFnDef defId, M.TyFnPtr sig)
         -> do mhand <- lookupFunction defId
               case mhand of
                 Just (me, sig')
                   | sig == sig' -> return me
                   | otherwise -> mirFail $
                       "ReifyFnPointer: bad MIR: method handle has wrong sig: " ++
                       show (defId, sig, sig')
                 Nothing -> mirFail $
                        "ReifyFnPointer: bad MIR: can't find method handle: " ++
                        show defId

      (M.ClosureFnPointer shimDefId, M.TyClosure [], M.TyFnPtr sig)
         -> do mhand <- lookupFunction shimDefId
               case mhand of
                 Just (me, sig')
                   | sig == sig' -> return me
                   | otherwise -> mirFail $
                       "ClosureFnPointer: bad MIR: method handle has wrong sig: " ++
                       show (shimDefId, sig, sig')
                 Nothing -> mirFail $
                        "ClosureFnPointer: bad MIR: can't find method handle: " ++
                        show shimDefId

      (M.Transmute, _, _) -> transmuteExp e ty1 ty2

      -- This casts from a safe pointer to an unsafe one.
      -- Since we don't track safeness this is just a no-op for now, but if
      -- we decide to track that, this needs to be updated.
      (M.UnsafeFnPointer, _, _) | ty1 == ty2 -> pure e

      _ -> mirFail $ "unimplemented cast: " ++ (show ck) ++
        "\n  ty: " ++ (show ty1) ++ "\n  as: " ++ (show ty2)
  where
    -- | Attempt to access the repr(transparent) field types of the two structs,
    -- failing if only one is repr(transparent)
    reprTransparentFieldTys :: AdtName -> AdtName -> MirGenerator h s ret (Maybe (Ty, Ty))
    reprTransparentFieldTys an1 an2 = do
      col <- use $ cs . collection
      adt1 <- findAdt an1
      adt2 <- findAdt an2
      case (reprTransparentFieldTy col adt1, reprTransparentFieldTy col adt2) of
        (Just field1Ty, Just field2Ty) ->
          pure $ Just (field1Ty, field2Ty)
        (Nothing, Nothing) ->
          pure Nothing
        (Just _, Nothing) ->
          mirFail $ unwords
            [ "reprTransparentFieldTys: impossible:"
            , show $ adt1 ^. M.adtname, "was repr(transparent), but"
            , show $ adt2 ^. M.adtname, "was not" ]
        (Nothing, Just _) ->
          mirFail $ unwords
            [ "reprTransparentFieldTys: impossible:"
            , show $ adt2 ^. M.adtname, "was repr(transparent), but"
            , show $ adt1 ^. M.adtname, "was not" ]

    -- | Perform an unsized cast from a reference to a struct containing an
    -- array in its (transitively) last field to one containing a slice or @str@
    -- in the same position.
    unsizeAdtSlice ::
      (Ty -> Mutability -> Ty) ->
      AdtName -> Mutability ->
      AdtName -> Mutability ->
      MirGenerator h s ret (MirExp s)
    unsizeAdtSlice ref an1 m1 an2 m2 =
      reprTransparentFieldTys an1 an2 >>= \case
        Just (field1Ty, field2Ty) ->
          evalCast' ck (ref field1Ty m1) e (ref field2Ty m2)
        Nothing ->
          unsizeAdtSliceNormal an1 an2

    -- | `unsizeAdtSlice`, for non-@repr(transparent)@ structs.
    unsizeAdtSliceNormal :: AdtName  -> AdtName -> MirGenerator h s ret (MirExp s)
    unsizeAdtSliceNormal an1 an2 = do
      adtRef <- case e of
        MirExp MirReferenceRepr adtRef -> pure adtRef
        _ -> mirFail "unsizeAdtSlice called on non-reference"
      col <- use $ cs . collection

      -- We expect to be casting from an array-containing DST to a
      -- slice-containing DST. For the target of the cast to be a valid DST, the
      -- slice needs to be its last field (or its last field's last field),
      -- which means the source needs to have an array in the same position
      lenExpr <- case findLastFieldRec col an1 of
        Just field ->
          case field ^. M.fty of
            M.TyArray _elemTy len ->
              pure $ R.App $ usizeLit $ fromIntegral len
            _ ->
              mirFail "attempted Unsize cast from non-array source"
        Nothing ->
          mirFail $ "unsizedAdtSlice: unable to determine last field of " <> show an1

      -- Sanity-check that we are indeed casting to a type with a slice in the
      -- expected position
      let ref = MirExp MirSliceRepr (mkSlice adtRef lenExpr)
      case findLastFieldRec col an2 of
        Nothing ->
          mirFail $ "unsizedAdtSlice: unable to determine last field of " <> show an2
        Just field ->
          case field ^. M.fty of
            M.TySlice _elemTy -> pure ref
            _ -> mirFail "attempted Unsize cast to non-slice target"

    -- | Perform an unsized cast from a reference to a struct containing any
    -- initializable type in its (transitively) last field to one containing a
    -- trait object in the same position. The restriction on initializability
    -- makes it substantially easier to implement `Mir.TransTy.structFieldRef` -
    -- see that function for details.
    unsizeAdtDyn ::
      VtableName ->
      (Ty -> Mutability -> Ty) ->
      AdtName -> Mutability ->
      AdtName -> Mutability ->
      MirGenerator h s ret (MirExp s)
    unsizeAdtDyn vtable ref an1 m1 an2 m2 =
      reprTransparentFieldTys an1 an2 >>= \case
        Just (field1Ty, field2Ty) ->
          evalCast' ck (ref field1Ty m1) e (ref field2Ty m2)
        Nothing ->
          unsizeAdtDynNormal vtable an1 an2

    -- | `unsizeAdtDyn`, for non-@repr(transparent)@ structs.
    unsizeAdtDynNormal :: VtableName -> AdtName  -> AdtName -> MirGenerator h s ret (MirExp s)
    unsizeAdtDynNormal vtable castSource castTarget = do
      col <- use $ cs . collection
      eventualTraitObject <- case findLastFieldRec col castSource of
        Nothing ->
          mirFail $ "unsizedAdtDyn: unable to determine last field of " <> show castSource
        Just field ->
          pure (field ^. M.fty)
      -- `FkMaybe` fields are not initializable, and our rationale for
      -- prohibiting them here is described in `unsizeAdtDyn`, above, and
      -- `Mir.TransTy.structFieldRef`
      case tyToFieldRepr col eventualTraitObject of
        Left err -> mirFail ("unsizeAdtDynNormal: " ++ err)
        Right (Some (FieldRepr (FkMaybe _))) ->
          mirFail "error: unsizeAdtDyn with non-initializable unsized field"
        Right (Some (FieldRepr (FkInit _))) ->
          case findLastFieldRec col castTarget of
            Nothing ->
              mirFail $ "unsizedAdtDyn: unable to determine last field of " <> show castTarget
            Just field ->
              case field ^. M.fty of
                M.TyDynamic traitName' -> mkTraitObject traitName' vtable e
                _ -> mirFail "attempted UnsizeVtable cast with non-trait-object target"

    unsizeArray ty sz ty'
      | ty == ty', MirExp MirReferenceRepr ref <- e
      = do
        Some elem_tp <- tyToReprM ty
        let len   = R.App $ usizeLit (fromIntegral sz)
        ref' <- subindexRef elem_tp ref (R.App $ usizeLit 0)
        let tup   = S.mkStruct mirSliceCtxRepr
                        (Ctx.Empty Ctx.:> ref' Ctx.:> len)
        return $ MirExp MirSliceRepr tup
      | otherwise = mirFail $
        "Type mismatch in cast: " ++ show ck ++ " " ++ show ty1 ++ " as " ++ show ty2

    -- Implementation of the "coerce unsized" operation.  If `Foo<T>:
    -- CoerceUnsized<Foo<U>>`, then this operation is enabled for converting
    -- `Foo<T>` to `Foo<U>`.  The actual operation consists of disassembling
    -- the struct, coercing any raw pointers inside, and putting it back
    -- together again.
    coerceUnsized :: HasCallStack =>
        M.CastKind -> M.AdtName -> M.AdtName -> MirExp s -> MirGenerator h s ret (MirExp s)
    coerceUnsized ck' an1 an2 expr = do
        col <- use $ cs . collection
        adt1 <- findAdt an1
        adt2 <- findAdt an2
        case (reprTransparentFieldTy col adt1, reprTransparentFieldTy col adt2) of
            (Just ty1', Just ty2') ->
              -- The struct is #[repr(transparent)], so it has only one non-ZST
              -- field. This field must be the pointer/ref field being coerced,
              -- as rustc currently forbids implementing CoerceUnsized if it
              -- can't a field to coerce. Since this field is being coerced, its
              -- old and new types should never be equal. Because CoerceUnsized
              -- is unstable, a future version of rustc might change this
              -- behavior, so we leave this check here in place as a safeguard.
              if ty1' == ty2'
                then pure expr
                else evalCast' ck' ty1' e ty2'
            (Nothing, Nothing) -> coerceUnsizedNormal ck adt1 adt2 expr
            _ -> mirFail $ "impossible: coerceUnsized: one of " ++ show (an1, an2) ++
                " is repr(transparent) and the other is not?"

    coerceUnsizedNormal :: HasCallStack =>
        M.CastKind -> M.Adt -> M.Adt -> MirExp s -> MirGenerator h s ret (MirExp s)
    coerceUnsizedNormal ck' adt1 adt2 expr = do
        when (adt1 ^. adtkind /= Struct || adt2 ^. adtkind /= Struct) $ mirFail $
            "coerceUnsized not yet implemented for non-struct types: " ++ show (an1, an2)
        let v1 = Maybe.fromJust $ adt1 ^? adtvariants . ix 0
        let v2 = Maybe.fromJust $ adt2 ^? adtvariants . ix 0
        let numFields = v1 ^. vfields . to length
        let numFields' = v2 ^. vfields . to length
        when (numFields' /= numFields) $ mirFail $
            "coerceUnsized on incompatible types (mismatched fields): " ++ show (an1, an2)
        vals' <- forM (zip3 [0..] (v1 ^. vfields) (v2 ^. vfields)) $ \(i, f1, f2) -> do
            val <- getStructField adt1 i expr
            -- Only compute a cast if the types are syntactically unequal.
            if (f1 ^. fty) == (f2 ^. fty)
              then pure val
              else evalCast' ck' (f1 ^. fty) val (f2 ^. fty)
        buildStruct adt2 vals'
      where
        an1 = adt1 ^. adtname
        an2 = adt2 ^. adtname


evalCast :: HasCallStack => M.CastKind -> M.Operand -> M.Ty -> MirGenerator h s ret (MirExp s)
evalCast ck op ty = do
    e <- evalOperand op
    evalCast' ck (M.typeOf op) e ty

transmuteExp ::
  forall h s ret.
  HasCallStack =>
  MirExp s ->
  M.Ty ->
  M.Ty ->
  MirGenerator h s ret (MirExp s)
transmuteExp e@(MirExp argTy argExpr) srcMirTy destMirTy = do
  Some retTy <- tyToReprM destMirTy
  col <- use $ cs . collection
  case (argTy, retTy) of
    -- Splitting an integer into pieces (usually bytes)
    (C.BVRepr w1, MirAggregateRepr)
      | TyArray (tyToRepr col -> Right (Some (C.BVRepr w2))) n <- destMirTy
      , natValue w1 == natValue w2 * fromIntegral n -> do
        pieces <- forM [0 .. n - 1] $ \i -> do
          Some i' <- return $ mkNatRepr $ fromIntegral i
          let offset = natMultiply i' w2
          LeqProof <- case testLeq (addNat offset w2) w1 of
            Just x -> return x
            Nothing -> panic "transmute" ["impossible: (w1 / w2 - 1) * w2 + w2 > w1?"]
          return $ MirExp (C.BVRepr w2) $ R.App $ E.BVSelect offset w2 w1 argExpr
        buildArrayLit (C.BVRepr w2) pieces

    -- Reconstructing an integer from pieces (usually bytes)
    (MirAggregateRepr, C.BVRepr w2)
      | TyArray (tyToRepr col -> Right (Some (C.BVRepr w1))) n <- srcMirTy
      , natValue w1 * fromIntegral n == natValue w2 -> do
        let pieceSize = 1   -- TODO: hardcoded size=1
        pieces <- forM [0 .. n - 1] $ \(fromIntegral -> i) -> do
          let off = pieceSize * i
          mirAggregate_get off pieceSize (C.BVRepr w1) argExpr
        let go :: (1 <= wp) =>
              NatRepr wp ->
              [R.Expr MIR s (C.BVType wp)] ->
              (forall wr. (1 <= wr) => NatRepr wr -> R.Expr MIR s (C.BVType wr) -> a) ->
              a
            go _ [] _ = panic "transmute" ["impossible: w2/w1 == 0?"]
            go wp [x] k = k wp x
            go wp (x:xs) k = go wp xs (\wr rest ->
              case leqAdd (leqProof (knownNat @1) wr) wp of
                LeqProof -> k (addNat wr wp) (R.App $ E.BVConcat wr wp rest x))
        concatExpr <- go w1 pieces $ \wr result -> do
          Refl <- case testEquality wr w2 of
            Just x -> return x
            Nothing -> panic "transmute" ["impossible: w1 * (w2/w1) != w2?"]
          return result
        return $ MirExp retTy concatExpr

    -- Cast integer to pointer, like `0 as *mut T`
    (C.BVRepr w, MirReferenceRepr) -> do
        int <- case srcMirTy of
            M.TyInt _ -> return $ sbvToUsize w R.App argExpr
            M.TyUint _ -> return $ bvToUsize w R.App argExpr
            _ -> mirFail $ "unexpected srcMirTy " ++ show srcMirTy ++ " for tpr " ++ show argTy
        MirExp MirReferenceRepr <$> integerToMirRef int

    -- Transmuting between values of the same Crucible repr
    _ | Just Refl <- testEquality argTy retTy -> return e

    _ -> mirFail $
      "can't transmute " ++ show argTy ++ " to " ++ show retTy

-- | Create a new trait object by combining `e` with the named vtable.  This is
-- only valid when `e` is TyRef or TyRawPtr.  Coercions via the `CoerceUnsized`
-- trait require unpacking and repacking structs, which we don't handle here.
mkTraitObject :: forall h s ret.
    HasCallStack =>
    M.TraitName ->
    M.VtableName ->
    MirExp s ->
    MirGenerator h s ret (MirExp s)
mkTraitObject traitName' vtableName e = do
    handles <- Maybe.fromMaybe (error $ "missing vtable handles for " ++ show vtableName) <$>
        use (cs . vtableMap . at vtableName)

    let mkEntry :: MirHandle -> MirExp s
        mkEntry (MirHandle _ _ fh) =
            MirExp (C.FunctionHandleRepr (FH.handleArgTypes fh) (FH.handleReturnType fh))
                (R.App $ E.HandleLit fh)
    vtable@(MirExp vtableTy _) <- return $ mkStructExp $ map mkEntry handles

    -- Check that the vtable we constructed has the appropriate type for the
    -- trait.  A mismatch would cause runtime errors at calls to trait methods.
    trait <- Maybe.fromMaybe (error $ "unknown trait " ++ show traitName') <$>
        use (cs . collection . M.traits . at traitName')
    col <- use $ cs . collection
    Some vtableTy' <- case traitVtableType col trait of
                        Left err -> error ("mkTraitObject: " ++ err)
                        Right x -> return x
    case testEquality vtableTy vtableTy' of
        Just _ -> return ()
        Nothing -> error $ unwords
            ["vtable signature mismatch for vtable", show vtableName,
                "of trait", show traitName', ":", show vtableTy, "!=", show vtableTy']

    return $ mkStructExp
        [ e
        , packAny vtable
        ]

    where
        -- | `E.MkStruct`, but lifted to work on `MirExp`s.  We use this for
        -- building vtables and trait objects.  These don't correspond to any
        -- `M.TyAdt` or `M.TyTuple`, so we can't use the higher-level
        -- `buildStruct` or `buildTupleM` functions for this.
        mkStructExp :: [MirExp s] -> MirExp s
        mkStructExp exps = mkStructExp' Ctx.Empty Ctx.Empty exps

        mkStructExp' :: forall ctx.
            C.CtxRepr ctx ->
            Ctx.Assignment (R.Expr MIR s) ctx ->
            [MirExp s] ->
            MirExp s
        mkStructExp' ctx asn [] = MirExp (C.StructRepr ctx) (S.app $ E.MkStruct ctx asn)
        mkStructExp' ctx asn (MirExp tpr expr : exps) =
            mkStructExp' (ctx Ctx.:> tpr) (asn Ctx.:> expr) exps

-- Expressions: evaluation of Rvalues and Lvalues

evalRval :: HasCallStack => M.Rvalue -> MirGenerator h s ret (MirExp s)
evalRval (M.Use op) = evalOperand op
evalRval (M.Repeat op size) = buildRepeat op size
evalRval (M.Ref _bk lv _) = evalPlace lv >>= addrOfPlace
evalRval (M.AddressOf _mutbl lv) = evalPlace lv >>= addrOfPlace
evalRval (M.Len lv) =
    case M.typeOf lv of
        M.TyArray _ len ->
            return $ MirExp UsizeRepr $ R.App $ usizeLit $ fromIntegral len
        ty@(M.TySlice _) -> do
            place <- evalPlace lv
            meta <- case place of
                MirPlace _tpr _ref meta -> pure meta
            case meta of
                SliceMeta len -> return $ MirExp UsizeRepr len
                _ -> mirFail $ "bad metadata " ++ show meta ++ " for reference to " ++ show ty
        ty -> mirFail $ "don't know how to take Len of " ++ show ty
evalRval (M.Cast ck op ty) = evalCast ck op ty
evalRval (M.BinaryOp binop op1 op2) = transBinOp binop op1 op2
evalRval (M.NullaryOp nop nty) = transNullaryOp  nop nty
evalRval (M.UnaryOp uop op) = transUnaryOp  uop op
evalRval (M.Discriminant lv _discrTy) = do
    e <- evalLvalue lv
    let enumTy = typeOf lv
    case enumTy of
      TyAdt aname _ _ -> do
        adt <- findAdt aname
        enumDiscriminant adt e
      _ -> mirFail $ "tried to access discriminant of non-enum type " ++ show enumTy

evalRval (M.Aggregate ak ops) =
    case ak of
        M.AKTuple ->  do
            let tys = map typeOf ops
            exps <- mapM evalOperand ops
            buildTupleMaybeM tys (map Just exps)
        M.AKArray ty -> do
            exps <- mapM evalOperand ops
            Some repr <- tyToReprM ty
            buildArrayLit repr exps
        M.AKClosure -> do
            -- Closure environments have the same
            -- representation as tuples.
            let tys = map typeOf ops
            exps <- mapM evalOperand ops
            buildTupleMaybeM tys (map Just exps)
        M.AKRawPtr ty _mutbl -> do
            args <- mapM evalOperand ops
            (MirExp tprPtr ptr, MirExp tprMeta meta) <- case args of
                [p, m] -> return (p, m)
                _ -> mirFail $ "evalRval: expected exactly two operands for " ++ show ak
                    ++ ", but got " ++ show args
            case ty of
                TySlice _ -> case (tprPtr, tprMeta) of
                    (MirReferenceRepr, UsizeRepr) -> do
                        let tup = S.mkStruct
                                (Ctx.Empty Ctx.:> MirReferenceRepr Ctx.:> knownRepr)
                                (Ctx.Empty Ctx.:> ptr Ctx.:> meta)
                        return $ MirExp MirSliceRepr tup
                    _ -> mirFail $ "evalRval: unexpected reprs " ++ show (tprPtr, tprMeta)
                        ++ " for aggregate " ++ show ak
                _ -> mirFail $ "evalRval: unsupported output type for " ++ show ak
evalRval (M.RAdtAg (M.AdtAg adt agv ops ty optField)) = do
    case ty of
      -- It's not legal to construct a MethodSpec using a Rust struct
      -- constructor, so we translate as "assert(false)" instead.  Only
      -- functions in the `method_spec::raw` should be creating MethodSpecs
      -- directly, and those functions will be overridden, so the code we
      -- generate here never runs.
      CTyMethodSpec ->
        mirFail $ "evalRval: can't construct MethodSpec without an override"
      CTyMethodSpecBuilder ->
        mirFail $ "evalRval: can't construct MethodSpecBuilder without an override"
      TyAdt _ _ _ -> do
        col <- use $ cs . collection
        es <- mapM evalOperand ops
        case findReprTransparentField col adt of
          Just rtIdx ->
            case optField of
              Nothing -> do
                -- `repr(transparent)` struct/enum case.
                op <- case ops ^? ix rtIdx of
                    Just op -> pure op
                    Nothing -> mirFail $ "repr(transparent) field index " ++ show rtIdx ++
                        " out of range for " ++ show (adt ^. adtname)
                evalOperand op
              Just unionFieldIdx
                | unionFieldIdx == rtIdx -> do
                    -- `repr(transparent)` union, initializing the primary
                    -- field.  The result is the value of the field.
                    op <- case ops ^? ix 0 of
                        Just op -> pure op
                        Nothing -> mirFail $ "missing operand for union AdtAg of type "
                            ++ show (adt ^. adtname)
                    evalOperand op
                | otherwise -> do
                    -- `repr(transparent)` union, initializing one of the
                    -- zero-sized fields.  The result is an uninitialized
                    -- union value.
                    initialValue ty >>= \mv -> case mv of
                        Just v -> return v
                        Nothing -> mirFail $ "uninitialized union AdtAg unsupported for " ++ show ty
          Nothing -> do
            case adt ^. adtkind of
                M.Struct -> buildStruct adt es
                M.Enum _ -> buildEnum adt (fromInteger agv) es
                M.Union -> do
                  fieldExpr <- case es of
                    [e] -> pure e
                    [] -> mirFail "evalRval: no union field initializer?"
                    _ -> mirFail "evalRval: multiple union field initializers?"
                  fieldIdx <- case optField of
                    Just idx -> pure idx
                    Nothing -> mirFail "evalRval: no union field initializer index?"
                  buildUnion adt fieldIdx fieldExpr
      _ -> mirFail $ "evalRval: unsupported type for AdtAg: " ++ show ty
evalRval (M.ThreadLocalRef did _) = staticPlace did >>= addrOfPlace

-- We treat CopyForDeref(lv) the same as Rvalue::Use(Operand::Copy(lv)).
evalRval (M.CopyForDeref lv) = evalLvalue lv

evalRval (M.ShallowInitBox {}) = mirFail
    "evalRval: ShallowInitBox not supported"

evalLvalue :: HasCallStack => M.Lvalue -> MirGenerator h s ret (MirExp s)
evalLvalue lv = evalPlace lv >>= readPlace


evalPlace :: HasCallStack => M.Lvalue -> MirGenerator h s ret (MirPlace s)
evalPlace (M.LBase var) = varPlace var
evalPlace (M.LProj lv proj) = do
    pl <- evalPlace lv
    evalPlaceProj (M.typeOf lv) pl proj

evalPlaceProj ::
  forall h s ret.
  HasCallStack =>
  M.Ty ->
  MirPlace s ->
  M.PlaceElem ->
  MirGenerator h s ret (MirPlace s)
evalPlaceProj ty (MirPlace tpr ref NoMeta) M.Deref = do
    -- In the general case (when T is a sized type), we have a MirPlace input of
    -- the form:
    --
    --   MirPlace (*T) <expr: **T> NoMeta
    --
    -- And we want to produce output of the form:
    --
    --   MirPlace T <expr': *T> NoMeta
    --
    -- Where *T is hand-wavy syntax for reference types (e.g., &T and *const T).
    -- Note the double indirection in <expr: **T>.
    --
    -- Things get a little bit trickier when dealing with unsized types,
    -- however. See the comments below.
    case ty of
        M.TyRef t _ -> doRef t
        M.TyRawPtr t _ -> doRef t
        CTyBox t -> doRef t
        _ -> mirFail $ "deref not supported on " ++ show ty
  where
    doRef :: M.Ty -> MirGenerator h s ret (MirPlace s)
    doRef (M.TySlice ty') | MirSliceRepr <- tpr = doSlice ty' ref
    doRef M.TyStr | MirSliceRepr <- tpr = doSlice (M.TyUint M.B8) ref
    doRef (M.TyDynamic _) | DynRefRepr <- tpr = doDyn ref
    doRef (M.TyAdt _ _ _)
      | MirSliceRepr <- tpr = doSliceAdt ref
      | DynRefRepr <- tpr = doDynAdt ref
    doRef ty' | MirReferenceRepr <- tpr = do
        -- This use of `tyToReprM` is okay because `TyDynamic` and other
        -- unsized cases are handled above.
        Some tpr' <- tyToReprM ty'
        MirPlace tpr' <$> readMirRef tpr ref <*> pure NoMeta
    doRef _ = mirFail $ "deref: bad repr for " ++ show ty ++ ": " ++ show tpr

    -- Slice types [U] are unsized, so we handle them differently. Given a
    -- MirPlace input of the form:
    --
    --   MirPlace (*[U]) <expr: **[U]> NoMeta
    --
    -- We produce output of the form:
    --
    --   MirPlace U <data: *U> (SliceMeta len)
    --
    -- Where `data` is the slice's data pointer and `len` is the slice's length.
    doSlice :: M.Ty -> R.Expr MIR s MirReferenceType -> MirGenerator h s ret (MirPlace s)
    doSlice ty' ref' = do
        -- This use of `tyToReprM` is okay because we know the element type of
        -- a slice is always sized.
        Some tpr' <- tyToReprM ty'
        slice <- readMirRef MirSliceRepr ref'
        let ptr = getSlicePtr slice
        let len = getSliceLen slice
        return $ MirPlace tpr' ptr (SliceMeta len)

    -- Types like `dyn Trait` are unsized, so we handle them differently. Given
    -- a MirPlace input of the form:
    --
    --   MirPlace (*dyn Trait) <expr: **dyn Trait> NoMeta
    --
    -- We produce output of the form:
    --
    --   MirPlace AnyType <data: *?> (DynMeta vtable)
    --
    -- Where `data` is the trait object's data pointer (a reference to some
    -- unknown type) and `vtable` is the trait object's vtable. Note that it is
    -- unimportant what type we use as the first argument to MirPlace, as there
    -- is no way to directly access `data` (e.g., you can't access (*x).field if
    -- `x: &dyn Trait`). As such, it is acceptable to fill it in with a dummy
    -- type like AnyType.
    doDyn :: R.Expr MIR s MirReferenceType -> MirGenerator h s ret (MirPlace s)
    doDyn ref' = do
        dynRef <- readMirRef DynRefRepr ref'
        let dynRefData = S.getStruct dynRefDataIndex dynRef
        let dynRefVtable = S.getStruct dynRefVtableIndex dynRef
        return $ MirPlace C.AnyRepr dynRefData (DynMeta dynRefVtable)

    -- For (dynamically-sized) ADTs wrapping slices, with MirPlace input of the
    -- form:
    --
    --   MirPlace (*S<[T]>) <expr: **S<[T]> NoMeta
    --
    -- We produce output of the form:
    --
    --   MirPlace AnyRepr <expr: *S<[T; len]> (SliceMeta len)
    --
    -- Where `len` is the wrapped slice's length.
    doSliceAdt :: R.Expr MIR s MirReferenceType -> MirGenerator h s ret (MirPlace s)
    doSliceAdt ref' =
      do
        -- Normally we'd use `tyToReprM` to get the ADT's representation,
        -- but that would involve computing its slice field's representation,
        -- which should error. Because it represents an unsized value, we don't
        -- expect to check/use this type directly elsewhere, so we can get away
        -- with an `AnyRepr` placeholder.
        let adtRepr = C.AnyRepr
        adtRef <- readMirRef MirSliceRepr ref'
        -- In both this case and the case of plain slices, `readMirRef` gives us
        -- access to a double-wide DST pointer. In both cases, the second half
        -- holds the slice length. In our case, the first half holds a pointer
        -- to the ADT, while in the slice case, the first half holds the slice's
        -- data pointer, i.e. a pointer to the first element of the slice.
        --
        -- In both cases, though, we can safely access the first half with
        -- `getSlicePtr`.
        let adtPtr = getSlicePtr adtRef
        let sliceLen = getSliceLen adtRef
        return $ MirPlace adtRepr adtPtr (SliceMeta sliceLen)

    -- For (dynamically-sized) ADTs wrapping trait objects, with MirPlace input
    -- of the form:
    --
    --   MirPlace (*S<dyn Trait>) <expr: **S<dyn Trait> NoMeta
    --
    -- We produce output of the form:
    --
    --   MirPlace AnyRepr <expr: *S<Concrete> (DynMeta vtable)
    --
    -- Where `vtable` is the vtable for `Trait` at `Concrete`.
    doDynAdt :: R.Expr MIR s MirReferenceType -> MirGenerator h s ret (MirPlace s)
    doDynAdt ref' =
      do
        -- Normally we'd use `tyToReprM` to get the ADT's representation,
        -- but that would involve computing its trait object field's
        -- representation, which will error. Because it represents an unsized
        -- value, we don't expect to check/use this type directly elsewhere, so
        -- we can get away with an `AnyRepr` placeholder.
        let adtRepr = C.AnyRepr
        dynRef <- readMirRef DynRefRepr ref'
        let adtPtr = S.getStruct dynRefDataIndex dynRef
        let vtable = S.getStruct dynRefVtableIndex dynRef
        return $ MirPlace adtRepr adtPtr (DynMeta vtable)

evalPlaceProj ty pl@(MirPlace tpr ref meta) (M.PField idx fieldTy) = do
  col <- use $ cs . collection
  case ty of
    CTyMaybeUninit _ -> do
        return $ MirPlace tpr ref NoMeta

    ty' | Just adt <- tyAdtDefSkipDowncast col ty', Just tIdx <- findReprTransparentField col adt ->
        if idx == tIdx then
            -- The field's low-level representation is identical to the struct
            -- itself, due to repr(transparent).
            return pl
        else do
            -- Since `findReprTransparentField` returned `Just`, we know that
            -- fields aside from `tIdx` must be zero-sized, and thus contain no
            -- actual data.  So we can return a dummy reference here.
            MirExp tpr' e <- initialValue fieldTy >>= \x -> case x of
                Just expr -> return expr
                Nothing -> mirFail $ "failed to produce dummy value of type " ++ show fieldTy
            ref' <- constMirRef tpr' e
            return $ MirPlace tpr' ref' NoMeta

    M.TyAdt nm _ _ -> do
        adt <- findAdt nm
        case adt ^. adtkind of
            Struct -> structFieldRef adt idx ref meta
            Enum _ -> mirFail $ "tried to access field of non-downcast " ++ show ty
            Union -> unionFieldRef adt idx ref

    M.TyDowncast (M.TyAdt nm _ _) i -> do
        adt <- findAdt nm
        enumFieldRef adt (fromInteger i) idx ref

    M.TyTuple ts -> tupleFieldRef ts idx tpr ref
    M.TyClosure ts -> tupleFieldRef ts idx tpr ref
    _ -> mirFail $
        "tried to get field " ++ show idx ++ " of unsupported type " ++ show ty
  where
    -- | Like `tyAdtDef`, but also accepts `TyDowncast (TyAdt ...)`.
    tyAdtDefSkipDowncast :: Collection -> M.Ty -> Maybe M.Adt
    tyAdtDefSkipDowncast col (M.TyDowncast ty' _) = tyAdtDef col ty'
    tyAdtDefSkipDowncast col ty' = tyAdtDef col ty'
evalPlaceProj ty (MirPlace tpr ref meta) (M.Index idxVar) = case (ty, tpr, meta) of
    (M.TyArray elemTy _sz, MirAggregateRepr, NoMeta) -> do
        idx' <- getIdx idxVar
        Some elemTpr <- tyToReprM elemTy
        MirPlace elemTpr <$> subindexRef elemTpr ref idx' <*> pure NoMeta

    (M.TySlice _elemTy, elemTpr, SliceMeta len) -> do
        idx <- getIdx idxVar
        G.assertExpr (R.App $ usizeLt idx len)
            (S.litExpr "Index out of range for access to slice")
        MirPlace elemTpr <$> mirRef_offset ref idx <*> pure NoMeta

    _ -> mirFail $ "indexing not supported on " ++ show (ty, tpr, meta)
  where
    getIdx :: M.Var -> MirGenerator h s ret (R.Expr MIR s UsizeType)
    getIdx var = do
        MirExp tpr' idx <- varExp var
        Refl <- testEqualityOrFail tpr' UsizeRepr $
            "expected index to be UsizeRepr, but got " ++ show tpr'
        return idx
evalPlaceProj ty (MirPlace tpr ref meta) (M.ConstantIndex idx _minLen fromEnd) = case (ty, tpr, meta) of
    -- TODO: should this check sz >= minLen?
    (M.TyArray elemTy sz, MirAggregateRepr, NoMeta) -> do
        idx' <- getIdx idx (R.App $ usizeLit $ fromIntegral sz) fromEnd
        Some elemTpr <- tyToReprM elemTy
        MirPlace elemTpr <$> subindexRef elemTpr ref idx' <*> pure NoMeta

    (M.TySlice _elemTy, elemTpr, SliceMeta len) -> do
        idx' <- getIdx idx len fromEnd
        G.assertExpr (R.App $ usizeLt idx' len)
            (S.litExpr "Index out of range for access to slice")
        MirPlace elemTpr <$> mirRef_offset ref idx' <*> pure NoMeta

    _ -> mirFail $ "indexing not supported on " ++ show (ty, tpr, meta)
  where
    getIdx :: Int -> R.Expr MIR s UsizeType -> Bool ->
        MirGenerator h s ret (R.Expr MIR s UsizeType)
    getIdx idx' len True = return $ R.App $ usizeSub len $ R.App $ usizeLit $ fromIntegral idx'
    getIdx idx' _ False = return $ R.App $ usizeLit $ fromIntegral idx'
-- Downcast is a no-op - it only affects the type reported by `M.type_of`.  The
-- `PField` case above looks for `TyDowncast` to handle enum accesses.
evalPlaceProj _ pl (M.Downcast _idx) = return pl
-- Subtype is a no-op, as it is only present in the MIR to making subtyping
-- explicit during optimizations and codegen.
evalPlaceProj _ pl (M.Subtype _ty) = return pl
-- Subslicing is defined on slices and arrays. See the haddock for `Subslice`
-- for details on the semantics of `fromIndex` and `toIndex`.
evalPlaceProj ty (MirPlace tpr ref meta) (M.Subslice fromIndex toIndex fromEnd) =
  case (ty, ref, tpr, meta) of
    (M.TySlice _elemTy, headRef, elemTpr, SliceMeta len) ->
      let lastIndex = mkLastIndex len
          newLen = R.App (lastIndex `usizeSub` firstIndex)
          newMeta = SliceMeta newLen
      in MirPlace elemTpr <$> mirRef_offset headRef firstIndex <*> pure newMeta

    -- TODO: https://github.com/GaloisInc/crucible/issues/1494
    --
    -- NB: after implementing this, update `Mir.Mir.typeOfProj`, which currently
    -- declares that `Subslice` unconditionally yields a slice. This is
    -- incorrect; `Subslice` applied to an array will yield an array.
    (M.TyArray {}, _, _, _) -> mirFail
      "evalPlaceProj: subslicing not yet supported on arrays"

    _ -> mirFail $
      "evalPlaceProj: subslicing not supported on " ++ show (ty, tpr, meta)
  where
    usize = R.App . usizeLit . fromIntegral
    firstIndex = usize fromIndex
    mkLastIndex len
      | fromEnd = R.App (len `usizeSub` usize toIndex)
      | otherwise = usize toIndex
evalPlaceProj ty (MirPlace _ _ meta) proj =
    mirFail $ "projection " ++ show proj ++ " not yet implemented for " ++ show (ty, meta)

--------------------------------------------------------------------------------------
-- ** Statements
--

-- Coerce `exp` from `ty1` to `ty2`.  Returns `Nothing` if the requested
-- coercion is not legal in Rust.
-- TODO: use this to implmeent parts of `evalCast`
tryCoerce :: M.Ty -> M.Ty -> MirExp s -> Maybe (MirGenerator h s ret (MirExp s))
tryCoerce ty1 ty2 expr
  | ty1 == ty2 = Just $ return expr
tryCoerce (M.TyRef ty1 M.Mut) (M.TyRef ty2 M.Immut) expr
  | ty1 == ty2 = Just $ return expr
-- Special hack: using `CTyBox` as a constructor (as `typeOf` does for the
-- `Box` nullop) produces a `TyAdt` with an invalid `DefId`.  This is because
-- we don't have a way to compute the correct hash inside the `CTyBox` ctor.
-- So we use this special case to avoid erroring on `CTyBox` assignments.  (The
-- `CTyBox` pattern ignores the bad field already.)
-- TODO: implement `Eq` to ignore the field, or else remove it entirely and use
-- a different key for `findAdt`.
tryCoerce (CTyBox ty1) (CTyBox ty2) expr
  | ty1 == ty2 = Just $ return expr
tryCoerce _ _ _ = Nothing

evalCoerce :: M.Ty -> M.Ty -> MirExp s -> MirGenerator h s ret (MirExp s)
evalCoerce ty1 ty2 expr@(MirExp tpr _)
  | Just action <- tryCoerce ty1 ty2 expr = action
  | otherwise = mirFail $ "illegal or unimplemented coercion from "
        ++ show ty1 ++ " (concretely " ++ show tpr ++ ") to " ++ show ty2

doAssignCoerce :: HasCallStack => M.Lvalue -> M.Ty -> MirExp s -> MirGenerator h s ret ()
doAssignCoerce lv ty expr =
    doAssign lv =<< evalCoerce ty (M.typeOf lv) expr

doAssign :: HasCallStack => M.Lvalue -> MirExp s -> MirGenerator h s ret ()
doAssign lv (MirExp tpr val) = do
    place <- evalPlace lv
    case place of
        MirPlace tpr' ref _ -> do
            Refl <- testEqualityOrFail tpr tpr' $
                "ill-typed assignment of " ++ show tpr ++ " to " ++ show tpr'
                    ++ " (" ++ show (M.typeOf lv) ++ ") " ++ show lv
            writeMirRef tpr ref val


transStatement :: HasCallStack => M.Statement -> MirGenerator h s ret ()
transStatement (M.Statement skind spos) = do
  setPosition spos
  transStatementKind skind

transStatementKind :: HasCallStack => M.StatementKind -> MirGenerator h s ret ()
transStatementKind (M.Assign lv rv) = do
  col <- use $ cs . collection
  -- Skip writes to zero-sized fields, as they are effectively no-ops.
  when (not $ isZeroSized col $ typeOf lv) $ do
    rve <- evalRval rv
    doAssignCoerce lv (M.typeOf rv) rve
transStatementKind (M.StorageLive _lv) = return ()
transStatementKind (M.StorageDead _lv) = return ()
transStatementKind (M.SetDiscriminant lv _i) = do
  case M.typeOf lv of
    -- Currently we require that all uses of `SetDiscriminant` get bundled up
    -- with related field writes into an `RAdtAg` assignment during the
    -- AllocateEnum pass.  Ideally this transformation would not be mandatory,
    -- but the problem is, rustc emits the `SetDiscriminant` statement *after*
    -- the field writes, not before.  Our current implementation of downcast
    -- field writes requires the downcast variant index to match the enum's
    -- current variant.  If we lifted this restriction (for example, by
    -- allowing an enum value to have multiple initialized variants
    -- simultaneously), then we could remove AllocateEnum.
    ty -> mirFail $ "don't know how to set discriminant of " ++ show ty
transStatementKind M.Nop = return ()
transStatementKind M.Deinit = return ()
transStatementKind (M.StmtIntrinsic ndi) =
    case ndi of
        -- rustc uses assumptions from `assume` to optimize code. If we
        -- encounter an occurrence of `assume` in MIR code, we should check
        -- that its argument is equal to `true`, as `assume(false)` is UB.
        NDIAssume cond -> do
            MirExp tpr e <- evalOperand cond
            Refl <- testEqualityOrFail tpr C.BoolRepr "expected Assume cond to be BoolType"
            G.assertExpr (S.app $ E.BoolEq e (S.app $ E.BoolLit True)) $
                S.app $ E.StringLit $ W4.UnicodeLiteral $ "assume(false) is undefined behavior"
        NDICopyNonOverlapping srcOp destOp countOp -> do
            srcExp <- evalOperand srcOp
            destExp <- evalOperand destOp
            countExp <- evalOperand countOp
            let elemTy = M.typeOfProj M.Deref $ M.typeOf srcOp
            Some tpr <- tyToReprM elemTy
            case (srcExp, destExp, countExp) of
                ( MirExp MirReferenceRepr src,
                  MirExp MirReferenceRepr dest,
                  MirExp UsizeRepr count )
                    -> void $ copyNonOverlapping tpr src dest count
                _   -> mirFail $ unlines
                         [ "bad arguments for intrinsics::copy_nonoverlapping: "
                         , show srcExp
                         , show destExp
                         , show countExp
                         ]
-- Per the docs, this statement kind is only useful in the const eval
-- interpreter, so it is a no-op for crucible-mir's purposes.
transStatementKind M.ConstEvalCounter = return ()

-- | Add a new `BranchTransInfo` entry for the current function.  Returns the
-- index of the new entry.
recordBranchTransInfo :: BranchTransInfo -> MirGenerator h s ret Int
recordBranchTransInfo info = do
    cur <- use $ transInfo . ftiBranches
    let idx = Seq.length cur
    transInfo . ftiBranches %= (Seq.|> info)
    return idx

-- | Mark the current block as unreachable in the translation metadata.
recordUnreachable :: MirGenerator h s ret ()
recordUnreachable = do
    blkID <- G.currentBlockID
    transInfo . ftiUnreachable %= Set.insert (Text.pack $ show $ blkID)

transSwitch ::
    Text ->         -- source location
    MirExp s ->     -- thing switching over
    [Integer] ->    -- switch comparisons
    [M.BasicBlockInfo] -> -- jumps
    MirGenerator h s ret a
transSwitch _pos _ [] [targ] = jumpToBlock targ
transSwitch pos expr vals blks = do
    setPosition pos
    lm <- use labelMap
    conds <- mapM (doCompare expr) vals
    labels <- forM blks $ \b -> case Map.lookup b lm of
        Just lab -> return lab
        Nothing -> mirFail "bad jump"

    isDropFlag <- switchIsDropFlagCheck vals blks
    let info = case (expr, vals, labels) of
            (MirExp C.BoolRepr _, [0], [_fd, _td]) | isDropFlag -> DropFlagBranch
            (MirExp C.BoolRepr _, [0], [fd, td]) ->
                BoolBranch (labelText td) (labelText fd) pos
            (MirExp C.BoolRepr _, [1], [td, fd]) ->
                BoolBranch (labelText td) (labelText fd) pos
            _ -> IntBranch vals (map labelText labels) pos
    branchId <- recordBranchTransInfo info

    go branchId 0 conds labels
  where
    doCompare :: MirExp s -> Integer -> MirGenerator h s ret (R.Expr MIR s C.BoolType)
    doCompare (MirExp C.BoolRepr e) x = case x of
        0 -> return $ S.app $ E.Not e
        1 -> return e
        _ -> mirFail $ "invalid BoolRepr constant " ++ show x ++ " in switch"
    doCompare (MirExp C.IntegerRepr e) x =
        return $ S.app $ E.IntEq e $ S.app $ E.IntLit x
    doCompare (MirExp (C.BVRepr w) e) x =
        return $ S.app $ E.BVEq w e $ S.app $ eBVLit w x
    doCompare (MirExp tpr _) _ =
        mirFail $ "invalid input type " ++ show tpr ++ " in switch"

    go :: Int -> Int -> [R.Expr MIR s C.BoolType] -> [R.Label s] ->
        MirGenerator h s ret a
    go _branchId _idx [] labels =
      case labels of
        [lab] -> G.jump lab
        _ ->
          mirFail $
            "no conditional but " ++ show (length labels) ++
            " labels in switch"
    go branchId idx [cond] labels =
      case labels of
        [lab1, lab2] -> do
          setPosition $ posStr branchId idx
          G.branch cond lab1 lab2
        _ ->
          mirFail $
            "conditional with " ++ show (length labels) ++
            " labels in switch"
    go branchId idx (cond : conds) labels =
      case labels of
        lab : labs -> do
          fallthrough <- G.defineBlockLabel $ go branchId (idx + 1) conds labs
          setPosition $ posStr branchId idx
          G.branch cond lab fallthrough
        [] -> mirFail "multiple conditionals but no labels in switch"

    labelText :: R.Label s -> Text
    labelText l = Text.pack $ show $ R.LabelID l

    posStr :: Int -> Int -> Text
    posStr branchId idx =
        pos <> " #" <> Text.pack (show branchId) <> "," <> Text.pack (show idx)

-- | Check if a switch appears to be a drop flag check.  Drop flag checks look
-- like this:
--
--          switchInt(_dropflag) -> [false: bb2, otherwise: bb1];
--
--      bb1:
--          _dropflag = const false;
--          drop(_var) -> bb2;
--
--      bb2:
--          ...
--
-- This has the unusual property that the false case jumps directly to the
-- "after" block - a normal `if` expression generates blocks for both the true
-- and false cases, even when the false case is empty.
switchIsDropFlagCheck :: [Integer] -> [M.BasicBlockInfo] -> MirGenerator h s ret Bool
switchIsDropFlagCheck [0] [f, t] = do
    fn <- expectFnContext
    let optTrueBb = fn ^. fbody . mblockmap . at t
    trueBb <- case optTrueBb of
        Just x -> return $ x
        Nothing -> mirFail $ "bad switch target " ++ show t
    let stmtsOk = case map _stmtKind (trueBb ^. bbstmts) of
            [Assign (LBase _) (Use (OpConstant (Constant TyBool (ConstBool False))))] ->
                True
            _ -> False
    let termOk = case trueBb ^. bbterminator . termKind of
            Drop _ dest _ -> dest == f
            _ -> False
    return $ stmtsOk && termOk
switchIsDropFlagCheck _ _ = return False

jumpToBlock :: M.BasicBlockInfo -> MirGenerator h s ret a
jumpToBlock bbi = do
    lm <- use labelMap
    case (Map.lookup bbi lm) of
      Just lab -> G.jump lab
      _ -> mirFail "bad jump"

doReturn :: HasCallStack => C.TypeRepr ret -> MirGenerator h s ret a
doReturn tr = do
    e <- getReturnExp tr

    -- In static initializers, "local" variables stay live past the end of the
    -- function so that the initializer can return references to them.  For
    -- example, in `static R: &'static i32 = &1;`, the initializer stores `1`
    -- into a local, then returns a reference to that local.  If we clean up
    -- that local like normal, then accesses to the returned reference will
    -- fail.  So we skip the cleanup when exiting a static initializer.
    --
    -- To detect if the current function is a static initializer, we check if
    -- there's an entry in `statics` matching the current `fname`.
    fn <- expectFnContext
    let curName = fn ^. fname
    isStatic <- use $ cs . collection . statics . to (Map.member curName)
    when (not isStatic) cleanupLocals

    G.returnFromFunction e

---------------------------------------------------------------------------------------------------
---------------------------------------------------------------------------------------------------
-- | Find the function expression for this name (instantiated with the given type arguments)
-- It could be a regular function, a static trait invocation, or a dictionary argument
--
-- Will return an expression of type (FnHandleType args ret)
--
-- Some of these predicates will turn into additional (term) arguments, but only the call
-- site knows which
lookupFunction :: forall h s ret. HasCallStack => MethName ->
   MirGenerator h s ret (Maybe (MirExp s, FnSig))
lookupFunction nm = do
  db   <- use debugLevel
  when (db > 3) $
    traceM $ "**lookupFunction: trying to resolve " ++ fmt nm

  -- these  are defined at the bottom of Mir.Generator
  isImpl    <- resolveFn nm
  isCustom  <- resolveCustom nm

  -- Given a (polymorphic) function handle, turn it into an expression by
  -- instantiating the type arguments
  let mkFunExp :: FH.FnHandle a r -> MirExp s
      mkFunExp fhandle =
        let fargctx  = FH.handleArgTypes fhandle
            fret     = FH.handleReturnType fhandle
        in MirExp (C.FunctionHandleRepr fargctx fret) $ R.App $ E.HandleLit fhandle

  case () of
    ()

       -- a custom function (we will find it elsewhere)
       | Just _ <- isCustom
       -> return Nothing

       -- a normal function
       | Just (MirHandle nm' fs fh) <- isImpl
       -> do
            when (db > 3) $ do
              traceM $ "**lookupFunction: " ++ fmt nm' ++ " resolved as normal call"

            return $ Just $ (mkFunExp fh, fs)

       | otherwise -> do
            when (db > 1) $ do
               traceM $ "***lookupFunction: Cannot find function " ++ show nm
            return Nothing

callHandle :: HasCallStack =>
    MirExp s -> Abi -> [M.Operand] -> MirGenerator h s ret (MirExp s)
callHandle e abi cargs
  | MirExp (C.FunctionHandleRepr ifargctx ifret) polyinst <- e = do
    db    <- use debugLevel
    when (db > 3) $
       traceM $ fmtDoc (PP.fillSep ["At normal function call of",
           PP.viaShow e, "with arguments", pretty cargs,
           "abi:",pretty abi])

    let tys = map typeOf cargs
    exps <- mapM evalOperand cargs
    exps' <- case abi of
      RustCall _
        -- Empty tuples use UnitRepr instead of StructRepr
        | [selfExp, MirExp C.UnitRepr _] <- exps -> do
          return [selfExp]

        | [selfExp, tupleExp@(MirExp MirAggregateRepr _)] <- exps
        , [_, M.TyTuple tupleTys] <- tys -> do
          tupleParts <- mapM (\(i, ty) -> getTupleElemTyped tupleExp i ty) (zip [0..] tupleTys)
          return $ selfExp : tupleParts

        -- Some code in rustc_codegen_cranelift suggests that there may be
        -- RustCall functions with only a tuple (which should be unpacked) and
        -- no self/receiver argument, but so far we haven't encountered such a
        -- thing.

        | otherwise -> mirFail $
          "callExp: RustCall arguments are the wrong shape: " ++ show cargs

      _ -> return exps

    exp_to_assgn exps' $ \ctx asgn -> do
      case (testEquality ctx ifargctx) of
        Just Refl -> do
          ret_e <- G.call polyinst asgn
          return (MirExp ifret ret_e)
        _ -> mirFail $ "type error in call of " ++ show e
                      ++ "\n    args      " ++ show ctx
                      ++ "\n vs fn params " ++ show ifargctx
  | otherwise = mirFail $ "don't know how to call handle " ++ show e

callExp :: HasCallStack =>
           M.DefId
        -> [M.Operand]
        -> MirGenerator h s ret (MirExp s)
callExp funid cargs = do
   db    <- use debugLevel
   mhand <- lookupFunction funid
   isCustom <- resolveCustom funid
   case () of
     () | Just (CustomOp op) <- isCustom -> do
          when (db > 3) $
            traceM $ fmtDoc (PP.fillSep ["At custom function call of",
                 pretty funid, "with arguments", pretty cargs])

          ops <- mapM evalOperand cargs
          let opTys = map M.typeOf cargs
          op opTys ops

        | Just (CustomOpNamed op) <- isCustom -> do
          when (db > 3) $
            traceM $ fmtDoc (PP.fillSep ["At custom function call of",
                 pretty funid, "with arguments", pretty cargs])

          ops <- mapM evalOperand cargs
          op funid ops

       | Just (CustomMirOp op) <- isCustom -> do
          when (db > 3) $
            traceM $ fmtDoc (PP.fillSep ["At custom function call of",
               pretty funid, "with arguments", pretty cargs])
          op cargs

       | Just (hand, sig) <- mhand -> do
         callHandle hand (sig ^. fsabi) cargs

     _ -> mirFail $ "callExp: Don't know how to call " ++ fmt funid



-- regular function calls: closure calls & dynamic trait method calls handled later
doCall :: forall h s ret a. (HasCallStack) => M.DefId -> [M.Operand]
   -> Maybe (M.Lvalue, M.BasicBlockInfo) -> MirGenerator h s ret a
doCall funid cargs cdest = do
    _am    <- use $ cs.collection
    isCustom <- resolveCustom funid
    case cdest of
      (Just (dest_lv, jdest)) -> do
            ret <- callExp funid cargs
            doAssign dest_lv ret
            jumpToBlock jdest

      Nothing
         -- special case for exit function that does not return
         | Just (CustomOpExit op) <- isCustom -> do
               exps <- mapM evalOperand cargs
               msg  <- op exps
               G.reportError (S.app $ E.StringLit $ W4.UnicodeLiteral msg)

        -- other functions that don't return
        | otherwise -> do
            _ <- callExp funid cargs
            -- TODO: is this the correct behavior?
            G.reportError (S.app $ E.StringLit $ fromString "Program terminated.")

transTerminator :: HasCallStack => M.Terminator -> C.TypeRepr ret -> MirGenerator h s ret a
transTerminator (M.Terminator tkind tpos) tr = do
    setPosition tpos
    transTerminatorKind tkind tpos tr

transTerminatorKind :: HasCallStack => M.TerminatorKind -> Text -> C.TypeRepr ret -> MirGenerator h s ret a
transTerminatorKind (M.Goto bbi) _tpos _tr =
    jumpToBlock bbi
transTerminatorKind t@(M.SwitchInt swop _swty svals stargs) tpos _tr
  | all Maybe.isJust svals = do
      s <- evalOperand swop
      transSwitch tpos s (Maybe.catMaybes svals) stargs
  | otherwise =
      mirFail $ "SwitchInt with no values to compare: " ++ show (pretty t)
transTerminatorKind (M.Return) _tpos tr =
    doReturn tr
transTerminatorKind (M.Call funcOp cargs cretdest) _tpos _retTy = case M.typeOf funcOp of
  M.TyFnDef defId ->
    doCall defId cargs cretdest -- cleanup ignored
  M.TyFnPtr _ -> do
    func <- evalOperand funcOp
    ret <- callHandle func RustAbi cargs
    case cretdest of
      Just (dest_lv, jdest) -> do
        doAssign dest_lv ret
        jumpToBlock jdest
      Nothing ->
        G.reportError (S.app $ E.StringLit $ fromString "Program terminated.")
  calleeTy -> mirFail $ "expected callee to be a function, but it was " <> show calleeTy
transTerminatorKind (M.Assert cond expected msg target) _tpos _tr = do
    MirExp tpr e <- evalOperand cond
    Refl <- testEqualityOrFail tpr C.BoolRepr "expected Assert cond to be BoolType"
    G.assertExpr (S.app $ E.BoolEq e (S.app $ E.BoolLit expected)) $
        S.app $ E.StringLit $ W4.UnicodeLiteral $ msg
    jumpToBlock target
transTerminatorKind (M.Resume) _tpos tr =
    doReturn tr -- resume happens when unwinding
transTerminatorKind (M.Drop dlv dt dropFn) _tpos _tr = do
    let ptrOp = M.Temp $ M.Cast M.Misc
            (M.Temp $ M.AddressOf M.Mut dlv) (M.TyRawPtr (M.typeOf dlv) M.Mut)
    maybe (return ()) (\f -> void $ callExp f [ptrOp]) dropFn
    jumpToBlock dt
transTerminatorKind M.Abort _tpos _tr =
    G.reportError (S.litExpr "process abort in unwinding")
transTerminatorKind M.Unreachable _tpos _tr = do
    recordUnreachable
    G.reportError (S.litExpr "Unreachable!!!!!")
transTerminatorKind M.InlineAsm _tpos _tr =
    mirFail "Inline assembly not supported"


--- translation of toplevel glue ---

-- | Allocate RefCells for all locals and populate `varMap`.  Locals are
-- default-initialized when possible using the result of `initialValue`.
initLocals :: [M.Var] -> MirGenerator h s ret ()
initLocals localVars = forM_ localVars $ \v -> do
    let name = v ^. varname
    let ty = v ^. varty
    Some tpr <- tyToReprM ty

    optVal <- initialValue ty >>= \case
        Nothing -> return Nothing
        Just (MirExp tpr' val) -> do
            Refl <- testEqualityOrFail tpr tpr' $
                "initialValue produced " ++ show tpr' ++ " instead of " ++ show tpr
                  ++ ", for " ++ show (pretty ty)
            return $ Just val

    -- FIXME: temporary hack to put every local behind a MirReference, to work
    -- around issues with `&fn()` variables.
    varinfo <-
      if True -- if Set.member name addrTaken
        then do
          ref <- newMirRef tpr
          case optVal of
              Nothing -> return ()
              Just val -> writeMirRef tpr ref val
          reg <- G.newReg ref
          return $ Some $ VarReference tpr reg
        else do
          reg <- case optVal of
              Nothing -> G.newUnassignedReg tpr
              Just val -> G.newReg val
          return $ Some $ VarRegister reg
    varMap %= Map.insert name varinfo

-- | Deallocate RefCells for all locals in `varMap`.
cleanupLocals :: MirGenerator h s ret ()
cleanupLocals = do
    vm <- use varMap
    forM_ (Map.elems vm) $ \(Some vi) -> case vi of
        VarReference _ reg -> G.readReg reg >>= dropMirRef
        _ -> return ()

buildLabelMap :: forall h s ret. M.MirBody -> MirGenerator h s ret (LabelMap s)
buildLabelMap (M.MirBody _ blocks _) = Map.fromList <$> mapM buildLabel blocks

buildLabel :: forall h s ret. M.BasicBlock -> MirGenerator h s ret (M.BasicBlockInfo, R.Label s)
buildLabel (M.BasicBlock bi _) = do
    lab <- G.newLabel
    return (bi, lab)

-- | Build the initial state for translation of functions
initFnState :: (?debug::Int,?customOps::CustomOpMap,?assertFalseOnError::Bool)
            => CollectionState
            -> FnTransContext
            -> FnState s
initFnState colState transCtxt =
  FnState { _varMap     = Map.empty,
            _transContext = transCtxt,
            _debugLevel = ?debug,
            _cs         = colState,
            _labelMap   = Map.empty,
            _customOps  = ?customOps,
            _assertFalseOnError = ?assertFalseOnError,
            _transInfo  = mempty
         }


-- do the statements and then the terminator
translateBlockBody :: HasCallStack => C.TypeRepr ret -> M.BasicBlockData -> MirGenerator h s ret a
translateBlockBody tr (M.BasicBlockData stmts terminator) = (mapM_ transStatement stmts)
   >> (transTerminator terminator tr)

--
registerBlock :: HasCallStack => C.TypeRepr ret -> M.BasicBlock -> MirGenerator h s ret ()
registerBlock tr (M.BasicBlock bbinfo' bbdata')  = do
    lm <- use labelMap
    case (Map.lookup bbinfo' lm) of
      Just lab -> do
        G.defineBlock lab (translateBlockBody tr bbdata')
      _ -> mirFail "bad label"



-------------------------------------------------------------------------------------------



-- | Translate a MIR function, returning a jump expression to its entry block
-- argvars are registers
-- The first block in the list is the entrance block
genFn :: HasCallStack =>
    M.Fn ->
    C.TypeRepr ret ->
    Ctx.Assignment (R.Atom s) args ->
    MirGenerator h s ret (G.Label s)
genFn (M.Fn fname' argvars sig body@(MirBody localvars blocks _)) rettype inputs = do

  lm <- buildLabelMap body
  labelMap .= lm

  initLocals (argvars ++ localvars)
  let inputExps = toListFC (\atom -> MirExp (R.typeOfAtom atom) (R.AtomExpr atom)) inputs
  inputExps' <- case sig ^. M.fsabi of
    M.RustCall (M.RcSpreadArg spreadArg) -> do
      -- The Rust signature looks like `(T, (U, V))`, but the Crucible version
      -- uses the untupled form `(T, U, V)`.  `argvars` follows the tupled
      -- form, but `inputExps` follows the untupled form.  Here we convert
      -- `inputExps` to match `argvars` by tupling up some of the arguments.
      --
      -- Arguments from `splitIndex` onward need to be tupled.  Note that
      -- `spreadArg` is 1-based (it's a MIR `Local` ID, and the first argument
      -- is local `_1`), but we convert to a 0-based index for convenience.
      let splitIndex = spreadArg - 1
      when (splitIndex > length inputExps) $
        mirFail $ "split index " ++ show splitIndex ++ " out of range for "
          ++ show (fmapFC R.typeOfAtom inputs)
      let selfExps = take splitIndex inputExps
      let tupleFieldExps = drop splitIndex inputExps
      tupleFieldTys <- case map typeOf $ drop splitIndex argvars of
        [M.TyTuple tys] -> return tys
        _ -> mirFail $ "expected tuple at position " ++ show splitIndex
          ++ ", but got " ++ show argvars
      tupleExp <- case tupleFieldTys of
        [] -> return $ MirExp C.UnitRepr (R.App E.EmptyApp)
        _ -> buildTupleMaybeM tupleFieldTys (map Just tupleFieldExps)
      return $ selfExps ++ [tupleExp]
    _ -> return inputExps
  initArgs inputExps' argvars

  db <- use debugLevel
  when (db > 3) $ do
     vmm <- use varMap
     let showVar var = fmt var ++ " : " ++ fmt (M.typeOf var)
     traceM $ "-----------------------------------------------------------------------------"
     traceM $ "Generating code for: " ++ show fname'
     traceM $ "Function args are: " ++ List.intercalate "," (map showVar argvars)
     traceM $ "VarMap is: " ++ fmt (Map.keys vmm)
     traceM $ "Body is:\n" ++ fmt body
     traceM $ "-----------------------------------------------------------------------------"
  blocks'@(enter NE.:| _) <- case body of
    M.MirBody _mvars (enter : _blocksRest) _ -> return (enter NE.:| blocks)
    _ -> mirFail $ "expected body to be MirBody, but got " ++ show body
  -- actually translate all of the blocks of the function
  mapM_ (registerBlock rettype) blocks'
  let (M.BasicBlock bbi _) = enter
  lm' <- use labelMap
  case (Map.lookup bbi lm') of
    Just lbl -> return lbl
    _ -> mirFail "bad thing happened"

  where
    initArgs :: HasCallStack =>
        [MirExp s] -> [M.Var] -> MirGenerator h s ret ()
    initArgs inputs0 vars =
        case (inputs0, vars) of
            ([], []) -> return ()
            (MirExp inputTpr inputExpr : inputs', var : vars') -> do
                mvi <- use $ varMap . at (var ^. varname)
                Some vi <- case mvi of
                    Just x -> return x
                    Nothing -> mirFail $ "no varinfo for arg " ++ show (var ^. varname)
                Refl <- testEqualityOrFail inputTpr (varInfoRepr vi) $
                    "type mismatch in initialization of " ++ show (var ^. varname) ++ ": " ++
                        show inputTpr ++ " != " ++ show (varInfoRepr vi)
                case vi of
                    VarRegister reg -> G.assignReg reg inputExpr
                    VarReference tpr refReg -> do
                        ref <- G.readReg refReg
                        writeMirRef tpr ref inputExpr
                    VarAtom _ -> mirFail $ "unexpected VarAtom"
                initArgs inputs' vars'
            _ -> mirFail $ "mismatched argument count for " ++ show fname'


genClosureFnPointerShim :: forall h s args ret.
  HasCallStack =>
  M.DefId ->
  C.TypeRepr ret ->
  Ctx.Assignment (R.Atom s) args ->
  MirGenerator h s ret (G.Label s)
genClosureFnPointerShim callOnceId tprRet argAtoms = do
  -- Look up `callOnceId` in the `HandleMap`.
  hm <- use $ cs . handleMap
  MirHandle _ sig (fh :: FH.FnHandle args' ret') <- case Map.lookup callOnceId hm of
    Just x -> return x
    Nothing -> mirFail $ "ClosureFnPointerShim callee " ++ show callOnceId ++ " not found"
  -- Check that the function `call_once` function signature looks like we
  -- expect, and extract the real argument types.
  --
  -- This implementation of `ClosureFnPointerShim` works for the cases we've
  -- seen so far, but hardcodes certain assumptions about the shape of the
  -- callee function `callOnceId` and duplicates a bit of the call translation
  -- from `callExp` and `callHandle`.  In the future, it might be better to
  -- turn this into a `CustomMirOp`, like `cloneShimDef` in `TransCustom`.
  -- However, currently it's not possible to obtain a function pointer to a
  -- `CustomOp` function (the `CustomOp` replaces the call instruction
  -- instead), which would need to be changed first.
  let callOnceArgTys = abiFnArgs sig
  when (sig ^. fsabi /= M.RustCall (M.RcSpreadArg 2)) $
    mirFail $ "expected " ++ show callOnceId
      ++ " to have RustCall ABI with spread_arg = 2, not " ++ show (sig ^. fsabi)
  callOnceArgTy0 <- case callOnceArgTys of
    x:_ -> return x
    [] -> mirFail $ "expected " ++ show callOnceId ++ " to have at least one arg, but got "
      ++ show callOnceArgTys
  when (callOnceArgTy0 /= M.TyClosure []) $
    mirFail $ "expected " ++ show callOnceId ++ " arg 0 to be an empty closure, but got "
      ++ show callOnceArgTy0
  -- Build the argument values for `call_once`.
  let tprArg0 = MirAggregateRepr
  arg0 <- mirAggregate_uninit_constSize 0
  let ctxArgs = Ctx.singleton tprArg0 Ctx.<++> fmapFC (R.typeOfAtom) argAtoms
  let args = Ctx.singleton arg0 Ctx.<++> fmapFC (R.AtomExpr @MIR) argAtoms
  -- More checks, necessary for the call below to typecheck.
  Refl <- testEqualityOrFail (FH.handleArgTypes fh) ctxArgs $
    "genClosureFnPointerShim: expected " ++ show callOnceId ++ " to take "
      ++ show ctxArgs ++ ", but got " ++ show (FH.handleArgTypes fh)
  Refl <- testEqualityOrFail (FH.handleReturnType fh) tprRet $
    "genClosureFnPointerShim: expected " ++ show callOnceId ++ " to return "
      ++ show tprRet ++ ", but got " ++ show (FH.handleReturnType fh)
  -- Actually call the function.
  let funcExp = R.App $ E.HandleLit fh
  label <- G.newLabel
  G.defineBlock label $ do
    ret <- G.call funcExp args
    G.returnFromFunction ret
  return label

transCommon :: forall h.
  ( HasCallStack, ?debug::Int, ?customOps::CustomOpMap, ?assertFalseOnError::Bool
  , ?printCrucible::Bool)
  => CollectionState
  -> M.DefId
  -> FnTransContext
  -> (forall s args ret.
    C.TypeRepr ret
    -> Ctx.Assignment (R.Atom s) args
    -> MirGenerator h s ret (G.Label s))
  -> ST h (Text, Core.AnyCFG MIR, FnTransInfo)
transCommon colState name context gen = do
    MirHandle _hname _hsig (handle :: FH.FnHandle args ret) <-
        case Map.lookup name (colState ^. handleMap) of
            Nothing -> error "bad handle!!"
            Just mh -> return mh
    ftiRef <- newSTRef mempty
    let rettype  = FH.handleReturnType handle
    let def :: G.FunctionDef MIR FnState args ret (ST h)
        def inputs = (s,f) where
          s = initFnState colState context
          f = do
              lbl <- gen rettype inputs
              fti <- use transInfo
              lift $ writeSTRef ftiRef fti
              G.jump lbl
    R.SomeCFG g <- defineFunctionNoAuxs handle def
    when ?printCrucible $ do
        traceM $ unwords [" =======", show name, "======="]
        traceShowM $ pretty g
        traceM $ unwords [" ======= end", show name, "======="]
    fti <- readSTRef ftiRef
    case SSA.toSSA g of
      Core.SomeCFG g_ssa -> return (M.idText name, Core.AnyCFG g_ssa, fti)

transInstance :: forall h.
  ( HasCallStack, ?debug::Int, ?customOps::CustomOpMap, ?assertFalseOnError::Bool
  , ?printCrucible::Bool)
  => CollectionState
  -> M.Intrinsic
  -> ST h (Maybe (Text, Core.AnyCFG MIR, Maybe FnTransInfo))
transInstance colState (M.Intrinsic defId (M.Instance kind origDefId _substs))
  -- If a function body is available, translate it, regardless of the `kind`.
  | Just fn <- colState ^. collection . M.functions . at defId = do
      (name, cfg, fti) <- transCommon colState defId (FnContext fn) (genFn fn)
      return $ Just (name, cfg, Just fti)
  -- For some `kind`s, we have special logic for generating a body.
  | M.IkVirtual dynTraitName methodIndex <- kind = do
      let methodId = origDefId
      (name, cfg) <- transVirtCall colState defId methodId dynTraitName methodIndex
      return $ Just (name, cfg, Nothing)
  | M.IkClosureFnPointerShim <- kind = do
      (name, cfg, fti) <- transCommon colState defId ShimContext
        (genClosureFnPointerShim origDefId)
      return $ Just (name, cfg, Just fti)
  | otherwise = return Nothing

transStatic :: forall h.
  ( HasCallStack, ?debug::Int, ?customOps::CustomOpMap, ?assertFalseOnError::Bool
  , ?printCrucible::Bool)
  => CollectionState
  -> M.Static
  -> ST h (Maybe (Text, Core.AnyCFG MIR, FnTransInfo))
transStatic colState st
  -- Statics with a `ConstVal` initializer don't need a CFG, and might not have
  -- a MIR body in `functions`.
  | Just _ <- st ^. M.sConstVal = return Nothing
  | otherwise = do
      let defId = st ^. M.sName
      fn <- case colState ^. collection . M.functions . at defId of
        Just x -> return x
        -- For each entry in `statics`, there should be a corresponding entry
        -- in `functions` giving the MIR body of the static initializer.
        Nothing -> panic "transStatic" ["function " ++ show defId ++ " not found for static"]
      (name, cfg, fti) <- transCommon colState defId (FnContext fn) (genFn fn)
      return $ Just (name, cfg, fti)


-- | Allocate method handles for each of the functions in the Collection
mkHandleMap :: (HasCallStack) => Collection -> FH.HandleAllocator -> IO HandleMap
mkHandleMap col halloc = mapM mkHandle (col ^. functions) where

    mkHandle :: M.Fn -> IO MirHandle
    mkHandle (M.Fn fname' _fargs fsig' _fbody)  = do
      let targs = abiFnArgs fsig'
          handleName = FN.functionNameFromText (M.idText fname')
      Some argctx <- case tyListToCtx col targs (Right . Some) of
         Left err -> fail ("mkHandle: " ++ err)
         Right x -> return x
      Some retrepr <- case tyToRepr col (fsig' ^. fsreturn_ty) of
        Left err -> fail ("mkHandle: " ++ err)
        Right x -> return x
      h <- FH.mkHandle' halloc handleName argctx retrepr
      return $ MirHandle fname' fsig' h

vtableShimName :: M.VtableName -> M.DefId -> Text
vtableShimName vtableName fnName =
    M.idText vtableName <> "$shim$" <> M.idText fnName

vtableShimSig :: M.VtableName -> M.DefId -> FnSig -> FnSig
vtableShimSig vtableName fnName sig = sig & M.fsarg_tys %~ \xs -> case xs of
    [] -> error $ unwords
        ["function", show fnName, "in", show vtableName, "has no receiver arg"]
    (_ : tys) -> M.TyErased : tys

-- | Allocate method handles for all vtable shims.
mkVtableMap :: (HasCallStack) => Collection -> FH.HandleAllocator -> IO VtableMap
mkVtableMap col halloc = mapM mkVtable (col ^. vtables)
  where
    mkVtable :: M.Vtable -> IO [MirHandle]
    mkVtable (M.Vtable name items) = mapM (mkHandle name) items

    mkHandle :: M.DefId -> M.VtableItem -> IO MirHandle
    mkHandle vtableName (VtableItem fnName _)
      | Just fn <- Map.lookup fnName (col ^. functions) = do
        let shimSig = vtableShimSig vtableName fnName (fn ^. M.fsig)
            handleName = FN.functionNameFromText (vtableShimName vtableName fnName)

        Some argctx <- case tyListToCtx col (abiFnArgs shimSig) (Right . Some) of
          Left err -> fail ("mkVtableMap: " ++ err)
          Right x -> return x

        Some retrepr <- case tyToRepr col (shimSig ^. M.fsreturn_ty) of
          Left err -> fail ("mkVtableMap: " ++ err)
          Right x -> return x

        h <- FH.mkHandle' halloc handleName argctx retrepr
        return $ MirHandle fnName shimSig h

      | otherwise = error $ unwords ["undefined function", show fnName, "in", show vtableName]

transVtable :: forall h. (HasCallStack, ?debug::Int, ?customOps::CustomOpMap, ?assertFalseOnError::Bool)
  => CollectionState
  -> M.Vtable
  -> ST h [(Text, Core.AnyCFG MIR)]
transVtable colState (M.Vtable name items)
  | Just handles <- Map.lookup name (colState ^. vtableMap) =
    zipWithM (transVtableShim colState name) items handles
  | otherwise = error $ unwords ["no vtableMap entry for", show name]

transVtableShim :: forall h. (HasCallStack, ?debug::Int, ?customOps::CustomOpMap, ?assertFalseOnError::Bool)
  => CollectionState
  -> M.VtableName
  -> M.VtableItem
  -> MirHandle
  -> ST h (Text, Core.AnyCFG MIR)
transVtableShim colState vtableName (VtableItem fnName defName)
        (MirHandle _hname _hsig (shimFH :: FH.FnHandle args ret)) =
    -- Unpack shim signature
    let shimArgs = FH.handleArgTypes shimFH in
    let shimRet = FH.handleReturnType shimFH in

    -- Retrieve impl Fn and FnHandle; unpack impl signature
    (\k -> case Map.lookup fnName (colState ^. collection.functions) of
            Just fn -> k fn
            Nothing -> die ["failed to look up implementation", show fnName])
        $ \implFn ->
    withMethodHandle fnName (die ["failed to look up implementation", show fnName])
        $ \implFH ->
    let implMirArg0 = case implFn ^. M.fsig . M.fsarg_tys of
                        arg_ty:_ -> arg_ty
                        [] -> die ["shim has no argument types"] in
    let implArgs = FH.handleArgTypes implFH in
    let implRet = FH.handleReturnType implFH in

    -- Peel off receiver from shim and impl arg lists
    -- NB: assignments built by `tyListToCtx` are constructed in reverse order
    elimAssignmentLeft shimArgs (die ["shim has no arguments"])
        $ \Refl shimArg0 shimArgs' ->
    elimAssignmentLeft implArgs (die ["impl has no arguments"])
        $ \Refl implArg0 implArgs' ->

    -- Check equalities over Crucible (translated) types:
    --  * Non-receiver arg types of impl and shim are equal
    (\k -> case testEquality implArgs' shimArgs' of { Just x -> k x;
        Nothing -> die ["argument type mismatch:", show implArgs, "vs", show shimArgs] })
        $ \Refl ->
    --  * Return types of impl and shim are equal
    (\k -> case testEquality implRet shimRet of { Just x -> k x;
        Nothing -> die ["return type mismatch:", show implRet, "vs", show shimRet] })
        $ \Refl ->
    --  * Shim receiver type is ANY
    (\k -> case testEquality shimArg0 C.AnyRepr of { Just x -> k x;
        Nothing -> die ["shim receiver is not ANY:", show shimArg0] }) $ \Refl ->

    -- Construct the shim and return it
    withBuildShim implMirArg0 implArg0 implArgs' implRet implFH $ \shimDef -> do
        R.SomeCFG g <- defineFunctionNoAuxs shimFH shimDef
        case SSA.toSSA g of
            Core.SomeCFG g_ssa -> return (vtableShimName vtableName fnName, Core.AnyCFG g_ssa)

  where
    die :: [String] -> a
    die xs = error $ dieMsg xs
    dieMsg :: [String] -> String
    dieMsg xs = unwords (["failed to generate vtable shim for", show vtableName,
            "entry", show defName, "(instance", show fnName, "):"] ++ xs)

    withMethodHandle :: forall r.
        MethName ->
        (r) ->
        (forall args' ret'. FH.FnHandle args' ret' -> r) ->
        r
    withMethodHandle name kNothing kJust =
        case Map.lookup name (colState ^. handleMap) of
            Just (MirHandle _ _ fh) -> kJust fh
            Nothing -> kNothing

    withBuildShim :: forall r recvTy argTys retTy.
        M.Ty -> C.TypeRepr recvTy -> C.CtxRepr argTys -> C.TypeRepr retTy ->
        FH.FnHandle (recvTy :<: argTys) retTy ->
        (G.FunctionDef MIR FnState (C.AnyType :<: argTys) retTy (ST h) -> r) ->
        r
    withBuildShim recvMirTy recvTy argTys retTy implFH k =
        k $ buildShim recvMirTy recvTy argTys retTy implFH

    fnState :: forall s. FnState s
    fnState = initFnState colState ShimContext

    buildShim :: forall recvTy argTys retTy .
        M.Ty -> C.TypeRepr recvTy -> C.CtxRepr argTys -> C.TypeRepr retTy ->
        FH.FnHandle (recvTy :<: argTys) retTy ->
        G.FunctionDef MIR FnState (C.AnyType :<: argTys) retTy (ST h)
    buildShim recvMirTy recvTy argTys _retTy implFH
      | M.TyRef    _recvMirTy' _ <- recvMirTy = buildShimForRef recvTy argTys implFH
      | M.TyRawPtr _recvMirTy' _ <- recvMirTy = buildShimForRef recvTy argTys implFH
      | otherwise = \_argsA -> (\x -> (fnState, x)) $ do
        mirFail $ dieMsg ["unsupported MIR receiver type", show recvMirTy]

    buildShimForRef :: forall recvTy argTys retTy .
        C.TypeRepr recvTy ->
        C.CtxRepr argTys ->
        FH.FnHandle (recvTy :<: argTys) retTy ->
        G.FunctionDef MIR FnState (C.AnyType :<: argTys) retTy (ST h)
    buildShimForRef recvTy argTys implFH = \argsA -> (\x -> (fnState, x)) $ do
        let (recv, args) = splitMethodArgs @C.AnyType @argTys argsA (Ctx.size argTys)
        recvDowncast <- G.fromJustExpr (R.App $ E.UnpackAny recvTy recv)
            (R.App $ E.StringLit $ fromString $ "bad receiver type for " ++ show fnName)
        G.tailCall (R.App $ E.HandleLit implFH) (recvDowncast <: args)

splitMethodArgs :: forall recvTy argTys s.
    Ctx.Assignment (R.Atom s) (recvTy :<: argTys) ->
    Ctx.Size argTys ->
    (R.Expr MIR s recvTy, Ctx.Assignment (R.Expr MIR s) argTys)
splitMethodArgs args argsSize =
    let (arg0, args') = splitAssignmentLeft args argsSize in
    (R.AtomExpr arg0, fmapFC R.AtomExpr args')


type (x :: k) :<: (xs :: Ctx.Ctx k) = Ctx.SingleCtx x Ctx.<+> xs

(<:) :: forall f tp ctx. f tp -> Ctx.Assignment f ctx -> Ctx.Assignment f (tp :<: ctx)
x <: xs = Ctx.singleton x Ctx.<++> xs

elimAssignmentLeft :: forall k f (ctx :: Ctx.Ctx k) r.
    Ctx.Assignment f ctx ->
    (Ctx.EmptyCtx :~: ctx -> r) ->
    (forall (tp :: k) (ctx' :: Ctx.Ctx k).
        tp :<: ctx' :~: ctx -> f tp -> Ctx.Assignment f ctx' -> r) ->
    r
elimAssignmentLeft xs kNil kCons = case Ctx.viewAssign xs of
    Ctx.AssignEmpty -> kNil Refl
    Ctx.AssignExtend xs' x' -> elimAssignmentLeft xs'
        (\Refl -> kCons Refl x' Ctx.empty)
        (\Refl x'' xs'' -> kCons Refl x'' (xs'' Ctx.:> x'))

unappendAssignment :: forall k f (xs :: Ctx.Ctx k) (ys :: Ctx.Ctx k).
    Ctx.Size ys ->
    Ctx.Assignment f (xs Ctx.<+> ys) ->
    (Ctx.Assignment f xs, Ctx.Assignment f ys)
unappendAssignment sz asn = case Ctx.viewSize sz of
    Ctx.ZeroSize ->
        -- ys ~ EmptyCtx  ->  xs <+> ys ~ xs
        (asn, Ctx.empty)
    Ctx.IncSize sz' ->
        -- ys ~ ys' ::> y'  ->  xs <+> ys ~ (xs <+> ys') ::> y'
        case Ctx.viewAssign asn of
            Ctx.AssignExtend asn' val' ->
                case unappendAssignment sz' asn' of
                    (asn1, asn2) -> (asn1, asn2 Ctx.:> val')

unwrapSingletonAssignment :: forall k f (tp :: k).
    Ctx.Assignment f (Ctx.SingleCtx tp) -> f tp
unwrapSingletonAssignment asn = case Ctx.viewAssign asn of
    Ctx.AssignExtend _ val -> val

splitAssignmentLeft :: forall k f (tp :: k) (ctx :: Ctx.Ctx k).
    Ctx.Assignment f (tp :<: ctx) ->
    Ctx.Size ctx ->
    (f tp, Ctx.Assignment f ctx)
splitAssignmentLeft xs sz =
    let (l, r) = unappendAssignment sz xs in
    (unwrapSingletonAssignment l, r)


lookupTrait :: M.Collection -> M.TraitName -> M.Trait
lookupTrait col traitName' = case col ^. M.traits . at traitName' of
    Just x -> x
    Nothing -> error $ "undefined trait " ++ show traitName'

-- Get the function signature of the declaration of a trait method.  Raises an
-- error if the method is not found in the trait.
traitMethodSig :: M.Trait -> M.MethName -> M.FnSig
traitMethodSig trait methName = case matchedMethSigs of
    [sig] -> sig
    [] -> error $ unwords ["undefined method", show methName,
        "in trait", show (trait ^. M.traitName)]
    _ -> error $ unwords ["multiply-defined method", show methName,
        "in trait", show (trait ^. M.traitName)]
  where
    matchedMethSigs =
        Maybe.mapMaybe (\item -> case item of
            TraitMethod methName' sig | methName' == methName -> Just sig
            _ -> Nothing) (trait ^. M.traitItems)

-- Generate method handles for all generated shims used in the current crate.
mkShimHandleMap :: (HasCallStack) =>
    Collection -> FH.HandleAllocator -> IO HandleMap
mkShimHandleMap col halloc = mconcat <$> mapM mkHandle (Map.toList $ col ^. M.intrinsics)
  where
    mkHandle :: (M.IntrinsicName, M.Intrinsic) ->
        IO (Map M.DefId MirHandle)
    mkHandle (name, intr)
      | IkVirtual dynTraitName _ <- intr ^. M.intrInst . M.inKind =
        let methName = intr ^. M.intrInst ^. M.inDefId
            trait = lookupTrait col dynTraitName
            methSig = traitMethodSig trait methName

            handleName = FN.functionNameFromText $ M.idText $ intr ^. M.intrName
        in liftM (Map.singleton name) $ do
            Some argctx <- case tyListToCtx col (abiFnArgs methSig) (Right . Some) of
              Left err -> fail ("mkShimHandleMap: " ++ err)
              Right x -> return x
            Some retrepr <- case tyToRepr col (methSig ^. M.fsreturn_ty) of
              Left err -> fail ("mkShimHandleMap: " ++ err)
              Right x -> return x
            h <- FH.mkHandle' halloc handleName argctx retrepr
            return $ MirHandle (intr ^. M.intrName) methSig h
      | IkClosureFnPointerShim <- intr ^. M.intrInst . M.inKind = do
        let callMutId = intr ^. M.intrInst . M.inDefId
        callMutFn <- case col ^. M.functions . at callMutId of
            Just x -> return x
            Nothing -> error $ "undefined function " ++ show callMutId
              ++ " for IkClosureFnPointerShim " ++ show name
        let callMutSig = callMutFn ^. M.fsig
        untupledArgTys <- case callMutSig ^? M.fsarg_tys . ix 1 of
            Just (M.TyTuple tys) -> return tys
            x -> error $ "expected tuple for second arg of " ++ show callMutId
              ++ ", but got " ++ show x ++ ", for IkClosureFnPointerShim " ++ show name
        let returnTy = callMutSig ^. M.fsreturn_ty
        let fnPtrSig = M.FnSig untupledArgTys returnTy RustAbi
        let handleName = FN.functionNameFromText $ M.idText $ intr ^. M.intrName

        Some argCtx <- case  tyListToCtx col untupledArgTys (Right . Some) of
          Left err -> fail ("mkShimHandleMap: " ++ err)
          Right x -> return x

        Some retRepr <- case tyToRepr col returnTy of
          Left err -> fail ("mkShimHandleMap: " ++ err)
          Right x -> return x

        h <- FH.mkHandle' halloc handleName argCtx retRepr
        let mh = MirHandle (intr ^. M.intrName) fnPtrSig h
        return $ Map.singleton name mh

      | otherwise = return Map.empty
      where


-- | Provided a @&dyn@ receiver and appropriate arguments, generate a pair of
-- @(function, arguments)@ expressions representing a virtual-call shim that
-- will look up and call the right concrete method and provide it those
-- arguments. See 'doVirtTailCall' for an example of actualy calling the
-- function.
mkVirtCall
  :: HasCallStack
  => M.Collection
  -> M.TraitName
  -> Integer -- ^ The method index
  -> C.TypeRepr recvTy -- ^ The type of the method receiver (should be @&dyn Trait@)
  -> R.Expr MIR s recvTy -- ^ The method receiver (should be @&dyn Trait@)
  -> C.CtxRepr argTys -- ^ The types of the arguments (excluding the receiver)
  -> Ctx.Assignment (R.Expr MIR s) argTys -- ^ The arguments (excluding the receiver)
  -> C.TypeRepr retTy -- ^ The return type
  -> G.Generator MIR s t ret (ST h)
    ( R.Expr MIR s (C.FunctionHandleType (C.AnyType :<: argTys) retTy)
    , Ctx.Assignment (R.Expr MIR s) (C.AnyType :<: argTys))
mkVirtCall col dynTraitName methIndex recvTy recvExpr argTys argExprs retTy =
    checkEq recvTy DynRefRepr (die ["method receiver is not `&dyn`/`&mut dyn`"])
        $ \Refl ->

    -- Unpack vtable type
    withSome vtableType $ \vtableStructTy ->
    elimStructType vtableStructTy (die ["vtable type is not a struct"])
        $ \Refl vtableTys ->

    let someVtableIdx = case Ctx.intIndex (fromInteger methIndex) (Ctx.size vtableTys) of
            Just x -> x
            Nothing -> die ["method index out of range for vtable:",
                "method =", show methIndex, "; size =", show (Ctx.size vtableTys)] in
    withSome someVtableIdx $ \vtableIdx ->

    -- Check that the vtable entry has the correct signature.
    elimFunctionHandleType (vtableTys Ctx.! vtableIdx) (die ["vtable entry is not a function"])
        $ \Refl vtsArgTys vtsRetTy ->
    elimAssignmentLeft vtsArgTys (die ["vtable shim has no arguments"])
        $ \Refl vtsRecvTy vtsArgTys' ->

    checkEq vtsRecvTy C.AnyRepr (die ["vtable shim receiver is not Any"])
        $ \Refl ->
    checkEq vtsArgTys' argTys
        (die ["vtable shim arguments don't match method; vtable shim =",
            show vtsArgTys', "; method =", show argTys])
        $ \Refl ->
    checkEq vtsRetTy retTy
        (die ["vtable shim return type doesn't match method; vtable shim =",
            show vtsRetTy, "; method =", show retTy])
        $ \Refl -> do

    let recvData = R.App $ E.GetStruct recvExpr dynRefDataIndex MirReferenceRepr
    let recvVtable = R.App $ E.GetStruct recvExpr dynRefVtableIndex C.AnyRepr

    -- Downcast the vtable to its proper struct type
    errBlk <- G.newLabel
    G.defineBlock errBlk $ do
        G.reportError $ R.App $ E.StringLit $ fromString $
            unwords ["bad vtable downcast:", show dynTraitName,
                "to", show vtableTys]

    let vtableStructTy' = C.StructRepr vtableTys
    okBlk <- G.newLambdaLabel' vtableStructTy'
    vtable <- G.continueLambda okBlk $ do
        G.branchMaybe (R.App $ E.UnpackAny vtableStructTy' recvVtable) okBlk errBlk

    -- Extract the function handle from the vtable
    let vtsFH = R.App $ E.GetStruct vtable vtableIdx
            (C.FunctionHandleRepr (C.AnyRepr <: argTys) vtsRetTy)

    pure (vtsFH, (R.App (E.PackAny MirReferenceRepr recvData) <: argExprs))

  where
    die :: [String] -> a
    die words' = error $ unwords
        (["failed to generate virtual-call shim for method", show methIndex,
            "of trait", show dynTraitName] ++ words')

    dynTrait = case col ^. M.traits . at dynTraitName of
        Just x -> x
        Nothing -> die ["undefined trait " ++ show dynTraitName]

    -- The type of the entire vtable.  Note `traitVtableType` wants the trait
    -- substs only, omitting the Self type.
    vtableType :: Some C.TypeRepr
    vtableType = case traitVtableType col dynTrait of
      Left err -> die ["vtableType: " ++ err]
      Right x -> x


-- | Use 'mkVirtCall' to create virtual-call function and argument expressions,
-- then tail-call that function on those arguments.
doVirtTailCall
  :: HasCallStack
  => M.Collection
  -> M.TraitName
  -> Integer -- ^ The method index
  -> C.TypeRepr recvTy -- ^ The type of the method receiver (should be @&dyn Trait@)
  -> R.Expr MIR s recvTy -- ^ The method receiver (should be @&dyn Trait@)
  -> C.CtxRepr argTys -- ^ The types of the arguments (excluding the receiver)
  -> Ctx.Assignment (R.Expr MIR s) argTys -- ^ The arguments (excluding the receiver)
  -> C.TypeRepr retTy -- ^ The return type
  -> G.Generator MIR s t retTy (ST h) (R.Expr MIR s retTy)
doVirtTailCall col dynTraitName methodIndex recvTy recvExpr argTys argExprs retTy = do
  (fnHandle, args) <- mkVirtCall col dynTraitName methodIndex recvTy recvExpr argTys argExprs retTy
  G.tailCall fnHandle args


-- | Use 'mkVirtCall' to create virtual-call function and argument expressions,
-- then call that function on those arguments.
--
-- Note the extra quantified variable in the return type in this vs.
-- 'doVirtTailCall', which makes this function slightly less restrictive:
--
-- > G.Generator MIR s t anyRetTy (ST h) (R.Expr MIR s retTy)
--
-- vs
--
-- > G.Generator MIR s t retTy    (ST h) (R.Expr MIR s retTy)
doVirtCall
  :: HasCallStack
  => M.Collection
  -> M.TraitName
  -> Integer -- ^ The method index
  -> C.TypeRepr recvTy -- ^ The type of the method receiver (should be @&dyn Trait@)
  -> R.Expr MIR s recvTy -- ^ The method receiver (should be @&dyn Trait@)
  -> C.CtxRepr argTys -- ^ The types of the arguments (excluding the receiver)
  -> Ctx.Assignment (R.Expr MIR s) argTys -- ^ The arguments (excluding the receiver)
  -> C.TypeRepr retTy -- ^ The return type
  -> G.Generator MIR s t anyRetTy (ST h) (R.Expr MIR s retTy)
doVirtCall col dynTraitName methodIndex recvTy recvExpr argTys argExprs retTy = do
  (fnHandle, args) <- mkVirtCall col dynTraitName methodIndex recvTy recvExpr argTys argExprs retTy
  G.call fnHandle args


-- | Translate a virtual call. The logic for looking up the right method in the
-- vtable is implemented in 'mkVirtCall'.
transVirtCall :: forall h. (HasCallStack, ?debug::Int, ?customOps::CustomOpMap, ?assertFalseOnError::Bool)
  => CollectionState
  -> M.IntrinsicName
  -> M.MethName
  -> M.TraitName
  -> Integer
  -> ST h (Text, Core.AnyCFG MIR)
transVirtCall colState intrName' methName dynTraitName methIndex
  | MirHandle _hname _hsig (methFH :: FH.FnHandle args ret) <- methMH =
    -- Unpack virtual-call shim signature.  The receiver should be `DynRefType`
    elimAssignmentLeft (FH.handleArgTypes methFH) (die ["method handle has no arguments"])
        $ \Refl recvTy argTys ->
    let retTy = FH.handleReturnType methFH

        -- | This is actually a 'G.FunctionDef', but that synonym hides some
        -- types we apparently need to write out in this signature.
        withArgs ::
          Ctx.Assignment (R.Atom s) args ->
          ([s], G.Generator MIR s [] ret (ST h) (R.Expr MIR s ret))
        withArgs argsAssn =
          let (recvExpr, argExprs) = splitMethodArgs argsAssn (Ctx.size argTys)
              callExpr =
                doVirtTailCall
                  (colState ^. collection)
                  dynTraitName
                  (fromInteger methIndex)
                  recvTy
                  recvExpr
                  argTys
                  argExprs
                  retTy
          in  ([], callExpr)
      in  do
            R.SomeCFG g <- defineFunctionNoAuxs methFH withArgs
            case SSA.toSSA g of
                Core.SomeCFG g_ssa -> return (M.idText intrName', Core.AnyCFG g_ssa)

  where
    die :: [String] -> a
    die words' = error $ unwords
        (["failed to generate virtual-call shim for", show methName,
            "(intrinsic", show intrName', "):"] ++ words')

    methMH = case Map.lookup intrName' (colState ^. handleMap) of
        Just x -> x
        Nothing -> die ["failed to find method handle for", show intrName']

withSome :: Some f -> (forall tp. f tp -> r) -> r
withSome s k = viewSome k s

elimStructType ::
    C.TypeRepr ty ->
    (r) ->
    (forall ctx. ty :~: C.StructType ctx -> C.CtxRepr ctx -> r) ->
    r
elimStructType ty kOther kStruct
  | C.StructRepr ctx <- ty = kStruct Refl ctx
  | otherwise = kOther

elimFunctionHandleType ::
    C.TypeRepr ty ->
    (r) ->
    (forall argTys retTy.
        ty :~: C.FunctionHandleType argTys retTy ->
        C.CtxRepr argTys -> C.TypeRepr retTy -> r) ->
    r
elimFunctionHandleType ty kOther kFH
  | C.FunctionHandleRepr argTys retTy <- ty = kFH Refl argTys retTy
  | otherwise = kOther

checkEq :: TestEquality f => f a -> f b ->
    r -> (a :~: b -> r) -> r
checkEq a b kNe kEq
  | Just pf <- testEquality a b = kEq pf
  | otherwise = kNe



mkDiscrMap :: M.Collection -> Map M.AdtName [Integer]
mkDiscrMap col = mconcat
    [ Map.singleton (adt ^. M.adtname) (adtIndices adt col)
    | adt <- Map.elems $ col ^. M.adts, Lens.is _Enum (adt ^. M.adtkind) ]

-- | Gather all of the 'M.DefId's in a 'M.Collection' and construct a
-- 'crateHashesMap' from it. To accomplish this, it suffices to look at the
-- domain of each map in a 'M.Collection' (with a handful of exceptions—see
-- the comments below), which ranges over 'M.DefId's.
mkCrateHashesMap :: M.Collection -> Map Text (NonEmpty Text)
mkCrateHashesMap
    (Collection _version
                functionsM adtsM adtsOrigM traitsM
                staticsM vtablesM intrinsicsM
                -- namedTys ranges over type names, which aren't full DefIds.
                _namedTysM
                _layoutsM
                _needDropsM
                langItemsM
                -- The roots and tests are duplicates of other Maps' DefIds.
                _rootsM _testsM) =
  Map.fromList $
       f functionsM
    ++ f adtsM
    ++ f adtsOrigM
    ++ f traitsM
    ++ f staticsM
    ++ f vtablesM
    ++ f intrinsicsM
    ++ f langItemsM
  where
    f :: Map M.DefId a -> [(Text, NonEmpty Text)]
    f m = map (\did -> (did ^. M.didCrate, did ^. M.didCrateDisambig :| []))
              (Map.keys m)

-- | Generate a map assigning a unique integer to every type in the program
mkTyIdMap :: M.Collection -> Map Ty Int
mkTyIdMap col = Map.fromList (zip (Map.keys (col ^. layouts)) [1..])

---------------------------------------------------------------------------

-- | transCollection: translate a MIR collection
transCollection ::
    (HasCallStack, ?debug::Int, ?assertFalseOnError::Bool,
     ?customOps::CustomOpMap,
     ?printCrucible::Bool)
    => M.Collection
    -> FH.HandleAllocator
    -> IO RustModule
transCollection col halloc = do

    when (?debug > 3) $ do
      traceM $ "MIR collection"
      traceM $ show (pretty col)

    -- build up the state in the Generator

    hmap1 <- mkHandleMap col halloc
    hmap2 <- mkShimHandleMap col halloc
    let hmap = hmap1 <> hmap2

    when (?debug > 3) $ do
      forM_ (Map.toList hmap) $ \(name, mh) -> do
        MirHandle _ sig handle <- return mh
        traceM $ "function " ++ show name ++ ":"
        traceM $ "  sig = " ++ show (pretty sig)
        traceM $ "  handle = " ++ show (FH.handleType handle)

    vm <- mkVtableMap col halloc

    -- translate the statics and create the initialization code
    -- allocate references for statics
    let allocateStatic :: Static -> Map M.DefId StaticVar -> IO (Map M.DefId StaticVar)
        allocateStatic static staticMap' = do
          Some staticRepr <- case tyToRepr col (static ^. sTy) of
            Left err -> fail ("allocateState: " ++ err)
            Right x -> return x
          let gname =  (M.idText (static ^. sName) <> "_global")
          g <- G.freshGlobalVar halloc gname staticRepr
          return $ Map.insert (static ^. sName) (StaticVar g) staticMap'

    sm <- foldrM allocateStatic Map.empty (col ^. statics)

    let dm = mkDiscrMap col
    let chm = mkCrateHashesMap col
    let tidm = mkTyIdMap col

    let colState :: CollectionState
        colState = CollectionState hmap vm sm dm chm tidm col

    -- translate all of the functions
    fnInfo <- Maybe.catMaybes <$>
      mapM (stToIO . transInstance colState) (Map.elems (col ^. M.intrinsics))
    staticInfo <- Maybe.catMaybes <$>
      mapM (stToIO . transStatic colState) (Map.elems (col ^. M.statics))
    let allInfo = fnInfo ++ [(n, c, Just i) | (n, c, i) <- staticInfo]
    let pairs1 = [(name, cfg) | (name, cfg, _) <- allInfo]
    let transInfo' = Map.fromList [(name, fti) | (name, _, Just fti) <- allInfo]
    pairs2 <- mapM (stToIO . transVtable colState) (Map.elems (col ^. M.vtables))

    return $ RustModule
                { _rmCS    = colState
                , _rmCFGs  = Map.fromList (pairs1 <> concat pairs2)
                , _rmTransInfo = transInfo'
                }

-- | Produce a crucible CFG that initializes the global variables for the static
-- part of the crate.
--
-- Note that while static items' definitions can depend on other static items,
-- this function does not currently translate static items in a way that
-- respects dependency order in general. (See #1108.) We do make a limited
-- effort to minimize the chances of static items being translated in the wrong
-- order, however. See the comments near @constValStatics@/@nonConstValStatics@
-- below.
transStatics ::
  (?debug::Int,?customOps::CustomOpMap,?assertFalseOnError::Bool) =>
  CollectionState -> FH.HandleAllocator -> IO (Core.AnyCFG MIR)
transStatics colState halloc = do
  let sm = colState ^. staticMap
  let hmap = colState ^. handleMap
  let initializeStatic :: forall h s r . Static -> MirGenerator h s r ()
      initializeStatic static =
        let staticName = static ^. sName in
        case Map.lookup staticName sm of
          Just (StaticVar g) ->
            let repr = G.globalType g in
            if |  Just constval <- static ^. sConstVal
               -> do let constty = static ^. sTy
                     Some tpr <- tyToReprM constty
                     MirExp constty' constval' <- transConstVal constty (Some tpr) constval
                     case testEquality repr constty' of
                       Just Refl -> G.writeGlobal g constval'
                       Nothing -> error $ "BUG: invalid type for constant initializer " ++ fmt staticName
                                       ++ ", expected " ++ show repr ++ ", got " ++ show constty'

               |  Just (MirHandle _ _ (handle :: FH.FnHandle init ret))
                    <- Map.lookup staticName hmap
               -> case ( testEquality repr        (FH.handleReturnType handle)
                       , testEquality (Ctx.empty) (FH.handleArgTypes handle)
                       ) of
                    (Just Refl, Just Refl) -> do
                      val <- G.call (G.App $ E.HandleLit handle) Ctx.empty
                      G.writeGlobal g val

                    _ -> error $ "BUG: invalid type for initializer function " ++ fmt staticName

               |  otherwise
               -> error $ "BUG: cannot find initializer for static " ++ fmt staticName
          Nothing -> error $ "BUG: cannot find global for " ++ fmt staticName

  -- TODO: make the name of the static initialization function configurable
  let initName = FN.functionNameFromText "static_initializer"
  initHandle <- FH.mkHandle' halloc initName Ctx.empty C.UnitRepr
  let allStatics :: [Static]
      allStatics = Map.elems (colState ^. collection.statics)
  -- Partition the static items into those with constant initializer expressions
  -- (constValStatics) and those with non-constant initializer expressions
  -- (nonConstValStatics). We do this because nonConstValStatics can depend on
  -- constValStatics, but because constValStatics typically use names like
  -- {{alloc}}[0], their names are almost certain to be later alphabetically
  -- than nonConstValStatics' names. This, in turn, is liable to trigger the
  -- issues observed in #1108 when one tries to translate a nonConstValStatic
  -- before the constValStatic that it depends on.
  --
  -- To work around #1108, we deliberately translate all constValStatics before
  -- translating any nonConstValStatics. This is not a complete fix for #1108,
  -- but it does make it far less likely to appear in practice.
  let constValStatics, nonConstValStatics :: [Static]
      (constValStatics, nonConstValStatics) =
        List.partition (\s -> Maybe.isJust (s ^. sConstVal)) allStatics
  let def :: G.FunctionDef MIR FnState Ctx.EmptyCtx C.UnitType (ST w)
      def _inputs = (s, f) where
          s = initFnState colState StaticContext
          f = do mapM_ initializeStatic constValStatics
                 mapM_ initializeStatic nonConstValStatics
                 return (R.App $ E.EmptyApp)
  init_cfg <- stToIO $ do
    R.SomeCFG g <- defineFunctionNoAuxs initHandle def
    case SSA.toSSA g of
        Core.SomeCFG g_ssa -> return (Core.AnyCFG g_ssa)

  return init_cfg

------------------------------------------------------------------------------------------------


--
-- Generate a loop that copies `len` elements starting at `ptr0` into a vector.
--
vectorCopy :: C.TypeRepr tp ->
              G.Expr MIR s MirReferenceType ->
              G.Expr MIR s UsizeType ->
              MirGenerator h s ret (G.Expr MIR s (C.VectorType tp))
vectorCopy tpr ptr0 len = do
  let cond = S.app $ usizeEq len $ S.app $ usizeLit 0
  c_id <- G.newLambdaLabel' (C.VectorRepr tpr)
  -- Then branch
  x_id <- G.defineBlockLabel $ do
    G.jumpToLambda c_id $ S.app $ E.VectorLit tpr mempty
  -- Else branch
  y_id <- G.defineBlockLabel $ do
    elt0 <- readMirRef tpr ptr0
    let out0 = S.app $ E.VectorReplicate tpr (S.app $ usizeToNat len) elt0
    iRef <- G.newRef $ S.app $ usizeLit 0
    ptrRef <- G.newRef ptr0
    outRef <- G.newRef out0
    let pos = PL.InternalPos
    G.while (pos, do i <- G.readRef iRef
                     return (G.App $ usizeLt i len))
            (pos, do i <- G.readRef iRef
                     ptr <- G.readRef ptrRef
                     out1 <- G.readRef outRef
                     elt <- readMirRef tpr ptr
                     let i' = S.app $ usizeAdd i (S.app $ usizeLit 1)
                     ptr' <- mirRef_offset ptr (S.app $ usizeLit 1)
                     let out2 = S.app $ vectorSetUsize tpr R.App out1 i elt
                     G.writeRef iRef i'
                     G.writeRef ptrRef ptr'
                     G.writeRef outRef out2)
    out1 <- G.readRef outRef
    G.jumpToLambda c_id out1
  G.continueLambda c_id (G.branch cond x_id y_id)

-- | Generate a loop that copies `len` elements starting at `ptr0` into a new
-- `MirAggregate`.  `size` is used as both the element size and the stride of
-- the array, matching the way that rustc lays out arrays.
aggregateCopy_constLen ::
  C.TypeRepr tp ->
  G.Expr MIR s MirReferenceType ->
  Int ->
  Word ->
  MirGenerator h s ret (G.Expr MIR s MirAggregateType)
aggregateCopy_constLen tpr ptr0 len size = do
  ag <- mirAggregate_uninit_constSize (fromIntegral len * size)
  ag' <- foldM
    (\ag' i -> do
       ptr <- mirRef_offset ptr0 (S.app $ usizeLit $ fromIntegral i)
       elt <- readMirRef tpr ptr
       mirAggregate_set (fromIntegral i * size) size tpr elt ag')
    ag (init [0 .. len])
  return ag'

ptrCopy ::
    C.TypeRepr tp ->
    G.Expr MIR s MirReferenceType ->
    G.Expr MIR s MirReferenceType ->
    G.Expr MIR s UsizeType ->
    MirGenerator h s ret ()
ptrCopy tpr src dest len = do
    iRef <- G.newRef $ S.app $ usizeLit 0
    let pos = PL.InternalPos
    G.while (pos, do i <- G.readRef iRef
                     return (G.App $ usizeLt i len))
            (pos, do i <- G.readRef iRef
                     src' <- mirRef_offset src i
                     dest' <- mirRef_offset dest i
                     val <- readMirRef tpr src'
                     writeMirRef tpr dest' val
                     let i' = S.app $ usizeAdd i (S.app $ usizeLit 1)
                     G.writeRef iRef i')
    G.dropRef iRef

copyNonOverlapping ::
    C.TypeRepr tp ->
    R.Expr MIR s MirReferenceType ->
    R.Expr MIR s MirReferenceType ->
    R.Expr MIR s UsizeType ->
    MirGenerator h s ret (MirExp s)
copyNonOverlapping tpr src dest count = do
    -- `count` must not exceed isize::MAX, else the overlap check
    -- will misbehave.
    let sizeBits = fromIntegral $ C.intValue (C.knownNat @SizeBits)
    let maxCount = R.App $ usizeLit (1 `shift` (sizeBits - 1))
    let countOk = R.App $ usizeLt count maxCount
    G.assertExpr countOk $ S.litExpr "count overflow in copy_nonoverlapping"

    nonOverlapping <- isNonOverlapping src dest count
    G.assertExpr nonOverlapping $ S.litExpr "src and dest overlap in copy_nonoverlapping"

    ptrCopy tpr src dest count
    return $ MirExp C.UnitRepr $ R.App E.EmptyApp

-- | Check if two allocations of the given size are non-overlapping.
-- Assumes @size <= isize::MAX@.
isNonOverlapping ::
    R.Expr MIR s MirReferenceType ->
    R.Expr MIR s MirReferenceType ->
    R.Expr MIR s UsizeType ->
    MirGenerator h s ret (G.Expr MIR s C.BoolType)
isNonOverlapping src dest size = do
  maybeOffset <- mirRef_tryOffsetFrom dest src
  -- If `maybeOffset` is Nothing, then src and dest definitely
  -- don't overlap, since they come from different allocations.
  -- If it's Just, the value must be >= size or <= -size to put
  -- the two regions far enough apart.
  let size' = usizeToIsize R.App size
      destAbove offset = R.App $ isizeLe size' offset
      destBelow offset = R.App $ isizeLe offset (R.App $ isizeNeg size')
  G.caseMaybe maybeOffset C.BoolRepr $ G.MatchMaybe
    (\offset -> return $ R.App $ E.Or (destAbove offset) (destBelow offset))
    (return $ R.App $ E.BoolLit True)

--  LocalWords:  params IndexMut FnOnce Fn IntoIterator iter impl
--  LocalWords:  tovec fromelem tmethsubst MirExp initializer callExp
--  LocalWords:  mkTraitObject mkCustomTraitObject TyClosure
--  LocalWords:  transTerminator transStatement

------------------------------------------------------------------------------------------------

-- | Define a CFG for a function, and check that there are no auxiliary
-- functions generated alongside it. This is a common pattern used throughout
-- this module.
defineFunctionNoAuxs ::
  FH.FnHandle init ret {- ^ Handle for the generated function -} ->
  G.FunctionDef MIR t init ret (ST s) {- ^ Generator action and initial state -} ->
  ST s (R.SomeCFG MIR init ret)
defineFunctionNoAuxs handle def = do
  ng <- newSTNonceGenerator
  (mainCFG, auxCFGs) <- G.defineFunction PL.InternalPos ng handle def
  unless (null auxCFGs) $
    error $ "defineFunctionNoAuxs: Expected no auxiliary functions, received "
         ++ show (length auxCFGs)
  pure mainCFG