content: -----------------------------------------------------------------------
  -- |
  -- 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.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 knownRepr "checkPathSat"
  
  pathSatOptions :: [ConfigDesc]
  pathSatOptions =
    [ mkOpt
        checkPathSatisfiability
        boolOptSty
        (Just (PP.pretty "Perform path satisfiability checks at symbolic branches"))
        (Just (ConcreteBool 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 sym considerSatisfiability =
    do tryExtendConfig pathSatOptions (getConfiguration sym)
       pathSatOpt <- liftIO $ getOptionSetting checkPathSatisfiability (getConfiguration sym)
       return $ GenericExecutionFeature $ onStep pathSatOpt
  
   where
   onStep ::
     OptionSetting BaseBoolType ->
     ExecState p sym ext rtp ->
     IO (ExecutionFeatureResult p sym ext rtp)
  
   onStep pathSatOpt (SymbolicBranchState p tp fp _tgt st) =
     getOpt pathSatOpt >>= \case
       False -> return ExecutionFeatureNoChange
       True ->
         do loc <- getCurrentProgramLoc sym
            considerSatisfiability ploc p >>= \case
                 IndeterminateBranchResult ->
                   return ExecutionFeatureNoChange
                 NoBranch chosen_branch -> withBackend (st ^. stateContext) $ \bak ->
                   do p' <- if chosen_branch then return p else notPred sym p
                      let frm = if chosen_branch then tp else fp
                      addAssumption bak (BranchCondition loc (pausedLoc frm) p')
                      ExecutionFeatureNewState <$> runReaderT (resumeFrame frm (asContFrame (st^.stateTree))) st
                 UnsatisfiableContext ->
                   return (ExecutionFeatureNewState (AbortState (InfeasibleBranch loc) st))
     where
       ploc = st ^. stateLocation
  
   onStep _ _ = return ExecutionFeatureNoChange
  
  
  checkSatToConsiderBranch ::
    IsSymInterface sym =>
    sym ->
    (Pred sym -> IO (SatResult () ())) ->
    (Pred sym -> IO BranchResult)
  checkSatToConsiderBranch sym checkSat p =
    do pnot <- notPred sym p
       p_res <- checkSat p
       pnot_res <- checkSat pnot
       case (p_res, pnot_res) of
         (Unsat{}, Unsat{}) -> return UnsatisfiableContext
         (_      , Unsat{}) -> return (NoBranch True)
         (Unsat{}, _      ) -> return (NoBranch False)
         _                  -> return IndeterminateBranchResult
  