crucible-llvm-0.9: src/Lang/Crucible/LLVM/Globals.hs
------------------------------------------------------------------------
-- |
-- 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 qualified Data.Foldable as Foldable
import Data.List (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 ctx m = Foldable.foldl' addAliases globalMap1 (Map.toList (llvmGlobalAliases ctx))
where
addAliases mp (glob, aliases) =
case Map.lookup glob mp of
Just initzr -> insertAll (map L.aliasName (Set.toList aliases)) initzr mp
Nothing -> mp -- should this be an error/exception?
globalMap0 = Map.fromList $ map (\g -> (L.globalSym g, g)) (L.modGlobals m)
globalMap1 = Map.map (id &&& globalToConst) globalMap0
loadRelConstInitMap = buildLoadRelConstInitMap globalMap0 m
insertAll ks v mp = foldr (flip Map.insert v) mp ks
-- Catch the error from @transConstant@, turn it into @Either@
globalToConst :: L.Global -> Either String (MemType, Maybe LLVMConst)
globalToConst g =
catchError
(globalToConst' g)
(\err -> Left $
"Encountered error while processing global "
++ show (LPP.ppSymbol (L.globalSym g))
++ ": "
++ err)
globalToConst' :: forall m. (MonadError String m)
=> L.Global -> m (MemType, Maybe LLVMConst)
globalToConst' g =
do let ?lc = ctx^.llvmTypeCtx -- implicitly passed to transConstant
let (gty, 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 Map.lookup (L.globalSym g) loadRelConstInitMap of
Just (L.Typed constInitTy constInitVal) ->
(constInitTy, Just constInitVal)
Nothing ->
(L.globalType g, L.globalValue g)
mt <- liftMemType gty
mbVal <- traverse (transConstant' mt) mbGval
return (mt, 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 = initializeMemory (const True)
initializeMemoryConstGlobals
:: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> bak
-> LLVMContext arch
-> L.Module
-> IO (MemImpl sym)
initializeMemoryConstGlobals = initializeMemory (L.gaConstant . L.globalAttrs)
initializeMemory
:: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> (L.Global -> Bool)
-> bak
-> LLVMContext arch
-> L.Module
-> IO (MemImpl sym)
initializeMemory predicate bak llvm_ctx llvmModl = do
-- Create initial memory of appropriate endianness
let ?lc = llvm_ctx^.llvmTypeCtx
let dl = llvmDataLayout ?lc
let endianness = dl^.intLayout
mem0 <- emptyMem endianness
-- allocate pointers values for function symbols, but do not yet bind them to
-- function handles
mem <- allocLLVMFunPtrs bak llvm_ctx mem0 llvmModl
-- Allocate global values
let globAliases = llvmGlobalAliases llvm_ctx
let globals = L.modGlobals llvmModl
let globalMap = Map.fromList $ map (\g -> (L.globalSym g, g)) globals
let loadRelConstInitMap = buildLoadRelConstInitMap globalMap llvmModl
gs_alloc <- mapM (\g -> do
let err msg = malformedLLVMModule
("Invalid type for global" <> fromString (show (L.globalSym g)))
[fromString 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].
(ty, mbGlobAlign) <-
case Map.lookup (L.globalSym g) loadRelConstInitMap of
Just constInit -> do
ty <- either err return $
liftMemType $
L.typedType 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.
pure (ty, Nothing)
Nothing -> do
ty <- either err return $ liftMemType $ L.globalType g
pure (ty, L.globalAlign g)
let sz = memTypeSize dl ty
let tyAlign = memTypeAlign dl ty
let aliases = map L.aliasName . Set.toList $
fromMaybe Set.empty (Map.lookup (L.globalSym g) 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 <-
case mbGlobAlign of
Just a | a > 0 ->
case toAlignment (toBytes a) of
Nothing -> fail $ "Invalid alignemnt: " ++ show a ++ "\n " ++
"specified for global: " ++ show (L.globalSym g)
Just al -> return al
_ -> return tyAlign
return (g, aliases, sz, alignment))
globals
allocGlobals bak (filter (\(g, _, _, _) -> predicate g) gs_alloc) 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 select bak gimap mem0 = foldM f mem0 (Map.elems gimap)
where
f mem (gl, _) | not (select gl) = return mem
f _ (_, Left msg) = fail msg
f mem (gl, Right (mty, Just cval)) = populateGlobal bak gl mty cval gimap mem
f mem (gl, Right (mty, Nothing)) = populateExternalGlobal bak gl mty 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 = populateGlobals (const 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 = populateGlobals f
where f = L.gaConstant . 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 bak gl memty mem
| laxLoadsAndStores ?memOpts
, indeterminateLoadBehavior ?memOpts == StableSymbolic
= do let sym = backendGetSym bak
bytes <- freshConstant sym emptySymbol
(BaseArrayRepr (Ctx.singleton $ BaseBVRepr ?ptrWidth)
(BaseBVRepr (knownNat @8)))
let dl = llvmDataLayout ?lc
let sz = memTypeSize dl memty
let tyAlign = memTypeAlign dl memty
sz' <- bvLit sym PtrWidth (bytesToBV PtrWidth sz)
ptr <- doResolveGlobal bak mem (L.globalSym gl)
doArrayConstStore bak mem ptr tyAlign bytes sz'
| otherwise = return 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 bak gl memty cval giMap mem =
do let sym = backendGetSym bak
let alignment = memTypeAlign (llvmDataLayout ?lc) 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 symbol = do
memimpl0 <- get
memimpl <-
case Map.lookup symbol (memImplGlobalMap mem) of
Just _ -> pure memimpl0 -- We already populated this one
Nothing ->
-- For explanations of the various modes of failure, see the
-- comment on 'GlobalInitializerMap'.
case Map.lookup symbol giMap of
Nothing -> fail $ unlines $
[ "Couldn't find global variable: " ++ show symbol ]
Just (glob, Left str) -> fail $ unlines $
[ "Couldn't find global variable's initializer: " ++
show symbol
, "Reason:"
, str
, "Full definition:"
, show glob
]
Just (glob, Right (_, Nothing)) -> fail $ unlines $
[ "Global was not a compile-time constant:" ++ show symbol
, "Full definition:"
, show glob
]
Just (glob, Right (memty_, Just cval_)) ->
liftIO $ populateGlobal bak glob memty_ cval_ giMap memimpl0
put memimpl
liftIO $ doResolveGlobal bak memimpl symbol
ty <- toStorableType memty
ptr <- doResolveGlobal bak mem (L.globalSym gl)
(val, mem') <- runStateT (constToLLVMValP sym populateRec cval) mem
storeConstRaw bak mem' ptr ty alignment 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 globalMap m = foldMap defineConstInits (L.modDefines m)
where
defineConstInits :: L.Define -> LoadRelConstInitMap
defineConstInits def = foldMap basicBlockConstInits (L.defBody def)
basicBlockConstInits :: L.BasicBlock -> LoadRelConstInitMap
basicBlockConstInits bb = foldMap stmtConstInits (L.bbStmts bb)
stmtConstInits :: L.Stmt -> LoadRelConstInitMap
stmtConstInits (L.Result _ instr _ _) = instrConstInits instr
stmtConstInits (L.Effect instr _ _) = instrConstInits instr
instrConstInits :: L.Instr -> LoadRelConstInitMap
instrConstInits (L.Call _ _ (L.ValSymbol fun) [ptr, _offset])
| L.Symbol funStr <- fun
, "llvm.load.relative.i" `isPrefixOf` funStr
, Just (gs, foldedConstTy, foldedConstInit) <-
foldLoadRelConstInit (L.typedValue ptr)
= Map.singleton gs (L.Typed foldedConstTy foldedConstInit)
instrConstInits _ =
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 (L.ValSymbol s)
| Just global <- Map.lookup s globalMap
, Just constInit <- L.globalValue global
-- Check that the type of the global variable is
-- [<constInitElems> x i32].
, L.ValArray (L.PrimType (L.Integer 32)) constInitElems <- constInit
, Just foldedConstInitElems <-
traverse (foldLoadRelConstInitElem global) constInitElems
= Just ( L.globalSym global
, L.Array (genericLength constInitElems) ptrToI8Type
, L.ValArray ptrToI8Type foldedConstInitElems
)
foldLoadRelConstInit (L.ValConstExpr (L.ConstConv L.BitCast tv _)) =
foldLoadRelConstInit (L.typedValue tv)
foldLoadRelConstInit _ =
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 constInitElem
| L.ValConstExpr
(L.ConstConv
(L.Trunc False False)
(L.Typed { L.typedValue =
L.ValConstExpr
(L.ConstArith
(L.Sub _ _)
(L.Typed { L.typedValue =
L.ValConstExpr (L.ConstConv L.PtrToInt x _) })
(L.ValConstExpr (L.ConstConv L.PtrToInt p _))) })
_truncTy) <- constInitElem
, L.ValSymbol pSym <- L.typedValue p
, L.globalSym global == pSym
= Just (L.ValConstExpr (L.ConstConv L.BitCast x ptrToI8Type))
| otherwise
= Nothing
-- Type type i8*.
ptrToI8Type :: L.Type
ptrToI8Type = L.PtrTo $ L.PrimType $ L.Integer 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.
-}