crucible-symio-0.1: src/Lang/Crucible/SymIO.hs
-----------------------------------------------------------------------
-- |
-- Module : Lang.Crucible.SymIO
-- Description : Core definitions of the symbolic filesystem model
-- Copyright : (c) Galois, Inc 2020
-- License : BSD3
-- Maintainer : Daniel Matichuk <dmatichuk@galois.com>
-- Stability : provisional
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Lang.Crucible.SymIO
(
-- * Setup
FDTarget(..)
, TargetDirection
, In
, Out
, fdTargetToText
, InitialFileSystemContents(..)
, emptyInitialFileSystemContents
-- * Filesystem types
-- $filetypes
, FileSystemType
, FileHandle
, FileHandleType
, FilePointer
, FilePointerType
, FileIdent
, DataChunk
, CA.mkArrayChunk
-- ** Reprs
, pattern FileRepr
, pattern FileSystemRepr
-- * Filesystem operations
-- $fileops
, initFS
, openFile
, openFile'
, readByte
, readByte'
, writeByte
, writeByte'
, readChunk
, readChunk'
, writeChunk
, writeChunk'
, closeFileHandle
, closeFileHandle'
, isHandleOpen
, invalidFileHandle
, symIOIntrinsicTypes
, CA.chunkToArray
, CA.arrayToChunk
, CA.evalChunk
-- * Error conditions
, FileIdentError(..)
, FileHandleError(..)
) where
import GHC.TypeNats
import GHC.Stack
import Control.Arrow ( first )
import Control.Monad.IO.Class ( MonadIO, liftIO )
import qualified Control.Monad.State as CMS
import qualified Control.Monad.Trans as CMT
import qualified Data.Text as Text
import qualified Data.Text.Encoding as Text
import qualified Data.Traversable as DT
import qualified Data.Map as Map
import qualified Data.BitVector.Sized as BV
import qualified Data.ByteString as BS
import qualified Data.Parameterized.Classes as PC
import Data.Parameterized.Context ( pattern (:>), pattern Empty )
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr
import Lang.Crucible.CFG.Core
import Lang.Crucible.Simulator.RegMap ( RegMap(..), emptyRegMap, RegEntry(..), unconsReg, regMapSize )
import Lang.Crucible.Simulator.SimError
import qualified Lang.Crucible.Simulator.OverrideSim as C
import Lang.Crucible.Backend
import Lang.Crucible.Utils.MuxTree
import qualified What4.Interface as W4
import qualified What4.Concrete as W4C
import What4.Partial
import qualified What4.CachedArray as CA
import Lang.Crucible.SymIO.Types
---------------------------------------
-- Interface
data TargetDirection = In | Out
type In = 'In
type Out = 'Out
-- | 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).
data FDTarget (k :: TargetDirection) where
FileTarget :: FilePath -> FDTarget In
StdinTarget :: FDTarget In
StdoutTarget :: FDTarget Out
StderrTarget :: FDTarget Out
deriving instance Eq (FDTarget k)
deriving instance Ord (FDTarget k)
deriving instance Show (FDTarget k)
instance PC.ShowF FDTarget where
showF = show
-- | Convert an 'FDTarget' to 'T.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
fdTargetToText :: FDTarget k -> Text.Text
fdTargetToText t =
case t of
FileTarget f -> Text.pack f
StdinTarget -> Text.pack "stdin"
StdoutTarget -> Text.pack "stdout"
StderrTarget -> Text.pack "stderr"
-- | 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
data InitialFileSystemContents sym =
InitialFileSystemContents { concreteFiles :: Map.Map (FDTarget In) BS.ByteString
, symbolicFiles :: Map.Map (FDTarget In) [W4.SymBV sym 8]
, useStdout :: Bool
, useStderr :: Bool
}
-- | An empty initial symbolic filesystem
--
-- This has no files and also disables stdout and stderr
emptyInitialFileSystemContents :: InitialFileSystemContents sym
emptyInitialFileSystemContents =
InitialFileSystemContents { concreteFiles = Map.empty
, symbolicFiles = Map.empty
, useStdout = False
, useStderr = False
}
singletonIf :: Bool -> a -> [a]
singletonIf b p = if b then [p] else []
-- $fileops
-- Top-level overrides for filesystem operations.
-- $filetypes
-- The associated crucible types used to interact with the filesystem.
-- | Create an initial 'FileSystem' based on files with initial symbolic and
-- concrete contents
initFS
:: 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)
initFS sym ptrSize initContents = do
let symContents = fmap (first Some) $ Map.toList (symbolicFiles initContents)
let stdioOutputs = concat [ singletonIf (useStdout initContents) (Some StdoutTarget, BS.empty)
, singletonIf (useStderr initContents) (Some StderrTarget, BS.empty)
]
let concContents = stdioOutputs ++ fmap (first Some) (Map.toList (concreteFiles initContents))
symContents' <- DT.forM concContents $ \(name, bytes) -> do
bytes' <- bytesToSym bytes
return (name, bytes')
let
contentsIdx = zip [0..] (symContents ++ symContents')
flatContents =
concat $ map (\(fileIdx, (_, bytes)) ->
map (\(offset, byte) -> (fileIdx, offset, byte)) (zip [0..] bytes))
contentsIdx
initArray <- CA.initArrayConcrete sym (W4.BaseBVRepr (knownNat @8))
(map mkFileEntry flatContents)
sizes <- DT.forM contentsIdx $ \(fileIdx, (_, bytes)) -> do
size_bv <- W4.bvLit sym ptrSize (BV.mkBV ptrSize (fromIntegral (length bytes)))
return $ (Ctx.empty :> W4C.ConcreteInteger fileIdx, size_bv)
sizes_arr <- CA.initArrayConcrete sym (W4.BaseBVRepr ptrSize) sizes
names <- DT.forM contentsIdx $ \(fileIdx, (name, _)) -> do
fileIdx_int <- W4.intLit sym fileIdx
return $ (name, justPartExpr sym (File ptrSize fileIdx_int))
return $ FileSystem
{ fsPtrSize = ptrSize
, fsFileNames = Map.fromList [ (fdTargetToText name, x)
| (Some name, x) <- names
]
, fsFileSizes = sizes_arr
, fsSymData = initArray
, fsConstraints = \x -> x
}
where
bytesToSym :: BS.ByteString -> IO [W4.SymBV sym 8]
bytesToSym bs = mapM (\w -> W4.bvLit sym (knownNat @8) (BV.word8 w)) (BS.unpack bs)
mkFileEntry ::
-- | file identifier, offset into file, byte value
(Integer, Integer, W4.SymBV sym 8) ->
(Ctx.Assignment W4C.ConcreteVal (EmptyCtx ::> BaseBVType wptr ::> BaseIntegerType),
W4.SymBV sym 8)
mkFileEntry (fileIdent, offset, byte) =
(Ctx.empty :> W4C.ConcreteBV ptrSize (BV.mkBV ptrSize offset) :> W4C.ConcreteInteger fileIdent, byte)
-- | Close a file by invalidating its file handle
closeFileHandle ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
(forall args'. Maybe FileHandleError -> C.OverrideSim p sym arch r args' ret a) ->
C.OverrideSim p sym arch r args ret a
closeFileHandle fvar fhdl cont = runFileMHandleCont fvar fhdl emptyRegMap (\a -> cont (eitherToMaybeL a)) $ \_ fhdl' -> do
sz <- getPtrSz
sym <- getSym
liftOV $ C.writeMuxTreeRef (MaybeRepr (FilePointerRepr sz)) fhdl' (maybePartExpr sym Nothing)
-- | Partial version of 'closeFileHandle' that asserts success.
closeFileHandle' ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
C.OverrideSim p sym arch r args ret ()
closeFileHandle' fvar fhdl = closeFileHandle fvar fhdl $ \merr ->
case merr of
Nothing -> return ()
Just FileHandleClosed ->
C.ovrWithBackend $ \bak ->
liftIO $ addFailedAssertion bak $
AssertFailureSimError
"Attempted to close already closed file handle."
"closeFileHandle': Unassigned file handle."
eitherToMaybeL :: Either a b -> Maybe a
eitherToMaybeL (Left a) = Just a
eitherToMaybeL _ = Nothing
-- | 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 ->
(forall args'. Either FileIdentError (FileHandle sym wptr) -> C.OverrideSim p sym arch r args' ret a) ->
C.OverrideSim p sym arch r args ret a
openFile fsVar ident cont = runFileMIdentCont fsVar ident cont $ \ident' -> do
file <- resolveFileIdent ident'
openResolvedFile file
-- | Partial version of 'openFile' that asserts success.
openFile' ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileIdent sym ->
C.OverrideSim p sym arch r args ret (FileHandle sym wptr)
openFile' fsVar ident = openFile fsVar ident $ \case
Left FileNotFound ->
C.ovrWithBackend $ \bak ->
liftIO $ addFailedAssertion bak $
AssertFailureSimError
"Could not open file."
("openFile': Invalid file identifier: " ++ show (W4.printSymExpr ident))
Right fhdl -> return fhdl
-- | Write a single byte to the given 'FileHandle' and increment it
writeByte ::
forall p sym arch r args ret wptr a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
W4.SymBV sym 8 ->
(forall args'. Maybe FileHandleError -> C.OverrideSim p sym arch r args' ret a) ->
C.OverrideSim p sym arch r args ret a
writeByte fsVar fhdl byte cont = do
let args = RegMap (Empty :> RegEntry (BVRepr (knownNat @8)) byte)
runFileMHandleCont fsVar fhdl args (\a -> cont (eitherToMaybeL a)) $ \(RegMap (Empty :> RegEntry _ byte')) fhdl' -> do
ptr <- getHandle fhdl'
writeBytePointer ptr byte'
sym <- getSym
repr <- getPtrSz
one <- liftIO $ W4.bvLit sym repr (BV.mkBV repr 1)
incHandleWrite fhdl' one
-- | Partial version of 'writeByte' that asserts success.
writeByte' ::
forall p sym arch r args ret wptr.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
W4.SymBV sym 8 ->
C.OverrideSim p sym arch r args ret ()
writeByte' fsVar fhdl byte = writeByte fsVar fhdl byte $ \case
Just FileHandleClosed ->
C.ovrWithBackend $ \bak ->
liftIO $ addFailedAssertion bak $
AssertFailureSimError
"Failed to write byte due to closed file handle."
"writeByte': Closed file handle"
Nothing -> return ()
-- | 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 ->
W4.SymBV sym wptr ->
(forall args'. Either FileHandleError (W4.SymBV sym wptr) -> C.OverrideSim p sym arch r args' ret a) ->
C.OverrideSim p sym arch r args ret a
writeChunk fsVar fhdl chunk sz cont = do
W4.BaseBVRepr ptrSz <- return $ W4.exprType sz
let args = RegMap (Empty :> RegEntry (BVRepr ptrSz) sz)
runFileMHandleCont fsVar fhdl args cont $ \(RegMap (Empty :> RegEntry _ sz')) fhdl' -> do
ptr <- getHandle fhdl'
writeChunkPointer ptr chunk sz'
incHandleWrite fhdl' sz'
-- | Partial version of 'writeArray' that asserts success.
writeChunk' ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
DataChunk sym wptr ->
W4.SymBV sym wptr ->
C.OverrideSim p sym arch r args ret (W4.SymBV sym wptr)
writeChunk' fsVar fhdl chunk sz = writeChunk fsVar fhdl chunk sz $ \case
Left FileHandleClosed ->
C.ovrWithBackend $ \bak ->
liftIO $ addFailedAssertion bak $
AssertFailureSimError
"Failed to write array due to closed file handle."
"writeArray': Closed file handle"
Right sz' -> return sz'
-- | 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 ->
(forall args'. Either FileHandleError (PartExpr (W4.Pred sym) (W4.SymBV sym 8)) -> C.OverrideSim p sym arch r args' ret a) ->
C.OverrideSim p sym arch r args ret a
readByte fsVar fhdl cont = runFileMHandleCont fsVar fhdl emptyRegMap cont $ \_ fhdl' -> do
ptr <- getHandle fhdl'
v <- readBytePointer ptr
sym <- getSym
repr <- getPtrSz
one <- liftIO $ W4.bvLit sym repr (BV.mkBV repr 1)
readBytes <- incHandleRead fhdl' one
valid <- liftIO $ W4.isEq sym one readBytes
return $ mkPE valid v
-- | Total version of 'readByte' that asserts success.
readByte' ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
C.OverrideSim p sym arch r args ret (PartExpr (W4.Pred sym) (W4.SymBV sym 8))
readByte' fsVar fhdl = readByte fsVar fhdl $ \case
Left FileHandleClosed ->
C.ovrWithBackend $ \bak ->
liftIO $ addFailedAssertion bak $
AssertFailureSimError
"Failed to read byte due to closed file handle."
"readByte': Closed file handle"
Right r -> return r
-- | 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 ->
W4.SymBV sym wptr ->
(forall args'. Either FileHandleError (DataChunk sym wptr, W4.SymBV sym wptr) -> C.OverrideSim p sym arch r args' ret a) ->
C.OverrideSim p sym arch r args ret a
readChunk fsVar fhdl sz cont = do
W4.BaseBVRepr ptrSz <- return $ W4.exprType sz
let args = RegMap (Empty :> RegEntry (BVRepr ptrSz) sz)
runFileMHandleCont fsVar fhdl args cont $ \(RegMap (Empty :> RegEntry _ sz')) fhdl' -> do
ptr <- getHandle fhdl'
chunk <- readChunkPointer ptr sz'
readSz <- incHandleRead fhdl' sz'
return (chunk, readSz)
-- | Partial version of 'readArray' that asserts success.
readChunk' ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
W4.SymBV sym wptr ->
C.OverrideSim p sym arch r args ret (DataChunk sym wptr, W4.SymBV sym wptr)
readChunk' fsVar fhdl sz = readChunk fsVar fhdl sz $ \case
Left FileHandleClosed ->
C.ovrWithBackend $ \bak ->
liftIO $ addFailedAssertion bak $
AssertFailureSimError
"Failed to read array due to closed file handle."
"readArray': Closed file handle"
Right arr -> return arr
-- | Returns a predicate indicating whether or not the file handle is still open.
isHandleOpen ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
C.OverrideSim p sym arch args r ret (W4.Pred sym)
isHandleOpen fvar fhdl = runFileM fvar $ do
sym <- getSym
repr <- getPtrSz
liftOV (C.readMuxTreeRef (MaybeRepr (FilePointerRepr repr)) fhdl) >>= \case
PE p _ -> return p
Unassigned -> return (W4.falsePred sym)
-- | Return a file handle that is already closed (i.e. any file operations
-- on it will necessarily fail).
invalidFileHandle ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
C.OverrideSim p sym arch args r ret (FileHandle sym wptr)
invalidFileHandle fvar = runFileM fvar $ do
repr <- getPtrSz
sym <- getSym
toMuxTree sym <$> (liftOV $ C.newEmptyRef (MaybeRepr (FilePointerRepr repr)))
-- | Returns a predicate indicating whether or not the file identifier
-- represents a valid file.
isFileIdentValid ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileIdent sym ->
C.OverrideSim p sym arch args r ret (W4.Pred sym)
isFileIdentValid fvar ident = runFileM fvar $ do
sym <- getSym
m <- CMS.gets fsFileNames
case W4.asString ident of
Just (W4.Char8Literal i')
| Right str <- Text.decodeUtf8' i'
-> case Map.lookup str m of
Just _ -> return $ W4.truePred sym
Nothing -> return $ W4.falsePred sym
_ -> return $ W4.falsePred sym
-----------------------------------------
-- Internal operations
-- | This internal monad defines a stateful context in which file operations are executed
--
-- Operations in this monad have full access to the symbolic filesystem (which
-- is normally carried throughout the symbolic execution).
--
-- Note that most operations actually use 'FileM' instead, which fixes some
-- useful constraints on top of the monad.
newtype FileM_ p arch r args ret sym wptr a = FileM { _unFM :: CMS.StateT (FileSystem sym wptr) (C.OverrideSim p sym arch r args ret) a }
deriving
( Applicative
, Functor
, Monad
, MonadIO
, CMS.MonadState (FileSystem sym wptr)
)
data FileHandleError = FileHandleClosed
data FileIdentError = FileNotFound
-- | The monad in which all filesystem operations run
type FileM p arch r args ret sym wptr a =
(IsSymInterface sym, 1 <= wptr) =>
FileM_ p arch r args ret sym wptr a
liftOV ::
C.OverrideSim p sym arch r args ret a ->
FileM p arch r args ret sym wptr a
liftOV f = FileM $ CMT.lift f
-- | Run a 'FileM_' action in the 'C.OverrideSim' monad
--
-- This extracts the current filesystem state and threads it appropriately
-- through the 'FileM_' monad context.
runFileM ::
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileM_ p arch r args ret sym wptr a ->
C.OverrideSim p sym arch r args ret a
runFileM fvar (FileM f) = do
fs <- C.readGlobal fvar
(a, fs') <- CMS.runStateT f fs
C.writeGlobal fvar fs'
return a
runFileMHandleCont ::
forall p sym arch r args args' ret a b wptr.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileHandle sym wptr ->
RegMap sym args' ->
(forall args''. Either FileHandleError a -> C.OverrideSim p sym arch r (args <+> args'') ret b) ->
(forall args''. RegMap sym args' -> FileHandle sym wptr -> FileM_ p arch r (args <+> args'') ret sym wptr a) ->
C.OverrideSim p sym arch r args ret b
runFileMHandleCont fvar fhdl (RegMap args') cont f = do
fs <- C.readGlobal fvar
p <- isHandleOpen fvar fhdl
sym <- C.getSymInterface
args <- C.getOverrideArgs
let
cont' = cont @(args' ::> FileHandleType wptr)
args'' = RegMap (args' :> RegEntry (FileHandleRepr (fsPtrSize fs)) fhdl)
resultCase :: C.OverrideSim p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b
resultCase = do
(args_args', RegEntry _ fhdl') <- unconsReg <$> C.getOverrideArgs
let (_, args'_) = splitRegs (regMapSize args) (Ctx.size args') args_args'
a <- runFileM fvar (f @(args' ::> FileHandleType wptr) args'_ fhdl')
cont' (Right a)
C.symbolicBranches args''
[(p, resultCase, Nothing)
,(W4.truePred sym, cont' (Left FileHandleClosed), Nothing)
]
splitRegs ::
Ctx.Size ctx ->
Ctx.Size ctx' ->
RegMap sym (ctx <+> ctx') ->
(RegMap sym ctx, RegMap sym ctx')
splitRegs sz sz' (RegMap m) = (RegMap (Ctx.take sz sz' m), RegMap (Ctx.drop sz sz' m))
runFileMIdentCont ::
forall p sym arch r args ret a b wptr.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr) ->
FileIdent sym ->
(forall args'. Either FileIdentError a -> C.OverrideSim p sym arch r (args <+> args') ret b) ->
(forall args'. FileIdent sym -> FileM_ p arch r (args <+> args') ret sym wptr a) ->
C.OverrideSim p sym arch r args ret b
runFileMIdentCont fvar ident cont f = do
p <- isFileIdentValid fvar ident
sym <- C.getSymInterface
let
cont' = cont @(EmptyCtx ::> FileIdentType)
args' = RegMap (Empty :> RegEntry (StringRepr Char8Repr) ident)
resultCase :: C.OverrideSim p sym arch r (args ::> FileIdentType) ret b
resultCase = do
(_, RegEntry _ fhdl') <- unconsReg <$> C.getOverrideArgs
a <- runFileM fvar (f @(EmptyCtx ::> FileIdentType) fhdl')
cont' (Right a)
C.symbolicBranches args'
[(p, resultCase, Nothing)
,(W4.truePred sym, cont' (Left FileNotFound), Nothing)
]
getSym :: FileM p arch r args ret sym wptr sym
getSym = liftOV C.getSymInterface
withBackend ::
(forall bak. IsSymBackend sym bak => bak -> FileM p arch r args ret sym wptr a) ->
FileM p arch r args ret sym wptr a
withBackend k =
FileM $ CMS.StateT $ \st ->
C.ovrWithBackend $ \bak ->
CMS.runStateT (_unFM (k bak)) st
getPtrSz :: FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz = CMS.gets fsPtrSize
-- | Get the (possibly symbolic) size in bytes of the given file
getFileSize :: FileHandle sym wptr -> FileM p arch r args ret sym wptr (W4.SymBV sym wptr)
getFileSize fhdl = do
(FilePointer (File _ fileid) _, _) <- readHandle fhdl
szArray <- CMS.gets fsFileSizes
sym <- getSym
liftIO $ CA.readSingle sym (Ctx.empty Ctx.:> fileid) szArray
readHandle ::
FileHandle sym wptr ->
FileM p arch r args ret sym wptr (FilePointer sym wptr, W4.Pred sym)
readHandle fhandle = do
repr <- getPtrSz
liftOV (C.readMuxTreeRef (MaybeRepr (FilePointerRepr repr)) fhandle) >>= \case
PE p v -> return (v, p)
Unassigned ->
withBackend $ \bak ->
liftIO $ addFailedAssertion bak $
AssertFailureSimError
"Read from closed file handle."
"readHandle: Unassigned file handle."
-- | Retrieve the pointer that the handle is currently at
getHandle ::
FileHandle sym wptr ->
FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle fhandle = do
(v, p) <- readHandle fhandle
withBackend $ \bak ->
liftIO $ assert bak p $
AssertFailureSimError
"Read from closed file handle."
"getHandle: File handle assertion failed."
return v
-- | Resolve a file identifier to a 'File'
--
-- Note that this adds a failing assertion if:
--
-- - The file does not exist (or the the filename is symbolic)
-- - The filename is malformed (i.e., not utf8)
resolveFileIdent ::
FileIdent sym ->
FileM p arch r args ret sym wptr (File sym wptr)
resolveFileIdent ident = do
m <- CMS.gets fsFileNames
let missingErr = AssertFailureSimError "missing file"
"resolveFileIdent attempted to lookup a file handle that does not exist"
withBackend $ \bak ->
case W4.asString ident of
Just (W4.Char8Literal i')
| Right str <- Text.decodeUtf8' i'
-> case Map.lookup str m of
Just n -> liftIO $ readPartExpr bak n missingErr
Nothing -> liftIO $ addFailedAssertion bak missingErr
_ -> liftIO $ addFailedAssertion bak $
Unsupported callStack "Unsupported string in resolveFileIdent"
openResolvedFile ::
File sym wptr ->
FileM p arch r args ret sym wptr (FileHandle sym wptr)
openResolvedFile file = do
sym <- getSym
repr <- getPtrSz
zero <- liftIO $ W4.bvLit sym repr (BV.mkBV repr 0)
ref <- toMuxTree sym <$> (liftOV $ C.newEmptyRef (MaybeRepr (FilePointerRepr repr)))
setHandle ref (FilePointer file zero)
return ref
setHandle ::
FileHandle sym wptr ->
FilePointer sym wptr ->
FileM p arch r args ret sym wptr ()
setHandle fhandle ptr = do
repr <- getPtrSz
sym <- getSym
let ptr' = justPartExpr sym ptr
liftOV $ C.writeMuxTreeRef (MaybeRepr (FilePointerRepr repr)) fhandle ptr'
-- | True if the read remains in bounds, if false, the result is the number of
-- bytes that were overrun
bytesOverrun ::
FileHandle sym wptr ->
FilePointer sym wptr ->
FileM p arch r args ret sym wptr (W4.Pred sym, W4.SymBV sym wptr)
bytesOverrun fhandle (FilePointer _ ptrOff) = do
sz <- getFileSize fhandle
sym <- getSym
inbounds <- liftIO $ W4.bvUle sym ptrOff sz
overrun <- liftIO $ W4.bvSub sym ptrOff sz
return $ (inbounds, overrun)
-- | Increment the filehandle by the number of bytes read, returning the
-- number of bytes that were actually incremented. This is less than
-- the number requested if the read is over the end of the file.
incHandleRead ::
FileHandle sym wptr ->
W4.SymBV sym wptr ->
FileM p arch r args ret sym wptr (W4.SymBV sym wptr)
incHandleRead fhandle sz = do
sym <- getSym
basePtr <- getHandle fhandle
ptr <- addToPointer sz basePtr
(inbounds, overrun) <- bytesOverrun fhandle ptr
off <- liftIO $ W4.bvSub sym sz overrun
readBytes <- liftIO $ W4.baseTypeIte sym inbounds sz off
ptr' <- addToPointer readBytes basePtr
setHandle fhandle ptr'
return readBytes
-- | Increment the filehandle by the number of bytes written. Currently
-- this is exactly the given value, since writing has no failure cases.
incHandleWrite ::
FileHandle sym wptr ->
W4.SymBV sym wptr ->
FileM p arch r args ret sym wptr (W4.SymBV sym wptr)
incHandleWrite fhandle sz = do
basePtr <- getHandle fhandle
ptr <- addToPointer sz basePtr
setHandle fhandle ptr
updateFileSize fhandle
return sz
-- | Update the file size of the given file handle if it now points past
-- the end of the file (i.e. after a successful write).
updateFileSize ::
FileHandle sym wptr ->
FileM p arch r args ret sym wptr ()
updateFileSize fhdl = do
(FilePointer (File _ fileid) off, _) <- readHandle fhdl
szArray <- CMS.gets fsFileSizes
sym <- getSym
oldsz <- liftIO $ CA.readSingle sym (Ctx.empty Ctx.:> fileid) szArray
szArray' <- liftIO $ CA.writeSingle sym (Ctx.empty Ctx.:> fileid) off szArray
outbounds <- liftIO $ W4.bvUlt sym oldsz off
szArray'' <- liftIO $ CA.muxArrays sym outbounds szArray' szArray
CMS.modify' $ \arr -> arr { fsFileSizes = szArray'' }
addToPointer ::
W4.SymBV sym wptr ->
FilePointer sym wptr ->
FileM p arch r args ret sym wptr (FilePointer sym wptr)
addToPointer i (FilePointer n off) = do
sym <- getSym
off' <- liftIO $ W4.bvAdd sym off i
return $ FilePointer n off'
writeBytePointer ::
FilePointer sym wptr ->
W4.SymBV sym 8 ->
FileM p arch r args ret sym wptr ()
writeBytePointer fptr bv = do
let idx = filePointerIdx fptr
sym <- getSym
dataArr <- CMS.gets fsSymData
dataArr' <- liftIO $ CA.writeSingle sym idx bv dataArr
CMS.modify' $ \fs -> fs { fsSymData = dataArr' }
readBytePointer ::
FilePointer sym wptr ->
FileM p arch r args ret sym wptr (W4.SymBV sym 8)
readBytePointer fptr = do
sym <- getSym
let idx = filePointerIdx fptr
dataArr <- CMS.gets fsSymData
liftIO $ CA.readSingle sym idx dataArr
writeChunkPointer ::
FilePointer sym wptr ->
DataChunk sym wptr ->
W4.SymBV sym wptr ->
FileM p arch r args ret sym wptr ()
writeChunkPointer fptr chunk sz = do
let idx = filePointerIdx fptr
sym <- getSym
dataArr <- CMS.gets fsSymData
dataArr' <- liftIO $ CA.writeChunk sym idx sz chunk dataArr
CMS.modify' $ \fs -> fs { fsSymData = dataArr' }
readChunkPointer ::
FilePointer sym wptr ->
-- | Number of bytes to read
W4.SymBV sym wptr ->
FileM p arch r args ret sym wptr (DataChunk sym wptr)
readChunkPointer fptr sz = do
let idx = filePointerIdx fptr
sym <- getSym
dataArr <- CMS.gets fsSymData
liftIO $ CA.readChunk sym idx sz dataArr
filePointerIdx ::
IsSymInterface sym =>
FilePointer sym wptr ->
FileSystemIndex sym wptr
filePointerIdx (FilePointer (File _ n) off) = Ctx.empty :> off :> n