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

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

A pointer with an existentially-quantified width

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

Pretty print a memory state to the given handle.

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

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

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.

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

Crucible type of pointers/bitvector values of width w.

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

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

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

Symbolic LLVM pointer or bitvector values of width w.

A pointer is a base point offset.

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

Compute the width of a pointer value.

Convert a raw bitvector value into an LLVM pointer value.

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

Allocate a memory region.

Allocate a memory region of unbounded size.

Allocate a memory region for the given handle.

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

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

Copy memory from source to destination.

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

Fill a memory range with copies of the specified byte.

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

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

Precondition: the multiplication size * number does not overflow.

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.

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

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.

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.

Store an array in memory.

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

Store an array of unbounded length in memory.

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

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.

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.

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.

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.

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.

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

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

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

Unpack an LLVMVal to produce a RegValue.

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

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

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

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.

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.

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

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

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

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.

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

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

Take a partial value and assert its safety

Turns a bytestring into an explicit array of bytes

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.

A predicate denoting the equality of two LLVMVals.

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

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

Coerce an LLVMPtr value into a memory-storable LLVMVal.

Produce the distinguished null pointer value.

Test if a pointer value is the null pointer.

Test whether two pointers are equal.

Add an offset to a pointer.

Subtract an offset from a pointer.

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

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

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

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.

Mux function specialized to LLVM pointer values.

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

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

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.

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

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.

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

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.

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

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.

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

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.

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.

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