Lang.Crucible.LLVM.MemModel

Memories

type Mem = IntrinsicType "LLVM_memory" EmptyCtx

The CrucibleType of an LLVM memory. RegValue sym Mem is implemented as MemImpl sym.

memRepr :: TypeRepr Mem

mkMemVar :: Text -> HandleAllocator -> IO (GlobalVar Mem)

data MemImpl sym

The implementation of an LLVM memory, containing an allocation-block source, global map, handle map, and heap.

Constructors

MemImpl

Fields

• memImplBlockSource :: BlockSource
• memImplGlobalMap :: GlobalMap sym
• memImplSymbolMap :: Map Natural Symbol
• memImplHandleMap :: Map Natural Dynamic
• memImplHeap :: Mem sym

data SomePointer sym

A pointer with an existentially-quantified width

Constructors

forall w.1 <= w => SomePointer !(LLVMPtr sym w)

type GlobalMap sym = Map Symbol (SomePointer sym)

emptyMem :: EndianForm -> IO (MemImpl sym)

Produce a fresh empty memory. NB, we start counting allocation blocks at '1'. Block number 0 is reserved for representing raw bitvectors.

memEndian :: MemImpl sym -> EndianForm

memAllocCount :: MemImpl sym -> Int

memWriteCount :: MemImpl sym -> Int

ppMem :: IsExpr (SymExpr sym) => Mem sym -> Doc ann

doDumpMem :: IsExprBuilder sym => Handle -> MemImpl sym -> IO ()

Pretty print a memory state to the given handle.

newtype BlockSource

Constructors

BlockSource (IORef Natural)

nextBlock :: BlockSource -> IO Natural

data MemOptions

This datatype encodes a variety of tweakable settings supported by the LLVM memory model. They generally involve some weakening of the strict rules of the language standard to allow common idioms, at the cost that reasoning using the resulting memory model is less generalizable (i.e., makes more assumptions about the runtime behavior of the system).

Constructors

MemOptions

Fields

• laxPointerOrdering :: !Bool

  Should we allow ordering comparisons on pointers that are not from the same allocation unit? This is not allowed by the C standard, but is nonetheless commonly done.

• laxConstantEquality :: !Bool

  Should we allow equality comparisons on pointers to constant data? Different symbols with the same data are allowed to be consolidated, so pointer apparently-distinct pointers will sometimes compare equal if the compiler decides to consolidate their storage.

• laxLoadsAndStores :: !Bool

  Should we relax some of Crucible's validity checks for memory loads and stores? If True, the following checks will be relaxed:

  • Reading from previously unwritten memory will succeed rather than throwing a NoSatisfyingWrite error. The semantics of what it means to read from uninitialized memory is controlled separately by the indeterminateLoadBehavior option.
  • If reading from a region that isn't allocated or isn't large enough, Crucible will proceed rather than throw an UnreadableRegion error.
  • Reading a value from a pointer with insufficent alignment is not treated as undefined behavior. That is, Crucible will not throw a ReadBadAlignment error.
  • Adding an offset to a pointer that results in a pointer to an address outside of the allocation is not treated as undefined behavior. That is, Crucible will not throw a PtrAddOffsetOutOfBounds error.

  This option is primarily useful for SV-COMP, which does not treat the scenarios listed above as fatal errors.

• indeterminateLoadBehavior :: IndeterminateLoadBehavior

  If laxLoadsAndStores is enabled, what should be the semantics of reading from uninitialized memory? See the Haddocks for IndeterminateLoadBehavior for an explanation of each possible semantics.

  If laxLoadsAndStores is disabled, this option has no effect.

• noSatisfyingWriteFreshConstant :: !Bool

  If True, for the NoSatisfyingWrite annotation, make a fresh constant as a proof obligation, which ensures it always fails. But, because it's a variable, it won't be constant-folded away and it's relatively sure the annotation will survive. If False, annotate false.

data IndeterminateLoadBehavior

What should be the semantics of reading from previously uninitialized memory?

Constructors

StableSymbolic

After allocating memory (be it through alloca, malloc, calloc, or a similar function), initialize it with a fresh symbolic value of the corresponding type. As a result, reading from "uninitialized" memory will always succeed, as uninitialized memory will contain symbolic data if it has not yet been written to. This is "stable" in the sense that reading from the same section of uninitialized memory multiple times will always yield the same symbolic value.

This is primarily useful for SV-COMP, as these semantics closely align with SV-COMP's expectations.

UnstableSymbolic

Each read from a section of uninitialized memory will return a fresh symbolic value of the corresponding type. The operative word is "fresh", as each of these symbolic values will be considered distinct. That is, the symbolic values are "unstable". Contrast this with StableSymbolic, in which multiple reads from the same section of uninitialized memory will all yield the same symbolic value.

One consequence of the UnstableSymbolic approach is that any pointer can be derefenced, even if it does not actually point to anything. Dereferencing such a pointer will simply yield a fresh symbolic value. On the other hand, dereferencing such a pointer continues to be a Crucible error in StableSymbolic.

Instances

Show IndeterminateLoadBehavior

Defined in Lang.Crucible.LLVM.MemModel.Options

Methods

showsPrec :: Int -> IndeterminateLoadBehavior -> ShowS

show :: IndeterminateLoadBehavior -> String

showList :: [IndeterminateLoadBehavior] -> ShowS

Eq IndeterminateLoadBehavior

Defined in Lang.Crucible.LLVM.MemModel.Options

Methods

