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.

memcmp.

See memcmpConcreteLen for the return value.

Asserts that the length is concrete (non-symbolic).

Compare two memory regions byte-by-byte with a concrete length.

Returns: * 0 if the regions are equal * A negative value if the first differing byte in s1 is less than in s2 * A positive value if the first differing byte in s1 is greater than in s2

strncmp - compare two null-terminated strings up to n characters.

See strncmpConcreteLen for the return value.

Asserts that the length is concrete (non-symbolic).

Compare two null-terminated strings up to n characters with a concrete length.

Returns: * 0 if the strings are equal (up to n characters or null terminator) * A negative value if the first differing byte in s1 is less than in s2 * A positive value if the first differing byte in s1 is greater than in s2

Requires that both strings have concrete null terminators.

Compare two concrete strings.

Uses fullyConcreteNullTerminatedStrings checker. Both strings must be fully concrete (no symbolic bytes).

Returns: * 0 if the strings are equal * A negative value if the first differing byte in s1 is less than in s2 * A positive value if the first differing byte in s1 is greater than in s2

Compare two strings with concrete null terminators.

Uses concretelyNullTerminatedStrings checker. The strings must have concrete null terminators, but may contain symbolic bytes before the terminator.

If a maximum length is provided, comparison stops at that length even if no null terminator is encountered.

Returns: * 0 if the strings are equal * A negative value if the first differing byte in s1 is less than in s2 * A positive value if the first differing byte in s1 is greater than in s2

Compare two strings with provably null terminators.

Uses provablyNullTerminatedStrings checker. Consults an SMT solver to check if bytes are provably null terminators.

If a maximum length is provided, comparison stops at that length even if no null terminator is encountered.

Returns: * 0 if the strings are equal * A negative value if the first differing byte in s1 is less than in s2 * A positive value if the first differing byte in s1 is greater than in s2

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.

Load a byte from each of two memory locations.

The loader can optionally add assumptions after loading bytes when iteration continues. This is used for null-terminated string operations where we need to assume loaded bytes are non-null.

Like ByteLoader, but for two bytes (usually from different strings) at once.

A BytesLoader for LLVM memory based on doLoad.

This version does not add any assumptions about loaded bytes. Use this for length-bounded operations like memcmp that need to handle null bytes in the middle of the data.

A BytesLoader for LLVM memory that adds non-null assumptions.

This version adds assumptions that loaded bytes are non-null when iteration continues. Use this for null-terminated string operations like strcmp.

Compute a result from two symbolic bytes, and check if loading should continue to the next pair of bytes.

Used to compare two byte streams simultaneously, e.g., for strcmp.

Like ByteChecker, but for two bytes (usually from different strings) at once.

BytesChecker for adding a maximum byte length.

Load sequences of bytes from two pointers simultaneously.

Used to implement strcmp. Similar to loadBytes but operates on two byte streams.

BytesChecker for comparing concrete strings.

Stops when either string has a concrete null terminator.

BytesChecker for comparing strings with concrete null terminators.

Stops when either string has a concrete null terminator.

BytesChecker for comparing strings with provably null terminators.

Stops when either string is provably null-terminated.

BytesChecker for comparing strings with concrete null terminators up to a maximum length.

Combines null-terminator checking (like strcmp) with length bounding (like memcmp). Used for strncmp.

The accumulator is a pair of the comparison result so far and the current index.

BytesChecker for comparing strings with provably null terminators up to a maximum length.

Combines provably null-terminator checking with length bounding.

The accumulator is a pair of the comparison result so far and the current index.

BytesChecker for comparing two bytes without length bounds.

Stops when bytes differ, otherwise continues indefinitely.

BytesChecker for comparing memory regions with a concrete length bound.

The accumulator is a pair of unit and the current index. Stops when the index reaches the maximum length, or when bytes differ.

Returns: * 0 if all bytes up to the length are equal * A negative value if the first differing byte in the first region is less * A positive value if the first differing byte in the first region is greater