-----------------------------------------------------------------------
-- |
-- Module           : What4.Concretize
-- Description      : Concretize values
-- Copyright        : (c) Galois, Inc 2024
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
--
-- In our terminology, concretization is the process of (1) obtaining a
-- model from an SMT solver and (2) requesting the value of a particular set
-- of symbolic expressions in said model. The operation (2) alone is called
-- "grounding", see "What4.GroundEval".
-----------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

module What4.Concretize
  ( ConcretizationFailure(..)
  , concretize
  , UniqueConcretizationFailure(..)
  , uniquelyConcretize
  ) where

import qualified What4.Expr.Builder as WEB
import qualified What4.Expr.GroundEval as WEG
import qualified What4.Interface as WI
import qualified What4.Protocol.Online as WPO
import qualified What4.Protocol.SMTWriter as WPS
import qualified What4.SatResult as WSat

-- | Reasons why attempting to resolve a symbolic expression as ground can fail.
data ConcretizationFailure
  = SolverUnknown
    -- ^ Querying the SMT solver yielded @UNKNOWN@.
  | UnsatInitialAssumptions
    -- ^ Querying the SMT solver for an initial model of the expression failed
    -- due to the initial assumptions in scope being unsatisfiable.
  deriving Int -> ConcretizationFailure -> ShowS
[ConcretizationFailure] -> ShowS
ConcretizationFailure -> String
(Int -> ConcretizationFailure -> ShowS)
-> (ConcretizationFailure -> String)
-> ([ConcretizationFailure] -> ShowS)
-> Show ConcretizationFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConcretizationFailure -> ShowS
showsPrec :: Int -> ConcretizationFailure -> ShowS
$cshow :: ConcretizationFailure -> String
show :: ConcretizationFailure -> String
$cshowList :: [ConcretizationFailure] -> ShowS
showList :: [ConcretizationFailure] -> ShowS
Show

-- | Get a 'WEG.GroundValue' for a 'WI.SymExpr' by asking an online solver for
-- a model.
--
-- In contrast with 'uniquelyConcretize', this function returns the value of the
-- 'WI.SymExpr' in just one of potentially many distinct models. See the Haddock
-- on 'uniquelyConcretize' for a further comparison.
concretize ::
  ( sym ~ WEB.ExprBuilder scope st fs
  , WPO.OnlineSolver solver
  ) =>
  WPO.SolverProcess scope solver ->
  -- | The symbolic term to query from the model
  WI.SymExpr sym tp ->
  IO (Either ConcretizationFailure (WEG.GroundValue tp))
concretize :: forall sym scope (st :: Type -> Type) fs solver (tp :: BaseType).
(sym ~ ExprBuilder scope st fs, OnlineSolver solver) =>
SolverProcess scope solver
-> SymExpr sym tp
-> IO (Either ConcretizationFailure (GroundValue tp))
concretize SolverProcess scope solver
sp SymExpr sym tp
val =
  case Expr scope tp -> Maybe (GroundValue tp)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> Maybe (GroundValue tp)
WEG.asGround SymExpr sym tp
Expr scope tp
val of
    Just GroundValue tp
gVal -> Either ConcretizationFailure (GroundValue tp)
-> IO (Either ConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundValue tp -> Either ConcretizationFailure (GroundValue tp)
forall a b. b -> Either a b
Right GroundValue tp
gVal)
    Maybe (GroundValue tp)
Nothing -> do
      SolverProcess scope solver
-> IO (Either ConcretizationFailure (GroundValue tp))
-> IO (Either ConcretizationFailure (GroundValue tp))
forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
WPO.inNewFrame SolverProcess scope solver
sp (IO (Either ConcretizationFailure (GroundValue tp))
 -> IO (Either ConcretizationFailure (GroundValue tp)))
-> IO (Either ConcretizationFailure (GroundValue tp))
-> IO (Either ConcretizationFailure (GroundValue tp))
forall a b. (a -> b) -> a -> b
$ do
        SatResult (GroundEvalFn scope) ()
msat <- SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
WPO.checkAndGetModel SolverProcess scope solver
sp String
"Ground value using model"
        case SatResult (GroundEvalFn scope) ()
msat of
          SatResult (GroundEvalFn scope) ()
WSat.Unknown -> Either ConcretizationFailure (GroundValue tp)
-> IO (Either ConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either ConcretizationFailure (GroundValue tp)
 -> IO (Either ConcretizationFailure (GroundValue tp)))
