Lang.Crucible.LLVM.MemModel.Generic

Documentation

data Mem sym

A symbolic representation of the LLVM heap.

This representation is designed to support a variety of operations including reads and writes of symbolic data to symbolic addresses, symbolic memcpy and memset, and merging two memories in a single memory using an if-then-else operation.

A common use case is that the symbolic simulator will branch into two execution states based on a symbolic branch, make different memory modifications on each branch, and then need to merge the two memories to resume execution along a single path using the branch condition. To support this, our memory representation supports "branch frames", at any point one can insert a fresh branch frame (see branchMem), and then at some later point merge two memories back into a single memory (see mergeMem). Our mergeMem implementation is able to efficiently merge memories, but requires that one only merge memories that were identical prior to the last branch.

emptyMem :: EndianForm -> Mem sym

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

Details of a single allocation. The Maybe SymBV argument is either a size or Nothing representing an unbounded allocation. The Mutability indicates whether the region is read-only. The String contains source location information for use in error messages.

Constructors

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

data MemAllocs sym

A record of which memory regions have been allocated or freed.

Instances

Monoid (MemAllocs sym)

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

mempty :: MemAllocs sym

mappend :: MemAllocs sym -> MemAllocs sym -> MemAllocs sym

mconcat :: [MemAllocs sym] -> MemAllocs sym

Semigroup (MemAllocs sym)

Defined in Lang.Crucible.LLVM.MemModel.MemLog

Methods

(<>) :: MemAllocs sym -> MemAllocs sym -> MemAllocs sym

sconcat :: NonEmpty (MemAllocs sym) -> MemAllocs sym

stimes :: Integral b => b -> MemAllocs sym -> MemAllocs sym

memAllocs :: Mem sym -> MemAllocs sym

memEndian :: Mem sym -> EndianForm

memAllocCount :: Mem sym -> Int

memWriteCount :: Mem sym -> Int

allocMem

Arguments

:: 1 <= w

=> AllocType

Type of allocation

-> Natural

Block id for allocation

-> Maybe (SymBV sym w)

Size

-> Alignment

-> Mutability

Is block read-only

-> String

Source location

-> Mem sym

-> Mem sym

Allocate a new empty memory region.

allocAndWriteMem

Arguments

:: (1 <= w, IsExprBuilder sym)

=> sym

-> NatRepr w

-> AllocType

Type of allocation

-> Natural

Block id for allocation

-> StorageType

-> Alignment

-> Mutability

Is block read-only

-> String

Source location

-> LLVMVal sym

Value to write

-> Mem sym

-> IO (Mem sym)

Allocate and initialize a new memory region.

readMem :: forall sym w. (1 <= w, IsSymInterface sym, HasLLVMAnn sym, ?memOpts :: MemOptions) => sym -> NatRepr w -> Maybe String -> LLVMPtr sym w -> StorageType -> Alignment -> Mem sym -> IO (PartLLVMVal sym)

Read a value from memory.

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

isValidPointer sym w b m returns the condition required to prove that p is a valid pointer in m. This means that p is in the range of some allocation OR ONE PAST THE END of an allocation. In other words p is a valid pointer if b <= p <= b+sz for some allocation at base b of size Just sz, or if b <= p for some allocation of size Nothing. Note that, even though b+sz is outside the allocation range of the allocation (loading through it will fail) it is nonetheless a valid pointer value. This strange special case is baked into the C standard to allow certain common coding patterns to be defined.

isAllocatedMutable :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> Alignment -> LLVMPtr sym w -> Maybe (SymBV sym w) -> Mem sym -> IO (Pred sym)

isAllocatedMutable sym w p sz m returns the condition required to prove range [p..p+sz) lies within a single mutable allocation in m.

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)

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

notAliasable :: forall sym w. IsSymInterface sym => sym -> LLVMPtr sym w -> LLVMPtr sym w -> Mem sym -> IO (Pred sym)

The LLVM memory model generally does not allow for different memory regions to alias each other: Pointers with different allocation block numbers will compare as definitely unequal. However, it does allow two immutable memory regions to alias each other. To make this sound, equality comparisons between pointers to different immutable memory regions must not evaluate to false. Therefore pointer equality comparisons assert that the pointers are not aliasable: they must not point to two different immutable blocks.

