-----------------------------------------------------------------------
-- |
-- 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 :: Instr -> [Char]
showInstr Instr
i = Doc -> [Char]
forall a. Show a => a -> [Char]
show (((?config::Config) => Doc) -> Doc
forall a. ((?config::Config) => a) -> a
L.ppLLVM38 (Fmt Instr
Instr -> Doc
L.ppInstr Instr
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 :: forall a b. (a -> b) -> GEP n a -> GEP n b
fmap = (a -> b) -> GEP n a -> GEP n b
forall (t :: Type -> Type) a b.
Traversable t =>
(a -> b) -> t a -> t b
fmapDefault
instance Foldable (GEP n) where
  foldMap :: forall m a. Monoid m => (a -> m) -> GEP n a -> m
foldMap = (a -> m) -> GEP n a -> m
forall (t :: Type -> Type) m a.
(Traversable t, Monoid m) =>
(a -> m) -> t a -> m
foldMapDefault

instance Traversable (GEP n) where
  traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEP n a -> f (GEP n b)
traverse a -> f b
f GEP n a
gep = case GEP n a
gep of
    GEP_scalar_base a
x            -> b -> GEP n b
b -> GEP 1 b
forall expr. expr -> GEP 1 expr
GEP_scalar_base (b -> GEP n b) -> f b -> f (GEP n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
    GEP_vector_base NatRepr n
n a
x          -> NatRepr n -> b -> GEP n b
forall (n :: Natural) expr. NatRepr n -> expr -> GEP n expr
GEP_vector_base NatRepr n
n (b -> GEP n b) -> f b -> f (GEP n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
    GEP_scatter NatRepr n
n GEP 1 a
gep'           -> NatRepr n -> GEP 1 b -> GEP n b
forall (n :: Natural) expr. NatRepr n -> GEP 1 expr -> GEP n expr
GEP_scatter NatRepr n
n (GEP 1 b -> GEP n b) -> f (GEP 1 b) -> f (GEP n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> GEP 1 a -> f (GEP 1 b)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEP 1 a -> f (GEP 1 b)
traverse a -> f b
f GEP 1 a
gep'
    GEP_field FieldInfo
fi GEP n a
gep'            -> FieldInfo -> GEP n b -> GEP n b
forall (n :: Natural) expr. FieldInfo -> GEP n expr -> GEP n expr
GEP_field FieldInfo
fi (GEP n b -> GEP n b) -> f (GEP n b) -> f (GEP n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> GEP n a -> f (GEP n b)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEP n a -> f (GEP n b)
traverse a -> f b
f GEP n a
gep'
    GEP_index_each MemType
mt GEP n a
gep' a
idx   -> MemType -> GEP n b -> b -> GEP n b
forall (n :: Natural) expr.
MemType -> GEP n expr -> expr -> GEP n expr
GEP_index_each MemType
mt (GEP n b -> b -> GEP n b) -> f (GEP n b) -> f (b -> GEP n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> GEP n a -> f (GEP n b)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEP n a -> f (GEP n b)
traverse a -> f b
f GEP n a
gep' f (b -> GEP n b) -> f b -> f (GEP n b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> a -> f b
f a
idx
    GEP_index_vector MemType
mt GEP n a
gep' a
idx -> MemType -> GEP n b -> b -> GEP n b
forall (n :: Natural) expr.
MemType -> GEP n expr -> expr -> GEP n expr
GEP_index_vector MemType
mt (GEP n b -> b -> GEP n b) -> f (GEP n b) -> f (b -> GEP n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> GEP n a -> f (GEP n b)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEP n a -> f (GEP n b)
traverse a -> f b
f GEP n a
gep' f (b -> GEP n b) -> f b -> f (GEP n b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> a -> f b
f a
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 :: forall a b. (a -> b) -> GEPResult a -> GEPResult b
fmap = (a -> b) -> GEPResult a -> GEPResult b
forall (t :: Type -> Type) a b.
Traversable t =>
(a -> b) -> t a -> t b
fmapDefault
instance Foldable GEPResult where
  foldMap :: forall m a. Monoid m => (a -> m) -> GEPResult a -> m
foldMap = (a -> m) -> GEPResult a -> m
forall (t :: Type -> Type) m a.
(Traversable t, Monoid m) =>
(a -> m) -> t a -> m
foldMapDefault

instance Traversable GEPResult where
  traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEPResult a -> f (GEPResult b)
traverse a -> f b
f (GEPResult NatRepr n
n MemType
mt GEP n a
gep) = NatRepr n -> MemType -> GEP n b -> GEPResult b
forall (w :: Natural) expr.
(1 <= w) =>
NatRepr w -> MemType -> GEP w expr -> GEPResult expr
GEPResult NatRepr n
n MemType
mt (GEP n b -> GEPResult b) -> f (GEP n b) -> f (GEPResult b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> GEP n a -> f (GEP n b)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEP n a -> f (GEP n b)
traverse a -> f b
f GEP n a
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 :: forall (wptr :: Natural) (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Bool
-> Type
-> Typed Value
-> [Typed Value]
-> m (GEPResult (Typed Value))
translateGEP Bool
_ Type
_ Typed Value
_ [] =
  [Char] -> m (GEPResult (Typed Value))
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"getelementpointer must have at least one index"

translateGEP Bool
inbounds Type
baseTy Typed Value
basePtr [Typed Value]
elts =
  do MemType
baseMemType <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
baseTy
     MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType (Typed Value -> Type
forall a. Typed a -> Type
L.typedType Typed Value
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 MemType
mt of
       -- Vector base case, with as many lanes as there are input pointers
       VecType Natural
n MemType
vmt
         | MemType -> Bool
isPointerMemType MemType
vmt
         , Some NatRepr x
lanes <- Natural -> Some NatRepr
mkNatRepr Natural
n
         , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
lanes
         ->  let mt' :: MemType
mt' = Natural -> MemType -> MemType
ArrayType Natural
0 MemType
baseMemType in
             NatRepr x
-> MemType
-> GEP x (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
go NatRepr x
lanes MemType
mt' (NatRepr x -> Typed Value -> GEP x (Typed Value)
forall (n :: Natural) expr. NatRepr n -> expr -> GEP n expr
GEP_vector_base NatRepr x
lanes Typed Value
basePtr) [Typed Value]
elts

       -- Scalar base case with exactly 1 lane
       MemType
_ | MemType -> Bool
isPointerMemType MemType
mt
         ->  let mt' :: MemType
mt' = Natural -> MemType -> MemType
ArrayType Natural
0 MemType
baseMemType in
             NatRepr 1
-> MemType
-> GEP 1 (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
go (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) MemType
mt' (Typed Value -> GEP 1 (Typed Value)
forall expr. expr -> GEP 1 expr
GEP_scalar_base Typed Value
basePtr) [Typed Value]
elts

         | Bool
otherwise
         -> m (GEPResult (Typed Value))
forall a. m a
badGEP
 where
 badGEP :: m a
 badGEP :: forall a. m a
badGEP = [Char] -> m a
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m a) -> [Char] -> m a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Invalid GEP", Instr -> [Char]
showInstr (Bool -> Type -> Typed Value -> [Typed Value] -> Instr
forall lab.
Bool
-> Type -> Typed (Value' lab) -> [Typed (Value' lab)] -> Instr' lab
L.GEP Bool
inbounds Type
baseTy Typed Value
basePtr [Typed Value]
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 :: forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
go NatRepr lanes
lanes MemType
mt GEP lanes (Typed Value)
gep [] = GEPResult (Typed Value) -> m (GEPResult (Typed Value))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr lanes
-> MemType -> GEP lanes (Typed Value) -> GEPResult (Typed Value)
forall (w :: Natural) expr.
(1 <= w) =>
NatRepr w -> MemType -> GEP w expr -> GEPResult expr
GEPResult NatRepr lanes
lanes MemType
mt GEP lanes (Typed Value)
gep)

 -- Resolve one offset value and recurse
 go NatRepr lanes
lanes MemType
mt GEP lanes (Typed Value)
gep (Typed Value
off:[Typed Value]
xs) =
   do MemType
offt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType (Typed Value -> Type
forall a. Typed a -> Type
L.typedType Typed Value
off)
      -- The meaning of the offset depends on the static type of the intermediate result
      case MemType
mt of
        ArrayType Natural
_ MemType
mt' -> NatRepr lanes
-> Typed Value
-> MemType
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> Typed Value
-> MemType
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
goArray NatRepr lanes
lanes Typed Value
off MemType
offt MemType
mt' GEP lanes (Typed Value)
gep [Typed Value]
xs
        VecType   Natural
_ MemType
mt' -> NatRepr lanes
-> Typed Value
-> MemType
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> Typed Value
-> MemType
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
goArray NatRepr lanes
lanes Typed Value
off MemType
offt MemType
mt' GEP lanes (Typed Value)
gep [Typed Value]
xs
        StructType StructInfo
si   -> NatRepr lanes
-> Typed Value
-> MemType
-> StructInfo
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> Typed Value
-> MemType
-> StructInfo
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
goStruct NatRepr lanes
lanes Typed Value
off MemType
offt StructInfo
si GEP lanes (Typed Value)
gep [Typed Value]
xs
        MemType
_ -> m (GEPResult (Typed Value))
forall a. m a
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 :: forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> Typed Value
-> MemType
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
goArray NatRepr lanes
lanes Typed Value
off MemType
offt MemType
mt' GEP lanes (Typed Value)
gep [Typed Value]
xs =
    case MemType
offt of
      -- Single array index, apply pointwise to all intermediate pointers
      IntType Natural
_
        -> NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
go NatRepr lanes
lanes MemType
mt' (MemType
-> GEP lanes (Typed Value)
-> Typed Value
-> GEP lanes (Typed Value)
forall (n :: Natural) expr.
MemType -> GEP n expr -> expr -> GEP n expr
GEP_index_each MemType
mt' GEP lanes (Typed Value)
gep Typed Value
off) [Typed Value]
xs

      -- Vector of indices, matching the current number of lanes, apply
      -- each offset to the corresponding base pointer
      VecType Natural
n (IntType Natural
_)
        | NatRepr lanes -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr lanes
lanes Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n
        -> NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
go NatRepr lanes
lanes MemType
mt' (MemType
-> GEP lanes (Typed Value)
-> Typed Value
-> GEP lanes (Typed Value)
forall (n :: Natural) expr.
MemType -> GEP n expr -> expr -> GEP n expr
GEP_index_vector MemType
mt' GEP lanes (Typed Value)
gep Typed Value
off) [Typed Value]
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 Natural
n (IntType Natural
_)
        | Some NatRepr x
n' <- Natural -> Some NatRepr
mkNatRepr Natural
n
        , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
n'
        , Just lanes :~: 1
Refl <- NatRepr lanes -> NatRepr 1 -> Maybe (lanes :~: 1)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr lanes
lanes (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)
        -> NatRepr x
-> MemType
-> GEP x (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
go NatRepr x
n' MemType
mt' (MemType
-> GEP x (Typed Value) -> Typed Value -> GEP x (Typed Value)
forall (n :: Natural) expr.
MemType -> GEP n expr -> expr -> GEP n expr
GEP_index_vector MemType
mt' (NatRepr x -> GEP 1 (Typed Value) -> GEP x (Typed Value)
forall (n :: Natural) expr. NatRepr n -> GEP 1 expr -> GEP n expr
GEP_scatter NatRepr x
n' GEP lanes (Typed Value)
GEP 1 (Typed Value)
gep) Typed Value
off) [Typed Value]
xs

      -- Otherwise, some sort of mismatch occured.
      MemType
_ -> m (GEPResult (Typed Value))
forall a. m a
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 :: forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> Typed Value
-> MemType
-> StructInfo
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
goStruct NatRepr lanes
lanes Typed Value
off MemType
offt StructInfo
si GEP lanes (Typed Value)
gep [Typed Value]
xs =
    do LLVMConst
off' <- MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
offt (Typed Value -> Value
forall a. Typed a -> a
L.typedValue Typed Value
off)
       case LLVMConst
off' of
         -- Special case for the zero value
         ZeroConst (IntType Natural
_) -> Integer -> m (GEPResult (Typed Value))
goidx Integer
0

         -- Single index; compute the corresponding field.
         IntConst NatRepr w
_ BV w
idx -> Integer -> m (GEPResult (Typed Value))
goidx (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
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 Natural
_) (i :: LLVMConst
i@(IntConst NatRepr w
_ BV w
idx) : [LLVMConst]
is) | (LLVMConst -> Bool) -> [LLVMConst] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (LLVMConst -> LLVMConst -> Bool
same LLVMConst
i) [LLVMConst]
is -> Integer -> m (GEPResult (Typed Value))
goidx (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
idx)
           where
           same :: LLVMConst -> LLVMConst -> Bool
           same :: LLVMConst -> LLVMConst -> Bool
same (IntConst NatRepr w
wx BV w
x) (IntConst NatRepr w
wy BV w
y)
             | Just w :~: w
Refl <- NatRepr w -> NatRepr w -> Maybe (w :~: w)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
wx NatRepr w
wy = BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
BV w
y
           same LLVMConst
_ LLVMConst
_ = Bool
False

         -- Otherwise, invalid GEP instruction
         LLVMConst
_ -> m (GEPResult (Typed Value))
forall a. m a
badGEP

            -- using the information from the struct type, figure out which
            -- field is indicated
      where goidx :: Integer -> m (GEPResult (Typed Value))
goidx Integer
idx | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Vector FieldInfo -> Int
forall a. Vector a -> Int
V.length Vector FieldInfo
flds) =
                 NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (lanes :: Natural).
(1 <= lanes) =>
NatRepr lanes
-> MemType
-> GEP lanes (Typed Value)
-> [Typed Value]
-> m (GEPResult (Typed Value))
go NatRepr lanes
lanes (FieldInfo -> MemType
fiType FieldInfo
fi) (FieldInfo -> GEP lanes (Typed Value) -> GEP lanes (Typed Value)
forall (n :: Natural) expr. FieldInfo -> GEP n expr -> GEP n expr
GEP_field FieldInfo
fi GEP lanes (Typed Value)
gep) [Typed Value]
xs
               where flds :: Vector FieldInfo
flds = StructInfo -> Vector FieldInfo
siFields StructInfo
si
                     fi :: FieldInfo
fi   = Vector FieldInfo
flds Vector FieldInfo -> Int -> FieldInfo
forall a. Vector a -> Int -> a
V.! (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
idx)

            goidx Integer
_ = m (GEPResult (Typed Value))
forall a. m a
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 :: LLVMConst -> [Char]
show LLVMConst
lc = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
    case LLVMConst
lc of
      (ZeroConst MemType
mem)     -> [[Char]
"ZeroConst", MemType -> [Char]
forall a. Show a => a -> [Char]
show MemType
mem]
      (IntConst NatRepr w
w BV w
x)      -> [[Char]
"IntConst", NatRepr w -> [Char]
forall a. Show a => a -> [Char]
show NatRepr w
w, BV w -> [Char]
forall a. Show a => a -> [Char]
show BV w
x]
      (FloatConst Float
f)      -> [[Char]
"FloatConst", Float -> [Char]
forall a. Show a => a -> [Char]
show Float
f]
      (DoubleConst Double
d)     -> [[Char]
"DoubleConst", Double -> [Char]
forall a. Show a => a -> [Char]
show Double
d]
      ld :: LLVMConst
ld@(LongDoubleConst FP80Value
_)-> [[Char]
"LongDoubleConst", LLVMConst -> [Char]
forall a. Show a => a -> [Char]
show LLVMConst
ld]
      (ArrayConst MemType
mem [LLVMConst]
a)  -> [[Char]
"ArrayConst", MemType -> [Char]
forall a. Show a => a -> [Char]
show MemType
mem, [LLVMConst] -> [Char]
forall a. Show a => a -> [Char]
show [LLVMConst]
a]
      (VectorConst MemType
mem [LLVMConst]
v) -> [[Char]
"VectorConst", MemType -> [Char]
forall a. Show a => a -> [Char]
show MemType
mem, [LLVMConst] -> [Char]
forall a. Show a => a -> [Char]
show [LLVMConst]
v]
      (StructConst StructInfo
si [LLVMConst]
a)  -> [[Char]
"StructConst", StructInfo -> [Char]
forall a. Show a => a -> [Char]
show StructInfo
si, [LLVMConst] -> [Char]
forall a. Show a => a -> [Char]
show [LLVMConst]
a]
      (SymbolConst Symbol
s Integer
x)   -> [[Char]
"SymbolConst", Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
s, Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
x]
      (UndefConst MemType
mem)    -> [[Char]
"UndefConst", MemType -> [Char]
forall a. Show a => a -> [Char]
show MemType
mem]
      (StringConst ByteString
bs)    -> [[Char]
"StringConst", ByteString -> [Char]
forall a. Show a => a -> [Char]
show ByteString
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 MemType
mem1)      == :: LLVMConst -> LLVMConst -> Bool
== (ZeroConst MemType
mem2)      = MemType
mem1 MemType -> MemType -> Bool
forall a. Eq a => a -> a -> Bool
== MemType
mem2
  (IntConst NatRepr w
w1 BV w
x1)      == (IntConst NatRepr w
w2 BV w
x2)      =
    case NatRepr w -> NatRepr w -> Either (w :~: w) ((w :~: w) -> Void)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
DecidableEq f =>
f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)
decEq NatRepr w
w1 NatRepr w
w2 of
      Left w :~: w
Refl -> BV w
x1 BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
BV w
x2
      Right (w :~: w) -> Void
_   -> Bool
False
  (FloatConst Float
f1)       == (FloatConst Float
f2)       = Float
f1 Float -> Float -> Bool
forall a. Eq a => a -> a -> Bool
== Float
f2
  (DoubleConst Double
d1)      == (DoubleConst Double
d2)      = Double
d1 Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
d2
  (LongDoubleConst FP80Value
ld1) == (LongDoubleConst FP80Value
ld2) = FP80Value
ld1 FP80Value -> FP80Value -> Bool
forall a. Eq a => a -> a -> Bool
== FP80Value
ld2
  (ArrayConst MemType
mem1 [LLVMConst]
a1)  == (ArrayConst MemType
mem2 [LLVMConst]
a2)  = MemType
mem1 MemType -> MemType -> Bool
forall a. Eq a => a -> a -> Bool
== MemType
mem2 Bool -> Bool -> Bool
&& [LLVMConst]
a1 [LLVMConst] -> [LLVMConst] -> Bool
forall a. Eq a => a -> a -> Bool
== [LLVMConst]
a2
  (VectorConst MemType
mem1 [LLVMConst]
v1) == (VectorConst MemType
mem2 [LLVMConst]
v2) = MemType
mem1 MemType -> MemType -> Bool
forall a. Eq a => a -> a -> Bool
== MemType
mem2 Bool -> Bool -> Bool
&& [LLVMConst]
v1 [LLVMConst] -> [LLVMConst] -> Bool
forall a. Eq a => a -> a -> Bool
== [LLVMConst]
v2
  (StructConst StructInfo
si1 [LLVMConst]
a1)  == (StructConst StructInfo
si2 [LLVMConst]
a2)  = StructInfo
si1 StructInfo -> StructInfo -> Bool
forall a. Eq a => a -> a -> Bool
== StructInfo
si2   Bool -> Bool -> Bool
&& [LLVMConst]
a1 [LLVMConst] -> [LLVMConst] -> Bool
forall a. Eq a => a -> a -> Bool
== [LLVMConst]
a2
  (SymbolConst Symbol
s1 Integer
x1)   == (SymbolConst Symbol
s2 Integer
x2)   = Symbol
s1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s2     Bool -> Bool -> Bool
&& Integer
x1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
x2
  (UndefConst  MemType
_)       == (UndefConst MemType
_)        = Bool
False
  LLVMConst
_                     == LLVMConst
_                     = Bool
False

-- | Create an LLVM constant value from a boolean.
boolConst :: Bool -> LLVMConst
boolConst :: Bool -> LLVMConst
boolConst Bool
False = NatRepr 1 -> BV 1 -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) (NatRepr 1 -> BV 1
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
boolConst Bool
True = NatRepr 1 -> BV 1 -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) (NatRepr 1 -> BV 1
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
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 :: forall (m :: Type -> Type).
MonadError [Char] m =>
Natural -> Integer -> m LLVMConst
intConst Natural
n Integer
0
  = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> LLVMConst
ZeroConst (Natural -> MemType
IntType Natural
n))
intConst Natural
n Integer
x
  | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr Natural
n
  , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
  = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w (NatRepr x -> Integer -> BV x
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w Integer
x))
intConst Natural
n Integer
_
  = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char]
"Invalid integer width: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
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 :: forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m (MemType, LLVMConst)
transConstantWithType (L.Typed Type
tp Value
v) =
  do MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
tp
     LLVMConst
c <- MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
v
     (MemType, LLVMConst) -> m (MemType, LLVMConst)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType
mt, LLVMConst
c)

