Copyright | (c) Galois Inc 2018 |
---|---|
License | BSD3 |
Maintainer | Rob Dockins <rdockins@galois.com> |
Stability | provisional |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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.
Synopsis
- initializeMemory :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => (Global -> Bool) -> bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
- initializeAllMemory :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
- initializeMemoryConstGlobals :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
- populateGlobal :: forall sym bak wptr. (?lc :: TypeContext, 16 <= wptr, HasPtrWidth wptr, IsSymBackend sym bak, HasLLVMAnn sym, ?memOpts :: MemOptions, HasCallStack) => bak -> Global -> MemType -> LLVMConst -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
- populateGlobals :: (?lc :: TypeContext, ?memOpts :: MemOptions, 16 <= wptr, HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) => (Global -> Bool) -> bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
- populateAllGlobals :: (?lc :: TypeContext, ?memOpts :: MemOptions, 16 <= wptr, HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) => bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
- populateConstGlobals :: (?lc :: TypeContext, ?memOpts :: MemOptions, 16 <= wptr, HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) => bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
- registerFunPtr :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> MemImpl sym -> String -> Symbol -> [Symbol] -> IO (LLVMPtr sym wptr, MemImpl sym)
- type GlobalInitializerMap = Map Symbol (Global, Either String (MemType, Maybe LLVMConst))
- makeGlobalMap :: forall arch wptr. (?lc :: TypeContext, HasPtrWidth wptr) => LLVMContext arch -> Module -> GlobalInitializerMap
Documentation
initializeMemory :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => (Global -> Bool) -> bak -> LLVMContext arch -> Module -> IO (MemImpl sym) Source #
initializeAllMemory :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> LLVMContext arch -> Module -> IO (MemImpl sym) Source #
Build the initial memory for an LLVM program. Note, this process allocates space for global variables, but does not set their initial values.
initializeMemoryConstGlobals :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> LLVMContext arch -> Module -> IO (MemImpl sym) Source #
:: forall sym bak wptr. (?lc :: TypeContext, 16 <= wptr, HasPtrWidth wptr, IsSymBackend sym bak, HasLLVMAnn sym, ?memOpts :: MemOptions, HasCallStack) | |
=> bak | |
-> Global | The global to populate |
-> MemType | Type of the global |
-> LLVMConst | Constant value to initialize with |
-> GlobalInitializerMap | |
-> MemImpl sym | |
-> IO (MemImpl sym) |
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.
:: (?lc :: TypeContext, ?memOpts :: MemOptions, 16 <= wptr, HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) | |
=> (Global -> Bool) | Filter function, globals that cause this to return true will be populated |
-> bak | |
-> GlobalInitializerMap | |
-> MemImpl sym | |
-> IO (MemImpl sym) |
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.
populateAllGlobals :: (?lc :: TypeContext, ?memOpts :: MemOptions, 16 <= wptr, HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) => bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym) Source #
Populate all the globals mentioned in the given GlobalInitializerMap
.
populateConstGlobals :: (?lc :: TypeContext, ?memOpts :: MemOptions, 16 <= wptr, HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) => bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym) Source #
Populate only the constant global variables mentioned in the
given GlobalInitializerMap
(and any they transitively refer to).
:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) | |
=> bak | |
-> MemImpl sym | |
-> String | Display name |
-> Symbol | Function name |
-> [Symbol] | Aliases |
-> IO (LLVMPtr sym wptr, MemImpl sym) |
Create a global allocation assocated with a function
type GlobalInitializerMap = Map Symbol (Global, Either String (MemType, Maybe LLVMConst)) Source #
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
.
makeGlobalMap :: forall arch wptr. (?lc :: TypeContext, HasPtrWidth wptr) => LLVMContext arch -> Module -> GlobalInitializerMap Source #
makeGlobalMap
creates a map from names of LLVM global variables
to the values of their initializers, if any are included in the module.