{-# 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
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
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
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. 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 -> ()
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
_ = forall c t. Solvable c t => c -> t
con Bool
True
  AssertionError
_ <~ :: AssertionError -> AssertionError -> SymBool
<~ AssertionError
_ = forall c t. Solvable c t => c -> t
con Bool
False
  AssertionError
_ >=~ :: AssertionError -> AssertionError -> SymBool
>=~ AssertionError
_ = forall c t. Solvable c t => c -> t
con Bool
True
  AssertionError
_ >~ :: AssertionError -> AssertionError -> SymBool
>~ AssertionError
_ = forall c t. Solvable c t => c -> t
con Bool
False
  AssertionError
_ symCompare :: AssertionError -> AssertionError -> UnionM Ordering
`symCompare` AssertionError
_ = 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
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
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
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. 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 -> ()
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 = forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ VerificationConditions
l forall a. Ord a => a -> a -> Bool
<= VerificationConditions
r
  VerificationConditions
l >~ :: VerificationConditions -> VerificationConditions -> SymBool
>~ VerificationConditions
r = forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ VerificationConditions
l forall a. Ord a => a -> a -> Bool
< VerificationConditions
r
  VerificationConditions
l <=~ :: VerificationConditions -> VerificationConditions -> SymBool
<=~ VerificationConditions
r = forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ VerificationConditions
l forall a. Ord a => a -> a -> Bool
>= VerificationConditions
r
  VerificationConditions
l <~ :: VerificationConditions -> VerificationConditions -> SymBool
<~ VerificationConditions
r = forall c t. Solvable c t => c -> t
con forall a b. (a -> b) -> a -> b
$ VerificationConditions
l forall a. Ord a => a -> a -> Bool
> VerificationConditions
r
  VerificationConditions
l symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering
`symCompare` VerificationConditions
r = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle forall a b. (a -> b) -> a -> b
$ VerificationConditions
l 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 = 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 = 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 = 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 = forall to from (erm :: * -> *).
(Mergeable to, TransformError from to, MonadError to erm,
 MonadUnion erm) =>
from -> SymBool -> erm ()
symAssertTransformableError VerificationConditions
AssumptionViolation