(==) :: IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool

(/=) :: IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool

defaultMemOptions :: MemOptions

The default memory model options:

• Require strict adherence to the language standard regarding pointer equality and ordering.
• Perform Crucible's default validity checks for memory loads and stores.

laxPointerMemOptions :: MemOptions

Like defaultMemOptions, but allow pointer ordering comparisons and equality comparisons of pointers to constant data.

Pointers

type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)

Crucible type of pointers/bitvector values of width w.

pattern LLVMPointerRepr :: () => (1 <= w, ty ~ LLVMPointerType w) => NatRepr w -> TypeRepr ty

This pattern synonym makes it easy to build and destruct runtime representatives of LLVMPointerType w.

pattern PtrRepr :: HasPtrWidth wptr => ty ~ LLVMPointerType wptr => TypeRepr ty

This pattern creates/matches against the TypeRepr for LLVM pointer values that are of the distinguished pointer width.

pattern SizeT :: HasPtrWidth wptr => ty ~ BVType wptr => TypeRepr ty

This pattern creates/matches against the TypeRepr for raw bitvector values that are of the distinguished pointer width.

type LLVMPtr sym w = RegValue sym (LLVMPointerType w)

Symbolic LLVM pointer or bitvector values of width w.

pattern LLVMPointer :: SymNat sym -> SymBV sym w -> LLVMPointer sym w

A pointer is a base point offset.

llvmPointerView :: LLVMPtr sym w -> (SymNat sym, SymBV sym w)

Alternative to the LLVMPointer pattern synonym, this function can be used as a view constructor instead to silence incomplete pattern warnings.

ptrWidth :: IsExprBuilder sym => LLVMPtr sym w -> NatRepr w

Compute the width of a pointer value.

ppPtr :: IsExpr (SymExpr sym) => LLVMPtr sym wptr -> Doc ann

ppTermExpr :: forall sym ann. IsExpr (SymExpr sym) => LLVMVal sym -> Doc ann

llvmPointer_bv :: IsSymInterface sym => sym -> SymBV sym w -> IO (LLVMPtr sym w)

Convert a raw bitvector value into an LLVM pointer value.

ptrToBv

Arguments

:: IsSymBackend sym bak

=> bak

-> SimErrorReason

Error to report if casting the pointer to a bitvector fails

-> LLVMPtr sym w

-> IO (SymBV sym w)

Assert that the given LLVM pointer value is actually a raw bitvector and extract its value.

projectLLVM_bv :: IsSymBackend sym bak => bak -> LLVMPtr sym w -> IO (SymBV sym w)

Assert that the given LLVM pointer value is actually a raw bitvector and extract its value.

Note that this assertion has a very generic message, which can be unhelpful to users when it fails. Consider using ptrToBv instead.

Memory operations

doMalloc

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> AllocType

stack, heap, or global

-> Mutability

whether region is read-only

-> String

source location for use in error messages

-> MemImpl sym

-> SymBV sym wptr

allocation size

-> Alignment

-> IO (LLVMPtr sym wptr, MemImpl sym)

Allocate a memory region.

doMallocUnbounded

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> AllocType

stack, heap, or global

-> Mutability

whether region is read-only

-> String

source location for use in error messages

-> MemImpl sym

-> Alignment

-> IO (LLVMPtr sym wptr, MemImpl sym)

Allocate a memory region of unbounded size.

data AllocType

Constructors

StackAlloc

HeapAlloc

GlobalAlloc

Instances

Show AllocType

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

showsPrec :: Int -> AllocType -> ShowS

show :: AllocType -> String

showList :: [AllocType] -> ShowS

Eq AllocType

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

(==) :: AllocType -> AllocType -> Bool

(/=) :: AllocType -> AllocType -> Bool

Ord AllocType

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

compare :: AllocType -> AllocType -> Ordering

(<) :: AllocType -> AllocType -> Bool

(<=) :: AllocType -> AllocType -> Bool

(>) :: AllocType -> AllocType -> Bool

(>=) :: AllocType -> AllocType -> Bool

max :: AllocType -> AllocType -> AllocType

min :: AllocType -> AllocType -> AllocType

data Mutability

Constructors

Mutable

Immutable

Instances

Show Mutability

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

showsPrec :: Int -> Mutability -> ShowS

show :: Mutability -> String

showList :: [Mutability] -> ShowS

Eq Mutability

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

(==) :: Mutability -> Mutability -> Bool

(/=) :: Mutability -> Mutability -> Bool

Ord Mutability

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

compare :: Mutability -> Mutability -> Ordering

(<) :: Mutability -> Mutability -> Bool

(<=) :: Mutability -> Mutability -> Bool

(>) :: Mutability -> Mutability -> Bool

(>=) :: Mutability -> Mutability -> Bool

max :: Mutability -> Mutability -> Mutability

min :: Mutability -> Mutability -> Mutability

data FuncLookupError

Reasons that looking up a function handle associated with an LLVM pointer may fail

Constructors

SymbolicPointer

RawBitvector

NoOverride

Uncallable SomeTypeRep

Instances

Eq FuncLookupError

Defined in Lang.Crucible.LLVM.Errors.MemoryError

Methods

(==) :: FuncLookupError -> FuncLookupError -> Bool

(/=) :: FuncLookupError -> FuncLookupError -> Bool

Ord FuncLookupError

Defined in Lang.Crucible.LLVM.Errors.MemoryError

Methods

compare :: FuncLookupError -> FuncLookupError -> Ordering

