-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.PathSatisfiability
-- Description      : Support for performing path satisfiability checks
--                    at symbolic branch points
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Ryan Scott <rscott@galois.com>, Langston Barrett <langston@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.PathSatisfiability
  ( checkPathSatisfiability
  , pathSatisfiabilityFeature
  , checkSatToConsiderBranch
  , BranchResult(..)
  ) where

import           Control.Monad.Reader
import           Lens.Micro ((^.))
import qualified Prettyprinter as PP

import           Lang.Crucible.Backend
import           Lang.Crucible.Backend.Online (BranchResult(..))
import           Lang.Crucible.CFG.Core
import           Lang.Crucible.Simulator.ExecutionTree
import           Lang.Crucible.Simulator.EvalStmt
import           Lang.Crucible.Simulator.Operations

import           What4.Concrete
import           What4.Config
import           What4.Interface
import           What4.ProgramLoc
import           What4.SatResult

checkPathSatisfiability :: ConfigOption BaseBoolType
checkPathSatisfiability :: ConfigOption BaseBoolType
checkPathSatisfiability = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"checkPathSat"

pathSatOptions :: [ConfigDesc]
pathSatOptions :: [ConfigDesc]
pathSatOptions =
  [ ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
      ConfigOption BaseBoolType
checkPathSatisfiability
      OptionStyle BaseBoolType
boolOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just (String -> Doc Void
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"Perform path satisfiability checks at symbolic branches"))
      (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
True))
  ]

-- | 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.
pathSatisfiabilityFeature :: forall sym.
  IsSymInterface sym =>
  sym ->
  -- | 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 'Lang.Crucible.Backend.Online.considerSatisfiability'.
  (Maybe ProgramLoc -> Pred sym -> IO BranchResult) ->
  IO (GenericExecutionFeature sym)
pathSatisfiabilityFeature :: forall sym.
IsSymInterface sym =>
sym
-> (Maybe ProgramLoc -> Pred sym -> IO BranchResult)
-> IO (GenericExecutionFeature sym)
pathSatisfiabilityFeature sym
sym Maybe ProgramLoc -> Pred sym -> IO BranchResult
considerSatisfiability =
  do [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
pathSatOptions (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration sym
sym)
     OptionSetting BaseBoolType
pathSatOpt <- IO (OptionSetting BaseBoolType) -> IO (OptionSetting BaseBoolType)
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (OptionSetting BaseBoolType)
 -> IO (OptionSetting BaseBoolType))
-> IO (OptionSetting BaseBoolType)
-> IO (OptionSetting BaseBoolType)
forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
checkPathSatisfiability (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration sym
sym)
     GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GenericExecutionFeature sym -> IO (GenericExecutionFeature sym))
-> GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a b. (a -> b) -> a -> b
$ (forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall sym.
(forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
GenericExecutionFeature ((forall p ext rtp.
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> GenericExecutionFeature sym)
-> (forall p ext rtp.
    (IsSymInterface sym, IsSyntaxExtension ext) =>
    ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall a b. (a -> b) -> a -> b
$ OptionSetting BaseBoolType
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p ext rtp.
OptionSetting BaseBoolType
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep OptionSetting BaseBoolType
pathSatOpt

 where
 onStep ::
   OptionSetting BaseBoolType ->
   ExecState p sym ext rtp ->
   IO (ExecutionFeatureResult p sym ext rtp)

 onStep :: forall p ext rtp.
OptionSetting BaseBoolType
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep OptionSetting BaseBoolType
pathSatOpt (SymbolicBranchState Pred sym
p PausedFrame p sym ext rtp f
tp PausedFrame p sym ext rtp f
fp CrucibleBranchTarget f postdom_args
_tgt SimState p sym ext rtp f ('Just args)
st) =
   OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt OptionSetting BaseBoolType
pathSatOpt IO Bool
-> (Bool -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     Bool
False -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange
     Bool
True ->
       do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
          Maybe ProgramLoc -> Pred sym -> IO BranchResult
considerSatisfiability Maybe ProgramLoc
ploc Pred sym
p IO BranchResult
-> (BranchResult -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               BranchResult
IndeterminateBranchResult ->
                 ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange
               NoBranch Bool
chosen_branch -> SimState p sym ext rtp f ('Just args)
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)) a.
SimState p sym ext rtp f args
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withStateBackend SimState p sym ext rtp f ('Just args)
st ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (ExecutionFeatureResult p sym ext rtp))
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
                 do Pred sym
p' <- if Bool
chosen_branch then Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Pred sym
p else sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
p
                    let frm :: PausedFrame p sym ext rtp f
frm = if Bool
chosen_branch then PausedFrame p sym ext rtp f
tp else PausedFrame p sym ext rtp f
fp
                    bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> Maybe ProgramLoc -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc
-> Maybe ProgramLoc -> e BaseBoolType -> CrucibleAssumption e
BranchCondition ProgramLoc
loc (PausedFrame p sym ext rtp f -> Maybe ProgramLoc
forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> Maybe ProgramLoc
pausedLoc PausedFrame p sym ext rtp f
frm) Pred sym
p')
                    ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNewState (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp)
-> IO (ExecState p sym ext rtp)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  (SimState p sym ext rtp f ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp f ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f
-> ReaderT
     (SimState p sym ext rtp f ('Just args))
     IO
     (ExecState p sym ext rtp)
forall sym p ext rtp f g (ba :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
PausedFrame p sym ext rtp f
-> ValueFromFrame p sym ext rtp f -> ExecCont p sym ext rtp g ba
resumeFrame PausedFrame p sym ext rtp f
frm (ActiveTree p sym ext rtp f ('Just args)
-> ValueFromFrame p sym ext rtp f
forall p sym ext ret f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext ret f args -> ValueFromFrame p sym ext ret f
asContFrame (SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting
     (ActiveTree p sym ext rtp f ('Just args))
     (SimState p sym ext rtp f ('Just args))
     (ActiveTree p sym ext rtp f ('Just args))
-> ActiveTree p sym ext rtp f ('Just args)
forall s a. s -> Getting a s a -> a
^. Getting
  (ActiveTree p sym ext rtp f ('Just args))
  (SimState p sym ext rtp f ('Just args))
  (ActiveTree p sym ext rtp f ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree))) SimState p sym ext rtp f ('Just args)
st
               BranchResult
UnsatisfiableContext ->
                 ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNewState (AbortExecReason
-> SimState p sym ext rtp f ('Just args) -> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f a -> ExecState p sym ext rtp
AbortState (ProgramLoc -> AbortExecReason
InfeasibleBranch ProgramLoc
loc) SimState p sym ext rtp f ('Just args)
st))
   where
     ploc :: Maybe ProgramLoc
ploc = SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting
     (Maybe ProgramLoc)
     (SimState p sym ext rtp f ('Just args))
     (Maybe ProgramLoc)
-> Maybe ProgramLoc
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe ProgramLoc)
  (SimState p sym ext rtp f ('Just args))
  (Maybe ProgramLoc)
forall p sym ext r1 f (a :: Maybe (Ctx CrucibleType)) r2.
Getting r2 (SimState p sym ext r1 f a) (Maybe ProgramLoc)
stateLocation

 onStep OptionSetting BaseBoolType
_ ExecState p sym ext rtp
_ = ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange


checkSatToConsiderBranch ::
  IsSymInterface sym =>
  sym ->
  (Pred sym -> IO (SatResult () ())) ->
  (Pred sym -> IO BranchResult)
checkSatToConsiderBranch :: forall sym.
IsSymInterface sym =>
sym
-> (Pred sym -> IO (SatResult () ()))
-> Pred sym
-> IO BranchResult
checkSatToConsiderBranch sym
sym Pred sym -> IO (SatResult () ())
checkSat Pred sym
p =
  do Pred sym
pnot <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
p
     SatResult () ()
p_res <- Pred sym -> IO (SatResult () ())
checkSat Pred sym
p
     SatResult () ()
pnot_res <- Pred sym -> IO (SatResult () ())
checkSat Pred sym
pnot
     case (SatResult () ()
p_res, SatResult () ()
pnot_res) of
       (Unsat{}, Unsat{}) -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BranchResult
UnsatisfiableContext
       (SatResult () ()
_      , Unsat{}) -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> BranchResult
NoBranch Bool
True)
       (Unsat{}, SatResult () ()
_      ) -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> BranchResult
NoBranch Bool
False)
       (SatResult () (), SatResult () ())
_                  -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BranchResult
IndeterminateBranchResult