transConstant ::
  (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
  L.Typed L.Value ->
  m LLVMConst
transConstant :: forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
x = (MemType, LLVMConst) -> LLVMConst
forall a b. (a, b) -> b
snd ((MemType, LLVMConst) -> LLVMConst)
-> m (MemType, LLVMConst) -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Typed Value -> m (MemType, LLVMConst)
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m (MemType, LLVMConst)
transConstantWithType Typed Value
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' :: forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
tp (Value
L.ValUndef) =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> LLVMConst
UndefConst MemType
tp)
transConstant' (IntType Natural
n) (L.ValInteger Integer
x) =
  Natural -> Integer -> m LLVMConst
forall (m :: Type -> Type).
MonadError [Char] m =>
Natural -> Integer -> m LLVMConst
intConst Natural
n Integer
x
transConstant' (IntType Natural
1) (L.ValBool Bool
b) =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst)
-> (BV 1 -> LLVMConst) -> BV 1 -> m LLVMConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr 1 -> BV 1 -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) (BV 1 -> m LLVMConst) -> BV 1 -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ if Bool
b
                                    then (NatRepr 1 -> BV 1
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
                                    else (NatRepr 1 -> BV 1
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
transConstant' MemType
FloatType (L.ValFloat Float
f) =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Float -> LLVMConst
FloatConst Float
f)
transConstant' MemType
DoubleType (L.ValDouble Double
d) =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Double -> LLVMConst
DoubleConst Double
d)
transConstant' MemType
X86_FP80Type (L.ValFP80 FP80Value
ld) =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FP80Value -> LLVMConst
LongDoubleConst FP80Value
ld)
transConstant' (PtrType SymType
_) (L.ValSymbol Symbol
s) =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Symbol -> Integer -> LLVMConst
SymbolConst Symbol
s Integer
0)
transConstant' MemType
PtrOpaqueType (L.ValSymbol Symbol
s) =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Symbol -> Integer -> LLVMConst
SymbolConst Symbol
s Integer
0)
transConstant' MemType
tp Value
L.ValZeroInit =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> LLVMConst
ZeroConst MemType
tp)
transConstant' (PtrType SymType
stp) Value
L.ValNull =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> LLVMConst
ZeroConst (SymType -> MemType
PtrType SymType
stp))
transConstant' MemType
PtrOpaqueType Value
L.ValNull =
  LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> LLVMConst
