System Model

This page describes how czz-llvm models various aspects of libc and the host operating system.

To maintain soundness, czz must under-approximate the behavior of the standard library and host OS. Every response that czz generates for a library call must be a possible response that the standard library and host OS might generate. The test suite compares the behavior of programs that make library calls when interpreted by czz-llvm to when they’re compiled by Clang and executed on the host, to ensure fidelity of czz-llvm’s models.

The hope is to enrich the Scheme API to the point where many such models could be written in Scheme.

Overrides

czz-llvm’s models of library functions are called overrides. The following table provides a high-level view of these overrides.

The “Impl.” column is short for “implementation”, for which there are several possible options:

• “None”: no override is available

• “czz”: the override is implemented as part of czz-llvm.

• “cru.”: the override is implemented as part of Crucible-LLVM. These overrides are generally suitable for program verification, so they are almost always sound.

• “musl”: the definition of this function is compiled by Clang from musl libc and linked into the LLVM module before execution by czz-llvm. This is sound up to bugs in musl, Clang, and llvm-link.

The “Sound” column is short for “soundness”, for which there are several possible options:

• “Yes?”: AFAIK this is sound, but more research may be needed to verify this.

• “Yes”: This is very likely sound based on my reading of the docs.

• “No”: This is known to be unsound (see documentation for specific overrides).

Category	Name	Tests	Impl.	Sound	Docs or Issue
Env. vars.	getenv	5	czz	Yes?	Docs
Env. vars.	setenv	2	None	n/a	#29
Env. vars.	unsetenv	2	None	No	Docs
Files	fclose	0	None	n/a	#43
Files	fopen	0	None	n/a	#42
Files	fprintf		czz	n/a	Docs
Files	fread	0	None	n/a	#44
Files	fwrite	0	None	n/a	#45
Formatting	__printf_chk	n/a	cru.	No	Docs
Formatting	printf	n/a	cru.	No	Docs
Formatting	sprintf		czz	No	Docs
Formatting	snprintf		czz	No	Docs
Formatting	__sprintf_chk		czz	No	Docs
Formatting	__snprintf_chk		czz	No	Docs
Math	abs	n/a	cru.	Yes	n/a
Math	labs	n/a	cru.	Yes	n/a
Math	llabs	n/a	cru.	Yes	n/a
Memory	__memcpy_chk	n/a	cru.	Yes	n/a
Memory	__memset_chk	n/a	cru.	Yes	n/a
Memory	calloc	n/a	cru.	Yes	n/a
Memory	free	n/a	cru.	Yes	n/a
Memory	htonl	n/a	cru.	Yes	n/a
Memory	htons	n/a	cru.	Yes	n/a
Memory	malloc	n/a	cru.	Yes	n/a
Memory	memcmp	n/a	musl	Yes	n/a
Memory	memcpy	n/a	cru.	Yes	n/a
Memory	memmove	n/a	cru.	Yes	n/a
Memory	memrchr	n/a	musl	Yes	n/a
Memory	memset	n/a	cru.	Yes	n/a
Memory	ntohl	n/a	cru.	Yes	n/a
Memory	ntohs	n/a	cru.	Yes	n/a
Memory	posix_memalign	n/a	cru.	Yes	n/a
Memory	realloc	n/a	cru.	Yes	n/a
Misc	__lctrans_cur	n/a	musl	Yes	n/a
Misc	__lctrans	n/a	musl	Yes	n/a
Misc	atoi	n/a	musl	Yes	n/a
Misc	getopt_long	n/a	musl	Yes	n/a
Misc	mbtowc	n/a	musl	Yes	n/a
Misc	rand	n/a	musl	Yes	n/a
Misc	srand	n/a	musl	Yes	n/a
Misc	signal		czz	Yes?	Docs
Network	accept		czz	No	Docs
Network	bind		czz	No	Docs
Network	listen		czz	No	Docs
Network	recv		czz	No	Docs
Network	send		czz	No	Docs
Network	setsockopt		czz	No	Docs
Network	socket		czz	No	Docs
Standard I/O	putchar	n/a	cru.	No	n/a
Standard I/O	puts	n/a	cru.	No	n/a
Strings	stpncpy	n/a	musl	Yes	n/a
Strings	strcmp	n/a	musl	Yes	n/a
Strings	strdup	n/a	musl	Yes	n/a
Strings	strlen	n/a	cru.	Yes	n/a
Strings	strcpy		czz	Yes	None
Strings	strncpy	n/a	musl	Yes	n/a
Strings	strrchr	n/a	musl	Yes	n/a
Time	gettimeofday	1	czz	Yes	Docs
Time	time	1	czz	Yes?	Docs

