------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Globals
-- Description      : Operations for working with LLVM global variables
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module provides support for dealing with LLVM global variables,
-- including initial allocation and populating variables with their
-- initial values.  A @GlobalInitializerMap@ is constructed during
-- module translation and can subsequently be used to populate
-- global variables.  This can either be done all at once using
-- @populateAllGlobals@; or it can be done in a more selective manner,
-- using one of the other \"populate\" operations.
------------------------------------------------------------------------

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE ImplicitParams        #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}

module Lang.Crucible.LLVM.Globals
  ( initializeMemory
  , initializeAllMemory
  , initializeMemoryConstGlobals
  , populateGlobal
  , populateGlobals
  , populateAllGlobals
  , populateConstGlobals
  , registerFunPtr

  , GlobalInitializerMap
  , makeGlobalMap
  ) where

import           Control.Arrow ((&&&))
import           Control.Monad (foldM)
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.Except (MonadError(..))
import           Control.Lens hiding (op, (:>) )
import           Data.List (foldl')
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import           Data.String
import           Control.Monad.State (StateT, runStateT, get, put)
import           Data.Maybe (fromMaybe)
import qualified Data.Parameterized.Context as Ctx

import qualified Text.LLVM.AST as L

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.NatRepr as NatRepr

import           Lang.Crucible.LLVM.Bytes
import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.MemType
import           Lang.Crucible.LLVM.MemModel
import qualified Lang.Crucible.LLVM.MemModel.Generic as G
import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
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.Backend

import           What4.Interface

import           GHC.Stack

------------------------------------------------------------------------
-- GlobalInitializerMap

-- | A @GlobalInitializerMap@ records the initialized values of globals in an @L.Module@.
--
-- The @Left@ constructor is used to signal errors in translation,
-- which can happen when:
--  * The declaration is ill-typed
--  * The global isn't linked (@extern global@)
--
-- The @Nothing@ constructor is used to signal that the global isn't actually a
-- compile-time constant.
--
-- These failures are as granular as possible (attached to the values)
-- so that simulation still succeeds if the module has a bad global that the
-- verified function never touches.
--
-- To actually initialize globals, saw-script translates them into
-- instances of @MemModel.LLVMVal@.
type GlobalInitializerMap = Map L.Symbol (L.Global, Either String (MemType, Maybe LLVMConst))


------------------------------------------------------------------------
-- makeGlobalMap

-- | @makeGlobalMap@ creates a map from names of LLVM global variables
-- to the values of their initializers, if any are included in the module.
makeGlobalMap :: forall arch wptr. (?lc :: TypeContext, HasPtrWidth wptr)
              => LLVMContext arch
              -> L.Module
              -> GlobalInitializerMap
makeGlobalMap :: forall (arch :: LLVMArch) (wptr :: Natural).
(?lc::TypeContext, HasPtrWidth wptr) =>
LLVMContext arch -> Module -> GlobalInitializerMap
makeGlobalMap LLVMContext arch
ctx Module
m = (GlobalInitializerMap
 -> (Symbol, Set GlobalAlias) -> GlobalInitializerMap)
-> GlobalInitializerMap
-> [(Symbol, Set GlobalAlias)]
-> GlobalInitializerMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' GlobalInitializerMap
-> (Symbol, Set GlobalAlias) -> GlobalInitializerMap
forall {b}.
Map Symbol b -> (Symbol, Set GlobalAlias) -> Map Symbol b
addAliases GlobalInitializerMap
globalMap (Map Symbol (Set GlobalAlias) -> [(Symbol, Set GlobalAlias)]
forall k a. Map k a -> [(k, a)]
Map.toList (LLVMContext arch -> Map Symbol (Set GlobalAlias)
forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmGlobalAliases LLVMContext arch
ctx))

  where
   addAliases :: Map Symbol b -> (Symbol, Set GlobalAlias) -> Map Symbol b
addAliases Map Symbol b
mp (Symbol
glob, Set GlobalAlias
aliases) =
        case Symbol -> Map Symbol b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
glob Map Symbol b
mp of
          Just b
initzr -> [Symbol] -> b -> Map Symbol b -> Map Symbol b
forall {t :: Type -> Type} {a} {b}.
(Foldable t, Ord a) =>
t a -> b -> Map a b -> Map a b
insertAll ((GlobalAlias -> Symbol) -> [GlobalAlias] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map GlobalAlias -> Symbol
L.aliasName (Set GlobalAlias -> [GlobalAlias]
forall a. Set a -> [a]
Set.toList Set GlobalAlias
aliases)) b
initzr Map Symbol b
mp
          Maybe b
Nothing     -> Map Symbol b
mp -- should this be an error/exception?

   globalMap :: GlobalInitializerMap
globalMap = [(Symbol, (Global, Either [Char] (MemType, Maybe LLVMConst)))]
-> GlobalInitializerMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Symbol, (Global, Either [Char] (MemType, Maybe LLVMConst)))]
 -> GlobalInitializerMap)
