The intrinsics supporting symbolic I/O in LLVM

Note that this includes the base intrinsic types from crucible-symio, so those do not need to be added again.

A representation of the filesystem for the LLVM frontend

This contains the underlying SymIO filesystem as well as the infrastructure for allocating fresh file handles

A wrapper around a RankN OverrideSim action

This enables us to make explicit that all of the type variables are free and can be instantiated at any types since this override action has to be returned from the initialLLVMFileSystem function.

Create an initial LLVMFileSystem based on given concrete and symbolic file contents

Note that this function takes a SymGlobalState because it needs to allocate a few distinguished global variables for its own bookkeeping. It adds them to the given global state and returns an updated global state, which must not be discarded.

The returned LLVMFileSystem is a wrapper around that global state, and is required to initialize the symbolic I/O overrides.

This function also returns an OverrideSim action (wrapped in a SomeOverrideSim) that must be run to initialize any standard IO file descriptors that have been requested. This action should be run *before* the entry point of the function that is being verified is invoked.

See Note [Standard IO Setup] for details

The file handling overrides

See the initialLLVMFileSystem function for creating the initial filesystem state

Allocate a fresh (integer/bitvector(32)) file descriptor that is associated with the given FileHandle

NOTE that this is a file descriptor in the POSIX sense, rather than a FILE* or the underlying FileHandle.

NOTE that we truncate the file descriptor source to 32 bits in this function; it could in theory overflow.

NOTE that the file descriptor counter is incremented monotonically as the simulator hits calls to open; this means that calls to open in parallel control flow branches would get sequential file descriptor values whereas the real program would likely allocate the same file descriptor value on both branches. This could be relevant for some bug finding scenarios.

TODO It would be interesting if we could add a symbolic offset to these values so that we can't make any concrete assertions about them. It isn't clear if that ever happens in real code. If we do that, we need an escape hatch to let us allocate file descriptors 0, 1, and 2 if needed.

Retrieve the FileHandle that the given descriptor represents, calling the continuation with Nothing if the descriptor does not represent a valid handle. Notably, a successfully resolved handle may itself still be closed.

Note that the continuation may be called multiple times if it is used within a symbolic branch. As a result, any side effects in the continuation may be performed multiple times.