{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}

-- |
-- Module      :   Grisette.Core.Control.Exception
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Core.Control.Exception
  ( -- * Predefined exceptions
    AssertionError (..),
    VerificationConditions (..),
    symAssert,
    symAssume,
  )
where

import Control.DeepSeq
import Control.Exception
import Control.Monad.Except
import GHC.Generics
import Generics.Deriving
import Grisette.Core.Control.Monad.Union
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.Error
import Grisette.Core.Data.Class.Evaluate
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.Mergeable
import Grisette.Core.Data.Class.SOrd
import Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solvable
import Grisette.Core.Data.Class.ToCon
import Grisette.Core.Data.Class.ToSym
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.Lib.Base
-- >>> import Grisette.IR.SymPrim
-- >>> import Control.Monad.Trans.Except

-- | Assertion error.
data AssertionError = AssertionError
  deriving (Int -> AssertionError -> ShowS
[AssertionError] -> ShowS
AssertionError -> String
(Int -> AssertionError -> ShowS)
-> (AssertionError -> String)
-> ([AssertionError] -> ShowS)
-> Show AssertionError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AssertionError] -> ShowS
$cshowList :: [AssertionError] -> ShowS
show :: AssertionError -> String
$cshow :: AssertionError -> String
showsPrec :: Int -> AssertionError -> ShowS
$cshowsPrec :: Int -> AssertionError -> ShowS
Show, AssertionError -> AssertionError -> Bool
(AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool) -> Eq AssertionError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssertionError -> AssertionError -> Bool
$c/= :: AssertionError -> AssertionError -> Bool
== :: AssertionError -> AssertionError -> Bool
$c== :: AssertionError -> AssertionError -> Bool
Eq, Eq AssertionError
Eq AssertionError
-> (AssertionError -> AssertionError -> Ordering)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> AssertionError)
-> (AssertionError -> AssertionError -> AssertionError)
-> Ord AssertionError
AssertionError -> AssertionError -> Bool
AssertionError -> AssertionError -> Ordering
AssertionError -> AssertionError -> AssertionError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: AssertionError -> AssertionError -> AssertionError
$cmin :: AssertionError -> AssertionError -> AssertionError
max :: AssertionError -> AssertionError -> AssertionError
$cmax :: AssertionError -> AssertionError -> AssertionError
>= :: AssertionError -> AssertionError -> Bool
$c>= :: AssertionError -> AssertionError -> Bool
> :: AssertionError -> AssertionError -> Bool
$c> :: AssertionError -> AssertionError -> Bool
<= :: AssertionError -> AssertionError -> Bool
$c<= :: AssertionError -> AssertionError -> Bool
< :: AssertionError -> AssertionError -> Bool
$c< :: AssertionError -> AssertionError -> Bool
compare :: AssertionError -> AssertionError -> Ordering
$ccompare :: AssertionError -> AssertionError -> Ordering
Ord, (forall x. AssertionError -> Rep AssertionError x)
-> (forall x. Rep AssertionError x -> AssertionError)
-> Generic AssertionError
forall x. Rep AssertionError x -> AssertionError
forall x. AssertionError -> Rep AssertionError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AssertionError x -> AssertionError
$cfrom :: forall x. AssertionError -> Rep AssertionError x
Generic, AssertionError -> ()
(AssertionError -> ()) -> NFData AssertionError
forall a. (a -> ()) -> NFData a
rnf :: AssertionError -> ()
$crnf :: AssertionError -> ()
NFData)
  deriving (ToCon AssertionError, ToSym AssertionError) via (Default AssertionError)

deriving via (Default AssertionError) instance Mergeable AssertionError

deriving via (Default AssertionError) instance SimpleMergeable AssertionError

deriving via (Default AssertionError) instance SEq AssertionError

instance SOrd AssertionError where
  AssertionError
_ <=~ :: AssertionError -> AssertionError -> SymBool
<=~ AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  AssertionError
_ <~ :: AssertionError -> AssertionError -> SymBool
<~ AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  AssertionError
_ >=~ :: AssertionError -> AssertionError -> SymBool
>=~ AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  AssertionError
_ >~ :: AssertionError -> AssertionError -> SymBool
>~ AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  AssertionError
_ symCompare :: AssertionError -> AssertionError -> UnionM Ordering
`symCompare` AssertionError
_ = Ordering -> UnionM Ordering
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
EQ