-> [(Symbol, (Global, Either [Char] (MemType, Maybe LLVMConst)))]
-> GlobalInitializerMap
forall a b. (a -> b) -> a -> b
$ (Global
 -> (Symbol, (Global, Either [Char] (MemType, Maybe LLVMConst))))
-> [Global]
-> [(Symbol, (Global, Either [Char] (MemType, Maybe LLVMConst)))]
forall a b. (a -> b) -> [a] -> [b]
map (Global -> Symbol
L.globalSym (Global -> Symbol)
-> (Global -> (Global, Either [Char] (MemType, Maybe LLVMConst)))
-> Global
-> (Symbol, (Global, Either [Char] (MemType, Maybe LLVMConst)))
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Global -> Global
forall a. a -> a
id (Global -> Global)
-> (Global -> Either [Char] (MemType, Maybe LLVMConst))
-> Global
-> (Global, Either [Char] (MemType, Maybe LLVMConst))
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Global -> Either [Char] (MemType, Maybe LLVMConst)
globalToConst))
                                  (Module -> [Global]
L.modGlobals Module
m)

   insertAll :: t a -> b -> Map a b -> Map a b
insertAll t a
ks b
v Map a b
mp = (a -> Map a b -> Map a b) -> Map a b -> t a -> Map a b
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((a -> b -> Map a b -> Map a b) -> b -> a -> Map a b -> Map a b
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert b
v) Map a b
mp t a
ks

   -- Catch the error from @transConstant@, turn it into @Either@
   globalToConst :: L.Global -> Either String (MemType, Maybe LLVMConst)
   globalToConst :: Global -> Either [Char] (MemType, Maybe LLVMConst)
globalToConst Global
g =
     Either [Char] (MemType, Maybe LLVMConst)
-> ([Char] -> Either [Char] (MemType, Maybe LLVMConst))
-> Either [Char] (MemType, Maybe LLVMConst)
forall a.
Either [Char] a -> ([Char] -> Either [Char] a) -> Either [Char] a
forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError
       (Global -> Either [Char] (MemType, Maybe LLVMConst)
forall (m :: Type -> Type).
MonadError [Char] m =>
Global -> m (MemType, Maybe LLVMConst)
globalToConst' Global
g)
       (\[Char]
err -> [Char] -> Either [Char] (MemType, Maybe LLVMConst)
forall a b. a -> Either a b
Left ([Char] -> Either [Char] (MemType, Maybe LLVMConst))
-> [Char] -> Either [Char] (MemType, Maybe LLVMConst)
forall a b. (a -> b) -> a -> b
$
         [Char]
"Encountered error while processing global "
           [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Symbol -> Doc
LPP.ppSymbol (Global -> Symbol
L.globalSym Global
g))
           [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": "
           [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
err)

   globalToConst' :: forall m. (MonadError String m)
                  => L.Global -> m (MemType, Maybe LLVMConst)
   globalToConst' :: forall (m :: Type -> Type).
MonadError [Char] m =>
Global -> m (MemType, Maybe LLVMConst)
globalToConst' Global
g =
     do let ?lc  = LLVMContext arch
ctxLLVMContext arch
-> Getting TypeContext (LLVMContext arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^.Getting TypeContext (LLVMContext arch) TypeContext
forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx -- implicitly passed to transConstant
        let gty :: Type
gty  = Global -> Type
L.globalType Global
g
        let gval :: Maybe Value
gval = Global -> Maybe Value
L.globalValue Global
g
        MemType
mt  <- Type -> m MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType Type
gty
        Maybe LLVMConst
val <- (Value -> m LLVMConst) -> Maybe Value -> m (Maybe LLVMConst)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (MemType -> Value -> m LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError [Char] m, HasPtrWidth wptr) =>
MemType -> Value -> m LLVMConst
transConstant' MemType
mt) Maybe Value
gval
        (MemType, Maybe LLVMConst) -> m (MemType, Maybe LLVMConst)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType
mt, Maybe LLVMConst
val)

-------------------------------------------------------------------------
-- initializeMemory

-- | Build the initial memory for an LLVM program.  Note, this process
-- allocates space for global variables, but does not set their
-- initial values.
initializeAllMemory
   :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
      , ?memOpts :: MemOptions )
   => bak
   -> LLVMContext arch
   -> L.Module
   -> IO (MemImpl sym)
initializeAllMemory :: forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
initializeAllMemory = (Global -> Bool)
-> bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
(Global -> Bool)
-> bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
initializeMemory (Bool -> Global -> Bool
forall a b. a -> b -> a
const Bool
True)

initializeMemoryConstGlobals
   :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
      , ?memOpts :: MemOptions )
   => bak
   -> LLVMContext arch
   -> L.Module
   -> IO (MemImpl sym)