ZeroConst MemType
PtrOpaqueType)
transConstant' (VecType Natural
n MemType
tp) (L.ValVector Type
_tp [Value]
xs)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Value] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Value]
xs)
  = MemType -> [LLVMConst] -> LLVMConst
VectorConst MemType
tp ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> m LLVMConst) -> [Value] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
tp) [Value]
xs
transConstant' (ArrayType Natural
n MemType
tp) (L.ValArray Type
_tp [Value]
xs)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Value] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Value]
xs)
  = MemType -> [LLVMConst] -> LLVMConst
ArrayConst MemType
tp ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> m LLVMConst) -> [Value] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
tp) [Value]
xs
transConstant' (StructType StructInfo
si) (L.ValStruct [Typed Value]
xs)
  | Bool -> Bool
not (StructInfo -> Bool
siIsPacked StructInfo
si)
  , Vector FieldInfo -> Int
forall a. Vector a -> Int
V.length (StructInfo -> Vector FieldInfo
siFields StructInfo
si) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Typed Value] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Typed Value]
xs
  = StructInfo -> [LLVMConst] -> LLVMConst
StructConst StructInfo
si ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Typed Value -> m LLVMConst) -> [Typed Value] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant [Typed Value]
xs
transConstant' (StructType StructInfo
si) (L.ValPackedStruct [Typed Value]
xs)
  | StructInfo -> Bool
siIsPacked StructInfo
si
  , Vector FieldInfo -> Int
forall a. Vector a -> Int
V.length (StructInfo -> Vector FieldInfo
siFields StructInfo
si) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Typed Value] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Typed Value]
xs
  = StructInfo -> [LLVMConst] -> LLVMConst
StructConst StructInfo
si ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Typed Value -> m LLVMConst) -> [Typed Value] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant [Typed Value]
xs

transConstant' (ArrayType Natural
n MemType
tp) (L.ValString [Word8]
cs)
  | MemType
tp MemType -> MemType -> Bool
forall a. Eq a => a -> a -> Bool
== Natural -> MemType
IntType Natural
8, Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Word8] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Word8]
cs)
  = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst)
-> (ByteString -> LLVMConst) -> ByteString -> m LLVMConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> LLVMConst
StringConst (ByteString -> m LLVMConst) -> ByteString -> m LLVMConst
forall a b. (a -> b) -> a -> b
$! [Word8] -> ByteString
BS.pack [Word8]
cs

transConstant' MemType
_ (L.ValConstExpr ConstExpr' BlockLabel
cexpr) = ConstExpr' BlockLabel -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
ConstExpr' BlockLabel -> m LLVMConst
transConstantExpr ConstExpr' BlockLabel
cexpr

transConstant' MemType
tp Value
val =
  [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Cannot compute constant value for expression: "
                       , [Char]
"Type: "  [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char]) -> Doc Any -> [Char]
forall a b. (a -> b) -> a -> b
$ MemType -> Doc Any
forall ann. MemType -> Doc ann
ppMemType MemType
tp)
                       , [Char]
"Value: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ Value -> Doc
LPP.ppValue Value
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 :: forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
GEPResult LLVMConst -> m (MemType, LLVMConst)
evalConstGEP (GEPResult NatRepr n
lanes MemType
finalMemType GEP n LLVMConst
gep0) =
   do [LLVMConst]
xs <- GEP n LLVMConst -> m [LLVMConst]
forall (n :: Natural). GEP n LLVMConst -> m [LLVMConst]
go GEP n LLVMConst
gep0
      Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([LLVMConst] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [LLVMConst]
xs) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
lanes)
             ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Unexpected vector length in result of constant GEP")
      case [LLVMConst]
xs of
        [LLVMConst
x] -> (MemType, LLVMConst) -> m (MemType, LLVMConst)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ( SymType -> MemType
PtrType (MemType -> SymType
MemType MemType
finalMemType), LLVMConst
x)
        [LLVMConst]
_   -> (MemType, LLVMConst) -> m (MemType, LLVMConst)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ( Natural -> MemType -> MemType
VecType (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([LLVMConst] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [LLVMConst]
xs)) (SymType -> MemType
PtrType (MemType -> SymType
MemType MemType
finalMemType))
                      , MemType -> [LLVMConst] -> LLVMConst
VectorConst (SymType -> MemType
PtrType (MemType -> SymType
MemType MemType
finalMemType)) [LLVMConst]
xs
                      )

  where
  dl :: DataLayout
dl = TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc

  asOffset :: MemType -> LLVMConst -> m Integer
  asOffset :: MemType -> LLVMConst -> m Integer
asOffset MemType
_ (ZeroConst (IntType Natural
_)) = Integer -> m Integer
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
0
  asOffset MemType
mt (IntConst NatRepr w
_ BV w
x) =
    do let x' :: Integer
x' = BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Bytes -> Integer
bytesToInteger (DataLayout -> MemType -> Bytes
memTypeSize DataLayout
dl MemType
mt)
       Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr wptr -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Computed offset overflow in constant GEP")
       Integer -> m Integer
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
x'
  asOffset MemType
ty LLVMConst
val = [Char] -> m Integer
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m Integer) -> [Char] -> m Integer
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
    [ [Char]
"Expected offset value in constant GEP"
    , [Char]
"Type: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ MemType -> [Char]
forall a. Show a => a -> [Char]
show MemType
ty
    , [Char]
"Offset: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ LLVMConst -> [Char]
forall a. Show a => a -> [Char]
show LLVMConst
val
    ]

  addOffset :: Integer -> LLVMConst -> m LLVMConst
  addOffset :: Integer -> LLVMConst -> m LLVMConst
addOffset Integer
x (SymbolConst Symbol
sym Integer
off) = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Symbol -> Integer -> LLVMConst
SymbolConst Symbol
sym (Integer
offInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
x))
  addOffset Integer
_ LLVMConst
constant = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
    [ [Char]
"Expected symbol constant in constant GEP"
    , [Char]
"Constant: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ LLVMConst -> [Char]
forall a. Show a => a -> [Char]
show LLVMConst
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 :: forall (n :: Natural). GEP n LLVMConst -> m [LLVMConst]
go (GEP_scalar_base LLVMConst
base)
    = [LLVMConst] -> m [LLVMConst]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [LLVMConst
base]

  -- Vector base, deconstruct the input value and return the
  -- corresponding values.
  go (GEP_vector_base NatRepr n
n LLVMConst
x)
    = Natural -> (LLVMConst -> m LLVMConst) -> LLVMConst -> m [LLVMConst]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf (NatRepr n -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
n) LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x

  -- Scatter a scalar input across n lanes
  go (GEP_scatter NatRepr n
n GEP 1 LLVMConst
gep)
    = do [LLVMConst]
ps <- GEP 1 LLVMConst -> m [LLVMConst]
forall (n :: Natural). GEP n LLVMConst -> m [LLVMConst]
go GEP 1 LLVMConst
gep
         case [LLVMConst]
ps of
           [LLVMConst
p] -> [LLVMConst] -> m [LLVMConst]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int -> LLVMConst -> [LLVMConst]
forall a. Int -> a -> [a]
replicate (NatRepr n -> Int
forall (n :: Natural). NatRepr n -> Int
widthVal NatRepr n
n) LLVMConst
p)
           [LLVMConst]
_   -> [Char] -> m [LLVMConst]
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"vector length mismatch in GEP scatter"

  -- Add the offset corresponding to the given field across
  -- all the lanes of the GEP
  go (GEP_field FieldInfo
fi GEP n LLVMConst
gep)
    = do [LLVMConst]
ps <- GEP n LLVMConst -> m [LLVMConst]
forall (n :: Natural). GEP n LLVMConst -> m [LLVMConst]
go GEP n LLVMConst
gep
         let i :: Integer
i = Bytes -> Integer
bytesToInteger (FieldInfo -> Bytes
fiOffset FieldInfo
fi)
         (LLVMConst -> m LLVMConst) -> [LLVMConst] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Integer -> LLVMConst -> m LLVMConst
addOffset Integer
i) [LLVMConst]
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 MemType
mt GEP n LLVMConst
gep LLVMConst
x)
    = do [LLVMConst]
ps <- GEP n LLVMConst -> m [LLVMConst]
forall (n :: Natural). GEP n LLVMConst -> m [LLVMConst]
go GEP n LLVMConst
gep
         Integer
i  <- MemType -> LLVMConst -> m Integer
asOffset MemType
mt LLVMConst
x
         (LLVMConst -> m LLVMConst) -> [LLVMConst] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Integer -> LLVMConst -> m LLVMConst
addOffset Integer
i) [LLVMConst]
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 MemType
mt GEP n LLVMConst
gep LLVMConst
x)
    = do [LLVMConst]
ps <- GEP n LLVMConst -> m [LLVMConst]
forall (n :: Natural). GEP n LLVMConst -> m [LLVMConst]
go GEP n LLVMConst
gep
         [Integer]
is <- Natural -> (LLVMConst -> m Integer) -> LLVMConst -> m [Integer]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([LLVMConst] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [LLVMConst]
ps)) (MemType -> LLVMConst -> m Integer
asOffset MemType
mt) LLVMConst
x
         (Integer -> LLVMConst -> m LLVMConst)
-> [Integer] -> [LLVMConst] -> m [LLVMConst]
forall (m :: Type -> Type) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Integer -> LLVMConst -> m LLVMConst
addOffset [Integer]
is [LLVMConst]
ps

-- | Evaluate a floating point comparison.
evalFcmp ::
  RealFloat a =>
  L.FCmpOp ->
  a -> a -> LLVMConst
