-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.PathSatisfiability
-- Description      : Support for performing path satisfiability checks
--                    at symbolic branch points
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@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.Lens( (^.) )
import           Control.Monad.Reader
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))
  ]


pathSatisfiabilityFeature :: 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)
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 -> SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeatureResult p sym ext rtp)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend (SimState p sym ext rtp f ('Just args)
st SimState p sym ext rtp f ('Just args)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f ('Just args))
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^. Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp f ('Just args))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext) ((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)
stSimState 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 r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(Maybe ProgramLoc -> f2 (Maybe ProgramLoc))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
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