content: -----------------------------------------------------------------------
  -- |
  -- 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.Functions (bindLLVMHandle, bindLLVMCFG)
  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 handleWarning mtrans =
     mapM_ (registerModuleFn handleWarning mtrans) (map (L.decName.fst) (mtrans ^. 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 handleWarning mtrans sym =
    liftIO (getTranslatedCFG mtrans sym) >>= \case
      Nothing ->
        fail $ unlines
          [ "Could not find definition for function"
          , show sym
          ]
      Just (decl, AnyCFG cfg, warns) -> do
        let llvmCtx = mtrans ^. transContext
        let mvar = llvmMemVar llvmCtx
        bindLLVMCFG mvar (L.decName decl) cfg
  
        binds <- use (stateContext . functionBindings)
        let h = cfgHandle cfg
        when (isJust $ lookupHandleMap h $ fnBindings binds) $
          do loc <- liftIO . getCurrentProgramLoc =<< getSymInterface
             liftIO (handleWarning (LLVMTranslationWarning sym (plSourceLoc loc) "LLVM function handle registered twice"))
        liftIO $ mapM_ handleWarning 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 handleWarning mtrans =
     mapM_ (registerLazyModuleFn handleWarning mtrans) (map (L.decName.fst) (mtrans ^. 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 handleWarning mtrans sym =
    liftIO (getTranslatedFnHandle mtrans sym) >>= \case
      Nothing -> 
        fail $ unlines
          [ "Could not find definition for function"
          , show sym
          ]
      Just (decl, SomeHandle h) ->
       do let llvmCtx = mtrans ^. transContext
          let mvar = llvmMemVar llvmCtx
          -- 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 =
                UseOverride
                $ mkOverride' (handleName h) (handleReturnType h)
                $ -- 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.
                  liftIO (getTranslatedCFG mtrans sym) >>= \case
                    Nothing ->
                      panic "registerLazyModuleFn"
                        [ "Could not find definition for function in bootstrapping code"
                        , show sym
                        ]
                    Just (_decl, AnyCFG cfg, warns) ->
                      case testEquality (handleType (cfgHandle cfg)) (handleType h) of
                        Nothing -> panic "registerLazyModuleFn"
                                        ["Translated CFG type does not match function handle type",
                                         show (handleType h), show (handleType (cfgHandle cfg)) ]
                        Just Refl ->
                          do liftIO $ mapM_ handleWarning warns
                             -- Here we rebind the function handle to use the translated CFG
                             bindLLVMHandle mvar (L.decName decl) h (UseCFG cfg (postdomInfo cfg))
                             -- Now, make recursive call to ourself, which should invoke the
                             -- newly-installed CFG
                             regValue <$> (callFnVal (HandleFnVal h) =<< getOverrideArgs)
     
          -- Bind the function handle to the appropriate global symbol.
          bindLLVMHandle mvar (L.decName decl) h s
  
  
  llvmGlobalsToCtx
     :: LLVMContext arch
     -> MemImpl sym
     -> SymGlobalState sym
  llvmGlobalsToCtx = llvmGlobals . llvmMemVar
  
  llvmGlobals
     :: GlobalVar Mem
     -> MemImpl sym
     -> SymGlobalState sym
  llvmGlobals memVar mem = emptyGlobals & insertGlobal memVar mem
  
  llvmExtensionImpl ::
    (HasLLVMAnn sym) =>
    MemOptions ->
    ExtensionImpl p sym LLVM
  llvmExtensionImpl mo =
    let ?memOpts = mo in
    ExtensionImpl
    { extensionEval = llvmExtensionEval
    , extensionExec = llvmStatementExec
    }
  