Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Ryan Scott <rscott@galois.com>, Langston Barrett <langston@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Simulator.PathSatisfiability

Description

Synopsis

checkPathSatisfiability :: ConfigOption BaseBoolType
pathSatisfiabilityFeature :: IsSymInterface sym => sym -> (Maybe ProgramLoc -> Pred sym -> IO BranchResult) -> IO (GenericExecutionFeature sym)
checkSatToConsiderBranch :: IsSymInterface sym => sym -> (Pred sym -> IO (SatResult () ())) -> Pred sym -> IO BranchResult
data BranchResult

Documentation

checkPathSatisfiability :: ConfigOption BaseBoolType Source #

pathSatisfiabilityFeature Source #

Arguments

:: 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. Usually, this is set to `considerSatisfiability`.
-> IO (GenericExecutionFeature sym)

Prune unsatisfiable execution traces during simulation.

At every symbolic branch point, an SMT solver is queried to determine if one or both symbolic branches are unsatisfiable. Only branches with satisfiable branch conditions are explored.

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

data BranchResult Source #

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

Instances details

Data BranchResult Source #

Instance details

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 Source #

Instance details

Defined in Lang.Crucible.Backend.Online

Associated Types

type Rep BranchResult

Instance details

Defined in Lang.Crucible.Backend.Online

type Rep BranchResult = D1 ('MetaData "BranchResult" "Lang.Crucible.Backend.Online" "crucible-0.8.0.0-4NPuSrI5sD835MFtwnvz2a" '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)))

Methods

from :: BranchResult -> Rep BranchResult x #

to :: Rep BranchResult x -> BranchResult #

Eq BranchResult Source #

Instance details

Defined in Lang.Crucible.Backend.Online

Methods

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

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

Ord BranchResult Source #

Instance details

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 Source #

Instance details

Defined in Lang.Crucible.Backend.Online

type Rep BranchResult = D1 ('MetaData "BranchResult" "Lang.Crucible.Backend.Online" "crucible-0.8.0.0-4NPuSrI5sD835MFtwnvz2a" '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)))