Files to which concrete or symbolic contents can be assigned

This covers both named files and the standard I/O streams. In the future, it could also cover sockets and other file-like entities. Note that the GADT tags are in place to let us restrict the InitialFileSystemContents to only refer to files that can serve as inputs (i.e., write only files cannot have initial contents).

Convert an FDTarget to Text

We need to do this because filenames are stored in a Crucible StringMap, so we can't use our custom ADT. We have to do some custom namespacing here to avoid collisions between named files and our special files.

We will adopt the convention that all actual files will have absolute paths in the symbolic filesystem. The special files will have names that are not valid absolute paths.

FIXME: Add some validation somewhere so that we actually enforce the absolute path property

The initial contents of the symbolic filesystem

Note that standard input will be enabled if it is specified as one of the FDTarget keys.

Standard output and standard error will be connected if possible and if their respective boolean flags are set to True

An empty initial symbolic filesystem

This has no files and also disables stdout and stderr

The crucible-level type of FileSystem

A file handle is a mutable file pointer that increments every time it is read.

The crucible type of file handles.

A file pointer represents an index into a particular file.

The File is similar to an inode, and uniquely identifies a file (as an index into the array of all files). The SymBV is the offset into the file that the file pointer is currently at (i.e., where the next read or write will be from).

The crucible type of FilePointer

An identifier for a file, which must be resolved into a File to access the underlying filesystem.

This is a file path

Create an initial FileSystem based on files with initial symbolic and concrete contents

Open a file by resolving a FileIdent into a File and then allocating a fresh FileHandle pointing to the start of its contents.

Partial version of openFile that asserts success.

Read a byte from a given FileHandle and increment it. The partial result is undefined if the read yields no results.

Total version of readByte that asserts success.

Write a single byte to the given FileHandle and increment it

Partial version of writeByte that asserts success.

Read a chunk from a given FileHandle of the given size, and increment the handle by the size. Returns a struct containing the array contents, and the number of bytes read.

Partial version of readArray that asserts success.

Write a chunk to the given FileHandle and increment it to the end of the written data. Returns the number of bytes written.

Partial version of writeArray that asserts success.

Close a file by invalidating its file handle

Partial version of closeFileHandle that asserts success.

Returns a predicate indicating whether or not the file handle is still open.

Return a file handle that is already closed (i.e. any file operations on it will necessarily fail).

The intrinsic types used in the symbolic filesystem