Concretization: Resolve a symbolic expression to a concrete value

This feature consults the SMT solver determine whether a symbolic
expression must be equal to a particular concrete expression.

This is used in Macaw to concretize pointers to global data, but is
generally useful.

what4/src/What4/Concrete.hs

@@ -44,6 +44,9 @@ module What4.Concrete
   , fromConcreteString
   , fromConcreteBV
   , fromConcreteComplex
+
+  , fromIndexLit
+  , toIndexLit
   ) where
 
 import qualified Data.List as List
@@ -61,6 +64,7 @@ import           Data.Parameterized.TH.GADT
 import           Data.Parameterized.TraversableFC
 
 import           What4.BaseTypes
+import           What4.IndexLit
 import           What4.Utils.Complex
 import           What4.Utils.StringLiteral
 
@@ -118,6 +122,25 @@ concreteType = \case
   ConcreteStruct xs         -> BaseStructRepr (fmapFC concreteType xs)
   ConcreteArray idxTy def _ -> BaseArrayRepr idxTy (concreteType def)
 
+fromIndexLit :: IndexLit tp -> ConcreteVal tp
+fromIndexLit =
+  \case
+    IntIndexLit i -> ConcreteInteger i
+    BVIndexLit w bv -> ConcreteBV w bv
+
+toIndexLit :: ConcreteVal tp -> Maybe (IndexLit tp)
+toIndexLit = \case
+  ConcreteInteger i         -> Just (IntIndexLit i)
+  ConcreteBV w bv           -> Just (BVIndexLit w bv)
+  -- Explicitly match all constructors to get a warning if we add one
+  ConcreteBool{}            -> Nothing
+  ConcreteReal{}            -> Nothing
+  ConcreteFloat{}           -> Nothing
+  ConcreteString{}          -> Nothing
+  ConcreteComplex{}         -> Nothing
+  ConcreteStruct{}          -> Nothing
+  ConcreteArray{}           -> Nothing
+
 $(return [])
 
 instance TestEquality ConcreteVal where

what4/src/What4/Concretize.hs

@@ -0,0 +1,95 @@
+-----------------------------------------------------------------------
+-- |
+-- 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 Control.Monad (forM)
+
+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
+  = ConversionError
+    -- ^ 'WEG.fromConcrete' failed
+  | 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 WI.asConcrete val of
+    Just val' ->
+      case WEG.fromConcrete val' of
+        Just val'' -> pure (Right val'')
+        Nothing -> pure (Left ConversionError)
+    Nothing -> do
+      -- First, check to see if there is a model of the symbolic value.
+      res <- WPO.inNewFrame sp $ do
+        msat <- WPO.checkAndGetModel sp "Concretize value (with no assumptions)"
+        mmodel <- case msat of
+          WSat.Unknown -> pure $ Left SolverUnknown
+          WSat.Unsat {} -> pure $ Left UnsatInitialAssumptions
+          WSat.Sat mdl -> pure $ Right mdl
+        forM mmodel $ \mdl -> WEG.groundEval mdl val
+      case res of
+        Left _failure -> pure res -- We failed to get a model
+        Right 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 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 res -- There is a single concrete result

what4/src/What4/Expr/GroundEval.hs