(<) :: FuncLookupError -> FuncLookupError -> Bool

(<=) :: FuncLookupError -> FuncLookupError -> Bool

(>) :: FuncLookupError -> FuncLookupError -> Bool

(>=) :: FuncLookupError -> FuncLookupError -> Bool

max :: FuncLookupError -> FuncLookupError -> FuncLookupError

min :: FuncLookupError -> FuncLookupError -> FuncLookupError

ppFuncLookupError :: FuncLookupError -> Doc ann

doLookupHandle :: (Typeable a, IsSymInterface sym) => sym -> MemImpl sym -> LLVMPtr sym wptr -> IO (Either FuncLookupError a)

Look up the handle associated with the given pointer, if any.

doInstallHandle

Arguments

:: (Typeable a, IsSymBackend sym bak)

=> bak

-> LLVMPtr sym wptr

-> a

handle

-> MemImpl sym

-> IO (MemImpl sym)

Associate a function handle with an existing allocation.

This can overwrite existing allocation/handle associations, and is used to do so when registering lazily-translated CFGs.

See also Lang.Crucible.LLVM.Functions.

doMemcpy

Arguments

:: (1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> NatRepr w

-> MemImpl sym

-> Bool

if true, require disjoint memory regions

-> LLVMPtr sym wptr

destination

-> LLVMPtr sym wptr

source

-> SymBV sym w

length

-> IO (MemImpl sym)

Copy memory from source to destination.

Precondition: the source and destination pointers fall within valid allocated regions.

doMemset

Arguments

:: (1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym)

=> bak

-> NatRepr w

-> MemImpl sym

-> LLVMPtr sym wptr

destination

-> SymBV sym 8

fill byte

-> SymBV sym w

length

-> IO (MemImpl sym)

Fill a memory range with copies of the specified byte.

Precondition: the memory range falls within a valid allocated region.

doInvalidate

Arguments

:: (1 <= w, IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> NatRepr w

-> MemImpl sym

-> LLVMPtr sym wptr

destination

-> Text

message

-> SymBV sym w

length

-> IO (MemImpl sym)

doCalloc

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> SymBV sym wptr

size

-> SymBV sym wptr

number

-> Alignment

Minimum alignment of the resulting allocation

-> IO (LLVMPtr sym wptr, MemImpl sym)

Allocate and zero a memory region with size * number bytes.

Precondition: the multiplication size * number does not overflow.

doFree :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (MemImpl sym)

Free the memory region pointed to by the given pointer.

Precondition: the pointer either points to the beginning of an allocated region, or is null. Freeing a null pointer has no effect.

doAlloca

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> SymBV sym wptr

allocation size

-> Alignment

pointer alignment

-> String

source location for use in error messages

-> IO (LLVMPtr sym wptr, MemImpl sym)

Allocate memory on the stack frame of the currently executing function.

doLoad

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> LLVMPtr sym wptr

pointer to load from

-> StorageType

type of value to load

-> TypeRepr tp

crucible type of the result

-> Alignment

assumed pointer alignment

-> IO (RegValue sym tp)

Load a RegValue from memory. Both the StorageType and TypeRepr arguments should be computed from a single SymType using toStorableType and llvmTypeAsRepr respectively.

Precondition: the pointer is valid and aligned, and the loaded value is defined.

doStore

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> LLVMPtr sym wptr

pointer to store into

-> TypeRepr tp

-> StorageType

type of value to store

-> Alignment

-> RegValue sym tp

value to store

-> IO (MemImpl sym)

Store a RegValue in memory. Both the StorageType and TypeRepr arguments should be computed from a single SymType using toStorableType and llvmTypeAsRepr respectively.

Precondition: the pointer is valid and points to a mutable memory region.

doArrayStore

Arguments

:: (IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym)

=> bak

-> MemImpl sym

-> LLVMPtr sym w

destination

-> Alignment

-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)

array value

-> SymBV sym w

array length

-> IO (MemImpl sym)

Store an array in memory.

Precondition: the pointer is valid and points to a mutable memory region.

doArrayStoreUnbounded

Arguments

:: (IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym)

=> bak

-> MemImpl sym

-> LLVMPtr sym w

destination

-> Alignment

-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)

array value

-> IO (MemImpl sym)

Store an array of unbounded length in memory.

Precondition: the pointer is valid and points to a mutable memory region.

doArrayConstStore

Arguments

:: (IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym)

=> bak

-> MemImpl sym

-> LLVMPtr sym w

destination

-> Alignment

-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)

array value

-> SymBV sym w

array length

-> IO (MemImpl sym)

Store an array in memory.

Precondition: the pointer is valid and points to a mutable or immutable memory region. Therefore it can be used to initialize read-only memory regions.

doArrayConstStoreUnbounded

Arguments

:: (IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym)

=> bak

-> MemImpl sym

-> LLVMPtr sym w

destination

-> Alignment

-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)

array value

-> IO (MemImpl sym)

Store an array of unbounded length in memory.

Precondition: the pointer is valid and points to a mutable or immutable memory region. Therefore it can be used to initialize read-only memory regions.

loadString

Arguments

:: forall sym bak wptr. (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions, HasCallStack)

=> bak

-> MemImpl sym

memory to read from

-> LLVMPtr sym wptr

pointer to string value

-> Maybe Int

maximum characters to read

-> IO [Word8]

Load a null-terminated string from the memory.