evalFcmp :: forall a. RealFloat a => FCmpOp -> a -> a -> LLVMConst
evalFcmp FCmpOp
op a
x a
y = Bool -> LLVMConst
boolConst (Bool -> LLVMConst) -> Bool -> LLVMConst
forall a b. (a -> b) -> a -> b
$ case FCmpOp
op of
  FCmpOp
L.Ffalse -> Bool
False
  FCmpOp
L.Ftrue  -> Bool
True
  FCmpOp
L.Foeq   -> Bool
ordered Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
  FCmpOp
L.Fone   -> Bool
ordered Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y
  FCmpOp
L.Fogt   -> Bool
ordered Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>  a
y
  FCmpOp
L.Foge   -> Bool
ordered Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y
  FCmpOp
L.Folt   -> Bool
ordered Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<  a
y
  FCmpOp
L.Fole   -> Bool
ordered Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y
  FCmpOp
L.Ford   -> Bool
ordered
  FCmpOp
L.Fueq   -> Bool
unordered Bool -> Bool -> Bool
|| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
  FCmpOp
L.Fune   -> Bool
unordered Bool -> Bool -> Bool
|| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y
  FCmpOp
L.Fugt   -> Bool
unordered Bool -> Bool -> Bool
|| a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>  a
y
  FCmpOp
L.Fuge   -> Bool
unordered Bool -> Bool -> Bool
|| a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y
  FCmpOp
L.Fult   -> Bool
unordered Bool -> Bool -> Bool
|| a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<  a
y
  FCmpOp
L.Fule   -> Bool
unordered Bool -> Bool -> Bool
|| a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y
  FCmpOp
L.Funo   -> Bool
unordered
 where
 unordered :: Bool
unordered = a -> Bool
forall a. RealFloat a => a -> Bool
isNaN a
x Bool -> Bool -> Bool
|| a -> Bool
forall a. RealFloat a => a -> Bool
isNaN a
y
 ordered :: Bool
ordered   = Bool -> Bool
not Bool
unordered

-- | Evaluate an integer comparison.
evalIcmp ::
  (1 <= w) =>
  L.ICmpOp ->
  NatRepr w ->
  BV.BV w -> BV.BV w -> LLVMConst
evalIcmp :: forall (w :: Natural).
(1 <= w) =>
ICmpOp -> NatRepr w -> BV w -> BV w -> LLVMConst
evalIcmp ICmpOp
op NatRepr w
w BV w
x BV w
y = Bool -> LLVMConst
boolConst (Bool -> LLVMConst) -> Bool -> LLVMConst
forall a b. (a -> b) -> a -> b
$ case ICmpOp
op of
  ICmpOp
L.Ieq  -> BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
y
  ICmpOp
L.Ine  -> BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
/= BV w
y
  ICmpOp
L.Iugt -> BV w -> BV w -> Bool
forall (w :: Natural). BV w -> BV w -> Bool
BV.ult BV w
y BV w
x
  ICmpOp
L.Iuge -> BV w -> BV w -> Bool
forall (w :: Natural). BV w -> BV w -> Bool
BV.ule BV w
y BV w
x
  ICmpOp
L.Iult -> BV w -> BV w -> Bool
forall (w :: Natural). BV w -> BV w -> Bool
BV.ult BV w
x BV w
y
  ICmpOp
L.Iule -> BV w -> BV w -> Bool
forall (w :: Natural). BV w -> BV w -> Bool
BV.ule BV w
x BV w
y
  ICmpOp
L.Isgt -> NatRepr w -> BV w -> BV w -> Bool
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Bool
BV.slt NatRepr w
w BV w
y BV w
x
  ICmpOp
L.Isge -> NatRepr w -> BV w -> BV w -> Bool
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Bool
BV.sle NatRepr w
w BV w
y BV w
x
  ICmpOp
L.Islt -> NatRepr w -> BV w -> BV w -> Bool
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Bool
BV.slt NatRepr w
w BV w
x BV w
y
  ICmpOp
L.Isle -> NatRepr w -> BV w -> BV w -> Bool
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Bool
BV.sle NatRepr w
w BV w
x BV w
y

-- | Evaluate a binary arithmetic operation.
evalArith ::
  (MonadError String m, HasPtrWidth wptr) =>
  L.ArithOp ->
  MemType ->
  Arith -> Arith -> m LLVMConst
evalArith :: forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
ArithOp -> MemType -> Arith -> Arith -> m LLVMConst
evalArith ArithOp
op (IntType Natural
m) (ArithI ArithInt
x) (ArithI ArithInt
y)
  | Just (Some NatRepr x
w) <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
m
  , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
  = ArithOp -> NatRepr x -> ArithInt -> ArithInt -> m LLVMConst
forall (w :: Natural) (m :: Type -> Type) (wptr :: Natural).
(1 <= w, MonadError [Char] m, HasPtrWidth wptr) =>
ArithOp -> NatRepr w -> ArithInt -> ArithInt -> m LLVMConst
evalIarith ArithOp
op NatRepr x
w ArithInt
x ArithInt
y
evalArith ArithOp
op MemType
FloatType (ArithF Float
x) (ArithF Float
y) = Float -> LLVMConst
FloatConst (Float -> LLVMConst) -> m Float -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ArithOp -> Float -> Float -> m Float
forall a (m :: Type -> Type).
(RealFrac a, MonadError [Char] m) =>
ArithOp -> a -> a -> m a
evalFarith ArithOp
op Float
x Float
y
evalArith ArithOp
op MemType
DoubleType (ArithD Double
x) (ArithD Double
y) = Double -> LLVMConst
DoubleConst (Double -> LLVMConst) -> m Double -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ArithOp -> Double -> Double -> m Double
forall a (m :: Type -> Type).
(RealFrac a, MonadError [Char] m) =>
ArithOp -> a -> a -> m a
evalFarith ArithOp
op Double
x Double
y
evalArith ArithOp
_ MemType
_ Arith
_ Arith
_ = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"binary arithmetic argument mismatch"

-- | Evaluate a unary arithmetic operation.
evalUnaryArith ::
  (MonadError String m, HasPtrWidth wptr) =>
  L.UnaryArithOp ->
  MemType ->
  Arith -> m LLVMConst
evalUnaryArith :: forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
UnaryArithOp -> MemType -> Arith -> m LLVMConst
evalUnaryArith UnaryArithOp
op MemType
FloatType (ArithF Float
x) = Float -> LLVMConst
FloatConst (Float -> LLVMConst) -> m Float -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> UnaryArithOp -> Float -> m Float
forall a (m :: Type -> Type).
(RealFrac a, MonadError [Char] m) =>
UnaryArithOp -> a -> m a
evalFunaryArith UnaryArithOp
op Float
x
evalUnaryArith UnaryArithOp
op MemType
DoubleType (ArithD Double
x) = Double -> LLVMConst
DoubleConst (Double -> LLVMConst) -> m Double -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> UnaryArithOp -> Double -> m Double
forall a (m :: Type -> Type).
(RealFrac a, MonadError [Char] m) =>
UnaryArithOp -> a -> m a
evalFunaryArith UnaryArithOp
op Double
x
evalUnaryArith UnaryArithOp
_ MemType
_ Arith
_ = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"unary arithmetic argument mismatch"

-- | Evaluate a binary floating-point operation.
evalFarith ::
  (RealFrac a, MonadError String m) =>
  L.ArithOp ->
  a -> a -> m a
evalFarith :: forall a (m :: Type -> Type).
(RealFrac a, MonadError [Char] m) =>
ArithOp -> a -> a -> m a
evalFarith ArithOp
op a
x a
y =
  case ArithOp
op of
    ArithOp
L.FAdd -> a -> m a
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y)
    ArithOp
L.FSub -> a -> m a
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y)
    ArithOp
L.FMul -> a -> m a
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
y)
    ArithOp
L.FDiv -> a -> m a
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
y)
    ArithOp
L.FRem -> a -> m a
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a -> a -> a
forall a. Real a => a -> a -> a
mod' a
x a
y)
    ArithOp
_ -> [Char] -> m a
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"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 :: forall a (m :: Type -> Type).
(RealFrac a, MonadError [Char] m) =>
UnaryArithOp -> a -> m a
evalFunaryArith UnaryArithOp
op a
x =
  case UnaryArithOp
op of
    UnaryArithOp
L.FNeg -> a -> m a
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a -> a
forall a. Num a => a -> a
negate a
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 :: forall (w :: Natural) (m :: Type -> Type) (wptr :: Natural).
(1 <= w, MonadError [Char] m, HasPtrWidth wptr) =>
ArithOp -> NatRepr w -> ArithInt -> ArithInt -> m LLVMConst
evalIarith ArithOp
op NatRepr w
w (ArithInt Integer
x) (ArithInt Integer
y)
  = NatRepr w -> BV w -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr w
w (BV w -> LLVMConst) -> m (BV w) -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ArithOp -> NatRepr w -> BV w -> BV w -> m (BV w)
forall (w :: Natural) (m :: Type -> Type).
(1 <= w, MonadError [Char] m) =>
ArithOp -> NatRepr w -> BV w -> BV w -> m (BV w)
evalIarith' ArithOp
op NatRepr w
w (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
x) (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
y)
evalIarith ArithOp
op NatRepr w
w (ArithPtr Symbol
sym Integer
x) (ArithInt Integer
y)
  | Just w :~: wptr
Refl <- NatRepr w -> NatRepr wptr -> Maybe (w :~: wptr)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
  , L.Add Bool
_ Bool
_ <- ArithOp
op
  = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> LLVMConst
SymbolConst Symbol
sym (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
y)
  | Bool
otherwise
  = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Illegal operation applied to pointer argument"
evalIarith ArithOp
op NatRepr w
w (ArithInt Integer
x) (ArithPtr Symbol
sym Integer
y)
  | Just w :~: wptr
Refl <- NatRepr w -> NatRepr wptr -> Maybe (w :~: wptr)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
  , L.Add Bool
_ Bool
_ <- ArithOp
op
  = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> LLVMConst
SymbolConst Symbol
sym (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
y)
  | Bool
otherwise
  = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Illegal operation applied to pointer argument"
evalIarith ArithOp
op NatRepr w
w (ArithPtr Symbol
symx Integer
x) (ArithPtr Symbol
symy Integer
y)
  | Just w :~: wptr
Refl <- NatRepr w -> NatRepr wptr -> Maybe (w :~: wptr)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
  , Symbol
symx Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
symy
  , L.Sub Bool
_ Bool
_ <- ArithOp
op
  = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst ?ptrWidth::NatRepr w
NatRepr w
?ptrWidth (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr w
NatRepr w
?ptrWidth (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y))
  | Bool
otherwise
  = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"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' :: forall (w :: Natural) (m :: Type -> Type).
(1 <= w, MonadError [Char] m) =>
ArithOp -> NatRepr w -> BV w -> BV w -> m (BV w)
evalIarith' ArithOp
op NatRepr w
w BV w
x BV w
y = do
  let nuwTest :: Bool -> Overflow a -> f ()
nuwTest Bool
nuw Overflow a
zres =
        Bool -> f () -> f ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
