Concretization

[langston-barrett]

The What4.Utils.ResolveBounds.BV.resolveSymBv function can be applied to a symbolic bitvector to (1) check if it is actually only equal to a single value or (2) get upper and lower bounds for it otherwise. There are reasonable use-cases that only require (1), which also has a much more reasonable upper bound on the number of SMT queries it issues.

Furthermore, we can probably easily generalize (1) to other base types. Here's the code:

what4/what4/src/What4/Utils/ResolveBounds/BV.hs

Lines 109 to 136 in 30309b5

	-- First check, if the SymBV can be trivially resolved as concrete. If so,
	-- this can avoid the need to call out to the solver at all.
	case WI.asBV symBV of
	Just bv -> pure $ BVConcrete bv
	-- Otherwise, we need to consult the solver.
	Nothing -> do
	-- First, ask for a particular model of the SymBV...
	modelForBV <- WPO.inNewFrame proc $ do
	msat <- WPO.checkAndGetModel proc "resolveSymBV (check with initial assumptions)"
	model <- case msat of
	WSat.Unknown -> failUnknown
	WSat.Unsat{} -> fail "resolveSymBV: Initial assumptions are unsatisfiable"
	WSat.Sat model -> pure model
	WEG.groundEval model symBV
	-- ...next, check if this is the only possible model for this SymBV. 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.
	isSymbolic <- WPO.inNewFrame proc $ do
	block <- WI.notPred sym =<< WI.bvEq sym symBV =<< WI.bvLit sym w modelForBV
	WPS.assume conn block
	msat <- WPO.check proc "resolveSymBV (check under assumption that model cannot happen)"
	case msat of
	WSat.Unknown -> failUnknown
	WSat.Sat{} -> pure True -- Truly symbolic
	WSat.Unsat{} -> pure False -- Concrete

To generalize, we can replace:

• asBV -> asConcrete
• bvLit -> concreteToSym
• bvEq -> isEq

In summary, it'd be nice to write a function with the signature

-- | Use an 'WPO.OnlineSolver' to attempt to resolve a 'WI.SymExpr' as concrete.
concretize ::
     forall w sym solver scope st fs
   . ( 1 PN.<= w
     , sym ~ WEB.ExprBuilder scope st fs
     , WPO.OnlineSolver solver
     )
  => sym
  -> WPO.SolverProcess scope solver
     -- ^ The online solver process to use to search for lower and upper
     --   bounds.
  -> WI.SymExpr tp
     -- ^ The expression to concretize.
  -> IO (Maybe (ConcreteVal tp))

and use it in the implementation of resolveSymBv.

[RyanGlScott]

See also the Concretize machinery in Data.Macaw.Symbolic.Concretize, which attempts to provide a more generic concretization interface akin to what you describe above as (1). (Despite living in macaw-symbolic, none of the code in that module is Macaw-specific.)

[langston-barrett]

See also Pate.Verification.Concretize