crucible-llvm-0.8.0.0: 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	None
Language	Haskell2010

Lang.Crucible.LLVM.Errors

Contents

Lenses

Description

Synopsis

data LLVMSafetyAssertion sym
data BadBehavior sym where
- BBUndefinedBehavior :: forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
- BBMemoryError :: forall sym. 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 :: forall (w :: Natural) sym. 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 :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> BadBehavior sym -> IO (BadBehavior sym)
classifier :: forall sym f. Functor f => (BadBehavior sym -> f (BadBehavior sym)) -> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym)
predicate :: forall sym f. Functor f => (Pred sym -> f (Pred sym)) -> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym)
extra :: forall sym f. Functor f => (Maybe Text -> f (Maybe Text)) -> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym)

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)

Instance details

Defined in Lang.Crucible.LLVM.Errors

type Rep (LLVMSafetyAssertion sym) = D1 ('MetaData "LLVMSafetyAssertion" "Lang.Crucible.LLVM.Errors" "crucible-llvm-0.8.0.0-3Ey4B49x4v26HVrIOnbh4e" '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)))))

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.8.0.0-3Ey4B49x4v26HVrIOnbh4e" '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 :: forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBMemoryError :: forall sym. 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 :: forall (w :: Natural) sym. 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 :: BaseType). SymExpr sym tp -> IO (GroundValue tp)) -> BadBehavior sym -> IO (BadBehavior sym) Source #

Lenses

classifier :: forall sym f. Functor f => (BadBehavior sym -> f (BadBehavior sym)) -> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym) Source #

predicate :: forall sym f. Functor f => (Pred sym -> f (Pred sym)) -> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym) Source #

extra :: forall sym f. Functor f => (Maybe Text -> f (Maybe Text)) -> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym) Source #