initializeMemoryConstGlobals :: forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
initializeMemoryConstGlobals = (Global -> Bool)
-> bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
(Global -> Bool)
-> bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
initializeMemory (GlobalAttrs -> Bool
L.gaConstant (GlobalAttrs -> Bool) -> (Global -> GlobalAttrs) -> Global -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Global -> GlobalAttrs
L.globalAttrs)

initializeMemory
   :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
      , ?memOpts :: MemOptions )
   => (L.Global -> Bool)
   -> bak
   -> LLVMContext arch
   -> L.Module
   -> IO (MemImpl sym)
initializeMemory :: forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
(Global -> Bool)
-> bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
initializeMemory Global -> Bool
predicate bak
bak LLVMContext arch
llvm_ctx Module
llvmModl = do
   -- Create initial memory of appropriate endianness
   let ?lc = LLVMContext arch
llvm_ctxLLVMContext arch
-> Getting TypeContext (LLVMContext arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^.Getting TypeContext (LLVMContext arch) TypeContext
forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx
   let dl :: DataLayout
dl = TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc
   let endianness :: EndianForm
endianness = DataLayout
dlDataLayout
-> Getting EndianForm DataLayout EndianForm -> EndianForm
forall s a. s -> Getting a s a -> a
^.Getting EndianForm DataLayout EndianForm
Lens' DataLayout EndianForm
intLayout
   MemImpl sym
mem0 <- EndianForm -> IO (MemImpl sym)
forall sym. EndianForm -> IO (MemImpl sym)
emptyMem EndianForm
endianness

   -- allocate pointers values for function symbols, but do not
   -- yet bind them to function handles
   let decls :: [Either Declare Define]
decls = (Declare -> Either Declare Define)
-> [Declare] -> [Either Declare Define]
forall a b. (a -> b) -> [a] -> [b]
map Declare -> Either Declare Define
forall a b. a -> Either a b
Left (Module -> [Declare]
L.modDeclares Module
llvmModl) [Either Declare Define]
-> [Either Declare Define] -> [Either Declare Define]
forall a. [a] -> [a] -> [a]
++ (Define -> Either Declare Define)
-> [Define] -> [Either Declare Define]
forall a b. (a -> b) -> [a] -> [b]
map Define -> Either Declare Define
forall a b. b -> Either a b
Right (Module -> [Define]
L.modDefines Module
llvmModl)
   MemImpl sym
mem <- (MemImpl sym -> Either Declare Define -> IO (MemImpl sym))
-> MemImpl sym -> [Either Declare Define] -> IO (MemImpl sym)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (MemImpl sym)
allocLLVMFunPtr bak
bak LLVMContext arch
llvm_ctx) MemImpl sym
mem0 [Either Declare Define]
decls

   -- Allocate global values
   let globAliases :: Map Symbol (Set GlobalAlias)
globAliases = LLVMContext arch -> Map Symbol (Set GlobalAlias)
forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmGlobalAliases LLVMContext arch
llvm_ctx
   let globals :: [Global]
globals     = Module -> [Global]
L.modGlobals Module
llvmModl
   [(Global, [Symbol], Bytes, Alignment)]
gs_alloc <- (Global -> IO (Global, [Symbol], Bytes, Alignment))
-> [Global] -> IO [(Global, [Symbol], Bytes, Alignment)]
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 (\Global
g -> do
                        let err :: [Char] -> IO MemType
err [Char]
msg = Doc Void -> [Doc Void] -> IO MemType
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule
                                    (Doc Void
"Invalid type for global" Doc Void -> Doc Void -> Doc Void
forall a. Semigroup a => a -> a -> a
<> [Char] -> Doc Void
forall a. IsString a => [Char] -> a
fromString (Symbol -> [Char]
forall a. Show a => a -> [Char]
show (Global -> Symbol
L.globalSym Global
g)))
                                    [[Char] -> Doc Void
forall a. IsString a => [Char] -> a
fromString [Char]
msg]
                        MemType
ty <- ([Char] -> IO MemType)
-> (MemType -> IO MemType) -> Either [Char] MemType -> IO MemType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Char] -> IO MemType
err MemType -> IO MemType
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either [Char] MemType -> IO MemType)
-> Either [Char] MemType -> IO MemType
forall a b. (a -> b) -> a -> b
$ Type -> Either [Char] MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType (Type -> Either [Char] MemType) -> Type -> Either [Char] MemType
forall a b. (a -> b) -> a -> b
$ Global -> Type
L.globalType Global
g
                        let sz :: Bytes
sz      = DataLayout -> MemType -> Bytes
memTypeSize DataLayout
dl MemType
ty
                        let tyAlign :: Alignment
tyAlign = DataLayout -> MemType -> Alignment
memTypeAlign DataLayout
dl MemType
ty
                        let aliases :: [Symbol]
