-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.SymIO.Types
-- Description      : Crucible type definitions related to VFS
-- Copyright        : (c) Galois, Inc 2020
-- License          : BSD3
-- Maintainer       : Daniel Matichuk <dmatichuk@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}
module Lang.Crucible.SymIO.Types
  ( symIOIntrinsicTypes
  , FilePointer(..)
  , FilePointerType
  , pattern FilePointerRepr
  , FileHandle
  , FileHandleType
  , pattern FileHandleRepr
  , FileIdent
  , FileIdentType
  , FileSystem(..)
  , muxFileSystem
  , FileSystemType
  , FileSystemIndex
  , pattern FileSystemRepr
  , File(..)
  , pattern FileRepr
  , FileType
  , muxFile
  , DataChunk
  , SizedDataChunk
  , SizedDataChunkType
  )
where

import           Data.Typeable
import           GHC.TypeNats

import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.Context
import           Data.Parameterized.Classes
import           Data.Parameterized.NatRepr

import           Lang.Crucible.Backend
import           Lang.Crucible.Simulator.RegValue
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.Intrinsics

import           What4.Interface
import qualified What4.CachedArray as CA

-- | The intrinsic types used in the symbolic filesystem
symIOIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
symIOIntrinsicTypes :: forall sym. IsSymInterface sym => IntrinsicTypes sym
symIOIntrinsicTypes = IntrinsicTypes sym -> IntrinsicTypes sym
forall a. a -> a
id
  (IntrinsicTypes sym -> IntrinsicTypes sym)
-> (IntrinsicTypes sym -> IntrinsicTypes sym)
-> IntrinsicTypes sym
-> IntrinsicTypes sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolRepr "VFS_filesystem"
-> IntrinsicMuxFn sym "VFS_filesystem"
-> IntrinsicTypes sym
-> IntrinsicTypes sym
forall {v} (k :: v -> *) (tp :: v) (a :: v -> *).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (SymbolRepr "VFS_filesystem"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol :: SymbolRepr "VFS_filesystem") IntrinsicMuxFn sym "VFS_filesystem"
forall sym (nm :: Symbol).
IntrinsicClass sym nm =>
IntrinsicMuxFn sym nm
IntrinsicMuxFn
  (IntrinsicTypes sym -> IntrinsicTypes sym)
-> (IntrinsicTypes sym -> IntrinsicTypes sym)
-> IntrinsicTypes sym
-> IntrinsicTypes sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolRepr "VFS_file"
-> IntrinsicMuxFn sym "VFS_file"
-> IntrinsicTypes sym
-> IntrinsicTypes sym
forall {v} (k :: v -> *) (tp :: v) (a :: v -> *).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (SymbolRepr "VFS_file"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol :: SymbolRepr "VFS_file") IntrinsicMuxFn sym "VFS_file"
forall sym (nm :: Symbol).
IntrinsicClass sym nm =>
IntrinsicMuxFn sym nm
IntrinsicMuxFn
  (IntrinsicTypes sym -> IntrinsicTypes sym)
-> (IntrinsicTypes sym -> IntrinsicTypes sym)
-> IntrinsicTypes sym
-> IntrinsicTypes sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolRepr "VFS_filepointer"
-> IntrinsicMuxFn sym "VFS_filepointer"
-> IntrinsicTypes sym
-> IntrinsicTypes sym
forall {v} (k :: v -> *) (tp :: v) (a :: v -> *).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (SymbolRepr "VFS_filepointer"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol :: SymbolRepr "VFS_filepointer") IntrinsicMuxFn sym "VFS_filepointer"
forall sym (nm :: Symbol).
IntrinsicClass sym nm =>
IntrinsicMuxFn sym nm
IntrinsicMuxFn
  (IntrinsicTypes sym -> IntrinsicTypes sym)
-> IntrinsicTypes sym -> IntrinsicTypes sym
forall a b. (a -> b) -> a -> b
$ IntrinsicTypes sym
forall {v} (k :: v -> *) (a :: v -> *). MapF k a
MapF.empty

-- | An identifier for a file, which must be resolved into a 'File' to access
-- the underlying filesystem.
--
-- This is a file path
type FileIdent sym = RegValue sym FileIdentType