deriving via (Default AssertionError) instance EvaluateSym AssertionError

deriving via (Default AssertionError) instance ExtractSymbolics AssertionError

-- | Verification conditions.
-- A crashed program path can terminate with either assertion violation errors or assumption violation errors.
data VerificationConditions
  = AssertionViolation
  | AssumptionViolation
  deriving (Int -> VerificationConditions -> ShowS
[VerificationConditions] -> ShowS
VerificationConditions -> String
(Int -> VerificationConditions -> ShowS)
-> (VerificationConditions -> String)
-> ([VerificationConditions] -> ShowS)
-> Show VerificationConditions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VerificationConditions] -> ShowS
$cshowList :: [VerificationConditions] -> ShowS
show :: VerificationConditions -> String
$cshow :: VerificationConditions -> String
showsPrec :: Int -> VerificationConditions -> ShowS
$cshowsPrec :: Int -> VerificationConditions -> ShowS
Show, VerificationConditions -> VerificationConditions -> Bool
(VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> Eq VerificationConditions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VerificationConditions -> VerificationConditions -> Bool
$c/= :: VerificationConditions -> VerificationConditions -> Bool
== :: VerificationConditions -> VerificationConditions -> Bool
$c== :: VerificationConditions -> VerificationConditions -> Bool
Eq, Eq VerificationConditions
Eq VerificationConditions
-> (VerificationConditions -> VerificationConditions -> Ordering)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions
    -> VerificationConditions -> VerificationConditions)
-> (VerificationConditions
    -> VerificationConditions -> VerificationConditions)
-> Ord VerificationConditions
VerificationConditions -> VerificationConditions -> Bool
VerificationConditions -> VerificationConditions -> Ordering
VerificationConditions
-> VerificationConditions -> VerificationConditions
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: VerificationConditions
-> VerificationConditions -> VerificationConditions
$cmin :: VerificationConditions
-> VerificationConditions -> VerificationConditions
max :: VerificationConditions
-> VerificationConditions -> VerificationConditions
$cmax :: VerificationConditions
-> VerificationConditions -> VerificationConditions
>= :: VerificationConditions -> VerificationConditions -> Bool
$c>= :: VerificationConditions -> VerificationConditions -> Bool
> :: VerificationConditions -> VerificationConditions -> Bool
$c> :: VerificationConditions -> VerificationConditions -> Bool
<= :: VerificationConditions -> VerificationConditions -> Bool
$c<= :: VerificationConditions -> VerificationConditions -> Bool
< :: VerificationConditions -> VerificationConditions -> Bool
$c< :: VerificationConditions -> VerificationConditions -> Bool
compare :: VerificationConditions -> VerificationConditions -> Ordering
$ccompare :: VerificationConditions -> VerificationConditions -> Ordering
Ord, (forall x. VerificationConditions -> Rep VerificationConditions x)
-> (forall x.
    Rep VerificationConditions x -> VerificationConditions)
-> Generic VerificationConditions
forall x. Rep VerificationConditions x -> VerificationConditions
forall x. VerificationConditions -> Rep VerificationConditions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep VerificationConditions x -> VerificationConditions
$cfrom :: forall x. VerificationConditions -> Rep VerificationConditions x
Generic, VerificationConditions -> ()
(VerificationConditions -> ()) -> NFData VerificationConditions
forall a. (a -> ()) -> NFData a
rnf :: VerificationConditions -> ()
$crnf :: VerificationConditions -> ()
NFData)
  deriving (ToCon VerificationConditions, ToSym VerificationConditions) via (Default VerificationConditions)

deriving via (Default VerificationConditions) instance Mergeable VerificationConditions

deriving via (Default VerificationConditions) instance SEq VerificationConditions

instance SOrd VerificationConditions where
  VerificationConditions
l >=~ :: VerificationConditions -> VerificationConditions -> SymBool
>=~ VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
<= VerificationConditions
r
  VerificationConditions
l >~ :: VerificationConditions -> VerificationConditions -> SymBool
>~ VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
< VerificationConditions
r
  VerificationConditions
l <=~ :: VerificationConditions -> VerificationConditions -> SymBool
<=~ VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
>= VerificationConditions
r
  VerificationConditions
l <~ :: VerificationConditions -> VerificationConditions -> SymBool
<~ VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
> VerificationConditions
r
  VerificationConditions
l symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering
`symCompare` VerificationConditions
r = Ordering -> UnionM Ordering
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (Ordering -> UnionM Ordering) -> Ordering -> UnionM Ordering
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` VerificationConditions
r

deriving via (Default VerificationConditions) instance EvaluateSym VerificationConditions

deriving via (Default VerificationConditions) instance ExtractSymbolics VerificationConditions

instance TransformError VerificationConditions VerificationConditions where
  transformError :: VerificationConditions -> VerificationConditions
transformError = VerificationConditions -> VerificationConditions
forall a. a -> a
id

instance TransformError AssertionError VerificationConditions where
  transformError :: AssertionError -> VerificationConditions
transformError AssertionError
_ = VerificationConditions
AssertionViolation

instance TransformError ArithException AssertionError where
  transformError :: ArithException -> AssertionError
transformError ArithException
_ = AssertionError
AssertionError

instance TransformError ArrayException AssertionError where
  transformError :: ArrayException -> AssertionError
transformError ArrayException
_ = AssertionError
AssertionError

instance TransformError AssertionError AssertionError where
  transformError :: AssertionError -> AssertionError
transformError = AssertionError -> AssertionError
forall a. a -> a
id

-- | Used within a monadic multi path computation to begin exception processing.
--
-- Checks the condition passed to the function.
-- The current execution path will be terminated with assertion error if the condition is false.
--
-- If the condition is symbolic, Grisette will split the execution into two paths based on the condition.
-- The symbolic execution will continue on the then-branch, where the condition is true.
-- For the else branch, where the condition is false, the execution will be terminated.
--
-- The resulting monadic environment should be compatible with the 'AssertionError'
-- error type. See 'TransformError' type class for details.
--
-- __/Examples/__:
--
-- Terminates the execution if the condition is false.
-- Note that we may lose the 'Mergeable' knowledge here if no possible execution
-- path is viable. This may affect the efficiency in theory, but in practice this
-- should not be a problem as all paths are terminated and no further evaluation
-- would be performed.
--
-- >>> symAssert (con False) :: ExceptT AssertionError UnionM ()
-- ExceptT {Left AssertionError}
-- >>> do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
-- ExceptT <Left AssertionError>
--
-- No effect if the condition is true:
--
-- >>> symAssert (con True) :: ExceptT AssertionError UnionM ()
-- ExceptT {Right ()}
-- >>> do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
-- ExceptT {Right 1}
--
-- Splitting the path and terminate one of them when the condition is symbolic.
--
-- >>> symAssert (ssym "a") :: ExceptT AssertionError UnionM ()
-- ExceptT {If (! a) (Left AssertionError) (Right ())}
-- >>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
-- ExceptT {If (! a) (Left AssertionError) (Right 1)}
--
-- 'AssertionError' is compatible with 'VerificationConditions':
--
-- >>> symAssert (ssym "a") :: ExceptT VerificationConditions UnionM ()
-- ExceptT {If (! a) (Left AssertionViolation) (Right ())}
symAssert ::
  (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) =>
  SymBool ->
  erm ()
symAssert :: forall to (erm :: * -> *).
(TransformError AssertionError to, Mergeable to, MonadError to erm,
 MonadUnion erm) =>
SymBool -> erm ()
symAssert = AssertionError -> SymBool -> erm ()
forall to from (erm :: * -> *).
(Mergeable to, TransformError from to, MonadError to erm,
 MonadUnion erm) =>
from -> SymBool -> erm ()
symAssertTransformableError AssertionError
AssertionError

-- | Used within a monadic multi path computation to begin exception processing.
--
-- Similar to 'symAssert', but terminates the execution path with 'AssumptionViolation' error.
--
-- /Examples/:
--
-- >>> symAssume (ssym "a") :: ExceptT VerificationConditions UnionM ()
-- ExceptT {If (! a) (Left AssumptionViolation) (Right ())}
symAssume ::
  (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) =>
  SymBool ->
  erm ()
symAssume :: forall to (erm :: * -> *).
(TransformError VerificationConditions to, Mergeable to,
 MonadError to erm, MonadUnion erm) =>
SymBool -> erm ()
symAssume = VerificationConditions -> SymBool -> erm ()
forall to from (erm :: * -> *).
(Mergeable to, TransformError from to, MonadError to erm,
 MonadUnion erm) =>
from -> SymBool -> erm ()
symAssertTransformableError VerificationConditions
AssumptionViolation