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.

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.

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

Allocate a new empty memory region.

Allocate and initialize a new memory region.

Read a value from memory.

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 sym w p sz m returns the condition required to prove range [p..p+sz) lies within a single mutable allocation in m.

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.

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.

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

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

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

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.

Explicitly invalidate a region of memory.

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

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

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.

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.

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

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

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.

Pretty print type.