-----------------------------------------------------------------------
-- |
-- 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 :: forall (k :: TargetDirection). FDTarget k -> FilePath
showF = FDTarget tp -> FilePath
forall a. Show a => a -> FilePath
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 :: forall (k :: TargetDirection). FDTarget k -> Text
fdTargetToText FDTarget k
t =
  case FDTarget k
t of
    FileTarget FilePath
f -> FilePath -> Text
Text.pack FilePath
f
    FDTarget k
StdinTarget -> FilePath -> Text
Text.pack FilePath
"stdin"
    FDTarget k
StdoutTarget -> FilePath -> Text
Text.pack FilePath
"stdout"
    FDTarget k
StderrTarget -> FilePath -> Text
Text.pack FilePath
"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 { forall sym.
InitialFileSystemContents sym -> Map (FDTarget 'In) ByteString
concreteFiles :: Map.Map (FDTarget In) BS.ByteString
                            , forall sym.
InitialFileSystemContents sym -> Map (FDTarget 'In) [SymBV sym 8]
symbolicFiles :: Map.Map (FDTarget In) [W4.SymBV sym 8]
                            , forall sym. InitialFileSystemContents sym -> Bool
useStdout :: Bool
                            , forall sym. InitialFileSystemContents sym -> Bool
useStderr :: Bool
                            }

-- | An empty initial symbolic filesystem
--
-- This has no files and also disables stdout and stderr
emptyInitialFileSystemContents :: InitialFileSystemContents sym
emptyInitialFileSystemContents :: forall sym. InitialFileSystemContents sym
emptyInitialFileSystemContents =
  InitialFileSystemContents { concreteFiles :: Map (FDTarget 'In) ByteString
concreteFiles = Map (FDTarget 'In) ByteString
forall k a. Map k a
Map.empty
                            , symbolicFiles :: Map (FDTarget 'In) [SymBV sym 8]
symbolicFiles = Map (FDTarget 'In) [SymBV sym 8]
forall k a. Map k a
Map.empty
                            , useStdout :: Bool
useStdout = Bool
False
                            , useStderr :: Bool
useStderr = Bool
False
                            }

singletonIf :: Bool -> a -> [a]
singletonIf :: forall a. Bool -> a -> [a]
singletonIf Bool
b a
p = if Bool
b then [a
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 :: forall sym (wptr :: Natural).
(1 <= wptr, IsSymInterface sym) =>
sym
-> NatRepr wptr
-> InitialFileSystemContents sym
-> IO (FileSystem sym wptr)
initFS sym
sym NatRepr wptr
ptrSize InitialFileSystemContents sym
initContents = do
  let symContents :: [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
symContents = ((FDTarget 'In, [SymExpr sym (BaseBVType 8)])
 -> (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
-> [(FDTarget 'In, [SymExpr sym (BaseBVType 8)])]
-> [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FDTarget 'In -> Some FDTarget)
-> (FDTarget 'In, [SymExpr sym (BaseBVType 8)])
-> (Some FDTarget, [SymExpr sym (BaseBVType 8)])
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first FDTarget 'In -> Some FDTarget
forall k (f :: k -> *) (x :: k). f x -> Some f
Some) ([(FDTarget 'In, [SymExpr sym (BaseBVType 8)])]
 -> [(Some FDTarget, [SymExpr sym (BaseBVType 8)])])
-> [(FDTarget 'In, [SymExpr sym (BaseBVType 8)])]
-> [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
forall a b. (a -> b) -> a -> b
$ Map (FDTarget 'In) [SymExpr sym (BaseBVType 8)]
-> [(FDTarget 'In, [SymExpr sym (BaseBVType 8)])]
forall k a. Map k a -> [(k, a)]
Map.toList (InitialFileSystemContents sym
-> Map (FDTarget 'In) [SymExpr sym (BaseBVType 8)]
forall sym.
InitialFileSystemContents sym -> Map (FDTarget 'In) [SymBV sym 8]
symbolicFiles InitialFileSystemContents sym
initContents)
  let stdioOutputs :: [(Some FDTarget, ByteString)]
stdioOutputs = [[(Some FDTarget, ByteString)]] -> [(Some FDTarget, ByteString)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Bool
-> (Some FDTarget, ByteString) -> [(Some FDTarget, ByteString)]
forall a. Bool -> a -> [a]
singletonIf (InitialFileSystemContents sym -> Bool
forall sym. InitialFileSystemContents sym -> Bool
useStdout InitialFileSystemContents sym
initContents) (FDTarget 'Out -> Some FDTarget
forall k (f :: k -> *) (x :: k). f x -> Some f
Some FDTarget 'Out
StdoutTarget, ByteString
BS.empty)
                            , Bool
-> (Some FDTarget, ByteString) -> [(Some FDTarget, ByteString)]
forall a. Bool -> a -> [a]
singletonIf (InitialFileSystemContents sym -> Bool
forall sym. InitialFileSystemContents sym -> Bool
useStderr InitialFileSystemContents sym
initContents) (FDTarget 'Out -> Some FDTarget
forall k (f :: k -> *) (x :: k). f x -> Some f
Some FDTarget 'Out
StderrTarget, ByteString
BS.empty)
                            ]
  let concContents :: [(Some FDTarget, ByteString)]
concContents = [(Some FDTarget, ByteString)]
stdioOutputs [(Some FDTarget, ByteString)]
-> [(Some FDTarget, ByteString)] -> [(Some FDTarget, ByteString)]
forall a. [a] -> [a] -> [a]
++ ((FDTarget 'In, ByteString) -> (Some FDTarget, ByteString))
-> [(FDTarget 'In, ByteString)] -> [(Some FDTarget, ByteString)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FDTarget 'In -> Some FDTarget)
-> (FDTarget 'In, ByteString) -> (Some FDTarget, ByteString)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first FDTarget 'In -> Some FDTarget
forall k (f :: k -> *) (x :: k). f x -> Some f
Some) (Map (FDTarget 'In) ByteString -> [(FDTarget 'In, ByteString)]
forall k a. Map k a -> [(k, a)]
Map.toList (InitialFileSystemContents sym -> Map (FDTarget 'In) ByteString
forall sym.
InitialFileSystemContents sym -> Map (FDTarget 'In) ByteString
concreteFiles InitialFileSystemContents sym
initContents))
  [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
symContents' <- [(Some FDTarget, ByteString)]
-> ((Some FDTarget, ByteString)
    -> IO (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
-> IO [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
DT.forM [(Some FDTarget, ByteString)]
concContents (((Some FDTarget, ByteString)
  -> IO (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
 -> IO [(Some FDTarget, [SymExpr sym (BaseBVType 8)])])
-> ((Some FDTarget, ByteString)
    -> IO (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
-> IO [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
forall a b. (a -> b) -> a -> b
$ \(Some FDTarget
name, ByteString
bytes) -> do
    [SymExpr sym (BaseBVType 8)]
bytes' <- ByteString -> IO [SymExpr sym (BaseBVType 8)]
bytesToSym ByteString
bytes
    (Some FDTarget, [SymExpr sym (BaseBVType 8)])
-> IO (Some FDTarget, [SymExpr sym (BaseBVType 8)])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some FDTarget
name, [SymExpr sym (BaseBVType 8)]
bytes')
  let
    contentsIdx :: [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
contentsIdx = [Integer]
-> [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
-> [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] ([(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
symContents [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
-> [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
-> [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
forall a. [a] -> [a] -> [a]
++ [(Some FDTarget, [SymExpr sym (BaseBVType 8)])]
symContents')
    flatContents :: [(Integer, Integer, SymExpr sym (BaseBVType 8))]
flatContents =
      [[(Integer, Integer, SymExpr sym (BaseBVType 8))]]
-> [(Integer, Integer, SymExpr sym (BaseBVType 8))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Integer, Integer, SymExpr sym (BaseBVType 8))]]
 -> [(Integer, Integer, SymExpr sym (BaseBVType 8))])
-> [[(Integer, Integer, SymExpr sym (BaseBVType 8))]]
-> [(Integer, Integer, SymExpr sym (BaseBVType 8))]
forall a b. (a -> b) -> a -> b
$ ((Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
 -> [(Integer, Integer, SymExpr sym (BaseBVType 8))])
-> [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
-> [[(Integer, Integer, SymExpr sym (BaseBVType 8))]]
forall a b. (a -> b) -> [a] -> [b]
map (\(Integer
fileIdx, (Some FDTarget
_, [SymExpr sym (BaseBVType 8)]
bytes)) ->
        ((Integer, SymExpr sym (BaseBVType 8))
 -> (Integer, Integer, SymExpr sym (BaseBVType 8)))
-> [(Integer, SymExpr sym (BaseBVType 8))]
-> [(Integer, Integer, SymExpr sym (BaseBVType 8))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Integer
offset, SymExpr sym (BaseBVType 8)
byte) -> (Integer
fileIdx, Integer
offset, SymExpr sym (BaseBVType 8)
byte)) ([Integer]
-> [SymExpr sym (BaseBVType 8)]
-> [(Integer, SymExpr sym (BaseBVType 8))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] [SymExpr sym (BaseBVType 8)]
bytes))
        [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
contentsIdx

  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
initArray <- sym
-> BaseTypeRepr (BaseBVType 8)
-> [(Assignment
       ConcreteVal ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType),
     SymExpr sym (BaseBVType 8))]
-> IO
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall sym (idx :: Ctx BaseType) (tp :: BaseType)
       (idx' :: Ctx BaseType) (tp' :: BaseType).
(IsSymExprBuilder sym, idx ~ (idx' ::> tp')) =>
sym
-> BaseTypeRepr tp
-> [(Assignment ConcreteVal idx, SymExpr sym tp)]
-> IO (CachedArray sym idx tp)
CA.initArrayConcrete sym
sym (NatRepr 8 -> BaseTypeRepr (BaseBVType 8)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))
    (((Integer, Integer, SymExpr sym (BaseBVType 8))
 -> (Assignment
       ConcreteVal ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType),
     SymExpr sym (BaseBVType 8)))
-> [(Integer, Integer, SymExpr sym (BaseBVType 8))]
-> [(Assignment
       ConcreteVal ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType),
     SymExpr sym (BaseBVType 8))]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Integer, SymExpr sym (BaseBVType 8))
-> (Assignment
      ConcreteVal ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType),
    SymExpr sym (BaseBVType 8))
mkFileEntry [(Integer, Integer, SymExpr sym (BaseBVType 8))]
flatContents)

  [(Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
  SymExpr sym (BaseBVType wptr))]
sizes <- [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
-> ((Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
    -> IO
         (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
          SymExpr sym (BaseBVType wptr)))
-> IO
     [(Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
       SymExpr sym (BaseBVType wptr))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
DT.forM [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
contentsIdx (((Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
  -> IO
       (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
        SymExpr sym (BaseBVType wptr)))
 -> IO
      [(Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
        SymExpr sym (BaseBVType wptr))])
-> ((Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
    -> IO
         (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
          SymExpr sym (BaseBVType wptr)))
-> IO
     [(Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
       SymExpr sym (BaseBVType wptr))]
forall a b. (a -> b) -> a -> b
$ \(Integer
fileIdx, (Some FDTarget
_, [SymExpr sym (BaseBVType 8)]
bytes)) -> do
    SymExpr sym (BaseBVType wptr)
size_bv <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym NatRepr wptr
ptrSize (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr wptr
ptrSize (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([SymExpr sym (BaseBVType 8)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SymExpr sym (BaseBVType 8)]
bytes)))
    (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
 SymExpr sym (BaseBVType wptr))
-> IO
     (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
      SymExpr sym (BaseBVType wptr))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
  SymExpr sym (BaseBVType wptr))
 -> IO
      (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
       SymExpr sym (BaseBVType wptr)))
-> (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
    SymExpr sym (BaseBVType wptr))
-> IO
     (Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
      SymExpr sym (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ (Assignment ConcreteVal EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment ConcreteVal EmptyCtx
-> ConcreteVal BaseIntegerType
-> Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Integer -> ConcreteVal BaseIntegerType
W4C.ConcreteInteger Integer
fileIdx, SymExpr sym (BaseBVType wptr)
size_bv)

  CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
sizes_arr <- sym
-> BaseTypeRepr (BaseBVType wptr)
-> [(Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
     SymExpr sym (BaseBVType wptr))]
-> IO
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall sym (idx :: Ctx BaseType) (tp :: BaseType)
       (idx' :: Ctx BaseType) (tp' :: BaseType).
(IsSymExprBuilder sym, idx ~ (idx' ::> tp')) =>
sym
-> BaseTypeRepr tp
-> [(Assignment ConcreteVal idx, SymExpr sym tp)]
-> IO (CachedArray sym idx tp)
CA.initArrayConcrete sym
sym (NatRepr wptr -> BaseTypeRepr (BaseBVType wptr)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr NatRepr wptr
ptrSize) [(Assignment ConcreteVal (EmptyCtx ::> BaseIntegerType),
  SymExpr sym (BaseBVType wptr))]
sizes

  [(Some FDTarget,
  PartExpr (SymExpr sym BaseBoolType) (File sym wptr))]
names <- [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
-> ((Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
    -> IO
         (Some FDTarget,
          PartExpr (SymExpr sym BaseBoolType) (File sym wptr)))
-> IO
     [(Some FDTarget,
       PartExpr (SymExpr sym BaseBoolType) (File sym wptr))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
DT.forM [(Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))]
contentsIdx (((Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
  -> IO
       (Some FDTarget,
        PartExpr (SymExpr sym BaseBoolType) (File sym wptr)))
 -> IO
      [(Some FDTarget,
        PartExpr (SymExpr sym BaseBoolType) (File sym wptr))])
-> ((Integer, (Some FDTarget, [SymExpr sym (BaseBVType 8)]))
    -> IO
         (Some FDTarget,
          PartExpr (SymExpr sym BaseBoolType) (File sym wptr)))
-> IO
     [(Some FDTarget,
       PartExpr (SymExpr sym BaseBoolType) (File sym wptr))]
forall a b. (a -> b) -> a -> b
$ \(Integer
fileIdx, (Some FDTarget
name, [SymExpr sym (BaseBVType 8)]
_)) -> do
    SymExpr sym BaseIntegerType
fileIdx_int <- sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym Integer
fileIdx
    (Some FDTarget,
 PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
-> IO
     (Some FDTarget,
      PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Some FDTarget,
  PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
 -> IO
      (Some FDTarget,
       PartExpr (SymExpr sym BaseBoolType) (File sym wptr)))
-> (Some FDTarget,
    PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
-> IO
     (Some FDTarget,
      PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
forall a b. (a -> b) -> a -> b
$ (Some FDTarget
name, sym
-> File sym wptr
-> PartExpr (SymExpr sym BaseBoolType) (File sym wptr)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
justPartExpr sym
sym (NatRepr wptr -> SymExpr sym BaseIntegerType -> File sym wptr
forall sym (w :: Natural).
NatRepr w -> SymInteger sym -> File sym w
File NatRepr wptr
ptrSize SymExpr sym BaseIntegerType
fileIdx_int))

  FileSystem sym wptr -> IO (FileSystem sym wptr)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FileSystem sym wptr -> IO (FileSystem sym wptr))
-> FileSystem sym wptr -> IO (FileSystem sym wptr)
forall a b. (a -> b) -> a -> b
$ FileSystem
    { fsPtrSize :: NatRepr wptr
fsPtrSize = NatRepr wptr
ptrSize
    , fsFileNames :: RegValue sym (StringMapType (FileType wptr))
fsFileNames = [(Text, PartExpr (SymExpr sym BaseBoolType) (File sym wptr))]
-> Map Text (PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (FDTarget x -> Text
forall (k :: TargetDirection). FDTarget k -> Text
fdTargetToText FDTarget x
name, PartExpr (SymExpr sym BaseBoolType) (File sym wptr)
x)
                                 | (Some FDTarget x
name, PartExpr (SymExpr sym BaseBoolType) (File sym wptr)
x) <- [(Some FDTarget,
  PartExpr (SymExpr sym BaseBoolType) (File sym wptr))]
names
                                 ]
    , fsFileSizes :: CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
fsFileSizes = CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
sizes_arr
    , fsSymData :: CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
fsSymData = CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
initArray
    , fsConstraints :: forall a. ((IsSymInterface sym, 1 <= wptr) => a) -> a
fsConstraints = \(IsSymInterface sym, 1 <= wptr) => a
x -> a
(IsSymInterface sym, 1 <= wptr) => a
x
    }

  where
    bytesToSym :: BS.ByteString -> IO [W4.SymBV sym 8]
    bytesToSym :: ByteString -> IO [SymExpr sym (BaseBVType 8)]
bytesToSym ByteString
bs = (Word8 -> IO (SymExpr sym (BaseBVType 8)))
-> [Word8] -> IO [SymExpr sym (BaseBVType 8)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Word8
w -> sym -> NatRepr 8 -> BV 8 -> IO (SymExpr sym (BaseBVType 8))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) (Word8 -> BV 8
BV.word8 Word8
w)) (ByteString -> [Word8]
BS.unpack ByteString
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 :: (Integer, Integer, SymExpr sym (BaseBVType 8))
-> (Assignment
      ConcreteVal ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType),
    SymExpr sym (BaseBVType 8))
mkFileEntry (Integer
fileIdent, Integer
offset, SymExpr sym (BaseBVType 8)
byte) =
      (Assignment ConcreteVal EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment ConcreteVal EmptyCtx
-> ConcreteVal (BaseBVType wptr)
-> Assignment ConcreteVal (EmptyCtx ::> BaseBVType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr wptr -> BV wptr -> ConcreteVal (BaseBVType wptr)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> ConcreteVal ('BaseBVType w)
W4C.ConcreteBV NatRepr wptr
ptrSize (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr wptr
ptrSize Integer
offset) Assignment ConcreteVal (EmptyCtx ::> BaseBVType wptr)
-> ConcreteVal BaseIntegerType
-> Assignment
     ConcreteVal ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Integer -> ConcreteVal BaseIntegerType
W4C.ConcreteInteger Integer
fileIdent, SymExpr sym (BaseBVType 8)
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 :: forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall (args' :: Ctx CrucibleType).
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
closeFileHandle GlobalVar (FileSystemType wptr)
fvar FileHandle sym wptr
fhdl forall (args' :: Ctx CrucibleType).
Maybe FileHandleError -> OverrideSim p sym arch r args' ret a
cont = GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym EmptyCtx
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError ()
    -> OverrideSim p sym arch r (args <+> args'') ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym EmptyCtx
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr ())
-> OverrideSim p sym arch r args ret a
forall p sym arch r (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (ret :: CrucibleType) a b
       (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym args'
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError a
    -> OverrideSim p sym arch r (args <+> args'') ret b)
-> (forall (args'' :: Ctx CrucibleType).
    RegMap sym args'
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMHandleCont GlobalVar (FileSystemType wptr)
fvar FileHandle sym wptr
fhdl RegMap sym EmptyCtx
forall sym. RegMap sym EmptyCtx
emptyRegMap (\Either FileHandleError ()
a -> Maybe FileHandleError
-> OverrideSim p sym arch r (args <+> args'') ret a
forall (args' :: Ctx CrucibleType).
Maybe FileHandleError -> OverrideSim p sym arch r args' ret a
cont (Either FileHandleError () -> Maybe FileHandleError
forall a b. Either a b -> Maybe a
eitherToMaybeL Either FileHandleError ()
a)) ((forall {args'' :: Ctx CrucibleType}.
  RegMap sym EmptyCtx
  -> FileHandle sym wptr
  -> FileM_ p arch r (args <+> args'') ret sym wptr ())
 -> OverrideSim p sym arch r args ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym EmptyCtx
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr ())
-> OverrideSim p sym arch r args ret a
forall a b. (a -> b) -> a -> b
$ \RegMap sym EmptyCtx
_ FileHandle sym wptr
fhdl' -> do
  NatRepr wptr
sz <- FileM_ p arch r (args <+> args'') ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
  sym
sym <- FileM_ p arch r (args <+> args'') ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  OverrideSim p sym arch r (args <+> args'') ret ()
-> FileM p arch r (args <+> args'') ret sym wptr ()
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV (OverrideSim p sym arch r (args <+> args'') ret ()
 -> FileM p arch r (args <+> args'') ret sym wptr ())
-> OverrideSim p sym arch r (args <+> args'') ret ()
-> FileM p arch r (args <+> args'') ret sym wptr ()
forall a b. (a -> b) -> a -> b
$ TypeRepr ('MaybeType (FilePointerType wptr))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
-> RegValue sym ('MaybeType (FilePointerType wptr))
-> OverrideSim p sym arch r (args <+> args'') ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
TypeRepr tp
-> MuxTree sym (RefCell tp)
-> RegValue sym tp
-> OverrideSim p sym ext rtp args ret ()
C.writeMuxTreeRef (TypeRepr (FilePointerType wptr)
-> TypeRepr ('MaybeType (FilePointerType wptr))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (NatRepr wptr -> TypeRepr (FilePointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FilePointerType w) =>
NatRepr w -> TypeRepr ty
FilePointerRepr NatRepr wptr
sz)) MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
FileHandle sym wptr
fhdl' (sym
-> Maybe (FilePointer sym wptr)
-> PartExpr (Pred sym) (FilePointer sym wptr)
forall sym a.
IsExprBuilder sym =>
sym -> Maybe a -> PartExpr (Pred sym) a
maybePartExpr sym
sym Maybe (FilePointer sym wptr)
forall a. Maybe a
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' :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr -> OverrideSim p sym arch r args ret ()
closeFileHandle' GlobalVar (FileSystemType wptr)
fvar FileHandle sym wptr
fhdl = GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall {args' :: Ctx CrucibleType}.
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args ret ()
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall (args' :: Ctx CrucibleType).
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
closeFileHandle GlobalVar (FileSystemType wptr)
fvar FileHandle sym wptr
fhdl ((forall {args' :: Ctx CrucibleType}.
  Maybe FileHandleError -> OverrideSim p sym arch r args' ret ())
 -> OverrideSim p sym arch r args ret ())
-> (forall {args' :: Ctx CrucibleType}.
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args ret ()
forall a b. (a -> b) -> a -> b
$ \Maybe FileHandleError
merr ->
  case Maybe FileHandleError
merr of
    Maybe FileHandleError
Nothing -> () -> OverrideSim p sym arch r args' ret ()
forall a. a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just FileHandleError
FileHandleClosed ->
      (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args' ret ()
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym arch r args' ret ())
 -> OverrideSim p sym arch r args' ret ())
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args' ret ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
        IO () -> OverrideSim p sym arch r args' ret ()
forall a. IO a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym arch r args' ret ())
-> IO () -> OverrideSim p sym arch r args' ret ()
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO ()
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$
          FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
            FilePath
"Attempted to close already closed file handle."
            FilePath
"closeFileHandle': Unassigned file handle."

eitherToMaybeL :: Either a b -> Maybe a
eitherToMaybeL :: forall a b. Either a b -> Maybe a
eitherToMaybeL (Left a
a) = a -> Maybe a
forall a. a -> Maybe a
Just a
a
eitherToMaybeL Either a b
_ = Maybe a
forall a. Maybe a
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 :: forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall (args' :: Ctx CrucibleType).
    Either FileIdentError (FileHandle sym wptr)
    -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
openFile GlobalVar (FileSystemType wptr)
fsVar FileIdent sym
ident forall (args' :: Ctx CrucibleType).
Either FileIdentError (FileHandle sym wptr)
-> OverrideSim p sym arch r args' ret a
cont = GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall (args' :: Ctx CrucibleType).
    Either
      FileIdentError
      (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
    -> OverrideSim p sym arch r (args <+> args') ret a)
-> (forall {args' :: Ctx CrucibleType}.
    FileIdent sym
    -> FileM_
         p
         arch
         r
         (args <+> args')
         ret
         sym
         wptr
         (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
-> OverrideSim p sym arch r args ret a
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall (args' :: Ctx CrucibleType).
    Either FileIdentError a
    -> OverrideSim p sym arch r (args <+> args') ret b)
-> (forall (args' :: Ctx CrucibleType).
    FileIdent sym -> FileM_ p arch r (args <+> args') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMIdentCont GlobalVar (FileSystemType wptr)
fsVar FileIdent sym
ident Either
  FileIdentError
  (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
-> OverrideSim p sym arch r (args <+> args') ret a
Either FileIdentError (FileHandle sym wptr)
-> OverrideSim p sym arch r (args <+> args') ret a
forall (args' :: Ctx CrucibleType).
Either
  FileIdentError
  (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
-> OverrideSim p sym arch r (args <+> args') ret a
forall (args' :: Ctx CrucibleType).
Either FileIdentError (FileHandle sym wptr)
-> OverrideSim p sym arch r args' ret a
cont ((forall {args' :: Ctx CrucibleType}.
  FileIdent sym
  -> FileM_
       p
       arch
       r
       (args <+> args')
       ret
       sym
       wptr
       (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
 -> OverrideSim p sym arch r args ret a)
-> (forall {args' :: Ctx CrucibleType}.
    FileIdent sym
    -> FileM_
         p
         arch
         r
         (args <+> args')
         ret
         sym
         wptr
         (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
-> OverrideSim p sym arch r args ret a
forall a b. (a -> b) -> a -> b
$ \FileIdent sym
ident' -> do
  File sym wptr
file <- FileIdent sym
-> FileM p arch r (args <+> args') ret sym wptr (File sym wptr)
forall sym p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural).
FileIdent sym -> FileM p arch r args ret sym wptr (File sym wptr)
resolveFileIdent FileIdent sym
ident'
  File sym wptr
-> FileM
     p arch r (args <+> args') ret sym wptr (FileHandle sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
File sym wptr
-> FileM p arch r args ret sym wptr (FileHandle sym wptr)
openResolvedFile File sym wptr
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' :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> OverrideSim p sym arch r args ret (FileHandle sym wptr)
openFile' GlobalVar (FileSystemType wptr)
fsVar FileIdent sym
ident = GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall {args' :: Ctx CrucibleType}.
    Either FileIdentError (FileHandle sym wptr)
    -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
-> OverrideSim p sym arch r args ret (FileHandle sym wptr)
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall (args' :: Ctx CrucibleType).
    Either FileIdentError (FileHandle sym wptr)
    -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
openFile GlobalVar (FileSystemType wptr)
fsVar FileIdent sym
ident ((forall {args' :: Ctx CrucibleType}.
  Either FileIdentError (FileHandle sym wptr)
  -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
 -> OverrideSim p sym arch r args ret (FileHandle sym wptr))
-> (forall {args' :: Ctx CrucibleType}.
    Either FileIdentError (FileHandle sym wptr)
    -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
-> OverrideSim p sym arch r args ret (FileHandle sym wptr)
forall a b. (a -> b) -> a -> b
$ \case
  Left FileIdentError
FileNotFound ->
    (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
-> OverrideSim p sym arch r args' ret (FileHandle sym wptr)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
 -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
-> OverrideSim p sym arch r args' ret (FileHandle sym wptr)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      IO (FileHandle sym wptr)
-> OverrideSim p sym arch r args' ret (FileHandle sym wptr)
forall a. IO a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (FileHandle sym wptr)
 -> OverrideSim p sym arch r args' ret (FileHandle sym wptr))
-> IO (FileHandle sym wptr)
-> OverrideSim p sym arch r args' ret (FileHandle sym wptr)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (FileHandle sym wptr)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (FileHandle sym wptr))
-> SimErrorReason -> IO (FileHandle sym wptr)
forall a b. (a -> b) -> a -> b
$
        FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
          FilePath
"Could not open file."
          (FilePath
"openFile': Invalid file identifier: " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> FilePath
forall a. Show a => a -> FilePath
show (SymExpr sym ('BaseStringType Char8) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr FileIdent sym
SymExpr sym ('BaseStringType Char8)
ident))
  Right FileHandle sym wptr
fhdl -> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
-> OverrideSim
     p
     sym
     arch
     r
     args'
     ret
     (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
forall a. a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. Monad m => a -> m a
return MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
FileHandle sym wptr
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 :: forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym 8
-> (forall (args' :: Ctx CrucibleType).
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
writeByte GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl SymBV sym 8
byte forall (args' :: Ctx CrucibleType).
Maybe FileHandleError -> OverrideSim p sym arch r args' ret a
cont = do
  let args :: RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType 8))
args = Assignment (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 8))
-> RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType 8))
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (RegEntry sym) EmptyCtx
-> RegEntry sym ('BaseToType (BaseBVType 8))
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType 8))
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> TypeRepr ('BaseToType (BaseBVType 8))
-> RegValue sym ('BaseToType (BaseBVType 8))
-> RegEntry sym ('BaseToType (BaseBVType 8))
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry (NatRepr 8 -> TypeRepr ('BaseToType (BaseBVType 8))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8)) RegValue sym ('BaseToType (BaseBVType 8))
SymBV sym 8
byte)
  GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType 8))
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError (SymExpr sym (BaseBVType wptr))
    -> OverrideSim p sym arch r (args <+> args'') ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType 8))
    -> FileHandle sym wptr
    -> FileM_
         p
         arch
         r
         (args <+> args'')
         ret
         sym
         wptr
         (SymExpr sym (BaseBVType wptr)))
-> OverrideSim p sym arch r args ret a
forall p sym arch r (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (ret :: CrucibleType) a b
       (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym args'
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError a
    -> OverrideSim p sym arch r (args <+> args'') ret b)
-> (forall (args'' :: Ctx CrucibleType).
    RegMap sym args'
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMHandleCont GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType 8))
args (\Either FileHandleError (SymExpr sym (BaseBVType wptr))
a -> Maybe FileHandleError
-> OverrideSim p sym arch r (args <+> args'') ret a
forall (args' :: Ctx CrucibleType).
Maybe FileHandleError -> OverrideSim p sym arch r args' ret a
cont (Either FileHandleError (SymExpr sym (BaseBVType wptr))
-> Maybe FileHandleError
forall a b. Either a b -> Maybe a
eitherToMaybeL Either FileHandleError (SymExpr sym (BaseBVType wptr))
a)) ((forall {args'' :: Ctx CrucibleType}.
  RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType 8))
  -> FileHandle sym wptr
  -> FileM_
       p
       arch
       r
       (args <+> args'')
       ret
       sym
       wptr
       (SymExpr sym (BaseBVType wptr)))
 -> OverrideSim p sym arch r args ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType 8))
    -> FileHandle sym wptr
    -> FileM_
         p
         arch
         r
         (args <+> args'')
         ret
         sym
         wptr
         (SymExpr sym (BaseBVType wptr)))
-> OverrideSim p sym arch r args ret a
forall a b. (a -> b) -> a -> b
$ \(RegMap (Assignment (RegEntry sym) ctx
Empty :> RegEntry TypeRepr tp
_ RegValue sym tp
byte')) FileHandle sym wptr
fhdl' -> do
    FilePointer sym wptr
ptr <- FileHandle sym wptr
-> FileM
     p arch r (args <+> args'') ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle FileHandle sym wptr
fhdl'
    FilePointer sym wptr
-> SymBV sym 8 -> FileM p arch r (args <+> args'') ret sym wptr ()
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> SymBV sym 8 -> FileM p arch r args ret sym wptr ()
writeBytePointer FilePointer sym wptr
ptr RegValue sym tp
SymBV sym 8
byte'
    sym
sym <- FileM_ p arch r (args <+> args'') ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
    NatRepr wptr
repr <- FileM_ p arch r (args <+> args'') ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
    SymExpr sym (BaseBVType wptr)
one <- IO (SymExpr sym (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (SymExpr sym (BaseBVType wptr))
forall a. IO a -> FileM_ p arch r (args <+> args'') ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType wptr))
 -> FileM_
      p
      arch
      r
      (args <+> args'')
      ret
      sym
      wptr
      (SymExpr sym (BaseBVType wptr)))
-> IO (SymExpr sym (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (SymExpr sym (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym NatRepr wptr
repr (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr wptr
repr Integer
1)
    FileHandle sym wptr
-> SymExpr sym (BaseBVType wptr)
-> FileM
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (SymExpr sym (BaseBVType wptr))
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
incHandleWrite FileHandle sym wptr
fhdl' SymExpr sym (BaseBVType wptr)
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' :: forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym 8
-> OverrideSim p sym arch r args ret ()
writeByte' GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl SymBV sym 8
byte = GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym 8
-> (forall {args' :: Ctx CrucibleType}.
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args ret ()
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym 8
-> (forall (args' :: Ctx CrucibleType).
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
writeByte GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl SymBV sym 8
byte ((forall {args' :: Ctx CrucibleType}.
  Maybe FileHandleError -> OverrideSim p sym arch r args' ret ())
 -> OverrideSim p sym arch r args ret ())
-> (forall {args' :: Ctx CrucibleType}.
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args ret ()
forall a b. (a -> b) -> a -> b
$ \case
  Just FileHandleError
FileHandleClosed ->
    (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args' ret ()
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym arch r args' ret ())
 -> OverrideSim p sym arch r args' ret ())
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym arch r args' ret ())
-> OverrideSim p sym arch r args' ret ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      IO () -> OverrideSim p sym arch r args' ret ()
forall a. IO a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym arch r args' ret ())
-> IO () -> OverrideSim p sym arch r args' ret ()
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO ()
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$
        FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
          FilePath
"Failed to write byte due to closed file handle."
          FilePath
"writeByte': Closed file handle"
  Maybe FileHandleError
Nothing -> () -> OverrideSim p sym arch r args' ret ()
forall a. a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. Monad m => a -> m a
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 :: forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> DataChunk sym wptr
-> SymBV sym wptr
-> (forall (args' :: Ctx CrucibleType).
    Either FileHandleError (SymBV sym wptr)
    -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
writeChunk GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl DataChunk sym wptr
chunk SymBV sym wptr
sz forall (args' :: Ctx CrucibleType).
Either FileHandleError (SymBV sym wptr)
-> OverrideSim p sym arch r args' ret a
cont = do
  W4.BaseBVRepr NatRepr w
ptrSz <- BaseTypeRepr (BaseBVType wptr)
-> OverrideSim
     p sym arch r args ret (BaseTypeRepr (BaseBVType wptr))
forall a. a -> OverrideSim p sym arch r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return (BaseTypeRepr (BaseBVType wptr)
 -> OverrideSim
      p sym arch r args ret (BaseTypeRepr (BaseBVType wptr)))
-> BaseTypeRepr (BaseBVType wptr)
-> OverrideSim
     p sym arch r args ret (BaseTypeRepr (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ SymBV sym wptr -> BaseTypeRepr (BaseBVType wptr)
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymBV sym wptr
sz
  let args :: RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
args = Assignment
  (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
-> RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (RegEntry sym) EmptyCtx
-> RegEntry sym ('BaseToType ('BaseBVType w))
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> TypeRepr ('BaseToType ('BaseBVType w))
-> RegValue sym ('BaseToType ('BaseBVType w))
-> RegEntry sym ('BaseToType ('BaseBVType w))
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry (NatRepr w -> TypeRepr ('BaseToType ('BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
ptrSz) RegValue sym ('BaseToType ('BaseBVType w))
SymBV sym wptr
sz)
  GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError (SymBV sym wptr)
    -> OverrideSim p sym arch r (args <+> args'') ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr (SymBV sym wptr))
-> OverrideSim p sym arch r args ret a
forall p sym arch r (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (ret :: CrucibleType) a b
       (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym args'
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError a
    -> OverrideSim p sym arch r (args <+> args'') ret b)
-> (forall (args'' :: Ctx CrucibleType).
    RegMap sym args'
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMHandleCont GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
args Either FileHandleError (SymBV sym wptr)
-> OverrideSim p sym arch r (args <+> args'') ret a
forall (args' :: Ctx CrucibleType).
Either FileHandleError (SymBV sym wptr)
-> OverrideSim p sym arch r args' ret a
forall (args'' :: Ctx CrucibleType).
Either FileHandleError (SymBV sym wptr)
-> OverrideSim p sym arch r (args <+> args'') ret a
cont ((forall {args'' :: Ctx CrucibleType}.
  RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
  -> FileHandle sym wptr
  -> FileM_ p arch r (args <+> args'') ret sym wptr (SymBV sym wptr))
 -> OverrideSim p sym arch r args ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr (SymBV sym wptr))
-> OverrideSim p sym arch r args ret a
forall a b. (a -> b) -> a -> b
$ \(RegMap (Assignment (RegEntry sym) ctx
Empty :> RegEntry TypeRepr tp
_ RegValue sym tp
sz')) FileHandle sym wptr
fhdl' -> do
    FilePointer sym wptr
ptr <- FileHandle sym wptr
-> FileM
     p arch r (args <+> args'') ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle FileHandle sym wptr
fhdl'
    FilePointer sym wptr
-> DataChunk sym wptr
-> SymBV sym wptr
-> FileM p arch r (args <+> args'') ret sym wptr ()
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> DataChunk sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr ()
writeChunkPointer FilePointer sym wptr
ptr DataChunk sym wptr
chunk RegValue sym tp
SymBV sym wptr
sz'
    FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r (args <+> args'') ret sym wptr (SymBV sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
incHandleWrite FileHandle sym wptr
fhdl' RegValue sym tp
SymBV sym wptr
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' :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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)
writeChunk' GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl DataChunk sym wptr
chunk SymBV sym wptr
sz = GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> DataChunk sym wptr
-> SymBV sym wptr
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (SymBV sym wptr)
    -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
-> OverrideSim p sym arch r args ret (SymBV sym wptr)
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> DataChunk sym wptr
-> SymBV sym wptr
-> (forall (args' :: Ctx CrucibleType).
    Either FileHandleError (SymBV sym wptr)
    -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
writeChunk GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl DataChunk sym wptr
chunk SymBV sym wptr
sz ((forall {args' :: Ctx CrucibleType}.
  Either FileHandleError (SymBV sym wptr)
  -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
 -> OverrideSim p sym arch r args ret (SymBV sym wptr))
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (SymBV sym wptr)
    -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
-> OverrideSim p sym arch r args ret (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ \case
  Left FileHandleError
FileHandleClosed ->
    (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
-> OverrideSim p sym arch r args' ret (SymBV sym wptr)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
 -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
-> OverrideSim p sym arch r args' ret (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      IO (SymBV sym wptr)
-> OverrideSim p sym arch r args' ret (SymBV sym wptr)
forall a. IO a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> OverrideSim p sym arch r args' ret (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> OverrideSim p sym arch r args' ret (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (SymBV sym wptr)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (SymBV sym wptr))
-> SimErrorReason -> IO (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$
        FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
          FilePath
"Failed to write array due to closed file handle."
          FilePath
"writeArray': Closed file handle"
  Right SymBV sym wptr
sz' -> SymBV sym wptr
-> OverrideSim p sym arch r args' ret (SymBV sym wptr)
forall a. a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. Monad m => a -> m a
return SymBV sym wptr
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 :: forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall (args' :: Ctx CrucibleType).
    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 GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl forall (args' :: Ctx CrucibleType).
Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
-> OverrideSim p sym arch r args' ret a
cont = GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym EmptyCtx
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
    -> OverrideSim p sym arch r (args <+> args'') ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym EmptyCtx
    -> FileHandle sym wptr
    -> FileM_
         p
         arch
         r
         (args <+> args'')
         ret
         sym
         wptr
         (PartExpr (Pred sym) (SymBV sym 8)))
-> OverrideSim p sym arch r args ret a
forall p sym arch r (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (ret :: CrucibleType) a b
       (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym args'
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError a
    -> OverrideSim p sym arch r (args <+> args'') ret b)
-> (forall (args'' :: Ctx CrucibleType).
    RegMap sym args'
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMHandleCont GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl RegMap sym EmptyCtx
forall sym. RegMap sym EmptyCtx
emptyRegMap Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
-> OverrideSim p sym arch r (args <+> args'') ret a
forall (args' :: Ctx CrucibleType).
Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
-> OverrideSim p sym arch r args' ret a
forall (args'' :: Ctx CrucibleType).
Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
-> OverrideSim p sym arch r (args <+> args'') ret a
cont ((forall {args'' :: Ctx CrucibleType}.
  RegMap sym EmptyCtx
  -> FileHandle sym wptr
  -> FileM_
       p
       arch
       r
       (args <+> args'')
       ret
       sym
       wptr
       (PartExpr (Pred sym) (SymBV sym 8)))
 -> OverrideSim p sym arch r args ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym EmptyCtx
    -> FileHandle sym wptr
    -> FileM_
         p
         arch
         r
         (args <+> args'')
         ret
         sym
         wptr
         (PartExpr (Pred sym) (SymBV sym 8)))
-> OverrideSim p sym arch r args ret a
forall a b. (a -> b) -> a -> b
$ \RegMap sym EmptyCtx
_ FileHandle sym wptr
fhdl' -> do
  FilePointer sym wptr
ptr <- FileHandle sym wptr
-> FileM
     p arch r (args <+> args'') ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle FileHandle sym wptr
fhdl'
  SymBV sym 8
v <- FilePointer sym wptr
-> FileM p arch r (args <+> args'') ret sym wptr (SymBV sym 8)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym 8)
readBytePointer FilePointer sym wptr
ptr
  sym
sym <- FileM_ p arch r (args <+> args'') ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  NatRepr wptr
repr <- FileM_ p arch r (args <+> args'') ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
  SymExpr sym (BaseBVType wptr)
one <- IO (SymExpr sym (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (SymExpr sym (BaseBVType wptr))
forall a. IO a -> FileM_ p arch r (args <+> args'') ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType wptr))
 -> FileM_
      p
      arch
      r
      (args <+> args'')
      ret
      sym
      wptr
      (SymExpr sym (BaseBVType wptr)))
-> IO (SymExpr sym (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (SymExpr sym (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym NatRepr wptr
repr (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr wptr
repr Integer
1)
  SymExpr sym (BaseBVType wptr)
readBytes <- FileHandle sym wptr
-> SymExpr sym (BaseBVType wptr)
-> FileM
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (SymExpr sym (BaseBVType wptr))
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
incHandleRead FileHandle sym wptr
fhdl' SymExpr sym (BaseBVType wptr)
one
  Pred sym
valid <- IO (Pred sym)
-> FileM_ p arch r (args <+> args'') ret sym wptr (Pred sym)
forall a. IO a -> FileM_ p arch r (args <+> args'') ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Pred sym)
 -> FileM_ p arch r (args <+> args'') ret sym wptr (Pred sym))
-> IO (Pred sym)
-> FileM_ p arch r (args <+> args'') ret sym wptr (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseBVType wptr)
-> SymExpr sym (BaseBVType wptr)
-> IO (Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
W4.isEq sym
sym SymExpr sym (BaseBVType wptr)
one SymExpr sym (BaseBVType wptr)
readBytes
  PartExpr (Pred sym) (SymBV sym 8)
-> FileM_
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (PartExpr (Pred sym) (SymBV sym 8))
forall a. a -> FileM_ p arch r (args <+> args'') ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (PartExpr (Pred sym) (SymBV sym 8)
 -> FileM_
      p
      arch
      r
      (args <+> args'')
      ret
      sym
      wptr
      (PartExpr (Pred sym) (SymBV sym 8)))
-> PartExpr (Pred sym) (SymBV sym 8)
-> FileM_
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (PartExpr (Pred sym) (SymBV sym 8))
forall a b. (a -> b) -> a -> b
$ Pred sym -> SymBV sym 8 -> PartExpr (Pred sym) (SymBV sym 8)
forall (p :: BaseType -> *) a.
IsExpr p =>
p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
mkPE Pred sym
valid SymBV sym 8
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' :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> OverrideSim
     p sym arch r args ret (PartExpr (Pred sym) (SymBV sym 8))
readByte' GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl = GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
    -> OverrideSim
         p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
-> OverrideSim
     p sym arch r args ret (PartExpr (Pred sym) (SymBV sym 8))
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall (args' :: Ctx CrucibleType).
    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 GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl ((forall {args' :: Ctx CrucibleType}.
  Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
  -> OverrideSim
       p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
 -> OverrideSim
      p sym arch r args ret (PartExpr (Pred sym) (SymBV sym 8)))
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8))
    -> OverrideSim
         p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
-> OverrideSim
     p sym arch r args ret (PartExpr (Pred sym) (SymBV sym 8))
forall a b. (a -> b) -> a -> b
$ \case
  Left FileHandleError
FileHandleClosed ->
    (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
-> OverrideSim
     p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
 -> OverrideSim
      p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
-> OverrideSim
     p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      IO (PartExpr (Pred sym) (SymBV sym 8))
-> OverrideSim
     p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8))
forall a. IO a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (PartExpr (Pred sym) (SymBV sym 8))
 -> OverrideSim
      p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8)))
-> IO (PartExpr (Pred sym) (SymBV sym 8))
-> OverrideSim
     p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8))
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (PartExpr (Pred sym) (SymBV sym 8))
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (PartExpr (Pred sym) (SymBV sym 8)))
-> SimErrorReason -> IO (PartExpr (Pred sym) (SymBV sym 8))
forall a b. (a -> b) -> a -> b
$
        FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
          FilePath
"Failed to read byte due to closed file handle."
          FilePath
"readByte': Closed file handle"
  Right PartExpr (Pred sym) (SymBV sym 8)
r -> PartExpr (Pred sym) (SymBV sym 8)
-> OverrideSim
     p sym arch r args' ret (PartExpr (Pred sym) (SymBV sym 8))
forall a. a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. Monad m => a -> m a
return PartExpr (Pred sym) (SymBV sym 8)
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 :: forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym wptr
-> (forall (args' :: Ctx CrucibleType).
    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 GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl SymBV sym wptr
sz forall (args' :: Ctx CrucibleType).
Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
-> OverrideSim p sym arch r args' ret a
cont = do
  W4.BaseBVRepr NatRepr w
ptrSz <- BaseTypeRepr (BaseBVType wptr)
-> OverrideSim
     p sym arch r args ret (BaseTypeRepr (BaseBVType wptr))
forall a. a -> OverrideSim p sym arch r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return (BaseTypeRepr (BaseBVType wptr)
 -> OverrideSim
      p sym arch r args ret (BaseTypeRepr (BaseBVType wptr)))
-> BaseTypeRepr (BaseBVType wptr)
-> OverrideSim
     p sym arch r args ret (BaseTypeRepr (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ SymBV sym wptr -> BaseTypeRepr (BaseBVType wptr)
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymBV sym wptr
sz
  let args :: RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
args = Assignment
  (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
-> RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (RegEntry sym) EmptyCtx
-> RegEntry sym ('BaseToType ('BaseBVType w))
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> TypeRepr ('BaseToType ('BaseBVType w))
-> RegValue sym ('BaseToType ('BaseBVType w))
-> RegEntry sym ('BaseToType ('BaseBVType w))
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry (NatRepr w -> TypeRepr ('BaseToType ('BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
ptrSz) RegValue sym ('BaseToType ('BaseBVType w))
SymBV sym wptr
sz)
  GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
    -> OverrideSim p sym arch r (args <+> args'') ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
    -> FileHandle sym wptr
    -> FileM_
         p
         arch
         r
         (args <+> args'')
         ret
         sym
         wptr
         (DataChunk sym wptr, SymBV sym wptr))
-> OverrideSim p sym arch r args ret a
forall p sym arch r (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (ret :: CrucibleType) a b
       (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym args'
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError a
    -> OverrideSim p sym arch r (args <+> args'') ret b)
-> (forall (args'' :: Ctx CrucibleType).
    RegMap sym args'
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMHandleCont GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
args Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
-> OverrideSim p sym arch r (args <+> args'') ret a
forall (args' :: Ctx CrucibleType).
Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
-> OverrideSim p sym arch r args' ret a
forall (args'' :: Ctx CrucibleType).
Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
-> OverrideSim p sym arch r (args <+> args'') ret a
cont ((forall {args'' :: Ctx CrucibleType}.
  RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
  -> FileHandle sym wptr
  -> FileM_
       p
       arch
       r
       (args <+> args'')
       ret
       sym
       wptr
       (DataChunk sym wptr, SymBV sym wptr))
 -> OverrideSim p sym arch r args ret a)
-> (forall {args'' :: Ctx CrucibleType}.
    RegMap sym (EmptyCtx ::> 'BaseToType (BaseBVType wptr))
    -> FileHandle sym wptr
    -> FileM_
         p
         arch
         r
         (args <+> args'')
         ret
         sym
         wptr
         (DataChunk sym wptr, SymBV sym wptr))
-> OverrideSim p sym arch r args ret a
forall a b. (a -> b) -> a -> b
$ \(RegMap (Assignment (RegEntry sym) ctx
Empty :> RegEntry TypeRepr tp
_ RegValue sym tp
sz')) FileHandle sym wptr
fhdl' -> do
    FilePointer sym wptr
ptr <- FileHandle sym wptr
-> FileM
     p arch r (args <+> args'') ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle FileHandle sym wptr
fhdl'
    DataChunk sym wptr
chunk <- FilePointer sym wptr
-> SymBV sym wptr
-> FileM
     p arch r (args <+> args'') ret sym wptr (DataChunk sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (DataChunk sym wptr)
readChunkPointer FilePointer sym wptr
ptr RegValue sym tp
SymBV sym wptr
sz'
    SymBV sym wptr
readSz <- FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r (args <+> args'') ret sym wptr (SymBV sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
incHandleRead FileHandle sym wptr
fhdl' RegValue sym tp
SymBV sym wptr
sz'
    (DataChunk sym wptr, SymBV sym wptr)
-> FileM_
     p
     arch
     r
     (args <+> args'')
     ret
     sym
     wptr
     (DataChunk sym wptr, SymBV sym wptr)
forall a. a -> FileM_ p arch r (args <+> args'') ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataChunk sym wptr
chunk, SymBV sym wptr
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' :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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)
readChunk' GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl SymBV sym wptr
sz = GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym wptr
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
    -> OverrideSim
         p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
-> OverrideSim
     p sym arch r args ret (DataChunk sym wptr, SymBV sym wptr)
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym wptr
-> (forall (args' :: Ctx CrucibleType).
    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 GlobalVar (FileSystemType wptr)
fsVar FileHandle sym wptr
fhdl SymBV sym wptr
sz ((forall {args' :: Ctx CrucibleType}.
  Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
  -> OverrideSim
       p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
 -> OverrideSim
      p sym arch r args ret (DataChunk sym wptr, SymBV sym wptr))
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
    -> OverrideSim
         p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
-> OverrideSim
     p sym arch r args ret (DataChunk sym wptr, SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ \case
  Left FileHandleError
FileHandleClosed ->
    (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
-> OverrideSim
     p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
 -> OverrideSim
      p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
-> OverrideSim
     p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      IO (DataChunk sym wptr, SymBV sym wptr)
-> OverrideSim
     p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr)
forall a. IO a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (DataChunk sym wptr, SymBV sym wptr)
 -> OverrideSim
      p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr))
-> IO (DataChunk sym wptr, SymBV sym wptr)
-> OverrideSim
     p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (DataChunk sym wptr, SymBV sym wptr)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (DataChunk sym wptr, SymBV sym wptr))
-> SimErrorReason -> IO (DataChunk sym wptr, SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$
        FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
          FilePath
"Failed to read array due to closed file handle."
          FilePath
"readArray': Closed file handle"
  Right (DataChunk sym wptr, SymBV sym wptr)
arr -> (DataChunk sym wptr, SymBV sym wptr)
-> OverrideSim
     p sym arch r args' ret (DataChunk sym wptr, SymBV sym wptr)
forall a. a -> OverrideSim p sym arch r args' ret a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataChunk sym wptr, SymBV sym wptr)
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 :: forall sym (wptr :: Natural) p arch args (r :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> OverrideSim p sym arch args r ret (Pred sym)
isHandleOpen GlobalVar (FileSystemType wptr)
fvar FileHandle sym wptr
fhdl = GlobalVar (FileSystemType wptr)
-> FileM_ p arch args r ret sym wptr (Pred sym)
-> OverrideSim p sym arch args r ret (Pred sym)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileM_ p arch r args ret sym wptr a
-> OverrideSim p sym arch r args ret a
runFileM GlobalVar (FileSystemType wptr)
fvar (FileM_ p arch args r ret sym wptr (Pred sym)
 -> OverrideSim p sym arch args r ret (Pred sym))
-> FileM_ p arch args r ret sym wptr (Pred sym)
-> OverrideSim p sym arch args r ret (Pred sym)
forall a b. (a -> b) -> a -> b
$ do
  sym
sym <- FileM_ p arch args r ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  NatRepr wptr
repr <- FileM_ p arch args r ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
  OverrideSim
  p
  sym
  arch
  args
  r
  ret
  (PartExpr (Pred sym) (RegValue sym (FilePointerType wptr)))
-> FileM
     p
     arch
     args
     r
     ret
     sym
     wptr
     (PartExpr (Pred sym) (RegValue sym (FilePointerType wptr)))
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV (TypeRepr ('MaybeType (FilePointerType wptr))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
-> OverrideSim
     p
     sym
     arch
     args
     r
     ret
     (RegValue sym ('MaybeType (FilePointerType wptr)))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
TypeRepr tp
-> MuxTree sym (RefCell tp)
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
C.readMuxTreeRef (TypeRepr (FilePointerType wptr)
-> TypeRepr ('MaybeType (FilePointerType wptr))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (NatRepr wptr -> TypeRepr (FilePointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FilePointerType w) =>
NatRepr w -> TypeRepr ty
FilePointerRepr NatRepr wptr
repr)) MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
FileHandle sym wptr
fhdl) FileM_
  p
  arch
  args
  r
  ret
  sym
  wptr
  (PartExpr (Pred sym) (RegValue sym (FilePointerType wptr)))
-> (PartExpr (Pred sym) (RegValue sym (FilePointerType wptr))
    -> FileM_ p arch args r ret sym wptr (Pred sym))
-> FileM_ p arch args r ret sym wptr (Pred sym)
forall a b.
FileM_ p arch args r ret sym wptr a
-> (a -> FileM_ p arch args r ret sym wptr b)
-> FileM_ p arch args r ret sym wptr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    PE Pred sym
p RegValue sym (FilePointerType wptr)
_ -> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a. a -> FileM_ p arch args r ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return Pred sym
p
    PartExpr (Pred sym) (RegValue sym (FilePointerType wptr))
Unassigned -> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a. a -> FileM_ p arch args r ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.falsePred sym
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 :: forall sym (wptr :: Natural) p arch args (r :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> OverrideSim p sym arch args r ret (FileHandle sym wptr)
invalidFileHandle GlobalVar (FileSystemType wptr)
fvar = GlobalVar (FileSystemType wptr)
-> FileM_ p arch args r ret sym wptr (FileHandle sym wptr)
-> OverrideSim p sym arch args r ret (FileHandle sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileM_ p arch r args ret sym wptr a
-> OverrideSim p sym arch r args ret a
runFileM GlobalVar (FileSystemType wptr)
fvar (FileM_ p arch args r ret sym wptr (FileHandle sym wptr)
 -> OverrideSim p sym arch args r ret (FileHandle sym wptr))
-> FileM_ p arch args r ret sym wptr (FileHandle sym wptr)
-> OverrideSim p sym arch args r ret (FileHandle sym wptr)
forall a b. (a -> b) -> a -> b
$ do
  NatRepr wptr
repr <- FileM_ p arch args r ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
  sym
sym <- FileM_ p arch args r ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  sym
-> RefCell ('MaybeType (FilePointerType wptr))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
toMuxTree sym
sym (RefCell ('MaybeType (FilePointerType wptr))
 -> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
-> FileM_
     p
     arch
     args
     r
     ret
     sym
     wptr
     (RefCell ('MaybeType (FilePointerType wptr)))
-> FileM_
     p
     arch
     args
     r
     ret
     sym
     wptr
     (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (OverrideSim
  p sym arch args r ret (RefCell ('MaybeType (FilePointerType wptr)))
-> FileM
     p
     arch
     args
     r
     ret
     sym
     wptr
     (RefCell ('MaybeType (FilePointerType wptr)))
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV (OverrideSim
   p sym arch args r ret (RefCell ('MaybeType (FilePointerType wptr)))
 -> FileM
      p
      arch
      args
      r
      ret
      sym
      wptr
      (RefCell ('MaybeType (FilePointerType wptr))))
-> OverrideSim
     p sym arch args r ret (RefCell ('MaybeType (FilePointerType wptr)))
-> FileM
     p
     arch
     args
     r
     ret
     sym
     wptr
     (RefCell ('MaybeType (FilePointerType wptr)))
forall a b. (a -> b) -> a -> b
$ TypeRepr ('MaybeType (FilePointerType wptr))
-> OverrideSim
     p sym arch args r ret (RefCell ('MaybeType (FilePointerType wptr)))
forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypeRepr tp -> OverrideSim p sym ext rtp args ret (RefCell tp)
C.newEmptyRef (TypeRepr (FilePointerType wptr)
-> TypeRepr ('MaybeType (FilePointerType wptr))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (NatRepr wptr -> TypeRepr (FilePointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FilePointerType w) =>
NatRepr w -> TypeRepr ty
FilePointerRepr NatRepr wptr
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 :: forall sym (wptr :: Natural) p arch args (r :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym -> OverrideSim p sym arch args r ret (Pred sym)
isFileIdentValid GlobalVar (FileSystemType wptr)
fvar FileIdent sym
ident = GlobalVar (FileSystemType wptr)
-> FileM_ p arch args r ret sym wptr (Pred sym)
-> OverrideSim p sym arch args r ret (Pred sym)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileM_ p arch r args ret sym wptr a
-> OverrideSim p sym arch r args ret a
runFileM GlobalVar (FileSystemType wptr)
fvar (FileM_ p arch args r ret sym wptr (Pred sym)
 -> OverrideSim p sym arch args r ret (Pred sym))
-> FileM_ p arch args r ret sym wptr (Pred sym)
-> OverrideSim p sym arch args r ret (Pred sym)
forall a b. (a -> b) -> a -> b
$ do
  sym
sym <- FileM_ p arch args r ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  Map Text (PartExpr (Pred sym) (File sym wptr))
m <- (FileSystem sym wptr
 -> Map Text (PartExpr (Pred sym) (File sym wptr)))
-> FileM_
     p
     arch
     args
     r
     ret
     sym
     wptr
     (Map Text (PartExpr (Pred sym) (File sym wptr)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> Map Text (PartExpr (Pred sym) (File sym wptr))
FileSystem sym wptr -> RegValue sym (StringMapType (FileType wptr))
forall sym (w :: Natural).
FileSystem sym w -> RegValue sym (StringMapType (FileType w))
fsFileNames
  case SymExpr sym ('BaseStringType Char8) -> Maybe (StringLiteral Char8)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> *) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
W4.asString FileIdent sym
SymExpr sym ('BaseStringType Char8)
ident of
    Just (W4.Char8Literal ByteString
i')
      | Right Text
str <- ByteString -> Either UnicodeException Text
Text.decodeUtf8' ByteString
i'
      -> case Text
-> Map Text (PartExpr (Pred sym) (File sym wptr))
-> Maybe (PartExpr (Pred sym) (File sym wptr))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
str Map Text (PartExpr (Pred sym) (File sym wptr))
m of
      Just PartExpr (Pred sym) (File sym wptr)
_ -> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a. a -> FileM_ p arch args r ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym))
-> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred sym
sym
      Maybe (PartExpr (Pred sym) (File sym wptr))
Nothing -> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a. a -> FileM_ p arch args r ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym))
-> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.falsePred sym
sym
    Maybe (StringLiteral Char8)
_ -> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a. a -> FileM_ p arch args r ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym))
-> Pred sym -> FileM_ p arch args r ret sym wptr (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.falsePred sym
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 { forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
FileM_ p arch r args ret sym wptr a
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
_unFM :: CMS.StateT (FileSystem sym wptr) (C.OverrideSim p sym arch r args ret) a }
  deriving
     ( Functor (FileM_ p arch r args ret sym wptr)
Functor (FileM_ p arch r args ret sym wptr) =>
(forall a. a -> FileM_ p arch r args ret sym wptr a)
-> (forall a b.
    FileM_ p arch r args ret sym wptr (a -> b)
    -> FileM_ p arch r args ret sym wptr a
    -> FileM_ p arch r args ret sym wptr b)
-> (forall a b c.
    (a -> b -> c)
    -> FileM_ p arch r args ret sym wptr a
    -> FileM_ p arch r args ret sym wptr b
    -> FileM_ p arch r args ret sym wptr c)
-> (forall a b.
    FileM_ p arch r args ret sym wptr a
    -> FileM_ p arch r args ret sym wptr b
    -> FileM_ p arch r args ret sym wptr b)
-> (forall a b.
    FileM_ p arch r args ret sym wptr a
    -> FileM_ p arch r args ret sym wptr b
    -> FileM_ p arch r args ret sym wptr a)
-> Applicative (FileM_ p arch r args ret sym wptr)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
forall a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
forall a b.
FileM_ p arch r args ret sym wptr (a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
forall a b c.
(a -> b -> c)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr c
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
Functor (FileM_ p arch r args ret sym wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
a -> FileM_ p arch r args ret sym wptr a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr (a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b c.
(a -> b -> c)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
a -> FileM_ p arch r args ret sym wptr a
pure :: forall a. a -> FileM_ p arch r args ret sym wptr a
$c<*> :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr (a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
<*> :: forall a b.
FileM_ p arch r args ret sym wptr (a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
$cliftA2 :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b c.
(a -> b -> c)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr c
liftA2 :: forall a b c.
(a -> b -> c)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr c
$c*> :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
*> :: forall a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
$c<* :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
<* :: forall a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
Applicative
     , (forall a b.
 (a -> b)
 -> FileM_ p arch r args ret sym wptr a
 -> FileM_ p arch r args ret sym wptr b)
-> (forall a b.
    a
    -> FileM_ p arch r args ret sym wptr b
    -> FileM_ p arch r args ret sym wptr a)
-> Functor (FileM_ p arch r args ret sym wptr)
forall a b.
a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
forall a b.
(a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
(a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
(a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
fmap :: forall a b.
(a -> b)
-> FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
$c<$ :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
<$ :: forall a b.
a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr a
Functor
     , Applicative (FileM_ p arch r args ret sym wptr)
Applicative (FileM_ p arch r args ret sym wptr) =>
(forall a b.
 FileM_ p arch r args ret sym wptr a
 -> (a -> FileM_ p arch r args ret sym wptr b)
 -> FileM_ p arch r args ret sym wptr b)
-> (forall a b.
    FileM_ p arch r args ret sym wptr a
    -> FileM_ p arch r args ret sym wptr b
    -> FileM_ p arch r args ret sym wptr b)
-> (forall a. a -> FileM_ p arch r args ret sym wptr a)
-> Monad (FileM_ p arch r args ret sym wptr)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
forall a b.
FileM_ p arch r args ret sym wptr a
-> (a -> FileM_ p arch r args ret sym wptr b)
-> FileM_ p arch r args ret sym wptr b
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
Applicative (FileM_ p arch r args ret sym wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
a -> FileM_ p arch r args ret sym wptr a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> (a -> FileM_ p arch r args ret sym wptr b)
-> FileM_ p arch r args ret sym wptr b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> (a -> FileM_ p arch r args ret sym wptr b)
-> FileM_ p arch r args ret sym wptr b
>>= :: forall a b.
FileM_ p arch r args ret sym wptr a
-> (a -> FileM_ p arch r args ret sym wptr b)
-> FileM_ p arch r args ret sym wptr b
$c>> :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
>> :: forall a b.
FileM_ p arch r args ret sym wptr a
-> FileM_ p arch r args ret sym wptr b
-> FileM_ p arch r args ret sym wptr b
$creturn :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
a -> FileM_ p arch r args ret sym wptr a
return :: forall a. a -> FileM_ p arch r args ret sym wptr a
Monad
     , Monad (FileM_ p arch r args ret sym wptr)
Monad (FileM_ p arch r args ret sym wptr) =>
(forall a. IO a -> FileM_ p arch r args ret sym wptr a)
-> MonadIO (FileM_ p arch r args ret sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
Monad (FileM_ p arch r args ret sym wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
IO a -> FileM_ p arch r args ret sym wptr a
liftIO :: forall a. IO a -> FileM_ p arch r args ret sym wptr a
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 :: forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV OverrideSim p sym arch r args ret a
f = StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileM_ p arch r args ret sym wptr a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileM_ p arch r args ret sym wptr a
FileM (StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
 -> FileM_ p arch r args ret sym wptr a)
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileM_ p arch r args ret sym wptr a
forall a b. (a -> b) -> a -> b
$ OverrideSim p sym arch r args ret a
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (FileSystem sym wptr) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
CMT.lift OverrideSim p sym arch r args ret a
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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileM_ p arch r args ret sym wptr a
-> OverrideSim p sym arch r args ret a
runFileM GlobalVar (FileSystemType wptr)
fvar (FileM StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
f) = do
  FileSystem sym wptr
fs <- GlobalVar (FileSystemType wptr)
-> OverrideSim
     p sym arch r args ret (RegValue sym (FileSystemType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
C.readGlobal GlobalVar (FileSystemType wptr)
fvar
  (a
a, FileSystem sym wptr
fs') <- StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileSystem sym wptr
-> OverrideSim p sym arch r args ret (a, FileSystem sym wptr)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
CMS.runStateT StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
f FileSystem sym wptr
fs
  GlobalVar (FileSystemType wptr)
-> RegValue sym (FileSystemType wptr)
-> OverrideSim p sym arch r args ret ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
C.writeGlobal GlobalVar (FileSystemType wptr)
fvar RegValue sym (FileSystemType wptr)
FileSystem sym wptr
fs'
  a -> OverrideSim p sym arch r args ret a
forall a. a -> OverrideSim p sym arch r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return a
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 :: forall p sym arch r (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (ret :: CrucibleType) a b
       (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> RegMap sym args'
-> (forall (args'' :: Ctx CrucibleType).
    Either FileHandleError a
    -> OverrideSim p sym arch r (args <+> args'') ret b)
-> (forall (args'' :: Ctx CrucibleType).
    RegMap sym args'
    -> FileHandle sym wptr
    -> FileM_ p arch r (args <+> args'') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMHandleCont GlobalVar (FileSystemType wptr)
fvar FileHandle sym wptr
fhdl (RegMap Assignment (RegEntry sym) args'
args') forall (args'' :: Ctx CrucibleType).
Either FileHandleError a
-> OverrideSim p sym arch r (args <+> args'') ret b
cont forall (args'' :: Ctx CrucibleType).
RegMap sym args'
-> FileHandle sym wptr
-> FileM_ p arch r (args <+> args'') ret sym wptr a
f = do
  FileSystem sym wptr
fs <- GlobalVar (FileSystemType wptr)
-> OverrideSim
     p sym arch r args ret (RegValue sym (FileSystemType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
C.readGlobal GlobalVar (FileSystemType wptr)
fvar
  SymExpr sym BaseBoolType
p <- GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> OverrideSim p sym arch r args ret (SymExpr sym BaseBoolType)
forall sym (wptr :: Natural) p arch args (r :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> OverrideSim p sym arch args r ret (Pred sym)
isHandleOpen GlobalVar (FileSystemType wptr)
fvar FileHandle sym wptr
fhdl
  sym
sym <- OverrideSim p sym arch r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
C.getSymInterface
  RegMap sym args
args <- OverrideSim p sym arch r args ret (RegMap sym args)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
C.getOverrideArgs
  let
    cont' :: Either FileHandleError a
-> OverrideSim
     p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b
cont' = forall (args'' :: Ctx CrucibleType).
Either FileHandleError a
-> OverrideSim p sym arch r (args <+> args'') ret b
cont @(args' ::> FileHandleType wptr)
    args'' :: RegMap sym (args' ::> FileHandleType wptr)
args'' = Assignment (RegEntry sym) (args' ::> FileHandleType wptr)
-> RegMap sym (args' ::> FileHandleType wptr)
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) args'
args' Assignment (RegEntry sym) args'
-> RegEntry sym (FileHandleType wptr)
-> Assignment (RegEntry sym) (args' ::> FileHandleType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> TypeRepr (FileHandleType wptr)
-> FileHandle sym wptr -> RegEntry sym (FileHandleType wptr)
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry (NatRepr wptr -> TypeRepr (FileHandleType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FileHandleType w) =>
NatRepr w -> TypeRepr ty
FileHandleRepr (FileSystem sym wptr -> NatRepr wptr
forall sym (w :: Natural). FileSystem sym w -> NatRepr w
fsPtrSize FileSystem sym wptr
fs)) FileHandle sym wptr
fhdl)
    resultCase :: C.OverrideSim p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b
    resultCase :: OverrideSim
  p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b
resultCase = do
      (RegMap sym (args <+> args')
args_args', RegEntry TypeRepr (FileHandleType wptr)
_ FileHandle sym wptr
fhdl') <- RegMap sym ((args <+> args') ::> FileHandleType wptr)
-> (RegMap sym (args <+> args'),
    RegEntry sym (FileHandleType wptr))
forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym (ctx ::> tp) -> (RegMap sym ctx, RegEntry sym tp)
unconsReg (RegMap sym ((args <+> args') ::> FileHandleType wptr)
 -> (RegMap sym (args <+> args'),
     RegEntry sym (FileHandleType wptr)))
-> OverrideSim
     p
     sym
     arch
     r
     ((args <+> args') ::> FileHandleType wptr)
     ret
     (RegMap sym ((args <+> args') ::> FileHandleType wptr))
-> OverrideSim
     p
     sym
     arch
     r
     ((args <+> args') ::> FileHandleType wptr)
     ret
     (RegMap sym (args <+> args'), RegEntry sym (FileHandleType wptr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim
  p
  sym
  arch
  r
  ((args <+> args') ::> FileHandleType wptr)
  ret
  (RegMap sym ((args <+> args') ::> FileHandleType wptr))
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
C.getOverrideArgs
      let (RegMap sym args
_, RegMap sym args'
args'_) = Size args
-> Size args'
-> RegMap sym (args <+> args')
-> (RegMap sym args, RegMap sym args')
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) sym.
Size ctx
-> Size ctx'
-> RegMap sym (ctx <+> ctx')
-> (RegMap sym ctx, RegMap sym ctx')
splitRegs (RegMap sym args -> Size args
forall sym (ctx :: Ctx CrucibleType). RegMap sym ctx -> Size ctx
regMapSize RegMap sym args
args) (Assignment (RegEntry sym) args' -> Size args'
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (RegEntry sym) args'
args') RegMap sym (args <+> args')
args_args'
      a
a <- GlobalVar (FileSystemType wptr)
-> FileM_
     p arch r ((args <+> args') ::> FileHandleType wptr) ret sym wptr a
-> OverrideSim
     p sym arch r ((args <+> args') ::> FileHandleType wptr) ret a
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileM_ p arch r args ret sym wptr a
-> OverrideSim p sym arch r args ret a
runFileM GlobalVar (FileSystemType wptr)
fvar (forall (args'' :: Ctx CrucibleType).
RegMap sym args'
-> FileHandle sym wptr
-> FileM_ p arch r (args <+> args'') ret sym wptr a
f @(args' ::> FileHandleType wptr) RegMap sym args'
args'_ FileHandle sym wptr
fhdl')
      Either FileHandleError a
-> OverrideSim
     p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b
cont' (a -> Either FileHandleError a
forall a b. b -> Either a b
Right a
a)

  RegMap sym (args' ::> FileHandleType wptr)
-> [(SymExpr sym BaseBoolType,
     OverrideSim
       p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b,
     Maybe Position)]
-> OverrideSim p sym arch r args ret b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (new_args :: Ctx CrucibleType) (res :: CrucibleType) a.
IsSymInterface sym =>
RegMap sym new_args
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> OverrideSim p sym ext rtp args res a
C.symbolicBranches RegMap sym (args' ::> FileHandleType wptr)
args''
    [(SymExpr sym BaseBoolType
p, OverrideSim
  p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b
resultCase, Maybe Position
forall a. Maybe a
Nothing)
    ,(sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred sym
sym, Either FileHandleError a
-> OverrideSim
     p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b
cont' (FileHandleError -> Either FileHandleError a
forall a b. a -> Either a b
Left FileHandleError
FileHandleClosed), Maybe Position
forall a. Maybe a
Nothing)
    ]

splitRegs ::
  Ctx.Size ctx ->
  Ctx.Size ctx' ->
  RegMap sym (ctx <+> ctx') ->
  (RegMap sym ctx, RegMap sym ctx')
splitRegs :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) sym.
Size ctx
-> Size ctx'
-> RegMap sym (ctx <+> ctx')
-> (RegMap sym ctx, RegMap sym ctx')
splitRegs Size ctx
sz Size ctx'
sz' (RegMap Assignment (RegEntry sym) (ctx <+> ctx')
m) = (Assignment (RegEntry sym) ctx -> RegMap sym ctx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Size ctx
-> Size ctx'
-> Assignment (RegEntry sym) (ctx <+> ctx')
-> Assignment (RegEntry sym) ctx
forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx
-> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
Ctx.take Size ctx
sz Size ctx'
sz' Assignment (RegEntry sym) (ctx <+> ctx')
m), Assignment (RegEntry sym) ctx' -> RegMap sym ctx'
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Size ctx
-> Size ctx'
-> Assignment (RegEntry sym) (ctx <+> ctx')
-> Assignment (RegEntry sym) ctx'
forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx
-> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
Ctx.drop Size ctx
sz Size ctx'
sz' Assignment (RegEntry sym) (ctx <+> ctx')
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 :: forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a b (wptr :: Natural).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall (args' :: Ctx CrucibleType).
    Either FileIdentError a
    -> OverrideSim p sym arch r (args <+> args') ret b)
-> (forall (args' :: Ctx CrucibleType).
    FileIdent sym -> FileM_ p arch r (args <+> args') ret sym wptr a)
-> OverrideSim p sym arch r args ret b
runFileMIdentCont GlobalVar (FileSystemType wptr)
fvar FileIdent sym
ident forall (args' :: Ctx CrucibleType).
Either FileIdentError a
-> OverrideSim p sym arch r (args <+> args') ret b
cont forall (args' :: Ctx CrucibleType).
FileIdent sym -> FileM_ p arch r (args <+> args') ret sym wptr a
f = do
  SymExpr sym BaseBoolType
p <- GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> OverrideSim p sym arch r args ret (SymExpr sym BaseBoolType)
forall sym (wptr :: Natural) p arch args (r :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym -> OverrideSim p sym arch args r ret (Pred sym)
isFileIdentValid GlobalVar (FileSystemType wptr)
fvar FileIdent sym
ident
  sym
sym <- OverrideSim p sym arch r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
C.getSymInterface
  let
    cont' :: Either FileIdentError a
-> OverrideSim
     p
     sym
     arch
     r
     (args <+> (EmptyCtx ::> 'BaseToType ('BaseStringType Char8)))
     ret
     b
cont' = forall (args' :: Ctx CrucibleType).
Either FileIdentError a
-> OverrideSim p sym arch r (args <+> args') ret b
cont @(EmptyCtx ::> FileIdentType)
    args' :: RegMap sym (EmptyCtx ::> 'BaseToType ('BaseStringType Char8))
args' = Assignment
  (RegEntry sym) (EmptyCtx ::> 'BaseToType ('BaseStringType Char8))
-> RegMap sym (EmptyCtx ::> 'BaseToType ('BaseStringType Char8))
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (RegEntry sym) EmptyCtx
-> RegEntry sym ('BaseToType ('BaseStringType Char8))
-> Assignment
     (RegEntry sym) (EmptyCtx ::> 'BaseToType ('BaseStringType Char8))
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> TypeRepr ('BaseToType ('BaseStringType Char8))
-> FileIdent sym
-> RegEntry sym ('BaseToType ('BaseStringType Char8))
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry (StringInfoRepr Char8
-> TypeRepr ('BaseToType ('BaseStringType Char8))
forall (si :: StringInfo).
StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
StringRepr StringInfoRepr Char8
Char8Repr) FileIdent sym
ident)
    resultCase :: C.OverrideSim p sym arch r (args ::> FileIdentType) ret b
    resultCase :: OverrideSim
  p sym arch r (args ::> 'BaseToType ('BaseStringType Char8)) ret b
resultCase = do
      (RegMap sym args
_, RegEntry TypeRepr ('BaseToType ('BaseStringType Char8))
_ FileIdent sym
fhdl') <- RegMap sym (args ::> 'BaseToType ('BaseStringType Char8))
-> (RegMap sym args,
    RegEntry sym ('BaseToType ('BaseStringType Char8)))
forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym (ctx ::> tp) -> (RegMap sym ctx, RegEntry sym tp)
unconsReg (RegMap sym (args ::> 'BaseToType ('BaseStringType Char8))
 -> (RegMap sym args,
     RegEntry sym ('BaseToType ('BaseStringType Char8))))
-> OverrideSim
     p
     sym
     arch
     r
     (args ::> 'BaseToType ('BaseStringType Char8))
     ret
     (RegMap sym (args ::> 'BaseToType ('BaseStringType Char8)))
-> OverrideSim
     p
     sym
     arch
     r
     (args ::> 'BaseToType ('BaseStringType Char8))
     ret
     (RegMap sym args,
      RegEntry sym ('BaseToType ('BaseStringType Char8)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim
  p
  sym
  arch
  r
  (args ::> 'BaseToType ('BaseStringType Char8))
  ret
  (RegMap sym (args ::> 'BaseToType ('BaseStringType Char8)))
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
C.getOverrideArgs
      a
a <- GlobalVar (FileSystemType wptr)
-> FileM_
     p
     arch
     r
     (args ::> 'BaseToType ('BaseStringType Char8))
     ret
     sym
     wptr
     a
-> OverrideSim
     p sym arch r (args ::> 'BaseToType ('BaseStringType Char8)) ret a
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileM_ p arch r args ret sym wptr a
-> OverrideSim p sym arch r args ret a
runFileM GlobalVar (FileSystemType wptr)
fvar (forall (args' :: Ctx CrucibleType).
FileIdent sym -> FileM_ p arch r (args <+> args') ret sym wptr a
f @(EmptyCtx ::> FileIdentType) FileIdent sym
fhdl')
      Either FileIdentError a
-> OverrideSim
     p
     sym
     arch
     r
     (args <+> (EmptyCtx ::> 'BaseToType ('BaseStringType Char8)))
     ret
     b
cont' (a -> Either FileIdentError a
forall a b. b -> Either a b
Right a
a)

  RegMap sym (EmptyCtx ::> 'BaseToType ('BaseStringType Char8))
-> [(SymExpr sym BaseBoolType,
     OverrideSim
       p
       sym
       arch
       r
       (args <+> (EmptyCtx ::> 'BaseToType ('BaseStringType Char8)))
       ret
       b,
     Maybe Position)]
-> OverrideSim p sym arch r args ret b
forall p sym ext rtp (args :: Ctx CrucibleType)
       (new_args :: Ctx CrucibleType) (res :: CrucibleType) a.
IsSymInterface sym =>
RegMap sym new_args
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> OverrideSim p sym ext rtp args res a
C.symbolicBranches RegMap sym (EmptyCtx ::> 'BaseToType ('BaseStringType Char8))
args'
    [(SymExpr sym BaseBoolType
p, OverrideSim
  p sym arch r (args ::> 'BaseToType ('BaseStringType Char8)) ret b
OverrideSim
  p
  sym
  arch
  r
  (args <+> (EmptyCtx ::> 'BaseToType ('BaseStringType Char8)))
  ret
  b
resultCase, Maybe Position
forall a. Maybe a
Nothing)
    ,(sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred sym
sym, Either FileIdentError a
-> OverrideSim
     p
     sym
     arch
     r
     (args <+> (EmptyCtx ::> 'BaseToType ('BaseStringType Char8)))
     ret
     b
cont' (FileIdentError -> Either FileIdentError a
forall a b. a -> Either a b
Left FileIdentError
FileNotFound), Maybe Position
forall a. Maybe a
Nothing)
    ]

getSym :: FileM p arch r args ret sym wptr sym
getSym :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym = OverrideSim p sym arch r args ret sym
-> FileM p arch r args ret sym wptr sym
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV OverrideSim p sym arch r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
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 :: forall sym p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural) a.
(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 forall bak.
IsSymBackend sym bak =>
bak -> FileM p arch r args ret sym wptr a
k =
  StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileM_ p arch r args ret sym wptr a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileM_ p arch r args ret sym wptr a
FileM (StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
 -> FileM_ p arch r args ret sym wptr a)
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileM_ p arch r args ret sym wptr a
forall a b. (a -> b) -> a -> b
$ (FileSystem sym wptr
 -> OverrideSim p sym arch r args ret (a, FileSystem sym wptr))
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
CMS.StateT ((FileSystem sym wptr
  -> OverrideSim p sym arch r args ret (a, FileSystem sym wptr))
 -> StateT
      (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a)
-> (FileSystem sym wptr
    -> OverrideSim p sym arch r args ret (a, FileSystem sym wptr))
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
forall a b. (a -> b) -> a -> b
$ \FileSystem sym wptr
st ->
    (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym arch r args ret (a, FileSystem sym wptr))
-> OverrideSim p sym arch r args ret (a, FileSystem sym wptr)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
C.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym arch r args ret (a, FileSystem sym wptr))
 -> OverrideSim p sym arch r args ret (a, FileSystem sym wptr))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym arch r args ret (a, FileSystem sym wptr))
-> OverrideSim p sym arch r args ret (a, FileSystem sym wptr)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      StateT (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
-> FileSystem sym wptr
-> OverrideSim p sym arch r args ret (a, FileSystem sym wptr)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
CMS.runStateT (FileM_ p arch r args ret sym wptr a
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural) a.
FileM_ p arch r args ret sym wptr a
-> StateT
     (FileSystem sym wptr) (OverrideSim p sym arch r args ret) a
_unFM (bak -> FileM p arch r args ret sym wptr a
forall bak.
IsSymBackend sym bak =>
bak -> FileM p arch r args ret sym wptr a
k bak
bak)) FileSystem sym wptr
st

getPtrSz :: FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz :: forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz = (FileSystem sym wptr -> NatRepr wptr)
-> FileM_ p arch r args ret sym wptr (NatRepr wptr)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr -> NatRepr wptr
forall sym (w :: Natural). FileSystem sym w -> NatRepr w
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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
getFileSize FileHandle sym wptr
fhdl = do
  (FilePointer (File NatRepr wptr
_ SymInteger sym
fileid) SymBV sym wptr
_, SymExpr sym BaseBoolType
_) <- FileHandle sym wptr
-> FileM
     p
     arch
     r
     args
     ret
     sym
     wptr
     (FilePointer sym wptr, SymExpr sym BaseBoolType)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
readHandle FileHandle sym wptr
fhdl
  CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray <- (FileSystem sym wptr
 -> CachedArray
      sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
fsFileSizes
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> FileM_ p arch r args ret sym wptr (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym
-> Assignment (SymExpr sym) (EmptyCtx ::> BaseIntegerType)
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
-> IO (SymBV sym wptr)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Assignment (SymExpr sym) idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
CA.readSingle sym
sym (Assignment (SymExpr sym) EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment (SymExpr sym) EmptyCtx
-> SymInteger sym
-> Assignment (SymExpr sym) (EmptyCtx ::> BaseIntegerType)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> SymInteger sym
fileid) CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray

readHandle ::
  FileHandle sym wptr ->
  FileM p arch r args ret sym wptr (FilePointer sym wptr, W4.Pred sym)
readHandle :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
readHandle FileHandle sym wptr
fhandle = do
  NatRepr wptr
repr <- FileM_ p arch r args ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
  OverrideSim
  p sym arch r args ret (PartExpr (Pred sym) (FilePointer sym wptr))
-> FileM
     p
     arch
     r
     args
     ret
     sym
     wptr
     (PartExpr (Pred sym) (FilePointer sym wptr))
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV (TypeRepr ('MaybeType (FilePointerType wptr))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
-> OverrideSim
     p
     sym
     arch
     r
     args
     ret
     (RegValue sym ('MaybeType (FilePointerType wptr)))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
TypeRepr tp
-> MuxTree sym (RefCell tp)
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
C.readMuxTreeRef (TypeRepr (FilePointerType wptr)
-> TypeRepr ('MaybeType (FilePointerType wptr))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (NatRepr wptr -> TypeRepr (FilePointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FilePointerType w) =>
NatRepr w -> TypeRepr ty
FilePointerRepr NatRepr wptr
repr)) MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
FileHandle sym wptr
fhandle) FileM_
  p
  arch
  r
  args
  ret
  sym
  wptr
  (PartExpr (Pred sym) (FilePointer sym wptr))
-> (PartExpr (Pred sym) (FilePointer sym wptr)
    -> FileM_
         p arch r args ret sym wptr (FilePointer sym wptr, Pred sym))
-> FileM_
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
forall a b.
FileM_ p arch r args ret sym wptr a
-> (a -> FileM_ p arch r args ret sym wptr b)
-> FileM_ p arch r args ret sym wptr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    PE Pred sym
p FilePointer sym wptr
v -> (FilePointer sym wptr, Pred sym)
-> FileM_
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePointer sym wptr
v, Pred sym
p)
    PartExpr (Pred sym) (FilePointer sym wptr)
Unassigned ->
      (forall bak.
 IsSymBackend sym bak =>
 bak
 -> FileM
      p arch r args ret sym wptr (FilePointer sym wptr, Pred sym))
-> FileM
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
forall sym p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural) a.
(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 ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> FileM
       p arch r args ret sym wptr (FilePointer sym wptr, Pred sym))
 -> FileM
      p arch r args ret sym wptr (FilePointer sym wptr, Pred sym))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> FileM
         p arch r args ret sym wptr (FilePointer sym wptr, Pred sym))
-> FileM
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
        IO (FilePointer sym wptr, Pred sym)
-> FileM_
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (FilePointer sym wptr, Pred sym)
 -> FileM_
      p arch r args ret sym wptr (FilePointer sym wptr, Pred sym))
-> IO (FilePointer sym wptr, Pred sym)
-> FileM_
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (FilePointer sym wptr, Pred sym)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (FilePointer sym wptr, Pred sym))
-> SimErrorReason -> IO (FilePointer sym wptr, Pred sym)
forall a b. (a -> b) -> a -> b
$
          FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
            FilePath
"Read from closed file handle."
            FilePath
"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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle FileHandle sym wptr
fhandle = do
  (FilePointer sym wptr
v, SymExpr sym BaseBoolType
p) <- FileHandle sym wptr
-> FileM
     p
     arch
     r
     args
     ret
     sym
     wptr
     (FilePointer sym wptr, SymExpr sym BaseBoolType)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
readHandle FileHandle sym wptr
fhandle
  (forall bak.
 IsSymBackend sym bak =>
 bak -> FileM p arch r args ret sym wptr ())
-> FileM p arch r args ret sym wptr ()
forall sym p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural) a.
(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 ((forall bak.
  IsSymBackend sym bak =>
  bak -> FileM p arch r args ret sym wptr ())
 -> FileM p arch r args ret sym wptr ())
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> FileM p arch r args ret sym wptr ())
-> FileM p arch r args ret sym wptr ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    IO () -> FileM_ p arch r args ret sym wptr ()
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FileM_ p arch r args ret sym wptr ())
-> IO () -> FileM_ p arch r args ret sym wptr ()
forall a b. (a -> b) -> a -> b
$ bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
p (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$
      FilePath -> FilePath -> SimErrorReason
AssertFailureSimError
        FilePath
"Read from closed file handle."
        FilePath
"getHandle: File handle assertion failed."
  FilePointer sym wptr
-> FileM_ p arch r args ret sym wptr (FilePointer sym wptr)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return FilePointer sym wptr
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 :: forall sym p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural).
FileIdent sym -> FileM p arch r args ret sym wptr (File sym wptr)
resolveFileIdent FileIdent sym
ident = do
  Map Text (PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
m <- (FileSystem sym wptr
 -> Map Text (PartExpr (SymExpr sym BaseBoolType) (File sym wptr)))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (File sym wptr)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> Map Text (PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
FileSystem sym wptr -> RegValue sym (StringMapType (FileType wptr))
forall sym (w :: Natural).
FileSystem sym w -> RegValue sym (StringMapType (FileType w))
fsFileNames
  let missingErr :: SimErrorReason
missingErr = FilePath -> FilePath -> SimErrorReason
AssertFailureSimError FilePath
"missing file"
                     FilePath
"resolveFileIdent attempted to lookup a file handle that does not exist"
  (forall bak.
 IsSymBackend sym bak =>
 bak -> FileM p arch r args ret sym wptr (File sym wptr))
-> FileM p arch r args ret sym wptr (File sym wptr)
forall sym p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (wptr :: Natural) a.
(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 ((forall bak.
  IsSymBackend sym bak =>
  bak -> FileM p arch r args ret sym wptr (File sym wptr))
 -> FileM p arch r args ret sym wptr (File sym wptr))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> FileM p arch r args ret sym wptr (File sym wptr))
-> FileM p arch r args ret sym wptr (File sym wptr)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    case SymExpr sym ('BaseStringType Char8) -> Maybe (StringLiteral Char8)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> *) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
W4.asString FileIdent sym
SymExpr sym ('BaseStringType Char8)
ident of
      Just (W4.Char8Literal ByteString
i')
        | Right Text
str <- ByteString -> Either UnicodeException Text
Text.decodeUtf8' ByteString
i'
        -> case Text
-> Map Text (PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
-> Maybe (PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
str Map Text (PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
m of
        Just PartExpr (SymExpr sym BaseBoolType) (File sym wptr)
n -> IO (File sym wptr)
-> FileM_ p arch r args ret sym wptr (File sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (File sym wptr)
 -> FileM_ p arch r args ret sym wptr (File sym wptr))
-> IO (File sym wptr)
-> FileM_ p arch r args ret sym wptr (File sym wptr)
forall a b. (a -> b) -> a -> b
$ bak
-> PartExpr (SymExpr sym BaseBoolType) (File sym wptr)
-> SimErrorReason
-> IO (File sym wptr)
forall sym bak v.
IsSymBackend sym bak =>
bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
readPartExpr bak
bak PartExpr (SymExpr sym BaseBoolType) (File sym wptr)
n SimErrorReason
missingErr
        Maybe (PartExpr (SymExpr sym BaseBoolType) (File sym wptr))
Nothing -> IO (File sym wptr)
-> FileM_ p arch r args ret sym wptr (File sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (File sym wptr)
 -> FileM_ p arch r args ret sym wptr (File sym wptr))
-> IO (File sym wptr)
-> FileM_ p arch r args ret sym wptr (File sym wptr)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (File sym wptr)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak SimErrorReason
missingErr
      Maybe (StringLiteral Char8)
_ -> IO (File sym wptr)
-> FileM_ p arch r args ret sym wptr (File sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (File sym wptr)
 -> FileM_ p arch r args ret sym wptr (File sym wptr))
-> IO (File sym wptr)
-> FileM_ p arch r args ret sym wptr (File sym wptr)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (File sym wptr)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (File sym wptr))
-> SimErrorReason -> IO (File sym wptr)
forall a b. (a -> b) -> a -> b
$
             CallStack -> FilePath -> SimErrorReason
Unsupported CallStack
HasCallStack => CallStack
callStack FilePath
"Unsupported string in resolveFileIdent"


openResolvedFile ::
  File sym wptr ->
  FileM p arch r args ret sym wptr (FileHandle sym wptr)
openResolvedFile :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
File sym wptr
-> FileM p arch r args ret sym wptr (FileHandle sym wptr)
openResolvedFile File sym wptr
file = do
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  NatRepr wptr
repr <- FileM_ p arch r args ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
  SymExpr sym (BaseBVType wptr)
zero <- IO (SymExpr sym (BaseBVType wptr))
-> FileM_
     p arch r args ret sym wptr (SymExpr sym (BaseBVType wptr))
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType wptr))
 -> FileM_
      p arch r args ret sym wptr (SymExpr sym (BaseBVType wptr)))
-> IO (SymExpr sym (BaseBVType wptr))
-> FileM_
     p arch r args ret sym wptr (SymExpr sym (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym NatRepr wptr
repr (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr wptr
repr Integer
0)
  MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
ref <- sym
-> RefCell ('MaybeType (FilePointerType wptr))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
toMuxTree sym
sym (RefCell ('MaybeType (FilePointerType wptr))
 -> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (RefCell ('MaybeType (FilePointerType wptr)))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (OverrideSim
  p sym arch r args ret (RefCell ('MaybeType (FilePointerType wptr)))
-> FileM
     p
     arch
     r
     args
     ret
     sym
     wptr
     (RefCell ('MaybeType (FilePointerType wptr)))
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV (OverrideSim
   p sym arch r args ret (RefCell ('MaybeType (FilePointerType wptr)))
 -> FileM
      p
      arch
      r
      args
      ret
      sym
      wptr
      (RefCell ('MaybeType (FilePointerType wptr))))
-> OverrideSim
     p sym arch r args ret (RefCell ('MaybeType (FilePointerType wptr)))
-> FileM
     p
     arch
     r
     args
     ret
     sym
     wptr
     (RefCell ('MaybeType (FilePointerType wptr)))
forall a b. (a -> b) -> a -> b
$ TypeRepr ('MaybeType (FilePointerType wptr))
-> OverrideSim
     p sym arch r args ret (RefCell ('MaybeType (FilePointerType wptr)))
forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypeRepr tp -> OverrideSim p sym ext rtp args ret (RefCell tp)
C.newEmptyRef (TypeRepr (FilePointerType wptr)
-> TypeRepr ('MaybeType (FilePointerType wptr))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (NatRepr wptr -> TypeRepr (FilePointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FilePointerType w) =>
NatRepr w -> TypeRepr ty
FilePointerRepr NatRepr wptr
repr)))
  FileHandle sym wptr
-> FilePointer sym wptr -> FileM p arch r args ret sym wptr ()
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FilePointer sym wptr -> FileM p arch r args ret sym wptr ()
setHandle MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
FileHandle sym wptr
ref (File sym wptr
-> SymExpr sym (BaseBVType wptr) -> FilePointer sym wptr
forall sym (w :: Natural).
File sym w -> SymBV sym w -> FilePointer sym w
FilePointer File sym wptr
file SymExpr sym (BaseBVType wptr)
zero)
  MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
forall a. a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
ref

setHandle ::
  FileHandle sym wptr ->
  FilePointer sym wptr ->
  FileM p arch r args ret sym wptr ()
setHandle :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FilePointer sym wptr -> FileM p arch r args ret sym wptr ()
setHandle FileHandle sym wptr
fhandle FilePointer sym wptr
ptr = do
  NatRepr wptr
repr <- FileM_ p arch r args ret sym wptr (NatRepr wptr)
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr (NatRepr wptr)
getPtrSz
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  let ptr' :: PartExpr (Pred sym) (FilePointer sym wptr)
ptr' = sym
-> FilePointer sym wptr
-> PartExpr (Pred sym) (FilePointer sym wptr)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
justPartExpr sym
sym FilePointer sym wptr
ptr
  OverrideSim p sym arch r args ret ()
-> FileM p arch r args ret sym wptr ()
forall p sym arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a (wptr :: Natural).
OverrideSim p sym arch r args ret a
-> FileM p arch r args ret sym wptr a
liftOV (OverrideSim p sym arch r args ret ()
 -> FileM p arch r args ret sym wptr ())
-> OverrideSim p sym arch r args ret ()
-> FileM p arch r args ret sym wptr ()
forall a b. (a -> b) -> a -> b
$ TypeRepr ('MaybeType (FilePointerType wptr))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
-> RegValue sym ('MaybeType (FilePointerType wptr))
-> OverrideSim p sym arch r args ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
TypeRepr tp
-> MuxTree sym (RefCell tp)
-> RegValue sym tp
-> OverrideSim p sym ext rtp args ret ()
C.writeMuxTreeRef (TypeRepr (FilePointerType wptr)
-> TypeRepr ('MaybeType (FilePointerType wptr))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (NatRepr wptr -> TypeRepr (FilePointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FilePointerType w) =>
NatRepr w -> TypeRepr ty
FilePointerRepr NatRepr wptr
repr)) MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
FileHandle sym wptr
fhandle RegValue sym ('MaybeType (FilePointerType wptr))
PartExpr (Pred sym) (FilePointer sym wptr)
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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (Pred sym, SymBV sym wptr)
bytesOverrun FileHandle sym wptr
fhandle (FilePointer File sym wptr
_ SymBV sym wptr
ptrOff) = do
  SymBV sym wptr
sz <- FileHandle sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
getFileSize FileHandle sym wptr
fhandle
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  Pred sym
inbounds <- IO (Pred sym) -> FileM_ p arch r args ret sym wptr (Pred sym)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Pred sym) -> FileM_ p arch r args ret sym wptr (Pred sym))
-> IO (Pred sym) -> FileM_ p arch r args ret sym wptr (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym wptr -> SymBV sym wptr -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUle sym
sym SymBV sym wptr
ptrOff SymBV sym wptr
sz
  SymBV sym wptr
overrun <- IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> FileM_ p arch r args ret sym wptr (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym wptr -> SymBV sym wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSub sym
sym SymBV sym wptr
ptrOff SymBV sym wptr
sz
  (Pred sym, SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (Pred sym, SymBV sym wptr)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Pred sym, SymBV sym wptr)
 -> FileM_ p arch r args ret sym wptr (Pred sym, SymBV sym wptr))
-> (Pred sym, SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (Pred sym, SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ (Pred sym
inbounds, SymBV sym wptr
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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
incHandleRead FileHandle sym wptr
fhandle SymBV sym wptr
sz = do
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  FilePointer sym wptr
basePtr <- FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle FileHandle sym wptr
fhandle
  FilePointer sym wptr
ptr <- SymBV sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
SymBV sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
addToPointer SymBV sym wptr
sz FilePointer sym wptr
basePtr
  (SymExpr sym BaseBoolType
inbounds, SymBV sym wptr
overrun) <- FileHandle sym wptr
-> FilePointer sym wptr
-> FileM
     p
     arch
     r
     args
     ret
     sym
     wptr
     (SymExpr sym BaseBoolType, SymBV sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (Pred sym, SymBV sym wptr)
bytesOverrun FileHandle sym wptr
fhandle FilePointer sym wptr
ptr
  SymBV sym wptr
off <- IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> FileM_ p arch r args ret sym wptr (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym wptr -> SymBV sym wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSub sym
sym SymBV sym wptr
sz SymBV sym wptr
overrun
  SymBV sym wptr
readBytes <- IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> FileM_ p arch r args ret sym wptr (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymBV sym wptr
-> SymBV sym wptr
-> IO (SymBV sym wptr)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym
-> SymExpr sym BaseBoolType
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
W4.baseTypeIte sym
sym SymExpr sym BaseBoolType
inbounds SymBV sym wptr
sz SymBV sym wptr
off
  FilePointer sym wptr
ptr' <- SymBV sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
SymBV sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
addToPointer SymBV sym wptr
readBytes FilePointer sym wptr
basePtr
  FileHandle sym wptr
-> FilePointer sym wptr -> FileM p arch r args ret sym wptr ()
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FilePointer sym wptr -> FileM p arch r args ret sym wptr ()
setHandle FileHandle sym wptr
fhandle FilePointer sym wptr
ptr'
  SymBV sym wptr
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return SymBV sym wptr
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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym wptr)
incHandleWrite FileHandle sym wptr
fhandle SymBV sym wptr
sz = do
  FilePointer sym wptr
basePtr <- FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
getHandle FileHandle sym wptr
fhandle
  FilePointer sym wptr
ptr <- SymBV sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
SymBV sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
addToPointer SymBV sym wptr
sz FilePointer sym wptr
basePtr
  FileHandle sym wptr
-> FilePointer sym wptr -> FileM p arch r args ret sym wptr ()
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FilePointer sym wptr -> FileM p arch r args ret sym wptr ()
setHandle FileHandle sym wptr
fhandle FilePointer sym wptr
ptr
  FileHandle sym wptr -> FileM p arch r args ret sym wptr ()
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr -> FileM p arch r args ret sym wptr ()
updateFileSize FileHandle sym wptr
fhandle
  SymBV sym wptr
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return SymBV sym wptr
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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr -> FileM p arch r args ret sym wptr ()
updateFileSize FileHandle sym wptr
fhdl = do
  (FilePointer (File NatRepr wptr
_ SymInteger sym
fileid) SymBV sym wptr
off, SymExpr sym BaseBoolType
_) <- FileHandle sym wptr
-> FileM
     p
     arch
     r
     args
     ret
     sym
     wptr
     (FilePointer sym wptr, SymExpr sym BaseBoolType)
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FileHandle sym wptr
-> FileM
     p arch r args ret sym wptr (FilePointer sym wptr, Pred sym)
readHandle FileHandle sym wptr
fhdl
  CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray <- (FileSystem sym wptr
 -> CachedArray
      sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
fsFileSizes
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  SymBV sym wptr
oldsz <- IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> FileM_ p arch r args ret sym wptr (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym
-> Assignment (SymExpr sym) (EmptyCtx ::> BaseIntegerType)
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
-> IO (SymBV sym wptr)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Assignment (SymExpr sym) idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
CA.readSingle sym
sym (Assignment (SymExpr sym) EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment (SymExpr sym) EmptyCtx
-> SymInteger sym
-> Assignment (SymExpr sym) (EmptyCtx ::> BaseIntegerType)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> SymInteger sym
fileid) CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray
  CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray' <- IO
  (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
   (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
 -> FileM_
      p
      arch
      r
      args
      ret
      sym
      wptr
      (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)))
-> IO
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ sym
-> Assignment (SymExpr sym) (EmptyCtx ::> BaseIntegerType)
-> SymBV sym wptr
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
-> IO
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym tp
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
CA.writeSingle sym
sym (Assignment (SymExpr sym) EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment (SymExpr sym) EmptyCtx
-> SymInteger sym
-> Assignment (SymExpr sym) (EmptyCtx ::> BaseIntegerType)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> SymInteger sym
fileid) SymBV sym wptr
off CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray
  SymExpr sym BaseBoolType
outbounds <- IO (SymExpr sym BaseBoolType)
-> FileM_ p arch r args ret sym wptr (SymExpr sym BaseBoolType)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> FileM_ p arch r args ret sym wptr (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> FileM_ p arch r args ret sym wptr (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymBV sym wptr
-> SymBV sym wptr
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUlt sym
sym SymBV sym wptr
oldsz SymBV sym wptr
off
  CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray'' <- IO
  (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
   (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
 -> FileM_
      p
      arch
      r
      args
      ret
      sym
      wptr
      (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)))
-> IO
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
-> IO
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr))
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Pred sym
-> CachedArray sym idx tp
-> CachedArray sym idx tp
-> IO (CachedArray sym idx tp)
CA.muxArrays sym
sym SymExpr sym BaseBoolType
outbounds CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray' CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType wptr)
szArray
  (FileSystem sym wptr -> FileSystem sym wptr)
-> FileM_ p arch r args ret sym wptr ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
CMS.modify' ((FileSystem sym wptr -> FileSystem sym wptr)
 -> FileM_ p arch r args ret sym wptr ())
-> (FileSystem sym wptr -> FileSystem sym wptr)
-> FileM_ p arch r args ret sym wptr ()
forall a b. (a -> b) -> a -> b
$ \FileSystem sym wptr
arr -> FileSystem sym wptr
arr { fsFileSizes = szArray'' }

addToPointer ::
  W4.SymBV sym wptr ->
  FilePointer sym wptr ->
  FileM p arch r args ret sym wptr (FilePointer sym wptr)
addToPointer :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
SymBV sym wptr
-> FilePointer sym wptr
-> FileM p arch r args ret sym wptr (FilePointer sym wptr)
addToPointer SymBV sym wptr
i (FilePointer File sym wptr
n SymBV sym wptr
off) = do
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  SymBV sym wptr
off' <- IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> FileM_ p arch r args ret sym wptr (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> FileM_ p arch r args ret sym wptr (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym -> SymBV sym wptr -> SymBV sym wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAdd sym
sym SymBV sym wptr
off SymBV sym wptr
i
  FilePointer sym wptr
-> FileM_ p arch r args ret sym wptr (FilePointer sym wptr)
forall a. a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePointer sym wptr
 -> FileM_ p arch r args ret sym wptr (FilePointer sym wptr))
-> FilePointer sym wptr
-> FileM_ p arch r args ret sym wptr (FilePointer sym wptr)
forall a b. (a -> b) -> a -> b
$ File sym wptr -> SymBV sym wptr -> FilePointer sym wptr
forall sym (w :: Natural).
File sym w -> SymBV sym w -> FilePointer sym w
FilePointer File sym wptr
n SymBV sym wptr
off'


writeBytePointer ::
  FilePointer sym wptr ->
  W4.SymBV sym 8 ->
  FileM p arch r args ret sym wptr ()
writeBytePointer :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> SymBV sym 8 -> FileM p arch r args ret sym wptr ()
writeBytePointer FilePointer sym wptr
fptr SymBV sym 8
bv = do
  let idx :: FileSystemIndex sym wptr
idx = FilePointer sym wptr -> FileSystemIndex sym wptr
forall sym (wptr :: Natural).
IsSymInterface sym =>
FilePointer sym wptr -> FileSystemIndex sym wptr
filePointerIdx FilePointer sym wptr
fptr
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr <- (FileSystem sym wptr
 -> CachedArray
      sym
      ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
      (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
fsSymData
  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr' <- IO
  (CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
   (CachedArray
      sym
      ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
      (BaseBVType 8))
 -> FileM_
      p
      arch
      r
      args
      ret
      sym
      wptr
      (CachedArray
         sym
         ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
         (BaseBVType 8)))
-> IO
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall a b. (a -> b) -> a -> b
$ sym
-> FileSystemIndex sym wptr
-> SymBV sym 8
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
-> IO
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym tp
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
CA.writeSingle sym
sym FileSystemIndex sym wptr
idx SymBV sym 8
bv CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr
  (FileSystem sym wptr -> FileSystem sym wptr)
-> FileM_ p arch r args ret sym wptr ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
CMS.modify' ((FileSystem sym wptr -> FileSystem sym wptr)
 -> FileM_ p arch r args ret sym wptr ())
-> (FileSystem sym wptr -> FileSystem sym wptr)
-> FileM_ p arch r args ret sym wptr ()
forall a b. (a -> b) -> a -> b
$ \FileSystem sym wptr
fs -> FileSystem sym wptr
fs { fsSymData = dataArr' }

readBytePointer ::
  FilePointer sym wptr ->
  FileM p arch r args ret sym wptr (W4.SymBV sym 8)
readBytePointer :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> FileM p arch r args ret sym wptr (SymBV sym 8)
readBytePointer FilePointer sym wptr
fptr = do
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  let idx :: FileSystemIndex sym wptr
idx = FilePointer sym wptr -> FileSystemIndex sym wptr
forall sym (wptr :: Natural).
IsSymInterface sym =>
FilePointer sym wptr -> FileSystemIndex sym wptr
filePointerIdx FilePointer sym wptr
fptr
  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr <- (FileSystem sym wptr
 -> CachedArray
      sym
      ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
      (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
fsSymData
  IO (SymBV sym 8) -> FileM_ p arch r args ret sym wptr (SymBV sym 8)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym 8)
 -> FileM_ p arch r args ret sym wptr (SymBV sym 8))
-> IO (SymBV sym 8)
-> FileM_ p arch r args ret sym wptr (SymBV sym 8)
forall a b. (a -> b) -> a -> b
$ sym
-> FileSystemIndex sym wptr
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
-> IO (SymBV sym 8)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Assignment (SymExpr sym) idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
CA.readSingle sym
sym FileSystemIndex sym wptr
idx CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr


writeChunkPointer ::
  FilePointer sym wptr ->
  DataChunk sym wptr ->
  W4.SymBV sym wptr ->
  FileM p arch r args ret sym wptr ()
writeChunkPointer :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> DataChunk sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr ()
writeChunkPointer FilePointer sym wptr
fptr DataChunk sym wptr
chunk SymBV sym wptr
sz = do
  let idx :: FileSystemIndex sym wptr
idx = FilePointer sym wptr -> FileSystemIndex sym wptr
forall sym (wptr :: Natural).
IsSymInterface sym =>
FilePointer sym wptr -> FileSystemIndex sym wptr
filePointerIdx FilePointer sym wptr
fptr
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr <- (FileSystem sym wptr
 -> CachedArray
      sym
      ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
      (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
fsSymData
  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr' <- IO
  (CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO
   (CachedArray
      sym
      ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
      (BaseBVType 8))
 -> FileM_
      p
      arch
      r
      args
      ret
      sym
      wptr
      (CachedArray
         sym
         ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
         (BaseBVType 8)))
-> IO
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall a b. (a -> b) -> a -> b
$ sym
-> FileSystemIndex sym wptr
-> SymExpr
     sym (CtxFirst ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType))
-> ArrayChunk
     sym
     (CtxFirst ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType))
     (BaseBVType 8)
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
-> IO
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(NonEmptyCtx ctx, IsSymExprBuilder sym) =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> ArrayChunk sym (CtxFirst ctx) tp
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
CA.writeChunk sym
sym FileSystemIndex sym wptr
idx SymBV sym wptr
SymExpr
  sym (CtxFirst ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType))
sz DataChunk sym wptr
ArrayChunk
  sym
  (CtxFirst ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType))
  (BaseBVType 8)
chunk CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr
  (FileSystem sym wptr -> FileSystem sym wptr)
-> FileM_ p arch r args ret sym wptr ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
CMS.modify' ((FileSystem sym wptr -> FileSystem sym wptr)
 -> FileM_ p arch r args ret sym wptr ())
-> (FileSystem sym wptr -> FileSystem sym wptr)
-> FileM_ p arch r args ret sym wptr ()
forall a b. (a -> b) -> a -> b
$ \FileSystem sym wptr
fs -> FileSystem sym wptr
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 :: forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
FilePointer sym wptr
-> SymBV sym wptr
-> FileM p arch r args ret sym wptr (DataChunk sym wptr)
readChunkPointer FilePointer sym wptr
fptr SymBV sym wptr
sz = do
  let idx :: FileSystemIndex sym wptr
idx = FilePointer sym wptr -> FileSystemIndex sym wptr
forall sym (wptr :: Natural).
IsSymInterface sym =>
FilePointer sym wptr -> FileSystemIndex sym wptr
filePointerIdx FilePointer sym wptr
fptr
  sym
sym <- FileM_ p arch r args ret sym wptr sym
forall p arch r (args :: Ctx CrucibleType) (ret :: CrucibleType)
       sym (wptr :: Natural).
FileM p arch r args ret sym wptr sym
getSym
  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr <- (FileSystem sym wptr
 -> CachedArray
      sym
      ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
      (BaseBVType 8))
-> FileM_
     p
     arch
     r
     args
     ret
     sym
     wptr
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
        (BaseBVType 8))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
CMS.gets FileSystem sym wptr
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
fsSymData
  IO (DataChunk sym wptr)
-> FileM_ p arch r args ret sym wptr (DataChunk sym wptr)
forall a. IO a -> FileM_ p arch r args ret sym wptr a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (DataChunk sym wptr)
 -> FileM_ p arch r args ret sym wptr (DataChunk sym wptr))
-> IO (DataChunk sym wptr)
-> FileM_ p arch r args ret sym wptr (DataChunk sym wptr)
forall a b. (a -> b) -> a -> b
$ sym
-> FileSystemIndex sym wptr
-> SymExpr
     sym (CtxFirst ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType))
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
     (BaseBVType 8)
-> IO
     (ArrayChunk
        sym
        (CtxFirst ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType))
        (BaseBVType 8))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(NonEmptyCtx ctx, IsSymExprBuilder sym) =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> CachedArray sym ctx tp
-> IO (ArrayChunk sym (CtxFirst ctx) tp)
CA.readChunk sym
sym FileSystemIndex sym wptr
idx SymBV sym wptr
SymExpr
  sym (CtxFirst ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType))
sz CachedArray
  sym
  ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
  (BaseBVType 8)
dataArr

filePointerIdx ::
  IsSymInterface sym =>
  FilePointer sym wptr ->
  FileSystemIndex sym wptr
filePointerIdx :: forall sym (wptr :: Natural).
IsSymInterface sym =>
FilePointer sym wptr -> FileSystemIndex sym wptr
filePointerIdx (FilePointer (File NatRepr wptr
_ SymInteger sym
n) SymBV sym wptr
off) = Assignment (SymExpr sym) EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment (SymExpr sym) EmptyCtx
-> SymBV sym wptr
-> Assignment (SymExpr sym) (EmptyCtx ::> BaseBVType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymBV sym wptr
off Assignment (SymExpr sym) (EmptyCtx ::> BaseBVType wptr)
-> SymInteger sym
-> Assignment
     (SymExpr sym) ((EmptyCtx ::> BaseBVType wptr) ::> BaseIntegerType)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymInteger sym
n