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.

Stores writeable memory allocations.

Compute the size of a MemAllocs log.

Allocate a new block with the given allocation ID.

Free the block with the given allocation ID.

Purge all stack allocations from the allocation log.

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.

Generalized function for checking whether a memory region ID is allocated.

The first predicate indicates whether the region was allocated, the second indicates whether it has *not* been freed.

Memory writes are represented as a list of chunks of writes. Chunks alternate between being indexed and being flat.

A chunk of memory writes is either indexed or flat (unindexed). An indexed chunk consists of writes to addresses with concrete base pointers and is represented as a map. A flat chunk consists of writes to addresses with symbolic base pointers. A merge of two indexed chunks is a indexed chunk, while any other merge is part of a flat chunk.

A state of memory as of a stack push, branch, or merge. Counts of the total number of allocations and writes are kept for performance metrics.

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.

Pretty print type.

Compute the ranges (pairs of the form pointer offset and size) for all memory writes, indexed by the pointer base. The result is Nothing if the memory contains any writes with symbolic pointer base, or without size.