From 939b3a3a159a4e27824a1396e3de9abe640154a0 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 24 May 2024 11:47:17 -0400 Subject: [PATCH] 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 | 23 ++++++++ what4/src/What4/Concretize.hs | 95 ++++++++++++++++++++++++++++++ what4/src/What4/Expr/GroundEval.hs | 87 +++++++++++++++++++++++++++ what4/src/What4/Interface.hs | 2 + what4/what4.cabal | 1 + 5 files changed, 208 insertions(+) create mode 100644 what4/src/What4/Concretize.hs diff --git a/what4/src/What4/Concrete.hs b/what4/src/What4/Concrete.hs index e9f53215..5e71dfcf 100644 --- a/what4/src/What4/Concrete.hs +++ b/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 diff --git a/what4/src/What4/Concretize.hs b/what4/src/What4/Concretize.hs new file mode 100644 index 00000000..3ad5b332 --- /dev/null +++ b/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 +-- 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 diff --git a/what4/src/What4/Expr/GroundEval.hs b/what4/src/What4/Expr/GroundEval.hs index 9209c485..9af5b8c4 100644 --- a/what4/src/What4/Expr/GroundEval.hs +++ b/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. diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs index 9b3a5299..1e73c199 100644 --- a/what4/src/What4/Interface.hs +++ b/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) diff --git a/what4/what4.cabal b/what4/what4.cabal index 543ee2ab..62bc2abc 100644 --- a/what4/what4.cabal +++ b/what4/what4.cabal @@ -147,6 +147,7 @@ library exposed-modules: What4.BaseTypes What4.Concrete + What4.Concretize What4.Config What4.FunctionName What4.IndexLit