writeMem :: (1 <= w, IsSymInterface sym, HasLLVMAnn sym, ?memOpts :: MemOptions) => sym -> NatRepr w -> Maybe String -> LLVMPtr sym w -> StorageType -> Alignment -> LLVMVal sym -> Mem sym -> IO (Mem sym, Pred sym, Pred sym)

Write a value to memory.

The returned predicates assert (in this order): * the pointer falls within an allocated, mutable memory region * the pointer's alignment is correct

writeConstMem :: (1 <= w, IsSymInterface sym, HasLLVMAnn sym, ?memOpts :: MemOptions) => sym -> NatRepr w -> Maybe String -> LLVMPtr sym w -> StorageType -> Alignment -> LLVMVal sym -> Mem sym -> IO (Mem sym, Pred sym, Pred sym)

Write a value to any memory region, mutable or immutable.

The returned predicates assert (in this order): * the pointer falls within an allocated memory region * the pointer's alignment is correct

copyMem

Arguments

:: (1 <= w, IsSymInterface sym)

=> sym

-> NatRepr w

-> LLVMPtr sym w

Dest

-> LLVMPtr sym w

Source

-> SymBV sym w

Size

-> Mem sym

-> IO (Mem sym, Pred sym, Pred sym)

Perform a mem copy (a la memcpy in C).

The returned predicates assert (in this order): * the source pointer falls within an allocated memory region * the dest pointer falls within an allocated, mutable memory region

setMem

Arguments

:: (1 <= w, IsSymInterface sym)

=> sym

-> NatRepr w

-> LLVMPtr sym w

Pointer

-> SymBV sym 8

Byte value

-> SymBV sym w

Number of bytes to set

-> Mem sym

-> IO (Mem sym, Pred sym)

Perform a mem set, filling a number of bytes with a given 8-bit value. The returned Pred asserts that the pointer falls within an allocated, mutable memory region.

invalidateMem

Arguments

:: (1 <= w, IsSymInterface sym)

=> sym

-> NatRepr w

-> LLVMPtr sym w

Pointer

-> Text

Message

-> SymBV sym w

Number of bytes to set

-> Mem sym

-> IO (Mem sym, Pred sym)

Explicitly invalidate a region of memory.

writeArrayMem

Arguments

:: (IsSymInterface sym, 1 <= w)

=> sym

-> NatRepr w

-> LLVMPtr sym w

Pointer

-> Alignment

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

Array value

-> Maybe (SymBV sym w)

Array size; if Nothing, the size is unrestricted

-> Mem sym

-> IO (Mem sym, Pred sym, Pred sym)

Write an array to memory.

The returned predicates assert (in this order): * the pointer falls within an allocated, mutable memory region * the pointer has the proper alignment

writeArrayConstMem

Arguments

:: (IsSymInterface sym, 1 <= w)

=> sym

-> NatRepr w

-> LLVMPtr sym w

Pointer

-> Alignment

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

Array value

-> Maybe (SymBV sym w)

Array size

-> Mem sym

-> IO (Mem sym, Pred sym, Pred sym)

Write an array to memory.

The returned predicates assert (in this order): * the pointer falls within an allocated memory region * the pointer has the proper alignment

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

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

freeMem

Arguments

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

=> sym

-> NatRepr w

-> LLVMPtr sym w

Base of allocation to free

-> Mem sym

-> String

Source location

-> IO (Mem sym, Pred sym, Pred sym, Pred sym)

Free a heap-allocated block of memory.

The returned predicates assert (in this order): * the pointer points to the base of a block * said block was heap-allocated, and mutable * said block was not previously freed

Because the LLVM memory model allows immutable blocks to alias each other, freeing an immutable block could lead to unsoundness.

branchMem :: Mem sym -> Mem sym

branchAbortMem :: Mem sym -> Mem sym

mergeMem :: IsExpr (SymExpr sym) => Pred sym -> Mem 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)))

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.

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.

possibleAllocInfo :: forall sym. IsExpr (SymExpr sym) => Natural -> MemAllocs sym -> Maybe (AllocInfo sym)

Look up the AllocInfo for the given allocation number. A Just result indicates that the specified memory region may or may not still be allocated; Nothing indicates that the memory region is definitely not allocated.

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

Pretty printing

ppType :: StorageType -> Doc ann

Pretty print type.

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

ppAllocs :: IsExpr (SymExpr sym) => MemAllocs sym -> Doc ann

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

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