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.

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, loadSymbolicString 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.

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

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 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 null terminator.

Used in loadSymbolicString.

ByteChecker for adding a maximum character length.

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.