{-# 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
(
LLVMConst(..)
, boolConst
, intConst
, transConstant
, transConstantWithType
, transConstant'
, transConstantExpr
, GEP(..)
, GEPResult(..)
, translateGEP
, 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
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))
data GEP (n :: Nat) (expr :: Type) where
GEP_scalar_base :: expr -> GEP 1 expr
GEP_vector_base :: NatRepr n -> expr -> GEP n expr
GEP_scatter :: NatRepr n -> GEP 1 expr -> GEP n expr
GEP_field :: FieldInfo -> GEP n expr -> GEP n expr
GEP_index_each :: MemType -> GEP n expr -> expr -> GEP n expr
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
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
translateGEP :: forall wptr m.
(?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
Bool ->
L.Type ->
L.Typed L.Value ->
[L.Typed L.Value] ->
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)
case MemType
mt of
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
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) ]
go ::
(1 <= lanes) =>
NatRepr lanes ->
MemType ->
GEP lanes (L.Typed L.Value) ->
[L.Typed L.Value] ->
m (GEPResult (L.Typed L.Value))
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)
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)
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
goArray ::
(1 <= lanes) =>
NatRepr lanes ->
L.Typed L.Value ->
MemType ->
MemType ->
GEP lanes (L.Typed L.Value) ->
[L.Typed L.Value] ->
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
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
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
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
MemType
_ -> m (GEPResult (Typed Value))
forall a. m a
badGEP
goStruct ::
(1 <= lanes) =>
NatRepr lanes ->
L.Typed L.Value ->
MemType ->
StructInfo ->
GEP lanes (L.Typed L.Value) ->
[L.Typed L.Value] ->
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
ZeroConst (IntType Natural
_) -> Integer -> m (GEPResult (Typed Value))
goidx Integer
0
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)
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
LLVMConst
_ -> m (GEPResult (Typed Value))
forall a. m a
badGEP
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
data LLVMConst where
ZeroConst :: !MemType -> LLVMConst
IntConst :: (1 <= w) => !(NatRepr w) -> !(BV.BV w) -> LLVMConst
FloatConst :: !Float -> LLVMConst
DoubleConst :: !Double -> LLVMConst
LongDoubleConst :: !L.FP80Value -> LLVMConst
StringConst :: !ByteString -> LLVMConst
ArrayConst :: !MemType -> [LLVMConst] -> LLVMConst
VectorConst :: !MemType -> [LLVMConst] -> LLVMConst
StructConst :: !StructInfo -> [LLVMConst] -> LLVMConst
SymbolConst :: !L.Symbol -> !Integer -> LLVMConst
UndefConst :: !MemType -> LLVMConst
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]
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
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)
intConst ::
MonadError String m =>
Natural ->
Integer ->
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)
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
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)
]
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
]
go :: GEP n LLVMConst -> m [LLVMConst]
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]
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
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"
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
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
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
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
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
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"
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"
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"
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)
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"
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"
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
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 ->
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]
evalBitCast ::
(?lc :: TypeContext, MonadError String m) =>
L.ConstExpr ->
MemType ->
LLVMConst ->
MemType ->
m LLVMConst
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)
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
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
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)
data ArithInt where
ArithInt :: Integer -> ArithInt
ArithPtr :: L.Symbol -> Integer -> ArithInt
data Arith where
ArithI :: ArithInt -> Arith
ArithF :: Float -> Arith
ArithD :: Double -> Arith
asArithInt ::
(MonadError String m, HasPtrWidth wptr) =>
Natural ->
LLVMConst ->
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 ->
LLVMConst ->
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 ->
LLVMConst ->
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 ->
LLVMConst ->
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 ->
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 ->
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"
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 ->
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__"