-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM
-- Description      : LLVM interface for Crucible
-- Copyright        : (c) Galois, Inc 2015-2016
-- License          : BSD3
-- Maintainer       : rdockins@galois.com
-- Stability        : provisional
------------------------------------------------------------------------

{-# 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)


-- | Register all the functions defined in the LLVM module.
--   This will immediately build Crucible CFGs for each function
--   defined in the module.
registerModule ::
   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
   (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
   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))

-- | Register a specific named function that is defined in the given
--   module translation. This will immediately build a Crucible CFG for
--   the named function.
registerModuleFn ::
   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
   (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
   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

-- | Lazily register all the functions defined in the LLVM module.  See
--   'registerLazyModuleFn' for a description.
registerLazyModule ::
   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
   (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
   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))

-- | Lazily register the named function that is defnied in the given module
--   translation. This will delay actually translating the function until it
--   is called. This done by first installing a bootstrapping override that
--   will peform the actual translation when first invoked, and then will backpatch
--   its own references to point to the translated function.
--
--   Note that the callback for printing translation warnings may be called at
--   a much-later point, when the function in question is actually first invoked.
registerLazyModuleFn ::
   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
   (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling translation warnings -} ->
   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 -- Bind the function handle we just created to the following bootstrapping code,
        -- which actually translates the function on its first execution and patches up
        -- behind itself.
        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
$ -- This inner action defines what to do when this function is called for the
                -- first time.  We actually translate the function and install it as the
                -- implementation for the function handle, instead of this bootstrapping code.
                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
                           -- Here we rebind the function handle to use the translated CFG
                           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))
                           -- Now, make recursive call to ourself, which should invoke the
                           -- newly-installed 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)
   
        -- Bind the function handle to the appropriate global symbol.
        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
  }