content: -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.LLVM.Translation.Constant
  -- Description      : LLVM constant expression evaluation and GEPs
  -- Copyright        : (c) Galois, Inc 2014-2015
  -- License          : BSD3
  -- Maintainer       : Rob Dockins <rdockins@galois.com>
  -- Stability        : provisional
  --
  -- This module provides translation-time evaluation of constant
  -- expressions.  It also provides an intermediate representation
  -- for GEP (getelementpointer) instructions that makes more explicit
  -- the places where vectorization may occur, as well as resolving type
  -- sizes and field offsets.
  --
  -- See @liftConstant@ for how to turn these into expressions.
  -----------------------------------------------------------------------
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ParallelListComp #-}
  {-# LANGUAGE PatternGuards #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  
  module Lang.Crucible.LLVM.Translation.Constant
    ( -- * Representation of LLVM constant values
      LLVMConst(..)
    , boolConst
    , intConst
  
      -- * Translations from LLVM syntax to constant values
    , transConstant
    , transConstantWithType
    , transConstant'
    , transConstantExpr
  
      -- * Intermediate representation for GEP
    , GEP(..)
    , GEPResult(..)
    , translateGEP
  
      -- * Utility functions
    , showInstr
    , testBreakpointFunction
    ) where
  
  import           Control.Lens( to, (^.) )
  import           Control.Monad
  import           Control.Monad.Except
  import           Data.ByteString (ByteString)
  import qualified Data.ByteString as BS
  import           Data.Bits
  import           Data.Kind
  import           Data.List (intercalate, isPrefixOf)
  import           Data.Traversable
  import           Data.Fixed (mod')
  import qualified Data.Vector as V
  import           Numeric.Natural
  import           GHC.TypeNats
  
  import qualified Text.LLVM.AST as L
  import qualified Text.LLVM.PP as L
  
  import qualified Data.BitVector.Sized as BV
  import qualified Data.BitVector.Sized.Overflow as BV
  import           Data.Parameterized.NatRepr
  import           Data.Parameterized.Some
  import           Data.Parameterized.DecidableEq (decEq)
  
  import           Lang.Crucible.LLVM.Bytes
  import           Lang.Crucible.LLVM.DataLayout( intLayout, EndianForm(..) )
  import           Lang.Crucible.LLVM.MemModel.Pointer
  import           Lang.Crucible.LLVM.MemType
  import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
  import           Lang.Crucible.LLVM.Translation.Types
  import           Lang.Crucible.LLVM.TypeContext
  
  -- | Pretty print an LLVM instruction
  showInstr :: L.Instr -> String
  showInstr i = show (L.ppLLVM38 (L.ppInstr i))
  
  -- | Intermediate representation of a GEP.
  --   A @GEP n expr@ is a representation of a GEP with
  --   @n@ parallel vector lanes with expressions represented
  --   by @expr@ values.
  data GEP (n :: Nat) (expr :: Type) where
    -- | Start a GEP with a single base pointer
    GEP_scalar_base  :: expr -> GEP 1 expr
  
    -- | Start a GEP with a vector of @n@ base pointers
    GEP_vector_base  :: NatRepr n -> expr -> GEP n expr
  
    -- | Copy a scalar base vector pointwise into a
    --   vector of length @n@.
    GEP_scatter      :: NatRepr n -> GEP 1 expr -> GEP n expr
  
    -- | Add the offset corresponding to the given field
    --   pointwise to each pointer
    GEP_field        :: FieldInfo -> GEP n expr -> GEP n expr
  
    -- | Add an offset corresponding to the given array index
    --   (multiplied by the given type size) pointwise to the pointers
    --   in each lane.
    GEP_index_each   :: MemType -> GEP n expr -> expr -> GEP n expr
  
    -- | Given a vector of offsets (whose length must match
    --   the number of lanes), multiply each one by the
    --   type size, and add the offsets to the corresponding
    --   pointers.
    GEP_index_vector :: MemType -> GEP n expr -> expr -> GEP n expr
  
  instance Functor (GEP n) where
    fmap = fmapDefault
  instance Foldable (GEP n) where
    foldMap = foldMapDefault
  
  instance Traversable (GEP n) where
    traverse f gep = case gep of
      GEP_scalar_base x            -> GEP_scalar_base <$> f x
      GEP_vector_base n x          -> GEP_vector_base n <$> f x
      GEP_scatter n gep'           -> GEP_scatter n <$> traverse f gep'
      GEP_field fi gep'            -> GEP_field fi <$> traverse f gep'
      GEP_index_each mt gep' idx   -> GEP_index_each mt <$> traverse f gep' <*> f idx
      GEP_index_vector mt gep' idx -> GEP_index_vector mt <$> traverse f gep' <*> f idx
  
  -- | The result of a GEP instruction translation.  It records the number
  --   of parallel vector lanes in the resulting instruction, the resulting
  --   memory type of the instruction, and the sequence of sub-operations
  --   required to compute the GEP instruction.
  data GEPResult expr where
    GEPResult :: (1 <= n) => NatRepr n -> MemType -> GEP n expr -> GEPResult expr
  
  instance Functor GEPResult where
    fmap = fmapDefault
  instance Foldable GEPResult where
    foldMap = foldMapDefault
  
  instance Traversable GEPResult where
    traverse f (GEPResult n mt gep) = GEPResult n mt <$> traverse f gep
  
  
  -- | Given the data for an LLVM getelementpointer instruction,
  -- preprocess the instruction into a @GEPResult@, checking
  -- types, computing vectorization lanes, etc.
  --
  -- As a concrete example, consider a call to
  -- @'translateGEP' inbounds baseTy basePtr elts@ with the following
  -- instruction:
  --
  -- @
  -- getelementptr [12 x i8], ptr %aptr, i64 0, i32 1
  -- @
  --
  -- Here:
  --
  -- * @inbounds@ is 'False', as the keyword of the same name is missing from
  --   the instruction. (Currently, @crucible-llvm@ ignores this information.)
  --
  -- * @baseTy@ is @[12 x i8]@. This is the type used as the basis for
  --   subsequent calculations.
  --
  -- * @basePtr@ is @ptr %aptr@. This pointer is used as the base address to
  --   start calculations from. Note that the type of @basePtr@ is /not/
  --   @baseTy@, but rather a pointer type.
  --
  -- * The @elts@ are @[i64 0, i32 1]@. These are the indices that indicate
  --   which of the elements of the aggregate object are indexed.
  translateGEP :: forall wptr m.
    (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
    Bool              {- ^ inbounds flag -} ->
    L.Type            {- ^ base type for calculations -} ->
    L.Typed L.Value   {- ^ base pointer expression -} ->
    [L.Typed L.Value] {- ^ index arguments -} ->
    m (GEPResult (L.Typed L.Value))
  
  translateGEP _ _ _ [] =
    throwError "getelementpointer must have at least one index"
  
  translateGEP inbounds baseTy basePtr elts =
    do baseMemType <- liftMemType baseTy
       mt <- liftMemType (L.typedType basePtr)
       -- Input value to a GEP must have a pointer type (or be a vector of pointer
       -- types), and the base type used for calculations must be representable
       -- as a memory type. The resulting memory type drives the interpretation of
       -- the GEP arguments.
       case mt of
         -- Vector base case, with as many lanes as there are input pointers
         VecType n vmt
           | isPointerMemType vmt
           , Some lanes <- mkNatRepr n
           , Just LeqProof <- isPosNat lanes
           ->  let mt' = ArrayType 0 baseMemType in
               go lanes mt' (GEP_vector_base lanes basePtr) elts
  
         -- Scalar base case with exactly 1 lane
         _ | isPointerMemType mt
           ->  let mt' = ArrayType 0 baseMemType in
               go (knownNat @1) mt' (GEP_scalar_base basePtr) elts
  
           | otherwise
           -> badGEP
   where
   badGEP :: m a
   badGEP = throwError $ unlines [ "Invalid GEP", showInstr (L.GEP inbounds baseTy basePtr elts) ]
  
   -- This auxilary function builds up the intermediate GEP mini-instructions that compute
   -- the overall GEP, as well as the resulting memory type of the final pointers and the
   -- number of vector lanes eventually computed by the GEP.
   go ::
     (1 <= lanes) =>
     NatRepr lanes               {- Number of lanes of the GEP so far -} ->
     MemType                     {- Memory type of the incoming pointer(s) -} ->
     GEP lanes (L.Typed L.Value) {- partial GEP computation -} ->
     [L.Typed L.Value]           {- remaining arguments to process -} ->
     m (GEPResult (L.Typed L.Value))
  
   -- Final step, all arguments are used up, return the GEPResult
   go lanes mt gep [] = return (GEPResult lanes mt gep)
  
   -- Resolve one offset value and recurse
   go lanes mt gep (off:xs) =
     do offt <- liftMemType (L.typedType off)
        -- The meaning of the offset depends on the static type of the intermediate result
        case mt of
          ArrayType _ mt' -> goArray lanes off offt mt' gep xs
          VecType   _ mt' -> goArray lanes off offt mt' gep xs
          StructType si   -> goStruct lanes off offt si gep xs
          _ -> badGEP
  
   -- If it is an array type, the offset should be considered an array index, or
   -- vector of array indices.
   goArray ::
     (1 <= lanes) =>
     NatRepr lanes   {- Number of lanes of the GEP so far -} ->
     L.Typed L.Value {- Current index value -} ->
     MemType         {- MemType of the index value -} ->
     MemType         {- MemType of the incoming pointer(s) -} ->
     GEP lanes (L.Typed L.Value) {- partial GEP computation -} ->
     [L.Typed L.Value] {- remaining arguments to process -} ->
     m (GEPResult (L.Typed L.Value))
   goArray lanes off offt mt' gep xs =
      case offt of
        -- Single array index, apply pointwise to all intermediate pointers
        IntType _
          -> go lanes mt' (GEP_index_each mt' gep off) xs
  
        -- Vector of indices, matching the current number of lanes, apply
        -- each offset to the corresponding base pointer
        VecType n (IntType _)
          | natValue lanes == n
          -> go lanes mt' (GEP_index_vector mt' gep off) xs
  
        -- Vector of indices, with a single incoming base pointer.  Scatter
        -- the base pointer across the correct number of lanes, and then
        -- apply the vector of offsets componentwise.
        VecType n (IntType _)
          | Some n' <- mkNatRepr n
          , Just LeqProof <- isPosNat n'
          , Just Refl <- testEquality lanes (knownNat @1)
          -> go n' mt' (GEP_index_vector mt' (GEP_scatter n' gep) off) xs
  
        -- Otherwise, some sort of mismatch occured.
        _ -> badGEP
  
   -- If it is a structure type, the index must be a constant value that indicates
   -- which field (counting from 0) is to be indexed.
   goStruct ::
     (1 <= lanes) =>
     NatRepr lanes     {- Number of lanes of the GEP so far -} ->
     L.Typed L.Value   {- Field index number -} ->
     MemType           {- MemType of the field index -} ->
     StructInfo        {- Struct layout information -} ->
     GEP lanes (L.Typed L.Value) {- partial GEP computation -} ->
     [L.Typed L.Value] {- remaining arguments to process -} ->
     m (GEPResult (L.Typed L.Value))
   goStruct lanes off offt si gep xs =
      do off' <- transConstant' offt (L.typedValue off)
         case off' of
           -- Special case for the zero value
           ZeroConst (IntType _) -> goidx 0
  
           -- Single index; compute the corresponding field.
           IntConst _ idx -> goidx (BV.asUnsigned idx)
  
           -- Special case.  A vector of indices is allowed, but it must be of the correct
           -- number of lanes, and each (constant) index must be the same value.
           VectorConst (IntType _) (i@(IntConst _ idx) : is) | all (same i) is -> goidx (BV.asUnsigned idx)
             where
             same :: LLVMConst -> LLVMConst -> Bool
             same (IntConst wx x) (IntConst wy y)
               | Just Refl <- testEquality wx wy = x == y
             same _ _ = False
  
           -- Otherwise, invalid GEP instruction
           _ -> badGEP
  
              -- using the information from the struct type, figure out which
              -- field is indicated
        where goidx idx | 0 <= idx && idx < toInteger (V.length flds) =
                   go lanes (fiType fi) (GEP_field fi gep) xs
                 where flds = siFields si
                       fi   = flds V.! (fromInteger idx)
  
              goidx _ = badGEP
  
  
  -- | Translation-time LLVM constant values.
  data LLVMConst where
    -- | A constant value consisting of all zero bits.
    ZeroConst     :: !MemType -> LLVMConst
    -- | A constant integer value, with bit-width @w@.
    IntConst      :: (1 <= w) => !(NatRepr w) -> !(BV.BV w) -> LLVMConst
    -- | A constant floating point value.
    FloatConst    :: !Float -> LLVMConst
    -- | A constant double value.
    DoubleConst   :: !Double -> LLVMConst
    -- | A constant long double value (X86_FP80)
    LongDoubleConst :: !L.FP80Value -> LLVMConst
    -- | A constant sequence of bytes
    StringConst   :: !ByteString -> LLVMConst
    -- | A constant array value.
    ArrayConst    :: !MemType -> [LLVMConst] -> LLVMConst
    -- | A constant vector value.
    VectorConst   :: !MemType -> [LLVMConst] -> LLVMConst
    -- | A constant structure value.
    StructConst   :: !StructInfo -> [LLVMConst] -> LLVMConst
    -- | A pointer value, consisting of a concrete offset from a global symbol.
    SymbolConst   :: !L.Symbol -> !Integer -> LLVMConst
    -- | The @undef@ value is quite strange. See: The LLVM Language Reference,
    -- § Undefined Values.
    UndefConst    :: !MemType -> LLVMConst
  
  
  -- | This also can't be derived, but is completely uninteresting.
  instance Show LLVMConst where
    show lc = intercalate " " $
      case lc of
        (ZeroConst mem)     -> ["ZeroConst", show mem]
        (IntConst w x)      -> ["IntConst", show w, show x]
        (FloatConst f)      -> ["FloatConst", show f]
        (DoubleConst d)     -> ["DoubleConst", show d]
        ld@(LongDoubleConst _)-> ["LongDoubleConst", show ld]
        (ArrayConst mem a)  -> ["ArrayConst", show mem, show a]
        (VectorConst mem v) -> ["VectorConst", show mem, show v]
        (StructConst si a)  -> ["StructConst", show si, show a]
        (SymbolConst s x)   -> ["SymbolConst", show s, show x]
        (UndefConst mem)    -> ["UndefConst", show mem]
        (StringConst bs)    -> ["StringConst", show bs]
  
  -- | The interesting cases here are:
  --  * @IntConst@: GHC can't derive this because @IntConst@ existentially
  --    quantifies the integer's width. We say that two integers are equal when
  --    they have the same width *and* the same value.
  --  * @UndefConst@: Two @undef@ values aren't necessarily the same...
  instance Eq LLVMConst where
    (ZeroConst mem1)      == (ZeroConst mem2)      = mem1 == mem2
    (IntConst w1 x1)      == (IntConst w2 x2)      =
      case decEq w1 w2 of
        Left Refl -> x1 == x2
        Right _   -> False
    (FloatConst f1)       == (FloatConst f2)       = f1 == f2
    (DoubleConst d1)      == (DoubleConst d2)      = d1 == d2
    (LongDoubleConst ld1) == (LongDoubleConst ld2) = ld1 == ld2
    (ArrayConst mem1 a1)  == (ArrayConst mem2 a2)  = mem1 == mem2 && a1 == a2
    (VectorConst mem1 v1) == (VectorConst mem2 v2) = mem1 == mem2 && v1 == v2
    (StructConst si1 a1)  == (StructConst si2 a2)  = si1 == si2   && a1 == a2
    (SymbolConst s1 x1)   == (SymbolConst s2 x2)   = s1 == s2     && x1 == x2
    (UndefConst  _)       == (UndefConst _)        = False
    _                     == _                     = False
  
  -- | Create an LLVM constant value from a boolean.
  boolConst :: Bool -> LLVMConst
  boolConst False = IntConst (knownNat @1) (BV.zero knownNat)
  boolConst True = IntConst (knownNat @1) (BV.one knownNat)
  
  -- | Create an LLVM constant of a given width.  The resulting integer
  --   constant value will be the unsigned integer value @n mod 2^w@.
  intConst ::
    MonadError String m =>
    Natural {- ^ width of the integer constant, @w@ -} ->
    Integer {- ^ value of the integer constant, @n@ -} ->
    m LLVMConst
  intConst n 0
    = return (ZeroConst (IntType n))
  intConst n x
    | Some w <- mkNatRepr n
    , Just LeqProof <- isPosNat w
    = return (IntConst w (BV.mkBV w x))
  intConst n _
    = throwError ("Invalid integer width: " ++ show n)
  
  -- | Compute the constant value of an expression.  Fail if the
  --   given value does not represent a constant.
  transConstantWithType ::
    (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
    L.Typed L.Value ->
    m (MemType, LLVMConst)
  transConstantWithType (L.Typed tp v) =
    do mt <- liftMemType tp
       c <- transConstant' mt v
       return (mt, c)
  
  transConstant ::
    (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
    L.Typed L.Value ->
    m LLVMConst
  transConstant x = snd <$> transConstantWithType x
  
  -- | Compute the constant value of an expression.  Fail if the
  --   given value does not represent a constant.
  transConstant' ::
    (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
    MemType ->
    L.Value ->
    m LLVMConst
  transConstant' tp (L.ValUndef) =
    return (UndefConst tp)
  transConstant' (IntType n) (L.ValInteger x) =
    intConst n x
  transConstant' (IntType 1) (L.ValBool b) =
    return . IntConst (knownNat @1) $ if b
                                      then (BV.one knownNat)
                                      else (BV.zero knownNat)
  transConstant' FloatType (L.ValFloat f) =
    return (FloatConst f)
  transConstant' DoubleType (L.ValDouble d) =
    return (DoubleConst d)
  transConstant' X86_FP80Type (L.ValFP80 ld) =
    return (LongDoubleConst ld)
  transConstant' (PtrType _) (L.ValSymbol s) =
    return (SymbolConst s 0)
  transConstant' PtrOpaqueType (L.ValSymbol s) =
    return (SymbolConst s 0)
  transConstant' tp L.ValZeroInit =
    return (ZeroConst tp)
  transConstant' (PtrType stp) L.ValNull =
    return (ZeroConst (PtrType stp))
  transConstant' PtrOpaqueType L.ValNull =
    return (ZeroConst PtrOpaqueType)
  transConstant' (VecType n tp) (L.ValVector _tp xs)
    | n == fromIntegral (length xs)
    = VectorConst tp <$> traverse (transConstant' tp) xs
  transConstant' (ArrayType n tp) (L.ValArray _tp xs)
    | n == fromIntegral (length xs)
    = ArrayConst tp <$> traverse (transConstant' tp) xs
  transConstant' (StructType si) (L.ValStruct xs)
    | not (siIsPacked si)
    , V.length (siFields si) == length xs
    = StructConst si <$> traverse transConstant xs
  transConstant' (StructType si) (L.ValPackedStruct xs)
    | siIsPacked si
    , V.length (siFields si) == length xs
    = StructConst si <$> traverse transConstant xs
  
  transConstant' (ArrayType n tp) (L.ValString cs)
    | tp == IntType 8, n == fromIntegral (length cs)
    = return . StringConst $! BS.pack cs
  
  transConstant' _ (L.ValConstExpr cexpr) = transConstantExpr cexpr
  
  transConstant' tp val =
    throwError $ unlines [ "Cannot compute constant value for expression: "
                         , "Type: "  ++ (show $ ppMemType tp)
                         , "Value: " ++ (show $ LPP.ppValue val)
                         ]
  
  
  -- | Evaluate a GEP instruction to a constant value.
  evalConstGEP :: forall m wptr.
    (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
    GEPResult LLVMConst ->
    m (MemType, LLVMConst)
  evalConstGEP (GEPResult lanes finalMemType gep0) =
     do xs <- go gep0
        unless (fromIntegral (length xs) == natValue lanes)
               (throwError "Unexpected vector length in result of constant GEP")
        case xs of
          [x] -> return ( PtrType (MemType finalMemType), x)
          _   -> return ( VecType (fromIntegral (length xs)) (PtrType (MemType finalMemType))
                        , VectorConst (PtrType (MemType finalMemType)) xs
                        )
  
    where
    dl = llvmDataLayout ?lc
  
    asOffset :: MemType -> LLVMConst -> m Integer
    asOffset _ (ZeroConst (IntType _)) = return 0
    asOffset mt (IntConst _ x) =
      do let x' = BV.asUnsigned x * bytesToInteger (memTypeSize dl mt)
         unless (x' <= maxUnsigned ?ptrWidth)
                (throwError "Computed offset overflow in constant GEP")
         return x'
    asOffset ty val = throwError $ unlines $
      [ "Expected offset value in constant GEP"
      , "Type: " ++ show ty
      , "Offset: " ++ show val
      ]
  
    addOffset :: Integer -> LLVMConst -> m LLVMConst
    addOffset x (SymbolConst sym off) = return (SymbolConst sym (off+x))
    addOffset _ constant = throwError $ unlines $
      [ "Expected symbol constant in constant GEP"
      , "Constant: " ++ show constant
      ]
  
    -- Given a processed GEP instruction, compute the sequence of output
    -- pointer values that result from the instruction.  If the GEP is
    -- scalar-valued, then the result will be a list of one element.
    go :: GEP n LLVMConst -> m [LLVMConst]
  
    -- Scalar base, return a list containing just the base value.
    go (GEP_scalar_base base)
      = return [base]
  
    -- Vector base, deconstruct the input value and return the
    -- corresponding values.
    go (GEP_vector_base n x)
      = asVectorOf (natValue n) return x
  
    -- Scatter a scalar input across n lanes
    go (GEP_scatter n gep)
      = do ps <- go gep
           case ps of
             [p] -> return (replicate (widthVal n) p)
             _   -> throwError "vector length mismatch in GEP scatter"
  
    -- Add the offset corresponding to the given field across
    -- all the lanes of the GEP
    go (GEP_field fi gep)
      = do ps <- go gep
           let i = bytesToInteger (fiOffset fi)
           traverse (addOffset i) ps
  
    -- Compute the offset corresponding to the given array index
    -- and add that offest across all the lanes of the GEP
    go (GEP_index_each mt gep x)
      = do ps <- go gep
           i  <- asOffset mt x
           traverse (addOffset i) ps
  
    -- For each index in the input vector, compute and offset according
    -- to the given memory type and add the corresponding offset across
    -- each lane of the GEP componentwise.
    go (GEP_index_vector mt gep x)
      = do ps <- go gep
           is <- asVectorOf (fromIntegral (length ps)) (asOffset mt) x
           zipWithM addOffset is ps
  
  -- | Evaluate a floating point comparison.
  evalFcmp ::
    RealFloat a =>
    L.FCmpOp ->
    a -> a -> LLVMConst
  evalFcmp op x y = boolConst $ case op of
    L.Ffalse -> False
    L.Ftrue  -> True
    L.Foeq   -> ordered && x == y
    L.Fone   -> ordered && x /= y
    L.Fogt   -> ordered && x >  y
    L.Foge   -> ordered && x >= y
    L.Folt   -> ordered && x <  y
    L.Fole   -> ordered && x <= y
    L.Ford   -> ordered
    L.Fueq   -> unordered || x == y
    L.Fune   -> unordered || x /= y
    L.Fugt   -> unordered || x >  y
    L.Fuge   -> unordered || x >= y
    L.Fult   -> unordered || x <  y
    L.Fule   -> unordered || x <= y
    L.Funo   -> unordered
   where
   unordered = isNaN x || isNaN y
   ordered   = not unordered
  
  -- | Evaluate an integer comparison.
  evalIcmp ::
    (1 <= w) =>
    L.ICmpOp ->
    NatRepr w ->
    BV.BV w -> BV.BV w -> LLVMConst
  evalIcmp op w x y = boolConst $ case op of
    L.Ieq  -> x == y
    L.Ine  -> x /= y
    L.Iugt -> BV.ult y x
    L.Iuge -> BV.ule y x
    L.Iult -> BV.ult x y
    L.Iule -> BV.ule x y
    L.Isgt -> BV.slt w y x
    L.Isge -> BV.sle w y x
    L.Islt -> BV.slt w x y
    L.Isle -> BV.sle w x y
  
  -- | Evaluate a binary arithmetic operation.
  evalArith ::
    (MonadError String m, HasPtrWidth wptr) =>
    L.ArithOp ->
    MemType ->
    Arith -> Arith -> m LLVMConst
  evalArith op (IntType m) (ArithI x) (ArithI y)
    | Just (Some w) <- someNat m
    , Just LeqProof <- isPosNat w
    = evalIarith op w x y
  evalArith op FloatType (ArithF x) (ArithF y) = FloatConst <$> evalFarith op x y
  evalArith op DoubleType (ArithD x) (ArithD y) = DoubleConst <$> evalFarith op x y
  evalArith _ _ _ _ = throwError "binary arithmetic argument mismatch"
  
  -- | Evaluate a unary arithmetic operation.
  evalUnaryArith ::
    (MonadError String m, HasPtrWidth wptr) =>
    L.UnaryArithOp ->
    MemType ->
    Arith -> m LLVMConst
  evalUnaryArith op FloatType (ArithF x) = FloatConst <$> evalFunaryArith op x
  evalUnaryArith op DoubleType (ArithD x) = DoubleConst <$> evalFunaryArith op x
  evalUnaryArith _ _ _ = throwError "unary arithmetic argument mismatch"
  
  -- | Evaluate a binary floating-point operation.
  evalFarith ::
    (RealFrac a, MonadError String m) =>
    L.ArithOp ->
    a -> a -> m a
  evalFarith op x y =
    case op of
      L.FAdd -> return (x + y)
      L.FSub -> return (x - y)
      L.FMul -> return (x * y)
      L.FDiv -> return (x / y)
      L.FRem -> return (mod' x y)
      _ -> throwError "Encountered integer arithmetic operation applied to floating point arguments"
  
  -- | Evaluate a unary floating-point operation.
  evalFunaryArith ::
    (RealFrac a, MonadError String m) =>
    L.UnaryArithOp ->
    a -> m a
  evalFunaryArith op x =
    case op of
      L.FNeg -> return (negate x)
  
  -- | Evaluate an integer or pointer arithmetic operation.
  evalIarith ::
    (1 <= w, MonadError String m, HasPtrWidth wptr) =>
    L.ArithOp ->
    NatRepr w ->
    ArithInt -> ArithInt -> m LLVMConst
  evalIarith op w (ArithInt x) (ArithInt y)
    = IntConst w <$> evalIarith' op w (BV.mkBV w x) (BV.mkBV w y)
  evalIarith op w (ArithPtr sym x) (ArithInt y)
    | Just Refl <- testEquality w ?ptrWidth
    , L.Add _ _ <- op
    = return $ SymbolConst sym (x+y)
    | otherwise
    = throwError "Illegal operation applied to pointer argument"
  evalIarith op w (ArithInt x) (ArithPtr sym y)
    | Just Refl <- testEquality w ?ptrWidth
    , L.Add _ _ <- op
    = return $ SymbolConst sym (x+y)
    | otherwise
    = throwError "Illegal operation applied to pointer argument"
  evalIarith op w (ArithPtr symx x) (ArithPtr symy y)
    | Just Refl <- testEquality w ?ptrWidth
    , symx == symy
    , L.Sub _ _ <- op
    = return $ IntConst ?ptrWidth (BV.mkBV ?ptrWidth (x - y))
    | otherwise
    = throwError "Illegal operation applied to pointer argument"
  
  -- | Evaluate an integer (non-pointer) arithmetic operation.
  evalIarith' ::
    (1 <= w, MonadError String m) =>
    L.ArithOp ->
    NatRepr w ->
    BV.BV w -> BV.BV w -> m (BV.BV w)
  evalIarith' op w x y = do
    let nuwTest nuw zres =
          when (nuw && BV.ofUnsigned zres)
               (throwError "Unsigned overflow in constant arithmetic operation")
    let nswTest nsw zres =
          when (nsw && BV.ofSigned zres)
               (throwError "Signed overflow in constant arithmetic operation")
    case op of
      L.Add nuw nsw ->
        do let zres = BV.addOf w x y
           nuwTest nuw zres
           nswTest nsw zres
           return (BV.ofResult zres)
  
      L.Sub nuw nsw ->
        do let zres = BV.subOf w x y
           nuwTest nuw zres
           nswTest nsw zres
           return (BV.ofResult zres)
  
      L.Mul nuw nsw ->
        do let zres = BV.mulOf w x y
           nuwTest nuw zres
           nswTest nsw zres
           return (BV.ofResult zres)
  
      L.UDiv exact ->
        do when (y == BV.zero w)
                (throwError "Division by 0 in constant arithmetic operation")
           let (z,r) = BV.uquotRem x y
           when (exact && r /= BV.zero w)
                (throwError "Exact division failed in constant arithmetic operation")
           return z
  
      L.SDiv exact ->
        do when (y == BV.zero w)
                (throwError "Division by 0 in constant arithmetic operation")
           when (x == BV.minSigned w && y == BV.mkBV w (-1))
                (throwError "Signed division overflow in constant arithmetic operation")
           let (z,r) = BV.squotRem w x y
           when (exact && r /= BV.zero w )
                (throwError "Exact division failed in constant arithmetic operation")
           return z
      L.URem ->
        do when (y == BV.zero w)
                (throwError "Division by 0 in constant arithmetic operation")
           let r = BV.urem x y
           return r
  
      L.SRem ->
        do when (y == BV.zero w)
                (throwError "Division by 0 in constant arithmetic operation")
           when (x == BV.minSigned w && y == BV.mkBV w (-1))
                (throwError "Signed division overflow in constant arithmetic operation")
           let r = BV.srem w x y
           return r
  
      _ -> throwError "Floating point operation applied to integer arguments"
  
  -- BGS: Leave this alone for now, as we don't have a good way to
  -- detect overflow from bitvector operations.
  -- | Evaluate a bitwise operation on integer values.
  evalBitwise ::
    (1 <= w, MonadError String m) =>
    L.BitOp ->
    NatRepr w ->
    BV.BV w -> BV.BV w -> m LLVMConst
  evalBitwise op w x y = IntConst w <$>
    let yshf = fromInteger (BV.asUnsigned y) :: Natural
    in case op of
         L.And -> return (BV.and x y)
         L.Or  -> return (BV.or  x y)
         L.Xor -> return (BV.xor x y)
         L.Shl nuw nsw ->
           do let zres = BV.shlOf w x yshf
              when (nuw && BV.ofUnsigned zres)
                   (throwError "Unsigned overflow in left shift")
              when (nsw && BV.ofSigned zres)
                   (throwError "Signed overflow in left shift")
              return (BV.ofResult zres)
         L.Lshr exact ->
           do let z = BV.lshr w x yshf
              when (exact && x /= BV.shl w z yshf)
                   (throwError "Exact right shift failed")
              return z
         L.Ashr exact ->
           do let z = BV.ashr w x yshf
              when (exact && x /= BV.shl w z yshf)
                   (throwError "Exact right shift failed")
              return z
  
  -- | Evaluate a conversion operation on constants.
  evalConv ::
    (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
    L.ConstExpr ->
    L.ConvOp ->
    MemType ->
    LLVMConst ->
    m LLVMConst
  evalConv expr op mt x = case op of
      L.FpToUi
        | IntType n <- mt
        , Just (Some w) <- someNat n
        , Just LeqProof <- isPosNat w
        , FloatConst f <- x
        -> return $ IntConst w (BV.mkBV w (truncate f))
  
        | IntType n <- mt
        , Just (Some w) <- someNat n
        , Just LeqProof <- isPosNat w
        , DoubleConst d <- x
        -> return $ IntConst w (BV.mkBV w (truncate d))
  
      L.FpToSi
        | IntType n <- mt
        , Just (Some w) <- someNat n
        , Just LeqProof <- isPosNat w
        , FloatConst f <- x
        -> return $ IntConst w (BV.mkBV w (truncate f))
  
        | IntType n <- mt
        , Just (Some w) <- someNat n
        , Just LeqProof <- isPosNat w
        , DoubleConst d <- x
        -> return $ IntConst w (BV.mkBV w (truncate d))
  
      L.UiToFp
        | FloatType <- mt
        , IntConst _w i <- x
        -> return $ FloatConst (fromInteger (BV.asUnsigned i) :: Float)
  
        | DoubleType <- mt
        , IntConst _w i <- x
        -> return $ DoubleConst (fromInteger (BV.asUnsigned i) :: Double)
  
      L.SiToFp
        | FloatType <- mt
        , IntConst w i <- x
        -> return $ FloatConst (fromInteger (BV.asSigned w i) :: Float)
  
        | DoubleType <- mt
        , IntConst w i <- x
        -> return $ DoubleConst (fromInteger (BV.asSigned w i) :: Double)
  
      L.Trunc
        | IntType n <- mt
        , IntConst w i <- x
        , Just (Some w') <- someNat n
        , Just LeqProof <- isPosNat w'
        -> case testNatCases w' w of
            NatCaseLT LeqProof -> return $ IntConst w' (BV.trunc w' i)
            NatCaseEQ -> return x
            NatCaseGT LeqProof ->
              throwError $ "Attempted to truncate " <> show w <> " bits to " <> show w'
  
      L.ZExt
        | IntType n <- mt
        , IntConst w i <- x
        , Just (Some w') <- someNat n
        , Just LeqProof <- isPosNat w'
        -> case testNatCases w w' of
            NatCaseLT LeqProof -> return $ IntConst w' (BV.zext w' i)
            NatCaseEQ -> return x
            NatCaseGT LeqProof ->
              throwError $ "Attempted to zext " <> show w <> " bits to " <> show w'
  
      L.SExt
        | IntType n <- mt
        , IntConst w i <- x
        , Just (Some w') <- someNat n
        , Just LeqProof <- isPosNat w'
        -> case testNatCases w w' of
            NatCaseLT LeqProof -> return $ IntConst w' (BV.sext w w' i)
            NatCaseEQ -> return x
            NatCaseGT LeqProof ->
              throwError $ "Attempted to sext " <> show w <> " bits to " <> show w'
  
      L.FpTrunc
        | DoubleType <- mt
        , DoubleConst d <- x
        -> return $ DoubleConst d
  
        | FloatType <- mt
        , DoubleConst d <- x
        -> return $ FloatConst (realToFrac d)
  
        | FloatType <- mt
        , FloatConst f <- x
        -> return $ FloatConst f
  
      L.FpExt
        | DoubleType <- mt
        , DoubleConst d <- x
        -> return $ DoubleConst d
  
        | DoubleType <- mt
        , FloatConst f <- x
        -> return $ DoubleConst (realToFrac f)
  
        | FloatType <- mt
        , FloatConst f <- x
        -> return $ FloatConst f
  
      L.IntToPtr -> return x
      L.PtrToInt -> return x
  
      _ -> badExp "unexpected conversion operation"
  
   where badExp msg = throwError $ unlines [msg, show expr]
  
  
  castToInt ::
    MonadError String m =>
    L.ConstExpr {- ^ original expression to evaluate -} ->
    EndianForm ->
    Natural ->
    MemType ->
    LLVMConst ->
    m Integer
  castToInt _expr _endian _w (IntType w) x = asInt w x
  castToInt expr endian w (VecType n tp) x
    | (m,0) <- w `divMod` n =
    do xs <- asVectorOf n (castToInt expr endian m tp) x
       let indices = case endian of
                       LittleEndian -> [0 .. n-1]
                       BigEndian -> reverse [0 .. n-1]
       let pieces = [ v `shiftL` (fromIntegral (i * m))
                    | i <- indices
                    | v <- xs
                    ]
       return (foldr (.|.) 0 pieces)
  
  castToInt expr _ _ _ _ =
    throwError $ unlines ["Cannot cast expression to integer type", show expr]
  
  castFromInt ::
    MonadError String m =>
    EndianForm ->
    Integer ->
    Natural ->
    MemType ->
    m LLVMConst
  castFromInt _ xint w (IntType w')
    | w == w'
    , Some wsz <- mkNatRepr w
    , Just LeqProof <- isPosNat wsz
    = return $ IntConst wsz (BV.mkBV wsz xint)
  
  castFromInt endian xint w (VecType n tp)
    | (m,0) <- w `divMod` n =
    do let mask = (1 `shiftL` fromIntegral m) - 1
       let indices = case endian of
                       LittleEndian -> [0 .. n-1]
                       BigEndian -> reverse [0 .. n-1]
       let pieces = [ mask .&. (xint `shiftR` fromIntegral (i * m))
                    | i <- indices
                    ]
       VectorConst tp <$> mapM (\x -> castFromInt endian x m tp) pieces
  
  castFromInt _ _ _ tp =
    throwError $ unlines ["Cant cast integer to type", show tp]
  
  -- | Evaluate a bitcast
  evalBitCast ::
    (?lc :: TypeContext, MonadError String m) =>
    L.ConstExpr {- ^ original expression to evaluate -} ->
    MemType     {- ^ input expressio type -} ->
    LLVMConst   {- ^ input expression -} ->
    MemType     {- ^ desired output type -} ->
    m LLVMConst
  
  -- cast zero constants to relabeled zero constants
  evalBitCast _ _ (ZeroConst _) tgtT = return (ZeroConst tgtT)
  
  -- pointer casts always succeed
  evalBitCast _ (PtrType _) expr (PtrType _) = return expr
  evalBitCast _ (PtrType _) expr PtrOpaqueType = return expr
  evalBitCast _ PtrOpaqueType expr (PtrType _) = return expr
  evalBitCast _ PtrOpaqueType expr PtrOpaqueType = return expr
  
  -- casts between vectors of the same length can just be done pointwise
  evalBitCast expr (VecType n srcT) (VectorConst _ xs) (VecType n' tgtT)
    | n == n' = VectorConst tgtT <$> traverse (\x -> evalBitCast expr srcT x tgtT) xs
  
  -- otherwise, cast via an intermediate integer type
  evalBitCast expr xty x toty
    | Just w1 <- memTypeBitwidth xty
    , Just w2 <- memTypeBitwidth toty
    , w1 == w2
    = do let endian = ?lc ^. to llvmDataLayout.intLayout
         xint <- castToInt expr endian w1 xty x
         castFromInt endian xint w1 toty
  
  evalBitCast expr _ _ _ =
     throwError $ unlines ["illegal constant bitcast", show expr]
  
  
  asVectorOf ::
    MonadError String m =>
    Natural ->
    (LLVMConst -> m a) ->
    (LLVMConst -> m [a])
  asVectorOf n f (ZeroConst (VecType m mt))
    | n == m
    = do x <- f (ZeroConst mt)
         return (replicate (fromIntegral n) x)
  
  asVectorOf n f (VectorConst _ xs)
    | n == fromIntegral (length xs)
    = traverse f xs
  
  asVectorOf n _ _
    = throwError ("Expected vector constant value of length: " ++ show n)
  
  -- | Type representing integer-like things.  These are either actual
  --   integer constants, or constant offsets from global symbols.
  data ArithInt where
    ArithInt :: Integer -> ArithInt
    ArithPtr :: L.Symbol -> Integer -> ArithInt
  
  -- | A constant value to which arithmetic operation can be applied.
  --   These are integers, pointers, floats and doubles.
  data Arith where
    ArithI :: ArithInt -> Arith
    ArithF :: Float -> Arith
    ArithD :: Double -> Arith
  
  asArithInt ::
    (MonadError String m, HasPtrWidth wptr) =>
    Natural   {- ^ expected integer width -} ->
    LLVMConst {- ^ constant value -} ->
    m ArithInt
  asArithInt n (ZeroConst (IntType m))
    | n == m
    = return (ArithInt 0)
  asArithInt n (IntConst w x)
    | n == natValue w
    = return (ArithInt (BV.asUnsigned x))
  asArithInt n (SymbolConst sym off)
    | n == natValue ?ptrWidth
    = return (ArithPtr sym off)
  asArithInt _ _
    = throwError "Expected integer value"
  
  asArith ::
    (MonadError String m, HasPtrWidth wptr) =>
    MemType   {- ^ expected type -} ->
    LLVMConst {- ^ constant value -} ->
    m Arith
  asArith (IntType n) x = ArithI <$> asArithInt n x
  asArith FloatType x   = ArithF <$> asFloat x
  asArith DoubleType x  = ArithD <$> asDouble x
  asArith _ _ = throwError "Expected arithmetic type"
  
  asInt ::
    MonadError String m =>
    Natural   {- ^ expected integer width -} ->
    LLVMConst {- ^ constant value -} ->
    m Integer
  asInt n (ZeroConst (IntType m))
    | n == m
    = return 0
  asInt n (IntConst w x)
    | n == natValue w
    = return (BV.asUnsigned x)
  asInt n _
    = throwError ("Expected integer constant of size " ++ show n)
  
  asBV ::
    MonadError String m =>
    NatRepr w {- ^ expected integer width -} ->
    LLVMConst {- ^ constant value -} ->
    m (BV.BV w)
  asBV w (ZeroConst (IntType m))
    | natValue w == m
    = return (BV.zero w)
  asBV w (IntConst w' x)
    | Just Refl <- w `testEquality` w'
    = return x
  asBV w _
    = throwError ("Expected integer constant of size " ++ show w)
  
  asFloat ::
    MonadError String m =>
    LLVMConst {- ^ constant value -} ->
    m Float
  asFloat (ZeroConst FloatType) = return 0
  asFloat (FloatConst x) = return x
  asFloat _ = throwError "Expected floating point constant"
  
  asDouble ::
    MonadError String m =>
    LLVMConst {- ^ constant value -} ->
    m Double
  asDouble (ZeroConst DoubleType) = return 0
  asDouble (DoubleConst x) = return x
  asDouble _ = throwError "Expected double constant"
  
  
  -- | Compute the value of a constant expression.  Fails if
  --   the expression does not actually represent a constant value.
  transConstantExpr :: forall m wptr.
    (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
    L.ConstExpr ->
    m LLVMConst
  transConstantExpr expr = case expr of
    L.ConstGEP inbounds _inrange baseTy base exps -> -- TODO? pay attention to the inrange flag
      do gep <- translateGEP inbounds baseTy base exps
         gep' <- traverse transConstant gep
         snd <$> evalConstGEP gep'
  
    L.ConstSelect b x y ->
      do b' <- transConstant b
         x' <- transConstant x
         y' <- transConstant y
         case b' of
           IntConst w v
             | v /= BV.zero w -> return x'
             | otherwise      -> return y'
           _ -> badExp "Expected boolean value in constant select"
  
    L.ConstBlockAddr _ _ ->
      badExp "constant block addresses not supported"
  
    L.ConstFCmp op a b ->
      do mt <- liftMemType (L.typedType a)
         case mt of
           VecType n FloatType ->
             do a' <- asVectorOf n asFloat =<< transConstant a
                b' <- asVectorOf n asFloat =<< transConstant b
                return $ VectorConst (IntType 1) $ zipWith (evalFcmp op) a' b'
           VecType n DoubleType ->
             do a' <- asVectorOf n asDouble =<< transConstant a
                b' <- asVectorOf n asDouble =<< transConstant b
                return $ VectorConst (IntType 1) $ zipWith (evalFcmp op) a' b'
           FloatType ->
             do a' <- asFloat =<< transConstant a
                b' <- asFloat =<< transConstant b
                return $ evalFcmp op a' b'
           DoubleType ->
             do a' <- asDouble =<< transConstant a
                b' <- asDouble =<< transConstant b
                return $ evalFcmp op a' b'
           _ -> badExp "Expected floating point arguments"
  
    L.ConstICmp op a b ->
      do mt <- liftMemType (L.typedType a)
         case mt of
           VecType n (IntType m)
             | Some w <- mkNatRepr m
             , Just LeqProof <- isPosNat w
             -> do a' <- asVectorOf n (asBV w) =<< transConstant a
                   b' <- asVectorOf n (asBV w) =<< transConstant b
                   return $ VectorConst (IntType 1) $ zipWith (evalIcmp op w) a' b'
           IntType m
             | Some w <- mkNatRepr m
             , Just LeqProof <- isPosNat w
             -> do a' <- asBV w =<< transConstant a
                   b' <- asBV w =<< transConstant b
                   return $ evalIcmp op w a' b'
           _ -> badExp "Expected integer arguments"
  
    L.ConstArith op (L.Typed tp a) b ->
      do mt <- liftMemType tp
         case mt of
            VecType n tp' ->
              do a' <- asVectorOf n (asArith tp') =<< transConstant' mt a
                 b' <- asVectorOf n (asArith tp') =<< transConstant' mt b
                 VectorConst tp' <$> zipWithM (evalArith op tp') a' b'
            tp' ->
              do a' <- asArith tp' =<< transConstant' mt a
                 b' <- asArith tp' =<< transConstant' mt b
                 evalArith op tp' a' b'
  
    L.ConstUnaryArith op (L.Typed tp a) ->
      do mt <- liftMemType tp
         case mt of
            VecType n tp' ->
              do a' <- asVectorOf n (asArith tp') =<< transConstant' mt a
                 VectorConst tp' <$> traverse (evalUnaryArith op tp') a'
            tp' ->
              do a' <- asArith tp' =<< transConstant' mt a
                 evalUnaryArith op tp' a'
  
    L.ConstBit op (L.Typed tp a) b ->
      do mt <- liftMemType tp
         case mt of
           VecType n (IntType m)
             | Some w <- mkNatRepr m
             , Just LeqProof <- isPosNat w
             -> do a' <- asVectorOf n (asBV w) =<< transConstant' mt a
                   b' <- asVectorOf n (asBV w) =<< transConstant' mt b
                   VectorConst (IntType m) <$> zipWithM (evalBitwise op w) a' b'
           IntType m
             | Some w <- mkNatRepr m
             , Just LeqProof <- isPosNat w
             -> do a' <- asBV w =<< transConstant' mt a
                   b' <- asBV w =<< transConstant' mt b
                   evalBitwise op w a' b'
           _ -> badExp "Expected integer arguments"
  
    L.ConstConv L.BitCast (L.Typed tp x) outty ->
     do toty <- liftMemType outty
        xty  <- liftMemType tp
        x' <- transConstant' xty x
        evalBitCast expr xty x' toty
  
    L.ConstConv op x outty ->
      do mt <- liftMemType outty
         x' <- transConstant x
         case mt of
           VecType n mt' ->
             do xs <- asVectorOf n return x'
                VectorConst mt' <$> traverse (evalConv expr op mt') xs
  
           _ -> evalConv expr op mt x'
  
   where
   badExp :: String -> m a
   badExp msg = throwError $ unlines [msg, show expr]
  
  testBreakpointFunction :: String -> Bool
  testBreakpointFunction = isPrefixOf "__breakpoint__"
  