-----------------------------------------------------------------------
-- |
-- 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