The pointer to read from must be concrete and nonnull. Moreover, we require all the characters in the string to be concrete. Otherwise it is very difficult to tell when the string has terminated. If a maximum number of characters is provided, no more than that number of charcters will be read. In either case, loadString will stop reading if it encounters a null-terminator.

loadMaybeString

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions, HasCallStack)

=> bak

-> MemImpl sym

memory to read from

-> LLVMPtr sym wptr

pointer to string value

-> Maybe Int

maximum characters to read

-> IO (Maybe [Word8])

Like loadString, except the pointer to load may be null. If the pointer is null, we return Nothing. Otherwise we load the string as with loadString and return it.

strLen

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

memory to read from

-> LLVMPtr sym wptr

pointer to string value

-> IO (SymBV sym wptr)

Compute the length of a null-terminated string.

The pointer to read from must be concrete and nonnull. The contents of the string may be symbolic; HOWEVER, this function will not terminate until it eventually reaches a concete null-terminator or a load error.

uncheckedMemcpy

Arguments

:: (IsSymInterface sym, HasPtrWidth wptr)

=> sym

-> MemImpl sym

-> LLVMPtr sym wptr

destination

-> LLVMPtr sym wptr

source

-> SymBV sym wptr

length

-> IO (MemImpl sym)

Copy memory from source to destination. This version does no checks to verify that the source and destination allocations are allocated and appropriately sized.

"Raw" operations with LLVMVal

data LLVMVal sym where

This datatype describes the variety of values that can be stored in the LLVM heap.

Constructors

LLVMValInt :: 1 <= w => SymNat sym -> SymBV sym w -> LLVMVal sym

NOTE! The ValInt constructor uniformly represents both pointers and raw bitvector values. The SymNat value is an allocation block number that identifies specific allocations. The block number '0' is special, and indicates that this value is actually a bitvector. Non-zero block numbers correspond to pointer values, where the SymBV value is an offset from the base pointer of the allocation.

LLVMValFloat :: FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym

LLVMValStruct :: Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym

LLVMValArray :: StorageType -> Vector (LLVMVal sym) -> LLVMVal sym

LLVMValString :: ByteString -> LLVMVal sym

LLVM Value Data given by a constant string of bytes

LLVMValZero :: StorageType -> LLVMVal sym

The zero value exists at all storage types, and represents the the value which is obtained by loading the approprite number of all zero bytes. It is useful for compactly representing large zero-initialized data structures.

LLVMValUndef :: StorageType -> LLVMVal sym

The undef value exists at all storage types.

Instances

IsExpr (SymExpr sym) => Show (LLVMVal sym)

Defined in Lang.Crucible.LLVM.MemModel.Value

Methods

showsPrec :: Int -> LLVMVal sym -> ShowS

show :: LLVMVal sym -> String

showList :: [LLVMVal sym] -> ShowS

IsExpr (SymExpr sym) => Pretty (LLVMVal sym)

This instance tries to make things as concrete as possible.

Defined in Lang.Crucible.LLVM.MemModel.Value

Methods

pretty :: LLVMVal sym -> Doc ann

prettyList :: [LLVMVal sym] -> Doc ann

ppLLVMValWithGlobals

Arguments

:: forall sym ann. IsSymInterface sym

=> sym

-> Map Natural Symbol

c.f. memImplSymbolMap

-> LLVMVal sym

-> Doc ann

Pretty-print an LLVMVal, but replace pointers to globals with the name of the global when possible. Probably pretty slow on big structures.

data FloatSize (fi :: FloatInfo) where

Constructors

SingleSize :: FloatSize SingleFloat

DoubleSize :: FloatSize DoubleFloat

X86_FP80Size :: FloatSize X86_80Float

Instances

TestEquality FloatSize

Defined in Lang.Crucible.LLVM.MemModel.Value

Methods

testEquality :: forall (a :: k) (b :: k). FloatSize a -> FloatSize b -> Maybe (a :~: b)

Show (FloatSize fi)

Defined in Lang.Crucible.LLVM.MemModel.Value

Methods

showsPrec :: Int -> FloatSize fi -> ShowS

show :: FloatSize fi -> String

showList :: [FloatSize fi] -> ShowS

Eq (FloatSize fi)

Defined in Lang.Crucible.LLVM.MemModel.Value

Methods

(==) :: FloatSize fi -> FloatSize fi -> Bool

(/=) :: FloatSize fi -> FloatSize fi -> Bool

Ord (FloatSize fi)

Defined in Lang.Crucible.LLVM.MemModel.Value

Methods

compare :: FloatSize fi -> FloatSize fi -> Ordering

(<) :: FloatSize fi -> FloatSize fi -> Bool

(<=) :: FloatSize fi -> FloatSize fi -> Bool

(>) :: FloatSize fi -> FloatSize fi -> Bool

(>=) :: FloatSize fi -> FloatSize fi -> Bool

max :: FloatSize fi -> FloatSize fi -> FloatSize fi

min :: FloatSize fi -> FloatSize fi -> FloatSize fi

unpackMemValue :: (HasCallStack, IsSymInterface sym) => sym -> TypeRepr tp -> LLVMVal sym -> IO (RegValue sym tp)

Unpack an LLVMVal to produce a RegValue.

packMemValue

Arguments

:: IsSymInterface sym

=> sym

-> StorageType

LLVM storage type

-> TypeRepr tp

Crucible type

-> RegValue sym tp

-> IO (LLVMVal sym)

Pack a RegValue into an LLVMVal. The LLVM storage type and the Crucible type must be compatible.

