grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Control.Exception

Description

 
Synopsis

Predefined exceptions

data AssertionError Source #

Assertion error.

Constructors

AssertionError 

Instances

Instances details
Generic AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Associated Types

type Rep AssertionError :: Type -> Type #

Show AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

NFData AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Methods

rnf :: AssertionError -> () #

Eq AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Ord AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SEq AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

EvaluateSym AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ExtractSymbolics AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Mergeable AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SOrd AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SimpleMergeable AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

AllSyms AssertionError Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

TransformError ArithException AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

TransformError ArrayException AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

TransformError AssertionError AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

TransformError AssertionError VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToCon AssertionError AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToSym AssertionError AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

type Rep AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

type Rep AssertionError = D1 ('MetaData "AssertionError" "Grisette.Core.Control.Exception" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'False) (C1 ('MetaCons "AssertionError" 'PrefixI 'False) (U1 :: Type -> Type))

data VerificationConditions Source #

Verification conditions. A crashed program path can terminate with either assertion violation errors or assumption violation errors.

Instances

Instances details
Generic VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Associated Types

type Rep VerificationConditions :: Type -> Type #

Show VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

NFData VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Methods

rnf :: VerificationConditions -> () #

Eq VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Ord VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SEq VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

EvaluateSym VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ExtractSymbolics VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

Mergeable VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

SOrd VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

AllSyms VerificationConditions Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

TransformError AssertionError VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

TransformError VerificationConditions VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToCon VerificationConditions VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToSym VerificationConditions VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

type Rep VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

type Rep VerificationConditions = D1 ('MetaData "VerificationConditions" "Grisette.Core.Control.Exception" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'False) (C1 ('MetaCons "AssertionViolation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AssumptionViolation" 'PrefixI 'False) (U1 :: Type -> Type))

symAssert :: (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm () Source #

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 ())}

symAssume :: (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm () Source #

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 ())}