aliases = (GlobalAlias -> Symbol) -> [GlobalAlias] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map GlobalAlias -> Symbol
L.aliasName ([GlobalAlias] -> [Symbol])
-> (Set GlobalAlias -> [GlobalAlias])
-> Set GlobalAlias
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set GlobalAlias -> [GlobalAlias]
forall a. Set a -> [a]
Set.toList (Set GlobalAlias -> [Symbol]) -> Set GlobalAlias -> [Symbol]
forall a b. (a -> b) -> a -> b
$
                              Set GlobalAlias -> Maybe (Set GlobalAlias) -> Set GlobalAlias
forall a. a -> Maybe a -> a
fromMaybe Set GlobalAlias
forall a. Set a
Set.empty (Symbol -> Map Symbol (Set GlobalAlias) -> Maybe (Set GlobalAlias)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Global -> Symbol
L.globalSym Global
g) Map Symbol (Set GlobalAlias)
globAliases)
                        -- LLVM documentation regarding global variable alignment:
                        --
                        -- An explicit alignment may be specified for
                        -- a global, which must be a power of 2. If
                        -- not present, or if the alignment is set to
                        -- zero, the alignment of the global is set by
                        -- the target to whatever it feels
                        -- convenient. If an explicit alignment is
                        -- specified, the global is forced to have
                        -- exactly that alignment.
                        Alignment
alignment <-
                          case Global -> Maybe Align
L.globalAlign Global
g of
                            Just Align
a | Align
a Align -> Align -> Bool
forall a. Ord a => a -> a -> Bool
> Align
0 ->
                              case Bytes -> Maybe Alignment
toAlignment (Align -> Bytes
forall a. Integral a => a -> Bytes
toBytes Align
a) of
                                Maybe Alignment
Nothing -> [Char] -> IO Alignment
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO Alignment) -> [Char] -> IO Alignment
forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid alignemnt: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Align -> [Char]
forall a. Show a => a -> [Char]
show Align
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                                  [Char]
"specified for global: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (Global -> Symbol
L.globalSym Global
g)
                                Just Alignment
al -> Alignment -> IO Alignment
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Alignment
al
                            Maybe Align
_ -> Alignment -> IO Alignment
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Alignment
tyAlign
                        (Global, [Symbol], Bytes, Alignment)
-> IO (Global, [Symbol], Bytes, Alignment)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Global
g, [Symbol]
aliases, Bytes
sz, Alignment
alignment))
                    [Global]
globals
   bak
-> [(Global, [Symbol], Bytes, Alignment)]
-> MemImpl sym
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> [(Global, [Symbol], Bytes, Alignment)]
-> MemImpl sym
-> IO (MemImpl sym)
allocGlobals bak
bak (((Global, [Symbol], Bytes, Alignment) -> Bool)
-> [(Global, [Symbol], Bytes, Alignment)]
-> [(Global, [Symbol], Bytes, Alignment)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Global
g, [Symbol]
_, Bytes
_, Alignment
_) -> Global -> Bool
predicate Global
g) [(Global, [Symbol], Bytes, Alignment)]
gs_alloc) MemImpl sym
mem


allocLLVMFunPtr ::
  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  bak ->
  LLVMContext arch ->
  MemImpl sym ->
  Either L.Declare L.Define ->
  IO (MemImpl sym)
allocLLVMFunPtr :: forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (MemImpl sym)
allocLLVMFunPtr bak
bak LLVMContext arch
llvm_ctx MemImpl sym
mem Either Declare Define
decl =
  do let (Symbol
symbol, [Char]
displayString) =
           case Either Declare Define
decl of
             Left Declare
d ->
               let s :: Symbol
s@(L.Symbol [Char]
nm) = Declare -> Symbol
L.decName Declare
d
                in ( Symbol
s, [Char]
"[external function] " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
nm )
             Right Define
d ->
               let s :: Symbol
s@(L.Symbol [Char]
nm) = Define -> Symbol
L.defName Define
d
                in ( Symbol
s, [Char]
"[defined function ] " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
nm)
     let funAliases :: Map Symbol (Set GlobalAlias)
funAliases = LLVMContext arch -> Map Symbol (Set GlobalAlias)
forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmFunctionAliases LLVMContext arch
llvm_ctx
     let aliases :: [Symbol]