loadRaw :: (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => sym -> MemImpl sym -> LLVMPtr sym wptr -> StorageType -> Alignment -> IO (PartLLVMVal sym)

Load an LLVM value from memory. Asserts that the pointer is valid and the result value is not undefined.

loadArrayConcreteSizeRaw :: forall sym wptr. (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => sym -> MemImpl sym -> LLVMPtr sym wptr -> Natural -> Alignment -> IO (Either (Pred sym) (Pred sym, SymArray sym (SingleCtx (BaseBVType wptr)) (BaseBVType 8)))

Load an array with concrete size from memory.

storeRaw

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> LLVMPtr sym wptr

pointer to store into

-> StorageType

type of value to store

-> Alignment

-> LLVMVal sym

value to store

-> IO (MemImpl sym)

Store an LLVM value in memory. Asserts that the pointer is valid and points to a mutable memory region.

condStoreRaw

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> Pred sym

Predicate that determines if we actually write.

-> LLVMPtr sym wptr

pointer to store into

-> StorageType

type of value to store

-> Alignment

-> LLVMVal sym

value to store

-> IO (MemImpl sym)

Store an LLVM value in memory if the condition is true, and otherwise leaves memory unchanged.

Asserts that the pointer is valid and points to a mutable memory region when cond is true.

storeConstRaw

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> LLVMPtr sym wptr

pointer to store into

-> StorageType

type of value to store

-> Alignment

-> LLVMVal sym

value to store

-> IO (MemImpl sym)

Store an LLVM value in memory. The pointed-to memory region may be either mutable or immutable; thus storeConstRaw can be used to initialize read-only memory regions.

mallocRaw

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> SymBV sym wptr

size in bytes

-> Alignment

-> IO (LLVMPtr sym wptr, MemImpl sym)

Allocate a memory region on the heap, with no source location info.

mallocConstRaw :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> MemImpl sym -> SymBV sym wptr -> Alignment -> IO (LLVMPtr sym wptr, MemImpl sym)

Allocate a read-only memory region on the heap, with no source location info.

constToLLVMVal

Arguments

:: forall wptr sym bak io. (MonadIO io, MonadFail io, HasPtrWidth wptr, IsSymBackend sym bak, HasCallStack)

=> bak

The symbolic backend

-> MemImpl sym

The current memory state, for looking up globals

-> LLVMConst

Constant expression to translate

-> io (LLVMVal sym)

Runtime representation of the constant expression

Translate a constant into an LLVM runtime value. Assumes all necessary globals have already been populated into the MemImpl.

constToLLVMValP

Arguments

:: forall wptr sym io. (MonadIO io, MonadFail io, HasPtrWidth wptr, IsSymInterface sym, HasCallStack)

=> sym

The symbolic backend

-> (Symbol -> io (LLVMPtr sym wptr))

How to look up global symbols

-> LLVMConst

Constant expression to translate

-> io (LLVMVal sym)

This is used (by saw-script) to initialize globals.

In this translation, we lose the distinction between pointers and ints.

This is parameterized (hence, "P") over a function for looking up the pointer values of global symbols. This parameter is used by populateGlobal to recursively populate globals that may reference one another.

ptrMessage

Arguments

:: IsSymInterface sym

=> String

-> LLVMPtr sym wptr

pointer involved in message

-> StorageType

type of value pointed to

-> String

For now, the core message should be on the first line, with details on further lines. Later we should make it more structured.

data PartLLVMVal sym where

Either an LLVMValue paired with a tree of predicates explaining just when it is actually valid, or a type mismatch.

Constructors

Err :: Pred sym -> PartLLVMVal sym

NoErr :: Pred sym -> LLVMVal sym -> PartLLVMVal sym

assertSafe :: IsSymBackend sym bak => bak -> PartLLVMVal sym -> IO (LLVMVal sym)

Take a partial value and assert its safety

explodeStringValue :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) => sym -> ByteString -> IO (LLVMVal sym)

Turns a bytestring into an explicit array of bytes

isZero :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) => sym -> LLVMVal sym -> IO (Maybe (Pred sym))

A special case for comparing values to the distinguished zero value.

Should be faster than using testEqual with zeroExpandLLVMVal for compound values, because we traverse subcomponents of vectors and structs, quitting early on a constantly false answer or LLVMValUndef.

Returns Nothing for LLVMValUndef.

testEqual :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) => sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))

A predicate denoting the equality of two LLVMVals.

Returns Nothing in the event that one of the values contains LLVMValUndef.

llvmValStorableType :: IsExprBuilder sym => LLVMVal sym -> StorageType

Storage types

data StorageType

Represents the storage type of an LLVM value. A Type specifies how a value is represented as bytes in memory.

Instances

Show StorageType

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

showsPrec :: Int -> StorageType -> ShowS

show :: StorageType -> String

showList :: [StorageType] -> ShowS

Eq StorageType

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

(==) :: StorageType -> StorageType -> Bool

(/=) :: StorageType -> StorageType -> Bool

Ord StorageType

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

compare :: StorageType -> StorageType -> Ordering

(<) :: StorageType -> StorageType -> Bool

(<=) :: StorageType -> StorageType -> Bool

(>) :: StorageType -> StorageType -> Bool

(>=) :: StorageType -> StorageType -> Bool

max :: StorageType -> StorageType -> StorageType

min :: StorageType -> StorageType -> StorageType

storageTypeF :: StorageType -> StorageTypeF StorageType

data StorageTypeF v

