content: -- |
  -- 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 sym conc (BBUndefinedBehavior ub) =
    BBUndefinedBehavior <$> UB.concUB sym conc ub
  concBadBehavior sym conc (BBMemoryError me) =
    BBMemoryError <$> ME.concMemoryError sym conc me
  
  -- -----------------------------------------------------------------------
  -- ** LLVMSafetyAssertion
  
  data LLVMSafetyAssertion sym =
    LLVMSafetyAssertion
      { _classifier :: BadBehavior sym -- ^ What could have gone wrong?
      , _predicate  :: Pred sym        -- ^ Is the value safe/defined?
      , _extra      :: Maybe Text      -- ^ Additional human-readable context
      }
    deriving (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' ub pred expl =
    LLVMSafetyAssertion (BBUndefinedBehavior ub) pred (Just expl)
  
  undefinedBehavior :: UB.UndefinedBehavior (RegValue' sym)
                    -> Pred sym
                    -> LLVMSafetyAssertion sym
  undefinedBehavior ub pred =
    LLVMSafetyAssertion (BBUndefinedBehavior ub) pred Nothing
  
  memoryError :: (1 <= w) => ME.MemoryOp sym w -> ME.MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym
  memoryError mop rsn pred =
    LLVMSafetyAssertion (BBMemoryError (ME.MemoryError mop rsn)) pred Nothing
  
  poison' :: Poison.Poison (RegValue' sym)
          -> Pred sym
          -> Text
          -> LLVMSafetyAssertion sym
  poison' poison_ pred expl =
    LLVMSafetyAssertion (BBUndefinedBehavior (UB.PoisonValueCreated poison_)) pred (Just expl)
  
  poison :: Poison.Poison (RegValue' sym)
         -> Pred sym
         -> LLVMSafetyAssertion sym
  poison poison_ pred =
    LLVMSafetyAssertion (BBUndefinedBehavior (UB.PoisonValueCreated poison_)) pred Nothing
  
  -- -----------------------------------------------------------------------
  -- ** Lenses
  
  classifier :: Simple Lens (LLVMSafetyAssertion sym) (BadBehavior sym)
  classifier = lens _classifier (\s v -> s { _classifier = v})
  
  predicate :: Simple Lens (LLVMSafetyAssertion sym) (Pred sym)
  predicate = lens _predicate (\s v -> s { _predicate = v})
  
  extra :: Simple Lens (LLVMSafetyAssertion sym) (Maybe Text)
  extra = lens _extra (\s v -> s { _extra = v})
  
  explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
  explainBB = \case
    BBUndefinedBehavior ub -> UB.explain ub
    BBMemoryError me       -> ME.explain me
  
  detailBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
  detailBB = \case
    BBUndefinedBehavior ub -> UB.ppDetails ub
    BBMemoryError me -> ME.details me
  
  ppBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
  ppBB = \case
    BBUndefinedBehavior ub -> UB.ppDetails ub
    BBMemoryError me -> ME.ppMemoryError me
  