-- | The crucible-level type of 'FileIdent'
type FileIdentType = StringType Char8

-- | The crucible-level type of 'FileSystem'
type FileSystemType w = IntrinsicType "VFS_filesystem" (EmptyCtx ::> BVType w)

-- | Defines the current state of a symbolic filesystem.
data FileSystem sym w =
  FileSystem
    {
      forall sym (w :: Natural). FileSystem sym w -> NatRepr w
fsPtrSize :: NatRepr w
    , forall sym (w :: Natural).
FileSystem sym w -> RegValue sym (StringMapType (FileType w))
fsFileNames :: RegValue sym (StringMapType (FileType w))
    -- ^ map from concrete file identifiers to files
    , forall sym (w :: Natural).
FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
fsFileSizes :: CA.CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
    -- ^ a symbolic map from files to their size
    , forall sym (w :: Natural).
FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
fsSymData :: CA.CachedArray sym (EmptyCtx ::> BaseBVType w ::> BaseIntegerType) (BaseBVType 8)
    -- ^ array representing symbolic file contents
    , forall sym (w :: Natural).
FileSystem sym w
-> forall a. ((IsSymInterface sym, 1 <= w) => a) -> a
fsConstraints :: forall a. ((IsSymInterface sym, 1 <= w) => a) -> a
    }

-- | A base index into the filesystem, consistent of a file identifier and an offset into that file.
type FileSystemIndex sym w = Assignment (SymExpr sym) (EmptyCtx ::> BaseBVType w ::> BaseIntegerType)

muxFileSystem ::
  IsSymInterface sym =>
  sym ->
  Pred sym ->
  FileSystem sym w ->
  FileSystem sym w ->
  IO (FileSystem sym w)
muxFileSystem :: forall sym (w :: Natural).
IsSymInterface sym =>
sym
-> Pred sym
-> FileSystem sym w
-> FileSystem sym w
-> IO (FileSystem sym w)
muxFileSystem sym
sym Pred sym
p FileSystem sym w
fsT FileSystem sym w
fsF = do
  CachedArray
  sym
  ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
  (BaseBVType 8)
symData <- sym
-> Pred sym
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
-> IO
     (CachedArray
        sym
        ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
        (BaseBVType 8))
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 Pred sym
p (FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
fsSymData FileSystem sym w
fsT) (FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray
     sym
     ((EmptyCtx ::> BaseBVType w) ::> BaseIntegerType)
     (BaseBVType 8)
fsSymData FileSystem sym w
fsF)
  Map Text (PartExpr (Pred sym) (File sym w))
symFiles <- sym
-> MuxFn (Pred sym) (File sym w)
-> MuxFn (Pred sym) (Map Text (PartExpr (Pred sym) (File sym w)))
forall sym e.
IsExprBuilder sym =>
sym
-> MuxFn (Pred sym) e
-> MuxFn (Pred sym) (Map Text (PartExpr (Pred sym) e))
muxStringMap sym
sym (sym -> MuxFn (Pred sym) (File sym w)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> Pred sym -> File sym w -> File sym w -> IO (File sym w)
muxFile sym
sym) Pred sym
p (FileSystem sym w -> RegValue sym (StringMapType (FileType w))
forall sym (w :: Natural).
FileSystem sym w -> RegValue sym (StringMapType (FileType w))
fsFileNames FileSystem sym w
fsT) (FileSystem sym w -> RegValue sym (StringMapType (FileType w))
forall sym (w :: Natural).
FileSystem sym w -> RegValue sym (StringMapType (FileType w))
fsFileNames FileSystem sym w
fsF)
  CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
symFileSizes <- sym
-> Pred sym
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
-> IO
     (CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w))
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 Pred sym
p (FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
fsFileSizes FileSystem sym w
fsT) (FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
forall sym (w :: Natural).
FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
fsFileSizes FileSystem sym w
fsF)
  FileSystem sym w -> IO (FileSystem sym w)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FileSystem sym w -> IO (FileSystem sym w))
-> FileSystem sym w -> IO (FileSystem sym w)
forall a b. (a -> b) -> a -> b
$ FileSystem sym w
fsT { fsSymData  = symData, fsFileNames = symFiles, fsFileSizes = symFileSizes }

