Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.LLVM.Globals

Description

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 #

populateGlobal Source #

Arguments

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

populateGlobals Source #

Arguments

:: (?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).

registerFunPtr Source #

Arguments

:: (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.