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

Lang.Crucible.LLVM.Errors.Poison

Description

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 #

Constructors

AddNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
AddNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
SubNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
SubNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
MulNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
MulNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
UDivExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
SDivExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ShlOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ShlNoUnsignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ShlNoSignedWrap :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
LshrExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
LshrOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
AshrExact :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
AshrOp2Big :: 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ExtractElementIndex :: 1 <= w => e (BVType w) -> Poison e	TODO(langston): store the `Vector`
InsertElementIndex :: 1 <= w => e (BVType w) -> Poison e	TODO(langston): store the `Vector`
LLVMAbsIntMin :: 1 <= w => e (BVType w) -> Poison e
GEPOutOfBounds :: (1 <= w, 1 <= wptr) => e (LLVMPointerType wptr) -> e (BVType w) -> Poison e

Instances

Instances details

OrdC Poison Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.Poison Methods compareC :: (forall (x :: k) (y :: k). f x -> g y -> OrderingF x y) -> Poison f -> Poison g -> Ordering #
TestEqualityC Poison Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.Poison Methods testEqualityC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> Poison f -> Poison f -> Bool #
FoldableF Poison Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.Poison Methods 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 #
Instance details Defined in Lang.Crucible.LLVM.Errors.Poison Methods fmapF :: (forall (x :: k). f x -> g x) -> Poison f -> Poison g #
TraversableF Poison Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.Poison Methods traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> Poison e -> m (Poison f) #

cite :: Poison e -> Doc ann Source #

Which section(s) of the document state that this is poison?

explain :: Poison e -> Doc ann Source #

standard :: Poison e -> Standard Source #

details :: forall sym ann. IsExpr (SymExpr sym) => Poison (RegValue' sym) -> [Doc ann] Source #

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.