crucible-llvm-0.6: Support for translating and executing LLVM code in Crucible

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

Contents

Lenses

Description

Synopsis

data LLVMSafetyAssertion sym
data BadBehavior sym where
- BBUndefinedBehavior :: UndefinedBehavior (RegValue' sym) -> BadBehavior sym
- BBMemoryError :: MemoryError sym -> BadBehavior sym
undefinedBehavior :: UndefinedBehavior (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym
undefinedBehavior' :: UndefinedBehavior (RegValue' sym) -> Pred sym -> Text -> LLVMSafetyAssertion sym
poison :: Poison (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym
poison' :: Poison (RegValue' sym) -> Pred sym -> Text -> LLVMSafetyAssertion sym
memoryError :: 1 <= w => MemoryOp sym w -> MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym
detailBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
ppBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
concBadBehavior :: IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> BadBehavior sym -> IO (BadBehavior sym)
classifier :: Simple Lens (LLVMSafetyAssertion sym) (BadBehavior sym)
predicate :: Simple Lens (LLVMSafetyAssertion sym) (Pred sym)
extra :: Simple Lens (LLVMSafetyAssertion sym) (Maybe Text)

Documentation

data LLVMSafetyAssertion sym Source #

Instances

Instances details

Generic (LLVMSafetyAssertion sym) Source #
Instance details Defined in Lang.Crucible.LLVM.Errors Associated Types type Rep (LLVMSafetyAssertion sym) :: Type -> Type # Methods from :: LLVMSafetyAssertion sym -> Rep (LLVMSafetyAssertion sym) x # to :: Rep (LLVMSafetyAssertion sym) x -> LLVMSafetyAssertion sym #
type Rep (LLVMSafetyAssertion sym) Source #
Instance details Defined in Lang.Crucible.LLVM.Errors type Rep (LLVMSafetyAssertion sym) = D1 ('MetaData "LLVMSafetyAssertion" "Lang.Crucible.LLVM.Errors" "crucible-llvm-0.6-JJ7tfvbGrbFFTkl5eJBN3H" 'False) (C1 ('MetaCons "LLVMSafetyAssertion" 'PrefixI 'True) (S1 ('MetaSel ('Just "_classifier") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (BadBehavior sym)) :: (S1 ('MetaSel ('Just "_predicate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pred sym)) :: S1 ('MetaSel ('Just "_extra") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)))))

data BadBehavior sym where Source #

Combine the three types of bad behaviors

Constructors

BBUndefinedBehavior :: UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBMemoryError :: MemoryError sym -> BadBehavior sym

undefinedBehavior :: UndefinedBehavior (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym Source #

undefinedBehavior' :: UndefinedBehavior (RegValue' sym) -> Pred sym -> Text -> LLVMSafetyAssertion sym Source #

poison :: Poison (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym Source #

poison' :: Poison (RegValue' sym) -> Pred sym -> Text -> LLVMSafetyAssertion sym Source #

memoryError :: 1 <= w => MemoryOp sym w -> MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym Source #

detailBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann Source #

explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann Source #

ppBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann Source #

concBadBehavior :: IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> BadBehavior sym -> IO (BadBehavior sym) Source #

Lenses

classifier :: Simple Lens (LLVMSafetyAssertion sym) (BadBehavior sym) Source #

predicate :: Simple Lens (LLVMSafetyAssertion sym) (Pred sym) Source #

extra :: Simple Lens (LLVMSafetyAssertion sym) (Maybe Text) Source #