Lang.Crucible.LLVM.SymIO

This module wraps the crucible-symio interface suitably for use within the LLVM frontend to crucible. It provides overrides for the following functions:

• open

• read

• write

• close

as specified by POSIX. Note that it does not yet cover the C stdio functions. This additional layer on top of crucible-symio is necessary to bridge the gap between LLVMPointer arguments and more primitive argument types (including that filenames need to be read from the LLVM memory model before they can be interpreted).

The limitations of this library are enumerated in the README for crux-llvm, which is the user-facing documentation for this functionality.

Types

llvmSymIOIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym

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.

data LLVMFileSystem ptrW

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

Constructors

LLVMFileSystem

Fields

• llvmFileSystem :: GlobalVar (FileSystemType ptrW)

  The underlying symbolic filesystem

• llvmFileDescMap :: GlobalVar (FDescMapType ptrW)

  Maintains the mapping from file descriptors to low-level crucible-symio FileHandles

• llvmHandles :: Map Natural Handle

  Handles that concrete output will be mirrored to; if this is empty, no mirroring will be performed

• llvmFilePointerRepr :: NatRepr ptrW

newtype SomeOverrideSim sym a where

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.

Constructors

SomeOverrideSim :: (forall p ext rtp args ret. OverrideSim p sym ext rtp args ret a) -> SomeOverrideSim sym a

initialLLVMFileSystem

Arguments

:: forall sym ptrW. (HasPtrWidth ptrW, IsSymInterface sym)

=> HandleAllocator

-> sym

-> NatRepr ptrW

The pointer width for the platform

-> InitialFileSystemContents sym

The initial contents of the symbolic filesystem

-> [(FDTarget Out, Handle)]

A mapping from file targets to handles, to which output should be mirrored. This is intended to support mirroring symbolic stdout/stderr to concrete stdout/stderr, but could be more flexible in the future (e.g., handling sockets).

Note that the writes to the associated underlying symbolic files are still recorded in the symbolic filesystem

-> SymGlobalState sym

The current globals, which will be updated with necessary bindings to support the filesystem

-> IO (LLVMFileSystem ptrW, SymGlobalState sym, SomeOverrideSim sym ())

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

Overrides

symio_overrides :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?memOpts :: MemOptions) => LLVMFileSystem wptr -> [OverrideTemplate p sym ext arch]

The file handling overrides

See the initialLLVMFileSystem function for creating the initial filesystem state

openFile :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMFileSystem wptr -> LLVMOverride p sym ext ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32) (BVType 32)

callOpenFile :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType 32) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))

closeFile :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMFileSystem wptr -> LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)

callCloseFile :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (BVType 32) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))

readFileHandle :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMFileSystem wptr -> LLVMOverride p sym ext (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType wptr)

callReadFileHandle :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (BVType 32) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))

writeFileHandle :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => LLVMFileSystem wptr -> LLVMOverride p sym ext (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr) ::> BVType wptr) (BVType wptr)

callWriteFileHandle :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) => GlobalVar Mem -> LLVMFileSystem wptr -> RegEntry sym (BVType 32) -> RegEntry sym (LLVMPointerType wptr) -> RegEntry sym (BVType wptr) -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))

File-related utilities

allocateFileDescriptor :: (IsSymInterface sym, HasPtrWidth wptr) => LLVMFileSystem wptr -> FileHandle sym wptr -> OverrideSim p sym ext r args ret (SymBV sym 32)

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.

lookupFileHandle :: IsSymInterface sym => LLVMFileSystem wptr -> SymBV sym 32 -> RegMap sym args'' -> (forall args'. Maybe (FileHandle sym wptr) -> RegMap sym args'' -> OverrideSim p sym ext r args' ret a) -> OverrideSim p sym ext r args ret a

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.

Orphan instances

IsSymInterface sym => IntrinsicClass sym "LLVM_fdescmap"

Associated Types

type Intrinsic sym "LLVM_fdescmap" ctx

Methods

pushBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_fdescmap" -> CtxRepr ctx -> Intrinsic sym "LLVM_fdescmap" ctx -> IO (Intrinsic sym "LLVM_fdescmap" ctx)

abortBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_fdescmap" -> CtxRepr ctx -> Intrinsic sym "LLVM_fdescmap" ctx -> IO (Intrinsic sym "LLVM_fdescmap" ctx)

muxIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "LLVM_fdescmap" -> CtxRepr ctx -> Pred sym -> Intrinsic sym "LLVM_fdescmap" ctx -> Intrinsic sym "LLVM_fdescmap" ctx -> IO (Intrinsic sym "LLVM_fdescmap" ctx)