@@ -24,6 +24,9 @@
 module What4.Expr.GroundEval
   ( -- * Ground evaluation
     GroundValue
+  , fromConcrete
+  , toConcrete
+  , groundToSym
   , GroundValueWrapper(..)
   , GroundArray(..)
   , lookupArray
@@ -56,6 +59,7 @@ import           LibBF (BigFloat)
 import qualified LibBF as BF
 
 import           What4.BaseTypes
+import           What4.Concrete (ConcreteVal(..), fromIndexLit, toIndexLit)
 import           What4.Interface
 import qualified What4.SemiRing as SR
 import qualified What4.SpecialFunctions as SFn
@@ -70,6 +74,7 @@ import           What4.Utils.Arithmetic ( roundAway )
 import           What4.Utils.Complex
 import           What4.Utils.FloatHelpers
 import           What4.Utils.StringLiteral
+import Data.Functor.Product (Product(Pair))
 
 
 type family GroundValue (tp :: BaseType) where
@@ -83,6 +88,88 @@ type family GroundValue (tp :: BaseType) where
   GroundValue (BaseArrayType idx b) = GroundArray idx b
   GroundValue (BaseStructType ctx)  = Ctx.Assignment GroundValueWrapper ctx
 
+-- | Convert a 'ConcreteVal' into a 'GroundValue'
+--
+-- May fail if the 'ConcreteVal' contains ill-typed array indices.
+fromConcrete :: ConcreteVal tp -> Maybe (GroundValue tp)
+fromConcrete =
+  \case
+    ConcreteBool b -> Just b
+    ConcreteInteger i -> Just i
+    ConcreteReal r -> Just r
+    ConcreteFloat _fpp bf -> Just bf
+    ConcreteString  s -> Just s
+    ConcreteComplex c -> Just c
+    ConcreteBV _w bv -> Just bv
+    ConcreteStruct fs -> traverseFC (fmap GVW . fromConcrete) fs
+    ConcreteArray _idxTys def upds ->
+      let upds' =
+            fmap Map.fromList $
+              traverse (\(idxs, val) -> (,) <$> traverseFC toIndexLit idxs <*> fromConcrete val) $
+              Map.toList upds
+      in ArrayConcrete <$> fromConcrete def <*> upds'
+
+-- | Convert a 'GroundValue' to a 'ConcreteVal'
+--
+-- Fails on 'ArrayMapping'.
+toConcrete :: BaseTypeRepr tp -> GroundValue tp -> Maybe (ConcreteVal tp)
+toConcrete tpr val =
+  case tpr of
+    BaseBoolRepr -> Just (ConcreteBool val)
+    BaseIntegerRepr -> Just (ConcreteInteger val)
+    BaseRealRepr -> Just (ConcreteReal val)
+    BaseFloatRepr fpp -> Just (ConcreteFloat fpp val)
+    BaseStringRepr {} -> Just (ConcreteString val)
+    BaseComplexRepr -> Just (ConcreteComplex val)
+    BaseBVRepr w -> Just (ConcreteBV w val)
+    BaseStructRepr xs ->
+      ConcreteStruct <$>
+        traverseFC
+          (\(Pair tpr' (GVW gv)) -> toConcrete tpr' gv)
+          (Ctx.zipWith Pair xs val)
+    BaseArrayRepr idxTys ty ->
+      case val of
+        ArrayMapping {} -> Nothing
+        ArrayConcrete def upds ->
+          ConcreteArray idxTys
+          <$> toConcrete ty def
+          <*> (fmap Map.fromList $
+                (traverse (\(idxs, gval) -> (,) <$> pure (fmapFC fromIndexLit idxs) <*> toConcrete ty gval) $
+                Map.toList upds))
+
+-- | Inject 'GroundValue' back into 'SymExpr'
+--
+-- c.f. 'What4.Interface.concreteToSym'.
+groundToSym ::
+  IsExprBuilder sym =>
+  sym ->
+  BaseTypeRepr tp ->
+  GroundValue tp ->
+  IO (SymExpr sym tp)
+groundToSym sym tpr val =
+  case tpr of
+    BaseBoolRepr -> pure (if val then truePred sym else falsePred sym)
+    BaseBVRepr w -> bvLit sym w val
+    BaseIntegerRepr -> intLit sym val
+    BaseRealRepr -> realLit sym val
+    BaseFloatRepr fpp -> floatLit sym fpp val
+    BaseStringRepr _ -> stringLit sym val
+    BaseComplexRepr -> mkComplexLit sym val
+    BaseStructRepr tps ->
+      mkStruct sym =<< Ctx.zipWithM (\tp (GVW gv) -> groundToSym  sym tp gv) tps val
+    BaseArrayRepr idxTy tpr' ->
+      case val of
+        ArrayConcrete def xs0 ->
+          go (Map.toAscList xs0) =<< constantArray sym idxTy =<< groundToSym sym tpr' def
+        ArrayMapping _ -> fail "Can't evaluate `groundToSym` on `ArrayMapping`"
+      where
+      go [] arr = return arr
+      go ((i, x) : xs) arr =
+        do arr' <- go xs arr
+           i' <- traverseFC (indexLit sym) i
+           x' <- groundToSym sym tpr' x
+           arrayUpdate sym arr' i' x'
+
 -- | A function that calculates ground values for elements.
 --   Clients of solvers should use the @groundEval@ function for computing
 --   values in models.

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