{-# 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
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
type FileIdent sym = RegValue sym FileIdentType
type FileIdentType = StringType Char8
type FileSystemType w = IntrinsicType "VFS_filesystem" (EmptyCtx ::> BVType w)
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))
, forall sym (w :: Natural).
FileSystem sym w
-> CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
fsFileSizes :: CA.CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
, 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)
, forall sym (w :: Natural).
FileSystem sym w
-> forall a. ((IsSymInterface sym, 1 <= w) => a) -> a
fsConstraints :: forall a. ((IsSymInterface sym, 1 <= w) => a) -> a
}
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)
type FileHandleType w = ReferenceType (MaybeType (FilePointerType w))
type FileHandle sym w = RegValue sym (FileHandleType w)
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)
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
data FilePointer sym w =
FilePointer (File sym w) (SymBV sym w)
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
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)
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)