From 494ac6416ed01eab6ae5d1be427d0aaae4c4bb91 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Fri, 7 Jun 2024 10:02:01 -0400
Subject: [PATCH] Inject ground values back into symbolic expressions (#268)

---
 what4/src/What4/Expr/GroundEval.hs | 36 ++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/what4/src/What4/Expr/GroundEval.hs b/what4/src/What4/Expr/GroundEval.hs
index 9209c485..4179cd77 100644
--- a/what4/src/What4/Expr/GroundEval.hs
+++ b/what4/src/What4/Expr/GroundEval.hs
@@ -25,6 +25,7 @@ module What4.Expr.GroundEval
   ( -- * Ground evaluation
     GroundValue
   , GroundValueWrapper(..)
+  , groundToSym
   , GroundArray(..)
   , lookupArray
   , GroundEvalFn(..)
@@ -83,6 +84,41 @@ type family GroundValue (tp :: BaseType) where
   GroundValue (BaseArrayType idx b) = GroundArray idx b
   GroundValue (BaseStructType ctx)  = Ctx.Assignment GroundValueWrapper ctx
 
+-- | Inject a 'GroundValue' back into a '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 -> do
+          def' <- groundToSym sym tpr' def
+          arr <- constantArray sym idxTy def'
+          go (Map.toAscList xs0) arr
+        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.