Lang.Crucible.Simulator.PathSatisfiability

Documentation

checkPathSatisfiability :: ConfigOption BaseBoolType

pathSatisfiabilityFeature

Arguments

:: forall sym. IsSymInterface sym

=> sym

-> (Maybe ProgramLoc -> Pred sym -> IO BranchResult)

An action for considering the satisfiability of a predicate. In the current state of the symbolic interface, indicate what we can determine about the given predicate.

-> IO (GenericExecutionFeature sym)

checkSatToConsiderBranch :: IsSymInterface sym => sym -> (Pred sym -> IO (SatResult () ())) -> Pred sym -> IO BranchResult

data BranchResult

Result of attempting to branch on a predicate.

Constructors

IndeterminateBranchResult

The both branches of the predicate might be satisfiable (although satisfiablility of either branch is not guaranteed).

NoBranch !Bool

Commit to the branch where the given predicate is equal to the returned boolean. The opposite branch is unsatisfiable (although the given branch is not necessarily satisfiable).

UnsatisfiableContext

The context before considering the given predicate was already unsatisfiable.

Instances

Data BranchResult

Defined in Lang.Crucible.Backend.Online

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BranchResult -> c BranchResult

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BranchResult

toConstr :: BranchResult -> Constr

dataTypeOf :: BranchResult -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BranchResult)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BranchResult)

gmapT :: (forall b. Data b => b -> b) -> BranchResult -> BranchResult

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BranchResult -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BranchResult -> r

gmapQ :: (forall d. Data d => d -> u) -> BranchResult -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BranchResult -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult

Generic BranchResult

Defined in Lang.Crucible.Backend.Online

Associated Types

type Rep BranchResult :: Type -> Type

Methods

from :: BranchResult -> Rep BranchResult x

to :: Rep BranchResult x -> BranchResult

Eq BranchResult

Defined in Lang.Crucible.Backend.Online

Methods

(==) :: BranchResult -> BranchResult -> Bool

(/=) :: BranchResult -> BranchResult -> Bool

Ord BranchResult

Defined in Lang.Crucible.Backend.Online

Methods

compare :: BranchResult -> BranchResult -> Ordering

(<) :: BranchResult -> BranchResult -> Bool

(<=) :: BranchResult -> BranchResult -> Bool

(>) :: BranchResult -> BranchResult -> Bool

(>=) :: BranchResult -> BranchResult -> Bool

max :: BranchResult -> BranchResult -> BranchResult

min :: BranchResult -> BranchResult -> BranchResult

type Rep BranchResult

Defined in Lang.Crucible.Backend.Online

type Rep BranchResult = D1 ('MetaData "BranchResult" "Lang.Crucible.Backend.Online" "crucible-0.7-8cOLouRuT7vG1hxVUUUvCh" 'False) (C1 ('MetaCons "IndeterminateBranchResult" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NoBranch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :+: C1 ('MetaCons "UnsatisfiableContext" 'PrefixI 'False) (U1 :: Type -> Type)))