nuw Bool -> Bool -> Bool
&& Overflow a -> Bool
forall a. Overflow a -> Bool
BV.ofUnsigned Overflow a
zres)
             (e -> f ()
forall a. e -> f a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError e
"Unsigned overflow in constant arithmetic operation")
  let nswTest :: Bool -> Overflow a -> f ()
nswTest Bool
nsw Overflow a
zres =
        Bool -> f () -> f ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
nsw Bool -> Bool -> Bool
&& Overflow a -> Bool
forall a. Overflow a -> Bool
BV.ofSigned Overflow a
zres)
             (e -> f ()
forall a. e -> f a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError e
"Signed overflow in constant arithmetic operation")
  case ArithOp
op of
    L.Add Bool
nuw Bool
nsw ->
      do let zres :: Overflow (BV w)
zres = NatRepr w -> BV w -> BV w -> Overflow (BV w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Overflow (BV w)
BV.addOf NatRepr w
w BV w
x BV w
y
         Bool -> Overflow (BV w) -> m ()
forall {f :: Type -> Type} {e} {a}.
(MonadError e f, IsString e) =>
Bool -> Overflow a -> f ()
nuwTest Bool
nuw Overflow (BV w)
zres
         Bool -> Overflow (BV w) -> m ()
forall {f :: Type -> Type} {e} {a}.
(MonadError e f, IsString e) =>
Bool -> Overflow a -> f ()
nswTest Bool
nsw Overflow (BV w)
zres
         BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Overflow (BV w) -> BV w
forall a. Overflow a -> a
BV.ofResult Overflow (BV w)
zres)

    L.Sub Bool
nuw Bool
nsw ->
      do let zres :: Overflow (BV w)
zres = NatRepr w -> BV w -> BV w -> Overflow (BV w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Overflow (BV w)
BV.subOf NatRepr w
w BV w
x BV w
y
         Bool -> Overflow (BV w) -> m ()
forall {f :: Type -> Type} {e} {a}.
(MonadError e f, IsString e) =>
Bool -> Overflow a -> f ()
nuwTest Bool
nuw Overflow (BV w)
zres
         Bool -> Overflow (BV w) -> m ()
forall {f :: Type -> Type} {e} {a}.
(MonadError e f, IsString e) =>
Bool -> Overflow a -> f ()
nswTest Bool
nsw Overflow (BV w)
zres
         BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Overflow (BV w) -> BV w
forall a. Overflow a -> a
BV.ofResult Overflow (BV w)
zres)

    L.Mul Bool
nuw Bool
nsw ->
      do let zres :: Overflow (BV w)
zres = NatRepr w -> BV w -> BV w -> Overflow (BV w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Overflow (BV w)
BV.mulOf NatRepr w
w BV w
x BV w
y
         Bool -> Overflow (BV w) -> m ()
forall {f :: Type -> Type} {e} {a}.
(MonadError e f, IsString e) =>
Bool -> Overflow a -> f ()
nuwTest Bool
nuw Overflow (BV w)
zres
         Bool -> Overflow (BV w) -> m ()
forall {f :: Type -> Type} {e} {a}.
(MonadError e f, IsString e) =>
Bool -> Overflow a -> f ()
nswTest Bool
nsw Overflow (BV w)
zres
         BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Overflow (BV w) -> BV w
forall a. Overflow a -> a
BV.ofResult Overflow (BV w)
zres)

    L.UDiv Bool
exact ->
      do Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (BV w
y BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Division by 0 in constant arithmetic operation")
         let (BV w
z,BV w
r) = BV w -> BV w -> (BV w, BV w)
forall (w :: Natural). BV w -> BV w -> (BV w, BV w)
BV.uquotRem BV w
x BV w
y
         Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
exact Bool -> Bool -> Bool
&& BV w
r BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Exact division failed in constant arithmetic operation")
         BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
z

    L.SDiv Bool
exact ->
      do Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (BV w
y BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Division by 0 in constant arithmetic operation")
         Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w Bool -> Bool -> Bool
&& BV w
y BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (-Integer
1))
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Signed division overflow in constant arithmetic operation")
         let (BV w
z,BV w
r) = NatRepr w -> BV w -> BV w -> (BV w, BV w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> (BV w, BV w)
BV.squotRem NatRepr w
w BV w
x BV w
y
         Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
exact Bool -> Bool -> Bool
&& BV w
r BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w )
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Exact division failed in constant arithmetic operation")
         BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
z
    ArithOp
L.URem ->
      do Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (BV w
y BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Division by 0 in constant arithmetic operation")
         let r :: BV w
r = BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.urem BV w
x BV w
y
         BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
r

    ArithOp
L.SRem ->
      do Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (BV w
y BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Division by 0 in constant arithmetic operation")
         Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w Bool -> Bool -> Bool
&& BV w
y BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (-Integer
1))
              ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Signed division overflow in constant arithmetic operation")
         let r :: BV w
r = NatRepr w -> BV w -> BV w -> BV w
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> BV w
BV.srem NatRepr w
w BV w
x BV w
y
         BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
r

    ArithOp
_ -> [Char] -> m (BV w)
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"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 :: forall (w :: Natural) (m :: Type -> Type).
(1 <= w, MonadError [Char] m) =>
BitOp -> NatRepr w -> BV w -> BV w -> m LLVMConst
evalBitwise BitOp
op NatRepr w
w BV w
x BV w
y = NatRepr w -> BV w -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr w
w (BV w -> LLVMConst) -> m (BV w) -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
  let yshf :: Natural
yshf = Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
y) :: Natural
  in case BitOp
op of
       BitOp
L.And -> BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.and BV w
x BV w
y)
       BitOp
L.Or  -> BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.or  BV w
x BV w
y)
       BitOp
L.Xor -> BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.xor BV w
x BV w
y)
       L.Shl Bool
nuw Bool
nsw ->
         do let zres :: Overflow (BV w)
zres = NatRepr w -> BV w -> Natural -> Overflow (BV w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> Natural -> Overflow (BV w)
BV.shlOf NatRepr w
w BV w
x Natural
yshf
            Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
nuw Bool -> Bool -> Bool
&& Overflow (BV w) -> Bool
forall a. Overflow a -> Bool
BV.ofUnsigned Overflow (BV w)
zres)
                 ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Unsigned overflow in left shift")
            Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
nsw Bool -> Bool -> Bool
&& Overflow (BV w) -> Bool
forall a. Overflow a -> Bool
BV.ofSigned Overflow (BV w)
zres)
                 ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Signed overflow in left shift")
            BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Overflow (BV w) -> BV w
forall a. Overflow a -> a
BV.ofResult Overflow (BV w)
zres)
       L.Lshr Bool
exact ->
         do let z :: BV w
z = NatRepr w -> BV w -> Natural -> BV w
forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.lshr NatRepr w
w BV w
x Natural
yshf
            Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
exact Bool -> Bool -> Bool
&& BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr w -> BV w -> Natural -> BV w
forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.shl NatRepr w
w BV w
z Natural
yshf)
                 ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Exact right shift failed")
            BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
z
       L.Ashr Bool
exact ->
         do let z :: BV w
z = NatRepr w -> BV w -> Natural -> BV w
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> Natural -> BV w
BV.ashr NatRepr w
w BV w
x Natural
yshf
            Bool -> m () -> m ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool
exact Bool -> Bool -> Bool
&& BV w
x BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr w -> BV w -> Natural -> BV w
forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.shl NatRepr w
w BV w
z Natural
yshf)
                 ([Char] -> m ()
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Exact right shift failed")
            BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
z

-- | Evaluate a conversion operation on constants.
evalConv ::
  (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
  L.ConstExpr ->
  L.ConvOp ->
  MemType ->
  LLVMConst ->
  m LLVMConst
evalConv :: forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
ConstExpr' BlockLabel
-> ConvOp -> MemType -> LLVMConst -> m LLVMConst
evalConv ConstExpr' BlockLabel
expr ConvOp
op MemType
mt LLVMConst
x = case ConvOp
op of
    ConvOp
L.FpToUi
      | IntType Natural
n <- MemType
mt
      , Just (Some NatRepr x
w) <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
n
      , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
      , FloatConst Float
f <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w (NatRepr x -> Integer -> BV x
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w (Float -> Integer
forall b. Integral b => Float -> b
forall a b. (RealFrac a, Integral b) => a -> b
truncate Float
f))

      | IntType Natural
n <- MemType
mt
      , Just (Some NatRepr x
w) <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
n
      , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
      , DoubleConst Double
d <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w (NatRepr x -> Integer -> BV x
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w (Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
truncate Double
d))

    ConvOp
L.FpToSi
      | IntType Natural
n <- MemType
mt
      , Just (Some NatRepr x
w) <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
n
      , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
      , FloatConst Float
f <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w (NatRepr x -> Integer -> BV x
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w (Float -> Integer
forall b. Integral b => Float -> b
forall a b. (RealFrac a, Integral b) => a -> b
truncate Float
f))

      | IntType Natural
n <- MemType
mt
      , Just (Some NatRepr x
w) <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
n
      , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
      , DoubleConst Double
d <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w (NatRepr x -> Integer -> BV x
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w (Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
truncate Double
d))

    ConvOp
L.UiToFp
      | MemType
FloatType <- MemType
mt
      , IntConst NatRepr w
_w BV w
i <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Float -> LLVMConst
FloatConst (Integer -> Float
forall a. Num a => Integer -> a
fromInteger (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
i) :: Float)

      | MemType
DoubleType <- MemType
mt
      , IntConst NatRepr w
_w BV w
i <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Double -> LLVMConst
DoubleConst (Integer -> Double
forall a. Num a => Integer -> a
fromInteger (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
i) :: Double)

    ConvOp
L.SiToFp
      | MemType
FloatType <- MemType
mt
      , IntConst NatRepr w
w BV w
i <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Float -> LLVMConst
FloatConst (Integer -> Float
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> BV w -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
w BV w
i) :: Float)

      | MemType
DoubleType <- MemType
mt
      , IntConst NatRepr w
w BV w
i <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Double -> LLVMConst
DoubleConst (Integer -> Double
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> BV w -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
w BV w
i) :: Double)

    ConvOp
L.Trunc
      | IntType Natural
n <- MemType
mt
      , IntConst NatRepr w