instance (IsSymInterface sym) => IntrinsicClass sym "VFS_filesystem" where
  type Intrinsic sym "VFS_filesystem" (EmptyCtx ::> BVType w) = FileSystem sym w

  muxIntrinsic :: forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr "VFS_filesystem"
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym "VFS_filesystem" ctx
-> Intrinsic sym "VFS_filesystem" ctx
-> IO (Intrinsic sym "VFS_filesystem" ctx)
muxIntrinsic sym
sym IntrinsicTypes sym
_iTypes SymbolRepr "VFS_filesystem"
_nm (Assignment TypeRepr ctx
Empty :> (BVRepr NatRepr n
_w)) = sym
-> Pred sym
-> FileSystem sym n
-> FileSystem sym n
-> IO (FileSystem sym n)
forall sym (w :: Natural).
IsSymInterface sym =>
sym
-> Pred sym
-> FileSystem sym w
-> FileSystem sym w
-> IO (FileSystem sym w)
muxFileSystem sym
sym
  muxIntrinsic sym
_ IntrinsicTypes sym
_ SymbolRepr "VFS_filesystem"
nm Assignment TypeRepr ctx
ctx = \Pred sym
_ Intrinsic sym "VFS_filesystem" ctx
_ Intrinsic sym "VFS_filesystem" ctx
_ -> SymbolRepr "VFS_filesystem"
-> Assignment TypeRepr ctx
-> IO (Intrinsic sym "VFS_filesystem" ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType) b.
HasCallStack =>
SymbolRepr nm -> CtxRepr ctx -> b
typeError SymbolRepr "VFS_filesystem"
nm Assignment TypeRepr ctx
ctx

pattern FileSystemRepr :: () => (1 <= w, ty ~ FileSystemType w) => NatRepr w -> TypeRepr ty
pattern $mFileSystemRepr :: forall {r} {ty :: CrucibleType}.
TypeRepr ty
-> (forall {w :: Natural}.
    (1 <= w, ty ~ FileSystemType w) =>
    NatRepr w -> r)
