Store a string to memory, adding a null terminator at the end.

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.

Load a null-terminated string (with a concrete null terminator) from memory.

The string must contain a concrete null terminator. If a maximum number of characters is provided, no more than that number of characters will be read. In either case, loadConcretelyNullTerminatedString will stop reading if it encounters a (concretely) null terminator.

Note that the loaded string may actually be smaller than the returned list if any of the symbolic bytes are equal to 0.

Load a null-terminated string from memory.

Consults an SMT solver to check if any of the loaded bytes are known to be null (0). If a maximum number of characters is provided, no more than that number of charcters will be read. In either case, loadProvablyNullTerminatedString will stop reading if it encounters a null terminator.

Note that the loaded string may actually be smaller than the returned list if any of the symbolic bytes are equal to 0.

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.

Implementation of libc strnlen.

strlen of a concrete string.

If any symbolic bytes are encountered, an assertion failure will be generated. If a maximum number of characters is provided, no more than that number of characters will be read. In either case, strlenConcreteString will stop reading if it encounters a null terminator.

strlen of a null-terminated string (with a concrete null terminator).

The string must contain a concrete null terminator. If a maximum number of characters is provided, no more than that number of characters will be read. In either case, strlenConcretelyNullTerminatedString will stop reading if it encounters a (concretely) null terminator.

This has the same behavior as strLen, except that it supports a maximum length.

strlen of a provably null-terminated string.

Consults an SMT solver to check if any of the loaded bytes are known to be null (0). If a maximum number of characters is provided, no more than that number of charcters will be read. In either case, strlenProvablyNullTerminatedString will stop reading if it encounters a (provably) null terminator.

strcpy of a concrete string.

Uses loadString to load the string, see that function for details.

Asserts that the regions are disjoint.

strcpy of a concretely null-terminated string.

Uses loadConcretelyNullTerminatedString to load the string, see that function for details.

Asserts that the regions are disjoint.

strcpy of a concrete string.

Uses loadProvablyNullTerminatedString to load the string, see that function for details.

Asserts that the regions are disjoint.

strdup of a concrete string.

Uses loadString to load the string, see that function for details.

Allocates memory and copies the string to it, returning the new pointer.

strdup of a concretely null-terminated string.

Uses loadConcretelyNullTerminatedString to load the string, see that function for details.

Allocates memory and copies the string to it, returning the new pointer.

strdup of a provably null-terminated string.

Uses loadProvablyNullTerminatedString to load the string, see that function for details.

Allocates memory and copies the string to it, returning the new pointer.

Whether to stop or keep going

Like Rust's std::ops::ControlFlow.

Compute a result from a symbolic byte, and check if the load should continue to the next byte.

Used to:

• Check if the byte is concrete (fullyConcreteNullTerminatedString)
• Check if the byte is concretely a null terminator (concretelyNullTerminatedString)
• Check if a byte is known by a solver to be a null terminator (nullTerminatedString)
• Check if we have surpassed a length limit (withMaxChars)

Note that it is relatively common for a to be a function [b] -> [b]. This is used to build up a snoc-list.

ByteChecker for adding a maximum character length.

ByteChecker for loading concrete strings.

Currently unused internally, but analogous with loadString. In fact, it would be good to define that function in terms of this one. However, this is blocked on TODO(#1406).

ByteChecker for loading symbolic strings with a concrete null terminator.

Used in loadConcretelyNullTerminatedString.

ByteChecker for loading symbolic strings with a provably-null terminator.

Used in loadSymbolicString.

ByteChecker for strlen of concrete strings.

ByteChecker for strlen of strings with a concrete null terminator.

ByteChecker for strlen for strings with a provably-null terminator.

Load a byte from memory.

The only ByteLoader defined here is llvmByteLoader, but Macaw users will most often want one based on doReadMemModel.

A ByteLoader for LLVM memory based on doLoad.

Load a sequence of bytes, one at a time.

Used to implement loadConcretelyNullTerminatedString and loadSymbolicString. Highly customizable via ByteLoader and ByteChecker.