| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Grisette.Core
Description
Synopsis
- class IsString t => Solvable c t | t -> c where
- pattern Con :: Solvable c t => c -> t
- slocsym :: Solvable c s => String -> SpliceQ s
- ilocsym :: Solvable c s => String -> Int -> SpliceQ s
- class LogicalOp b where
- class ITEOp v where
- class SEq a where
- class (SimpleMergeable b, SEq b, Eq b, LogicalOp b, Solvable Bool b, ITEOp b) => SymBoolOp b
- class SEq a => SOrd a where
- class SomeBV bv where
- someBVConcat :: bv -> bv -> bv
- someBVZext :: forall p l. KnownNat l => p l -> bv -> bv
- someBVSext :: forall p l. KnownNat l => p l -> bv -> bv
- someBVExt :: forall p l. KnownNat l => p l -> bv -> bv
- someBVSelect :: forall p ix q w. (KnownNat ix, KnownNat w) => p ix -> q w -> bv -> bv
- someBVZext' :: forall l bv. SomeBV bv => NatRepr l -> bv -> bv
- someBVSext' :: forall l bv. SomeBV bv => NatRepr l -> bv -> bv
- someBVExt' :: forall l bv. SomeBV bv => NatRepr l -> bv -> bv
- someBVSelect' :: forall ix w bv. SomeBV bv => NatRepr ix -> NatRepr w -> bv -> bv
- someBVExtract :: forall p (i :: Nat) q (j :: Nat) bv. (SomeBV bv, KnownNat i, KnownNat j) => p i -> q j -> bv -> bv
- someBVExtract' :: forall (i :: Nat) (j :: Nat) bv. SomeBV bv => NatRepr i -> NatRepr j -> bv -> bv
- class SizedBV bv where
- sizedBVConcat :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => bv l -> bv r -> bv (l + r)
- sizedBVZext :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVSext :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVExt :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVSelect :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> bv n -> bv w
- sizedBVExtract :: forall proxy i j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i) => proxy i -> proxy j -> bv n -> bv ((i - j) + 1)
- class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where
- safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)
- safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)
- safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)
- safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)
- class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e where
- safeAdd :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeNeg :: (MonadError e uf, MonadUnion uf) => a -> uf a
- safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
- safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a
- safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
- class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a
- class Function f where
- data UnionM a
- class (Eq t, Ord t, Hashable t) => IsConcrete t
- makeUnionWrapper :: String -> Name -> Q [Dec]
- makeUnionWrapper' :: [String] -> Name -> Q [Dec]
- liftToMonadUnion :: (Mergeable a, MonadUnion u) => UnionM a -> u a
- unionSize :: UnionM a -> Int
- class Mergeable a where
- class Mergeable1 (u :: Type -> Type) where
- liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a)
- rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a)
- class Mergeable2 (u :: Type -> Type -> Type) where
- liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
- rootStrategy2 :: (Mergeable a, Mergeable b, Mergeable2 u) => MergingStrategy (u a b)
- class Mergeable3 (u :: Type -> Type -> Type -> Type) where
- liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (u a b c)
- rootStrategy3 :: (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) => MergingStrategy (u a b c)
- data MergingStrategy a where
- SimpleStrategy :: (SymBool -> a -> a -> a) -> MergingStrategy a
- SortedStrategy :: (Ord idx, Typeable idx, Show idx) => (a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
- NoStrategy :: MergingStrategy a
- derivedRootStrategy :: (Generic a, Mergeable' (Rep a)) => MergingStrategy a
- wrapStrategy :: MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
- product2Strategy :: (a -> b -> r) -> (r -> (a, b)) -> MergingStrategy a -> MergingStrategy b -> MergingStrategy r
- data DynamicSortedIdx where
- DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx
- data StrategyList container where
- StrategyList :: forall bool a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
- buildStrategyList :: forall bool a container. Functor container => MergingStrategy a -> container a -> StrategyList container
- resolveStrategy :: forall x. MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
- resolveStrategy' :: forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
- class Mergeable a => SimpleMergeable a where
- class SimpleMergeable1 u where
- liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a
- mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a
- class Mergeable2 u => SimpleMergeable2 u where
- liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b
- mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b
- class (SimpleMergeable1 u, Mergeable1 u) => UnionLike u where
- single :: a -> u a
- unionIf :: SymBool -> u a -> u a -> u a
- mergeWithStrategy :: MergingStrategy a -> u a -> u a
- mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a
- mrgSingleWithStrategy :: MergingStrategy a -> a -> u a
- mrgIf :: (UnionLike u, Mergeable a) => SymBool -> u a -> u a -> u a
- merge :: (UnionLike u, Mergeable a) => u a -> u a
- mrgSingle :: (UnionLike u, Mergeable a) => a -> u a
- class UnionLike u => UnionPrjOp (u :: Type -> Type) where
- pattern SingleU :: UnionPrjOp u => a -> u a
- pattern IfU :: UnionPrjOp u => SymBool -> u a -> u a -> u a
- type MonadUnion u = (UnionLike u, Monad u)
- class (UnionLike m, Monad m) => MonadParallelUnion m where
- parBindUnion :: (Mergeable b, NFData b) => m a -> (a -> m b) -> m b
- simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
- onUnion :: forall bool u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r
- onUnion2 :: forall bool u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r
- onUnion3 :: forall bool u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
- onUnion4 :: forall bool u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
- (#~) :: (Function f, SimpleMergeable (Ret f), UnionPrjOp u, Functor u) => f -> u (Arg f) -> Ret f
- class ToCon a b where
- class ToSym a b where
- toSym :: a -> b
- newtype FreshIndex = FreshIndex Int
- data FreshIdent where
- FreshIdent :: String -> FreshIdent
- FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
- name :: String -> FreshIdent
- nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
- data FileLocation = FileLocation {}
- nameWithLoc :: String -> SpliceQ FreshIdent
- class Monad m => MonadFresh m where
- nextFreshIndex :: m FreshIndex
- getFreshIdent :: m FreshIdent
- type Fresh = FreshT Identity
- data FreshT m a
- runFresh :: Fresh a -> FreshIdent -> a
- runFreshT :: Monad m => FreshT m a -> FreshIdent -> m a
- class Mergeable a => GenSym spec a where
- fresh :: MonadFresh m => spec -> m (UnionM a)
- class GenSymSimple spec a where
- simpleFresh :: MonadFresh m => spec -> m a
- genSym :: GenSym spec a => spec -> FreshIdent -> UnionM a
- genSymSimple :: forall spec a. GenSymSimple spec a => spec -> FreshIdent -> a
- derivedNoSpecFresh :: forall bool a m u. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a)
- derivedNoSpecSimpleFresh :: forall a m. (Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) => () -> m a
- derivedSameShapeSimpleFresh :: forall a m. (Generic a, GenSymSameShape (Rep a), MonadFresh m) => a -> m a
- chooseFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a)
- chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a
- chooseUnionFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a)
- choose :: forall bool a u. Mergeable a => [a] -> FreshIdent -> UnionM a
- chooseSimple :: forall a. SimpleMergeable a => [a] -> FreshIdent -> a
- chooseUnion :: forall a u. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a
- data EnumGenBound a = EnumGenBound a a
- newtype EnumGenUpperBound a = EnumGenUpperBound a
- data ListSpec spec = ListSpec {
- genListMinLength :: Int
- genListMaxLength :: Int
- genListSubSpec :: spec
- data SimpleListSpec spec = SimpleListSpec {
- genSimpleListLength :: Int
- genSimpleListSubSpec :: spec
- data AssertionError = AssertionError
- data VerificationConditions
- class TransformError from to where
- transformError :: from -> to
- symAssert :: (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm ()
- symAssume :: (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm ()
- symAssertWith :: (Mergeable e, MonadError e erm, MonadUnion erm) => e -> SymBool -> erm ()
- symAssertTransformableError :: (Mergeable to, TransformError from to, MonadError to erm, MonadUnion erm) => from -> SymBool -> erm ()
- symThrowTransformableError :: (Mergeable to, Mergeable a, TransformError from to, MonadError to erm, MonadUnion erm) => from -> erm a
- newtype CBMCEither a b = CBMCEither {
- runCBMCEither :: Either a b
- newtype CBMCExceptT e m a = CBMCExceptT {
- runCBMCExceptT :: m (CBMCEither e a)
- cbmcExcept :: Monad m => Either e a -> CBMCExceptT e m a
- mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b
- withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a
- class Solver config failure | config -> failure where
- class UnionWithExcept t u e v | t -> u e v where
- extractUnionExcept :: t -> u (Either e v)
- solveExcept :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure) => config -> (Either e v -> SymBool) -> t -> IO (Either failure Model)
- solveMultiExcept :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure) => config -> Int -> (Either e v -> SymBool) -> t -> IO ([Model], failure)
- class CEGISSolver config failure | config -> failure where
- cegisMultiInputs :: (EvaluateSym inputs, ExtractSymbolics inputs) => config -> [inputs] -> (inputs -> CEGISCondition) -> IO ([inputs], Either failure Model)
- data CEGISCondition = CEGISCondition SymBool SymBool
- cegisPostCond :: SymBool -> CEGISCondition
- cegisPrePost :: SymBool -> SymBool -> CEGISCondition
- cegis :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs) => config -> inputs -> CEGISCondition -> IO ([inputs], Either failure Model)
- cegisExcept :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> (Either e v -> CEGISCondition) -> t -> IO ([inputs], Either failure Model)
- cegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> t -> IO ([inputs], Either failure Model)
- cegisExceptVC :: (UnionWithExcept t u e v, UnionPrjOp u, Monad u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> t -> IO ([inputs], Either failure Model)
- cegisExceptMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u e v, UnionPrjOp u, Monad u) => config -> [inputs] -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], Either failure Model)
- cegisExceptStdVCMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u) => config -> [inputs] -> (inputs -> t) -> IO ([inputs], Either failure Model)
- cegisExceptVCMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u e v, UnionPrjOp u, Monad u) => config -> [inputs] -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], Either failure Model)
- class Monoid symbolSet => SymbolSetOps symbolSet (typedSymbol :: Type -> Type) | symbolSet -> typedSymbol where
- emptySet :: symbolSet
- isEmptySet :: symbolSet -> Bool
- containsSymbol :: forall a. typedSymbol a -> symbolSet -> Bool
- insertSymbol :: forall a. typedSymbol a -> symbolSet -> symbolSet
- intersectionSet :: symbolSet -> symbolSet -> symbolSet
- unionSet :: symbolSet -> symbolSet -> symbolSet
- differenceSet :: symbolSet -> symbolSet -> symbolSet
- class SymbolSetOps symbolSet typedSymbol => SymbolSetRep rep symbolSet (typedSymbol :: * -> *) where
- buildSymbolSet :: rep -> symbolSet
- class ExtractSymbolics a where
- extractSymbolics :: a -> SymbolSet
- class SymbolSetOps symbolSet typedSymbol => ModelOps model symbolSet typedSymbol | model -> symbolSet typedSymbol where
- emptyModel :: model
- isEmptyModel :: model -> Bool
- modelContains :: typedSymbol a -> model -> Bool
- valueOf :: typedSymbol t -> model -> Maybe t
- insertValue :: typedSymbol t -> t -> model -> model
- exceptFor :: symbolSet -> model -> model
- exceptFor' :: typedSymbol t -> model -> model
- restrictTo :: symbolSet -> model -> model
- extendTo :: symbolSet -> model -> model
- exact :: symbolSet -> model -> model
- class ModelRep rep model | rep -> model where
- buildModel :: rep -> model
- class EvaluateSym a where
- evaluateSym :: Bool -> Model -> a -> a
- evaluateSymToCon :: (ToCon a b, EvaluateSym a) => Model -> a -> b
- class SubstituteSym a where
- substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
- class SubstituteSym' a where
- substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> a c -> a c
- newtype Default a = Default {
- unDefault :: a
- newtype Default1 (f :: Type -> Type) a = Default1 {
- unDefault1 :: f a
- htmemo :: (Eq k, Hashable k) => (k -> a) -> k -> a
- htmemo2 :: (Eq k1, Hashable k1, Eq k2, Hashable k2) => (k1 -> k2 -> a) -> k1 -> k2 -> a
- htmemo3 :: (Eq k1, Hashable k1, Eq k2, Hashable k2, Eq k3, Hashable k3) => (k1 -> k2 -> k3 -> a) -> k1 -> k2 -> k3 -> a
- htmup :: (Eq k, Hashable k) => (b -> c) -> (k -> b) -> k -> c
- htmemoFix :: (Eq k, Hashable k) => ((k -> a) -> k -> a) -> k -> a
- mrgTrue :: Mergeable Bool => UnionM Bool
- mrgFalse :: Mergeable Bool => UnionM Bool
- mrgUnit :: Mergeable () => UnionM ()
- mrgTuple2 :: forall (a :: Type) (b :: Type). Mergeable (a, b) => a -> b -> UnionM (a, b)
- mrgTuple3 :: forall (a :: Type) (b :: Type) (c :: Type). Mergeable (a, b, c) => a -> b -> c -> UnionM (a, b, c)
- mrgJust :: forall (a :: Type). Mergeable (Maybe a) => a -> UnionM (Maybe a)
- mrgNothing :: forall (a :: Type). Mergeable (Maybe a) => UnionM (Maybe a)
- mrgLeft :: forall (a :: Type) (b :: Type). Mergeable (Either a b) => a -> UnionM (Either a b)
- mrgRight :: forall (a :: Type) (b :: Type). Mergeable (Either a b) => b -> UnionM (Either a b)
- mrgInL :: forall {k :: Type} (f :: k -> Type) (g :: k -> Type) (a :: k). Mergeable (Sum f g a) => f a -> UnionM (Sum f g a)
- mrgInR :: forall {k :: Type} (f :: k -> Type) (g :: k -> Type) (a :: k). Mergeable (Sum f g a) => g a -> UnionM (Sum f g a)
- mrgAssertionViolation :: Mergeable VerificationConditions => UnionM VerificationConditions
- mrgAssumptionViolation :: Mergeable VerificationConditions => UnionM VerificationConditions
Note for the examples
The examples may assume a z3 solver available in PATH.
Symbolic values
Grisette is a tool for performing symbolic evaluation on programs. Symbolic evaluation is a technique that allows us to analyze all possible runs of a program by representing inputs (or the program itself) as symbolic values and evaluating the program to produce symbolic constraints over these values. These constraints can then be used to find concrete assignments to the symbolic values that meet certain criteria, such as triggering a bug in a verification task or satisfying a specification in a synthesis task.
One of the challenges of symbolic evaluation is the well-known path explosion problem, which occurs when traditions symbolic evaluation techniques evaluate and reason about the possible paths one-by-one. This can lead to exponential growth in the number of paths that need to be analyzed, making the process impractical for many tasks. To address this issue, Grisette uses a technique called "path merging". In path merging, symbolic values are merged together in order to reduce the number of paths that need to be explored simultaneously. This can significantly improve the performance of symbolic evaluation, especially for tasks such as program synthesis that are prone to the path explosion problem.
In Grisette, we make a distinction between two kinds of symbolic values: solvable types and unsolvable types. These two types of values are merged differently.
Solvable types are types that are directly supported by the underlying solver and are represented as symbolic formulas. Examples include symbolic Booleans, integers and bit vectors. The values of solvable types can be fully merged into a single value, which can significantly reduce the number of paths that need to be explored.
For example, there are three symbolic Booleans a, b and c, in the
following code, and a symbolic Boolean x is defined to be the result of
a conditional expression:
x = if a then b else c -- pseudo code, not real Grisette code
The result would be a single symbolic Boolean formula:
-- result: x is (ite a b c)
If we further add 1 to x, we will not have to split to two paths,
but we can directly construct a formula with the merged state:
x + 1 -- result (+ 1 (ite a b c))
Unsolvable types, on the other hand, are types that are not directly supported by the solver and cannot be fully merged into a single formula. Examples include lists, algebraic data types, and concrete Haskell integer types. To symbolically evaluate values in unsolvable types, Grisette provides a symbolic union container, which is a set of values guarded by their path conditions. The values of unsolvable types are partially merged in a symbolic union, which is essentially an if-then-else tree.
For example, assume that the lists have the type
[.
In the following example, the result shows that SymBool][b] and [c] can be
merged together in the same symbolic union because they have the same
length:
x = if a then [b] else [c] -- pseudo code, not real Grisette code -- result: Single [(ite a b c)]
The second example shows that [b] and [c,d] cannot be merged
together because they have different lengths:
if a then [b] else [c, d] -- pseudo code, not real Grisette code -- result: If a (Single [b]) (Single [c,d])
The following example is more complicated. To make the merging efficient, Grisette would maintain a representation invariant of the symbolic unions. In this case, the lists with length 1 should be placed at the then branch, and the lists with length 2 should be placed at the else branch.
if a1 then [b] else if a2 then [c, d] else [f] -- pseudo code, not real Grisette code -- result: If (|| a1 (! a2)) (Single [(ite a1 b f)]) (Single [c,d])
When we further operate on this partially merged values,
we will need to split into multiple paths. For example, when we apply head
onto the last result, we will distribute head among the branches:
head (if a1 then [b] else if a2 then [c, d] else [f]) -- pseudo code, not real Grisette code -- intermediate result: If (|| a1 (! a2)) (Single (head [(ite a1 b f)])) (Single (head [c,d])) -- intermediate result: If (|| a1 (! a2)) (Single (ite a1 b f)) (Single c)
Then the result would be further merged into a single value:
-- final result: Single (ite (|| a1 (! a2)) (ite a1 b f) c)
Generally, merging the possible branches in a symbolic union can reduce
the number of paths to be explored in the future, but can make the path
conditions larger and harder to solve. To have a good balance between
this, Grisette has built a hierarchical merging algorithm, which is
configurable via MergingStrategy. For algebraic data types, we have
prebuilt merging strategies via the derivation of the Mergeable type
class. You only need to know the details of the merging algorithm if you
are going to work with non-algebraic data types.
Solvable types
A solvable type is a type that can be represented as a formula and is directly supported by the underlying constraint solvers. Grisette currently provides an implementation for the following solvable types:
SymBool(symbolic Booleans)SymInteger(symbolic unbounded integers)SymIntNnn)SymWordNnn)
The two bit vector types has their lengths checked at compile time.
Grisette also provides runtime-checked versions of these types:
SomeSymIntN and SomeSymWordN.
Values of a solvable type can consist of concrete values, symbolic
constants (placeholders for concrete values that can be assigned by a
solver to satisfy a formula), and complex symbolic formulas with
symbolic operations. The Solvable type class provides a way to
construct concrete values and symbolic constants.
Examples:
>>>import Grisette>>>con True :: SymBool -- a concrete valuetrue>>>ssym "a" :: SymBool -- a symbolic constanta
With the OverloadedStrings GHC extension enabled, symbolic constants
can also be constructed from strings.
>>>:set -XOverloadedStrings>>>"a" :: SymBoola
Symbolic operations are provided through a set of type classes,
such as SEq, SOrd, and Num. Please check out the documentation for
more details.
Examples:
>>>let a = "a" :: SymInteger>>>let b = "b" :: SymInteger>>>a ==~ b(= a b)
Creation of solvable type values
class IsString t => Solvable c t | t -> c where Source #
The class defines the creation and pattern matching of solvable type values.
Methods
Wrap a concrete value in a symbolic value.
>>>con True :: SymBooltrue
conView :: t -> Maybe c Source #
Extract the concrete value from a symbolic value.
>>>conView (con True :: SymBool)Just True
>>>conView (ssym "a" :: SymBool)Nothing
Generate simply-named symbolic constants.
Two symbolic constants with the same name are the same symbolic constant, and will always be assigned with the same value by the solver.
>>>ssym "a" :: SymBoola>>>(ssym "a" :: SymBool) == ssym "a"True>>>(ssym "a" :: SymBool) == ssym "b"False>>>(ssym "a" :: SymBool) &&~ ssym "a"a
isym :: String -> Int -> t Source #
Generate indexed symbolic constants.
Two symbolic constants with the same name but different indices are not the same symbolic constants.
>>>isym "a" 1 :: SymBoola@1
sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> t Source #
Generate simply-named symbolic constants with some extra information for disambiguation.
Two symbolic constants with the same name but different extra information (including info with different types) are considered to be different.
>>>sinfosym "a" "someInfo" :: SymIntegera:"someInfo"
iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> t Source #
Generate indexed symbolic constants with some extra information for disambiguation.
Two symbolic constants with the same name and index but different extra information (including info with different types) are considered to be different.
>>>iinfosym "a" 1 "someInfo" :: SymIntegera@1:"someInfo"
Instances
pattern Con :: Solvable c t => c -> t Source #
Extract the concrete value from a solvable value with conView.
>>>case con True :: SymBool of Con v -> vTrue
slocsym :: Solvable c s => String -> SpliceQ s Source #
Generate simply-named symbolic variables. The file location will be attached to the identifier.
>>>$$(slocsym "a") :: SymBoola:<interactive>:...
Calling slocsymb with the same name at different location will always
generate different symbolic constants. Calling slocsymb at the same
location for multiple times will generate the same symbolic constants.
>>>($$(slocsym "a") :: SymBool) == $$(slocsym "a")False>>>let f _ = $$(slocsym "a") :: SymBool>>>f () == f ()True
ilocsym :: Solvable c s => String -> Int -> SpliceQ s Source #
Generate indexed symbolic variables. The file location will be attached to identifier.
>>>$$(ilocsym "a" 1) :: SymBoola@1:<interactive>:...
Calling ilocsymb with the same name and index at different location will
always generate different symbolic constants. Calling slocsymb at the same
location for multiple times will generate the same symbolic constants.
Symbolic operators
class LogicalOp b where Source #
Symbolic logical operators for symbolic booleans.
>>>let t = con True :: SymBool>>>let f = con False :: SymBool>>>let a = "a" :: SymBool>>>let b = "b" :: SymBool>>>t ||~ ftrue>>>a ||~ ttrue>>>a ||~ fa>>>a ||~ b(|| a b)>>>t &&~ ffalse>>>a &&~ ta>>>a &&~ ffalse>>>a &&~ b(&& a b)>>>nots tfalse>>>nots ftrue>>>nots a(! a)>>>t `xors` ftrue>>>t `xors` tfalse>>>a `xors` t(! a)>>>a `xors` fa>>>a `xors` b(|| (&& (! a) b) (&& a (! b)))
Methods
(||~) :: b -> b -> b infixr 2 Source #
Symbolic disjunction
(&&~) :: b -> b -> b infixr 3 Source #
Symbolic conjunction
Symbolic negation
Symbolic exclusive disjunction
implies :: b -> b -> b Source #
Symbolic implication
ITE operator for solvable (see Grisette.Core)s, including symbolic boolean, integer, etc.
>>>let a = "a" :: SymBool>>>let b = "b" :: SymBool>>>let c = "c" :: SymBool>>>ites a b c(ite a b c)
Instances
| ITEOp SomeSymIntN Source # | |
Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN Source # | |
| ITEOp SomeSymWordN Source # | |
Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN Source # | |
| ITEOp SymBool Source # | |
| ITEOp SymInteger Source # | |
Defined in Grisette.Core.Data.Class.Bool Methods ites :: SymBool -> SymInteger -> SymInteger -> SymInteger Source # | |
| (ITEOp a, Mergeable a) => ITEOp (UnionM a) Source # | |
| (KnownNat n, 1 <= n) => ITEOp (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => ITEOp (SymWordN n) Source # | |
| (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa -~> sb) Source # | |
| (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa =~> sb) Source # | |
Symbolic equality. Note that we can't use Haskell's Eq class since
symbolic comparison won't necessarily return a concrete Bool value.
>>>let a = 1 :: SymInteger>>>let b = 2 :: SymInteger>>>a ==~ bfalse>>>a /=~ btrue
>>>let a = "a" :: SymInteger>>>let b = "b" :: SymInteger>>>a /=~ b(! (= a b))>>>a /=~ b(! (= a b))
Note: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving SEq via (Default X)
Instances
class (SimpleMergeable b, SEq b, Eq b, LogicalOp b, Solvable Bool b, ITEOp b) => SymBoolOp b Source #
Aggregation for the operations on symbolic boolean types
class SEq a => SOrd a where Source #
Symbolic total order. Note that we can't use Haskell's Ord class since
symbolic comparison won't necessarily return a concrete Bool or Ordering
value.
>>>let a = 1 :: SymInteger>>>let b = 2 :: SymInteger>>>a <~ btrue>>>a >~ bfalse
>>>let a = "a" :: SymInteger>>>let b = "b" :: SymInteger>>>a <~ b(< a b)>>>a <=~ b(<= a b)>>>a >~ b(< b a)>>>a >=~ b(<= b a)
For symCompare, Ordering is not a solvable type, and the result would
be wrapped in a union-like monad. See UnionMBase and UnionLike for more
information.
>>>a `symCompare` b :: UnionM Ordering -- UnionM is UnionMBase specialized with SymBool{If (< a b) LT (If (= a b) EQ GT)}
Note: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving SOrd via (Default X)
Minimal complete definition
Methods
(<~) :: a -> a -> SymBool infix 4 Source #
(<=~) :: a -> a -> SymBool infix 4 Source #
(>~) :: a -> a -> SymBool infix 4 Source #
(>=~) :: a -> a -> SymBool infix 4 Source #
symCompare :: a -> a -> UnionM Ordering Source #
Instances
class SomeBV bv where Source #
Bit vector operations. Including concatenation (someBVConcat),
extension (someBVZext, someBVSext, someBVExt), and selection
(someBVSelect).
Methods
someBVConcat :: bv -> bv -> bv Source #
Concatenation of two bit vectors.
>>>someBVConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))0b101010
Arguments
| :: forall p l. KnownNat l | |
| => p l | Desired output length |
| -> bv | Bit vector to extend |
| -> bv |
Zero extension of a bit vector.
>>>someBVZext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))0b000101
Arguments
| :: forall p l. KnownNat l | |
| => p l | Desired output length |
| -> bv | Bit vector to extend |
| -> bv |
Sign extension of a bit vector.
>>>someBVSext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))0b111101
Arguments
| :: forall p l. KnownNat l | |
| => p l | Desired output length |
| -> bv | Bit vector to extend |
| -> bv |
Extension of a bit vector. Signedness is determined by the input bit vector type.
>>>someBVExt (Proxy @6) (SomeSymIntN (0b101 :: SymIntN 3))0b111101>>>someBVExt (Proxy @6) (SomeSymIntN (0b001 :: SymIntN 3))0b000001>>>someBVExt (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))0b000101>>>someBVExt (Proxy @6) (SomeSymWordN (0b001 :: SymWordN 3))0b000001
Arguments
| :: forall p ix q w. (KnownNat ix, KnownNat w) | |
| => p ix | Index of the least significant bit of the slice |
| -> q w | Desired output width, |
| -> bv | Bit vector to select from |
| -> bv |
Slicing out a smaller bit vector from a larger one,
selecting a slice with width w starting from index ix.
The least significant bit is indexed as 0.
>>>someBVSelect (Proxy @1) (Proxy @3) (SomeSymIntN (0b001010 :: SymIntN 6))0b101
Instances
Zero extension of a bit vector.
>>>someBVZext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))0b000101
Sign extension of a bit vector.
>>>someBVSext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))0b111101
Extension of a bit vector. Signedness is determined by the input bit vector type.
>>>someBVExt' (natRepr @6) (SomeSymIntN (0b101 :: SymIntN 3))0b111101>>>someBVExt' (natRepr @6) (SomeSymIntN (0b001 :: SymIntN 3))0b000001>>>someBVExt' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))0b000101>>>someBVExt' (natRepr @6) (SomeSymWordN (0b001 :: SymWordN 3))0b000001
Arguments
| :: forall ix w bv. SomeBV bv | |
| => NatRepr ix | Index of the least significant bit of the slice |
| -> NatRepr w | Desired output width, |
| -> bv | Bit vector to select from |
| -> bv |
Slicing out a smaller bit vector from a larger one,
selecting a slice with width w starting from index ix.
The least significant bit is indexed as 0.
>>>someBVSelect' (natRepr @1) (natRepr @3) (SomeSymIntN (0b001010 :: SymIntN 6))0b101
Arguments
| :: forall p (i :: Nat) q (j :: Nat) bv. (SomeBV bv, KnownNat i, KnownNat j) | |
| => p i | The start position to extract from, |
| -> q j | The end position to extract from, |
| -> bv | Bit vector to extract from |
| -> bv |
Slicing out a smaller bit vector from a larger one, extract a slice from
bit i down to j.
The least significant bit is indexed as 0.
>>>someBVExtract (Proxy @4) (Proxy @2) (SomeSymIntN (0b010100 :: SymIntN 6))0b101
Arguments
| :: forall (i :: Nat) (j :: Nat) bv. SomeBV bv | |
| => NatRepr i | The start position to extract from, |
| -> NatRepr j | The end position to extract from, |
| -> bv | Bit vector to extract from |
| -> bv |
Slicing out a smaller bit vector from a larger one, extract a slice from
bit i down to j.
The least significant bit is indexed as 0.
>>>someBVExtract' (natRepr @4) (natRepr @2) (SomeSymIntN (0b010100 :: SymIntN 6))0b101
class SizedBV bv where Source #
Sized bit vector operations. Including concatenation (sizedBVConcat),
extension (sizedBVZext, sizedBVSext, sizedBVExt), and selection
(sizedBVSelect).
Methods
sizedBVConcat :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => bv l -> bv r -> bv (l + r) Source #
Concatenation of two bit vectors.
>>>sizedBVConcat (0b101 :: SymIntN 3) (0b010 :: SymIntN 3)0b101010
Arguments
| :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) | |
| => proxy r | Desired output width |
| -> bv l | Bit vector to extend |
| -> bv r |
Zero extension of a bit vector.
>>>sizedBVZext (Proxy @6) (0b101 :: SymIntN 3)0b000101
Arguments
| :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) | |
| => proxy r | Desired output width |
| -> bv l | Bit vector to extend |
| -> bv r |
Signed extension of a bit vector.
>>>sizedBVSext (Proxy @6) (0b101 :: SymIntN 3)0b111101
Arguments
| :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) | |
| => proxy r | Desired output width |
| -> bv l | Bit vector to extend |
| -> bv r |
Extension of a bit vector. Signedness is determined by the input bit vector type.
>>>sizedBVExt (Proxy @6) (0b101 :: SymIntN 3)0b111101>>>sizedBVExt (Proxy @6) (0b001 :: SymIntN 3)0b000001>>>sizedBVExt (Proxy @6) (0b101 :: SymWordN 3)0b000101>>>sizedBVExt (Proxy @6) (0b001 :: SymWordN 3)0b000001
Arguments
| :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) | |
| => proxy ix | Index of the least significant bit of the slice |
| -> proxy w | Desired output width, |
| -> bv n | Bit vector to select from |
| -> bv w |
Slicing out a smaller bit vector from a larger one, selecting a slice with
width w starting from index ix.
The least significant bit is indexed as 0.
>>>sizedBVSelect (Proxy @2) (Proxy @3) (con 0b010100 :: SymIntN 6)0b101
Instances
| SizedBV IntN Source # | |
Defined in Grisette.Core.Data.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> IntN n -> IntN w Source # | |
| SizedBV WordN Source # | |
Defined in Grisette.Core.Data.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> WordN n -> WordN w Source # | |
| SizedBV SymIntN Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymIntN l -> SymIntN r -> SymIntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> SymIntN n -> SymIntN w Source # | |
| SizedBV SymWordN Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymWordN l -> SymWordN r -> SymWordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> SymWordN n -> SymWordN w Source # | |
Arguments
| :: forall proxy i j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i) | |
| => proxy i | The start position to extract from, |
| -> proxy j | The end position to extract from, |
| -> bv n | Bit vector to extract from |
| -> bv ((i - j) + 1) |
Slicing out a smaller bit vector from a larger one, extract a slice from
bit i down to j.
The least significant bit is indexed as 0.
>>>sizedBVExtract (Proxy @4) (Proxy @2) (con 0b010100 :: SymIntN 6)0b101
class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where Source #
Safe division with monadic error handling in multi-path
execution. These procedures throw an exception when the
divisor is zero. The result should be able to handle errors with
MonadError.
Minimal complete definition
(safeDivMod | safeDiv, safeMod), (safeDivMod' | safeDiv', safeMod')
Methods
safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #
Safe signed div with monadic error handling in multi-path execution.
>>>safeDiv (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymIntegerExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}
safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #
Safe signed mod with monadic error handling in multi-path execution.
>>>safeMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymIntegerExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}
safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a) Source #
Safe signed divMod with monadic error handling in multi-path execution.
>>>safeDivMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymInteger, SymInteger)ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}
safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #
Safe signed quot with monadic error handling in multi-path execution.
safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #
Safe signed rem with monadic error handling in multi-path execution.
safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a) Source #
Safe signed quotRem with monadic error handling in multi-path execution.
safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #
Safe signed div with monadic error handling in multi-path execution.
The error is transformed.
>>>safeDiv' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymIntegerExceptT {If (= b 0) (Left ()) (Right (div a b))}
safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #
Safe signed mod with monadic error handling in multi-path execution.
The error is transformed.
>>>safeMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymIntegerExceptT {If (= b 0) (Left ()) (Right (mod a b))}
safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a) Source #
Safe signed divMod with monadic error handling in multi-path execution.
The error is transformed.
>>>safeDivMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM (SymInteger, SymInteger)ExceptT {If (= b 0) (Left ()) (Right ((div a b),(mod a b)))}
safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #
Safe signed quot with monadic error handling in multi-path execution.
The error is transformed.
safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #
Safe signed rem with monadic error handling in multi-path execution.
The error is transformed.
safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a) Source #
Safe signed quotRem with monadic error handling in multi-path execution.
The error is transformed.
Instances
class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e where Source #
Safe division with monadic error handling in multi-path
execution. These procedures throw an exception when overflow or underflow happens.
The result should be able to handle errors with MonadError.
Methods
safeAdd :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #
Safe + with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
>>>safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymIntegerExceptT {Right (+ a b)}>>>safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)ExceptT {If (ite (< 0x0 a) (&& (< 0x0 b) (< (+ a b) 0x0)) (&& (< a 0x0) (&& (< b 0x0) (<= 0x0 (+ a b))))) (If (< 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a b))}
safeNeg :: (MonadError e uf, MonadUnion uf) => a -> uf a Source #
Safe negate with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
>>>safeNeg (ssym "a") :: ExceptT ArithException UnionM SymIntegerExceptT {Right (- a)}>>>safeNeg (ssym "a") :: ExceptT ArithException UnionM (SymIntN 4)ExceptT {If (= a 0x8) (Left arithmetic overflow) (Right (- a))}
safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a Source #
Safe - with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
>>>safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymIntegerExceptT {Right (+ a (- b))}>>>safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)ExceptT {If (ite (<= 0x0 a) (&& (< b 0x0) (< (+ a (- b)) 0x0)) (&& (< a 0x0) (&& (< 0x0 b) (< 0x0 (+ a (- b)))))) (If (<= 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a (- b)))}
safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #
Safe + with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
The error is transformed.
safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a Source #
Safe negate with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
The error is transformed.
safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a Source #
Safe - with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
The error is transformed.
Instances
class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a Source #
Aggregation for the operations on symbolic integer types
Instances
class Function f where Source #
Abstraction for function-like types.
Methods
(#) :: f -> Arg f -> Ret f infixl 9 Source #
Function application operator.
The operator is not right associated (like ($)). It is left associated,
and you can provide many arguments with this operator once at a time.
>>>(+1) # 23
>>>(+) # 2 # 35
Instances
| (Function f, Mergeable f, Mergeable a, Ret f ~ a) => Function (UnionM f) Source # | |
| (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) Source # | |
| (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa -~> sb) Source # | |
| (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Function (sa =~> sb) Source # | |
| Eq a => Function (a =-> b) Source # | |
| Function (a -> b) Source # | |
Unsolvable types
There are types that cannot be directly represented as SMT formulas and therefore not supported by the SMT solvers. These types are referred to as unsolvable types. To symbolically evaluate such types, we represent them with symbolic unions. A symbolic union is a set of multiple values from different execution paths, each guarded with a corresponding path condition. The value of a union can be determined by an SMT solver based on the truth value of the path conditions.
In Grisette, the symbolic union type is UnionM.
Two constructs are useful in constructing symbolic union values: mrgIf
and mrgSingle.
mrgSingle unconditionally wraps a value in a symbolic union container,
while mrgIf models branching control flow semantics with symbolic
conditions.
Here are some examples of using mrgSingle and mrgIf:
>>>mrgSingle ["a"] :: UnionM [SymInteger]{[a]}>>>mrgIf "a" (mrgSingle ["b"]) (mrgSingle ["c", "d"]) :: UnionM [SymInteger]{If a [b] [c,d]}
UnionM is a monad, and its bind operation is similar to tree
substitution.
This means you can then use monadic constructs to model sequential programs.
For example, the following pseudo code can be
modeled in Grisette with the combinators provided by Grisette, and the do-notation:
x = if a then [b] else [b,c] -- pseudo code, not Grisette code y = if d then [e] else [e,f] return (x ++ y :: [SymInteger])
>>>:{ret :: UnionM [SymInteger] ret = do x <- mrgIf "a" (single ["b"]) (single ["b","c"]) y <- mrgIf "d" (single ["e"]) (single ["e","f"]) mrgReturn $ x ++ y -- we will explain mrgReturn later :}
When this code is evaluated, the result would be as follows:
>>>ret{If (&& a d) [b,e] (If (|| a d) [b,(ite a e c),(ite a f e)] [b,c,e,f])}
In the result, we can see that the results are reorganized and the two lists with the same length are merged together. This is important for scaling symbolic evaluation to real-world problems.
The mrgReturn function is crucial for ensuring that the results
are merged. It resolves the Mergeable constraint, and retrieves a
merging strategy for the contained type from the constraint.
The merging strategy is then cached in the UnionMBase container to
help merge the result of the entire do-block.
This is necessary due to
the constrained-monad problem,
as the return function from the Monad type class cannot resolve
extra constraints.
Our solution to this problem with merging strategy caching is inspired
by the knowledge propagation technique introduced in the
blog post by Oleg Kiselyov.
In addition to mrgReturn,
Grisette provides many combinators with the mrg prefix.
You should use these combinators and always have the result cache the merging strategy.
Consider the following code:
>>>return 1 :: UnionM Integer<1>>>>mrgReturn 1 :: UnionM Integer{1}>>>mrgIf "a" (return 1) (return 2) :: UnionM Integer{If a 1 2}
In the first example, using return instead of mrgReturn results in a
UAny container (printed as <...>), which means that no merging
strategy is cached.
In the second and third example, using mrgReturn or mrgIf results in
a UMrg container (printed as {...}),
which means that the merging strategy is cached.
When working with UnionM, it is important to always use the mrg prefixed
combinators to ensure that the merging strategy is properly cached.
This will enable Grisette to properly merge the results of the entire do-block
and scale symbolic evaluation to real-world problems.
Those functions that merges the results can also further propagate the
cached merging strategy, note that the result is merged:
>>>f x y = mrgIf "f" (return x) (return y)>>>do; a <- mrgIf "a" (return 1) (return 2); f a (a + 1) :: UnionM Integer{If (&& a f) 1 (If (|| a f) 2 3)}
For more details of this, see the documentation for UnionMBase and
MergingStrategy.
To make a type compatible with the symbolic evaluation and merging in
Grisette, you need to implement the Mergeable type class.
If you are only working with algebraic
data types, you can derive the Mergeable instance automatically
For example:
>>>:set -XDerivingStrategies>>>:set -XDerivingVia>>>:set -XDeriveGeneric>>>import GHC.Generics>>>:{data X = X SymInteger Integer deriving (Generic, Show) deriving (Mergeable) via (Default X) :}
This allows you to use the UnionM type to represent values of type X,
and have them merged with the mrgIf combinator:
>>>mrgIf "c1" (mrgSingle $ X "b" 1) (mrgIf "c2" (mrgSingle $ X "c" 2) (mrgSingle $ X "d" 1)) :: UnionM X{If (|| c1 (! c2)) (X (ite c1 b d) 1) (X c 2)}
It is also possible to apply monad transformers onto UnionM to extend
it with various mechanisms.
For example, by applying ExceptT,
you can symbolically evaluate a program with error handling.
To do this, you will need to define an error type and derive the Mergeable
instance for it. Then, you can use the combinators provided by MonadError
(and the mrg* variants of them) for error handling, and the mrgIf
combinator will also work with transformed UnionM containers.
Here's an example using the ExceptT transformer
to model error handling in Grisette:
>>>import Control.Monad.Except>>>:{data Error = Fail deriving (Show, Generic) deriving (Mergeable) via (Default Error) :}
>>>mrgIf "a" (throwError Fail) (return "x") :: ExceptT Error UnionM SymIntegerExceptT {If a (Left Fail) (Right x)}
This will return a symbolic union value representing a program that
throws an error in the then branch and returns a value in the else
branch.
The following is the details of the merging algorithm.
If you are not going to manually configure the system by writing a
MergingStrategy and will only use the derived strategies,
you can safely ignore the following contents in this section.
In Grisette, the symbolic union has the Ordered Guards (ORG) representation, which can be viewed as a nested if-then-else with some representation invariant.
For example, the following symbolic union represents a symbolic list of symbolic integers with length 1, 2 or 3. The values are kept sorted in the container: the list with length 1 is placed at the first place, the list with length 2 is placed at the second place, and so on.
\[ \left\{\begin{aligned} &\texttt{[a]}&&\mathrm{if}&&\texttt{c1}\\ &\texttt{[b,b]}&&\mathrm{else~if}&&\texttt{c2}\\& \texttt{[a,b,c]}&&\mathrm{otherwise} \end{aligned}\right. \]
In Haskell syntax, the container is represented as the following nested if-then-else tree
If c1 [a] (If c2 [b,b] [a,b,c])
The representations means that when c1 is true, then the value is a
list [a], or when c1 is false and c2 is true, the value is a list
[b,b], or otherwise the value is [a,b,c].
This representation allows you to use
the constructs that are not supported by the underlying solvers freely.
For example, when applying head on this structure, we can just
distribute the head function through the three branches, and get
\[ \left\{\begin{aligned} &\texttt{head [a]}&&\mathrm{if}&&\texttt{c1}\\ &\texttt{head [b,b]}&&\mathrm{else~if}&&\texttt{c2}\\ &\texttt{head [a,b,c]}&&\mathrm{otherwise} \end{aligned}\right. \]
or, equivalently
\[ \left\{\begin{aligned} &\texttt{a}&&\mathrm{if}&&\texttt{c1}\\ &\texttt{b}&&\mathrm{else~if}&&\texttt{c2}\\ &\texttt{a}&&\mathrm{otherwise} \end{aligned}\right. \]
Further symbolic evaluation will also distribute computations over the branches in this result, and the identical branches will cause redundant computation. To mitigate this, Grisette would try to merge the branches, and the previous result would become
\[ \left\{\begin{aligned} &\texttt{a}&&\mathrm{if}&&\texttt{c1}\vee\neg\texttt{c2}\\ &\texttt{b}&&\mathrm{otherwise}\\ \end{aligned}\right. \]
Note that if the contained type is symbolic Boolean, we may further merge the values into a single formula.
\[ \left\{\begin{aligned}&\texttt{(ite c1 a (ite c2 b a))}&&\mathrm{unconditional}\end{aligned}\right. \]
In Grisette, such merging happens in the mrgIf or unionIf functions,
which model the symbolic conditional branching semantics.
To keep the merging efficient and generate small constraints, we enforce
that the symbolic union maintains the values in a sorted way, and merge
the unions with a mergesort-style merging algorithm. In the following
example, the two ORG containers passed to the mrgIf are sorted
with the natural ordering on the integers. In the result, the values are
also organized in a sorted way, and the path conditions are correctly
maintained.
\[ \texttt{mrgIf}\left[ \texttt{c}, \left\{\begin{aligned} &\texttt{1}&&\mathrm{if}&&\texttt{c1}\\ &\texttt{3}&&\mathrm{else~if}&&\texttt{c2}\\ &\texttt{4}&&\mathrm{otherwise} \end{aligned}\right., \left\{\begin{aligned} &\texttt{1}&&\mathrm{if}&&\texttt{c3}\\ &\texttt{2}&&\mathrm{else~if}&&\texttt{c4}\\ &\texttt{4}&&\mathrm{otherwise} \end{aligned}\right. \right] =\left\{\begin{aligned} &\texttt{1}&&\mathrm{if}&&\texttt{(ite c c1 c3)}\\ &\texttt{2}&&\mathrm{else~if}&&\texttt{(&& (! c) c3)}\\ &\texttt{3}&&\mathrm{else~if}&&\texttt{(&& c c2)}\\ &\texttt{4}&&\mathrm{otherwise} \end{aligned}\right. \]
So far, we have described ORG as a flat list of values. When the list is long, it is beneficial to partition the values and merge (some or all) partitions into nested ORG values. This hierarchical ORG representation is particularly useful for complex data types, such as tuples, which tend to yield long lists.
In the following example, v* are values, while t* are ORG containers.
The values in the containers are first partitioned into three groups:
{v11, v12, v13}, {v2}, and {v13}.
In each group, the values share some common features, (e.g., they are
constructed with the same data constructor).
The values in each group are organized in a subtree, e.g., the first group
is organized in the subtree t1.
The hierarchical representation also keeps a representation invariant:
at each level in the hierarchy, the values (or the subtrees) are also sorted
by some criteria. Here, in the first level, the values are sorted by the
constructor declaration order, and in the second level, the values are sorted
by the concrete field in the constructor A.
This criteria is given by the MergingStrategy in the Mergeable class,
called the root merging strategy of the type.
data X = A Integer SymInteger | B | C
\[ \left\{\begin{aligned} &\texttt{t1}&&\mathrm{if}&&\texttt{c1}\\ &\texttt{B}&&\mathrm{else if}&&\texttt{c2}\\ &\texttt{C}&&\mathrm{otherwise}&& \end{aligned}\right. \hspace{2em}\mathrm{where}\hspace{2em} \texttt{t1} = \left\{\begin{aligned} &\texttt{A 1 a}&&\mathrm{if}&&\texttt{c11}\\ &\texttt{A 3 b}&&\mathrm{else if}&&\texttt{c12}\\ &\texttt{A 4 (&& x y)}&&\mathrm{otherwise}&& \end{aligned}\right. \]
In Haskell syntax, it can be represented as follows:
If c1 (If c11 (A 1 a) (If c12 (A 3 b) (A 4 (&& x y))))
(If c2 B
C)All the symbolic unions in Grisette should maintain the hierarchical
sorted invariant, and are sorted in the same way, with respect to the same
merging strategy (the root merging strategy for the type).
We can then merge the containers with a hierarchical
merging algorithm: at each level, we align the values and subtrees, and merge
the aligned ones. In the following example, mrgIf resolves the root merging
strategy s, and calls the function mrgIf', which accepts the merging strategy
as an argument. The symbolic union operands to the mrgIf' function must be
sorted with the merging strategy passed to the function.
Here we use the name of the subtrees and values to indicate the order of them:
t1should be placed beforev3in thethenbranch,t1andv4can be aligned witht1'andv4', respectively.
The aligned subtrees will be merged recursively with mrgIf', with a
sub-strategy given by the merging strategy s for the subtrees.
For example, t1 and t1' will be merged with the sub-strategy s'.
The aligned values will be merged with a merging function, also given by
the merging strategy s. For example, v4 and v4' will be merged with
the merging function f'.
The ordering and the sub-strategies are abstracted with SortedStrategy,
and the merging functions will be wrapped in SimpleStrategy.
The merging algorithm can then be configured by implementing the merging
strategies for the types contained in a symbolic union. See the documentation
for MergingStrategy for details.
\[ \begin{aligned} & \texttt{mrgIf}\left[ \texttt{c}, \left\{\begin{aligned} &\texttt{t1}&&\mathrm{if}&&\texttt{c1}\\ &\texttt{v3}&&\mathrm{else~if}&&\texttt{c2}\\ &\texttt{v4}&&\mathrm{otherwise} \end{aligned}\right., \left\{\begin{aligned} &\texttt{t1'}&&\mathrm{if}&&\texttt{c3}\\ &\texttt{t2'}&&\mathrm{else~if}&&\texttt{c4}\\ &\texttt{v4'}&&\mathrm{otherwise} \end{aligned}\right. \right]\\ =~ & \texttt{mrgIf'}\left[ \texttt{s}, \texttt{c}, \left\{\begin{aligned} &\texttt{t1}&&\mathrm{if}&&\texttt{c1}\\ &\texttt{v3}&&\mathrm{else~if}&&\texttt{c2}\\ &\texttt{v4}&&\mathrm{otherwise} \end{aligned}\right., \left\{\begin{aligned} &\texttt{t1'}&&\mathrm{if}&&\texttt{c3}\\ &\texttt{t2'}&&\mathrm{else~if}&&\texttt{c4}\\ &\texttt{v4'}&&\mathrm{otherwise} \end{aligned}\right. \right]\\ =~ & \left\{\begin{aligned} &\texttt{mrgIf' s' c t1 t1'}&&\mathrm{if}&&\texttt{(ite c c1 c3)}\\ &\texttt{t2'}&&\mathrm{else~if}&&\texttt{(&& (! c) c4)}\\ &\texttt{v3}&&\mathrm{else~if}&&\texttt{(&& c c2)}\\ &\texttt{f' c v4 v4'}&&\mathrm{otherwise} \end{aligned}\right. \end{aligned} \]
For more details of the algorithm, please refer to Grisette's paper.
UnionM Monad
UnionM is the Union container (hidden) enhanced with
MergingStrategy
knowledge propagation.
The Union models the underlying semantics evaluation semantics for
unsolvable types with the nested if-then-else tree semantics, and can be
viewed as the following structure:
data Union a = Single a | If bool (Union a) (Union a)
The Single constructor is for a single value with the path condition
true, and the If constructor is the if operator in an if-then-else
tree.
For clarity, when printing a UnionM value, we will omit the Single
constructor. The following two representations has the same semantics.
If c1 (If c11 v11 (If c12 v12 v13))
(If c2 v2
v3)\[ \left\{\begin{aligned}&t_1&&\mathrm{if}&&c_1\\&v_2&&\mathrm{else if}&&c_2\\&v_3&&\mathrm{otherwise}&&\end{aligned}\right.\hspace{2em}\mathrm{where}\hspace{2em}t_1 = \left\{\begin{aligned}&v_{11}&&\mathrm{if}&&c_{11}\\&v_{12}&&\mathrm{else if}&&c_{12}\\&v_{13}&&\mathrm{otherwise}&&\end{aligned}\right. \]
To reduce the size of the if-then-else tree to reduce the number of paths to
execute, Grisette would merge the branches in a Union container and
maintain a representation invariant for them. To perform this merging
procedure, Grisette relies on a type class called Mergeable and the
merging strategy defined by it.
Union is a monad, so we can easily write code with the do-notation and
monadic combinators. However, the standard monadic operators cannot
resolve any extra constraints, including the Mergeable constraint (see
The constrained-monad
problem
by Sculthorpe et al.).
This prevents the standard do-notations to merge the results automatically,
and would result in bad performance or very verbose code.
To reduce this boilerplate, Grisette provide another monad, UnionM that
would try to cache the merging strategy.
The UnionM has two data constructors (hidden intentionally), UAny and UMrg.
The UAny data constructor (printed as <...>) wraps an arbitrary (probably
unmerged) Union. It is constructed when no Mergeable knowledge is
available (for example, when constructed with Haskell's return).
The UMrg data constructor (printed as {...}) wraps a merged UnionM along with the
Mergeable constraint. This constraint can be propagated to the contexts
without Mergeable knowledge, and helps the system to merge the resulting
Union.
Examples:
return cannot resolve the Mergeable constraint.
>>>return 1 :: UnionM Integer<1>
mrgReturn can resolve the Mergeable constraint.
>>>import Grisette.Lib.Base>>>mrgReturn 1 :: UnionM Integer{1}
unionIf cannot resolve the Mergeable constraint.
>>>unionIf "a" (return 1) (unionIf "b" (return 1) (return 2)) :: UnionM Integer<If a 1 (If b 1 2)>
But unionIf is able to merge the result if some of the branches are merged:
>>>unionIf "a" (return 1) (unionIf "b" (mrgReturn 1) (return 2)) :: UnionM Integer{If (|| a b) 1 2}
The >>= operator uses unionIf internally. When the final statement in a do-block
merges the values, the system can then merge the final result.
>>>:{do x <- unionIf (ssym "a") (return 1) (unionIf (ssym "b") (return 1) (return 2)) mrgSingle $ x + 1 :: UnionM Integer :} {If (|| a b) 2 3}
Calling a function that merges a result at the last line of a do-notation
will also merge the whole block. If you stick to these mrg* combinators and
all the functions will merge the results, the whole program can be
symbolically evaluated efficiently.
>>>f x y = mrgIf "c" x y>>>:{do x <- unionIf (ssym "a") (return 1) (unionIf (ssym "b") (return 1) (return 2)) f x (x + 1) :: UnionM Integer :} {If (&& c (|| a b)) 1 (If (|| a (|| b c)) 2 3)}
In Grisette.Lib.Base, Grisette.Lib.Mtl, we also provided more mrg*
variants of other combinators. You should stick to these combinators to
ensure efficient merging by Grisette.
Instances
class (Eq t, Ord t, Hashable t) => IsConcrete t Source #
Tag for concrete types. Useful for specifying the merge strategy for some parametrized types where we should have different merge strategy for symbolic and concrete ones.
Instances
| IsConcrete Integer Source # | |
Defined in Grisette.Core.Control.Monad.UnionM | |
| IsConcrete Bool Source # | |
Defined in Grisette.Core.Control.Monad.UnionM | |
Arguments
| :: String | Prefix for generated wrappers |
| -> Name | The type to generate the wrappers for |
| -> Q [Dec] |
Generate constructor wrappers that wraps the result in a union-like monad.
$(makeUnionWrapper "mrg" ''Maybe)
generates
mrgNothing :: (SymBoolOp bool, Monad u, Mergeable bool t, MonadUnion bool u) => u (Maybe t) mrgNothing = mrgSingle Nothing mrgJust :: (SymBoolOp bool, Monad u, Mergeable bool t, MonadUnion bool u) => t -> u (Maybe t) mrgJust = \x -> mrgSingle (Just x)
Arguments
| :: [String] | Names for generated wrappers |
| -> Name | The type to generate the wrappers for |
| -> Q [Dec] |
Generate constructor wrappers that wraps the result in a union-like monad with provided names.
$(makeUnionWrapper' ["mrgTuple2"] ''(,))
generates
mrgTuple2 :: (SymBoolOp bool, Monad u, Mergeable bool t1, Mergeable bool t2, MonadUnion bool u) => t1 -> t2 -> u (t1, t2) mrgTuple2 = \v1 v2 -> mrgSingle (v1, v2)
liftToMonadUnion :: (Mergeable a, MonadUnion u) => UnionM a -> u a Source #
Lift the UnionM to any MonadUnion.
unionSize :: UnionM a -> Int Source #
The size of a union is defined as the number of branches. For example,
>>>unionSize (single True)1>>>unionSize (mrgIf "a" (single 1) (single 2) :: UnionM Integer)2>>>unionSize (choose [1..7] "a" :: UnionM Integer)7
Merging
Mergeable
class Mergeable a where Source #
Each type is associated with a root merge strategy given by rootStrategy.
The root merge strategy should be able to merge every value of the type.
Grisette will use the root merge strategy to merge the values of the type in
a union.
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving Mergeable via (Default X)
Instances
class Mergeable1 (u :: Type -> Type) where Source #
Lifting of the Mergeable class to unary type constructors.
Methods
liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a) Source #
Lift merge strategy through the type constructor.
Instances
rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a) Source #
Lift the root merge strategy through the unary type constructor.
class Mergeable2 (u :: Type -> Type -> Type) where Source #
Lifting of the Mergeable class to binary type constructors.
Methods
liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b) Source #
Lift merge strategy through the type constructor.
Instances
| Mergeable2 Either Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (Either a b) Source # | |
| Mergeable2 (,) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b) Source # | |
| Mergeable a => Mergeable2 ((,,) a) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a0 -> MergingStrategy b -> MergingStrategy (a, a0, b) Source # | |
rootStrategy2 :: (Mergeable a, Mergeable b, Mergeable2 u) => MergingStrategy (u a b) Source #
Lift the root merge strategy through the binary type constructor.
class Mergeable3 (u :: Type -> Type -> Type -> Type) where Source #
Lifting of the Mergeable class to ternary type constructors.
Methods
liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (u a b c) Source #
Lift merge strategy through the type constructor.
Instances
| Mergeable3 (,,) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (a, b, c) Source # | |
rootStrategy3 :: (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) => MergingStrategy (u a b c) Source #
Lift the root merge strategy through the binary type constructor.
Merging strategy
data MergingStrategy a where Source #
Merging strategies.
You probably do not need to know the details of this type if you are only going to use algebraic data types. You can get merging strategies for them with type derivation.
In Grisette, a merged union (if-then-else tree) follows the hierarchical sorted representation invariant with regards to some merging strategy.
A merging strategy encodes how to merge a subset of the values of a given type. We have three types of merging strategies:
- Simple strategy
- Sorted strategy
- No strategy
The SimpleStrategy merges values with a simple merge function.
For example,
- the symbolic boolean values can be directly merged with
ites. - the set
{1}, which is a subset of the values of the typeInteger, can be simply merged as the set contains only a single value. - all the
Justvalues of the typeMaybe SymBoolcan be simply merged by merging the wrapped symbolic boolean withites.
The SortedStrategy merges values by first grouping the values with an
indexing function, and the values with the same index will be organized as
a sub-tree in the if-then-else structure of UnionBase.
Each group (sub-tree) will be further merged with a sub-strategy for the
index.
The index type should be a totally ordered type (with the Ord
type class). Grisette will use the indexing function to partition the values
into sub-trees, and organize them in a sorted way. The sub-trees will further
be merged with the sub-strategies. For example,
- all the integers can be merged with
SortedStrategyby indexing with the identity function and use theSimpleStrategyshown before as the sub-strategies. - all the
Maybe SymBoolvalues can be merged withSortedStrategyby indexing withisJust, theNothingandJustvalues can then then be merged with different simple strategies as sub-strategies.
The NoStrategy does not perform any merging.
For example, we cannot merge values with function types that returns concrete
lists.
For ADTs, we can automatically derive the Mergeable type class, which
provides a merging strategy.
If the derived version does not work for you, you should determine
if your type can be directly merged with a merging function. If so, you can
implement the merging strategy as a SimpleStrategy.
If the type cannot be directly merged with a merging function, but could be
partitioned into subsets of values that can be simply merged with a function,
you should implement the merging strategy as a SortedStrategy.
For easier building of the merging strategies, check out the combinators
like wrapStrategy.
For more details, please see the documents of the constructors, or refer to Grisette's paper.
Constructors
| SimpleStrategy | Simple mergeable strategy. For symbolic booleans, we can implement its merge strategy as follows: SimpleStrategy ites :: MergingStrategy SymBool |
Fields
| |
| SortedStrategy | Sorted mergeable strategy. For Integers, we can implement its merge strategy as follows: SortedStrategy id (\_ -> SimpleStrategy $ \_ t _ -> t) For SortedStrategy
(\case; Nothing -> False; Just _ -> True)
(\idx ->
if idx
then SimpleStrategy $ \_ t _ -> t
else SimpleStrategy $ \cond (Just l) (Just r) -> Just $ ites cond l r) |
Fields
| |
| NoStrategy :: MergingStrategy a | For preventing the merging intentionally. This could be useful for keeping some value concrete and may help generate more efficient formulas. See Grisette's paper for details. |
derivedRootStrategy :: (Generic a, Mergeable' (Rep a)) => MergingStrategy a Source #
Generic derivation for the Mergeable class.
Usually you can derive the merging strategy with the DerivingVia and
DerivingStrategies extension.
data X = ... deriving (Generic) deriving Mergeable via (Default X)
Manual merging strategy construction
Arguments
| :: MergingStrategy a | The merge strategy to be wrapped |
| -> (a -> b) | The wrap function |
| -> (b -> a) | The unwrap function, which does not have to be defined for every value |
| -> MergingStrategy b |
Useful utility function for building merge strategies manually.
For example, to build the merge strategy for the just branch of Maybe a,
one could write
wrapStrategy Just fromMaybe rootStrategy :: MergingStrategy (Maybe a)
Arguments
| :: (a -> b -> r) | The wrap function |
| -> (r -> (a, b)) | The unwrap function, which does not have to be defined for every value |
| -> MergingStrategy a | The first merge strategy to be wrapped |
| -> MergingStrategy b | The second merge strategy to be wrapped |
| -> MergingStrategy r |
Useful utility function for building merge strategies for product types manually.
For example, to build the merge strategy for the following product type, one could write
data X = X { x1 :: Int, x2 :: Bool }
product2Strategy X (\(X a b) -> (a, b)) rootStrategy rootStrategy
:: MergingStrategy Xdata DynamicSortedIdx where Source #
Helper type for combining arbitrary number of indices into one. Useful when trying to write efficient merge strategy for lists/vectors.
Constructors
| DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx |
Instances
| Show DynamicSortedIdx Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods showsPrec :: Int -> DynamicSortedIdx -> ShowS # show :: DynamicSortedIdx -> String # showList :: [DynamicSortedIdx] -> ShowS # | |
| Eq DynamicSortedIdx Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods (==) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (/=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # | |
| Ord DynamicSortedIdx Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods compare :: DynamicSortedIdx -> DynamicSortedIdx -> Ordering # (<) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (<=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (>) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (>=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # max :: DynamicSortedIdx -> DynamicSortedIdx -> DynamicSortedIdx # min :: DynamicSortedIdx -> DynamicSortedIdx -> DynamicSortedIdx # | |
data StrategyList container where Source #
Helper type for building efficient merge strategy for list-like containers.
Constructors
| StrategyList :: forall bool a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container |
Instances
buildStrategyList :: forall bool a container. Functor container => MergingStrategy a -> container a -> StrategyList container Source #
Helper function for building efficient merge strategy for list-like containers.
resolveStrategy :: forall x. MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x) Source #
Resolves the indices and the terminal merge strategy for a value of some Mergeable type.
resolveStrategy' :: forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x) Source #
Resolves the indices and the terminal merge strategy for a value given a merge strategy for its type.
Simple mergeable types
class Mergeable a => SimpleMergeable a where Source #
This class indicates that a type has a simple root merge strategy.
Note: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving (Mergeable, SimpleMergeable) via (Default X)
Methods
mrgIte :: SymBool -> a -> a -> a Source #
Performs if-then-else with the simple root merge strategy.
>>>mrgIte "a" "b" "c" :: SymInteger(ite a b c)
Instances
class SimpleMergeable1 u where Source #
Lifting of the SimpleMergeable class to unary type constructors.
Methods
liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a Source #
Lift mrgIte through the type constructor.
>>>liftMrgIte mrgIte "a" (Identity "b") (Identity "c") :: Identity SymIntegerIdentity (ite a b c)
Instances
mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a Source #
Lift the standard mrgIte function through the type constructor.
>>>mrgIte1 "a" (Identity "b") (Identity "c") :: Identity SymIntegerIdentity (ite a b c)
class Mergeable2 u => SimpleMergeable2 u where Source #
Lifting of the SimpleMergeable class to binary type constructors.
Methods
liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b Source #
Lift mrgIte through the type constructor.
>>>liftMrgIte2 mrgIte mrgIte "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)((ite a b d),(ite a c e))
Instances
mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b Source #
Lift the standard mrgIte function through the type constructor.
>>>mrgIte2 "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)((ite a b d),(ite a c e))
UnionLike operations
class (SimpleMergeable1 u, Mergeable1 u) => UnionLike u where Source #
Special case of the Mergeable1 and SimpleMergeable1 class for type
constructors that are SimpleMergeable when applied to any Mergeable
types.
This type class is used to generalize the mrgIf function to other
containers, for example, monad transformer transformed Unions.
Minimal complete definition
Methods
Wrap a single value in the union.
Note that this function cannot propagate the Mergeable knowledge.
>>>single "a" :: UnionM SymInteger<a>>>>mrgSingle "a" :: UnionM SymInteger{a}
unionIf :: SymBool -> u a -> u a -> u a Source #
If-then-else on two union values.
Note that this function cannot capture the Mergeable knowledge. However,
it may use the merging strategy from the branches to merge the results.
>>>unionIf "a" (single "b") (single "c") :: UnionM SymInteger<If a b c>>>>unionIf "a" (mrgSingle "b") (single "c") :: UnionM SymInteger{(ite a b c)}
mergeWithStrategy :: MergingStrategy a -> u a -> u a Source #
Merge the contents with some merge strategy.
>>>mergeWithStrategy rootStrategy $ unionIf "a" (single "b") (single "c") :: UnionM SymInteger{(ite a b c)}
Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.
This function is to be called when the Mergeable constraint can not be resolved,
e.g., the merge strategy for the contained type is given with Mergeable1.
In other cases, merge is usually a better alternative.
mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result merged with some merge strategy.
>>>mrgIfWithStrategy rootStrategy "a" (mrgSingle "b") (single "c") :: UnionM SymInteger{(ite a b c)}
Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.
This function is to be called when the Mergeable constraint can not be resolved,
e.g., the merge strategy for the contained type is given with Mergeable1.
In other cases, mrgIf is usually a better alternative.
mrgSingleWithStrategy :: MergingStrategy a -> a -> u a Source #
Wrap a single value in the union and capture the Mergeable knowledge.
>>>mrgSingleWithStrategy rootStrategy "a" :: UnionM SymInteger{a}
Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.
This function is to be called when the Mergeable constraint can not be resolved,
e.g., the merge strategy for the contained type is given with Mergeable1.
In other cases, mrgSingle is usually a better alternative.
Instances
mrgIf :: (UnionLike u, Mergeable a) => SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result merged with the type's root merge strategy.
Equivalent to mrgIfWithStrategy rootStrategy
>>>mrgIf "a" (single "b") (single "c") :: UnionM SymInteger{(ite a b c)}
merge :: (UnionLike u, Mergeable a) => u a -> u a Source #
Merge the contents with the type's root merge strategy.
Equivalent to mergeWithStrategy rootStrategy
>>>merge $ unionIf "a" (single "b") (single "c") :: UnionM SymInteger{(ite a b c)}
mrgSingle :: (UnionLike u, Mergeable a) => a -> u a Source #
Wrap a single value in the type and propagate the type's root merge strategy.
Equivalent to mrgSingleWithStrategy rootStrategy
>>>mrgSingle "a" :: UnionM SymInteger{a}
class UnionLike u => UnionPrjOp (u :: Type -> Type) where Source #
Union containers that can be projected back into single value or if-guarded values.
Methods
singleView :: u a -> Maybe a Source #
Pattern match to extract single values.
>>>singleView (single 1 :: UnionM Integer)Just 1>>>singleView (unionIf "a" (single 1) (single 2) :: UnionM Integer)Nothing
ifView :: u a -> Maybe (SymBool, u a, u a) Source #
Pattern match to extract if values.
>>>ifView (single 1 :: UnionM Integer)Nothing>>>ifView (unionIf "a" (single 1) (single 2) :: UnionM Integer)Just (a,<1>,<2>)>>>ifView (mrgIf "a" (single 1) (single 2) :: UnionM Integer)Just (a,{1},{2})
The leftmost value in the union.
>>>leftMost (unionIf "a" (single 1) (single 2) :: UnionM Integer)1
Instances
pattern SingleU :: UnionPrjOp u => a -> u a Source #
Pattern match to extract single values with singleView.
>>>case (single 1 :: UnionM Integer) of SingleU v -> v1
pattern IfU :: UnionPrjOp u => SymBool -> u a -> u a -> u a Source #
type MonadUnion u = (UnionLike u, Monad u) Source #
Class for monads that support union-like operations and Mergeable knowledge propagation.
class (UnionLike m, Monad m) => MonadParallelUnion m where Source #
Parallel union monad.
With the QualifiedDo extension and the Grisette.Qualified.ParallelUnionDo
module, one can execute the paths in parallel and merge the results with:
:set -XQualifiedDo -XOverloadedStrings
import Grisette
import qualified Grisette.Qualified.ParallelUnionDo as P
P.do
x <- mrgIf "a" (return 1) (return 2) :: UnionM Int
return $ x + 1
-- {If a 2 3}Methods
parBindUnion :: (Mergeable b, NFData b) => m a -> (a -> m b) -> m b Source #
Instances
simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a Source #
Merge the simply mergeable values in a union, and extract the merged value.
In the following example, unionIf will not merge the results, and
simpleMerge will merge it and extract the single merged value.
>>>unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool<If a b c>>>>simpleMerge $ (unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool)(ite a b c)
onUnion :: forall bool u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r Source #
Lift a function to work on union values.
>>>sumU = onUnion sum>>>sumU (unionIf "cond" (return ["a"]) (return ["b","c"]) :: UnionM [SymInteger])(ite cond a (+ b c))
onUnion2 :: forall bool u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r Source #
Lift a function to work on union values.
onUnion3 :: forall bool u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r Source #
Lift a function to work on union values.
onUnion4 :: forall bool u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r Source #
Lift a function to work on union values.
(#~) :: (Function f, SimpleMergeable (Ret f), UnionPrjOp u, Functor u) => f -> u (Arg f) -> Ret f infixl 9 Source #
Helper for applying functions on UnionPrjOp and SimpleMergeable.
>>>let f :: Integer -> UnionM Integer = \x -> mrgIf (ssym "a") (mrgSingle $ x + 1) (mrgSingle $ x + 2)>>>f #~ (mrgIf (ssym "b" :: SymBool) (mrgSingle 0) (mrgSingle 2) :: UnionM Integer){If (&& b a) 1 (If b 2 (If a 3 4))}
Conversion between Concrete and Symbolic values
class ToCon a b where Source #
Convert a symbolic value to concrete value if possible.
Methods
toCon :: a -> Maybe b Source #
Convert a symbolic value to concrete value if possible.
If the symbolic value cannot be converted to concrete, the result will be Nothing.
>>>toCon (ssym "a" :: SymInteger) :: Maybe IntegerNothing
>>>toCon (con 1 :: SymInteger) :: Maybe IntegerJust 1
toCon works on complex types too.
>>>toCon ([con 1, con 2] :: [SymInteger]) :: Maybe [Integer]Just [1,2]
>>>toCon ([con 1, ssym "a"] :: [SymInteger]) :: Maybe [Integer]Nothing
Instances
class ToSym a b where Source #
Convert a concrete value to symbolic value.
Methods
Convert a concrete value to symbolic value.
>>>toSym False :: SymBoolfalse
>>>toSym [False, True] :: [SymBool][false,true]
Instances
Symbolic Generation
It is usually useful to generate complex symbolic values. For example, in program synthesis task, we may want to generate symbolic programs to represent the search space given some specification.
To help with this, we provide a set of classes and functions. The core
of the symbolic generation is the Fresh monad, the GenSymSimple class,
and the GenSym class.
The Fresh monad is a combination of specialized state and reader
monads. It keeps an identifier, and an index. The generated symbolic
constants would be constructed with both the identifier and the index.
Each time a new symbolic constant is generated, the index would be
incremented. This keeps that the generated symbolic constants are unique.
The GenSymSimple class helps generate symbolic values that do not require
a symbolic union, for example, symbolic Booleans.
It provides the simpleFresh function, which accepts a specification
for the symbolic values to generate.
We do not need any specification to generate a symbolic Boolean, so we provide a unit value as the specification:
>>>runFresh (simpleFresh ()) "x" :: SymBoolx@0
We can generate a list of symbolic Booleans by specifying the length of the list, and the specification for the elements. The two elements in the generated list are unique as they have different indices.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "x" :: [SymBool][x@0,x@1]>>>runFresh (simpleFresh (SimpleListSpec 2 (SimpleListSpec 1 ()))) "x" :: [[SymBool]][[x@0],[x@1]]
The GenSym class helps generate symbolic values that require a symbolic
union, for example, lists with different lengths.
It provides the fresh function, which accepts a specification
for the symbolic values to generate.
We can generate a list of length 0, 1, or 2 by specifying the minimum and maximum lengths, and the specification for the elements:
>>>runFresh (fresh (ListSpec 0 2 ())) "x" :: UnionM [SymBool]{If x@2 [] (If x@3 [x@1] [x@0,x@1])}
We can generate many symbolic values at once with the Fresh monad.
The symbolic constants are ensured to be unique:
>>>:set -XScopedTypeVariables>>>:{flip runFresh "x" $ do a :: SymBool <- simpleFresh () b :: UnionM [SymBool] <- fresh (ListSpec 0 2 ()) return (a, b) :} (x@0,{If x@3 [] (If x@4 [x@2] [x@1,x@2])})
When you are just generating a symbolic value, and do not need to compose
multiple simpleFresh or fresh calls, you can use the genSym and
genSymSimple functions instead.
>>>genSymSimple (SimpleListSpec 2 ()) "x" :: [SymBool][x@0,x@1]>>>genSym (ListSpec 0 2 ()) "x" :: UnionM [SymBool]{If x@2 [] (If x@3 [x@1] [x@0,x@1])}
Symbolic choices from a list of symbolic values is very useful.
With the chooseFresh function,
we can generate a symbolic value by choosing from a list of
alternative values.
Grisette would generate symbolic Boolean guards to perform the symbolic
choice.
>>>:{(flip runFresh "x" $ do a <- simpleFresh () b <- simpleFresh () chooseFresh [[a],[a,b],[a,a,b]]) :: UnionM [SymBool] :} {If x@2 [x@0] (If x@3 [x@0,x@1] [x@0,x@0,x@1])}
Symbolic Generation Context
newtype FreshIndex Source #
Index type used for GenSym.
To generate fresh variables, a monadic stateful context will be maintained. The index should be increased every time a new symbolic constant is generated.
Constructors
| FreshIndex Int |
Instances
data FreshIdent where Source #
Identifier type used for GenSym
The constructor is hidden intentionally. You can construct an identifier by:
- a raw name
The following two expressions will refer to the same identifier (the solver won't distinguish them and would assign the same value to them). The user may need to use unique names to avoid unintentional identifier collision.
>>>name "a"a
>>>"a" :: FreshIdent -- available when OverloadedStrings is enableda
- bundle the calling file location with the name to ensure global uniqueness
Identifiers created at different locations will not be the same. The identifiers created at the same location will be the same.
>>>$$(nameWithLoc "a") -- a sample result could be "a:<interactive>:18:4-18"a:<interactive>:...
- bundle the calling file location with some user provided information
Identifiers created with different name or different additional information will not be the same.
>>>nameWithInfo "a" (1 :: Int)a:1
Constructors
| FreshIdent :: String -> FreshIdent | |
| FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent |
Instances
name :: String -> FreshIdent Source #
Simple name identifier. The same identifier refers to the same symbolic variable in the whole program.
The user may need to use unique names to avoid unintentional identifier collision.
nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent Source #
Identifier with extra information. The same name with the same information refers to the same symbolic variable in the whole program.
The user may need to use unique names or additional information to avoid unintentional identifier collision.
data FileLocation Source #
Instances
nameWithLoc :: String -> SpliceQ FreshIdent Source #
Identifier with the current location as extra information.
>>>$$(nameWithLoc "a") -- a sample result could be "a:<interactive>:18:4-18"a:<interactive>:...
The uniqueness is ensured for the call to nameWithLoc at different location.
Symbolic Generation Monad
class Monad m => MonadFresh m where Source #
Monad class for fresh symbolic value generation.
The monad should be a reader monad for the FreshIdent and a state monad for
the FreshIndex.
Methods
nextFreshIndex :: m FreshIndex Source #
Increase the index by one and return the new index.
getFreshIdent :: m FreshIdent Source #
Get the identifier.
Instances
A symbolic generation monad transformer. It is a reader monad transformer for identifiers and a state monad transformer for indices.
Each time a fresh symbolic variable is generated, the index should be increased.
Instances
runFresh :: Fresh a -> FreshIdent -> a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
runFreshT :: Monad m => FreshT m a -> FreshIdent -> m a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
Symbolic Generation Class
class Mergeable a => GenSym spec a where Source #
Class of types in which symbolic values can be generated with respect to some specification.
The result will be wrapped in a union-like monad. This ensures that we can generate those types with complex merging rules.
The uniqueness of symbolic constants is managed with the a monadic context.
Fresh and FreshT can be useful.
Minimal complete definition
Nothing
Methods
fresh :: MonadFresh m => spec -> m (UnionM a) Source #
Generate a symbolic value given some specification. Within a single
MonadFresh context, calls to fresh would generate unique symbolic
constants.
The following example generates a symbolic boolean. No specification is needed.
>>>runFresh (fresh ()) "a" :: UnionM SymBool{a@0}
The following example generates booleans, which cannot be merged into a
single value with type Bool. No specification is needed.
>>>runFresh (fresh ()) "a" :: UnionM Bool{If a@0 False True}
The following example generates Maybe Bools.
There are more than one symbolic constants introduced, and their uniqueness
is ensured. No specification is needed.
>>>runFresh (fresh ()) "a" :: UnionM (Maybe Bool){If a@0 Nothing (If a@1 (Just False) (Just True))}
The following example generates lists of symbolic booleans with length 1 to 2.
>>>runFresh (fresh (ListSpec 1 2 ())) "a" :: UnionM [SymBool]{If a@2 [a@1] [a@0,a@1]}
When multiple symbolic values are generated, there will not be any identifier collision
>>>runFresh (do; a <- fresh (); b <- fresh (); return (a, b)) "a" :: (UnionM SymBool, UnionM SymBool)({a@0},{a@1})
default fresh :: GenSymSimple spec a => MonadFresh m => spec -> m (UnionM a) Source #
Instances
class GenSymSimple spec a where Source #
Class of types in which symbolic values can be generated with respect to some specification.
The result will not be wrapped in a union-like monad.
The uniqueness of symbolic constants is managed with the a monadic context.
Fresh and FreshT can be useful.
Methods
simpleFresh :: MonadFresh m => spec -> m a Source #
Generate a symbolic value given some specification. The uniqueness is ensured.
The following example generates a symbolic boolean. No specification is needed.
>>>runFresh (simpleFresh ()) "a" :: SymBoola@0
The following code generates list of symbolic boolean with length 2. As the length is fixed, we don't have to wrap the result in unions.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "a" :: [SymBool][a@0,a@1]
Instances
genSym :: GenSym spec a => spec -> FreshIdent -> UnionM a Source #
Generate a symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.
>>>genSym (ListSpec 1 2 ()) "a" :: UnionM [SymBool]{If a@2 [a@1] [a@0,a@1]}
genSymSimple :: forall spec a. GenSymSimple spec a => spec -> FreshIdent -> a Source #
Generate a simple symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.
>>>genSymSimple (SimpleListSpec 2 ()) "a" :: [SymBool][a@0,a@1]
Symbolic Generation Class Derivation
derivedNoSpecFresh :: forall bool a m u. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a) Source #
We cannot provide DerivingVia style derivation for GenSym, while you can
use this fresh implementation to implement GenSym for your own types.
This fresh implementation is for the types that does not need any specification.
It will generate product types by generating each fields with () as specification,
and generate all possible values for a sum type.
Note: Never use on recursive types.
derivedNoSpecSimpleFresh :: forall a m. (Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) => () -> m a Source #
We cannot provide DerivingVia style derivation for GenSymSimple, while
you can use this simpleFresh implementation to implement GenSymSimple fo
your own types.
This simpleFresh implementation is for the types that does not need any specification.
It will generate product types by generating each fields with () as specification.
It will not work on sum types.
Note: Never use on recursive types.
derivedSameShapeSimpleFresh :: forall a m. (Generic a, GenSymSameShape (Rep a), MonadFresh m) => a -> m a Source #
We cannot provide DerivingVia style derivation for GenSymSimple, while
you can use this simpleFresh implementation to implement GenSymSimple fo
your own types.
This simpleFresh implementation is for the types that can be generated with
a reference value of the same type.
For sum types, it will generate the result with the same data constructor. For product types, it will generate the result by generating each field with the corresponding reference value.
Note: Can be used on recursive types.
Symbolic choice
chooseFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a) Source #
Symbolically chooses one of the provided values.
The procedure creates n - 1 fresh symbolic boolean variables every time it
is evaluated, and use these variables to conditionally select one of the n
provided expressions.
The result will be wrapped in a union-like monad, and also a monad
maintaining the MonadFresh context.
>>>runFresh (chooseFresh [1,2,3]) "a" :: UnionM Integer{If a@0 1 (If a@1 2 3)}
chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a Source #
Symbolically chooses one of the provided values.
The procedure creates n - 1 fresh symbolic boolean variables every time it is evaluated, and use
these variables to conditionally select one of the n provided expressions.
The result will not be wrapped in a union-like monad, but will be
wrapped in a monad maintaining the Fresh context.
>>>import Data.Proxy>>>runFresh (chooseSimpleFresh [ssym "b", ssym "c", ssym "d"]) "a" :: SymInteger(ite a@0 b (ite a@1 c d))
chooseUnionFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a) Source #
Symbolically chooses one of the provided values wrapped in union-like
monads. The procedure creates n - 1 fresh symbolic boolean variables every
time it is evaluated, and use these variables to conditionally select one of
the n provided expressions.
The result will be wrapped in a union-like monad, and also a monad
maintaining the Fresh context.
>>>let a = runFresh (chooseFresh [1, 2]) "a" :: UnionM Integer>>>let b = runFresh (chooseFresh [2, 3]) "b" :: UnionM Integer>>>runFresh (chooseUnionFresh [a, b]) "c" :: UnionM Integer{If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)}
choose :: forall bool a u. Mergeable a => [a] -> FreshIdent -> UnionM a Source #
A wrapper for chooseFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
chooseSimple :: forall a. SimpleMergeable a => [a] -> FreshIdent -> a Source #
A wrapper for chooseSimpleFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
chooseUnion :: forall a u. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a Source #
A wrapper for chooseUnionFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
Useful specifications
data EnumGenBound a Source #
Specification for numbers with lower bound (inclusive) and upper bound (exclusive)
>>>runFresh (fresh (EnumGenBound @Integer 0 4)) "c" :: UnionM Integer{If c@0 0 (If c@1 1 (If c@2 2 3))}
Constructors
| EnumGenBound a a |
Instances
| (Enum v, Mergeable v) => GenSym (EnumGenBound v) v Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => EnumGenBound v -> m (UnionM v) Source # | |
newtype EnumGenUpperBound a Source #
Specification for enum values with upper bound (exclusive). The result would chosen from [0 .. upperbound].
>>>runFresh (fresh (EnumGenUpperBound @Integer 4)) "c" :: UnionM Integer{If c@0 0 (If c@1 1 (If c@2 2 3))}
Constructors
| EnumGenUpperBound a |
Instances
| (Enum v, Mergeable v) => GenSym (EnumGenUpperBound v) v Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => EnumGenUpperBound v -> m (UnionM v) Source # | |
Specification for list generation.
>>>runFresh (fresh (ListSpec 0 2 ())) "c" :: UnionM [SymBool]{If c@2 [] (If c@3 [c@1] [c@0,c@1])}
>>>runFresh (fresh (ListSpec 0 2 (SimpleListSpec 1 ()))) "c" :: UnionM [[SymBool]]{If c@2 [] (If c@3 [[c@1]] [[c@0],[c@1]])}
Constructors
| ListSpec | |
Fields
| |
data SimpleListSpec spec Source #
Specification for list generation of a specific length.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "c" :: [SymBool][c@0,c@1]
Constructors
| SimpleListSpec | |
Fields
| |
Instances
| Show spec => Show (SimpleListSpec spec) Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods showsPrec :: Int -> SimpleListSpec spec -> ShowS # show :: SimpleListSpec spec -> String # showList :: [SimpleListSpec spec] -> ShowS # | |
| (GenSymSimple spec a, Mergeable a) => GenSym (SimpleListSpec spec) [a] Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SimpleListSpec spec -> m (UnionM [a]) Source # | |
| GenSymSimple spec a => GenSymSimple (SimpleListSpec spec) [a] Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SimpleListSpec spec -> m [a] Source # | |
Error Handling
Grisette supports using ExceptT to handle errors,
and provides the mrg* variants for the combinators in Grisette.Lib.Mtl,
for example, mrgThrowError.
>>>import Control.Monad.Except>>>import Grisette.Lib.Mtl>>>mrgThrowError AssertionError :: ExceptT AssertionError UnionM ()ExceptT {Left AssertionError}
You can define your own error types, and reason about them with the solver APIs.
>>>:set -XDerivingVia -XDeriveGeneric -XDerivingStrategies -XLambdaCase>>>import GHC.Generics>>>import Grisette.Backend.SBV>>>:{data Error = Error1 | Error2 | Error3 deriving (Show, Generic) deriving (Mergeable) via Default Error :}
>>>let [a,b,c] = ["a","b","c"] :: [SymBool]>>>res = mrgIf a (throwError Error1) (mrgIf b (return c) (throwError Error2)) :: ExceptT Error UnionM SymBool>>>resExceptT {If (|| a (! b)) (If a (Left Error1) (Left Error2)) (Right c)}>>>solveExcept (precise z3) (\case Left _ -> con False; Right x -> x) resRight (Model {a -> False :: Bool, b -> True :: Bool, c -> True :: Bool})
The solver call in the above example means that we want the solver to find the conditions under which no error is thrown, and the result is true. For more details, please refer to the documentation of the solver APIs.
For those who prefer to encode errors as assertions and assumptions,
we provide the symAssert and symAssume functions. These functions
relies on the TransformError type class to transform the assertions
and assumptions to the user-defined error type.
See their documentation for details.
Predefined errors
data AssertionError Source #
Assertion error.
Constructors
| AssertionError |
Instances
data VerificationConditions Source #
Verification conditions. A crashed program path can terminate with either assertion violation errors or assumption violation errors.
Constructors
| AssertionViolation | |
| AssumptionViolation |
Instances
Error transformation
class TransformError from to where Source #
This class indicates that the error type to can always represent the
error type from.
This is useful in implementing generic procedures that may throw errors.
For example, we support symbolic division and modulo operations. These
operations should throw an error when the divisor is zero, and we use the
standard error type ArithException for this purpose.
However, the user may use other type to represent errors, so we need this
type class to transform the ArithException to the
user-defined types.
Another example of these generic procedures is the
symAssert and symAssume functions.
They can be used with any error types that are
compatible with the AssertionError and
VerificationConditions types, respectively.
Methods
transformError :: from -> to Source #
Transforms an error with type from to an error with type to.
Instances
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 IntegerExceptT <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 IntegerExceptT {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 IntegerExceptT {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 ())}
symAssertWith :: (Mergeable e, MonadError e erm, MonadUnion erm) => e -> SymBool -> erm () Source #
symAssertTransformableError :: (Mergeable to, TransformError from to, MonadError to erm, MonadUnion erm) => from -> SymBool -> erm () Source #
Used within a monadic multi path computation for exception processing.
Terminate the current execution path with the specified error if the condition does not hold. Compatible error can be transformed.
>>>let assert = symAssertTransformableError AssertionError>>>assert "a" :: ExceptT AssertionError UnionM ()ExceptT {If (! a) (Left AssertionError) (Right ())}
symThrowTransformableError :: (Mergeable to, Mergeable a, TransformError from to, MonadError to erm, MonadUnion erm) => from -> erm a Source #
Used within a monadic multi path computation to begin exception processing.
Terminate the current execution path with the specified error. Compatible errors can be transformed.
>>>symThrowTransformableError Overflow :: ExceptT AssertionError UnionM ()ExceptT {Left AssertionError}
Simulate CBMC error handling
newtype CBMCEither a b Source #
A wrapper type for Either. Uses different merging strategies.
Constructors
| CBMCEither | |
Fields
| |
Instances
newtype CBMCExceptT e m a Source #
Similar to ExceptT, but with different error handling mechanism.
Constructors
| CBMCExceptT | |
Fields
| |
Instances
cbmcExcept :: Monad m => Either e a -> CBMCExceptT e m a Source #
Wrap an Either value in CBMCExceptT
mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b Source #
Map the error and values in a CBMCExceptT
withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a Source #
Map the error in a CBMCExceptT
Solver backend
Grisette abstracts the solver backend with the Solver type class,
and the most basic solver call is the solve function.
In the following code, we will search for the integer solutions to two
equation systems.
The first equation system, as shown below, has the solution (x, y) = (13, -7).
\[ \left\{ \begin{aligned} x + y &= 6 \\ x - y &= 20 \end{aligned} \right. \]
The second equation system, as shown below, has no integer solutions.
\[ \left\{ \begin{aligned} x + y &= 6 \\ x - y &= 19 \end{aligned} \right. \]
>>>import Grisette.IR.SymPrim>>>import Grisette.Backend.SBV>>>let x = "x" :: SymInteger>>>let y = "y" :: SymInteger>>>solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)Right (Model {x -> 13 :: Integer, y -> -7 :: Integer})>>>solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 19)Left Unsat
The first parameter of solve is the solver configuration.
Here it means that we should not perform any approximation, and should
use the Z3 solver.
The second parameter is the formula to be solved. It have the type SymBool.
The solve function would return a model if the formula is satisfiable.
The model is a mapping from symbolic variables to concrete values,
as shown in the following example.
Right (Model {x -> 13 :: Integer, y -> -7 :: Integer})This model maps x to 13, and y to -7. With this model, we can then evaluate symbolic values. The following code evaluates the product of x and y under the solution of the equation system.
>>>Right m <- solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)>>>evaluateSym False m (x * y)-91
You may notice that the first argument to the evaluateSym function is
a Boolean value False. This argument controls whether the evaluation
should assign a default value to the symbolic constants that does not
appear in the model. When the argument is False, the evaluation would
preserve any symbolic constants that does not appear in the model, and
partially evaluate the expression. When the argument is True, the
evaluation would assign a default value to the symbolic constants that
does not appear in the model, e.g., 0 for integers, and the evaluation
result would become a concrete value -91.
>>>let z = "z" :: SymInteger>>>evaluateSym False m (x * y + z)(+ -91 z)>>>evaluateSym True m (x * y + z)-91
Grisette also provides convenient functions to solve problems with error handling. The lambda case function used in the following code means that we would like the solver to find path that would not lead to an error. This is done by mapping left values (failed paths) to false, and right values (successful paths) to true.
The following example finds bugs in a program in the hard way. It is an overkill for such a simple program, but it is a good example to show how to use Grisette to solve problems with error handling.
We can first define the error type used in the program.
>>>:set -XLambdaCase -XDeriveGeneric -XDerivingStrategies -XDerivingVia>>>import Control.Monad.Except>>>import Control.Exception>>>import GHC.Generics>>>:{data Error = Arith | Assert deriving (Show, Generic) deriving (Mergeable, SEq) via (Default Error) :}
Then we can perform the symbolic evaluation. The divs function throws
ArithException when the divisor is 0, which would be transformed to
Arith, and the symAssert function would throw AssertionError when
the condition is false, which would be transformed to Assert.
>>>let x = "x" :: SymInteger>>>let y = "y" :: SymInteger>>>assert = symAssertWith Assert>>>sdiv = safeDiv' (const Arith)>>>:{-- equivalent concrete program: -- let x = x `div` y -- if z > 0 then assert (x >= y) else return () res :: ExceptT Error UnionM () res = do z <- x `sdiv` y mrgIf (z >~ 0) (assert (x >=~ y)) (return ()) :}
Then we can ask the solver to find a counter-example that would lead to
an assertion violation error, but do not trigger the division by zero
error.
This can be done by asking the solver to find a path that produce
Left Assert.
>>>resExceptT {If (|| (= y 0) (&& (< 0 (div x y)) (! (<= y x)))) (If (= y 0) (Left Arith) (Left Assert)) (Right ())}
>>> solveExcept (UnboundedReasoning z3) (==~ Left Assert) res
Right (Model {x -> -6 :: Integer, y -> -3 :: Integer}) -- possible outputGrisette also provide implementation for counter-example guided inductive
synthesis (CEGIS) algorithm. See the documentation for CEGISSolver for
more details.
Solver interface
class Solver config failure | config -> failure where Source #
A solver interface.
Methods
Arguments
| :: config | solver configuration |
| -> SymBool | formula to solve, the solver will try to make it true |
| -> IO (Either failure Model) |
Solve a single formula. Find an assignment to it to make it true.
>>>solve (precise z3) ("a" &&~ ("b" :: SymInteger) ==~ 1)Right (Model {a -> True :: Bool, b -> 1 :: Integer})>>>solve (precise z3) ("a" &&~ nots "a")Left Unsat
Arguments
| :: config | solver configuration |
| -> Int | maximum number of models to return |
| -> SymBool | formula to solve, the solver will try to make it true |
| -> IO ([Model], failure) |
Solve a single formula while returning multiple models to make it true. The maximum number of desired models are given.
>>> solveMulti (precise z3) 4 ("a" ||~ "b")
[Model {a -> True :: Bool, b -> False :: Bool},Model {a -> False :: Bool, b -> True :: Bool},Model {a -> True :: Bool, b -> True :: Bool}]Arguments
| :: config | solver configuration |
| -> SymBool | formula to solve, the solver will try to make it true |
| -> IO [Model] |
Solve a single formula while returning multiple models to make it true. All models are returned.
>>> solveAll (precise z3) ("a" ||~ "b")
[Model {a -> True :: Bool, b -> False :: Bool},Model {a -> False :: Bool, b -> True :: Bool},Model {a -> True :: Bool, b -> True :: Bool}]Instances
| Solver (GrisetteSMTConfig n) SolvingFailure Source # | |
Defined in Grisette.Backend.SBV.Data.SMT.Solving Methods solve :: GrisetteSMTConfig n -> SymBool -> IO (Either SolvingFailure Model) Source # solveMulti :: GrisetteSMTConfig n -> Int -> SymBool -> IO ([Model], SolvingFailure) Source # solveAll :: GrisetteSMTConfig n -> SymBool -> IO [Model] Source # | |
class UnionWithExcept t u e v | t -> u e v where Source #
A class that abstracts the union-like structures that contains exceptions.
Methods
extractUnionExcept :: t -> u (Either e v) Source #
Extract a union of exceptions and values from the structure.
Instances
| UnionWithExcept (UnionM (Either e v)) UnionM e v Source # | |
Defined in Grisette.Core.Control.Monad.UnionM | |
| UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v Source # | |
Defined in Grisette.Core.Control.Monad.UnionM Methods extractUnionExcept :: UnionM (CBMCEither e v) -> UnionM (Either e v) Source # | |
| (Monad u, UnionLike u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v Source # | |
Defined in Grisette.Core.Control.Monad.CBMCExcept Methods extractUnionExcept :: CBMCExceptT e u v -> u (Either e v) Source # | |
| UnionWithExcept (ExceptT e u v) u e v Source # | |
Defined in Grisette.Core.Data.Class.Solver Methods extractUnionExcept :: ExceptT e u v -> u (Either e v) Source # | |
Arguments
| :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure) | |
| => config | solver configuration |
| -> (Either e v -> SymBool) | mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true |
| -> t | the program to be solved, should be a union of exception and values |
| -> IO (Either failure Model) |
Solver procedure for programs with error handling.
>>>:set -XLambdaCase>>>import Control.Monad.Except>>>let x = "x" :: SymInteger>>>:{res :: ExceptT AssertionError UnionM () res = do symAssert $ x >~ 0 -- constrain that x is positive symAssert $ x <~ 2 -- constrain that x is less than 2 :}
>>>:{translate (Left _) = con False -- errors are not desirable translate _ = con True -- non-errors are desirable :}
>>>solveExcept (precise z3) translate resRight (Model {x -> 1 :: Integer})
Arguments
| :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, Solver config failure) | |
| => config | solver configuration |
| -> Int | maximum number of models to return |
| -> (Either e v -> SymBool) | mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true |
| -> t | the program to be solved, should be a union of exception and values |
| -> IO ([Model], failure) |
Solver procedure for programs with error handling. Would return multiple models if possible.
Counter-example Guided Inductive Synthesis (CEGIS)
class CEGISSolver config failure | config -> failure where Source #
Counter-example guided inductive synthesis (CEGIS) solver interface.
Methods
Arguments
| :: (EvaluateSym inputs, ExtractSymbolics inputs) | |
| => config | The configuration of the solver |
| -> [inputs] | Some initial counter-examples. Providing some concrete
inputs may help the solver to find a model faster. Providing
symbolic inputs would cause the solver to find the program
that works on all the inputs representable by it (see
|
| -> (inputs -> CEGISCondition) | The function mapping the inputs to the conditions for the solver to solve. |
| -> IO ([inputs], Either failure Model) | The counter-examples generated during the CEGIS loop, and the model found by the solver. |
CEGIS with multiple (possibly symbolic) inputs. Solves the following formula (see
CEGISCondition for details).
\[ \forall P. (\exists I\in\mathrm{inputs}. \mathrm{pre}(P, I)) \wedge (\forall I\in\mathrm{inputs}. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I)) \]
For simpler queries, where the inputs are representable by a single
symbolic value, you may want to use cegis or cegisExcept instead.
We have an example for the cegis call.
Instances
| CEGISSolver (GrisetteSMTConfig n) SolvingFailure Source # | |
Defined in Grisette.Backend.SBV.Data.SMT.Solving Methods cegisMultiInputs :: (EvaluateSym inputs, ExtractSymbolics inputs) => GrisetteSMTConfig n -> [inputs] -> (inputs -> CEGISCondition) -> IO ([inputs], Either SolvingFailure Model) Source # | |
data CEGISCondition Source #
The condition for CEGIS to solve.
The first argument is the pre-condition, and the second argument is the post-condition.
The CEGIS procedures would try to find a model for the formula
\[ \forall P. (\exists I. \mathrm{pre}(P, I)) \wedge (\forall I. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I)) \]
In program synthesis tasks, \(P\) is the symbolic constants in the symbolic program, and \(I\) is the input. The pre-condition is used to restrict the search space of the program. The procedure would only return programs that meets the pre-conditions on every possible inputs, and there are at least one possible input. The post-condition is used to specify the desired program behaviors.
Constructors
| CEGISCondition SymBool SymBool |
Instances
cegisPostCond :: SymBool -> CEGISCondition Source #
Construct a CEGIS condition with only a post-condition. The pre-condition would be set to true, meaning that all programs in the program space are allowed.
cegisPrePost :: SymBool -> SymBool -> CEGISCondition Source #
Construct a CEGIS condition with both pre- and post-conditions.
Arguments
| :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs) | |
| => config | The configuration of the solver |
| -> inputs | Initial symbolic inputs. The solver will try to find a
program that works on all the inputs representable by it (see
|
| -> CEGISCondition | The condition for the solver to solve. All the symbolic constants that are not in the inputs will be considered as part of the symbolic program. |
| -> IO ([inputs], Either failure Model) | The counter-examples generated during the CEGIS loop, and the model found by the solver. |
CEGIS with a single symbolic input to represent a set of inputs.
The following example tries to find the value of c such that for all
positive x, x * c && c -2. The c >~ -2 clause is used to make
the solution unique.
>>>:set -XOverloadedStrings>>>let [x,c] = ["x","c"] :: [SymInteger]>>>cegis (precise z3) x (cegisPrePost (x >~ 0) (x * c <~ 0 &&~ c >~ -2))([],Right (Model {c -> -1 :: Integer}))
cegisExcept :: (UnionWithExcept t u e v, UnionPrjOp u, Functor u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> (Either e v -> CEGISCondition) -> t -> IO ([inputs], Either failure Model) Source #
CEGIS for symbolic programs with error handling, using a single symbolic input to represent a set of inputs.
cegisExcept is particularly useful when custom error types are used.
With cegisExcept, you define how the errors are interpreted to the
CEGIS conditions after the symbolic evaluation. This could increase the
readability and modularity of the code.
The following example tries to find the value of c such that for all
positive x, x * c && c -2. The c >~ -2 assertion is used to make
the solution unique.
>>>:set -XOverloadedStrings>>>let [x,c] = ["x","c"] :: [SymInteger]>>>import Control.Monad.Except>>>:{res :: ExceptT VerificationConditions UnionM () res = do symAssume $ x >~ 0 symAssert $ x * c <~ 0 symAssert $ c >~ -2 :}
>>>:{translation (Left AssumptionViolation) = cegisPrePost (con False) (con True) translation (Left AssertionViolation) = cegisPostCond (con False) translation _ = cegisPostCond (con True) :}
>>>cegisExcept (precise z3) x translation res([],Right (Model {c -> -1 :: Integer}))
cegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> t -> IO ([inputs], Either failure Model) Source #
CEGIS for symbolic programs with error handling, using a single symbolic
input to represent a set of inputs. This function saves the efforts to
implement the translation function for the standard error type
VerificationConditions, and the standard result type ().
This function translates assumption violations to failed pre-conditions,
and translates assertion violations to failed post-conditions.
The () result will not fail any conditions.
The following example tries to find the value of c such that for all
positive x, x * c && c -2. The c >~ -2 assertion is used to make
the solution unique.
>>>:set -XOverloadedStrings>>>let [x,c] = ["x","c"] :: [SymInteger]>>>import Control.Monad.Except>>>:{res :: ExceptT VerificationConditions UnionM () res = do symAssume $ x >~ 0 symAssert $ x * c <~ 0 symAssert $ c >~ -2 :}
>>>cegisExceptStdVC (precise z3) x res([],Right (Model {c -> -1 :: Integer}))
cegisExceptVC :: (UnionWithExcept t u e v, UnionPrjOp u, Monad u, EvaluateSym inputs, ExtractSymbolics inputs, CEGISSolver config failure) => config -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> t -> IO ([inputs], Either failure Model) Source #
CEGIS for symbolic programs with error handling, using a single symbolic input to represent a set of inputs.
The errors should be translated to assertion or assumption violations.
cegisExceptMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u e v, UnionPrjOp u, Monad u) => config -> [inputs] -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], Either failure Model) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly symbolic) inputs to represent a set of inputs.
cegisExceptStdVCMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u VerificationConditions (), UnionPrjOp u, Monad u) => config -> [inputs] -> (inputs -> t) -> IO ([inputs], Either failure Model) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly
symbolic) inputs to represent a set of inputs. This function saves the
efforts to implement the translation function for the standard error type
VerificationConditions, and the standard result type ().
This function translates assumption violations to failed pre-conditions,
and translates assertion violations to failed post-conditions.
The () result will not fail any conditions.
cegisExceptVCMultiInputs :: (CEGISSolver config failure, EvaluateSym inputs, ExtractSymbolics inputs, UnionWithExcept t u e v, UnionPrjOp u, Monad u) => config -> [inputs] -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], Either failure Model) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly symbolic) inputs to represent a set of inputs.
The errors should be translated to assertion or assumption violations.
Symbolic constant extraction
class Monoid symbolSet => SymbolSetOps symbolSet (typedSymbol :: Type -> Type) | symbolSet -> typedSymbol where Source #
The operations on symbolic constant sets
Note that symbolic constants with different types are considered different.
>>>let aBool = "a" :: TypedSymbol Bool>>>let bBool = "b" :: TypedSymbol Bool>>>let cBool = "c" :: TypedSymbol Bool>>>let aInteger = "a" :: TypedSymbol Integer>>>emptySet :: SymbolSetSymbolSet {}>>>containsSymbol aBool (buildSymbolSet aBool :: SymbolSet)True>>>containsSymbol bBool (buildSymbolSet aBool :: SymbolSet)False>>>insertSymbol aBool (buildSymbolSet aBool :: SymbolSet)SymbolSet {a :: Bool}>>>insertSymbol aInteger (buildSymbolSet aBool :: SymbolSet)SymbolSet {a :: Bool, a :: Integer}>>>let abSet = buildSymbolSet (aBool, bBool) :: SymbolSet>>>let acSet = buildSymbolSet (aBool, cBool) :: SymbolSet>>>intersectionSet abSet acSetSymbolSet {a :: Bool}>>>unionSet abSet acSetSymbolSet {a :: Bool, b :: Bool, c :: Bool}>>>differenceSet abSet acSetSymbolSet {b :: Bool}
Methods
emptySet :: symbolSet Source #
Construct an empty set
isEmptySet :: symbolSet -> Bool Source #
Check if the set is empty
containsSymbol :: forall a. typedSymbol a -> symbolSet -> Bool Source #
Check if the set contains the given symbol
insertSymbol :: forall a. typedSymbol a -> symbolSet -> symbolSet Source #
Insert a symbol into the set
intersectionSet :: symbolSet -> symbolSet -> symbolSet Source #
Set intersection
unionSet :: symbolSet -> symbolSet -> symbolSet Source #
Set union
differenceSet :: symbolSet -> symbolSet -> symbolSet Source #
Set difference
Instances
| SymbolSetOps SymbolSet TypedSymbol Source # | |
Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods emptySet :: SymbolSet Source # isEmptySet :: SymbolSet -> Bool Source # containsSymbol :: TypedSymbol a -> SymbolSet -> Bool Source # insertSymbol :: TypedSymbol a -> SymbolSet -> SymbolSet Source # intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet Source # unionSet :: SymbolSet -> SymbolSet -> SymbolSet Source # differenceSet :: SymbolSet -> SymbolSet -> SymbolSet Source # | |
class SymbolSetOps symbolSet typedSymbol => SymbolSetRep rep symbolSet (typedSymbol :: * -> *) where Source #
A type class for building a symbolic constant set manually from a symbolic constant set representation
>>>buildSymbolSet ("a" :: TypedSymbol Bool, "b" :: TypedSymbol Bool) :: SymbolSetSymbolSet {a :: Bool, b :: Bool}
Instances
class ExtractSymbolics a where Source #
Extracts all the symbolic variables that are transitively contained in the given value.
>>>extractSymbolics ("a" :: SymBool) :: SymbolSetSymbolSet {a :: Bool}
>>>extractSymbolics (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: UnionM [SymBool]) :: SymbolSetSymbolSet {a :: Bool, b :: Bool, c :: Bool, d :: Bool}
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving ExtractSymbolics via (Default X)
Methods
extractSymbolics :: a -> SymbolSet Source #
Instances
Evaluation with a model
When given a satisfiable formula, a solver can return a model that specifies the concrete assignments of the variables in the formula to make the formula true. We can use this model to evaluate some symbolic values by substituting the symbolic constants with the concrete assignments.
class SymbolSetOps symbolSet typedSymbol => ModelOps model symbolSet typedSymbol | model -> symbolSet typedSymbol where Source #
The operations on Models.
Note that symbolic constants with different types are considered different.
>>>let aBool = "a" :: TypedSymbol Bool>>>let bBool = "b" :: TypedSymbol Bool>>>let cBool = "c" :: TypedSymbol Bool>>>let aInteger = "a" :: TypedSymbol Integer>>>emptyModel :: ModelModel {}>>>valueOf aBool (buildModel (aBool ::= True) :: Model)Just True>>>valueOf bBool (buildModel (aBool ::= True) :: Model)Nothing>>>insertValue bBool False (buildModel (aBool ::= True) :: Model)Model {a -> True :: Bool, b -> False :: Bool}>>>let abModel = buildModel (aBool ::= True, bBool ::= False) :: Model>>>let acSet = buildSymbolSet (aBool, cBool) :: SymbolSet>>>exceptFor acSet abModelModel {b -> False :: Bool}>>>restrictTo acSet abModelModel {a -> True :: Bool}>>>extendTo acSet abModelModel {a -> True :: Bool, b -> False :: Bool, c -> False :: Bool}>>>exact acSet abModelModel {a -> True :: Bool, c -> False :: Bool}
Minimal complete definition
emptyModel, isEmptyModel, modelContains, valueOf, insertValue, exceptFor, exceptFor', restrictTo, extendTo
Methods
emptyModel :: model Source #
Construct an empty model
isEmptyModel :: model -> Bool Source #
Check if the model is empty
modelContains :: typedSymbol a -> model -> Bool Source #
Check if the model contains the given symbol
valueOf :: typedSymbol t -> model -> Maybe t Source #
Extract the assigned value for a given symbolic constant
insertValue :: typedSymbol t -> t -> model -> model Source #
Insert an assignment into the model
exceptFor :: symbolSet -> model -> model Source #
Returns a model that removed all the assignments for the symbolic constants in the set
exceptFor' :: typedSymbol t -> model -> model Source #
Returns a model that removed the assignments for the symbolic constants
restrictTo :: symbolSet -> model -> model Source #
Returns a model that only keeps the assignments for the symbolic constants in the set
extendTo :: symbolSet -> model -> model Source #
Returns a model that extends the assignments for the symbolic constants in the set by assigning default values to them
exact :: symbolSet -> model -> model Source #
Returns a model that contains the assignments for exactly the symbolic constants in the set by removing assignments for the symbolic constants that are not in the set and add assignments for the missing symbolic constants by assigning default values to them.
Instances
| ModelOps Model SymbolSet TypedSymbol Source # | |
Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods emptyModel :: Model Source # isEmptyModel :: Model -> Bool Source # modelContains :: TypedSymbol a -> Model -> Bool Source # valueOf :: TypedSymbol t -> Model -> Maybe t Source # insertValue :: TypedSymbol t -> t -> Model -> Model Source # exceptFor :: SymbolSet -> Model -> Model Source # exceptFor' :: TypedSymbol t -> Model -> Model Source # restrictTo :: SymbolSet -> Model -> Model Source # | |
class ModelRep rep model | rep -> model where Source #
A type class for building a model manually from a model representation
Methods
buildModel :: rep -> model Source #
Build a model
>>>let aBool = "a" :: TypedSymbol Bool>>>let bBool = "b" :: TypedSymbol Bool>>>buildModel (aBool ::= True, bBool ::= False) :: ModelModel {a -> True :: Bool, b -> False :: Bool}
Instances
class EvaluateSym a where Source #
Evaluating symbolic values with some model.
>>>let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model>>>evaluateSym False model ([ssym "a", ssym "b"] :: [SymInteger])[1,b]
If we set the first argument true, the missing variables will be filled in with some default values:
>>>evaluateSym True model ([ssym "a", ssym "b"] :: [SymInteger])[1,0]
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving EvaluateSym via (Default X)
Methods
evaluateSym :: Bool -> Model -> a -> a Source #
Evaluate a symbolic variable with some model, possibly fill in values for the missing variables.
Instances
evaluateSymToCon :: (ToCon a b, EvaluateSym a) => Model -> a -> b Source #
Evaluate a symbolic variable with some model, fill in values for the missing variables, and transform to concrete ones
>>>let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model>>>evaluateSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer][1,0]
Substitution of a symbol
class SubstituteSym a where Source #
Substitution of symbolic constants.
>>>a = "a" :: TypedSymbol Bool>>>v = "x" &&~ "y" :: SymBool>>>substituteSym a v (["a" &&~ "b", "a"] :: [SymBool])[(&& (&& x y) b),(&& x y)]
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving SubstituteSym via (Default X)
Methods
substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a Source #
Instances
class SubstituteSym' a where Source #
Auxiliary class for SubstituteSym instance derivation
Methods
substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> a c -> a c Source #
Auxiliary function for substituteSym derivation
Instances
Type Class Derivation
This newtype wrapper can be used to derive default instances for
classes taking an argument of kind Type.
Instances
| (Generic a, Generic b, ToCon' (Rep a) (Rep b)) => ToCon a (Default b) Source # | |
| (Generic a, Generic b, ToSym' (Rep a) (Rep b)) => ToSym a (Default b) Source # | |
Defined in Grisette.Core.Data.Class.ToSym | |
| (Generic a, GEq a, Enum' (Rep a)) => GEnum (Default a) | The |
Defined in Generics.Deriving.Default | |
| (Generic a, GEq' (Rep a)) => GEq (Default a) | |
| (Generic a, GMonoid' (Rep a)) => GMonoid (Default a) | |
| (Generic a, GSemigroup' (Rep a)) => GSemigroup (Default a) | Semigroups often have many sensible implementations of
In other cases, one may wish to use the existing wrapper newtypes in
newtype FirstSemigroup = FirstSemigroup |
| (Generic a, GShow' (Rep a)) => GShow (Default a) | For example, with this type: newtype TestShow = TestShow
In this example, In general, when using a newtype wrapper, the instance can be derived
via the wrapped type, as here (via |
| (Generic a, Uniplate' (Rep a) a, Context' (Rep a) a) => Uniplate (Default a) | |
Defined in Generics.Deriving.Default Methods children :: Default a -> [Default a] # context :: Default a -> [Default a] -> Default a # descend :: (Default a -> Default a) -> Default a -> Default a # descendM :: Monad m => (Default a -> m (Default a)) -> Default a -> m (Default a) # transform :: (Default a -> Default a) -> Default a -> Default a # transformM :: Monad m => (Default a -> m (Default a)) -> Default a -> m (Default a) # | |
| (Generic a, SEq' (Rep a)) => SEq (Default a) Source # | |
| (Generic a, EvaluateSym' (Rep a)) => EvaluateSym (Default a) Source # | |
Defined in Grisette.Core.Data.Class.Evaluate | |
| (Generic a, ExtractSymbolics' (Rep a)) => ExtractSymbolics (Default a) Source # | |
Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: Default a -> SymbolSet Source # | |
| (Generic a, Mergeable' (Rep a)) => Mergeable (Default a) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (Default a) Source # | |
| (SEq a, Generic a, SOrd' (Rep a)) => SOrd (Default a) Source # | |
Defined in Grisette.Core.Data.Class.SOrd | |
| (Generic a, Mergeable' (Rep a), SimpleMergeable' (Rep a)) => SimpleMergeable (Default a) Source # | |
| (Generic a, SubstituteSym' (Rep a)) => SubstituteSym (Default a) Source # | |
Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Default a -> Default a Source # | |
| (Generic a, AllSyms' (Rep a)) => AllSyms (Default a) Source # | |
newtype Default1 (f :: Type -> Type) a #
This newtype wrapper can be used to derive default instances for
classes taking an argument of kind Type -> Type
Constructors
| Default1 | |
Fields
| |
Instances
| (Generic1 f, GCopoint' (Rep1 f)) => GCopoint (Default1 f) | |
Defined in Generics.Deriving.Default | |
| (Generic1 t, GFoldable' (Rep1 t)) => GFoldable (Default1 t) | |
Defined in Generics.Deriving.Default Methods gfoldMap :: Monoid m => (a -> m) -> Default1 t a -> m # gfold :: Monoid m => Default1 t m -> m # gfoldr :: (a -> b -> b) -> b -> Default1 t a -> b # gfoldr' :: (a -> b -> b) -> b -> Default1 t a -> b # gfoldl :: (a -> b -> a) -> a -> Default1 t b -> a # gfoldl' :: (a -> b -> a) -> a -> Default1 t b -> a # | |
| (Generic1 f, GFunctor' (Rep1 f)) => GFunctor (Default1 f) | |
Defined in Generics.Deriving.Default | |
| (Generic1 t, GFunctor' (Rep1 t), GFoldable' (Rep1 t), GTraversable' (Rep1 t)) => GTraversable (Default1 t) | |
Defined in Generics.Deriving.Default | |
| (Generic1 u, Mergeable1' (Rep1 u)) => Mergeable1 (Default1 u) Source # | |
Defined in Grisette.Core.Data.Class.Mergeable Methods liftRootStrategy :: MergingStrategy a -> MergingStrategy (Default1 u a) Source # | |
Utilities
Memoization
htmemo :: (Eq k, Hashable k) => (k -> a) -> k -> a Source #
Function memoizer with mutable hash table.
htmemo2 :: (Eq k1, Hashable k1, Eq k2, Hashable k2) => (k1 -> k2 -> a) -> k1 -> k2 -> a Source #
Function memoizer with mutable hash table. Works on binary functions.
htmemo3 :: (Eq k1, Hashable k1, Eq k2, Hashable k2, Eq k3, Hashable k3) => (k1 -> k2 -> k3 -> a) -> k1 -> k2 -> k3 -> a Source #
Function memoizer with mutable hash table. Works on ternary functions.
htmup :: (Eq k, Hashable k) => (b -> c) -> (k -> b) -> k -> c Source #
Lift a memoizer to work with one more argument.
htmemoFix :: (Eq k, Hashable k) => ((k -> a) -> k -> a) -> k -> a Source #
Memoizing recursion. Use like fix.
Bundled Constructor Wrappers
mrgTuple3 :: forall (a :: Type) (b :: Type) (c :: Type). Mergeable (a, b, c) => a -> b -> c -> UnionM (a, b, c) Source #
mrgLeft :: forall (a :: Type) (b :: Type). Mergeable (Either a b) => a -> UnionM (Either a b) Source #
mrgRight :: forall (a :: Type) (b :: Type). Mergeable (Either a b) => b -> UnionM (Either a b) Source #
mrgInL :: forall {k :: Type} (f :: k -> Type) (g :: k -> Type) (a :: k). Mergeable (Sum f g a) => f a -> UnionM (Sum f g a) Source #