Constructors

Bitvector !Bytes

Size of bitvector in bytes (must be > 0).

Float

Double

X86_FP80

Array !Natural !v

Number of elements and element type

Struct !(Vector (Field v))

Instances

Show v => Show (StorageTypeF v)

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

showsPrec :: Int -> StorageTypeF v -> ShowS

show :: StorageTypeF v -> String

showList :: [StorageTypeF v] -> ShowS

Eq v => Eq (StorageTypeF v)

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

(==) :: StorageTypeF v -> StorageTypeF v -> Bool

(/=) :: StorageTypeF v -> StorageTypeF v -> Bool

Ord v => Ord (StorageTypeF v)

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

compare :: StorageTypeF v -> StorageTypeF v -> Ordering

(<) :: StorageTypeF v -> StorageTypeF v -> Bool

(<=) :: StorageTypeF v -> StorageTypeF v -> Bool

(>) :: StorageTypeF v -> StorageTypeF v -> Bool

(>=) :: StorageTypeF v -> StorageTypeF v -> Bool

max :: StorageTypeF v -> StorageTypeF v -> StorageTypeF v

min :: StorageTypeF v -> StorageTypeF v -> StorageTypeF v

data Field v

Instances

Foldable Field

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

fold :: Monoid m => Field m -> m

foldMap :: Monoid m => (a -> m) -> Field a -> m

foldMap' :: Monoid m => (a -> m) -> Field a -> m

foldr :: (a -> b -> b) -> b -> Field a -> b

foldr' :: (a -> b -> b) -> b -> Field a -> b

foldl :: (b -> a -> b) -> b -> Field a -> b

foldl' :: (b -> a -> b) -> b -> Field a -> b

foldr1 :: (a -> a -> a) -> Field a -> a

foldl1 :: (a -> a -> a) -> Field a -> a

toList :: Field a -> [a]

null :: Field a -> Bool

length :: Field a -> Int

elem :: Eq a => a -> Field a -> Bool

maximum :: Ord a => Field a -> a

minimum :: Ord a => Field a -> a

sum :: Num a => Field a -> a

product :: Num a => Field a -> a

Traversable Field

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

traverse :: Applicative f => (a -> f b) -> Field a -> f (Field b)

sequenceA :: Applicative f => Field (f a) -> f (Field a)

mapM :: Monad m => (a -> m b) -> Field a -> m (Field b)

sequence :: Monad m => Field (m a) -> m (Field a)

Functor Field

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

fmap :: (a -> b) -> Field a -> Field b

(<$) :: a -> Field b -> Field a

Show v => Show (Field v)

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

showsPrec :: Int -> Field v -> ShowS

show :: Field v -> String

showList :: [Field v] -> ShowS

Eq v => Eq (Field v)

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

(==) :: Field v -> Field v -> Bool

(/=) :: Field v -> Field v -> Bool

Ord v => Ord (Field v)

Defined in Lang.Crucible.LLVM.MemModel.Type

Methods

compare :: Field v -> Field v -> Ordering

(<) :: Field v -> Field v -> Bool

(<=) :: Field v -> Field v -> Bool

(>) :: Field v -> Field v -> Bool

(>=) :: Field v -> Field v -> Bool

max :: Field v -> Field v -> Field v

min :: Field v -> Field v -> Field v

storageTypeSize :: StorageType -> Bytes

fieldVal :: Lens (Field a) (Field b) a b

fieldPad :: Field v -> Bytes

fieldOffset :: Field v -> Offset

bitvectorType :: Bytes -> StorageType

arrayType :: Natural -> StorageType -> StorageType

mkStructType :: Vector (StorageType, Bytes) -> StorageType

floatType :: StorageType

doubleType :: StorageType

x86_fp80Type :: StorageType

toStorableType :: (MonadFail m, HasPtrWidth wptr) => MemType -> m StorageType

Pointer operations

ptrToPtrVal :: 1 <= w => LLVMPtr sym w -> LLVMVal sym

Coerce an LLVMPtr value into a memory-storable LLVMVal.

mkNullPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> IO (LLVMPtr sym w)

Produce the distinguished null pointer value.

ptrIsNull :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> IO (Pred sym)

Test if a pointer value is the null pointer.

ptrEq :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (Pred sym)

Test whether two pointers are equal.

ptrAdd :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)

Add an offset to a pointer.

ptrSub :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)

Subtract an offset from a pointer.

ptrDiff :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (SymBV sym w, Pred sym)

Compute the difference between two pointers. The returned predicate asserts that the pointers point into the same allocation block.

doPtrAddOffset

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)

=> bak

-> MemImpl sym

-> LLVMPtr sym wptr

base pointer

-> SymBV sym wptr

offset

-> IO (LLVMPtr sym wptr)

Add an offset to a pointer and asserts that the result is a valid pointer.

doPtrSubtract :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym) => bak -> MemImpl sym -> LLVMPtr sym wptr -> LLVMPtr sym wptr -> IO (SymBV sym wptr)

isValidPointer :: (IsSymInterface sym, HasPtrWidth wptr) => sym -> LLVMPtr sym wptr -> MemImpl sym -> IO (Pred sym)

This predicate tests if the pointer is a valid, live pointer into the heap, OR is the distinguished NULL pointer.

isAllocatedAlignedPointer

Arguments

:: (1 <= w, IsSymInterface sym)

=> sym

-> NatRepr w

-> Alignment

minimum required pointer alignment

-> Mutability