w BV w
i <- LLVMConst
x
      , Just (Some NatRepr x
w') <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
n
      , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w'
      -> case NatRepr x -> NatRepr w -> NatCases x w
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr x
w' NatRepr w
w of
          NatCaseLT LeqProof (x + 1) w
LeqProof -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w' (NatRepr x -> BV w -> BV x
forall (w' :: Natural) (w :: Natural).
((w' + 1) <= w) =>
NatRepr w' -> BV w -> BV w'
BV.trunc NatRepr x
w' BV w
i)
          NatCases x w
NatCaseEQ -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x
          NatCaseGT LeqProof (w + 1) x
LeqProof ->
            [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [Char]
"Attempted to truncate " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr w -> [Char]
forall a. Show a => a -> [Char]
show NatRepr w
w [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" bits to " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr x -> [Char]
forall a. Show a => a -> [Char]
show NatRepr x
w'

    ConvOp
L.ZExt
      | IntType Natural
n <- MemType
mt
      , IntConst NatRepr w
w BV w
i <- LLVMConst
x
      , Just (Some NatRepr x
w') <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
n
      , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w'
      -> case NatRepr w -> NatRepr x -> NatCases w x
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w NatRepr x
w' of
          NatCaseLT LeqProof (w + 1) x
LeqProof -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w' (NatRepr x -> BV w -> BV x
forall (w :: Natural) (w' :: Natural).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
BV.zext NatRepr x
w' BV w
i)
          NatCases w x
NatCaseEQ -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x
          NatCaseGT LeqProof (x + 1) w
LeqProof ->
            [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [Char]
"Attempted to zext " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr w -> [Char]
forall a. Show a => a -> [Char]
show NatRepr w
w [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" bits to " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr x -> [Char]
forall a. Show a => a -> [Char]
show NatRepr x
w'

    ConvOp
L.SExt
      | IntType Natural
n <- MemType
mt
      , IntConst NatRepr w
w BV w
i <- LLVMConst
x
      , Just (Some NatRepr x
w') <- Natural -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Natural
n
      , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w'
      -> case NatRepr w -> NatRepr x -> NatCases w x
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w NatRepr x
w' of
          NatCaseLT LeqProof (w + 1) x
LeqProof -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
w' (NatRepr w -> NatRepr x -> BV w -> BV x
forall (w :: Natural) (w' :: Natural).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
BV.sext NatRepr w
w NatRepr x
w' BV w
i)
          NatCases w x
NatCaseEQ -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x
          NatCaseGT LeqProof (x + 1) w
LeqProof ->
            [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [Char]
"Attempted to sext " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr w -> [Char]
forall a. Show a => a -> [Char]
show NatRepr w
w [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" bits to " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr x -> [Char]
forall a. Show a => a -> [Char]
show NatRepr x
w'

    ConvOp
L.FpTrunc
      | MemType
DoubleType <- MemType
mt
      , DoubleConst Double
d <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Double -> LLVMConst
DoubleConst Double
d

      | MemType
FloatType <- MemType
mt
      , DoubleConst Double
d <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Float -> LLVMConst
FloatConst (Double -> Float
forall a b. (Real a, Fractional b) => a -> b
realToFrac Double
d)

      | MemType
FloatType <- MemType
mt
      , FloatConst Float
f <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Float -> LLVMConst
FloatConst Float
f

    ConvOp
L.FpExt
      | MemType
DoubleType <- MemType
mt
      , DoubleConst Double
d <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Double -> LLVMConst
DoubleConst Double
d

      | MemType
DoubleType <- MemType
mt
      , FloatConst Float
f <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Double -> LLVMConst
DoubleConst (Float -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Float
f)

      | MemType
FloatType <- MemType
mt
      , FloatConst Float
f <- LLVMConst
x
      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ Float -> LLVMConst
FloatConst Float
f

    ConvOp
L.IntToPtr -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x
    ConvOp
L.PtrToInt -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x

    ConvOp
_ -> [Char] -> m LLVMConst
badExp [Char]
"unexpected conversion operation"

 where badExp :: [Char] -> m LLVMConst
badExp [Char]
msg = [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [[Char]
msg, ConstExpr' BlockLabel -> [Char]
forall a. Show a => a -> [Char]
show ConstExpr' BlockLabel
expr]


castToInt ::
  MonadError String m =>
  L.ConstExpr {- ^ original expression to evaluate -} ->
  EndianForm ->
  Natural ->
  MemType ->
  LLVMConst ->
  m Integer
castToInt :: forall (m :: Type -> Type).
MonadError [Char] m =>
ConstExpr' BlockLabel
-> EndianForm -> Natural -> MemType -> LLVMConst -> m Integer
castToInt ConstExpr' BlockLabel
_expr EndianForm
_endian Natural
_w (IntType Natural
w) LLVMConst
x = Natural -> LLVMConst -> m Integer
forall (m :: Type -> Type).
MonadError [Char] m =>
Natural -> LLVMConst -> m Integer
asInt Natural
w LLVMConst
x
castToInt ConstExpr' BlockLabel
expr EndianForm
endian Natural
w (VecType Natural
n MemType
tp) LLVMConst
x
  | (Natural
m,Natural
0) <- Natural
w Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
n =
  do [Integer]
xs <- Natural -> (LLVMConst -> m Integer) -> LLVMConst -> m [Integer]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (ConstExpr' BlockLabel
-> EndianForm -> Natural -> MemType -> LLVMConst -> m Integer
forall (m :: Type -> Type).
MonadError [Char] m =>
ConstExpr' BlockLabel
-> EndianForm -> Natural -> MemType -> LLVMConst -> m Integer
castToInt ConstExpr' BlockLabel
expr EndianForm
endian Natural
m MemType
tp) LLVMConst
x
     let indices :: [Natural]
indices = case EndianForm
endian of
                     EndianForm
LittleEndian -> [Natural
0 .. Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1]
                     EndianForm
BigEndian -> [Natural] -> [Natural]
forall a. [a] -> [a]
reverse [Natural
0 .. Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1]
     let pieces :: [Integer]
pieces = [ Integer
v Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
m))
                  | Natural
i <- [Natural]
indices
                  | Integer
v <- [Integer]
xs
                  ]
     Integer -> m Integer
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.|.) Integer
0 [Integer]
pieces)

castToInt ConstExpr' BlockLabel
expr EndianForm
_ Natural
_ MemType
_ LLVMConst
_ =
  [Char] -> m Integer
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m Integer) -> [Char] -> m Integer
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [[Char]
"Cannot cast expression to integer type", ConstExpr' BlockLabel -> [Char]
forall a. Show a => a -> [Char]
show ConstExpr' BlockLabel
expr]

castFromInt ::
  MonadError String m =>
  EndianForm ->
  Integer ->
  Natural ->
  MemType ->
  m LLVMConst
castFromInt :: forall (m :: Type -> Type).
MonadError [Char] m =>
EndianForm -> Integer -> Natural -> MemType -> m LLVMConst
castFromInt EndianForm
_ Integer
xint Natural
w (IntType Natural
w')
  | Natural
w Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
w'
  , Some NatRepr x
wsz <- Natural -> Some NatRepr
mkNatRepr Natural
w
  , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
wsz
  = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr x
wsz (NatRepr x -> Integer -> BV x
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
wsz Integer
xint)

castFromInt EndianForm
endian Integer
xint Natural
w (VecType Natural
n MemType
tp)
  | (Natural
m,Natural
0) <- Natural
w Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
n =
  do let mask :: Integer
mask = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
m) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
     let indices :: [Natural]
indices = case EndianForm
endian of
                     EndianForm
LittleEndian -> [Natural
0 .. Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1]
                     EndianForm
BigEndian -> [Natural] -> [Natural]
forall a. [a] -> [a]
reverse [Natural
0 .. Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1]
     let pieces :: [Integer]
pieces = [ Integer
mask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Integer
xint Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
m))
                  | Natural
i <- [Natural]
indices
                  ]
     MemType -> [LLVMConst] -> LLVMConst
VectorConst MemType
tp ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> m LLVMConst) -> [Integer] -> m [LLVMConst]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\Integer
x -> EndianForm -> Integer -> Natural -> MemType -> m LLVMConst
forall (m :: Type -> Type).
MonadError [Char] m =>
EndianForm -> Integer -> Natural -> MemType -> m LLVMConst
castFromInt EndianForm
endian Integer
x Natural
m MemType
tp) [Integer]
pieces

castFromInt EndianForm
_ Integer
_ Natural
_ MemType
tp =
  [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [[Char]
"Cant cast integer to type", MemType -> [Char]
forall a. Show a => a -> [Char]
show MemType
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 :: forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
ConstExpr' BlockLabel
-> MemType -> LLVMConst -> MemType -> m LLVMConst
evalBitCast ConstExpr' BlockLabel
_ MemType
_ (ZeroConst MemType
_) MemType
tgtT = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> LLVMConst
ZeroConst MemType
tgtT)

-- pointer casts always succeed
evalBitCast ConstExpr' BlockLabel
_ (PtrType SymType
_) LLVMConst
expr (PtrType SymType
_) = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
expr
evalBitCast ConstExpr' BlockLabel
_ (PtrType SymType
_) LLVMConst
expr MemType
PtrOpaqueType = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
expr
evalBitCast ConstExpr' BlockLabel
_ MemType
PtrOpaqueType LLVMConst
expr (PtrType SymType
_) = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
expr
evalBitCast ConstExpr' BlockLabel
_ MemType
PtrOpaqueType LLVMConst
expr MemType
PtrOpaqueType = LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
expr

-- casts between vectors of the same length can just be done pointwise
evalBitCast ConstExpr' BlockLabel
expr (VecType Natural
n MemType
srcT) (VectorConst MemType
_ [LLVMConst]
xs) (VecType Natural
n' MemType
tgtT)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n' = MemType -> [LLVMConst] -> LLVMConst
VectorConst MemType
tgtT ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (LLVMConst -> m LLVMConst) -> [LLVMConst] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\LLVMConst
x -> ConstExpr' BlockLabel
-> MemType -> LLVMConst -> MemType -> m LLVMConst
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
ConstExpr' BlockLabel
-> MemType -> LLVMConst -> MemType -> m LLVMConst
evalBitCast ConstExpr' BlockLabel
expr MemType
srcT LLVMConst
x MemType
tgtT) [LLVMConst]
xs

-- otherwise, cast via an intermediate integer type
evalBitCast ConstExpr' BlockLabel
expr MemType
xty LLVMConst
x MemType
toty
  | Just Natural
w1 <- MemType -> Maybe Natural
memTypeBitwidth MemType
xty
  , Just Natural
w2 <- MemType -> Maybe Natural
memTypeBitwidth MemType
toty
  , Natural
w1 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
w2
  = do let endian :: EndianForm
endian = ?lc::TypeContext
TypeContext
?lc TypeContext
-> Getting EndianForm TypeContext EndianForm -> EndianForm
forall s a. s -> Getting a s a -> a
^. (TypeContext -> DataLayout)
-> (DataLayout -> Const EndianForm DataLayout)
-> TypeContext
-> Const EndianForm TypeContext
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to TypeContext -> DataLayout
llvmDataLayout((DataLayout -> Const EndianForm DataLayout)
 -> TypeContext -> Const EndianForm TypeContext)
-> ((EndianForm -> Const EndianForm EndianForm)
    -> DataLayout -> Const EndianForm DataLayout)
-> Getting EndianForm TypeContext EndianForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(EndianForm -> Const EndianForm EndianForm)
-> DataLayout -> Const EndianForm DataLayout
Lens' DataLayout EndianForm
intLayout
       Integer
xint <- ConstExpr' BlockLabel
-> EndianForm -> Natural -> MemType -> LLVMConst -> m Integer
forall (m :: Type -> Type).
MonadError [Char] m =>
ConstExpr' BlockLabel
-> EndianForm -> Natural -> MemType -> LLVMConst -> m Integer
castToInt ConstExpr' BlockLabel
expr EndianForm
endian Natural
w1 MemType
xty LLVMConst
x
       EndianForm -> Integer -> Natural -> MemType -> m LLVMConst
forall (m :: Type -> Type).
MonadError [Char] m =>
EndianForm -> Integer -> Natural -> MemType -> m LLVMConst
castFromInt EndianForm
endian Integer
xint Natural
w1 MemType
toty

evalBitCast ConstExpr' BlockLabel
expr MemType
_ LLVMConst
_ MemType
_ =
   [Char] -> m LLVMConst
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m LLVMConst) -> [Char] -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [[Char]
"illegal constant bitcast", ConstExpr' BlockLabel -> [Char]
forall a. Show a => a -> [Char]
show ConstExpr' BlockLabel
expr]


asVectorOf ::
  MonadError String m =>
  Natural ->
  (LLVMConst -> m a) ->
  (LLVMConst -> m [a])
asVectorOf :: forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n LLVMConst -> m a
f (ZeroConst (VecType Natural
m MemType
mt))
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m
  = do a
x <- LLVMConst -> m a
f (MemType -> LLVMConst
ZeroConst MemType
mt)
       [a] -> m [a]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int -> a -> [a]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) a
x)