Environment Variables

czz-llvm models environment variables as an array of null-terminated strings. Each seed stores an initial array of environment variables that is propagated to the envp parameter of main (if present). This array is part of the interpreter state, it may be modified by calls to setenv and unsetenv and these modifications will be reflected in subsequent calls to getenv.

Overrides

getenv

getenv(s) scans through the array of environment variables, tries to find one of the form ${s}=${v} (where ${s} is the value of s). If such a value is not found, it returns NULL. Otherwise, it allocates fresh memory big enough to contain v, writes v to it, and returns a pointer to that allocation.

unsetenv

unsetenv(s) removes all variables of the form s=v. It always succeeds and returns 0.

This override is unsound, it should set EINVAL on a null pointer argument.

Files

fprintf

Only works for stdout and stderr. See also printf.

Formatting

The _chk overrides don’t do any extra checking, but this might be OK since Crucible-LLVM will detect any memory errors or undefined behavior.

printf

See the upstream docs.

Math

Memory

See upstream documentation.

Miscellaneous

signal

czz-llvm never sends signals to the target. Thus, it’s sound to ignore the signal handler passed to signal, and this is what czz-llvm does. It returns a null pointer, which may not actually be sound (null pointers are not mentioned in the docs).

Network

accept

This override is unsound:

• It always returns zero, instead of a new file descriptor.

• It doesn’t check for usage errors, such as EINVAL or EOPNOTSUPP.

It is also incomplete; it doesn’t model exceptional system states like EAGAIN, ENOMEM, or EPERM.

bind

This override is unsound; it doesn’t check for usage errors, such as EINVAL or EADDRINUSE.

It is also incomplete; it doesn’t model exceptional system states like EACCES or ELOOP.

listen

This override is unsound; it doesn’t check for usage errors, such as EOPNOTSUPP or EADDRINUSE.

It is also incomplete; it doesn’t model failure and always returns zero.

recv

This override writes a completely random string of bytes to the input buffer.

This override is unsound; it doesn’t check for usage errors, such as EINVAL or ENOTCONN.

It is also incomplete:

• It doesn’t model exceptional system states like ECONNREFUSED or EAGAIN.

• It asserts that flags is zero.

• It always returns the number of bytes written, never -1.

send

This override returns a random number of bytes sent.

This override is unsound; it doesn’t check for usage errors, such as EINVAL or ENOTCONN.

It is also incomplete; it doesn’t model exceptional system states like ECONNRESET or ENOBUFS. It always returns the number of bytes written, never -1.

setsockopt

This override is unsound; it doesn’t check for usage errors, such as EINVAL or ENOTSOCK. It always returns zero.

socket

This override is unsound; it doesn’t check for usage errors, such as EINVAL.

It is also incomplete:

• It doesn’t model exceptional system states like EPROTONOSUPPORT or ENOBUFS.

• It only supports AF_INET, SOCK_STREAM, and a protocol of zero.

Standard I/O

Strings

Time

gettimeofday

gettimeofday always returns 0. This is sound, see the manpage:

The time returned by gettimeofday() is affected by discontinuous jumps in the system time (e.g., if the sys‐ tem administrator manually changes the system time).

time

time always returns 0.