-> Either ConcretizationFailure (GroundValue tp)
-> IO (Either ConcretizationFailure (GroundValue tp))
forall a b. (a -> b) -> a -> b
$ ConcretizationFailure
-> Either ConcretizationFailure (GroundValue tp)
forall a b. a -> Either a b
Left ConcretizationFailure
SolverUnknown
          WSat.Unsat {} -> Either ConcretizationFailure (GroundValue tp)
-> IO (Either ConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either ConcretizationFailure (GroundValue tp)
 -> IO (Either ConcretizationFailure (GroundValue tp)))
-> Either ConcretizationFailure (GroundValue tp)
-> IO (Either ConcretizationFailure (GroundValue tp))
forall a b. (a -> b) -> a -> b
$ ConcretizationFailure
-> Either ConcretizationFailure (GroundValue tp)
forall a b. a -> Either a b
Left ConcretizationFailure
UnsatInitialAssumptions
          WSat.Sat GroundEvalFn scope
mdl -> GroundValue tp -> Either ConcretizationFailure (GroundValue tp)
forall a b. b -> Either a b
Right (GroundValue tp -> Either ConcretizationFailure (GroundValue tp))
-> IO (GroundValue tp)
-> IO (Either ConcretizationFailure (GroundValue tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GroundEvalFn scope
-> forall (tp :: BaseType). Expr scope tp -> IO (GroundValue tp)
forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WEG.groundEval GroundEvalFn scope
mdl SymExpr sym tp
Expr scope tp
val

data UniqueConcretizationFailure
  = GroundingFailure ConcretizationFailure
  | MultipleModels
    -- ^ There are multiple possible models for the expression, which means it
    -- is truly symbolic and therefore unable to be uniquely concretized.
  deriving Int -> UniqueConcretizationFailure -> ShowS
[UniqueConcretizationFailure] -> ShowS
UniqueConcretizationFailure -> String
(Int -> UniqueConcretizationFailure -> ShowS)
-> (UniqueConcretizationFailure -> String)
-> ([UniqueConcretizationFailure] -> ShowS)
-> Show UniqueConcretizationFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UniqueConcretizationFailure -> ShowS
showsPrec :: Int -> UniqueConcretizationFailure -> ShowS
$cshow :: UniqueConcretizationFailure -> String
show :: UniqueConcretizationFailure -> String
$cshowList :: [UniqueConcretizationFailure] -> ShowS
showList :: [UniqueConcretizationFailure] -> ShowS
Show

-- | Attempt to resolve the given 'WI.SymExpr' to a unique concrete value using
-- an online SMT solver connection.
--
-- The implementation of this function (1) asks for a model from the solver.
-- If it gets one, it (2) adds a blocking clause and asks for another. If there
-- was only one model, concretize the initial value and return it with 'Right'.
-- Otherwise, return an explanation of why concretization failed with 'Left'.
-- This behavior is contrasted with 'concretize', which just does (1).
uniquelyConcretize ::
  ( sym ~ WEB.ExprBuilder scope st fs
  , WPO.OnlineSolver solver
  ) =>
  -- | The symbolic backend
  sym ->
  WPO.SolverProcess scope solver ->
  -- | The symbolic term to concretize
  WI.SymExpr sym tp ->
  IO (Either UniqueConcretizationFailure (WEG.GroundValue tp))
uniquelyConcretize :: forall sym scope (st :: Type -> Type) fs solver (tp :: BaseType).
(sym ~ ExprBuilder scope st fs, OnlineSolver solver) =>
sym
-> SolverProcess scope solver
-> SymExpr sym tp
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
uniquelyConcretize sym
sym SolverProcess scope solver
sp SymExpr sym tp
val =
  case Expr scope tp -> Maybe (GroundValue tp)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> Maybe (GroundValue tp)
WEG.asGround SymExpr sym tp
Expr scope tp
val of
    Just GroundValue tp
gVal -> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (GroundValue tp
-> Either UniqueConcretizationFailure (GroundValue tp)
forall a b. b -> Either a b
Right GroundValue tp
gVal)
    Maybe (GroundValue tp)
Nothing -> do
      -- First, check to see if there is a model of the symbolic value.
      Either ConcretizationFailure (GroundValue tp)
concVal_ <- SolverProcess scope solver
-> SymExpr (ExprBuilder scope Any Any) tp
-> IO (Either ConcretizationFailure (GroundValue tp))
forall sym scope (st :: Type -> Type) fs solver (tp :: BaseType).
(sym ~ ExprBuilder scope st fs, OnlineSolver solver) =>
SolverProcess scope solver
-> SymExpr sym tp
-> IO (Either ConcretizationFailure (GroundValue tp))
concretize SolverProcess scope solver
sp SymExpr sym tp
SymExpr (ExprBuilder scope Any Any) tp
val
      case Either ConcretizationFailure (GroundValue tp)
concVal_ of
        Left ConcretizationFailure
e -> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (UniqueConcretizationFailure
-> Either UniqueConcretizationFailure (GroundValue tp)
forall a b. a -> Either a b
Left (ConcretizationFailure -> UniqueConcretizationFailure
GroundingFailure ConcretizationFailure
e))
        Right GroundValue tp
concVal -> do
          -- We found a model, so check to see if this is the only possible
          -- model for this symbolic value.  We do this by adding a blocking
          -- clause that assumes the `SymExpr` is /not/ equal to the model we
          -- found in the previous step. If this is unsatisfiable, the SymExpr
          -- can only be equal to that model, so we can conclude it is concrete.
          -- If it is satisfiable, on the other hand, the `SymExpr` can be
          -- multiple values, so it is truly symbolic.
          SolverProcess scope solver
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
WPO.inNewFrame SolverProcess scope solver
sp (IO (Either UniqueConcretizationFailure (GroundValue tp))
 -> IO (Either UniqueConcretizationFailure (GroundValue tp)))
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a b. (a -> b) -> a -> b
$ do
            Expr scope tp
injectedConcVal <- sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
WEG.groundToSym sym
sym (Expr scope tp -> BaseTypeRepr tp
forall (tp :: BaseType). Expr scope tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
WI.exprType SymExpr sym tp
Expr scope tp
val) GroundValue tp
concVal
            Expr scope BaseBoolType
eq <- sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
WI.isEq sym
sym SymExpr sym tp
val SymExpr sym tp
Expr scope tp
injectedConcVal
            Expr scope BaseBoolType
block <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym Pred sym
Expr scope BaseBoolType
eq
            WriterConn scope solver -> Expr scope BaseBoolType -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
WPS.assume (SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
WPO.solverConn SolverProcess scope solver
sp) Expr scope BaseBoolType
block
            SatResult (GroundEvalFn scope) ()
msat' <- SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
WPO.checkAndGetModel SolverProcess scope solver
sp String
"Concretize value (with blocking clause)"
            case SatResult (GroundEvalFn scope) ()
msat' of
              SatResult (GroundEvalFn scope) ()
WSat.Unknown -> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either UniqueConcretizationFailure (GroundValue tp)
 -> IO (Either UniqueConcretizationFailure (GroundValue tp)))
-> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a b. (a -> b) -> a -> b
$ UniqueConcretizationFailure
-> Either UniqueConcretizationFailure (GroundValue tp)
forall a b. a -> Either a b
Left (UniqueConcretizationFailure
 -> Either UniqueConcretizationFailure (GroundValue tp))
-> UniqueConcretizationFailure
-> Either UniqueConcretizationFailure (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ ConcretizationFailure -> UniqueConcretizationFailure
GroundingFailure (ConcretizationFailure -> UniqueConcretizationFailure)
-> ConcretizationFailure -> UniqueConcretizationFailure
forall a b. (a -> b) -> a -> b
$ ConcretizationFailure
SolverUnknown
              WSat.Sat GroundEvalFn scope
_mdl -> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either UniqueConcretizationFailure (GroundValue tp)
 -> IO (Either UniqueConcretizationFailure (GroundValue tp)))
-> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a b. (a -> b) -> a -> b
$ UniqueConcretizationFailure
-> Either UniqueConcretizationFailure (GroundValue tp)
forall a b. a -> Either a b
Left (UniqueConcretizationFailure
 -> Either UniqueConcretizationFailure (GroundValue tp))
-> UniqueConcretizationFailure
-> Either UniqueConcretizationFailure (GroundValue tp)
forall a b. (a -> b) -> a -> b
$ UniqueConcretizationFailure
MultipleModels
              WSat.Unsat {} -> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either UniqueConcretizationFailure (GroundValue tp)
 -> IO (Either UniqueConcretizationFailure (GroundValue tp)))
-> Either UniqueConcretizationFailure (GroundValue tp)
-> IO (Either UniqueConcretizationFailure (GroundValue tp))
forall a b. (a -> b) -> a -> b
$ GroundValue tp
-> Either UniqueConcretizationFailure (GroundValue tp)
forall a b. b -> Either a b
Right GroundValue tp
concVal -- There is a single concrete result