asVectorOf Natural
n LLVMConst -> m a
f (VectorConst MemType
_ [LLVMConst]
xs)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([LLVMConst] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [LLVMConst]
xs)
  = (LLVMConst -> m a) -> [LLVMConst] -> m [a]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse LLVMConst -> m a
f [LLVMConst]
xs

asVectorOf Natural
n LLVMConst -> m a
_ LLVMConst
_
  = [Char] -> m [a]
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char]
"Expected vector constant value of length: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
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 :: forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
Natural -> LLVMConst -> m ArithInt
asArithInt Natural
n (ZeroConst (IntType Natural
m))
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m
  = ArithInt -> m ArithInt
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> ArithInt
ArithInt Integer
0)
asArithInt Natural
n (IntConst NatRepr w
w BV w
x)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w
  = ArithInt -> m ArithInt
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> ArithInt
ArithInt (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
x))
asArithInt Natural
n (SymbolConst Symbol
sym Integer
off)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr wptr -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
  = ArithInt -> m ArithInt
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Symbol -> Integer -> ArithInt
ArithPtr Symbol
sym Integer
off)
asArithInt Natural
_ LLVMConst
_
  = [Char] -> m ArithInt
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Expected integer value"

asArith ::
  (MonadError String m, HasPtrWidth wptr) =>
  MemType   {- ^ expected type -} ->
  LLVMConst {- ^ constant value -} ->
  m Arith
asArith :: forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> LLVMConst -> m Arith
asArith (IntType Natural
n) LLVMConst
x = ArithInt -> Arith
ArithI (ArithInt -> Arith) -> m ArithInt -> m Arith
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> LLVMConst -> m ArithInt
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
Natural -> LLVMConst -> m ArithInt
asArithInt Natural
n LLVMConst
x
asArith MemType
FloatType LLVMConst
x   = Float -> Arith
ArithF (Float -> Arith) -> m Float -> m Arith
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> LLVMConst -> m Float
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Float
asFloat LLVMConst
x
asArith MemType
DoubleType LLVMConst
x  = Double -> Arith
ArithD (Double -> Arith) -> m Double -> m Arith
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> LLVMConst -> m Double
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Double
asDouble LLVMConst
x
asArith MemType
_ LLVMConst
_ = [Char] -> m Arith
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Expected arithmetic type"

asInt ::
  MonadError String m =>
  Natural   {- ^ expected integer width -} ->
  LLVMConst {- ^ constant value -} ->
  m Integer
asInt :: forall (m :: Type -> Type).
MonadError [Char] m =>
Natural -> LLVMConst -> m Integer
asInt Natural
n (ZeroConst (IntType Natural
m))
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m
  = Integer -> m Integer
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
0
asInt Natural
n (IntConst NatRepr w
w BV w
x)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w
  = Integer -> m Integer
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
x)
asInt Natural
n LLVMConst
_
  = [Char] -> m Integer
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char]
"Expected integer constant of size " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
n)

asBV ::
  MonadError String m =>
  NatRepr w {- ^ expected integer width -} ->
  LLVMConst {- ^ constant value -} ->
  m (BV.BV w)
asBV :: forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr w
w (ZeroConst (IntType Natural
m))
  | NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
m
  = BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
asBV NatRepr w
w (IntConst NatRepr w
w' BV w
x)
  | Just w :~: w
