-- |
-- Module           : Lang.Crucible.LLVM.Errors
-- Description      : Safety assertions for the LLVM syntax extension
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Langston Barrett <lbarrett@galois.com>
-- Stability        : provisional
--
--------------------------------------------------------------------------

{-# 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
    -- ** Lenses
  , 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

-- -----------------------------------------------------------------------
-- ** BadBehavior

-- | Combine the three types of bad behaviors
--
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

-- -----------------------------------------------------------------------
-- ** LLVMSafetyAssertion

data LLVMSafetyAssertion sym =
  LLVMSafetyAssertion
    { forall sym. LLVMSafetyAssertion sym -> BadBehavior sym
_classifier :: BadBehavior sym -- ^ What could have gone wrong?
    , forall sym. LLVMSafetyAssertion sym -> Pred sym
_predicate  :: Pred sym        -- ^ Is the value safe/defined?
    , forall sym. LLVMSafetyAssertion sym -> Maybe Text
_extra      :: Maybe Text      -- ^ Additional human-readable context
    }
  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)

-- -----------------------------------------------------------------------
-- ** Constructors

-- We expose these rather than the constructors to retain the freedom to
-- change the internal representation.

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

-- -----------------------------------------------------------------------
-- ** Lenses

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)
extra :: forall sym (f :: Type -> Type).
Functor f =>
(Maybe Text -> f (Maybe Text))
-> LLVMSafetyAssertion sym -> f (LLVMSafetyAssertion sym)
extra = (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