Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Langston Barrett <lbarrett@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.LLVM.Errors.MemoryError

Description

See crucible-llvm-clitest-dataub for tests demonstrating some of these.

Synopsis

data MemoryError sym where
- MemoryError :: forall (w :: Natural) sym. 1 <= w => MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
type MemErrContext sym (w :: Nat) = MemoryOp sym w
explain :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
details :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
ppMemoryError :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
data MemoryOp sym (w :: Nat)
- = MemLoadOp StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
- | MemStoreOp StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
- | MemStoreBytesOp (Maybe String) (LLVMPtr sym w) (Maybe (SymBV sym w)) (Mem sym)
- | 1 <= wlen => MemCopyOp (Maybe String, LLVMPtr sym w) (Maybe String, LLVMPtr sym w) (SymBV sym wlen) (Mem sym)
- | MemLoadHandleOp (Maybe Type) (Maybe String) (LLVMPtr sym w) (Mem sym)
- | 1 <= wlen => MemInvalidateOp Text (Maybe String) (LLVMPtr sym w) (SymBV sym wlen) (Mem sym)
memOpMem :: forall sym (w :: Nat). MemoryOp sym w -> Mem sym
ppMemoryOp :: forall sym (w :: Nat) ann. IsExpr (SymExpr sym) => MemoryOp sym w -> Doc ann
data MemoryErrorReason
- = TypeMismatch StorageType StorageType
- | UnexpectedArgumentType Text [StorageType]
- | ApplyViewFail ValueView
- | Invalid StorageType
- | Invalidated Text
- | NoSatisfyingWrite StorageType
- | UnwritableRegion
- | UnreadableRegion
- | BadFunctionPointer FuncLookupError
- | OverlappingRegions
ppMemoryErrorReason :: MemoryErrorReason -> Doc ann
data FuncLookupError
- = SymbolicPointer
- | RawBitvector
- | NoOverride
- | Uncallable SomeTypeRep
ppFuncLookupError :: FuncLookupError -> Doc ann
concMemoryError :: IsExprBuilder sym => sym -> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> MemoryError sym -> IO (MemoryError sym)
concMemoryOp :: forall (w :: Natural) sym. (1 <= w, IsExprBuilder sym) => sym -> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> MemoryOp sym w -> IO (MemoryOp sym w)

Documentation

data MemoryError sym where Source #

Constructors

MemoryError :: forall (w :: Natural) sym. 1 <= w => MemoryOp sym w -> MemoryErrorReason -> MemoryError sym

type MemErrContext sym (w :: Nat) = MemoryOp sym w Source #

explain :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann Source #

details :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann Source #

ppMemoryError :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann Source #

data MemoryOp sym (w :: Nat) Source #

Constructors

MemLoadOp StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
MemStoreOp StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
MemStoreBytesOp (Maybe String) (LLVMPtr sym w) (Maybe (SymBV sym w)) (Mem sym)
1 <= wlen => MemCopyOp (Maybe String, LLVMPtr sym w) (Maybe String, LLVMPtr sym w) (SymBV sym wlen) (Mem sym)
MemLoadHandleOp (Maybe Type) (Maybe String) (LLVMPtr sym w) (Mem sym)
1 <= wlen => MemInvalidateOp Text (Maybe String) (LLVMPtr sym w) (SymBV sym wlen) (Mem sym)

memOpMem :: forall sym (w :: Nat). MemoryOp sym w -> Mem sym Source #

ppMemoryOp :: forall sym (w :: Nat) ann. IsExpr (SymExpr sym) => MemoryOp sym w -> Doc ann Source #

data MemoryErrorReason Source #

The kinds of type errors that arise while reading memory/constructing LLVM values

Constructors

TypeMismatch StorageType StorageType
UnexpectedArgumentType Text [StorageType]
ApplyViewFail ValueView
Invalid StorageType
Invalidated Text
NoSatisfyingWrite StorageType
UnwritableRegion
UnreadableRegion
BadFunctionPointer FuncLookupError
OverlappingRegions

Instances

Instances details

Eq MemoryErrorReason Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.MemoryError Methods (==) :: MemoryErrorReason -> MemoryErrorReason -> Bool # (/=) :: MemoryErrorReason -> MemoryErrorReason -> Bool #
Ord MemoryErrorReason Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.MemoryError Methods compare :: MemoryErrorReason -> MemoryErrorReason -> Ordering # (<) :: MemoryErrorReason -> MemoryErrorReason -> Bool # (<=) :: MemoryErrorReason -> MemoryErrorReason -> Bool # (>) :: MemoryErrorReason -> MemoryErrorReason -> Bool # (>=) :: MemoryErrorReason -> MemoryErrorReason -> Bool # max :: MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason # min :: MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason #

ppMemoryErrorReason :: MemoryErrorReason -> Doc ann Source #

data FuncLookupError Source #

Reasons that looking up a function handle associated with an LLVM pointer may fail

Constructors

SymbolicPointer
RawBitvector
NoOverride
Uncallable SomeTypeRep

Instances

Instances details

Eq FuncLookupError Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.MemoryError Methods (==) :: FuncLookupError -> FuncLookupError -> Bool # (/=) :: FuncLookupError -> FuncLookupError -> Bool #
Ord FuncLookupError Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.MemoryError Methods compare :: FuncLookupError -> FuncLookupError -> Ordering # (<) :: FuncLookupError -> FuncLookupError -> Bool # (<=) :: FuncLookupError -> FuncLookupError -> Bool # (>) :: FuncLookupError -> FuncLookupError -> Bool # (>=) :: FuncLookupError -> FuncLookupError -> Bool # max :: FuncLookupError -> FuncLookupError -> FuncLookupError # min :: FuncLookupError -> FuncLookupError -> FuncLookupError #

ppFuncLookupError :: FuncLookupError -> Doc ann Source #

concMemoryError :: IsExprBuilder sym => sym -> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> MemoryError sym -> IO (MemoryError sym) Source #

concMemoryOp :: forall (w :: Natural) sym. (1 <= w, IsExprBuilder sym) => sym -> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> MemoryOp sym w -> IO (MemoryOp sym w) Source #