-> ((# #) -> r)
-> r
$bFileSystemRepr :: forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FileSystemType w) =>
NatRepr w -> TypeRepr ty
FileSystemRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_filesystem") -> Just Refl)
                                           (Empty :> BVRepr w)
  where
    FileSystemRepr NatRepr w
w = SymbolRepr "VFS_filesystem"
-> CtxRepr (EmptyCtx ::> BVType w) -> TypeRepr (FileSystemType w)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('IntrinsicType nm ctx)
IntrinsicRepr SymbolRepr "VFS_filesystem"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol (Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment TypeRepr EmptyCtx
-> TypeRepr (BVType w) -> CtxRepr (EmptyCtx ::> BVType w)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr w -> TypeRepr (BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w)

-- | The crucible type of file handles.
type FileHandleType w = ReferenceType (MaybeType (FilePointerType w))

-- |  A file handle is a mutable file pointer that increments every time it is read.
type FileHandle sym w = RegValue sym (FileHandleType w)

-- | A 'File' represents a file in the filesystem independent
-- of any open handles to it
--
-- The 'NatRepr' records the size of file pointers (in bits)
--
-- The 'SymInteger' is an index into the underlying array of arrays that represents file contents
data File sym w = File (NatRepr w) (SymInteger sym)

pattern FileRepr :: () => (1 <= w, ty ~ FileType w) => NatRepr w -> TypeRepr ty
pattern $mFileRepr :: forall {r} {ty :: CrucibleType}.
TypeRepr ty
-> (forall {w :: Natural}.
    (1 <= w, ty ~ FileType w) =>
    NatRepr w -> r)
-> ((# #) -> r)
-> r
$bFileRepr :: forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FileType w) =>
NatRepr w -> TypeRepr ty
FileRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_file") -> Just Refl)
                                           (Empty :> BVRepr w)
  where
    FileRepr NatRepr w
w = SymbolRepr "VFS_file"
-> CtxRepr (EmptyCtx ::> BVType w) -> TypeRepr (FileType w)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('IntrinsicType nm ctx)
IntrinsicRepr SymbolRepr "VFS_file"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol (Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment TypeRepr EmptyCtx
-> TypeRepr (BVType w) -> CtxRepr (EmptyCtx ::> BVType w)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr w -> TypeRepr (BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w)

-- | The crucible-level type of 'File'
type FileType w = IntrinsicType "VFS_file" (EmptyCtx ::> BVType w)

instance (IsSymInterface sym) => IntrinsicClass sym "VFS_file" where
  type Intrinsic sym "VFS_file" (EmptyCtx ::> BVType w) = File sym w

  muxIntrinsic :: forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr "VFS_file"
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym "VFS_file" ctx
-> Intrinsic sym "VFS_file" ctx
-> IO (Intrinsic sym "VFS_file" ctx)
muxIntrinsic sym
sym IntrinsicTypes sym
_iTypes SymbolRepr "VFS_file"
_nm (Assignment TypeRepr ctx
Empty :> BVRepr NatRepr n
_w) = sym -> Pred sym -> File sym n -> File sym n -> IO (File sym n)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> Pred sym -> File sym w -> File sym w -> IO (File sym w)
muxFile sym
sym
  muxIntrinsic sym
_ IntrinsicTypes sym
_ SymbolRepr "VFS_file"
nm Assignment TypeRepr ctx
ctx = SymbolRepr "VFS_file"
-> Assignment TypeRepr ctx
-> Pred sym
-> Intrinsic sym "VFS_file" ctx
-> Intrinsic sym "VFS_file" ctx
-> IO (Intrinsic sym "VFS_file" ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType) b.
HasCallStack =>
SymbolRepr nm -> CtxRepr ctx -> b
typeError SymbolRepr "VFS_file"
nm Assignment TypeRepr ctx
ctx

muxFile ::
  IsSymInterface sym =>
  sym ->
  Pred sym ->
  File sym w ->
  File sym w ->
  IO (File sym w)
muxFile :: forall sym (w :: Natural).
IsSymInterface sym =>
sym -> Pred sym -> File sym w -> File sym w -> IO (File sym w)
muxFile sym
sym Pred sym
p (File NatRepr w
w SymInteger sym
f1) (File NatRepr w
_w SymInteger sym
f2) = NatRepr w -> SymInteger sym -> File sym w
forall sym (w :: Natural).
NatRepr w -> SymInteger sym -> File sym w
File NatRepr w
w (SymInteger sym -> File sym w)
-> IO (SymInteger sym) -> IO (File sym w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
baseTypeIte sym
sym Pred sym
p SymInteger sym
f1 SymInteger sym
f2

-- | A file pointer represents an index into a particular file.
--
-- The 'File' is similar to an inode, and uniquely identifies a file (as an
-- index into the array of all files).  The 'SymBV' is the offset into the file
-- that the file pointer is currently at (i.e., where the next read or write
-- will be from).
data FilePointer sym w =
  FilePointer (File sym w) (SymBV sym w) 

-- | The crucible type of 'FilePointer'
type FilePointerType w = IntrinsicType "VFS_filepointer" (EmptyCtx ::> BVType w)

instance (IsSymInterface sym) => IntrinsicClass sym "VFS_filepointer" where
  type Intrinsic sym "VFS_filepointer" (EmptyCtx ::> BVType w) = FilePointer sym w

  muxIntrinsic :: forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr "VFS_filepointer"
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym "VFS_filepointer" ctx
-> Intrinsic sym "VFS_filepointer" ctx
-> IO (Intrinsic sym "VFS_filepointer" ctx)
muxIntrinsic sym
sym IntrinsicTypes sym
_iTypes SymbolRepr "VFS_filepointer"
_nm (Assignment TypeRepr ctx
Empty :> (BVRepr NatRepr n
_w)) = sym
-> Pred sym
-> FilePointer sym n
-> FilePointer sym n
-> IO (FilePointer sym n)
forall (w :: Natural) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> Pred sym
-> FilePointer sym w
-> FilePointer sym w
-> IO (FilePointer sym w)
muxFilePointer sym
sym
  muxIntrinsic sym
_ IntrinsicTypes sym
_ SymbolRepr "VFS_filepointer"
nm Assignment TypeRepr ctx
ctx = SymbolRepr "VFS_filepointer"
-> Assignment TypeRepr ctx
-> Pred sym
-> Intrinsic sym "VFS_filepointer" ctx
-> Intrinsic sym "VFS_filepointer" ctx
-> IO (Intrinsic sym "VFS_filepointer" ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType) b.
HasCallStack =>
SymbolRepr nm -> CtxRepr ctx -> b
typeError SymbolRepr "VFS_filepointer"
nm Assignment TypeRepr ctx
ctx

-- | Mux on 'FilePointer'
muxFilePointer ::
  (1 <= w) =>
  IsSymInterface sym =>
  sym ->
  Pred sym ->
  FilePointer sym w ->
  FilePointer sym w ->
  IO (FilePointer sym w)
muxFilePointer :: forall (w :: Natural) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> Pred sym
-> FilePointer sym w
-> FilePointer sym w
-> IO (FilePointer sym w)
muxFilePointer sym
sym Pred sym
p (FilePointer File sym w
f1 SymBV sym w
off1) (FilePointer File sym w
f2 SymBV sym w
off2) =
  do File sym w
b   <- sym -> Pred sym -> File sym w -> File sym w -> IO (File sym w)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> Pred sym -> File sym w -> File sym w -> IO (File sym w)
muxFile sym
sym Pred sym
p File sym w
f1 File sym w
f2
     SymBV sym w
off <- sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p SymBV sym w
off1 SymBV sym w
off2
     FilePointer sym w -> IO (FilePointer sym w)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePointer sym w -> IO (FilePointer sym w))
-> FilePointer sym w -> IO (FilePointer sym w)
forall a b. (a -> b) -> a -> b
$ File sym w -> SymBV sym w -> FilePointer sym w
forall sym (w :: Natural).
File sym w -> SymBV sym w -> FilePointer sym w
FilePointer File sym w
b SymBV sym w
off


type DataChunk sym w = CA.ArrayChunk sym (BaseBVType w) (BaseBVType 8)

type SizedDataChunkType w = SymbolicStructType (EmptyCtx ::> BaseArrayType (EmptyCtx ::> BaseBVType w) (BaseBVType 8) ::> BaseBVType w)
type SizedDataChunk sym w = SymStruct sym (EmptyCtx ::> BaseArrayType (EmptyCtx ::> BaseBVType w) (BaseBVType 8) ::> BaseBVType w)

-- | A file handle is a reference to an optional file pointer
--
-- If the file pointer is not present, the file handle is closed. Otherwise, the
-- file pointer is the current pointer into the file (i.e., that will be read
-- from or written to next).
--
-- Note that this is just the repr and the real file handle value is symbolic
-- and stored in a Crucible reference.
pattern FileHandleRepr :: () => (1 <= w, ty ~ FileHandleType w) => NatRepr w -> TypeRepr ty
pattern $mFileHandleRepr :: forall {r} {ty :: CrucibleType}.
TypeRepr ty
-> (forall {w :: Natural}.
    (1 <= w, ty ~ FileHandleType w) =>
    NatRepr w -> r)
-> ((# #) -> r)
-> r
$bFileHandleRepr :: forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FileHandleType w) =>
NatRepr w -> TypeRepr ty
FileHandleRepr w = ReferenceRepr (MaybeRepr (FilePointerRepr w))

pattern FilePointerRepr :: () => (1 <= w, ty ~ FilePointerType w) => NatRepr w -> TypeRepr ty
pattern $mFilePointerRepr :: forall {r} {ty :: CrucibleType}.
TypeRepr ty
-> (forall {w :: Natural}.
    (1 <= w, ty ~ FilePointerType w) =>
    NatRepr w -> r)
-> ((# #) -> r)
-> r
$bFilePointerRepr :: forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FilePointerType w) =>
NatRepr w -> TypeRepr ty
FilePointerRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_filepointer") -> Just Refl)
                                           (Empty :> BVRepr w)
  where
    FilePointerRepr NatRepr w
w = SymbolRepr "VFS_filepointer"
-> CtxRepr (EmptyCtx ::> BVType w) -> TypeRepr (FilePointerType w)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('IntrinsicType nm ctx)
IntrinsicRepr SymbolRepr "VFS_filepointer"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol (Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment TypeRepr EmptyCtx
-> TypeRepr (BVType w) -> CtxRepr (EmptyCtx ::> BVType w)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr w -> TypeRepr (BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w)