Copyright | (c) Galois Inc 2018 |
---|---|
License | BSD3 |
Maintainer | Langston Barrett <lbarrett@galois.com> |
Stability | provisional |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
This module is intended to be imported qualified.
Undefined values follow control flow, wereas the poison values follow data flow. See the module-level comment in Lang.Crucible.LLVM.Translation.
This email provides an explanation and motivation for poison and undef
values: https://lists.llvm.org/pipermail/llvm-dev/2016-October/106182.html
Synopsis
- data Poison (e :: CrucibleType -> Type) where
- AddNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- AddNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- SubNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- SubNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- MulNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- MulNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- UDivExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- SDivExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ShlOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ShlNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ShlNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- LshrExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- LshrOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- AshrExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- AshrOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ExtractElementIndex :: 1 <= w => e (BVType w) -> Poison e
- InsertElementIndex :: 1 <= w => e (BVType w) -> Poison e
- LLVMAbsIntMin :: 1 <= w => e (BVType w) -> Poison e
- GEPOutOfBounds :: (1 <= w, 1 <= wptr) => e (LLVMPointerType wptr) -> e (BVType w) -> Poison e
- cite :: Poison e -> Doc ann
- explain :: Poison e -> Doc ann
- standard :: Poison e -> Standard
- details :: forall sym ann. IsExpr (SymExpr sym) => Poison (RegValue' sym) -> [Doc ann]
- pp :: (Poison e -> [Doc ann]) -> Poison e -> Doc ann
- ppReg :: IsExpr (SymExpr sym) => Poison (RegValue' sym) -> Doc ann
- concPoison :: forall sym. IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> Poison (RegValue' sym) -> IO (Poison (RegValue' sym))
Documentation
data Poison (e :: CrucibleType -> Type) where Source #
AddNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
AddNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
SubNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
SubNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
MulNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
MulNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
UDivExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
SDivExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
ShlOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
ShlNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
ShlNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
LshrExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
LshrOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
AshrExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
AshrOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e | Arguments: |
ExtractElementIndex :: 1 <= w => e (BVType w) -> Poison e | TODO(langston): store the |
InsertElementIndex :: 1 <= w => e (BVType w) -> Poison e | TODO(langston): store the |
LLVMAbsIntMin :: 1 <= w => e (BVType w) -> Poison e | |
GEPOutOfBounds :: (1 <= w, 1 <= wptr) => e (LLVMPointerType wptr) -> e (BVType w) -> Poison e |
Instances
OrdC Poison Source # | |
TestEqualityC Poison Source # | |
Defined in Lang.Crucible.LLVM.Errors.Poison | |
FoldableF Poison Source # | |
Defined in Lang.Crucible.LLVM.Errors.Poison foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> Poison e -> m # foldrF :: (forall (s :: k). e s -> b -> b) -> b -> Poison e -> b # foldlF :: (forall (s :: k). b -> e s -> b) -> b -> Poison e -> b # foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> Poison e -> b # foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> Poison e -> b # toListF :: (forall (tp :: k). f tp -> a) -> Poison f -> [a] # | |
FunctorF Poison Source # | |
Defined in Lang.Crucible.LLVM.Errors.Poison | |
TraversableF Poison Source # | |
Defined in Lang.Crucible.LLVM.Errors.Poison traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> Poison e -> m (Poison f) # |
pp :: (Poison e -> [Doc ann]) -> Poison e -> Doc ann Source #
Pretty print an error message relating to LLVM poison values, when given a printer to produce a detailed message.
ppReg :: IsExpr (SymExpr sym) => Poison (RegValue' sym) -> Doc ann Source #
Pretty print an error message relating to LLVM poison values
concPoison :: forall sym. IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> Poison (RegValue' sym) -> IO (Poison (RegValue' sym)) Source #
Concretize a poison error message.