------------------------------------------------------------------------
-- |
-- 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

  , 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', genericLength, isPrefixOf)
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           Data.Parameterized.NatRepr as NatRepr

import           Lang.Crucible.LLVM.Bytes
import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.Functions (allocLLVMFunPtrs)
import           Lang.Crucible.LLVM.MemType
import           Lang.Crucible.LLVM.MemModel
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
globalMap1 (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?

   globalMap0 :: Map Symbol Global
globalMap0 = [(Symbol, Global)] -> Map Symbol Global
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Symbol, Global)] -> Map Symbol Global)
-> [(Symbol, Global)] -> Map Symbol Global
forall a b. (a -> b) -> a -> b
$ (Global -> (Symbol, Global)) -> [Global] -> [(Symbol, Global)]
forall a b. (a -> b) -> [a] -> [b]
map (\Global
g -> (Global -> Symbol
L.globalSym Global
g, Global
g)) (Module -> [Global]
L.modGlobals Module
m)
   globalMap1 :: GlobalInitializerMap
globalMap1 = (Global -> (Global, Either [Char] (MemType, Maybe LLVMConst)))
-> Map Symbol Global -> GlobalInitializerMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (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) Map Symbol Global
globalMap0
   loadRelConstInitMap :: LoadRelConstInitMap
loadRelConstInitMap = Map Symbol Global -> Module -> LoadRelConstInitMap
buildLoadRelConstInitMap Map Symbol Global
globalMap0 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 (Type
gty, Maybe Value
mbGval) =
              -- Check if a global variable was passed as an argument to
              -- llvm.load.relative.i* (i.e., if it is reltable-like), and if
              -- so, use an altered value for the constant initializer that uses
              -- `bitcast`. See
              -- Note [Undoing LLVM's relative table lookup conversion pass].
              case Symbol -> LoadRelConstInitMap -> Maybe (Typed Value)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Global -> Symbol
L.globalSym Global
g) LoadRelConstInitMap
loadRelConstInitMap of
                Just (L.Typed Type
constInitTy Value
constInitVal) ->
                  (Type
constInitTy, Value -> Maybe Value
forall a. a -> Maybe a
Just Value
constInitVal)
                Maybe (Typed Value)
Nothing ->
                  (Global -> Type
L.globalType Global
g, 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
mbVal <- (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
mbGval
        (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
mbVal)

-------------------------------------------------------------------------
-- 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
   MemImpl sym
mem <- bak
-> LLVMContext arch -> MemImpl sym -> Module -> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch -> MemImpl sym -> Module -> IO (MemImpl sym)
allocLLVMFunPtrs bak
bak LLVMContext arch
llvm_ctx MemImpl sym
mem0 Module
llvmModl

   -- 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
   let globalMap :: Map Symbol Global
globalMap   = [(Symbol, Global)] -> Map Symbol Global
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Symbol, Global)] -> Map Symbol Global)
-> [(Symbol, Global)] -> Map Symbol Global
forall a b. (a -> b) -> a -> b
$ (Global -> (Symbol, Global)) -> [Global] -> [(Symbol, Global)]
forall a b. (a -> b) -> [a] -> [b]
map (\Global
g -> (Global -> Symbol
L.globalSym Global
g, Global
g)) [Global]
globals
   let loadRelConstInitMap :: LoadRelConstInitMap
loadRelConstInitMap = Map Symbol Global -> Module -> LoadRelConstInitMap
buildLoadRelConstInitMap Map Symbol Global
globalMap 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]
                        -- Check if a global variable was passed as an argument
                        -- to llvm.load.relative.i* (i.e., if it is
                        -- reltable-like), and if so, use an altered type that
                        -- uses pointers instead of `i32`s. Also, do not use the
                        -- original global's alignment. See
                        -- Note [Undoing LLVM's relative table lookup conversion pass].
                        (MemType
ty, Maybe Align
mbGlobAlign) <-
                          case Symbol -> LoadRelConstInitMap -> Maybe (Typed Value)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Global -> Symbol
L.globalSym Global
g) LoadRelConstInitMap
loadRelConstInitMap of
                            Just Typed Value
constInit -> do
                              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
$
                                    Typed Value -> Type
forall a. Typed a -> Type
L.typedType Typed Value
constInit
                              -- Return Nothing for the alignment so that we
                              -- will instead use crucible-llvm's alignment
                              -- inference to compute the alignment of the
                              -- new constant initializer.
                              (MemType, Maybe Align) -> IO (MemType, Maybe Align)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MemType
ty, Maybe Align
forall a. Maybe a
Nothing)
                            Maybe (Typed Value)
Nothing -> do
                              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
                              (MemType, Maybe Align) -> IO (MemType, Maybe Align)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MemType
ty, Global -> Maybe Align
L.globalAlign 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 Maybe Align
mbGlobAlign 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


