Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Langston Barrett <lbarrett@galois.com>
Stability	provisional
Safe Haskell	None
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 :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- AddNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- SubNoUnsignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- SubNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- MulNoUnsignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- MulNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- UDivExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- SDivExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ShlOp2Big :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ShlNoUnsignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ShlNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- LshrExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- LshrOp2Big :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- AshrExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- AshrOp2Big :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e
- ExtractElementIndex :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> Poison e
- InsertElementIndex :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> Poison e
- LLVMAbsIntMin :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> Poison e
- GEPOutOfBounds :: forall (w :: Natural) (wptr :: Natural) (e :: CrucibleType -> Type). (1 <= w, 1 <= wptr) => e (LLVMPointerType wptr) -> e (BVType w) -> Poison e
cite :: forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
explain :: forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
standard :: forall (e :: CrucibleType -> Type). Poison e -> Standard
details :: IsExpr (SymExpr sym) => Poison (RegValue' sym) -> [Doc ann]
pp :: forall (e :: CrucibleType -> Type) ann. (Poison e -> [Doc ann]) -> Poison e -> Doc ann
ppReg :: IsExpr (SymExpr sym) => Poison (RegValue' sym) -> Doc ann
concPoison :: IsExprBuilder sym => sym -> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> Poison (RegValue' sym) -> IO (Poison (RegValue' sym))

Documentation

data Poison (e :: CrucibleType -> Type) where Source #

Constructors

AddNoUnsignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
AddNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
SubNoUnsignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
SubNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
MulNoUnsignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
MulNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
UDivExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
SDivExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ShlOp2Big :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ShlNoUnsignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ShlNoSignedWrap :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
LshrExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
LshrOp2Big :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
AshrExact :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
AshrOp2Big :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> e (BVType w) -> Poison e	Arguments: `op1`, `op2`
ExtractElementIndex :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> Poison e	TODO(langston): store the `Vector`
InsertElementIndex :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> Poison e	TODO(langston): store the `Vector`
LLVMAbsIntMin :: forall (w :: Natural) (e :: CrucibleType -> Type). 1 <= w => e (BVType w) -> Poison e
GEPOutOfBounds :: forall (w :: Natural) (wptr :: Natural) (e :: CrucibleType -> Type). (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 :: CrucibleType) (y :: CrucibleType). 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 :: CrucibleType) (y :: CrucibleType). 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 :: CrucibleType). e s -> m) -> Poison e -> m # foldrF :: (forall (s :: CrucibleType). e s -> b -> b) -> b -> Poison e -> b # foldlF :: (forall (s :: CrucibleType). b -> e s -> b) -> b -> Poison e -> b # foldrF' :: (forall (s :: CrucibleType). e s -> b -> b) -> b -> Poison e -> b # foldlF' :: (forall (s :: CrucibleType). b -> e s -> b) -> b -> Poison e -> b # toListF :: (forall (tp :: CrucibleType). f tp -> a) -> Poison f -> [a] #
FunctorF Poison Source #
Instance details Defined in Lang.Crucible.LLVM.Errors.Poison Methods fmapF :: (forall (x :: CrucibleType). 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 :: CrucibleType). e s -> m (f s)) -> Poison e -> m (Poison f) #

cite :: forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann Source #

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

explain :: forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann Source #

standard :: forall (e :: CrucibleType -> Type). Poison e -> Standard Source #

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

pp :: forall (e :: CrucibleType -> Type) ann. (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 :: IsExprBuilder sym => sym -> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> Poison (RegValue' sym) -> IO (Poison (RegValue' sym)) Source #

Concretize a poison error message.