{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.LLVM.Translation.Monad
(
LLVMGenerator
, LLVMGenerator'
, LLVMState(..)
, identMap
, blockInfoMap
, translationWarnings
, functionSymbol
, addWarning
, LLVMTranslationWarning(..)
, IdentMap
, LLVMBlockInfo(..)
, LLVMBlockInfoMap
, buildBlockInfoMap
, initialState
, getMemVar
, MalformedLLVMModule(..)
, malformedLLVMModule
, renderMalformedLLVMModule
, LLVMContext(..)
, llvmTypeCtx
, mkLLVMContext
, useTypedVal
) where
import Control.Lens hiding (op, (:>), to, from )
import Control.Monad (unless)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.State.Strict (MonadState(..))
import Data.IORef (IORef, modifyIORef)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Text (Text)
import qualified Text.LLVM.AST as L
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr as NatRepr
import Data.Parameterized.Some
import Lang.Crucible.CFG.Generator
import Lang.Crucible.Panic ( panic )
import Lang.Crucible.LLVM.DataLayout
import Lang.Crucible.LLVM.Extension
import Lang.Crucible.LLVM.MalformedLLVMModule
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.MemType
import Lang.Crucible.LLVM.Translation.BlockInfo
import Lang.Crucible.LLVM.Translation.Types
import Lang.Crucible.LLVM.TypeContext
import Lang.Crucible.Types
data LLVMContext arch
= LLVMContext
{
forall (arch :: LLVMArch). LLVMContext arch -> ArchRepr arch
llvmArch :: ArchRepr arch
, forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth :: forall a. (16 <= (ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
, forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar :: GlobalVar Mem
, forall (arch :: LLVMArch). LLVMContext arch -> TypeContext
_llvmTypeCtx :: TypeContext
, forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmGlobalAliases :: Map L.Symbol (Set L.GlobalAlias)
, forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmFunctionAliases :: Map L.Symbol (Set L.GlobalAlias)
}
llvmTypeCtx :: Simple Lens (LLVMContext arch) TypeContext
llvmTypeCtx :: forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx = (LLVMContext arch -> TypeContext)
-> (LLVMContext arch -> TypeContext -> LLVMContext arch)
-> Lens
(LLVMContext arch) (LLVMContext arch) TypeContext TypeContext
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMContext arch -> TypeContext
forall (arch :: LLVMArch). LLVMContext arch -> TypeContext
_llvmTypeCtx (\LLVMContext arch
s TypeContext
v -> LLVMContext arch
s{ _llvmTypeCtx = v })
mkLLVMContext :: GlobalVar Mem
-> L.Module
-> IO (Some LLVMContext)
mkLLVMContext :: GlobalVar Mem -> Module -> IO (Some LLVMContext)
mkLLVMContext GlobalVar Mem
mvar Module
m = do
let ([Doc Void]
errs, TypeContext
typeCtx) = Module -> ([Doc Void], TypeContext)
forall ann. Module -> ([Doc ann], TypeContext)
typeContextFromModule Module
m
Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless ([Doc Void] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Doc Void]
errs) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
Doc Void -> [Doc Void] -> IO ()
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule Doc Void
"Failed to construct LLVM type context" [Doc Void]
errs
let dl :: DataLayout
dl = TypeContext -> DataLayout
llvmDataLayout TypeContext
typeCtx
case Natural -> Some NatRepr
mkNatRepr (DataLayout -> Natural
ptrBitwidth DataLayout
dl) of
Some (NatRepr x
wptr :: NatRepr wptr) | Just LeqProof 16 x
LeqProof <- NatRepr 16 -> NatRepr x -> Maybe (LeqProof 16 x)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16) NatRepr x
wptr ->
NatRepr x
-> (HasPtrWidth x => IO (Some LLVMContext))
-> IO (Some LLVMContext)
forall (w :: Natural) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr x
wptr ((HasPtrWidth x => IO (Some LLVMContext)) -> IO (Some LLVMContext))
-> (HasPtrWidth x => IO (Some LLVMContext))
-> IO (Some LLVMContext)
forall a b. (a -> b) -> a -> b
$
do let archRepr :: ArchRepr ('X86 x)
archRepr = NatRepr x -> ArchRepr ('X86 x)
forall (w :: Natural). NatRepr w -> ArchRepr ('X86 w)
X86Repr NatRepr x
wptr
let ctx :: LLVMContext (X86 wptr)
ctx :: LLVMContext ('X86 x)
ctx = LLVMContext
{ llvmArch :: ArchRepr ('X86 x)
llvmArch = ArchRepr ('X86 x)
archRepr
, llvmMemVar :: GlobalVar Mem
llvmMemVar = GlobalVar Mem
mvar
, llvmPtrWidth :: forall a.
((16 <= ArchWidth ('X86 x)) => NatRepr (ArchWidth ('X86 x)) -> a)
-> a
llvmPtrWidth = \(16 <= ArchWidth ('X86 x)) => NatRepr (ArchWidth ('X86 x)) -> a
x -> (16 <= ArchWidth ('X86 x)) => NatRepr (ArchWidth ('X86 x)) -> a
NatRepr (ArchWidth ('X86 x)) -> a
x NatRepr x
NatRepr (ArchWidth ('X86 x))
wptr
, _llvmTypeCtx :: TypeContext
_llvmTypeCtx = TypeContext
typeCtx
, llvmGlobalAliases :: Map Symbol (Set GlobalAlias)
llvmGlobalAliases = Map Symbol (Set GlobalAlias)
forall a. Monoid a => a
mempty
, llvmFunctionAliases :: Map Symbol (Set GlobalAlias)
llvmFunctionAliases = Map Symbol (Set GlobalAlias)
forall a. Monoid a => a
mempty
}
Some LLVMContext -> IO (Some LLVMContext)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMContext ('X86 x) -> Some LLVMContext
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some LLVMContext ('X86 x)
ctx)
Some NatRepr
_ ->
[Char] -> IO (Some LLVMContext)
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"Cannot load LLVM bitcode file with illegal pointer width: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bytes -> [Char]
forall a. Show a => a -> [Char]
show (DataLayout
dlDataLayout -> Getting Bytes DataLayout Bytes -> Bytes
forall s a. s -> Getting a s a -> a
^.Getting Bytes DataLayout Bytes
Lens' DataLayout Bytes
ptrSize))
type LLVMGenerator s arch ret a =
(?lc :: TypeContext, HasPtrWidth (ArchWidth arch)) =>
Generator LLVM s (LLVMState arch) ret IO a
type LLVMGenerator' s arch ret =
Generator LLVM s (LLVMState arch) ret IO
getMemVar :: LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar :: forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar = LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar (LLVMContext arch -> GlobalVar Mem)
-> (LLVMState arch s -> LLVMContext arch)
-> LLVMState arch s
-> GlobalVar Mem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMState arch s -> LLVMContext arch
forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMContext arch
llvmContext (LLVMState arch s -> GlobalVar Mem)
-> Generator LLVM s (LLVMState arch) reg IO (LLVMState arch s)
-> Generator LLVM s (LLVMState arch) reg IO (GlobalVar Mem)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Generator LLVM s (LLVMState arch) reg IO (LLVMState arch s)
forall s (m :: Type -> Type). MonadState s m => m s
get
type IdentMap s = Map L.Ident (Either (Some (Reg s)) (Some (Atom s)))
data LLVMTranslationWarning =
LLVMTranslationWarning
L.Symbol
Position
Text
data LLVMState arch s
= LLVMState
{
forall (arch :: LLVMArch) s. LLVMState arch s -> IdentMap s
_identMap :: !(IdentMap s)
, forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMBlockInfoMap s
_blockInfoMap :: !(LLVMBlockInfoMap s)
, forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMContext arch
llvmContext :: LLVMContext arch
, forall (arch :: LLVMArch) s.
LLVMState arch s -> IORef [LLVMTranslationWarning]
_translationWarnings :: IORef [LLVMTranslationWarning]
, forall (arch :: LLVMArch) s. LLVMState arch s -> Symbol
_functionSymbol :: L.Symbol
}
identMap :: Lens' (LLVMState arch s) (IdentMap s)
identMap :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IdentMap s -> f (IdentMap s))
-> LLVMState arch s -> f (LLVMState arch s)
identMap = (LLVMState arch s -> IdentMap s)
-> (LLVMState arch s -> IdentMap s -> LLVMState arch s)
-> Lens
(LLVMState arch s) (LLVMState arch s) (IdentMap s) (IdentMap s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> IdentMap s
forall (arch :: LLVMArch) s. LLVMState arch s -> IdentMap s
_identMap (\LLVMState arch s
s IdentMap s
v -> LLVMState arch s
s { _identMap = v })
blockInfoMap :: Lens' (LLVMState arch s) (LLVMBlockInfoMap s)
blockInfoMap :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(LLVMBlockInfoMap s -> f (LLVMBlockInfoMap s))
-> LLVMState arch s -> f (LLVMState arch s)
blockInfoMap = (LLVMState arch s -> LLVMBlockInfoMap s)
-> (LLVMState arch s -> LLVMBlockInfoMap s -> LLVMState arch s)
-> Lens
(LLVMState arch s)
(LLVMState arch s)
(LLVMBlockInfoMap s)
(LLVMBlockInfoMap s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> LLVMBlockInfoMap s
forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMBlockInfoMap s
_blockInfoMap (\LLVMState arch s
s LLVMBlockInfoMap s
v -> LLVMState arch s
s { _blockInfoMap = v })
translationWarnings :: Lens' (LLVMState arch s) (IORef [LLVMTranslationWarning])
translationWarnings :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IORef [LLVMTranslationWarning]
-> f (IORef [LLVMTranslationWarning]))
-> LLVMState arch s -> f (LLVMState arch s)
translationWarnings = (LLVMState arch s -> IORef [LLVMTranslationWarning])
-> (LLVMState arch s
-> IORef [LLVMTranslationWarning] -> LLVMState arch s)
-> Lens
(LLVMState arch s)
(LLVMState arch s)
(IORef [LLVMTranslationWarning])
(IORef [LLVMTranslationWarning])
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> IORef [LLVMTranslationWarning]
forall (arch :: LLVMArch) s.
LLVMState arch s -> IORef [LLVMTranslationWarning]
_translationWarnings (\LLVMState arch s
s IORef [LLVMTranslationWarning]
v -> LLVMState arch s
s { _translationWarnings = v })
functionSymbol :: Lens' (LLVMState arch s) L.Symbol
functionSymbol :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(Symbol -> f Symbol) -> LLVMState arch s -> f (LLVMState arch s)
functionSymbol = (LLVMState arch s -> Symbol)
-> (LLVMState arch s -> Symbol -> LLVMState arch s)
-> Lens (LLVMState arch s) (LLVMState arch s) Symbol Symbol
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> Symbol
forall (arch :: LLVMArch) s. LLVMState arch s -> Symbol
_functionSymbol (\LLVMState arch s
s Symbol
v -> LLVMState arch s
s{ _functionSymbol = v })
addWarning :: Text -> LLVMGenerator s arch ret ()
addWarning :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Text -> LLVMGenerator s arch ret ()
addWarning Text
warn =
do IORef [LLVMTranslationWarning]
r <- Getting
(IORef [LLVMTranslationWarning])
(LLVMState arch s)
(IORef [LLVMTranslationWarning])
-> Generator
LLVM s (LLVMState arch) ret IO (IORef [LLVMTranslationWarning])
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
(IORef [LLVMTranslationWarning])
(LLVMState arch s)
(IORef [LLVMTranslationWarning])
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IORef [LLVMTranslationWarning]
-> f (IORef [LLVMTranslationWarning]))
-> LLVMState arch s -> f (LLVMState arch s)
translationWarnings
Symbol
s <- Getting Symbol (LLVMState arch s) Symbol
-> Generator LLVM s (LLVMState arch) ret IO Symbol
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting Symbol (LLVMState arch s) Symbol
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(Symbol -> f Symbol) -> LLVMState arch s -> f (LLVMState arch s)
functionSymbol
Position
p <- 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
IO () -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. IO a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IORef [LLVMTranslationWarning]
-> ([LLVMTranslationWarning] -> [LLVMTranslationWarning]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [LLVMTranslationWarning]
r ((Symbol -> Position -> Text -> LLVMTranslationWarning
LLVMTranslationWarning Symbol
s Position
p Text
warn)LLVMTranslationWarning
-> [LLVMTranslationWarning] -> [LLVMTranslationWarning]
forall a. a -> [a] -> [a]
:))
buildIdentMap :: (?lc :: TypeContext, HasPtrWidth wptr)
=> [L.Typed L.Ident]
-> Bool
-> CtxRepr ctx
-> Ctx.Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap :: forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap [Typed Ident]
ts Bool
True CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn IdentMap s
m =
TypeRepr ('VectorType 'AnyType)
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall {ctx' :: Ctx CrucibleType}.
Some (Atom s)
-> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) s a.
TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packBase (TypeRepr 'AnyType -> TypeRepr ('VectorType 'AnyType)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr 'AnyType
AnyRepr) CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn ((forall {ctx' :: Ctx CrucibleType}.
Some (Atom s)
-> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s)
-> (forall {ctx' :: Ctx CrucibleType}.
Some (Atom s)
-> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall a b. (a -> b) -> a -> b
$ \Some (Atom s)
_x CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' ->
[Typed Ident]
-> Bool
-> CtxRepr ctx'
-> Assignment (Atom s) ctx'
-> IdentMap s
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap [Typed Ident]
ts Bool
False CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' IdentMap s
m
buildIdentMap [] Bool
_ CtxRepr ctx
ctx Assignment (Atom s) ctx
_ IdentMap s
m
| CtxRepr ctx -> Bool
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Bool
Ctx.null CtxRepr ctx
ctx = IdentMap s
m
| Bool
otherwise =
[Char] -> [[Char]] -> IdentMap s
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"crucible-llvm:Translation.buildIdentMap"
[ [Char]
"buildIdentMap: passed arguments do not match LLVM input signature" ]
buildIdentMap (Typed Ident
ti:[Typed Ident]
ts) Bool
_ CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn IdentMap s
m = do
let ty :: MemType
ty = case Type -> Either [Char] MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType (Typed Ident -> Type
forall a. Typed a -> Type
L.typedType Typed Ident
ti) of
Right MemType
t -> MemType
t
Left [Char]
err -> [Char] -> [[Char]] -> MemType
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"crucible-llvm:Translation.buildIdentMap"
[ [Char]
"Error attempting to lift type " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Typed Ident -> [Char]
forall a. Show a => a -> [Char]
show Typed Ident
ti
, [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
err
]
MemType
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall {ctx' :: Ctx CrucibleType}.
Some (Atom s)
-> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s a.
HasPtrWidth wptr =>
MemType
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packType MemType
ty CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn ((forall {ctx' :: Ctx CrucibleType}.
Some (Atom s)
-> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s)
-> (forall {ctx' :: Ctx CrucibleType}.
Some (Atom s)
-> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall a b. (a -> b) -> a -> b
$ \Some (Atom s)
x CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' ->
[Typed Ident]
-> Bool
-> CtxRepr ctx'
-> Assignment (Atom s) ctx'
-> IdentMap s
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap [Typed Ident]
ts Bool
False CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' (Ident
-> Either (Some (Reg s)) (Some (Atom s))
-> IdentMap s
-> IdentMap s
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Typed Ident -> Ident
forall a. Typed a -> a
L.typedValue Typed Ident
ti) (Some (Atom s) -> Either (Some (Reg s)) (Some (Atom s))
forall a b. b -> Either a b
Right Some (Atom s)
x) IdentMap s
m)
initialState :: (?lc :: TypeContext, HasPtrWidth wptr)
=> L.Define
-> LLVMContext arch
-> CtxRepr args
-> Ctx.Assignment (Atom s) args
-> IORef [LLVMTranslationWarning]
-> LLVMState arch s
initialState :: forall (wptr :: Natural) (arch :: LLVMArch)
(args :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
Define
-> LLVMContext arch
-> CtxRepr args
-> Assignment (Atom s) args
-> IORef [LLVMTranslationWarning]
-> LLVMState arch s
initialState Define
d LLVMContext arch
llvmctx CtxRepr args
args Assignment (Atom s) args
asgn IORef [LLVMTranslationWarning]
warnRef =
let m :: IdentMap s
m = [Typed Ident]
-> Bool
-> CtxRepr args
-> Assignment (Atom s) args
-> IdentMap s
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap ([Typed Ident] -> [Typed Ident]
forall a. [a] -> [a]
reverse (Define -> [Typed Ident]
L.defArgs Define
d)) (Define -> Bool
L.defVarArgs Define
d) CtxRepr args
args Assignment (Atom s) args
asgn IdentMap s
forall k a. Map k a
Map.empty in
LLVMState { _identMap :: IdentMap s
_identMap = IdentMap s
m
, _blockInfoMap :: LLVMBlockInfoMap s
_blockInfoMap = LLVMBlockInfoMap s
forall k a. Map k a
Map.empty
, llvmContext :: LLVMContext arch
llvmContext = LLVMContext arch
llvmctx
, _translationWarnings :: IORef [LLVMTranslationWarning]
_translationWarnings = IORef [LLVMTranslationWarning]
warnRef
, _functionSymbol :: Symbol
_functionSymbol = Define -> Symbol
L.defName Define
d
}
packType :: HasPtrWidth wptr
=> MemType
-> CtxRepr ctx
-> Ctx.Assignment (Atom s) ctx
-> (forall ctx'. Some (Atom s) -> CtxRepr ctx' -> Ctx.Assignment (Atom s) ctx' -> a)
-> a
packType :: forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s a.
HasPtrWidth wptr =>
MemType
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packType MemType
tp CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> 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
repr ->
TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) s a.
TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packBase TypeRepr tp
repr CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
k
packBase
:: TypeRepr tp
-> CtxRepr ctx
-> Ctx.Assignment (Atom s) ctx
-> (forall ctx'. Some (Atom s) -> CtxRepr ctx' -> Ctx.Assignment (Atom s) ctx' -> a)
-> a
packBase :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) s a.
TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packBase TypeRepr tp
ctp CtxRepr ctx
ctx0 Assignment (Atom s) ctx
asgn forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
k =
case CtxRepr ctx
ctx0 of
Assignment TypeRepr ctx
ctx' Ctx.:> TypeRepr tp
ctp' ->
case TypeRepr tp -> TypeRepr tp -> Maybe (tp :~: tp)
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 tp
ctp TypeRepr tp
ctp' of
Maybe (tp :~: tp)
Nothing -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"crucible type mismatch",TypeRepr tp -> [Char]
forall a. Show a => a -> [Char]
show TypeRepr tp
ctp,TypeRepr tp -> [Char]
forall a. Show a => a -> [Char]
show TypeRepr tp
ctp']
Just tp :~: tp
Refl ->
let asgn' :: Assignment (Atom s) ctx
asgn' = Assignment (Atom s) (ctx '::> tp) -> Assignment (Atom s) ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f (ctx '::> tp) -> Assignment f ctx
Ctx.init Assignment (Atom s) ctx
Assignment (Atom s) (ctx '::> tp)
asgn
idx :: Index (ctx '::> tp) tp
idx = Size ctx -> Index (ctx '::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
Ctx.nextIndex (Assignment (Atom s) ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (Atom s) ctx
asgn')
in Some (Atom s)
-> Assignment TypeRepr ctx -> Assignment (Atom s) ctx -> a
forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
k (Atom s tp -> Some (Atom s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Assignment (Atom s) ctx
asgn Assignment (Atom s) ctx -> Index ctx tp -> Atom s tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
Index (ctx '::> tp) tp
idx))
Assignment TypeRepr ctx
ctx'
Assignment (Atom s) ctx
asgn'
CtxRepr ctx
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"packType: ran out of actual arguments!"