Mutable means pointed-to region must be writable

-> LLVMPtr sym w

pointer

-> Maybe (SymBV sym w)

size (Nothing means entire address space)

-> MemImpl sym

memory

-> IO (Pred sym)

Return the condition required to prove that the pointer points to a range of size bytes that falls within an allocated region of the appropriate mutability, and also that the pointer is sufficiently aligned.

muxLLVMPtr :: 1 <= w => IsSymInterface sym => sym -> Pred sym -> LLVMPtr sym w -> LLVMPtr sym w -> IO (LLVMPtr sym w)

Mux function specialized to LLVM pointer values.

isAligned :: forall sym w. (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> LLVMPtr sym w -> Alignment -> IO (Pred sym)

Generate a predicate asserting that the given pointer satisfies the specified alignment constraint.

Disjointness

assertDisjointRegions

Arguments

:: (1 <= w, HasPtrWidth wptr, IsSymBackend sym bak, HasLLVMAnn sym)

=> bak

-> MemoryOp sym wptr

-> NatRepr w

-> LLVMPtr sym wptr

pointer to region 1

-> SymBV sym w

length of region 1

-> LLVMPtr sym wptr

pointer to region 2

-> SymBV sym w

length of region 2

-> IO ()

Assert that two memory regions are disjoint. Two memory regions are disjoint if any of the following are true:

1. Their block pointers are different
2. Their blocks are the same, but dest+dlen <= src
3. Their blocks are the same, but src+slen <= dest

buildDisjointRegionsAssertion

Arguments

:: (1 <= w, HasPtrWidth wptr, IsSymInterface sym)

=> sym

-> NatRepr w

-> LLVMPtr sym wptr

pointer to region 1

-> SymBV sym w

length of region 1

-> LLVMPtr sym wptr

pointer to region 2

-> SymBV sym w

length of region 2

-> IO (Pred sym)

buildDisjointRegionsAssertionWithSub

Arguments

:: (HasPtrWidth wptr, IsSymInterface sym)

=> sym

-> LLVMPtr sym wptr

pointer to region 1

-> SymBV sym wptr

length of region 1

-> LLVMPtr sym wptr

pointer to region 2

-> SymBV sym wptr

length of region 2

-> IO (Pred sym)

Build the condition that two memory regions are disjoint, using subtraction and comparison to zero instead of direct comparison (that is, 0 <= y - x instead of x <= y). This enables semiring and abstract domain simplifications. The result if false if any offset is not positive when interpreted as signed bitvector.

Globals

newtype GlobalSymbol

Constructors

GlobalSymbol Symbol

Instances

Show GlobalSymbol

Defined in Lang.Crucible.LLVM.Types

Methods

showsPrec :: Int -> GlobalSymbol -> ShowS

show :: GlobalSymbol -> String

showList :: [GlobalSymbol] -> ShowS

Eq GlobalSymbol

Defined in Lang.Crucible.LLVM.Types

Methods

(==) :: GlobalSymbol -> GlobalSymbol -> Bool

(/=) :: GlobalSymbol -> GlobalSymbol -> Bool

Ord GlobalSymbol

Defined in Lang.Crucible.LLVM.Types

Methods

compare :: GlobalSymbol -> GlobalSymbol -> Ordering

(<) :: GlobalSymbol -> GlobalSymbol -> Bool

(<=) :: GlobalSymbol -> GlobalSymbol -> Bool

(>) :: GlobalSymbol -> GlobalSymbol -> Bool

(>=) :: GlobalSymbol -> GlobalSymbol -> Bool

max :: GlobalSymbol -> GlobalSymbol -> GlobalSymbol

min :: GlobalSymbol -> GlobalSymbol -> GlobalSymbol

doResolveGlobal

Arguments

:: (IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack)

=> bak

-> MemImpl sym

-> Symbol

name of global

-> IO (LLVMPtr sym wptr)

Look up a Symbol in the global map of the given MemImpl. Panic if the symbol is not present in the global map.

registerGlobal :: (IsExprBuilder sym, 1 <= wptr) => MemImpl sym -> [Symbol] -> LLVMPtr sym wptr -> MemImpl sym

Add an entry to the global map of the given MemImpl.

This takes a list of symbols because there may be aliases to a global.

allocGlobals :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> [(Global, [Symbol], Bytes, Alignment)] -> MemImpl sym -> IO (MemImpl sym)

Allocate memory for each global, and register all the resulting pointers in the global map.

allocGlobal :: (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => bak -> MemImpl sym -> (Global, [Symbol], Bytes, Alignment) -> IO (MemImpl sym)

isGlobalPointer

Arguments

:: forall sym w. IsSymInterface sym

=> Map Natural Symbol

c.f. memImplSymbolMap

-> LLVMPtr sym w

-> Maybe Symbol

Look up a pointer in the memImplGlobalMap to see if it's a global.

This is best-effort and will only work if the pointer is fully concrete and matches the address of the global on the nose. It is used in SAWscript for friendly error messages.

Misc

llvmStatementExec :: (HasLLVMAnn sym, ?memOpts :: MemOptions) => EvalStmtFunc p sym LLVM

Top-level evaluation function for LLVM extension statements. LLVM extension statements are used to implement the memory model operations.

pushStackFrameMem :: Text -> Mem sym -> Mem sym

popStackFrameMem :: forall sym. Mem sym -> Mem sym

asMemAllocationArrayStore

Arguments

:: forall sym w. (IsSymInterface sym, 1 <= w)

=> sym

-> NatRepr w

-> LLVMPtr sym w

Pointer

-> Mem sym

-> IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8), SymBV sym w))

