crucible-symio 0.1.1 → 0.2.0.0
raw patch · 3 files changed
+10/−6 lines, 3 filesdep ~basedep ~cruciblenew-uploaderPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, crucible
API changes (from Hackage documentation)
- Lang.Crucible.SymIO: [FileTarget] :: FilePath -> FDTarget In
+ Lang.Crucible.SymIO: [FileTarget] :: FilePath -> FDTarget 'In
- Lang.Crucible.SymIO: [StderrTarget] :: FDTarget Out
+ Lang.Crucible.SymIO: [StderrTarget] :: FDTarget 'Out
- Lang.Crucible.SymIO: [StdinTarget] :: FDTarget In
+ Lang.Crucible.SymIO: [StdinTarget] :: FDTarget 'In
- Lang.Crucible.SymIO: [StdoutTarget] :: FDTarget Out
+ Lang.Crucible.SymIO: [StdoutTarget] :: FDTarget 'Out
- Lang.Crucible.SymIO: arrayToChunk :: forall sym idx tp. IsSymExprBuilder sym => sym -> SymArray sym (EmptyCtx ::> idx) tp -> IO (ArrayChunk sym idx tp)
+ Lang.Crucible.SymIO: arrayToChunk :: forall sym (idx :: BaseType) (tp :: BaseType). IsSymExprBuilder sym => sym -> SymArray sym ((EmptyCtx :: Ctx BaseType) ::> idx) tp -> IO (ArrayChunk sym idx tp)
- Lang.Crucible.SymIO: chunkToArray :: forall sym idx tp. IsSymExprBuilder sym => sym -> BaseTypeRepr idx -> ArrayChunk sym idx tp -> IO (SymArray sym (EmptyCtx ::> idx) tp)
+ Lang.Crucible.SymIO: chunkToArray :: forall sym (idx :: BaseType) (tp :: BaseType). IsSymExprBuilder sym => sym -> BaseTypeRepr idx -> ArrayChunk sym idx tp -> IO (SymArray sym ((EmptyCtx :: Ctx BaseType) ::> idx) tp)
- Lang.Crucible.SymIO: closeFileHandle :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> (forall args'. Maybe FileHandleError -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
+ Lang.Crucible.SymIO: 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
- Lang.Crucible.SymIO: closeFileHandle' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch r args ret ()
+ Lang.Crucible.SymIO: 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 ()
- Lang.Crucible.SymIO: data FilePointer sym w
+ Lang.Crucible.SymIO: data FilePointer sym (w :: Nat)
- Lang.Crucible.SymIO: fdTargetToText :: FDTarget k -> Text
+ Lang.Crucible.SymIO: fdTargetToText :: forall (k :: TargetDirection). FDTarget k -> Text
- Lang.Crucible.SymIO: initFS :: forall sym wptr. (1 <= wptr, IsSymInterface sym) => sym -> NatRepr wptr -> InitialFileSystemContents sym -> IO (FileSystem sym wptr)
+ Lang.Crucible.SymIO: initFS :: forall sym (wptr :: Natural). (1 <= wptr, IsSymInterface sym) => sym -> NatRepr wptr -> InitialFileSystemContents sym -> IO (FileSystem sym wptr)
- Lang.Crucible.SymIO: invalidFileHandle :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> OverrideSim p sym arch args r ret (FileHandle sym wptr)
+ Lang.Crucible.SymIO: 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)
- Lang.Crucible.SymIO: isHandleOpen :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch args r ret (Pred sym)
+ Lang.Crucible.SymIO: 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)
- Lang.Crucible.SymIO: mkArrayChunk :: forall sym idx tp. IsSymExprBuilder sym => sym -> (SymExpr sym idx -> IO (SymExpr sym tp)) -> IO (ArrayChunk sym idx tp)
+ Lang.Crucible.SymIO: mkArrayChunk :: forall sym (idx :: BaseType) (tp :: BaseType). IsSymExprBuilder sym => sym -> (SymExpr sym idx -> IO (SymExpr sym tp)) -> IO (ArrayChunk sym idx tp)
- Lang.Crucible.SymIO: openFile :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileIdent sym -> (forall args'. Either FileIdentError (FileHandle sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
+ Lang.Crucible.SymIO: 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
- Lang.Crucible.SymIO: openFile' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileIdent sym -> OverrideSim p sym arch r args ret (FileHandle sym wptr)
+ Lang.Crucible.SymIO: 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)
- Lang.Crucible.SymIO: pattern FileSystemRepr :: () => (1 <= w, ty ~ FileSystemType w) => NatRepr w -> TypeRepr ty
+ Lang.Crucible.SymIO: pattern FileSystemRepr :: forall ty (w :: Natural). () => (1 <= w, ty ~ FileSystemType w) => NatRepr w -> TypeRepr ty
- Lang.Crucible.SymIO: readByte :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> (forall args'. Either FileHandleError (PartExpr (Pred sym) (SymBV sym 8)) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
+ Lang.Crucible.SymIO: 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
- Lang.Crucible.SymIO: readByte' :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> OverrideSim p sym arch r args ret (PartExpr (Pred sym) (SymBV sym 8))
+ Lang.Crucible.SymIO: 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))
- Lang.Crucible.SymIO: readChunk :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym wptr -> (forall args'. Either FileHandleError (DataChunk sym wptr, SymBV sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
+ Lang.Crucible.SymIO: 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
- Lang.Crucible.SymIO: readChunk' :: (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)
+ Lang.Crucible.SymIO: 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)
- Lang.Crucible.SymIO: type DataChunk sym w = ArrayChunk sym (BaseBVType w) (BaseBVType 8)
+ Lang.Crucible.SymIO: type DataChunk sym (w :: Nat) = ArrayChunk sym BaseBVType w BaseBVType 8
- Lang.Crucible.SymIO: type FileHandle sym w = RegValue sym (FileHandleType w)
+ Lang.Crucible.SymIO: type FileHandle sym (w :: Nat) = RegValue sym FileHandleType w
- Lang.Crucible.SymIO: type FileHandleType w = ReferenceType (MaybeType (FilePointerType w))
+ Lang.Crucible.SymIO: type FileHandleType (w :: Nat) = ReferenceType MaybeType FilePointerType w
- Lang.Crucible.SymIO: type FilePointerType w = IntrinsicType "VFS_filepointer" (EmptyCtx ::> BVType w)
+ Lang.Crucible.SymIO: type FilePointerType (w :: Nat) = IntrinsicType "VFS_filepointer" EmptyCtx :: Ctx CrucibleType ::> BVType w
- Lang.Crucible.SymIO: type FileSystemType w = IntrinsicType "VFS_filesystem" (EmptyCtx ::> BVType w)
+ Lang.Crucible.SymIO: type FileSystemType (w :: Nat) = IntrinsicType "VFS_filesystem" EmptyCtx :: Ctx CrucibleType ::> BVType w
- Lang.Crucible.SymIO: writeByte :: forall p sym arch r args ret wptr a. (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym 8 -> (forall args'. Maybe FileHandleError -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
+ Lang.Crucible.SymIO: 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
- Lang.Crucible.SymIO: writeByte' :: forall p sym arch r args ret wptr. (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> SymBV sym 8 -> OverrideSim p sym arch r args ret ()
+ Lang.Crucible.SymIO: 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 ()
- Lang.Crucible.SymIO: writeChunk :: (IsSymInterface sym, 1 <= wptr) => GlobalVar (FileSystemType wptr) -> FileHandle sym wptr -> DataChunk sym wptr -> SymBV sym wptr -> (forall args'. Either FileHandleError (SymBV sym wptr) -> OverrideSim p sym arch r args' ret a) -> OverrideSim p sym arch r args ret a
+ Lang.Crucible.SymIO: 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
- Lang.Crucible.SymIO: writeChunk' :: (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)
+ Lang.Crucible.SymIO: 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)
Files
- CHANGELOG.md +4/−0
- crucible-symio.cabal +4/−4
- tests/TestMain.hs +2/−2
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Revision history for crucible-symio +## 0.2 -- 2025-11-09++* Add support for GHC 9.10.1 and drop support for 9.4.8.+ ## 0.1.1 -- 2024-08-30 * Add support for GHC 9.8
crucible-symio.cabal view
@@ -6,14 +6,14 @@ reading and writing symbolic data. An example use case would be to support verifying programs that e.g., use configuration files or accept input from files. name: crucible-symio-version: 0.1.1+version: 0.2.0.0 license: BSD-3-Clause license-file: LICENSE author: Daniel Matichuk maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com build-type: Simple category: Language-extra-source-files: CHANGELOG.md+extra-doc-files: CHANGELOG.md source-repository head type: git@@ -21,7 +21,7 @@ subdir: crucible-symio common shared- build-depends: base >=4.12 && <4.20,+ build-depends: base >=4.12 && <4.21, aeson, bv-sized, bytestring,@@ -63,7 +63,7 @@ main-is: TestMain.hs hs-source-dirs: tests, src ghc-options: -Wall -Wcompat- build-depends: base >=4.12 && <4.20,+ build-depends: base >=4.12 && <4.21, what4, crucible, crucible-symio,
tests/TestMain.hs view
@@ -21,7 +21,7 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} -module Main where+module Main (main) where import GHC.TypeNats import Control.Lens ( (^.) )@@ -158,7 +158,7 @@ showAbortedResult :: CS.AbortedResult c d -> String showAbortedResult ar = case ar of CS.AbortedExec reason _ -> show reason- CS.AbortedExit code -> show code+ CS.AbortedExit code _ -> show code CS.AbortedBranch _ _ res' res'' -> "BRANCH: " <> showAbortedResult res' <> "\n" <> showAbortedResult res'' data FSTest (wptr :: Nat) where