{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.LLVM.Errors
( LLVMSafetyAssertion
, BadBehavior(..)
, undefinedBehavior
, undefinedBehavior'
, poison
, poison'
, memoryError
, detailBB
, explainBB
, ppBB
, concBadBehavior
, classifier
, predicate
, extra
) where
import Prelude hiding (pred)
import Control.Lens
import Data.Text (Text)
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Prettyprinter
import What4.Interface
import What4.Expr (GroundValue)
import Lang.Crucible.Simulator.RegValue (RegValue'(..))
import qualified Lang.Crucible.LLVM.Errors.MemoryError as ME
import qualified Lang.Crucible.LLVM.Errors.Poison as Poison
import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
data BadBehavior sym where
BBUndefinedBehavior :: UB.UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBMemoryError :: ME.MemoryError sym -> BadBehavior sym
deriving Typeable
concBadBehavior ::
IsExprBuilder sym =>
sym ->
(forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
BadBehavior sym -> IO (BadBehavior sym)
concBadBehavior :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> BadBehavior sym
-> IO (BadBehavior sym)
concBadBehavior sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub) =
UndefinedBehavior (RegValue' sym) -> BadBehavior sym
forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBUndefinedBehavior (UndefinedBehavior (RegValue' sym) -> BadBehavior sym)
-> IO (UndefinedBehavior (RegValue' sym)) -> IO (BadBehavior sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> UndefinedBehavior (RegValue' sym)
-> IO (UndefinedBehavior (RegValue' sym))
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> UndefinedBehavior (RegValue' sym)
-> IO (UndefinedBehavior (RegValue' sym))
UB.concUB sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc UndefinedBehavior (RegValue' sym)
ub
concBadBehavior sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (BBMemoryError MemoryError sym
me) =
MemoryError sym -> BadBehavior sym
forall sym. MemoryError sym -> BadBehavior sym
BBMemoryError (MemoryError sym -> BadBehavior sym)
-> IO (MemoryError sym) -> IO (BadBehavior sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemoryError sym
-> IO (MemoryError sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemoryError sym
-> IO (MemoryError sym)
ME.concMemoryError sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemoryError sym
me
data LLVMSafetyAssertion sym =
LLVMSafetyAssertion
{ forall sym. LLVMSafetyAssertion sym -> BadBehavior sym
_classifier :: BadBehavior sym
, forall sym. LLVMSafetyAssertion sym -> Pred sym
_predicate :: Pred sym
, :: Maybe Text
}
deriving ((forall x.
LLVMSafetyAssertion sym -> Rep (LLVMSafetyAssertion sym) x)
-> (forall x.
Rep (LLVMSafetyAssertion sym) x -> LLVMSafetyAssertion sym)
-> Generic (LLVMSafetyAssertion sym)
forall x.
Rep (LLVMSafetyAssertion sym) x -> LLVMSafetyAssertion sym
forall x.
LLVMSafetyAssertion sym -> Rep (LLVMSafetyAssertion sym) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall sym x.
Rep (LLVMSafetyAssertion sym) x -> LLVMSafetyAssertion sym
forall sym x.
LLVMSafetyAssertion sym -> Rep (LLVMSafetyAssertion sym) x
$cfrom :: forall sym x.
LLVMSafetyAssertion sym -> Rep (LLVMSafetyAssertion sym) x
from :: forall x.
LLVMSafetyAssertion sym -> Rep (LLVMSafetyAssertion sym) x
$cto :: forall sym x.
Rep (LLVMSafetyAssertion sym) x -> LLVMSafetyAssertion sym
to :: forall x.
Rep (LLVMSafetyAssertion sym) x -> LLVMSafetyAssertion sym
Generic, Typeable)
undefinedBehavior' :: UB.UndefinedBehavior (RegValue' sym)
-> Pred sym
-> Text
-> LLVMSafetyAssertion sym
undefinedBehavior' :: forall sym.
UndefinedBehavior (RegValue' sym)
-> Pred sym -> Text -> LLVMSafetyAssertion sym
undefinedBehavior' UndefinedBehavior (RegValue' sym)
ub Pred sym
pred Text
expl =
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
forall sym.
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
LLVMSafetyAssertion (UndefinedBehavior (RegValue' sym) -> BadBehavior sym
forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub) Pred sym
pred (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
expl)
undefinedBehavior :: UB.UndefinedBehavior (RegValue' sym)
-> Pred sym
-> LLVMSafetyAssertion sym
undefinedBehavior :: forall sym.
UndefinedBehavior (RegValue' sym)
-> Pred sym -> LLVMSafetyAssertion sym
undefinedBehavior UndefinedBehavior (RegValue' sym)
ub Pred sym
pred =
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
forall sym.
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
LLVMSafetyAssertion (UndefinedBehavior (RegValue' sym) -> BadBehavior sym
forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub) Pred sym
pred Maybe Text
forall a. Maybe a
Nothing
memoryError :: (1 <= w) => ME.MemoryOp sym w -> ME.MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym
memoryError :: forall (w :: Natural) sym.
(1 <= w) =>
MemoryOp sym w
-> MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym
memoryError MemoryOp sym w
mop MemoryErrorReason
rsn Pred sym
pred =
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
forall sym.
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
LLVMSafetyAssertion (MemoryError sym -> BadBehavior sym
forall sym. MemoryError sym -> BadBehavior sym
BBMemoryError (MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
forall (w :: Natural) sym.
(1 <= w) =>
MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
ME.MemoryError MemoryOp sym w
mop MemoryErrorReason
rsn)) Pred sym
pred Maybe Text
forall a. Maybe a
Nothing
poison' :: Poison.Poison (RegValue' sym)
-> Pred sym
-> Text
-> LLVMSafetyAssertion sym
poison' :: forall sym.
Poison (RegValue' sym)
-> Pred sym -> Text -> LLVMSafetyAssertion sym
poison' Poison (RegValue' sym)
poison_ Pred sym
pred Text
expl =
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
forall sym.
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
LLVMSafetyAssertion (UndefinedBehavior (RegValue' sym) -> BadBehavior sym
forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBUndefinedBehavior (Poison (RegValue' sym) -> UndefinedBehavior (RegValue' sym)
forall (e :: CrucibleType -> Type). Poison e -> UndefinedBehavior e
UB.PoisonValueCreated Poison (RegValue' sym)
poison_)) Pred sym
pred (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
expl)
poison :: Poison.Poison (RegValue' sym)
-> Pred sym
-> LLVMSafetyAssertion sym
poison :: forall sym.
Poison (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym
poison Poison (RegValue' sym)
poison_ Pred sym
pred =
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
forall sym.
BadBehavior sym
-> Pred sym -> Maybe Text -> LLVMSafetyAssertion sym
LLVMSafetyAssertion (UndefinedBehavior (RegValue' sym) -> BadBehavior sym
forall sym. UndefinedBehavior (RegValue' sym) -> BadBehavior sym
BBUndefinedBehavior (Poison (RegValue' sym) -> UndefinedBehavior (RegValue' sym)
forall (e :: CrucibleType -> Type). Poison e -> UndefinedBehavior e
UB.PoisonValueCreated Poison (RegValue' sym)
poison_)) Pred sym
pred Maybe Text
forall a. Maybe a
Nothing
classifier :: Simple Lens (LLVMSafetyAssertion sym) (BadBehavior sym)
classifier :: forall sym (f :: Type -> Type).
Functor f =>
(BadBehavior sym -> f (BadBehavior sym))
-> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym)
classifier = (LLVMSafetyAssertion sym -> BadBehavior sym)
-> (LLVMSafetyAssertion sym
-> BadBehavior sym -> LLVMSafetyAssertion sym)
-> Lens
(LLVMSafetyAssertion sym)
(LLVMSafetyAssertion sym)
(BadBehavior sym)
(BadBehavior sym)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMSafetyAssertion sym -> BadBehavior sym
forall sym. LLVMSafetyAssertion sym -> BadBehavior sym
_classifier (\LLVMSafetyAssertion sym
s BadBehavior sym
v -> LLVMSafetyAssertion sym
s { _classifier = v})
predicate :: Simple Lens (LLVMSafetyAssertion sym) (Pred sym)
predicate :: forall sym (f :: Type -> Type).
Functor f =>
(Pred sym -> f (Pred sym))
-> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym)
predicate = (LLVMSafetyAssertion sym -> SymExpr sym BaseBoolType)
-> (LLVMSafetyAssertion sym
-> SymExpr sym BaseBoolType -> LLVMSafetyAssertion sym)
-> Lens
(LLVMSafetyAssertion sym)
(LLVMSafetyAssertion sym)
(SymExpr sym BaseBoolType)
(SymExpr sym BaseBoolType)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMSafetyAssertion sym -> SymExpr sym BaseBoolType
forall sym. LLVMSafetyAssertion sym -> Pred sym
_predicate (\LLVMSafetyAssertion sym
s SymExpr sym BaseBoolType
v -> LLVMSafetyAssertion sym
s { _predicate = v})
extra :: Simple Lens (LLVMSafetyAssertion sym) (Maybe Text)
= (LLVMSafetyAssertion sym -> Maybe Text)
-> (LLVMSafetyAssertion sym
-> Maybe Text -> LLVMSafetyAssertion sym)
-> Lens
(LLVMSafetyAssertion sym)
(LLVMSafetyAssertion sym)
(Maybe Text)
(Maybe Text)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMSafetyAssertion sym -> Maybe Text
forall sym. LLVMSafetyAssertion sym -> Maybe Text
_extra (\LLVMSafetyAssertion sym
s Maybe Text
v -> LLVMSafetyAssertion sym
s { _extra = v})
explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
explainBB :: forall sym ann. IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
explainBB = \case
BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub -> UndefinedBehavior (RegValue' sym) -> Doc ann
forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
UB.explain UndefinedBehavior (RegValue' sym)
ub
BBMemoryError MemoryError sym
me -> MemoryError sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
ME.explain MemoryError sym
me
detailBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
detailBB :: forall sym ann. IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
detailBB = \case
BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub -> UndefinedBehavior (RegValue' sym) -> Doc ann
forall sym ann.
IsExpr (SymExpr sym) =>
UndefinedBehavior (RegValue' sym) -> Doc ann
UB.ppDetails UndefinedBehavior (RegValue' sym)
ub
BBMemoryError MemoryError sym
me -> MemoryError sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
ME.details MemoryError sym
me
ppBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
ppBB :: forall sym ann. IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
ppBB = \case
BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub -> UndefinedBehavior (RegValue' sym) -> Doc ann
forall sym ann.
IsExpr (SymExpr sym) =>
UndefinedBehavior (RegValue' sym) -> Doc ann
UB.ppDetails UndefinedBehavior (RegValue' sym)
ub
BBMemoryError MemoryError sym
me -> MemoryError sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
ME.ppMemoryError MemoryError sym
me