{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.LLVM
( LLVM
, registerModule
, registerModuleFn
, registerLazyModule
, registerLazyModuleFn
, llvmGlobalsToCtx
, llvmGlobals
, register_llvm_overrides
, llvmExtensionImpl
) where
import Control.Lens
import Control.Monad (when)
import Control.Monad.IO.Class
import qualified Text.LLVM.AST as L
import Lang.Crucible.Analysis.Postdom
import Lang.Crucible.Backend
import Lang.Crucible.CFG.Core
import Lang.Crucible.FunctionHandle
import Lang.Crucible.LLVM.Eval (llvmExtensionEval)
import Lang.Crucible.Panic (panic)
import Lang.Crucible.LLVM.Extension (ArchWidth)
import Lang.Crucible.LLVM.Intrinsics
import Lang.Crucible.LLVM.MemModel
( llvmStatementExec, HasPtrWidth, HasLLVMAnn, MemOptions, MemImpl
, Mem
)
import Lang.Crucible.LLVM.Translation
import Lang.Crucible.Simulator (regValue, FnVal(..))
import Lang.Crucible.Simulator.ExecutionTree
import Lang.Crucible.Simulator.GlobalState
import Lang.Crucible.Simulator.OverrideSim
import What4.Interface (getCurrentProgramLoc)
import What4.ProgramLoc (plSourceLoc)
registerModule ::
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ()) ->
ModuleTranslation arch ->
OverrideSim p sym LLVM rtp l a ()
registerModule :: forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
(a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch -> OverrideSim p sym LLVM rtp l a ()
registerModule LLVMTranslationWarning -> IO ()
handleWarning ModuleTranslation arch
mtrans =
(Symbol -> OverrideSim p sym LLVM rtp l a ())
-> [Symbol] -> OverrideSim p sym LLVM rtp l a ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> Symbol
-> OverrideSim p sym LLVM rtp l a ()
forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
(a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> Symbol
-> OverrideSim p sym LLVM rtp l a ()
registerModuleFn LLVMTranslationWarning -> IO ()
handleWarning ModuleTranslation arch
mtrans) (((Declare, SomeHandle) -> Symbol)
-> [(Declare, SomeHandle)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Declare -> Symbol
L.decName(Declare -> Symbol)
-> ((Declare, SomeHandle) -> Declare)
-> (Declare, SomeHandle)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Declare, SomeHandle) -> Declare
forall a b. (a, b) -> a
fst) (ModuleTranslation arch
mtrans ModuleTranslation arch
-> Getting
[(Declare, SomeHandle)]
(ModuleTranslation arch)
[(Declare, SomeHandle)]
-> [(Declare, SomeHandle)]
forall s a. s -> Getting a s a -> a
^. Getting
[(Declare, SomeHandle)]
(ModuleTranslation arch)
[(Declare, SomeHandle)]
forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
([(Declare, SomeHandle)] -> f [(Declare, SomeHandle)])
-> ModuleTranslation arch -> f (ModuleTranslation arch)
modTransDefs))
registerModuleFn ::
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ()) ->
ModuleTranslation arch ->
L.Symbol ->
OverrideSim p sym LLVM rtp l a ()
registerModuleFn :: forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
(a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> Symbol
-> OverrideSim p sym LLVM rtp l a ()
registerModuleFn LLVMTranslationWarning -> IO ()
handleWarning ModuleTranslation arch
mtrans Symbol
sym =
IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> OverrideSim
p
sym
LLVM
rtp
l
a
(Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall (arch :: LLVMArch).
ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
getTranslatedCFG ModuleTranslation arch
mtrans Symbol
sym) OverrideSim
p
sym
LLVM
rtp
l
a
(Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> OverrideSim p sym LLVM rtp l a ())
-> OverrideSim p sym LLVM rtp l a ()
forall a b.
OverrideSim p sym LLVM rtp l a a
-> (a -> OverrideSim p sym LLVM rtp l a b)
-> OverrideSim p sym LLVM rtp l a b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
Nothing ->
String -> OverrideSim p sym LLVM rtp l a ()
forall a. String -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> OverrideSim p sym LLVM rtp l a ())
-> String -> OverrideSim p sym LLVM rtp l a ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"Could not find definition for function"
, Symbol -> String
forall a. Show a => a -> String
show Symbol
sym
]
Just (Declare
decl, AnyCFG CFG LLVM blocks init ret
cfg, [LLVMTranslationWarning]
warns) -> do
let h :: FnHandle init ret
h = CFG LLVM blocks init ret -> FnHandle init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG LLVM blocks init ret
cfg
s :: FnState p sym LLVM init ret
s = CFG LLVM blocks init ret
-> CFGPostdom blocks -> FnState p sym LLVM init ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)).
CFG ext blocks args ret
-> CFGPostdom blocks -> FnState p sym ext args ret
UseCFG CFG LLVM blocks init ret
cfg (CFG LLVM blocks init ret -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
(r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
postdomInfo CFG LLVM blocks init ret
cfg)
FunctionBindings p sym LLVM
binds <- Getting
(FunctionBindings p sym LLVM)
(SimState p sym LLVM rtp (OverrideLang a) ('Just l))
(FunctionBindings p sym LLVM)
-> OverrideSim p sym LLVM rtp l a (FunctionBindings p sym LLVM)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((SimContext p sym LLVM
-> Const (FunctionBindings p sym LLVM) (SimContext p sym LLVM))
-> SimState p sym LLVM rtp (OverrideLang a) ('Just l)
-> Const
(FunctionBindings p sym LLVM)
(SimState p sym LLVM rtp (OverrideLang a) ('Just l))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
(f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext ((SimContext p sym LLVM
-> Const (FunctionBindings p sym LLVM) (SimContext p sym LLVM))
-> SimState p sym LLVM rtp (OverrideLang a) ('Just l)
-> Const
(FunctionBindings p sym LLVM)
(SimState p sym LLVM rtp (OverrideLang a) ('Just l)))
-> ((FunctionBindings p sym LLVM
-> Const
(FunctionBindings p sym LLVM) (FunctionBindings p sym LLVM))
-> SimContext p sym LLVM
-> Const (FunctionBindings p sym LLVM) (SimContext p sym LLVM))
-> Getting
(FunctionBindings p sym LLVM)
(SimState p sym LLVM rtp (OverrideLang a) ('Just l))
(FunctionBindings p sym LLVM)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionBindings p sym LLVM
-> Const
(FunctionBindings p sym LLVM) (FunctionBindings p sym LLVM))
-> SimContext p sym LLVM
-> Const (FunctionBindings p sym LLVM) (SimContext p sym LLVM)
forall p sym ext (f :: Type -> Type).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
functionBindings)
let llvmCtx :: LLVMContext arch
llvmCtx = ModuleTranslation arch
mtrans ModuleTranslation arch
-> Getting
(LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
-> LLVMContext arch
forall s a. s -> Getting a s a -> a
^. Getting
(LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext
LLVMContext arch
-> Symbol
-> FnHandle init ret
-> FnState p sym LLVM init ret
-> OverrideSim p sym LLVM rtp l a ()
forall sym (wptr :: Natural) (arch :: LLVMArch)
(args :: Ctx CrucibleType) (ret :: CrucibleType) p rtp
(l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMContext arch
-> Symbol
-> FnHandle args ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
bind_llvm_handle LLVMContext arch
llvmCtx (Declare -> Symbol
L.decName Declare
decl) FnHandle init ret
h FnState p sym LLVM init ret
s
Bool
-> OverrideSim p sym LLVM rtp l a ()
-> OverrideSim p sym LLVM rtp l a ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Maybe (FnState p sym LLVM init ret) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (FnState p sym LLVM init ret) -> Bool)
-> Maybe (FnState p sym LLVM init ret) -> Bool
forall a b. (a -> b) -> a -> b
$ FnHandle init ret
-> FnHandleMap (FnState p sym LLVM)
-> Maybe (FnState p sym LLVM init ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
(f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandle args ret -> FnHandleMap f -> Maybe (f args ret)
lookupHandleMap FnHandle init ret
h (FnHandleMap (FnState p sym LLVM)
-> Maybe (FnState p sym LLVM init ret))
-> FnHandleMap (FnState p sym LLVM)
-> Maybe (FnState p sym LLVM init ret)
forall a b. (a -> b) -> a -> b
$ FunctionBindings p sym LLVM -> FnHandleMap (FnState p sym LLVM)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
fnBindings FunctionBindings p sym LLVM
binds) (OverrideSim p sym LLVM rtp l a ()
-> OverrideSim p sym LLVM rtp l a ())
-> OverrideSim p sym LLVM rtp l a ()
-> OverrideSim p sym LLVM rtp l a ()
forall a b. (a -> b) -> a -> b
$
do ProgramLoc
loc <- IO ProgramLoc -> OverrideSim p sym LLVM rtp l a ProgramLoc
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc -> OverrideSim p sym LLVM rtp l a ProgramLoc)
-> (sym -> IO ProgramLoc)
-> sym
-> OverrideSim p sym LLVM rtp l a ProgramLoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc (sym -> OverrideSim p sym LLVM rtp l a ProgramLoc)
-> OverrideSim p sym LLVM rtp l a sym
-> OverrideSim p sym LLVM rtp l a ProgramLoc
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< OverrideSim p sym LLVM rtp l a sym
forall p sym ext rtp (args :: Ctx CrucibleType)
(ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
IO () -> OverrideSim p sym LLVM rtp l a ()
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (LLVMTranslationWarning -> IO ()
handleWarning (Symbol -> Position -> Text -> LLVMTranslationWarning
LLVMTranslationWarning Symbol
sym (ProgramLoc -> Position
plSourceLoc ProgramLoc
loc) Text
"LLVM function handle registered twice"))
IO () -> OverrideSim p sym LLVM rtp l a ()
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym LLVM rtp l a ())
-> IO () -> OverrideSim p sym LLVM rtp l a ()
forall a b. (a -> b) -> a -> b
$ (LLVMTranslationWarning -> IO ())
-> [LLVMTranslationWarning] -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LLVMTranslationWarning -> IO ()
handleWarning [LLVMTranslationWarning]
warns
registerLazyModule ::
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ()) ->
ModuleTranslation arch ->
OverrideSim p sym LLVM rtp l a ()
registerLazyModule :: forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
(a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch -> OverrideSim p sym LLVM rtp l a ()
registerLazyModule LLVMTranslationWarning -> IO ()
handleWarning ModuleTranslation arch
mtrans =
(Symbol -> OverrideSim p sym LLVM rtp l a ())
-> [Symbol] -> OverrideSim p sym LLVM rtp l a ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> Symbol
-> OverrideSim p sym LLVM rtp l a ()
forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
(a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> Symbol
-> OverrideSim p sym LLVM rtp l a ()
registerLazyModuleFn LLVMTranslationWarning -> IO ()
handleWarning ModuleTranslation arch
mtrans) (((Declare, SomeHandle) -> Symbol)
-> [(Declare, SomeHandle)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Declare -> Symbol
L.decName(Declare -> Symbol)
-> ((Declare, SomeHandle) -> Declare)
-> (Declare, SomeHandle)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Declare, SomeHandle) -> Declare
forall a b. (a, b) -> a
fst) (ModuleTranslation arch
mtrans ModuleTranslation arch
-> Getting
[(Declare, SomeHandle)]
(ModuleTranslation arch)
[(Declare, SomeHandle)]
-> [(Declare, SomeHandle)]
forall s a. s -> Getting a s a -> a
^. Getting
[(Declare, SomeHandle)]
(ModuleTranslation arch)
[(Declare, SomeHandle)]
forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
([(Declare, SomeHandle)] -> f [(Declare, SomeHandle)])
-> ModuleTranslation arch -> f (ModuleTranslation arch)
modTransDefs))
registerLazyModuleFn ::
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ()) ->
ModuleTranslation arch ->
L.Symbol ->
OverrideSim p sym LLVM rtp l a ()
registerLazyModuleFn :: forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
(a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> Symbol
-> OverrideSim p sym LLVM rtp l a ()
registerLazyModuleFn LLVMTranslationWarning -> IO ()
handleWarning ModuleTranslation arch
mtrans Symbol
sym =
IO (Maybe (Declare, SomeHandle))
-> OverrideSim p sym LLVM rtp l a (Maybe (Declare, SomeHandle))
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (ModuleTranslation arch
-> Symbol -> IO (Maybe (Declare, SomeHandle))
forall (arch :: LLVMArch).
ModuleTranslation arch
-> Symbol -> IO (Maybe (Declare, SomeHandle))
getTranslatedFnHandle ModuleTranslation arch
mtrans Symbol
sym) OverrideSim p sym LLVM rtp l a (Maybe (Declare, SomeHandle))
-> (Maybe (Declare, SomeHandle)
-> OverrideSim p sym LLVM rtp l a ())
-> OverrideSim p sym LLVM rtp l a ()
forall a b.
OverrideSim p sym LLVM rtp l a a
-> (a -> OverrideSim p sym LLVM rtp l a b)
-> OverrideSim p sym LLVM rtp l a b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (Declare, SomeHandle)
Nothing ->
String -> OverrideSim p sym LLVM rtp l a ()
forall a. String -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> OverrideSim p sym LLVM rtp l a ())
-> String -> OverrideSim p sym LLVM rtp l a ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"Could not find definition for function"
, Symbol -> String
forall a. Show a => a -> String
show Symbol
sym
]
Just (Declare
decl, SomeHandle FnHandle args ret
h) ->
do
let s :: FnState p sym LLVM args ret
s =
Override p sym LLVM args ret -> FnState p sym LLVM args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FnState p sym ext args ret
UseOverride
(Override p sym LLVM args ret -> FnState p sym LLVM args ret)
-> Override p sym LLVM args ret -> FnState p sym LLVM args ret
forall a b. (a -> b) -> a -> b
$ FunctionName
-> TypeRepr ret
-> (forall {r}.
OverrideSim p sym LLVM r args ret (RegValue sym ret))
-> Override p sym LLVM args ret
forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride' (FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle args ret
h) (FnHandle args ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType FnHandle args ret
h)
((forall {r}. OverrideSim p sym LLVM r args ret (RegValue sym ret))
-> Override p sym LLVM args ret)
-> (forall {r}.
OverrideSim p sym LLVM r args ret (RegValue sym ret))
-> Override p sym LLVM args ret
forall a b. (a -> b) -> a -> b
$
IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> OverrideSim
p
sym
LLVM
r
args
ret
(Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a. IO a -> OverrideSim p sym LLVM r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall (arch :: LLVMArch).
ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
getTranslatedCFG ModuleTranslation arch
mtrans Symbol
sym) OverrideSim
p
sym
LLVM
r
args
ret
(Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> OverrideSim p sym LLVM r args ret (RegValue sym ret))
-> OverrideSim p sym LLVM r args ret (RegValue sym ret)
forall a b.
OverrideSim p sym LLVM r args ret a
-> (a -> OverrideSim p sym LLVM r args ret b)
-> OverrideSim p sym LLVM r args ret b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
Nothing ->
String
-> [String] -> OverrideSim p sym LLVM r args ret (RegValue sym ret)
forall a. HasCallStack => String -> [String] -> a
panic String
"registerLazyModuleFn"
[ String
"Could not find definition for function in bootstrapping code"
, Symbol -> String
forall a. Show a => a -> String
show Symbol
sym
]
Just (Declare
_decl, AnyCFG CFG LLVM blocks init ret
cfg, [LLVMTranslationWarning]
warns) ->
case TypeRepr (FunctionHandleType init ret)
-> TypeRepr (FunctionHandleType args ret)
-> Maybe
(FunctionHandleType init ret :~: FunctionHandleType args ret)
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 (FnHandle init ret -> TypeRepr (FunctionHandleType init ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType (CFG LLVM blocks init ret -> FnHandle init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG LLVM blocks init ret
cfg)) (FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType FnHandle args ret
h) of
Maybe (FunctionHandleType init ret :~: FunctionHandleType args ret)
Nothing -> String
-> [String] -> OverrideSim p sym LLVM r args ret (RegValue sym ret)
forall a. HasCallStack => String -> [String] -> a
panic String
"registerLazyModuleFn"
[String
"Translated CFG type does not match function handle type",
TypeRepr (FunctionHandleType args ret) -> String
forall a. Show a => a -> String
show (FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType FnHandle args ret
h), TypeRepr (FunctionHandleType init ret) -> String
forall a. Show a => a -> String
show (FnHandle init ret -> TypeRepr (FunctionHandleType init ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType (CFG LLVM blocks init ret -> FnHandle init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG LLVM blocks init ret
cfg)) ]
Just FunctionHandleType init ret :~: FunctionHandleType args ret
Refl ->
do IO () -> OverrideSim p sym LLVM r args ret ()
forall a. IO a -> OverrideSim p sym LLVM r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym LLVM r args ret ())
-> IO () -> OverrideSim p sym LLVM r args ret ()
forall a b. (a -> b) -> a -> b
$ (LLVMTranslationWarning -> IO ())
-> [LLVMTranslationWarning] -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LLVMTranslationWarning -> IO ()
handleWarning [LLVMTranslationWarning]
warns
FnHandle args ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM r args ret ()
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()
bindFnHandle FnHandle args ret
h (CFG LLVM blocks args ret
-> CFGPostdom blocks -> FnState p sym LLVM args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)).
CFG ext blocks args ret
-> CFGPostdom blocks -> FnState p sym ext args ret
UseCFG CFG LLVM blocks args ret
CFG LLVM blocks init ret
cfg (CFG LLVM blocks init ret -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
(r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
postdomInfo CFG LLVM blocks init ret
cfg))
RegEntry sym ret -> RegValue sym ret
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (RegEntry sym ret -> RegValue sym ret)
-> OverrideSim p sym LLVM r args ret (RegEntry sym ret)
-> OverrideSim p sym LLVM r args ret (RegValue sym ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (FnVal sym args ret
-> RegMap sym args
-> OverrideSim p sym LLVM r args ret (RegEntry sym ret)
forall sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType) p
rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
(IsExprBuilder sym, IsSyntaxExtension ext) =>
FnVal sym args ret
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callFnVal (FnHandle args ret -> FnVal sym args ret
forall (args :: Ctx CrucibleType) (res :: CrucibleType) sym.
FnHandle args res -> FnVal sym args res
HandleFnVal FnHandle args ret
h) (RegMap sym args
-> OverrideSim p sym LLVM r args ret (RegEntry sym ret))
-> OverrideSim p sym LLVM r args ret (RegMap sym args)
-> OverrideSim p sym LLVM r args ret (RegEntry sym ret)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< OverrideSim p sym LLVM r args ret (RegMap sym args)
forall p sym ext rtp (args :: Ctx CrucibleType)
(ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs)
let llvmCtx :: LLVMContext arch
llvmCtx = ModuleTranslation arch
mtrans ModuleTranslation arch
-> Getting
(LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
-> LLVMContext arch
forall s a. s -> Getting a s a -> a
^. Getting
(LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext
LLVMContext arch
-> Symbol
-> FnHandle args ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
forall sym (wptr :: Natural) (arch :: LLVMArch)
(args :: Ctx CrucibleType) (ret :: CrucibleType) p rtp
(l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMContext arch
-> Symbol
-> FnHandle args ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
bind_llvm_handle LLVMContext arch
llvmCtx (Declare -> Symbol
L.decName Declare
decl) FnHandle args ret
h FnState p sym LLVM args ret
s
llvmGlobalsToCtx
:: LLVMContext arch
-> MemImpl sym
-> SymGlobalState sym
llvmGlobalsToCtx :: forall (arch :: LLVMArch) sym.
LLVMContext arch -> MemImpl sym -> SymGlobalState sym
llvmGlobalsToCtx = GlobalVar Mem -> MemImpl sym -> SymGlobalState sym
forall sym. GlobalVar Mem -> MemImpl sym -> SymGlobalState sym
llvmGlobals (GlobalVar Mem -> MemImpl sym -> SymGlobalState sym)
-> (LLVMContext arch -> GlobalVar Mem)
-> LLVMContext arch
-> MemImpl sym
-> SymGlobalState sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar
llvmGlobals
:: GlobalVar Mem
-> MemImpl sym
-> SymGlobalState sym
llvmGlobals :: forall sym. GlobalVar Mem -> MemImpl sym -> SymGlobalState sym
llvmGlobals GlobalVar Mem
memVar MemImpl sym
mem = SymGlobalState sym
forall sym. SymGlobalState sym
emptyGlobals SymGlobalState sym
-> (SymGlobalState sym -> SymGlobalState sym) -> SymGlobalState sym
forall a b. a -> (a -> b) -> b
& GlobalVar Mem
-> RegValue sym Mem -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal GlobalVar Mem
memVar RegValue sym Mem
MemImpl sym
mem
llvmExtensionImpl ::
(HasLLVMAnn sym) =>
MemOptions ->
ExtensionImpl p sym LLVM
llvmExtensionImpl :: forall sym p.
HasLLVMAnn sym =>
MemOptions -> ExtensionImpl p sym LLVM
llvmExtensionImpl MemOptions
mo =
let ?memOpts = ?memOpts::MemOptions
MemOptions
mo in
ExtensionImpl
{ extensionEval :: forall bak rtp (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (ctx :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym LLVM rtp blocks r ctx
-> EvalAppFunc sym (ExprExtension LLVM)
extensionEval = bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym LLVM rtp blocks r ctx
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> ExprExtension LLVM f tp
-> IO (RegValue sym tp)
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym LLVM rtp blocks r ctx
-> EvalAppFunc sym LLVMExtensionExpr
forall sym bak p ext rtp (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (ctx :: Ctx CrucibleType).
(HasLLVMAnn sym, IsSymBackend sym bak) =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym ext rtp blocks r ctx
-> EvalAppFunc sym LLVMExtensionExpr
forall bak rtp (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (ctx :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym LLVM rtp blocks r ctx
-> EvalAppFunc sym (ExprExtension LLVM)
llvmExtensionEval
, extensionExec :: EvalStmtFunc p sym LLVM
extensionExec = StmtExtension LLVM (RegEntry sym) tp'
-> CrucibleState p sym LLVM rtp blocks r ctx
-> IO (RegValue sym tp', CrucibleState p sym LLVM rtp blocks r ctx)
forall sym p.
(HasLLVMAnn sym, ?memOpts::MemOptions) =>
EvalStmtFunc p sym LLVM
EvalStmtFunc p sym LLVM
llvmStatementExec
}