aliases = (GlobalAlias -> Symbol) -> [GlobalAlias] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map GlobalAlias -> Symbol
L.aliasName ([GlobalAlias] -> [Symbol]) -> [GlobalAlias] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [GlobalAlias]
-> (Set GlobalAlias -> [GlobalAlias])
-> Maybe (Set GlobalAlias)
-> [GlobalAlias]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Set GlobalAlias -> [GlobalAlias]
forall a. Set a -> [a]
Set.toList (Maybe (Set GlobalAlias) -> [GlobalAlias])
-> Maybe (Set GlobalAlias) -> [GlobalAlias]
forall a b. (a -> b) -> a -> b
$ Symbol -> Map Symbol (Set GlobalAlias) -> Maybe (Set GlobalAlias)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
symbol Map Symbol (Set GlobalAlias)
funAliases
     (LLVMPointer sym wptr
_ptr, MemImpl sym
mem') <- bak
-> MemImpl sym
-> [Char]
-> Symbol
-> [Symbol]
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> [Char]
-> Symbol
-> [Symbol]
-> IO (LLVMPtr sym wptr, MemImpl sym)
registerFunPtr bak
bak MemImpl sym
mem [Char]
displayString Symbol
symbol [Symbol]
aliases
     MemImpl sym -> IO (MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MemImpl sym
mem'

-- | Create a global allocation assocated with a function
registerFunPtr ::
  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  bak ->
  MemImpl sym ->
  -- | Display name
  String ->
  -- | Function name
  L.Symbol ->
  -- | Aliases
  [L.Symbol] ->
  IO (LLVMPtr sym wptr, MemImpl sym)
registerFunPtr :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> [Char]
-> Symbol
-> [Symbol]
-> IO (LLVMPtr sym wptr, MemImpl sym)
registerFunPtr bak
bak MemImpl sym
mem [Char]
displayName Symbol
nm [Symbol]
aliases = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  SymExpr sym (BaseBVType wptr)
z <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> BV wptr
forall (w :: Natural). NatRepr w -> BV w
BV.zero ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)
  (LLVMPointer sym wptr
ptr, MemImpl sym
mem') <- bak
-> AllocType
-> Mutability
-> [Char]
-> MemImpl sym
-> SymExpr sym (BaseBVType wptr)
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> [Char]
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
G.GlobalAlloc Mutability
G.Immutable [Char]
displayName MemImpl sym
mem SymExpr sym (BaseBVType wptr)
z Alignment
noAlignment
  (LLVMPointer sym wptr, MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((LLVMPointer sym wptr, MemImpl sym)
 -> IO (LLVMPointer sym wptr, MemImpl sym))
-> (LLVMPointer sym wptr, MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym)
forall a b. (a -> b) -> a -> b
$ (LLVMPointer sym wptr
ptr, MemImpl sym -> [Symbol] -> LLVMPtr sym wptr -> MemImpl sym
forall sym (wptr :: Natural).
(IsExprBuilder sym, 1 <= wptr) =>
MemImpl sym -> [Symbol] -> LLVMPtr sym wptr -> MemImpl sym
registerGlobal MemImpl sym
mem' (Symbol
nmSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
aliases) LLVMPtr sym wptr
LLVMPointer sym wptr
ptr)

------------------------------------------------------------------------
-- ** populateGlobals

-- | Populate the globals mentioned in the given @GlobalInitializerMap@
--   provided they satisfy the given filter function.
--
--   This will (necessarily) populate any globals that the ones in the
--   filtered list transitively reference.
populateGlobals ::
  ( ?lc :: TypeContext
  , ?memOpts :: MemOptions
  , 16 <= wptr
  , HasPtrWidth wptr
  , HasLLVMAnn sym
  , IsSymBackend sym bak) =>
  (L.Global -> Bool)   {- ^ Filter function, globals that cause this to return true will be populated -} ->
  bak ->
  GlobalInitializerMap ->
  MemImpl sym ->
  IO (MemImpl sym)
populateGlobals :: forall (wptr :: Natural) sym bak.
(?lc::TypeContext, ?memOpts::MemOptions, 16 <= wptr,
 HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) =>
(Global -> Bool)
-> bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
populateGlobals Global -> Bool
select bak
bak GlobalInitializerMap
gimap MemImpl sym
mem0 = (MemImpl sym
 -> (Global, Either [Char] (MemType, Maybe LLVMConst))
 -> IO (MemImpl sym))
-> MemImpl sym
-> [(Global, Either [Char] (MemType, Maybe LLVMConst))]
-> IO (MemImpl sym)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM MemImpl sym
-> (Global, Either [Char] (MemType, Maybe LLVMConst))
-> IO (MemImpl sym)
f MemImpl sym
mem0 (GlobalInitializerMap
-> [(Global, Either [Char] (MemType, Maybe LLVMConst))]
forall k a. Map k a -> [a]
Map.elems GlobalInitializerMap
gimap)
  where
  f :: MemImpl sym
-> (Global, Either [Char] (MemType, Maybe LLVMConst))
-> IO (MemImpl sym)
f MemImpl sym
mem (Global
gl, Either [Char] (MemType, Maybe LLVMConst)
_) | Bool -> Bool
not (Global -> Bool
select Global
gl)    = MemImpl sym -> IO (MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MemImpl sym
mem
  f MemImpl sym
_   (Global
_,  Left [Char]
msg)               = [Char] -> IO (MemImpl sym)
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
msg
  f MemImpl sym
mem (Global
gl, Right (MemType
mty, Just LLVMConst
cval)) = bak
-> Global
-> MemType
-> LLVMConst
-> GlobalInitializerMap
-> MemImpl sym
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(?lc::TypeContext, 16 <= wptr, HasPtrWidth wptr,
 IsSymBackend sym bak, HasLLVMAnn sym, ?memOpts::MemOptions,
 HasCallStack) =>
bak
-> Global
-> MemType
-> LLVMConst
-> GlobalInitializerMap
-> MemImpl sym
-> IO (MemImpl sym)
populateGlobal bak
bak Global
gl MemType
mty LLVMConst
cval GlobalInitializerMap
gimap MemImpl sym
mem
  f MemImpl sym
mem (Global
gl, Right (MemType
mty, Maybe LLVMConst
Nothing))   = bak -> Global -> MemType -> MemImpl sym -> IO (MemImpl sym)
forall (wptr :: Natural) sym bak.
(?lc::TypeContext, 16 <= wptr, HasPtrWidth wptr,
 IsSymBackend sym bak, HasLLVMAnn sym, HasCallStack,
 ?memOpts::MemOptions) =>
bak -> Global -> MemType -> MemImpl sym -> IO (MemImpl sym)
populateExternalGlobal bak
bak Global
gl MemType
mty MemImpl sym
mem


-- | Populate all the globals mentioned in the given @GlobalInitializerMap@.
populateAllGlobals ::
  ( ?lc :: TypeContext
  , ?memOpts :: MemOptions
  , 16 <= wptr
  , HasPtrWidth wptr
  , HasLLVMAnn sym
  , IsSymBackend sym bak) =>
  bak ->
  GlobalInitializerMap ->
  MemImpl sym ->
  IO (MemImpl sym)
populateAllGlobals :: forall (wptr :: Natural) sym bak.
(?lc::TypeContext, ?memOpts::MemOptions, 16 <= wptr,
 HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) =>
bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
populateAllGlobals = (Global -> Bool)
-> bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
forall (wptr :: Natural) sym bak.
(?lc::TypeContext, ?memOpts::MemOptions, 16 <= wptr,
 HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) =>
(Global -> Bool)
-> bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
populateGlobals (Bool -> Global -> Bool
forall a b. a -> b -> a
const Bool
True)


-- | Populate only the constant global variables mentioned in the
--   given @GlobalInitializerMap@ (and any they transitively refer to).
populateConstGlobals ::
  ( ?lc :: TypeContext
  , ?memOpts :: MemOptions
  , 16 <= wptr
  , HasPtrWidth wptr
  , HasLLVMAnn sym
  , IsSymBackend sym bak) =>
  bak ->
  GlobalInitializerMap ->
  MemImpl sym ->
  IO (MemImpl sym)
populateConstGlobals :: forall (wptr :: Natural) sym bak.
(?lc::TypeContext, ?memOpts::MemOptions, 16 <= wptr,
 HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) =>
bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
populateConstGlobals = (Global -> Bool)
-> bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
forall (wptr :: Natural) sym bak.
(?lc::TypeContext, ?memOpts::MemOptions, 16 <= wptr,
 HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) =>
(Global -> Bool)
-> bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
populateGlobals Global -> Bool
f
  where f :: Global -> Bool
f = GlobalAttrs -> Bool
L.gaConstant (GlobalAttrs -> Bool) -> (Global -> GlobalAttrs) -> Global -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Global -> GlobalAttrs
L.globalAttrs


-- | Ordinarily external globals do not receive initalizing writes.  However,
--   when 'lax-loads-and-stores` is enabled in the `stable-symbolic` mode, we
--   populate external global variables with fresh bytes.
populateExternalGlobal ::
  ( ?lc :: TypeContext
  , 16 <= wptr
  , HasPtrWidth wptr
  , IsSymBackend sym bak
  , HasLLVMAnn sym
  , HasCallStack
  , ?memOpts :: MemOptions
  ) =>
  bak ->
  L.Global {- ^ The global to populate -} ->
  MemType {- ^ Type of the global -} ->
  MemImpl sym ->
  IO (MemImpl sym)
populateExternalGlobal :: forall (wptr :: Natural) sym bak.
(?lc::TypeContext, 16 <= wptr, HasPtrWidth wptr,
 IsSymBackend sym bak, HasLLVMAnn sym, HasCallStack,
 ?memOpts::MemOptions) =>
bak -> Global -> MemType -> MemImpl sym -> IO (MemImpl sym)
populateExternalGlobal bak
bak Global
gl MemType
memty MemImpl sym
mem
  | MemOptions -> Bool
laxLoadsAndStores ?memOpts::MemOptions
MemOptions
?memOpts
  , MemOptions -> IndeterminateLoadBehavior
indeterminateLoadBehavior ?memOpts::MemOptions
MemOptions
?memOpts IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool
forall a. Eq a => a -> a -> Bool
== IndeterminateLoadBehavior
StableSymbolic

  =  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
        SymExpr
  sym
  ('BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) ('BaseBVType 8))
bytes <- sym
-> SolverSymbol
-> BaseTypeRepr
     ('BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) ('BaseBVType 8))
-> IO
     (SymExpr
        sym
        ('BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) ('BaseBVType 8)))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol
                    (Assignment BaseTypeRepr (EmptyCtx ::> 'BaseBVType wptr)
-> BaseTypeRepr ('BaseBVType 8)
-> BaseTypeRepr
     ('BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) ('BaseBVType 8))
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr (BaseTypeRepr ('BaseBVType wptr)
-> Assignment BaseTypeRepr (EmptyCtx ::> 'BaseBVType wptr)
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton (BaseTypeRepr ('BaseBVType wptr)
 -> Assignment BaseTypeRepr (EmptyCtx ::> 'BaseBVType wptr))
-> BaseTypeRepr ('BaseBVType wptr)
-> Assignment BaseTypeRepr (EmptyCtx ::> 'BaseBVType wptr)
forall a b. (a -> b) -> a -> b
$ NatRepr wptr -> BaseTypeRepr ('BaseBVType wptr)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth)
                        (NatRepr 8 -> BaseTypeRepr ('BaseBVType 8)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8)))
        let dl :: DataLayout
dl = TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc
        let sz :: Bytes
sz = DataLayout -> MemType -> Bytes
memTypeSize DataLayout
dl MemType
memty
        let tyAlign :: Alignment
tyAlign = DataLayout -> MemType -> Alignment
memTypeAlign DataLayout
dl MemType
memty
        SymExpr sym ('BaseBVType wptr)
sz' <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym ('BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (NatRepr wptr -> Bytes -> BV wptr
forall (w :: Natural). NatRepr w -> Bytes -> BV w
bytesToBV NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth Bytes
sz)
        LLVMPointer sym wptr
ptr <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem (Global -> Symbol
L.globalSym Global
gl)
        bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Alignment
-> SymExpr
     sym
     ('BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) ('BaseBVType 8))
-> SymExpr sym ('BaseBVType wptr)
-> IO (MemImpl sym)
forall sym bak (w :: Natural).
(IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym) =>
bak
-> MemImpl sym
-> LLVMPtr sym w
-> Alignment
-> SymArray sym (SingleCtx (BaseBVType w)) ('BaseBVType 8)
-> SymBV sym w
-> IO (MemImpl sym)
doArrayConstStore bak
bak MemImpl sym
mem LLVMPtr sym wptr
LLVMPointer sym wptr
ptr Alignment
tyAlign SymExpr
  sym
  ('BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) ('BaseBVType 8))
bytes SymExpr sym ('BaseBVType wptr)
sz'

  | Bool
otherwise = MemImpl sym -> IO (MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MemImpl sym
mem


-- | Write the value of the given LLVMConst into the given global variable.
--   This is intended to be used at initialization time, and will populate
--   even read-only global data.
populateGlobal :: forall sym bak wptr.
  ( ?lc :: TypeContext
  , 16 <= wptr
  , HasPtrWidth wptr
  , IsSymBackend sym bak
  , HasLLVMAnn sym
  , ?memOpts :: MemOptions
  , HasCallStack
  ) =>
  bak ->
  L.Global {- ^ The global to populate -} ->
  MemType {- ^ Type of the global -} ->
  LLVMConst {- ^ Constant value to initialize with -} ->
  GlobalInitializerMap ->
  MemImpl sym ->
  IO (MemImpl sym)
populateGlobal :: forall sym bak (wptr :: Natural).
(?lc::TypeContext, 16 <= wptr, HasPtrWidth wptr,
 IsSymBackend sym bak, HasLLVMAnn sym, ?memOpts::MemOptions,
 HasCallStack) =>
bak
-> Global
-> MemType
-> LLVMConst
-> GlobalInitializerMap
-> MemImpl sym
-> IO (MemImpl sym)
populateGlobal bak
bak Global
gl MemType
memty LLVMConst
cval GlobalInitializerMap
giMap MemImpl sym
mem =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     let alignment :: Alignment
alignment = DataLayout -> MemType -> Alignment
memTypeAlign (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) MemType
memty

     -- So that globals can populate and look up the globals they reference
     -- during initialization
     let populateRec :: HasCallStack
                     => L.Symbol -> StateT (MemImpl sym) IO (LLVMPtr sym wptr)
         populateRec :: HasCallStack =>
Symbol -> StateT (MemImpl sym) IO (LLVMPtr sym wptr)
populateRec Symbol
symbol = do
           MemImpl sym
memimpl0 <- StateT (MemImpl sym) IO (MemImpl sym)
forall s (m :: Type -> Type). MonadState s m => m s
get
           MemImpl sym
memimpl <-
            case Symbol -> Map Symbol (SomePointer sym) -> Maybe (SomePointer sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
symbol (MemImpl sym -> Map Symbol (SomePointer sym)
forall sym. MemImpl sym -> GlobalMap sym
memImplGlobalMap MemImpl sym
mem) of
              Just SomePointer sym
_  -> MemImpl sym -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. a -> StateT (MemImpl sym) IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure MemImpl sym
memimpl0 -- We already populated this one
              Maybe (SomePointer sym)
Nothing ->
                -- For explanations of the various modes of failure, see the
                -- comment on 'GlobalInitializerMap'.
                case Symbol
-> GlobalInitializerMap
-> Maybe (Global, Either [Char] (MemType, Maybe LLVMConst))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
symbol GlobalInitializerMap
giMap of
                  Maybe (Global, Either [Char] (MemType, Maybe LLVMConst))
Nothing -> [Char] -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. [Char] -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> StateT (MemImpl sym) IO (MemImpl sym))
-> [Char] -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
                    [ [Char]
"Couldn't find global variable: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
symbol ]
                  Just (Global
glob, Left [Char]
str) -> [Char] -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. [Char] -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> StateT (MemImpl sym) IO (MemImpl sym))
-> [Char] -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
                    [ [Char]
"Couldn't find global variable's initializer: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                        Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
symbol
                    , [Char]
"Reason:"
                    , [Char]
str
                    , [Char]
"Full definition:"
                    , Global -> [Char]
forall a. Show a => a -> [Char]
show Global
glob
                    ]
                  Just (Global
glob, Right (MemType
_, Maybe LLVMConst
Nothing)) -> [Char] -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. [Char] -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> StateT (MemImpl sym) IO (MemImpl sym))
-> [Char] -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
                    [ [Char]
"Global was not a compile-time constant:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
symbol
                    , [Char]
"Full definition:"
                    , Global -> [Char]
forall a. Show a => a -> [Char]
show Global
glob
                    ]
                  Just (Global
glob, Right (MemType
memty_, Just LLVMConst
cval_)) ->
                    IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym))
-> IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> Global
-> MemType
-> LLVMConst
-> GlobalInitializerMap
-> MemImpl sym
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(?lc::TypeContext, 16 <= wptr, HasPtrWidth wptr,
 IsSymBackend sym bak, HasLLVMAnn sym, ?memOpts::MemOptions,
 HasCallStack) =>
bak
-> Global
-> MemType
-> LLVMConst
-> GlobalInitializerMap
-> MemImpl sym
-> IO (MemImpl sym)
populateGlobal bak
bak Global
glob MemType
memty_ LLVMConst
cval_ GlobalInitializerMap
giMap MemImpl sym
memimpl0
           MemImpl sym -> StateT (MemImpl sym) IO ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put MemImpl sym
memimpl
           IO (LLVMPointer sym wptr)
-> StateT (MemImpl sym) IO (LLVMPointer sym wptr)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym wptr)
 -> StateT (MemImpl sym) IO (LLVMPointer sym wptr))
-> IO (LLVMPointer sym wptr)
-> StateT (MemImpl sym) IO (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
memimpl Symbol
symbol

     StorageType
ty <- MemType -> IO StorageType
forall (m :: Type -> Type) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
memty
     LLVMPointer sym wptr
ptr <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem (Global -> Symbol
L.globalSym Global
gl)
     (LLVMVal sym
val, MemImpl sym
mem') <- StateT (MemImpl sym) IO (LLVMVal sym)
-> MemImpl sym -> IO (LLVMVal sym, MemImpl sym)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT (sym
-> (Symbol -> StateT (MemImpl sym) IO (LLVMPtr sym wptr))
-> LLVMConst
-> StateT (MemImpl sym) IO (LLVMVal sym)
forall (wptr :: Natural) sym (io :: Type -> Type).
(MonadIO io, MonadFail io, HasPtrWidth wptr, IsSymInterface sym,
 HasCallStack) =>
sym
-> (Symbol -> io (LLVMPtr sym wptr))
-> LLVMConst
-> io (LLVMVal sym)
constToLLVMValP sym
sym HasCallStack =>
Symbol -> StateT (MemImpl sym) IO (LLVMPtr sym wptr)
Symbol -> StateT (MemImpl sym) IO (LLVMPtr sym wptr)
populateRec LLVMConst
cval) MemImpl sym
mem
     bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> LLVMVal sym
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> LLVMVal sym
-> IO (MemImpl sym)
storeConstRaw bak
bak MemImpl sym
mem' LLVMPtr sym wptr
LLVMPointer sym wptr
ptr StorageType
ty Alignment
alignment LLVMVal sym
val