{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.LLVM.Translation.Expr
( LLVMExpr(..)
, ScalarView(..)
, asScalar
, asVectorWithType
, asVector
, pattern PointerExpr
, pattern BitvectorAsPointerExpr
, pointerAsBitvectorExpr
, unpackOne
, unpackVec
, unpackArgs
, zeroExpand
, undefExpand
, explodeVector
, constToLLVMVal
, transValue
, transTypedValue
, transTypeAndValue
, liftConstant
, callIsNull
, callIntToBool
, callAlloca
, callPushFrame
, callPopFrame
, callPtrAddOffset
, callPtrSubtract
, callLoad
, callStore
) where
import Control.Lens hiding ((:>))
import Control.Monad
import Control.Monad.Except
import qualified Data.ByteString as BS
import Data.Foldable (toList)
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.String
import qualified Data.Vector as V
import Numeric.Natural
import GHC.Exts ( Proxy#, proxy# )
import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Context ( pattern (:>) )
import Data.Parameterized.NatRepr as NatRepr
import Data.Parameterized.Some
import Data.Text (Text)
import qualified Text.LLVM.AST as L
import qualified Lang.Crucible.CFG.Core as C
import Lang.Crucible.CFG.Expr
import Lang.Crucible.CFG.Generator
import Lang.Crucible.CFG.Extension ()
import Lang.Crucible.LLVM.DataLayout
import Lang.Crucible.LLVM.Extension
import Lang.Crucible.LLVM.MemType
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.Translation.Constant
import Lang.Crucible.LLVM.Translation.Monad
import Lang.Crucible.LLVM.Translation.Types
import Lang.Crucible.LLVM.TypeContext
import Lang.Crucible.Syntax
import Lang.Crucible.Types
import What4.InterpretedFloatingPoint (X86_80Val(..))
data LLVMExpr s (arch :: LLVMArch) where
BaseExpr :: TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
ZeroExpr :: MemType -> LLVMExpr s arch
UndefExpr :: MemType -> LLVMExpr s arch
VecExpr :: MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
StructExpr :: Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
instance Show (LLVMExpr s arch) where
show :: LLVMExpr s arch -> String
show (BaseExpr TypeRepr tp
ty Expr LLVM s tp
x) = Expr LLVM s tp -> String
forall k (f :: k -> Type) (tp :: k). ShowF f => f tp -> String
forall (tp :: CrucibleType). Expr LLVM s tp -> String
C.showF Expr LLVM s tp
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
ty
show (ZeroExpr MemType
mt) = String
"<zero :" String -> ShowS
forall a. [a] -> [a] -> [a]
++ MemType -> String
forall a. Show a => a -> String
show MemType
mt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
show (UndefExpr MemType
mt) = String
"<undef :" String -> ShowS
forall a. [a] -> [a] -> [a]
++ MemType -> String
forall a. Show a => a -> String
show MemType
mt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
show (VecExpr MemType
_mt Seq (LLVMExpr s arch)
xs) = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ((LLVMExpr s arch -> String) -> [LLVMExpr s arch] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map LLVMExpr s arch -> String
forall a. Show a => a -> String
show (Seq (LLVMExpr s arch) -> [LLVMExpr s arch]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (LLVMExpr s arch)
xs)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
show (StructExpr Seq (MemType, LLVMExpr s arch)
xs) = String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " (((MemType, LLVMExpr s arch) -> String)
-> [(MemType, LLVMExpr s arch)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (MemType, LLVMExpr s arch) -> String
forall {a} {a}. Show a => (a, a) -> String
f (Seq (MemType, LLVMExpr s arch) -> [(MemType, LLVMExpr s arch)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (MemType, LLVMExpr s arch)
xs)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
where f :: (a, a) -> String
f (a
_mt,a
x) = a -> String
forall a. Show a => a -> String
show a
x
data ScalarView s (arch :: LLVMArch) where
Scalar :: Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
NotScalar :: ScalarView s arch
asScalar :: (?lc :: TypeContext, HasPtrWidth (ArchWidth arch))
=> LLVMExpr s arch
-> ScalarView s arch
asScalar :: forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar (BaseExpr TypeRepr tp
tp Expr LLVM s tp
xs)
= Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
forall (arch :: LLVMArch) (tp :: CrucibleType) s.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
Scalar Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr tp
tp Expr LLVM s tp
xs
asScalar (ZeroExpr MemType
llvmtp)
= let ?err = ?err::String -> ScalarView s arch
String -> ScalarView s arch
forall a. HasCallStack => String -> a
error
in Proxy# arch
-> MemType
-> (forall {tp :: CrucibleType}.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
zeroExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
llvmtp ((forall {tp :: CrucibleType}.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch)
-> (forall {tp :: CrucibleType}.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex -> Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
forall (arch :: LLVMArch) (tp :: CrucibleType) s.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
Scalar Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex
asScalar (UndefExpr MemType
llvmtp)
= let ?err = ?err::String -> ScalarView s arch
String -> ScalarView s arch
forall a. HasCallStack => String -> a
error
in Proxy# arch
-> MemType
-> (forall {tp :: CrucibleType}.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
undefExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
llvmtp ((forall {tp :: CrucibleType}.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch)
-> (forall {tp :: CrucibleType}.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex -> Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
forall (arch :: LLVMArch) (tp :: CrucibleType) s.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
Scalar Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex
asScalar LLVMExpr s arch
_ = ScalarView s arch
forall s (arch :: LLVMArch). ScalarView s arch
NotScalar
asVectorWithType :: LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
asVectorWithType :: forall s (arch :: LLVMArch).
LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
asVectorWithType LLVMExpr s arch
v =
case LLVMExpr s arch
v of
ZeroExpr (VecType Natural
n MemType
t) -> (MemType, Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. a -> Maybe a
Just (MemType
t, Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
t))
UndefExpr (VecType Natural
n MemType
t) -> (MemType, Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. a -> Maybe a
Just (MemType
t, Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
t))
VecExpr MemType
t Seq (LLVMExpr s arch)
s -> (MemType, Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. a -> Maybe a
Just (MemType
t, Seq (LLVMExpr s arch)
s)
LLVMExpr s arch
_ -> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. Maybe a
Nothing
asVector :: LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
asVector :: forall s (arch :: LLVMArch).
LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
asVector = ((MemType, Seq (LLVMExpr s arch)) -> Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
-> Maybe (Seq (LLVMExpr s arch))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (MemType, Seq (LLVMExpr s arch)) -> Seq (LLVMExpr s arch)
forall a b. (a, b) -> b
snd (Maybe (MemType, Seq (LLVMExpr s arch))
-> Maybe (Seq (LLVMExpr s arch)))
-> (LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch)))
-> LLVMExpr s arch
-> Maybe (Seq (LLVMExpr s arch))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
forall s (arch :: LLVMArch).
LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
asVectorWithType
nullPointerExpr :: (HasPtrWidth w) => Expr LLVM s (LLVMPointerType w)
nullPointerExpr :: forall (w :: Natural) s.
HasPtrWidth w =>
Expr LLVM s (LLVMPointerType w)
nullPointerExpr = NatRepr w
-> Expr LLVM s NatType
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s NatType
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
PointerExpr NatRepr w
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (App LLVM (Expr LLVM s) NatType -> Expr LLVM s NatType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Natural -> App LLVM (Expr LLVM s) NatType
forall ext (f :: CrucibleType -> Type).
Natural -> App ext f NatType
NatLit Natural
0)) (App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w -> BV w -> App LLVM (Expr LLVM s) (BVType w)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr w
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth)))
pattern PointerExpr
:: (1 <= w)
=> NatRepr w
-> Expr LLVM s NatType
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
pattern $mPointerExpr :: forall {r} {w :: Natural} {s}.
(1 <= w) =>
Expr LLVM s (LLVMPointerType w)
-> (NatRepr w
-> Expr LLVM s NatType -> Expr LLVM s (BVType w) -> r)
-> ((# #) -> r)
-> r
$bPointerExpr :: forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s NatType
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
PointerExpr w blk off = App (ExtensionApp (LLVM_PointerExpr w blk off))
pattern BitvectorAsPointerExpr
:: (1 <= w)
=> NatRepr w
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
pattern $mBitvectorAsPointerExpr :: forall {r} {w :: Natural} {s}.
(1 <= w) =>
Expr LLVM s (LLVMPointerType w)
-> (NatRepr w -> Expr LLVM s (BVType w) -> r) -> ((# #) -> r) -> r
$bBitvectorAsPointerExpr :: forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr w ex = PointerExpr w (App (NatLit 0)) ex
pointerAsBitvectorExpr
:: (1 <= w)
=> NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType w))
pointerAsBitvectorExpr :: forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType w))
pointerAsBitvectorExpr NatRepr w
_ (BitvectorAsPointerExpr NatRepr w
_ Expr LLVM s (BVType w)
ex) =
Expr LLVM s (BVType w)
-> Generator
LLVM s (LLVMState arch) ret IO (Expr LLVM s (BVType w))
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s (BVType w)
ex
pointerAsBitvectorExpr NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex =
do Expr LLVM s (LLVMPointerType w)
ex' <- Expr LLVM s (LLVMPointerType w)
-> Generator
LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType w))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation Expr LLVM s (LLVMPointerType w)
ex
let blk :: Expr LLVM s NatType
blk = App LLVM (Expr LLVM s) NatType -> Expr LLVM s NatType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) NatType
-> App LLVM (Expr LLVM s) NatType
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) NatType
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> a (LLVMPointerType w) -> LLVMExtensionExpr a NatType
LLVM_PointerBlock NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
let off :: Expr LLVM s (BVType w)
off = App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) (BVType w)
-> App LLVM (Expr LLVM s) (BVType w)
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) (BVType w)
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w
-> a (LLVMPointerType w)
-> LLVMExtensionExpr a ('BaseToType (BaseBVType w))
LLVM_PointerOffset NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
Expr LLVM s BoolType
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
assertExpr (Expr LLVM s NatType
blk Expr LLVM s NatType -> Expr LLVM s NatType -> Expr LLVM s BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(EqExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
.== Natural -> Expr LLVM s NatType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Natural
0)
(Text -> Expr LLVM s (StringType Unicode)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Text
"Expected bitvector, but found pointer")
Expr LLVM s (BVType w)
-> Generator
LLVM s (LLVMState arch) ret IO (Expr LLVM s (BVType w))
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s (BVType w)
off
unpackArgs :: forall s a arch
. (?err :: String -> a
,HasPtrWidth (ArchWidth arch)
)
=> [LLVMExpr s arch]
-> (forall ctx. Proxy# arch -> CtxRepr ctx -> Ctx.Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs :: forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs = CtxRepr EmptyCtx
-> Assignment (Expr LLVM s) EmptyCtx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx
-> Assignment (Expr LLVM s) ctx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
go CtxRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment (Expr LLVM s) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
where go :: CtxRepr ctx
-> Ctx.Assignment (Expr LLVM s) ctx
-> [LLVMExpr s arch]
-> (forall ctx'. Proxy# arch -> CtxRepr ctx' -> Ctx.Assignment (Expr LLVM s) ctx' -> a)
-> a
go :: forall (ctx :: Ctx CrucibleType).
CtxRepr ctx
-> Assignment (Expr LLVM s) ctx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
go CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn [] forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k = Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn
go CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn (LLVMExpr s arch
v:[LLVMExpr s arch]
vs) forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k = LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne LLVMExpr s arch
v (\Proxy# arch
_ TypeRepr tpr
tyr Expr LLVM s tpr
ex -> CtxRepr (ctx ::> tpr)
-> Assignment (Expr LLVM s) (ctx ::> tpr)
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx
-> Assignment (Expr LLVM s) ctx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
go (CtxRepr ctx
ctx CtxRepr ctx -> TypeRepr tpr -> CtxRepr (ctx ::> tpr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> TypeRepr tpr
tyr) (Assignment (Expr LLVM s) ctx
asgn Assignment (Expr LLVM s) ctx
-> Expr LLVM s tpr -> Assignment (Expr LLVM s) (ctx ::> tpr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr LLVM s tpr
ex) [LLVMExpr s arch]
vs Proxy# arch -> CtxRepr ctx' -> Assignment (Expr LLVM s) ctx' -> a
forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k)
unpackOne
:: (?err :: String -> a, HasPtrWidth (ArchWidth arch))
=> LLVMExpr s arch
-> (forall tpr. Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne :: forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne (BaseExpr TypeRepr tp
tyr Expr LLVM s tp
ex) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k = Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr tp
tyr Expr LLVM s tp
ex
unpackOne (UndefExpr MemType
tp) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k = Proxy# arch
-> MemType
-> (forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
undefExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
tp Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k
unpackOne (ZeroExpr MemType
tp) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k = Proxy# arch
-> MemType
-> (forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
zeroExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
tp Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k
unpackOne (StructExpr Seq (MemType, LLVMExpr s arch)
vs) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k =
[LLVMExpr s arch]
-> (forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs (((MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> [(MemType, LLVMExpr s arch)] -> [LLVMExpr s arch]
forall a b. (a -> b) -> [a] -> [b]
map (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a, b) -> b
snd ([(MemType, LLVMExpr s arch)] -> [LLVMExpr s arch])
-> [(MemType, LLVMExpr s arch)] -> [LLVMExpr s arch]
forall a b. (a -> b) -> a -> b
$ Seq (MemType, LLVMExpr s arch) -> [(MemType, LLVMExpr s arch)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (MemType, LLVMExpr s arch)
vs) ((forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a)
-> (forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy CtxRepr ctx
struct_ctx Assignment (Expr LLVM s) ctx
struct_asgn ->
Proxy# arch
-> TypeRepr ('StructType ctx) -> Expr LLVM s ('StructType ctx) -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k Proxy# arch
archProxy (CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
struct_ctx) (CtxRepr ctx
-> Assignment (Expr LLVM s) ctx -> Expr LLVM s ('StructType ctx)
forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
IsExpr e =>
CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
mkStruct CtxRepr ctx
struct_ctx Assignment (Expr LLVM s) ctx
struct_asgn)
unpackOne (VecExpr MemType
tp Seq (LLVMExpr s arch)
vs) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k =
MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr tp
tpr (Seq (LLVMExpr s arch) -> [LLVMExpr s arch]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (LLVMExpr s arch)
vs) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
unpackVec :: forall tpr s arch a
. ( ?err :: String -> a
, HasPtrWidth (ArchWidth arch)
)
=> Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec :: forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
_archProxy TypeRepr tpr
tpr = [Expr LLVM s tpr]
-> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
go [] ([LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a)
-> ([LLVMExpr s arch] -> [LLVMExpr s arch])
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LLVMExpr s arch] -> [LLVMExpr s arch]
forall a. [a] -> [a]
reverse
where go :: [Expr LLVM s tpr] -> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
go :: [Expr LLVM s tpr]
-> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
go [Expr LLVM s tpr]
vs [] Expr LLVM s (VectorType tpr) -> a
k = Expr LLVM s (VectorType tpr) -> a
k (TypeRepr tpr
-> Vector (Expr LLVM s tpr) -> Expr LLVM s (VectorType tpr)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
TypeRepr tp -> Vector (e tp) -> e (VectorType tp)
vectorLit TypeRepr tpr
tpr (Vector (Expr LLVM s tpr) -> Expr LLVM s (VectorType tpr))
-> Vector (Expr LLVM s tpr) -> Expr LLVM s (VectorType tpr)
forall a b. (a -> b) -> a -> b
$ [Expr LLVM s tpr] -> Vector (Expr LLVM s tpr)
forall a. [a] -> Vector a
V.fromList [Expr LLVM s tpr]
vs)
go [Expr LLVM s tpr]
vs (LLVMExpr s arch
x:[LLVMExpr s arch]
xs) Expr LLVM s (VectorType tpr) -> a
k = LLVMExpr s arch
-> (forall {tpr :: CrucibleType}.
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne LLVMExpr s arch
x ((forall {tpr :: CrucibleType}.
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a)
-> (forall {tpr :: CrucibleType}.
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
_archProxy' TypeRepr tpr
tpr' Expr LLVM s tpr
v ->
case TypeRepr tpr -> TypeRepr tpr -> Maybe (tpr :~: tpr)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tpr
tpr TypeRepr tpr
tpr' of
Just tpr :~: tpr
Refl -> [Expr LLVM s tpr]
-> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
go (Expr LLVM s tpr
Expr LLVM s tpr
vExpr LLVM s tpr -> [Expr LLVM s tpr] -> [Expr LLVM s tpr]
forall a. a -> [a] -> [a]
:[Expr LLVM s tpr]
vs) [LLVMExpr s arch]
xs Expr LLVM s (VectorType tpr) -> a
k
Maybe (tpr :~: tpr)
Nothing -> ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"type mismatch in array value", TypeRepr tpr -> String
forall a. Show a => a -> String
show TypeRepr tpr
tpr, TypeRepr tpr -> String
forall a. Show a => a -> String
show TypeRepr tpr
tpr']
zeroExpand :: (?err :: String -> a, HasPtrWidth (ArchWidth arch))
=> Proxy# arch
-> MemType
-> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
zeroExpand :: forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
zeroExpand Proxy# arch
_proxyArch (IntType Natural
w) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
case Natural -> Some NatRepr
mkNatRepr Natural
w of
Some NatRepr x
w' | Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w' ->
Proxy# arch
-> TypeRepr (LLVMPointerType x)
-> Expr LLVM s (LLVMPointerType x)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (NatRepr x -> TypeRepr (LLVMPointerType x)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr x
w') (Expr LLVM s (LLVMPointerType x) -> a)
-> Expr LLVM s (LLVMPointerType x) -> a
forall a b. (a -> b) -> a -> b
$
NatRepr x
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr x
w' (Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x))
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall a b. (a -> b) -> a -> b
$
App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x))
-> App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> App LLVM (Expr LLVM s) (BVType x)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr x
w' (NatRepr x -> BV x
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
w')
Some NatRepr
_ -> ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"illegal integer size", Natural -> String
forall a. Show a => a -> String
show Natural
w]
zeroExpand Proxy# arch
_proxyArch (StructType StructInfo
si) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
[LLVMExpr s arch]
-> (forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs ((MemType -> LLVMExpr s arch) -> [MemType] -> [LLVMExpr s arch]
forall a b. (a -> b) -> [a] -> [b]
map MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr [MemType]
tps) ((forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a)
-> (forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn -> Proxy# arch
-> TypeRepr ('StructType ctx) -> Expr LLVM s ('StructType ctx) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
archProxy (CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
ctx) (CtxRepr ctx
-> Assignment (Expr LLVM s) ctx -> Expr LLVM s ('StructType ctx)
forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
IsExpr e =>
CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
mkStruct CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn)
where tps :: [MemType]
tps = (FieldInfo -> MemType) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map FieldInfo -> MemType
fiType ([FieldInfo] -> [MemType]) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> a -> b
$ Vector FieldInfo -> [FieldInfo]
forall a. Vector a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Vector FieldInfo -> [FieldInfo])
-> Vector FieldInfo -> [FieldInfo]
forall a b. (a -> b) -> a -> b
$ StructInfo -> Vector FieldInfo
siFields StructInfo
si
zeroExpand Proxy# arch
proxyArch (ArrayType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
proxyArch TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
zeroExpand Proxy# arch
proxyArch (VecType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
proxyArch TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
zeroExpand Proxy# arch
proxyArch (PtrType SymType
_tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k = Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
HasPtrWidth w =>
Expr LLVM s (LLVMPointerType w)
nullPointerExpr
zeroExpand Proxy# arch
proxyArch MemType
PtrOpaqueType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k = Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
HasPtrWidth w =>
Expr LLVM s (LLVMPointerType w)
nullPointerExpr
zeroExpand Proxy# arch
proxyArch MemType
FloatType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k = Proxy# arch
-> TypeRepr ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (FloatInfoRepr 'SingleFloat -> TypeRepr ('FloatType 'SingleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'SingleFloat
SingleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Float -> App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
forall ext (f :: CrucibleType -> Type).
Float -> App ext f ('FloatType 'SingleFloat)
FloatLit Float
0))
zeroExpand Proxy# arch
proxyArch MemType
DoubleType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k = Proxy# arch
-> TypeRepr ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (FloatInfoRepr 'DoubleFloat -> TypeRepr ('FloatType 'DoubleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'DoubleFloat
DoubleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Double -> App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
forall ext (f :: CrucibleType -> Type).
Double -> App ext f ('FloatType 'DoubleFloat)
DoubleLit Double
0))
zeroExpand Proxy# arch
_prxyArch MemType
X86_FP80Type forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
_ = ?err::String -> a
String -> a
?err String
"Cannot zero expand x86_fp80 values"
zeroExpand Proxy# arch
_prxyArch MemType
MetadataType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
_ = ?err::String -> a
String -> a
?err String
"Cannot zero expand metadata"
undefExpand :: ( ?err :: String -> a
, HasPtrWidth (ArchWidth arch)
)
=> Proxy# arch
-> MemType
-> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
undefExpand :: forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
undefExpand Proxy# arch
_archProxy (IntType Natural
w) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
case Natural -> Some NatRepr
mkNatRepr Natural
w of
Some NatRepr x
w' | Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w' ->
Proxy# arch
-> TypeRepr (LLVMPointerType x)
-> Expr LLVM s (LLVMPointerType x)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (NatRepr x -> TypeRepr (LLVMPointerType x)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr x
w') (Expr LLVM s (LLVMPointerType x) -> a)
-> Expr LLVM s (LLVMPointerType x) -> a
forall a b. (a -> b) -> a -> b
$
NatRepr x
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr x
w' (Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x))
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall a b. (a -> b) -> a -> b
$
App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x))
-> App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall a b. (a -> b) -> a -> b
$ NatRepr x -> App LLVM (Expr LLVM s) (BVType x)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> App ext f ('BaseToType (BaseBVType w))
BVUndef NatRepr x
w'
Some NatRepr
_ -> ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"illegal integer size", Natural -> String
forall a. Show a => a -> String
show Natural
w]
undefExpand Proxy# arch
_archProxy (PtrType SymType
_tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr (Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a)
-> Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch)))
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch)))
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> App ext f ('BaseToType (BaseBVType w))
BVUndef NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth
undefExpand Proxy# arch
_archProxy MemType
PtrOpaqueType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr (Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a)
-> Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch)))
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch)))
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> App ext f ('BaseToType (BaseBVType w))
BVUndef NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth
undefExpand Proxy# arch
_archProxy (StructType StructInfo
si) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
[LLVMExpr s arch]
-> (forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs ((MemType -> LLVMExpr s arch) -> [MemType] -> [LLVMExpr s arch]
forall a b. (a -> b) -> [a] -> [b]
map MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr [MemType]
tps) ((forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a)
-> (forall {ctx :: Ctx CrucibleType}.
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn -> Proxy# arch
-> TypeRepr ('StructType ctx) -> Expr LLVM s ('StructType ctx) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
archProxy (CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
ctx) (CtxRepr ctx
-> Assignment (Expr LLVM s) ctx -> Expr LLVM s ('StructType ctx)
forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
IsExpr e =>
CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
mkStruct CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn)
where tps :: [MemType]
tps = (FieldInfo -> MemType) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map FieldInfo -> MemType
fiType ([FieldInfo] -> [MemType]) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> a -> b
$ Vector FieldInfo -> [FieldInfo]
forall a. Vector a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Vector FieldInfo -> [FieldInfo])
-> Vector FieldInfo -> [FieldInfo]
forall a b. (a -> b) -> a -> b
$ StructInfo -> Vector FieldInfo
siFields StructInfo
si
undefExpand Proxy# arch
archProxy (ArrayType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
archProxy TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
undefExpand Proxy# arch
archProxy (VecType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
archProxy TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
undefExpand Proxy# arch
_archProxy MemType
FloatType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
Proxy# arch
-> TypeRepr ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (FloatInfoRepr 'SingleFloat -> TypeRepr ('FloatType 'SingleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'SingleFloat
SingleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (FloatInfoRepr 'SingleFloat
-> App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type).
FloatInfoRepr fi -> App ext f ('FloatType fi)
FloatUndef FloatInfoRepr 'SingleFloat
SingleFloatRepr))
undefExpand Proxy# arch
_archProxy MemType
DoubleType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
Proxy# arch
-> TypeRepr ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (FloatInfoRepr 'DoubleFloat -> TypeRepr ('FloatType 'DoubleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'DoubleFloat
DoubleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (FloatInfoRepr 'DoubleFloat
-> App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type).
FloatInfoRepr fi -> App ext f ('FloatType fi)
FloatUndef FloatInfoRepr 'DoubleFloat
DoubleFloatRepr))
undefExpand Proxy# arch
_archProxy MemType
X86_FP80Type forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
Proxy# arch
-> TypeRepr ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (FloatInfoRepr 'X86_80Float -> TypeRepr ('FloatType 'X86_80Float)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'X86_80Float
X86_80FloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (FloatInfoRepr 'X86_80Float
-> App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type).
FloatInfoRepr fi -> App ext f ('FloatType fi)
FloatUndef FloatInfoRepr 'X86_80Float
X86_80FloatRepr))
undefExpand Proxy# arch
_archPrxy MemType
tp forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
_ = ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"cannot undef expand type:", MemType -> String
forall a. Show a => a -> String
show MemType
tp]
explodeVector :: Natural -> LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
explodeVector :: forall s (arch :: LLVMArch).
Natural -> LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
explodeVector Natural
n (UndefExpr (VecType Natural
n' MemType
tp)) | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n' = Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
tp))
explodeVector Natural
n (ZeroExpr (VecType Natural
n' MemType
tp)) | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n' = Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
tp))
explodeVector Natural
n (VecExpr MemType
_tp Seq (LLVMExpr s arch)
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 (Seq (LLVMExpr s arch) -> Int
forall a. Seq a -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length Seq (LLVMExpr s arch)
xs) = Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Seq (LLVMExpr s arch)
xs
explodeVector Natural
n (BaseExpr (VectorRepr TypeRepr tp1
tpr) Expr LLVM s tp
v) =
let xs :: [LLVMExpr s arch]
xs = [ TypeRepr tp1 -> Expr LLVM s tp1 -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr tp1
tpr (App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp1 -> Expr LLVM s tp1
forall (tp :: CrucibleType).
App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp -> Expr LLVM s tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp1 -> Expr LLVM s tp1)
-> App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp1 -> Expr LLVM s tp1
forall a b. (a -> b) -> a -> b
$ TypeRepr tp1
-> Expr LLVM s ('VectorType tp1)
-> Expr LLVM s NatType
-> App LLVM (Expr LLVM s) tp1
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp -> f (VectorType tp) -> f NatType -> App ext f tp
VectorGetEntry TypeRepr tp1
tpr Expr LLVM s tp
Expr LLVM s ('VectorType tp1)
v (Natural -> Expr LLVM s NatType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Natural
i)) | Natural
i <- [Natural
0..Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1] ]
in Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
xs)
explodeVector Natural
_ LLVMExpr s arch
_ = Maybe (Seq (LLVMExpr s arch))
forall a. Maybe a
Nothing
liftConstant ::
HasPtrWidth (ArchWidth arch) =>
LLVMConst ->
LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant :: forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c = case LLVMConst
c of
ZeroConst MemType
mt ->
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
mt
UndefConst MemType
mt ->
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
mt
IntConst NatRepr w
w BV w
i ->
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr (LLVMPointerType w)
-> Expr LLVM s (LLVMPointerType w) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (NatRepr w -> TypeRepr (LLVMPointerType w)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr w
w) (NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr w
w (App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w -> BV w -> App LLVM (Expr LLVM s) (BVType w)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr w
w BV w
i)))
FloatConst Float
f ->
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (FloatInfoRepr 'SingleFloat -> TypeRepr ('FloatType 'SingleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'SingleFloat
SingleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Float -> App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
forall ext (f :: CrucibleType -> Type).
Float -> App ext f ('FloatType 'SingleFloat)
FloatLit Float
f))
DoubleConst Double
d ->
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (FloatInfoRepr 'DoubleFloat -> TypeRepr ('FloatType 'DoubleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'DoubleFloat
DoubleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Double -> App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
forall ext (f :: CrucibleType -> Type).
Double -> App ext f ('FloatType 'DoubleFloat)
DoubleLit Double
d))
LongDoubleConst (L.FP80_LongDouble Word16
ex Word64
man) ->
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (FloatInfoRepr 'X86_80Float -> TypeRepr ('FloatType 'X86_80Float)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'X86_80Float
X86_80FloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (X86_80Val -> App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
forall ext (f :: CrucibleType -> Type).
X86_80Val -> App ext f ('FloatType 'X86_80Float)
X86_80Lit (Word16 -> Word64 -> X86_80Val
X86_80Val Word16
ex Word64
man)))
StringConst ByteString
bs ->
do [LLVMExpr s arch]
vs <- (Word8
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [Word8]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
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 (\Word8
b -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (NatRepr 8 -> BV 8 -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word8 -> BV 8
BV.word8 Word8
b))) (ByteString -> [Word8]
BS.unpack ByteString
bs)
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
i8 (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs)
ArrayConst MemType
mt [LLVMConst]
vs ->
do [LLVMExpr s arch]
vs' <- (LLVMConst
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [LLVMConst]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
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 (\LLVMConst
c' -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c') [LLVMConst]
vs
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
mt (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')
VectorConst MemType
mt [LLVMConst]
vs ->
do [LLVMExpr s arch]
vs' <- (LLVMConst
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [LLVMConst]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
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 (\LLVMConst
c' -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c') [LLVMConst]
vs
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
mt (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')
StructConst StructInfo
si [LLVMConst]
vs ->
do [LLVMExpr s arch]
vs' <- (LLVMConst
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [LLVMConst]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
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 (\LLVMConst
c' -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c') [LLVMConst]
vs
let ts :: [MemType]
ts = (FieldInfo -> MemType) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map FieldInfo -> MemType
fiType ([FieldInfo] -> [MemType]) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> a -> b
$ Vector FieldInfo -> [FieldInfo]
forall a. Vector a -> [a]
V.toList (StructInfo -> Vector FieldInfo
siFields StructInfo
si)
Bool
-> Generator LLVM s (LLVMState arch) ret IO ()
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless ([LLVMExpr s arch] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [LLVMExpr s arch]
vs' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [MemType] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [MemType]
ts)
(String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Type mismatch in structure constant")
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
StructExpr ([(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList ([MemType] -> [LLVMExpr s arch] -> [(MemType, LLVMExpr s arch)]
forall a b. [a] -> [b] -> [(a, b)]
zip [MemType]
ts [LLVMExpr s arch]
vs')))
SymbolConst Symbol
sym Integer
0 ->
do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base <- StmtExtension
LLVM
(Expr LLVM s)
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch))))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr (ArchWidth arch)
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
(Expr LLVM s)
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
LLVM_ResolveGlobal ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth GlobalVar Mem
memVar (Symbol -> GlobalSymbol
GlobalSymbol Symbol
sym))
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TypeRepr
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base)
SymbolConst Symbol
sym Integer
off ->
do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base <- StmtExtension
LLVM
(Expr LLVM s)
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch))))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr (ArchWidth arch)
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
(Expr LLVM s)
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
LLVM_ResolveGlobal ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth GlobalVar Mem
memVar (Symbol -> GlobalSymbol
GlobalSymbol Symbol
sym))
let off' :: Expr LLVM s (BVType (ArchWidth arch))
off' = App (ExprExt (Expr LLVM s)) (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall (tp :: CrucibleType).
App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp -> Expr LLVM s tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App
(ExprExt (Expr LLVM s)) (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch)))
-> App
(ExprExt (Expr LLVM s)) (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> BV (ArchWidth arch)
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth (NatRepr (ArchWidth arch) -> Integer -> BV (ArchWidth arch)
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth Integer
off)
Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
ptr <- StmtExtension
LLVM
(Expr LLVM s)
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch))))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr (ArchWidth arch)
-> GlobalVar Mem
-> Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Expr LLVM s (BVType (ArchWidth arch))
-> LLVMStmt
(Expr LLVM s)
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (LLVMPointerType wptr)
-> f (BVType wptr)
-> LLVMStmt f (LLVMPointerType wptr)
LLVM_PtrAddOffset ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth GlobalVar Mem
memVar Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base Expr LLVM s (BVType (ArchWidth arch))
off')
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TypeRepr
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr
LLVM
s
('IntrinsicType
"LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
ptr)
transTypeAndValue ::
L.Typed L.Value ->
LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v =
do let err :: String -> a
err String
msg =
Doc Void -> [Doc Void] -> a
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule
Doc Void
"Invalid value type"
[ String -> Doc Void
forall a. IsString a => String -> a
fromString String
msg ]
MemType
tp <- (String -> Generator LLVM s (LLVMState arch) ret IO MemType)
-> (MemType -> Generator LLVM s (LLVMState arch) ret IO MemType)
-> Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> Generator LLVM s (LLVMState arch) ret IO MemType
forall {a}. String -> a
err MemType -> Generator LLVM s (LLVMState arch) ret IO MemType
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType)
-> Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType
forall a b. (a -> b) -> a -> b
$ Type -> Either String MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError String m) =>
Type -> m MemType
liftMemType (Type -> Either String MemType) -> Type -> Either String MemType
forall a b. (a -> b) -> a -> b
$ Typed Value -> Type
forall a. Typed a -> Type
L.typedType Typed Value
v
(\LLVMExpr s arch
ex -> (MemType
tp, LLVMExpr s arch
ex)) (LLVMExpr s arch -> (MemType, LLVMExpr s arch))
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
-> Generator
LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
tp (Typed Value -> Value
forall a. Typed a -> a
L.typedValue Typed Value
v)
transTypedValue ::
L.Typed L.Value ->
LLVMGenerator s arch ret (LLVMExpr s arch)
transTypedValue :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transTypedValue Typed Value
v = (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a, b) -> b
snd ((MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> Generator
LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v
transValue :: forall s arch ret.
MemType
-> L.Value
-> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
ty Value
L.ValUndef =
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
ty
transValue MemType
ty Value
L.ValZeroInit =
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue ty :: MemType
ty@(PtrType SymType
_) Value
L.ValNull =
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue ty :: MemType
ty@MemType
PtrOpaqueType Value
L.ValNull =
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue ty :: MemType
ty@(PtrType SymType
_) (L.ValInteger Integer
0) =
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue ty :: MemType
ty@MemType
PtrOpaqueType (L.ValInteger Integer
0) =
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue ty :: MemType
ty@(PtrType SymType
_) v :: Value
v@(L.ValInteger Integer
_) =
Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Attempted to use integer ", Value -> String
forall a. Show a => a -> String
show Value
v, String
" as pointer: ", MemType -> String
forall a. Show a => a -> String
show MemType
ty]
transValue ty :: MemType
ty@MemType
PtrOpaqueType v :: Value
v@(L.ValInteger Integer
_) =
Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Attempted to use integer ", Value -> String
forall a. Show a => a -> String
show Value
v, String
" as pointer: ", MemType -> String
forall a. Show a => a -> String
show MemType
ty]
transValue ty :: MemType
ty@(IntType Natural
_) Value
L.ValNull =
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue MemType
_ (L.ValString [Word8]
str) = do
let eight :: NatRepr 8
eight = NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 8
let bv8 :: TypeRepr (LLVMPointerType 8)
bv8 = NatRepr 8 -> TypeRepr (LLVMPointerType 8)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 8
eight
let chars :: Vector (Expr LLVM s (LLVMPointerType 8))
chars = [Expr LLVM s (LLVMPointerType 8)]
-> Vector (Expr LLVM s (LLVMPointerType 8))
forall a. [a] -> Vector a
V.fromList ([Expr LLVM s (LLVMPointerType 8)]
-> Vector (Expr LLVM s (LLVMPointerType 8)))
-> [Expr LLVM s (LLVMPointerType 8)]
-> Vector (Expr LLVM s (LLVMPointerType 8))
forall a b. (a -> b) -> a -> b
$ (Word8 -> Expr LLVM s (LLVMPointerType 8))
-> [Word8] -> [Expr LLVM s (LLVMPointerType 8)]
forall a b. (a -> b) -> [a] -> [b]
map (NatRepr 8
-> Expr LLVM s (BVType 8) -> Expr LLVM s (LLVMPointerType 8)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr 8
eight (Expr LLVM s (BVType 8) -> Expr LLVM s (LLVMPointerType 8))
-> (Word8 -> Expr LLVM s (BVType 8))
-> Word8
-> Expr LLVM s (LLVMPointerType 8)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. App LLVM (Expr LLVM s) (BVType 8) -> Expr LLVM s (BVType 8)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType 8) -> Expr LLVM s (BVType 8))
-> (Word8 -> App LLVM (Expr LLVM s) (BVType 8))
-> Word8
-> Expr LLVM s (BVType 8)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr 8 -> BV 8 -> App LLVM (Expr LLVM s) (BVType 8)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr 8
eight (BV 8 -> App LLVM (Expr LLVM s) (BVType 8))
-> (Word8 -> BV 8) -> Word8 -> App LLVM (Expr LLVM s) (BVType 8)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr 8 -> Integer -> BV 8
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 8
eight (Integer -> BV 8) -> (Word8 -> Integer) -> Word8 -> BV 8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Word8 -> Int) -> Word8 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Int
forall a. Enum a => a -> Int
fromEnum) ([Word8] -> [Expr LLVM s (LLVMPointerType 8)])
-> [Word8] -> [Expr LLVM s (LLVMPointerType 8)]
forall a b. (a -> b) -> a -> b
$ [Word8]
str
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('VectorType (LLVMPointerType 8))
-> Expr LLVM s ('VectorType (LLVMPointerType 8)) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (TypeRepr (LLVMPointerType 8)
-> TypeRepr ('VectorType (LLVMPointerType 8))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr (LLVMPointerType 8)
bv8) (App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
-> Expr LLVM s ('VectorType (LLVMPointerType 8))
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
-> Expr LLVM s ('VectorType (LLVMPointerType 8)))
-> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
-> Expr LLVM s ('VectorType (LLVMPointerType 8))
forall a b. (a -> b) -> a -> b
$ TypeRepr (LLVMPointerType 8)
-> Vector (Expr LLVM s (LLVMPointerType 8))
-> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1 -> Vector (f tp1) -> App ext f ('VectorType tp1)
VectorLit TypeRepr (LLVMPointerType 8)
bv8 (Vector (Expr LLVM s (LLVMPointerType 8))
-> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8)))
-> Vector (Expr LLVM s (LLVMPointerType 8))
-> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
forall a b. (a -> b) -> a -> b
$ Vector (Expr LLVM s (LLVMPointerType 8))
chars)
transValue MemType
_ (L.ValIdent Ident
i) = do
IdentMap s
m <- Getting (IdentMap s) (LLVMState arch s) (IdentMap s)
-> Generator LLVM s (LLVMState arch) ret IO (IdentMap s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting (IdentMap s) (LLVMState arch s) (IdentMap s)
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IdentMap s -> f (IdentMap s))
-> LLVMState arch s -> f (LLVMState arch s)
identMap
case Ident
-> IdentMap s -> Maybe (Either (Some (Reg s)) (Some (Atom s)))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i IdentMap s
m of
Maybe (Either (Some (Reg s)) (Some (Atom s)))
Nothing -> do
Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ String
"Could not find identifier " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ident -> String
forall a. Show a => a -> String
show Ident
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
Just (Left (Some Reg s x
r)) -> do
Expr LLVM s x
e <- Reg s x -> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s x
r
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr x -> Expr LLVM s x -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (Reg s x -> TypeRepr x
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s x
r) Expr LLVM s x
e
Just (Right (Some Atom s x
a)) -> do
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr x -> Expr LLVM s x -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (Atom s x -> TypeRepr x
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s x
a) (Atom s x -> Expr LLVM s x
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr Atom s x
a)
transValue (IntType Natural
n) (L.ValInteger Integer
i) =
ExceptT String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
-> Generator
LLVM s (LLVMState arch) ret IO (Either String LLVMConst)
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (Natural
-> Integer
-> ExceptT
String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
forall (m :: Type -> Type).
MonadError String m =>
Natural -> Integer -> m LLVMConst
intConst Natural
n Integer
i) Generator LLVM s (LLVMState arch) ret IO (Either String LLVMConst)
-> (Either String LLVMConst
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b.
Generator LLVM s (LLVMState arch) ret IO a
-> (a -> Generator LLVM s (LLVMState arch) ret IO b)
-> Generator LLVM s (LLVMState arch) ret IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left String
err -> String
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
err
Right LLVMConst
c -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c
transValue (IntType Natural
1) (L.ValBool Bool
b) =
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Bool -> LLVMConst
boolConst Bool
b)
transValue MemType
FloatType (L.ValFloat Float
f) =
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Float -> LLVMConst
FloatConst Float
f)
transValue MemType
DoubleType (L.ValDouble Double
d) =
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Double -> LLVMConst
DoubleConst Double
d)
transValue (StructType StructInfo
_) (L.ValStruct [Typed Value]
vs) = do
[(MemType, LLVMExpr s arch)]
vs' <- (Typed Value
-> Generator
LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch))
-> [Typed Value]
-> Generator
LLVM s (LLVMState arch) ret IO [(MemType, LLVMExpr s arch)]
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 (\Typed Value
v -> Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v) [Typed Value]
vs
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
StructExpr (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList ([(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch))
-> [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)]
vs')
transValue (StructType StructInfo
_) (L.ValPackedStruct [Typed Value]
vs) = do
[(MemType, LLVMExpr s arch)]
vs' <- (Typed Value
-> Generator
LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch))
-> [Typed Value]
-> Generator
LLVM s (LLVMState arch) ret IO [(MemType, LLVMExpr s arch)]
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 (\Typed Value
v -> Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v) [Typed Value]
vs
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
StructExpr (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList ([(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch))
-> [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)]
vs')
transValue (ArrayType Natural
_ MemType
tp) (L.ValArray Type
_ [Value]
vs) = do
[LLVMExpr s arch]
vs' <- (Value
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [Value]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
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 (\Value
v -> MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
tp Value
v) [Value]
vs
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
tp (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')
transValue (VecType Natural
_ MemType
tp) (L.ValVector Type
_ [Value]
vs) = do
[LLVMExpr s arch]
vs' <- (Value
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [Value]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
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 (\Value
v -> MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
tp Value
v) [Value]
vs
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
tp (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')
transValue MemType
_ (L.ValSymbol Symbol
symbol) = do
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Symbol -> Integer -> LLVMConst
SymbolConst Symbol
symbol Integer
0)
transValue MemType
_ (L.ValConstExpr ConstExpr' BlockLabel
cexp) =
do Either String LLVMConst
res <- ExceptT String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
-> Generator
LLVM s (LLVMState arch) ret IO (Either String LLVMConst)
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (ConstExpr' BlockLabel
-> ExceptT
String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError String m, HasPtrWidth wptr) =>
ConstExpr' BlockLabel -> m LLVMConst
transConstantExpr ConstExpr' BlockLabel
cexp)
case Either String LLVMConst
res of
Left String
err -> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
"Error translating constant", String
err]
Right LLVMConst
cv -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
cv
transValue MemType
ty Value
v =
Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"unsupported LLVM value:", Value -> String
forall a. Show a => a -> String
show Value
v, String
"of type", MemType -> String
forall a. Show a => a -> String
show MemType
ty]
callIsNull
:: (1 <= w)
=> NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIsNull :: forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIsNull NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex = App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType)
-> (Expr LLVM s BoolType -> App LLVM (Expr LLVM s) BoolType)
-> Expr LLVM s BoolType
-> Expr LLVM s BoolType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr LLVM s BoolType -> App LLVM (Expr LLVM s) BoolType
forall (f :: CrucibleType -> Type) ext.
f BoolType -> App ext f BoolType
Not (Expr LLVM s BoolType -> Expr LLVM s BoolType)
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIntToBool NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex
callIntToBool
:: (1 <= w)
=> NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIntToBool :: forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIntToBool NatRepr w
w (BitvectorAsPointerExpr NatRepr w
_ Expr LLVM s (BVType w)
bv) =
case Expr LLVM s (BVType w)
bv of
App (BVLit NatRepr w
_ BV w
i) -> if BV w
i 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
NatRepr w
w then Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s BoolType
forall (e :: CrucibleType -> Type). IsExpr e => e BoolType
false else Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s BoolType
forall (e :: CrucibleType -> Type). IsExpr e => e BoolType
true
Expr LLVM s (BVType w)
_ -> Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w
-> Expr LLVM s (BVType w) -> App LLVM (Expr LLVM s) BoolType
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> App ext f BoolType
BVNonzero NatRepr w
w Expr LLVM s (BVType w)
bv))
callIntToBool NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex =
do Expr LLVM s (LLVMPointerType w)
ex' <- Expr LLVM s (LLVMPointerType w)
-> Generator
LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType w))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation Expr LLVM s (LLVMPointerType w)
ex
let blk :: Expr LLVM s NatType
blk = App LLVM (Expr LLVM s) NatType -> Expr LLVM s NatType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) NatType
-> App LLVM (Expr LLVM s) NatType
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) NatType
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> a (LLVMPointerType w) -> LLVMExtensionExpr a NatType
LLVM_PointerBlock NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
let off :: Expr LLVM s (BVType w)
off = App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) (BVType w)
-> App LLVM (Expr LLVM s) (BVType w)
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) (BVType w)
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w
-> a (LLVMPointerType w)
-> LLVMExtensionExpr a ('BaseToType (BaseBVType w))
LLVM_PointerOffset NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr LLVM s NatType
blk Expr LLVM s NatType -> Expr LLVM s NatType -> Expr LLVM s BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(EqExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
./= Natural -> Expr LLVM s NatType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Natural
0 Expr LLVM s BoolType
-> Expr LLVM s BoolType -> Expr LLVM s BoolType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e BoolType -> e BoolType -> e BoolType
.|| (App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w
-> Expr LLVM s (BVType w) -> App LLVM (Expr LLVM s) BoolType
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> App ext f BoolType
BVNonzero NatRepr w
w Expr LLVM s (BVType w)
off)))
callAlloca
:: wptr ~ ArchWidth arch
=> Expr LLVM s (BVType wptr)
-> Alignment
-> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callAlloca :: forall (wptr :: Natural) (arch :: LLVMArch) s
(ret :: CrucibleType).
(wptr ~ ArchWidth arch) =>
Expr LLVM s (BVType wptr)
-> Alignment
-> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callAlloca Expr LLVM s (BVType wptr)
sz Alignment
alignment = do
GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
String
loc <- Position -> String
forall a. Show a => a -> String
show (Position -> String)
-> Generator LLVM s (LLVMState arch) ret IO Position
-> Generator LLVM s (LLVMState arch) ret IO String
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Generator LLVM s (LLVMState arch) ret IO Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Generator ext s t ret m Position
getPosition
StmtExtension LLVM (Expr LLVM s) (LLVMPointerType wptr)
-> Generator
LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType wptr))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr wptr
-> GlobalVar Mem
-> Expr LLVM s (BVType wptr)
-> Alignment
-> String
-> LLVMStmt (Expr LLVM s) (LLVMPointerType wptr)
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (BVType wptr)
-> Alignment
-> String
-> LLVMStmt
f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
LLVM_Alloca ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth GlobalVar Mem
memVar Expr LLVM s (BVType wptr)
sz Alignment
alignment String
loc)
callPushFrame :: Text -> LLVMGenerator s arch ret ()
callPushFrame :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Text -> LLVMGenerator s arch ret ()
callPushFrame Text
nm = do
GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (Text -> GlobalVar Mem -> LLVMStmt (Expr LLVM s) 'UnitType
forall (f :: CrucibleType -> Type).
Text -> GlobalVar Mem -> LLVMStmt f 'UnitType
LLVM_PushFrame Text
nm GlobalVar Mem
memVar)
callPopFrame :: LLVMGenerator s arch ret ()
callPopFrame :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
LLVMGenerator s arch ret ()
callPopFrame = do
GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem -> LLVMStmt (Expr LLVM s) 'UnitType
forall (f :: CrucibleType -> Type).
GlobalVar Mem -> LLVMStmt f 'UnitType
LLVM_PopFrame GlobalVar Mem
memVar)
callPtrAddOffset ::
wptr ~ ArchWidth arch
=> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (BVType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callPtrAddOffset :: forall (wptr :: Natural) (arch :: LLVMArch) s
(ret :: CrucibleType).
(wptr ~ ArchWidth arch) =>
Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (BVType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callPtrAddOffset Expr LLVM s (LLVMPointerType wptr)
base Expr LLVM s (BVType wptr)
off = do
GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
StmtExtension LLVM (Expr LLVM s) (LLVMPointerType wptr)
-> Generator
LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType wptr))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr wptr
-> GlobalVar Mem
-> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (BVType wptr)
-> LLVMStmt (Expr LLVM s) (LLVMPointerType wptr)
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (LLVMPointerType wptr)
-> f (BVType wptr)
-> LLVMStmt f (LLVMPointerType wptr)
LLVM_PtrAddOffset ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth GlobalVar Mem
memVar Expr LLVM s (LLVMPointerType wptr)
base Expr LLVM s (BVType wptr)
off)
callPtrSubtract ::
wptr ~ ArchWidth arch
=> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (LLVMPointerType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType wptr))
callPtrSubtract :: forall (wptr :: Natural) (arch :: LLVMArch) s
(ret :: CrucibleType).
(wptr ~ ArchWidth arch) =>
Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (LLVMPointerType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType wptr))
callPtrSubtract Expr LLVM s (LLVMPointerType wptr)
x Expr LLVM s (LLVMPointerType wptr)
y = do
GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
StmtExtension LLVM (Expr LLVM s) (BVType wptr)
-> Generator
LLVM s (LLVMState arch) ret IO (Expr LLVM s (BVType wptr))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr wptr
-> GlobalVar Mem
-> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (LLVMPointerType wptr)
-> LLVMStmt (Expr LLVM s) (BVType wptr)
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (LLVMPointerType wptr)
-> f (LLVMPointerType wptr)
-> LLVMStmt f ('BaseToType (BaseBVType wptr))
LLVM_PtrSubtract ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth GlobalVar Mem
memVar Expr LLVM s (LLVMPointerType wptr)
x Expr LLVM s (LLVMPointerType wptr)
y)
callLoad :: MemType
-> TypeRepr tp
-> LLVMExpr s arch
-> Alignment
-> LLVMGenerator s arch ret (LLVMExpr s arch)
callLoad :: forall (tp :: CrucibleType) s (arch :: LLVMArch)
(ret :: CrucibleType).
MemType
-> TypeRepr tp
-> LLVMExpr s arch
-> Alignment
-> LLVMGenerator s arch ret (LLVMExpr s arch)
callLoad MemType
typ TypeRepr tp
expectTy (LLVMExpr s arch -> ScalarView s arch
forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar -> Scalar Proxy# arch
_ TypeRepr tp
PtrRepr Expr LLVM s tp
ptr) Alignment
align =
do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
StorageType
typ' <- MemType -> Generator LLVM s (LLVMState arch) ret IO StorageType
forall (m :: Type -> Type) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
typ
Expr LLVM s tp
v <- StmtExtension LLVM (Expr LLVM s) tp
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> TypeRepr tp
-> StorageType
-> Alignment
-> LLVMStmt (Expr LLVM s) tp
forall (wptr :: Natural) (f :: CrucibleType -> Type)
(a :: CrucibleType).
HasPtrWidth wptr =>
GlobalVar Mem
-> f (LLVMPointerType wptr)
-> TypeRepr a
-> StorageType
-> Alignment
-> LLVMStmt f a
LLVM_Load GlobalVar Mem
memVar Expr LLVM s tp
Expr LLVM s (LLVMPointerType (ArchWidth arch))
ptr TypeRepr tp
expectTy StorageType
typ' Alignment
align)
LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr tp
expectTy Expr LLVM s tp
v)
callLoad MemType
_ TypeRepr tp
_ LLVMExpr s arch
_ Alignment
_ =
String
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> String
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Unexpected argument type in callLoad"]
callStore :: MemType
-> LLVMExpr s arch
-> LLVMExpr s arch
-> Alignment
-> LLVMGenerator s arch ret ()
callStore :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType
-> LLVMExpr s arch
-> LLVMExpr s arch
-> Alignment
-> LLVMGenerator s arch ret ()
callStore MemType
typ (LLVMExpr s arch -> ScalarView s arch
forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar -> Scalar Proxy# arch
_ TypeRepr tp
PtrRepr Expr LLVM s tp
ptr) (ZeroExpr MemType
_mt) Alignment
_align =
do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
StorageType
typ' <- MemType -> Generator LLVM s (LLVMState arch) ret IO StorageType
forall (m :: Type -> Type) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
typ
Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> Bytes
-> LLVMStmt (Expr LLVM s) 'UnitType
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
GlobalVar Mem
-> f (LLVMPointerType wptr) -> Bytes -> LLVMStmt f 'UnitType
LLVM_MemClear GlobalVar Mem
memVar Expr LLVM s tp
Expr LLVM s (LLVMPointerType (ArchWidth arch))
ptr (StorageType -> Bytes
storageTypeSize StorageType
typ'))
callStore MemType
typ (LLVMExpr s arch -> ScalarView s arch
forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar -> Scalar Proxy# arch
_ TypeRepr tp
PtrRepr Expr LLVM s tp
ptr) LLVMExpr s arch
v Alignment
align =
do let ?err = ?err::String -> Generator LLVM s (LLVMState arch) ret IO ()
String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail
LLVMExpr s arch
-> (forall {tpr :: CrucibleType}.
Proxy# arch
-> TypeRepr tpr
-> Expr LLVM s tpr
-> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne LLVMExpr s arch
v ((forall {tpr :: CrucibleType}.
Proxy# arch
-> TypeRepr tpr
-> Expr LLVM s tpr
-> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO ())
-> (forall {tpr :: CrucibleType}.
Proxy# arch
-> TypeRepr tpr
-> Expr LLVM s tpr
-> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
_ TypeRepr tpr
vtpr Expr LLVM s tpr
vexpr -> do
GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
StorageType
typ' <- MemType -> Generator LLVM s (LLVMState arch) ret IO StorageType
forall (m :: Type -> Type) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
typ
Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
(t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> TypeRepr tpr
-> StorageType
-> Alignment
-> Expr LLVM s tpr
-> LLVMStmt (Expr LLVM s) 'UnitType
forall (wptr :: Natural) (f :: CrucibleType -> Type)
(tp :: CrucibleType).
HasPtrWidth wptr =>
GlobalVar Mem
-> f (LLVMPointerType wptr)
-> TypeRepr tp
-> StorageType
-> Alignment
-> f tp
-> LLVMStmt f 'UnitType
LLVM_Store GlobalVar Mem
memVar Expr LLVM s tp
Expr LLVM s (LLVMPointerType (ArchWidth arch))
ptr TypeRepr tpr
vtpr StorageType
typ' Alignment
align Expr LLVM s tpr
vexpr)
callStore MemType
_ LLVMExpr s arch
_ LLVMExpr s arch
_ Alignment
_ =
String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Generator LLVM s (LLVMState arch) ret IO ())
-> String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Unexpected argument type in callStore"]