Refl <- NatRepr w
w NatRepr w -> NatRepr w -> Maybe (w :~: w)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` NatRepr w
w'
  = BV w -> m (BV w)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BV w
BV w
x
asBV NatRepr w
w LLVMConst
_
  = [Char] -> m (BV w)
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char]
"Expected integer constant of size " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ NatRepr w -> [Char]
forall a. Show a => a -> [Char]
show NatRepr w
w)

asFloat ::
  MonadError String m =>
  LLVMConst {- ^ constant value -} ->
  m Float
asFloat :: forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Float
asFloat (ZeroConst MemType
FloatType) = Float -> m Float
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Float
0
asFloat (FloatConst Float
x) = Float -> m Float
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Float
x
asFloat LLVMConst
_ = [Char] -> m Float
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"Expected floating point constant"

asDouble ::
  MonadError String m =>
  LLVMConst {- ^ constant value -} ->
  m Double
asDouble :: forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Double
asDouble (ZeroConst MemType
DoubleType) = Double -> m Double
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Double
0
asDouble (DoubleConst Double
x) = Double -> m Double
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Double
x
asDouble LLVMConst
_ = [Char] -> m Double
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError [Char]
"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 :: forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
ConstExpr' BlockLabel -> m LLVMConst
transConstantExpr ConstExpr' BlockLabel
expr = case ConstExpr' BlockLabel
expr of
  L.ConstGEP Bool
inbounds Maybe Word64
_inrange Type
baseTy Typed Value
base [Typed Value]
exps -> -- TODO? pay attention to the inrange flag
    do GEPResult (Typed Value)
gep <- Bool
-> Type
-> Typed Value
-> [Typed Value]
-> m (GEPResult (Typed Value))
forall (wptr :: Natural) (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Bool
-> Type
-> Typed Value
-> [Typed Value]
-> m (GEPResult (Typed Value))
translateGEP Bool
inbounds Type
baseTy Typed Value
base [Typed Value]
exps
       GEPResult LLVMConst
gep' <- (Typed Value -> m LLVMConst)
-> GEPResult (Typed Value) -> m (GEPResult LLVMConst)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> GEPResult a -> f (GEPResult b)
traverse Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant GEPResult (Typed Value)
gep
       (MemType, LLVMConst) -> LLVMConst
forall a b. (a, b) -> b
snd ((MemType, LLVMConst) -> LLVMConst)
-> m (MemType, LLVMConst) -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GEPResult LLVMConst -> m (MemType, LLVMConst)
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
GEPResult LLVMConst -> m (MemType, LLVMConst)
evalConstGEP GEPResult LLVMConst
gep'

  L.ConstSelect Typed Value
b Typed Value
x Typed Value
y ->
    do LLVMConst
b' <- Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
b
       LLVMConst
x' <- Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
x
       LLVMConst
y' <- Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
y
       case LLVMConst
b' of
         IntConst NatRepr w
w BV w
v
           | BV w
v BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x'
           | Bool
otherwise      -> LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
y'
         LLVMConst
_ -> [Char] -> m LLVMConst
forall a. [Char] -> m a
badExp [Char]
"Expected boolean value in constant select"

  L.ConstBlockAddr Typed Value
_ BlockLabel
_ ->
    [Char] -> m LLVMConst
forall a. [Char] -> m a
badExp [Char]
"constant block addresses not supported"

  L.ConstFCmp FCmpOp
op Typed Value
a Typed Value
b ->
    do MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType (Typed Value -> Type
forall a. Typed a -> Type
L.typedType Typed Value
a)
       case MemType
mt of
         VecType Natural
n MemType
FloatType ->
           do [Float]
a' <- Natural -> (LLVMConst -> m Float) -> LLVMConst -> m [Float]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n LLVMConst -> m Float
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Float
asFloat (LLVMConst -> m [Float]) -> m LLVMConst -> m [Float]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
a
              [Float]
b' <- Natural -> (LLVMConst -> m Float) -> LLVMConst -> m [Float]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n LLVMConst -> m Float
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Float
asFloat (LLVMConst -> m [Float]) -> m LLVMConst -> m [Float]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
b
              LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ MemType -> [LLVMConst] -> LLVMConst
VectorConst (Natural -> MemType
IntType Natural
1) ([LLVMConst] -> LLVMConst) -> [LLVMConst] -> LLVMConst
forall a b. (a -> b) -> a -> b
$ (Float -> Float -> LLVMConst) -> [Float] -> [Float] -> [LLVMConst]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (FCmpOp -> Float -> Float -> LLVMConst
forall a. RealFloat a => FCmpOp -> a -> a -> LLVMConst
evalFcmp FCmpOp
op) [Float]
a' [Float]
b'
         VecType Natural
n MemType
DoubleType ->
           do [Double]
a' <- Natural -> (LLVMConst -> m Double) -> LLVMConst -> m [Double]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n LLVMConst -> m Double
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Double
asDouble (LLVMConst -> m [Double]) -> m LLVMConst -> m [Double]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
a
              [Double]
b' <- Natural -> (LLVMConst -> m Double) -> LLVMConst -> m [Double]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n LLVMConst -> m Double
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Double
asDouble (LLVMConst -> m [Double]) -> m LLVMConst -> m [Double]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
b
              LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ MemType -> [LLVMConst] -> LLVMConst
VectorConst (Natural -> MemType
IntType Natural
1) ([LLVMConst] -> LLVMConst) -> [LLVMConst] -> LLVMConst
forall a b. (a -> b) -> a -> b
$ (Double -> Double -> LLVMConst)
-> [Double] -> [Double] -> [LLVMConst]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (FCmpOp -> Double -> Double -> LLVMConst
forall a. RealFloat a => FCmpOp -> a -> a -> LLVMConst
evalFcmp FCmpOp
op) [Double]
a' [Double]
b'
         MemType
FloatType ->
           do Float
a' <- LLVMConst -> m Float
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Float
asFloat (LLVMConst -> m Float) -> m LLVMConst -> m Float
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
a
              Float
b' <- LLVMConst -> m Float
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Float
asFloat (LLVMConst -> m Float) -> m LLVMConst -> m Float
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
b
              LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ FCmpOp -> Float -> Float -> LLVMConst
forall a. RealFloat a => FCmpOp -> a -> a -> LLVMConst
evalFcmp FCmpOp
op Float
a' Float
b'
         MemType
DoubleType ->
           do Double
a' <- LLVMConst -> m Double
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Double
asDouble (LLVMConst -> m Double) -> m LLVMConst -> m Double
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
a
              Double
b' <- LLVMConst -> m Double
forall (m :: Type -> Type).
MonadError [Char] m =>
LLVMConst -> m Double
asDouble (LLVMConst -> m Double) -> m LLVMConst -> m Double
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
b
              LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ FCmpOp -> Double -> Double -> LLVMConst
forall a. RealFloat a => FCmpOp -> a -> a -> LLVMConst
evalFcmp FCmpOp
op Double
a' Double
b'
         MemType
_ -> [Char] -> m LLVMConst
forall a. [Char] -> m a
badExp [Char]
"Expected floating point arguments"

  L.ConstICmp ICmpOp
op Typed Value
a Typed Value
b ->
    do MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType (Typed Value -> Type
forall a. Typed a -> Type
L.typedType Typed Value
a)
       case MemType
mt of
         VecType Natural
n (IntType Natural
m)
           | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr Natural
m
           , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
           -> do [BV x]
a' <- Natural -> (LLVMConst -> m (BV x)) -> LLVMConst -> m [BV x]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w) (LLVMConst -> m [BV x]) -> m LLVMConst -> m [BV x]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
a
                 [BV x]
b' <- Natural -> (LLVMConst -> m (BV x)) -> LLVMConst -> m [BV x]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w) (LLVMConst -> m [BV x]) -> m LLVMConst -> m [BV x]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
b
                 LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ MemType -> [LLVMConst] -> LLVMConst
VectorConst (Natural -> MemType
IntType Natural
1) ([LLVMConst] -> LLVMConst) -> [LLVMConst] -> LLVMConst
forall a b. (a -> b) -> a -> b
$ (BV x -> BV x -> LLVMConst) -> [BV x] -> [BV x] -> [LLVMConst]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (ICmpOp -> NatRepr x -> BV x -> BV x -> LLVMConst
forall (w :: Natural).
(1 <= w) =>
ICmpOp -> NatRepr w -> BV w -> BV w -> LLVMConst
evalIcmp ICmpOp
op NatRepr x
w) [BV x]
a' [BV x]
b'
         IntType Natural
m
           | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr Natural
m
           , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
           -> do BV x
a' <- NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w (LLVMConst -> m (BV x)) -> m LLVMConst -> m (BV x)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
a
                 BV x
b' <- NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w (LLVMConst -> m (BV x)) -> m LLVMConst -> m (BV x)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
b
                 LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMConst -> m LLVMConst) -> LLVMConst -> m LLVMConst
forall a b. (a -> b) -> a -> b
$ ICmpOp -> NatRepr x -> BV x -> BV x -> LLVMConst
forall (w :: Natural).
(1 <= w) =>
ICmpOp -> NatRepr w -> BV w -> BV w -> LLVMConst
evalIcmp ICmpOp
op NatRepr x
w BV x
a' BV x
b'
         MemType
_ -> [Char] -> m LLVMConst
forall a. [Char] -> m a
badExp [Char]
"Expected integer arguments"

  L.ConstArith ArithOp
op (L.Typed Type
tp Value
a) Value
b ->
    do MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
tp
       case MemType
mt of
          VecType Natural
n MemType
tp' ->
            do [Arith]
a' <- Natural -> (LLVMConst -> m Arith) -> LLVMConst -> m [Arith]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (MemType -> LLVMConst -> m Arith
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> LLVMConst -> m Arith
asArith MemType
tp') (LLVMConst -> m [Arith]) -> m LLVMConst -> m [Arith]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
a
               [Arith]
b' <- Natural -> (LLVMConst -> m Arith) -> LLVMConst -> m [Arith]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (MemType -> LLVMConst -> m Arith
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> LLVMConst -> m Arith
asArith MemType
tp') (LLVMConst -> m [Arith]) -> m LLVMConst -> m [Arith]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
b
               MemType -> [LLVMConst] -> LLVMConst
VectorConst MemType
tp' ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arith -> Arith -> m LLVMConst)
-> [Arith] -> [Arith] -> m [LLVMConst]
forall (m :: Type -> Type) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (ArithOp -> MemType -> Arith -> Arith -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
ArithOp -> MemType -> Arith -> Arith -> m LLVMConst
evalArith ArithOp
op MemType
tp') [Arith]
a' [Arith]
b'
          MemType
tp' ->
            do Arith
a' <- MemType -> LLVMConst -> m Arith
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> LLVMConst -> m Arith
asArith MemType
tp' (LLVMConst -> m Arith) -> m LLVMConst -> m Arith
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
a
               Arith
b' <- MemType -> LLVMConst -> m Arith
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> LLVMConst -> m Arith
asArith MemType
tp' (LLVMConst -> m Arith) -> m LLVMConst -> m Arith
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
b
               ArithOp -> MemType -> Arith -> Arith -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
ArithOp -> MemType -> Arith -> Arith -> m LLVMConst
evalArith ArithOp
op MemType
tp' Arith
a' Arith
b'

  L.ConstUnaryArith UnaryArithOp
op (L.Typed Type
tp Value
a) ->
    do MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
tp
       case MemType
mt of
          VecType Natural
n MemType
tp' ->
            do [Arith]
a' <- Natural -> (LLVMConst -> m Arith) -> LLVMConst -> m [Arith]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (MemType -> LLVMConst -> m Arith
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> LLVMConst -> m Arith
asArith MemType
tp') (LLVMConst -> m [Arith]) -> m LLVMConst -> m [Arith]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
a
               MemType -> [LLVMConst] -> LLVMConst
VectorConst MemType
tp' ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arith -> m LLVMConst) -> [Arith] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (UnaryArithOp -> MemType -> Arith -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
UnaryArithOp -> MemType -> Arith -> m LLVMConst
evalUnaryArith UnaryArithOp
op MemType
tp') [Arith]
a'
          MemType
tp' ->
            do Arith
a' <- MemType -> LLVMConst -> m Arith
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> LLVMConst -> m Arith
asArith MemType
tp' (LLVMConst -> m Arith) -> m LLVMConst -> m Arith
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
a
               UnaryArithOp -> MemType -> Arith -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(MonadError [Char] m, HasPtrWidth wptr) =>
UnaryArithOp -> MemType -> Arith -> m LLVMConst
evalUnaryArith UnaryArithOp
op MemType
tp' Arith
a'

  L.ConstBit BitOp
op (L.Typed Type
tp Value
a) Value
b ->
    do MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
tp
       case MemType
mt of
         VecType Natural
n (IntType Natural
m)
           | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr Natural
m
           , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
           -> do [BV x]
a' <- Natural -> (LLVMConst -> m (BV x)) -> LLVMConst -> m [BV x]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w) (LLVMConst -> m [BV x]) -> m LLVMConst -> m [BV x]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
a
                 [BV x]
b' <- Natural -> (LLVMConst -> m (BV x)) -> LLVMConst -> m [BV x]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n (NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w) (LLVMConst -> m [BV x]) -> m LLVMConst -> m [BV x]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
b
                 MemType -> [LLVMConst] -> LLVMConst
VectorConst (Natural -> MemType
IntType Natural
m) ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (BV x -> BV x -> m LLVMConst) -> [BV x] -> [BV x] -> m [LLVMConst]
forall (m :: Type -> Type) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (BitOp -> NatRepr x -> BV x -> BV x -> m LLVMConst
forall (w :: Natural) (m :: Type -> Type).
(1 <= w, MonadError [Char] m) =>
BitOp -> NatRepr w -> BV w -> BV w -> m LLVMConst
evalBitwise BitOp
op NatRepr x
w) [BV x]
a' [BV x]
b'
         IntType Natural
m
           | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr Natural
m
           , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
           -> do BV x
a' <- NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w (LLVMConst -> m (BV x)) -> m LLVMConst -> m (BV x)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
a
                 BV x
b' <- NatRepr x -> LLVMConst -> m (BV x)
forall (m :: Type -> Type) (w :: Natural).
MonadError [Char] m =>
NatRepr w -> LLVMConst -> m (BV w)
asBV NatRepr x
w (LLVMConst -> m (BV x)) -> m LLVMConst -> m (BV x)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt Value
b
                 BitOp -> NatRepr x -> BV x -> BV x -> m LLVMConst
forall (w :: Natural) (m :: Type -> Type).
(1 <= w, MonadError [Char] m) =>
BitOp -> NatRepr w -> BV w -> BV w -> m LLVMConst
evalBitwise BitOp
op NatRepr x
w BV x
a' BV x
b'
         MemType
_ -> [Char] -> m LLVMConst
forall a. [Char] -> m a
badExp [Char]
"Expected integer arguments"

  L.ConstConv ConvOp
L.BitCast (L.Typed Type
tp Value
x) Type
outty ->
   do MemType
toty <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
outty
      MemType
xty  <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
tp
      LLVMConst
x' <- MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
xty Value
x
      ConstExpr' BlockLabel
-> MemType -> LLVMConst -> MemType -> m LLVMConst
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
ConstExpr' BlockLabel
-> MemType -> LLVMConst -> MemType -> m LLVMConst
evalBitCast ConstExpr' BlockLabel
expr MemType
xty LLVMConst
x' MemType
toty

  L.ConstConv ConvOp
op Typed Value
x Type
outty ->
    do MemType
mt <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
outty
       LLVMConst
x' <- Typed Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
Typed Value -> m LLVMConst
transConstant Typed Value
x
       case MemType
mt of
         VecType Natural
n MemType
mt' ->
           do [LLVMConst]
xs <- Natural -> (LLVMConst -> m LLVMConst) -> LLVMConst -> m [LLVMConst]
forall (m :: Type -> Type) a.
MonadError [Char] m =>
Natural -> (LLVMConst -> m a) -> LLVMConst -> m [a]
asVectorOf Natural
n LLVMConst -> m LLVMConst
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LLVMConst
x'
              MemType -> [LLVMConst] -> LLVMConst
VectorConst MemType
mt' ([LLVMConst] -> LLVMConst) -> m [LLVMConst] -> m LLVMConst
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (LLVMConst -> m LLVMConst) -> [LLVMConst] -> m [LLVMConst]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (ConstExpr' BlockLabel
-> ConvOp -> MemType -> LLVMConst -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
ConstExpr' BlockLabel
-> ConvOp -> MemType -> LLVMConst -> m LLVMConst
evalConv ConstExpr' BlockLabel
expr ConvOp
op MemType
mt') [LLVMConst]
xs

         MemType
_ -> ConstExpr' BlockLabel
-> ConvOp -> MemType -> LLVMConst -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
ConstExpr' BlockLabel
-> ConvOp -> MemType -> LLVMConst -> m LLVMConst
evalConv ConstExpr' BlockLabel
expr ConvOp
op MemType
mt LLVMConst
x'

 where
 badExp :: String -> m a
 badExp :: forall a. [Char] -> m a
badExp [Char]
msg = [Char] -> m a
forall a. [Char] -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m a) -> [Char] -> m a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [[Char]
msg, ConstExpr' BlockLabel -> [Char]
forall a. Show a => a -> [Char]
show ConstExpr' BlockLabel
expr]

testBreakpointFunction :: String -> Bool
testBreakpointFunction :: [Char] -> Bool
testBreakpointFunction = [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [Char]
"__breakpoint__"