------------------------------------------------------------------------
-- ** 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

------------------------------------------------------------------------
-- ** llvm.load.relative constant initializers

-- | A map of global variable names ('L.Symbol's) that appear as arguments to
-- calls to the @llvm.load.relative.i*@ intrinsic. See
-- @Note [Undoing LLVM's relative table lookup conversion pass]@ for why we need
-- this.
type LoadRelConstInitMap = Map L.Symbol (L.Typed L.Value)

-- | @buildLoadRelConstInitMap globalMap m@ takes a 'L.Module' (@m@) and a map
-- of global variable symbols to their definitions (@globalMap@) and computes
-- a 'LoadRelConstInitMap'. See
-- @Note [Undoing LLVM's relative table lookup conversion pass]@ for why we need
-- to do this.
buildLoadRelConstInitMap ::
  Map L.Symbol L.Global ->
  L.Module ->
  LoadRelConstInitMap
buildLoadRelConstInitMap :: Map Symbol Global -> Module -> LoadRelConstInitMap
buildLoadRelConstInitMap Map Symbol Global
globalMap Module
m = (Define -> LoadRelConstInitMap) -> [Define] -> LoadRelConstInitMap
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Define -> LoadRelConstInitMap
defineConstInits (Module -> [Define]
L.modDefines Module
m)
  where
    defineConstInits :: L.Define -> LoadRelConstInitMap
    defineConstInits :: Define -> LoadRelConstInitMap
defineConstInits Define
def = (BasicBlock -> LoadRelConstInitMap)
-> [BasicBlock] -> LoadRelConstInitMap
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap BasicBlock -> LoadRelConstInitMap
basicBlockConstInits (Define -> [BasicBlock]
L.defBody Define
def)

    basicBlockConstInits :: L.BasicBlock -> LoadRelConstInitMap
    basicBlockConstInits :: BasicBlock -> LoadRelConstInitMap
basicBlockConstInits BasicBlock
bb = (Stmt -> LoadRelConstInitMap) -> [Stmt] -> LoadRelConstInitMap
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Stmt -> LoadRelConstInitMap
stmtConstInits (BasicBlock -> [Stmt]
forall lab. BasicBlock' lab -> [Stmt' lab]
L.bbStmts BasicBlock
bb)

    stmtConstInits :: L.Stmt -> LoadRelConstInitMap
    stmtConstInits :: Stmt -> LoadRelConstInitMap
stmtConstInits (L.Result Ident
_ Instr' BlockLabel
instr [([Char], ValMd' BlockLabel)]
_) = Instr' BlockLabel -> LoadRelConstInitMap
instrConstInits Instr' BlockLabel
instr
    stmtConstInits (L.Effect Instr' BlockLabel
instr [([Char], ValMd' BlockLabel)]
_)   = Instr' BlockLabel -> LoadRelConstInitMap
instrConstInits Instr' BlockLabel
instr

    instrConstInits :: L.Instr -> LoadRelConstInitMap
    instrConstInits :: Instr' BlockLabel -> LoadRelConstInitMap
instrConstInits (L.Call Bool
_ Type
_ (L.ValSymbol Symbol
fun) [Typed Value
ptr, Typed Value
_offset])
      | L.Symbol [Char]
funStr <- Symbol
fun
      , [Char]
"llvm.load.relative.i" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
funStr
      , Just (Symbol
gs, Type
foldedConstTy, Value
foldedConstInit) <-
          Value -> Maybe (Symbol, Type, Value)
foldLoadRelConstInit (Typed Value -> Value
forall a. Typed a -> a
L.typedValue Typed Value
ptr)
      = Symbol -> Typed Value -> LoadRelConstInitMap
forall k a. k -> a -> Map k a
Map.singleton Symbol
gs (Type -> Value -> Typed Value
forall a. Type -> a -> Typed a
L.Typed Type
foldedConstTy Value
foldedConstInit)
    instrConstInits Instr' BlockLabel
_ =
      LoadRelConstInitMap
forall k a. Map k a
Map.empty

    -- Check if the first argument to a call to llvm.load.relative.i* is
    -- "reltable-like", and if so, return @Just (symb, ty, val)@, where:
    --
    -- - @symb@ is the name of the global variable corresponding to the
    --   argument.
    --
    -- - @ty@ is the type of the global variable's new constant initializer.
    --
    -- - @val@ is the new constant initializer value.
    --
    -- See Note [Undoing LLVM's relative table lookup conversion pass] for an
    -- explanation of what "reltable-like" means.
    foldLoadRelConstInit :: L.Value -> Maybe (L.Symbol, L.Type, L.Value)
    foldLoadRelConstInit :: Value -> Maybe (Symbol, Type, Value)
foldLoadRelConstInit (L.ValSymbol Symbol
s)
      | Just Global
global <- Symbol -> Map Symbol Global -> Maybe Global
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s Map Symbol Global
globalMap
      , Just Value
constInit <- Global -> Maybe Value
L.globalValue Global
global
      -- Check that the type of the global variable is
      -- [<constInitElems> x i32].
      , L.ValArray (L.PrimType (L.Integer Word32
32)) [Value]
constInitElems <- Value
constInit
      , Just [Value]
foldedConstInitElems <-
          (Value -> Maybe Value) -> [Value] -> Maybe [Value]
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) -> [a] -> f [b]
traverse (Global -> Value -> Maybe Value
foldLoadRelConstInitElem Global
global) [Value]
constInitElems
      = (Symbol, Type, Value) -> Maybe (Symbol, Type, Value)
forall a. a -> Maybe a
Just ( Global -> Symbol
L.globalSym Global
global
             , Word64 -> Type -> Type
forall ident. Word64 -> Type' ident -> Type' ident
L.Array ([Value] -> Word64
forall i a. Num i => [a] -> i
genericLength [Value]
constInitElems) Type
ptrToI8Type
             , Type -> [Value] -> Value
forall lab. Type -> [Value' lab] -> Value' lab
L.ValArray Type
ptrToI8Type [Value]
foldedConstInitElems
             )
    foldLoadRelConstInit (L.ValConstExpr (L.ConstConv ConvOp
L.BitCast Typed Value
tv Type
_)) =
      Value -> Maybe (Symbol, Type, Value)
foldLoadRelConstInit (Typed Value -> Value
forall a. Typed a -> a
L.typedValue Typed Value
tv)
    foldLoadRelConstInit Value
_ =
      Maybe (Symbol, Type, Value)
forall a. Maybe a
Nothing

    -- Check that an element of a constant initializer is of the form
    -- `trunc(ptrtoint x - ptrtoint p)`, and if so, return `Just x`. Otherwise,
    -- return Nothing.
    foldLoadRelConstInitElem :: L.Global -> L.Value -> Maybe L.Value
    foldLoadRelConstInitElem :: Global -> Value -> Maybe Value
foldLoadRelConstInitElem Global
global Value
constInitElem
      | L.ValConstExpr
          (L.ConstConv ConvOp
L.Trunc
            (L.Typed { typedValue :: forall a. Typed a -> a
L.typedValue =
              L.ValConstExpr
                (L.ConstArith
                  (L.Sub Bool
_ Bool
_)
                  (L.Typed { typedValue :: forall a. Typed a -> a
L.typedValue =
                    L.ValConstExpr (L.ConstConv ConvOp
L.PtrToInt Typed Value
x Type
_) })
                  (L.ValConstExpr (L.ConstConv ConvOp
L.PtrToInt Typed Value
p Type
_))) })
            Type
_truncTy) <- Value
constInitElem
      , L.ValSymbol Symbol
pSym <- Typed Value -> Value
forall a. Typed a -> a
L.typedValue Typed Value
p
      , Global -> Symbol
L.globalSym Global
global Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
pSym
      = Value -> Maybe Value
forall a. a -> Maybe a
Just (ConstExpr' BlockLabel -> Value
forall lab. ConstExpr' lab -> Value' lab
L.ValConstExpr (ConvOp -> Typed Value -> Type -> ConstExpr' BlockLabel
forall lab. ConvOp -> Typed (Value' lab) -> Type -> ConstExpr' lab
L.ConstConv ConvOp
L.BitCast Typed Value
x Type
ptrToI8Type))

      | Bool
otherwise
      = Maybe Value
forall a. Maybe a
Nothing

    -- Type type i8*.
    ptrToI8Type :: L.Type
    ptrToI8Type :: Type
ptrToI8Type = Type -> Type
forall ident. Type' ident -> Type' ident
L.PtrTo (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (PrimType -> Type) -> PrimType -> Type
forall a b. (a -> b) -> a -> b
$ Word32 -> PrimType
L.Integer Word32
8

{-
Note [Undoing LLVM's relative table lookup conversion pass]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Clang 14.0.0+ include a `rel-lookup-table-converter` optimization pass that is
enabled with -O1 or greater. This optimization usually applies to code that
looks like table lookups. For instance, this pass would take this C code:

  const char *F(int tag) {
    static const char *const table[] = {
      "A",
      "B",
    };

    return table[tag];
  }

And optimize it to LLVM bitcode that looks like this:

  @reltable.F = internal unnamed_addr constant [2 x i32] [i32 trunc (i64 sub (i64 ptrtoint ([2 x i8]* @.str to i64), i64 ptrtoint ([2 x i32]* @reltable.F to i64)) to i32), i32 trunc (i64 sub (i64 ptrtoint ([2 x i8]* @.str.1 to i64), i64 ptrtoint ([2 x i32]* @reltable.F to i64)) to i32)], align 4
  @.str = private unnamed_addr constant [2 x i8] c"A\00", align 1
  @.str.1 = private unnamed_addr constant [2 x i8] c"B\00", align 1

  define dso_local i8* @F(i32 noundef %0) local_unnamed_addr #0 {
    %2 = sext i32 %0 to i64
    %3 = shl i64 %2, 2
    %4 = call i8* @llvm.load.relative.i64(i8* bitcast ([2 x i32]* @reltable.F to i8*), i64 %3)
    ret i8* %4
  }

There are several remarkable things about this LLVM bitcode:

* The definition of @F is backed up a relative lookup table @reltable.F.
  Invoking @F is tantamount to looking up a value in the table by using the
  special @llvm.load.relative.i* intrinsic, which is described here:
  https://releases.llvm.org/17.0.1/docs/LangRef.html#llvm-load-relative-intrinsic

* The definition of @reltable.F itself is quite unorthodox. Conceptually, it is
  an array of strings (@.str and @.str1), but where each element of the array
  contains the relative offset of the string to the table itself. As a result,
  it is not an array of pointers, but rather an array of i32s!

* Each i32 in the array consists of the address of each string represented as an
  integer (obtained via ptrtoint) subtracted from the address of the table,
  followed by a trunc to ensure the result fits in an i32. (One weird result of
  this encoding is that @reltable.F is defined recursively in terms of itself.)

This optimization pass is handy for Clang's purposes, as it allows Clang to
produce more efficient assembly code. Unfortunately, this encoding is quite
problematic for crucible-llvm. The problem ultimately lies in the fact that we
are performing pointer arithmetic on pointers from completely different
allocation regions (e.g., subtracting @reltable.F from @.str), which
crucible-llvm has no ability to reason about. (This optimization is also
problematic for CHERI, which tracks pointer provenance in a similar way—see
https://github.com/CTSRD-CHERI/llvm-project/issues/572).

What's more, we don't have a reliable way of avoiding this optimization, as
Clang's optimization pass manager doesn't provide a way to disable individual
passes via command-line arguments. We could tell users to downgrade from -O1
from -O0, but this would be a pretty severe workaround.

Our solution is to manually "undo" the optimization ourselves. That is, we
replace the definition of @reltable.F with bitcode that looks like this:

  @reltable.F = internal unnamed_addr constant [2 x i8*] [i8* bitcast ([2 x i8]* @.str to i8*), i8* bitcast ([2 x i8]* @.str.1 to i8*)]

This avoids any problematic uses of pointer arithmetic altogether. Here is how
we do this:

1. When processing global definitions in an LLVM module, we identify the names
   of all globals that are passed as the first argument to
   @llvm.load.relative.i*. We'll refer to these as "reltable-like" globals.

   This check assumes that the globals are passed directly to
   @llvm.load.relative.i*, rather than going through any intermediate
   variables. This is likely a safe assumption to make, considering that
   Clang's -O1 settings will usually optimize away any such intermediate
   variables.

2. For each reltable-like global, we check that the global has a constant
   initializer of type [<N> x i32] where each element is of the form
   `trunc (ptrtoint x - ptrtoint p)`. This is somewhat fragile, but the
   documentation for llvm.load.relative.i* implies that LLVM itself checks
   for code that looks like this, so we follow suit.

3. For each element in the constant initializer array, we turn
   `trunc (ptrtoint x - ptrtoint p)` into `bitcast x to i8*`. Note that the
   this changes its type from `i32` to `i8*`.

4. When translating a global definition to Crucible, we check if the global
   is reltable-like. If so, we replace its constant initializer with the
   `bitcast`ed version. We must also make sure that the global is translated
   at type `[<N> x i8*]` rather than `[<N> x i32]`.

   Furthermore, we must also make sure not to use the original global's
   alignment, as the `bitcast`ed version will almost certainly have different
   alignment requirements. We rely on crucible-llvm's alignment inference to
   figure out what the new alignment should be.

5. In the override for llvm.load.relative.i*, we make sure to adjust the second
   argument (the pointer offset). This is because LLVM assumes that the offset
   is for something of type `[<N> x i32]`, so an offset value of 4 (four bytes)
   refers to the first element, an offset value of 8 refers to the second
   element, and so on. On the other hand, something of type `[<N> x i8*]` will
   likely require different offsets, since the size of a pointer may be greater
   than four bytes (e.g., it is eight bytes on 64-bit architectures).

   To account for this difference, we divide the offset value by 4 and then
   multiply it by the number of bytes in the size of a pointer.

It is worth emphasizing that this is a very ad hoc workaround. At the same time,
it is likely the best we can do without substantially changing how crucible-llvm
tracks pointer provenance.
-}