Copyright | (c) Galois Inc 2020 |
---|---|
License | BSD3 |
Maintainer | Daniel Matichuk <dmatichuk@galois.com> |
Stability | provisional |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- data FDTarget (k :: TargetDirection) where
- FileTarget :: FilePath -> FDTarget In
- StdinTarget :: FDTarget In
- StdoutTarget :: FDTarget Out
- StderrTarget :: FDTarget Out
- data TargetDirection
- type In = 'In
- type Out = 'Out
- fdTargetToText :: FDTarget k -> Text
- data InitialFileSystemContents sym = InitialFileSystemContents {
- concreteFiles :: Map (FDTarget In) ByteString
- symbolicFiles :: Map (FDTarget In) [SymBV sym 8]
- useStdout :: Bool
- useStderr :: Bool
- emptyInitialFileSystemContents :: InitialFileSystemContents sym
- type FileSystemType w = IntrinsicType "VFS_filesystem" (EmptyCtx ::> BVType w)
- type FileHandle sym w = RegValue sym (FileHandleType w)
- type FileHandleType w = ReferenceType (MaybeType (FilePointerType w))
- data FilePointer sym w
- type FilePointerType w = IntrinsicType "VFS_filepointer" (EmptyCtx ::> BVType w)
- type FileIdent sym = RegValue sym FileIdentType
- type DataChunk sym w = ArrayChunk sym (BaseBVType w) (BaseBVType 8)
- mkArrayChunk :: forall sym idx tp. IsSymExprBuilder sym => sym -> (SymExpr sym idx -> IO (SymExpr sym tp)) -> IO (ArrayChunk sym idx tp)
- pattern FileRepr :: () => (1 <= w, ty ~ FileType w) => NatRepr w -> TypeRepr ty
- pattern FileSystemRepr :: () => (1 <= w, ty ~ FileSystemType w) => NatRepr w -> TypeRepr ty
- initFS :: forall sym wptr. (1 <= wptr, IsSymInterface sym) => sym -> NatRepr wptr -> InitialFileSystemContents sym -> IO (FileSystem sym wptr)
- openFile :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileIdent sym -> (forall args'. Either FileIdentError (FileHandle sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
- openFile' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileIdent sym -> OverrideSim p sym arch r args ret (FileHandle sym wptr)
- readByte :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> (forall args'. Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8)) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
- readByte' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch r args ret (PartExpr (Pred sym) (SymBV sym 8))
- writeByte :: forall p sym arch r args ret wptr a. (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym 8 -> (forall args'. Maybe FileHandleError -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
- writeByte' :: forall p sym arch r args ret wptr. (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym 8 -> OverrideSim p sym arch r args ret ()
- readChunk :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym wptr -> (forall args'. Either FileHandleError (DataChunk sym wptr, SymBV sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
- readChunk' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym wptr -> OverrideSim p sym arch r args ret (DataChunk sym wptr, SymBV sym wptr)
- writeChunk :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> DataChunk sym wptr -> SymBV sym wptr -> (forall args'. Either FileHandleError (SymBV sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
- writeChunk' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> DataChunk sym wptr -> SymBV sym wptr -> OverrideSim p sym arch r args ret (SymBV sym wptr)
- closeFileHandle :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> (forall args'. Maybe FileHandleError -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
- closeFileHandle' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch r args ret ()
- isHandleOpen :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch args r ret (Pred sym)
- invalidFileHandle :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> OverrideSim p sym arch args r ret (FileHandle sym wptr)
- symIOIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
- chunkToArray :: forall sym idx tp. IsSymExprBuilder sym => sym -> BaseTypeRepr idx -> ArrayChunk sym idx tp -> IO (SymArray sym (EmptyCtx ::> idx) tp)
- arrayToChunk :: forall sym idx tp. IsSymExprBuilder sym => sym -> SymArray sym (EmptyCtx ::> idx) tp -> IO (ArrayChunk sym idx tp)
- evalChunk :: ArrayChunk sym idx tp -> SymExpr sym idx -> IO (SymExpr sym tp)
- data FileIdentError = FileNotFound
- data FileHandleError = FileHandleClosed
Setup
data FDTarget (k :: TargetDirection) where Source #
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).
FileTarget :: FilePath -> FDTarget In | |
StdinTarget :: FDTarget In | |
StdoutTarget :: FDTarget Out | |
StderrTarget :: FDTarget Out |
Instances
ShowF FDTarget Source # | |
Show (FDTarget k) Source # | |
Eq (FDTarget k) Source # | |
Ord (FDTarget k) Source # | |
data TargetDirection Source #
fdTargetToText :: FDTarget k -> Text Source #
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
data InitialFileSystemContents sym Source #
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
InitialFileSystemContents | |
|
emptyInitialFileSystemContents :: InitialFileSystemContents sym Source #
An empty initial symbolic filesystem
This has no files and also disables stdout and stderr
Filesystem types
The associated crucible types used to interact with the filesystem.
type FileSystemType w = IntrinsicType "VFS_filesystem" (EmptyCtx ::> BVType w) Source #
The crucible-level type of FileSystem
type FileHandle sym w = RegValue sym (FileHandleType w) Source #
A file handle is a mutable file pointer that increments every time it is read.
type FileHandleType w = ReferenceType (MaybeType (FilePointerType w)) Source #
The crucible type of file handles.
data FilePointer sym w Source #
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).
type FilePointerType w = IntrinsicType "VFS_filepointer" (EmptyCtx ::> BVType w) Source #
The crucible type of FilePointer
type FileIdent sym = RegValue sym FileIdentType Source #
An identifier for a file, which must be resolved into a File
to access
the underlying filesystem.
This is a file path
type DataChunk sym w = ArrayChunk sym (BaseBVType w) (BaseBVType 8) Source #
mkArrayChunk :: forall sym idx tp. IsSymExprBuilder sym => sym -> (SymExpr sym idx -> IO (SymExpr sym tp)) -> IO (ArrayChunk sym idx tp) Source #
Reprs
pattern FileSystemRepr :: () => (1 <= w, ty ~ FileSystemType w) => NatRepr w -> TypeRepr ty Source #
Filesystem operations
Top-level overrides for filesystem operations.
:: forall sym wptr. (1 <= wptr, IsSymInterface sym) | |
=> sym | The symbolic backend |
-> NatRepr wptr | A type-level representative of the pointer width |
-> InitialFileSystemContents sym | The initial contents of the filesystem |
-> IO (FileSystem sym wptr) |
Create an initial FileSystem
based on files with initial symbolic and
concrete contents
openFile :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileIdent sym -> (forall args'. Either FileIdentError (FileHandle sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a Source #
Open a file by resolving a FileIdent
into a File
and then allocating a fresh
FileHandle
pointing to the start of its contents.
openFile' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileIdent sym -> OverrideSim p sym arch r args ret (FileHandle sym wptr) Source #
Partial version of openFile
that asserts success.
readByte :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> (forall args'. Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8)) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a Source #
Read a byte from a given FileHandle
and increment it.
The partial result is undefined if the read yields no results.
readByte' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch r args ret (PartExpr (Pred sym) (SymBV sym 8)) Source #
Total version of readByte
that asserts success.
writeByte :: forall p sym arch r args ret wptr a. (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym 8 -> (forall args'. Maybe FileHandleError -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a Source #
Write a single byte to the given FileHandle
and increment it
writeByte' :: forall p sym arch r args ret wptr. (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym 8 -> OverrideSim p sym arch r args ret () Source #
Partial version of writeByte
that asserts success.
readChunk :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym wptr -> (forall args'. Either FileHandleError (DataChunk sym wptr, SymBV sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a Source #
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.
readChunk' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym wptr -> OverrideSim p sym arch r args ret (DataChunk sym wptr, SymBV sym wptr) Source #
Partial version of readArray
that asserts success.
writeChunk :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> DataChunk sym wptr -> SymBV sym wptr -> (forall args'. Either FileHandleError (SymBV sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a Source #
Write a chunk to the given FileHandle
and increment it to the end of
the written data. Returns the number of bytes written.
writeChunk' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> DataChunk sym wptr -> SymBV sym wptr -> OverrideSim p sym arch r args ret (SymBV sym wptr) Source #
Partial version of writeArray
that asserts success.
closeFileHandle :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> (forall args'. Maybe FileHandleError -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a Source #
Close a file by invalidating its file handle
closeFileHandle' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch r args ret () Source #
Partial version of closeFileHandle
that asserts success.
isHandleOpen :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch args r ret (Pred sym) Source #
Returns a predicate indicating whether or not the file handle is still open.
invalidFileHandle :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> OverrideSim p sym arch args r ret (FileHandle sym wptr) Source #
Return a file handle that is already closed (i.e. any file operations on it will necessarily fail).
symIOIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym Source #
The intrinsic types used in the symbolic filesystem
chunkToArray :: forall sym idx tp. IsSymExprBuilder sym => sym -> BaseTypeRepr idx -> ArrayChunk sym idx tp -> IO (SymArray sym (EmptyCtx ::> idx) tp) Source #
arrayToChunk :: forall sym idx tp. IsSymExprBuilder sym => sym -> SymArray sym (EmptyCtx ::> idx) tp -> IO (ArrayChunk sym idx tp) Source #