Check if LLVMPtr sym w points inside an allocation that is backed by an SMT array store. If true, return a predicate that indicates when the given array backs the given pointer, the SMT array, and the size of the allocation.

NOTE: this operation is linear in the size of the list of previous memory writes. This means that memory writes as well as memory reads require a traversal of the list of previous writes. The performance of this operation can be improved by using a map to index the writes by allocation index.

asMemMatchingArrayStore :: (IsSymInterface sym, 1 <= w) => sym -> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> Mem sym -> IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)))

data SomeFnHandle where

Constructors

SomeFnHandle :: FnHandle args ret -> SomeFnHandle

VarargsFnHandle :: FnHandle (args ::> VectorType AnyType) ret -> SomeFnHandle

data SomeAlloc sym

Constructors

forall w.1 <= w => SomeAlloc AllocType Natural (Maybe (SymBV sym w)) Mutability Alignment String

Instances

IsSymInterface sym => Eq (SomeAlloc sym)

Defined in Lang.Crucible.LLVM.MemModel.Generic

Methods

(==) :: SomeAlloc sym -> SomeAlloc sym -> Bool

(/=) :: SomeAlloc sym -> SomeAlloc sym -> Bool

possibleAllocs :: forall sym. IsSymInterface sym => Natural -> Mem sym -> [SomeAlloc sym]

Find an overapproximation of the set of allocations with this number.

ppSomeAlloc :: forall sym ann. IsExprBuilder sym => SomeAlloc sym -> Doc ann

doConditionalWriteOperation

Arguments

:: IsSymBackend sym bak

=> bak

-> MemImpl sym

-> Pred sym

write condition

-> (MemImpl sym -> IO (MemImpl sym))

memory write operation

-> IO (MemImpl sym)

Perform a memory write operation if the condition is true, do not change the memory otherwise.

Asserts that the write operation is valid when cond is true.

mergeWriteOperations

Arguments

:: IsSymBackend sym bak

=> bak

-> MemImpl sym

-> Pred sym

merge condition

-> (MemImpl sym -> IO (MemImpl sym))

true branch memory write operation

-> (MemImpl sym -> IO (MemImpl sym))

false branch memory write operation

-> IO (MemImpl sym)

Merge memory write operations on condition: if the condition is true, perform the true branch write operation, otherwise perform the false branch write operation.

Asserts that the true branch write operation is valid when cond is true, and that the false branch write operation is valid when cond is not true.

type HasLLVMAnn sym = ?recordLLVMAnnotation :: CallStack -> BoolAnn sym -> BadBehavior sym -> IO ()

type LLVMAnnMap sym = Map (BoolAnn sym) (CallStack, BadBehavior sym)

data CexExplanation sym (tp :: BaseType) where

Constructors

NoExplanation :: CexExplanation sym tp

DisjOfFailures :: [(CallStack, BadBehavior sym)] -> CexExplanation sym BaseBoolType

Instances

Semigroup (CexExplanation sym BaseBoolType)

Defined in Lang.Crucible.LLVM.MemModel.Partial

Methods

(<>) :: CexExplanation sym BaseBoolType -> CexExplanation sym BaseBoolType -> CexExplanation sym BaseBoolType

sconcat :: NonEmpty (CexExplanation sym BaseBoolType) -> CexExplanation sym BaseBoolType

stimes :: Integral b => b -> CexExplanation sym BaseBoolType -> CexExplanation sym BaseBoolType

explainCex :: forall t st fs sym. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => sym -> LLVMAnnMap sym -> Maybe (GroundEvalFn t) -> IO (Pred sym -> IO (CexExplanation sym BaseBoolType))

PtrWidth (re-exports)

type HasPtrWidth w = (1 <= w, 16 <= w, ?ptrWidth :: NatRepr w)

This constraint captures the idea that there is a distinguished pointer width in scope which is appropriate according to the C notion of pointer, and object size. In particular, it must be at least 16-bits wide (as required for the size_t type).

pattern PtrWidth :: HasPtrWidth w => w ~ w' => NatRepr w'

withPtrWidth :: forall w a. 16 <= w => NatRepr w -> (HasPtrWidth w => a) -> a

Concretization

concPtr :: (IsExprBuilder sym, 1 <= w) => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> RegValue sym (LLVMPointerType w) -> IO (RegValue sym (LLVMPointerType w))

concLLVMVal :: IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> LLVMVal sym -> IO (LLVMVal sym)

concMem :: IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> Mem sym -> IO (Mem sym)

concMemImpl :: IsSymInterface sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> MemImpl sym -> IO (MemImpl sym)

Orphan instances

IsSymInterface sym => IntrinsicClass sym "LLVM_memory"

Associated Types

type Intrinsic sym "LLVM_memory" ctx

Methods

pushBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_memory" -> CtxRepr ctx -> Intrinsic sym "LLVM_memory" ctx -> IO (Intrinsic sym "LLVM_memory" ctx)

abortBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_memory" -> CtxRepr ctx -> Intrinsic sym "LLVM_memory" ctx -> IO (Intrinsic sym "LLVM_memory" ctx)

muxIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_memory" -> CtxRepr ctx -> Pred sym -> Intrinsic sym "LLVM_memory" ctx -> Intrinsic sym "LLVM_memory" ctx -> IO (Intrinsic sym "LLVM_memory" ctx)