Concretization

what4/src/What4/Concretize.hs

@@ -0,0 +1,85 @@
+-----------------------------------------------------------------------
+-- |
+-- Module           : What4.Concretize
+-- Description      : Concretize values
+-- Copyright        : (c) Galois, Inc 2024
+-- License          : BSD3
+-- Maintainer       : Langston Barrett <[email protected]>
+-- Stability        : provisional
+-----------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+
+module What4.Concretize
+  ( ConcretizationFailure(..)
+  , concretize
+  ) 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 concrete 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.
+  | MultipleModels
+    -- ^ There are multiple possible models for the expression, which means it
+    -- is truly symbolic and therefore unable to be concretized.
+  deriving Show
+
+-- | Attempt to resolve the given 'WI.SymExpr' to a concrete value using an
+-- online SMT solver connection.
+--
+-- The implementation of this function asks for a model from the solver. If it
+-- gets one, it 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'.
+concretize ::
+  ( 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 ConcretizationFailure (WEG.GroundValue tp))
+concretize sym sp val =
+  case WEG.asGround val of
+    Just gVal -> pure (Right gVal)
+    Nothing -> do
+      WPO.inNewFrame sp $ do
+        -- First, check to see if there is a model of the symbolic value.
+        msat <- WPO.checkAndGetModel sp "Concretize value (with no assumptions)"
+        case msat of
+          WSat.Unknown -> pure $ Left SolverUnknown
+          WSat.Unsat {} -> pure $ Left UnsatInitialAssumptions
+          WSat.Sat mdl -> do
+            concVal <- WEG.groundEval mdl val
+            -- 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 SymBV is /not/ equal to the model we
+            -- found in the previous step. If this is unsatisfiable, the SymBV
+            -- can only be equal to that model, so we can conclude it is
+            -- concrete. If it is satisfiable, on the other hand, the SymBV can
+            -- be multiple values, so it is truly symbolic.
+            WPO.inNewFrame sp $ do
+              injectedConcVal <- WEG.groundToSym sym (WI.exprType val) concVal
+              eq <- WI.isEq sym val injectedConcVal
+              block <- WI.notPred sym eq
+              WPS.assume (WPO.solverConn sp) block
+              msat' <- WPO.checkAndGetModel sp "Concretize value (with blocking clause)"
+              case msat' of
+                WSat.Unknown -> pure $ Left SolverUnknown -- Total failure
+                WSat.Sat _mdl -> pure $ Left MultipleModels  -- There are multiple models
+                WSat.Unsat {} -> pure (Right concVal) -- There is a single concrete result

what4/src/What4/Expr/GroundEval.hs

@@ -24,8 +24,9 @@
 module What4.Expr.GroundEval
   ( -- * Ground evaluation
     GroundValue
-  , GroundValueWrapper(..)
+  , asGround
   , groundToSym
+  , GroundValueWrapper(..)
   , GroundArray(..)
   , lookupArray
   , GroundEvalFn(..)
@@ -84,6 +85,20 @@ type family GroundValue (tp :: BaseType) where
   GroundValue (BaseArrayType idx b) = GroundArray idx b
   GroundValue (BaseStructType ctx)  = Ctx.Assignment GroundValueWrapper ctx
 
+-- | Return a ground representation of a value, if it is ground.
+asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)
+asGround x =
+  case exprType x of
+    BaseBoolRepr       -> asConstantPred x
+    BaseIntegerRepr    -> asInteger x
+    BaseRealRepr       -> asRational x
+    BaseStringRepr _si -> asString x
+    BaseComplexRepr    -> asComplex x
+    BaseBVRepr _w       -> asBV x
+    BaseFloatRepr _fpp  -> asFloat x
+    BaseStructRepr _   -> asStruct x >>= traverseFC (fmap GVW . asGround)
+    BaseArrayRepr _idx _tp -> Nothing
+
 -- | Inject a 'GroundValue' back into a 'SymExpr'.
 --
 -- c.f. 'What4.Interface.concreteToSym'.

what4/src/What4/Interface.hs

@@ -3218,6 +3218,8 @@ asConcrete x =
       pure (ConcreteArray idx c_def Map.empty)
 
 -- | Create a literal symbolic value from a concrete value.
+--
+-- c.f. 'What4.Expr.GroundEval.groundToSym'
 concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp)
 concreteToSym sym = \case
    ConcreteBool True    -> return (truePred sym)

what4/what4.cabal

@@ -147,6 +147,7 @@ library
   exposed-modules:
     What4.BaseTypes
     What4.Concrete
+    What4.Concretize
     What4.Config
     What4.FunctionName
     What4.IndexLit