Inject concrete values back into symbolic expressions

crucible/src/Lang/Crucible/Concretize.hs

@@ -37,6 +37,9 @@ module Lang.Crucible.Concretize
   , concRegValue
   , concRegEntry
   , concRegMap
+    -- * There and back again
+  , IntrinsicConcToSymFn
+  , concToSym
   ) where
 
 import           Data.Kind (Type)
@@ -100,7 +103,7 @@ type family ConcRegValue sym tp where
   ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx
   ConcRegValue sym (ReferenceType tp) = [RefCell tp]
   ConcRegValue sym (WordMapType w tp) = ()  -- TODO: possible to do something meaningful?
-  ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx)
+  ConcRegValue sym (RecursiveType nm ctx) = (ConcRegValue sym (UnrollType nm ctx))
   ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx
   ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp)
 
@@ -429,3 +432,129 @@ concRegMap ::
   RegMap sym tps ->
   IO (Ctx.Assignment (ConcRV' sym) tps)
 concRegMap ctx (RM.RegMap m) = traverseFC (fmap ConcRV' . concRegEntry ctx) m
+
+---------------------------------------------------------------------
+-- * concToSym
+
+-- | Function for re-symbolizing an intrinsic type
+type IntrinsicConcToSymFn :: Symbol -> Type
+newtype IntrinsicConcToSymFn nm
+  = IntrinsicConcToSymFn
+    (forall sym ctx.
+      W4I.IsExprBuilder sym =>
+      sym ->
+      Ctx.Assignment TypeRepr ctx ->
+      ConcIntrinsic nm ctx ->
+      IO (RegValue sym (IntrinsicType nm ctx)))
+
+-- | Helper, not exported
+concToSymAny ::
+  W4I.IsExprBuilder sym =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  ConcRegValue sym AnyType ->
+  IO (RegValue sym AnyType)
+concToSymAny sym iFns (ConcAnyValue tp' (ConcRV' v')) =
+  RV.AnyValue tp' <$> concToSym sym iFns tp' v'
+
+-- | Helper, not exported
+concToSymFn ::
+  W4I.IsExprBuilder sym =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  Ctx.Assignment (TypeRepr) as ->
+  TypeRepr r ->
+  ConcRegValue sym (FunctionHandleType as r) ->
+  IO (RegValue sym (FunctionHandleType as r))
+concToSymFn sym iFns as r f =
+  case f of
+    ConcClosureFnVal clos vtp (ConcRV' v) -> do
+      v' <- concToSym sym iFns vtp v
+      clos' <- concToSymFn sym iFns (as Ctx.:> vtp) r clos
+      pure (RV.ClosureFnVal clos' vtp v')
+
+    ConcVarargsFnVal hdl extra ->
+      pure (RV.VarargsFnVal hdl extra)
+
+    ConcHandleFnVal hdl ->
+      pure (RV.HandleFnVal hdl)
+
+-- | Helper, not exported
+concToSymIntrinsic ::
+  W4I.IsExprBuilder sym =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  SymbolRepr nm ->
+  CtxRepr ctx ->
+  ConcRegValue sym (IntrinsicType nm ctx) ->
+  IO (RegValue sym (IntrinsicType nm ctx))
+concToSymIntrinsic sym iFns nm tyCtx v =
+  case MapF.lookup nm iFns of
+    Nothing -> 
+      let strNm = Text.unpack (symbolRepr nm) in
+      fail ("Missing concretization function for intrinsic: " ++ strNm)
+    Just (IntrinsicConcToSymFn f) -> f sym tyCtx v
+
+-- | Helper, not exported
+concToSymMaybe ::
+  W4I.IsExprBuilder sym =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  TypeRepr tp ->
+  ConcRegValue sym (MaybeType tp) ->
+  IO (RegValue sym (MaybeType tp))
+concToSymMaybe sym iFns tp =
+  \case
+    Nothing -> pure (W4P.Err ())
+    Just v ->
+      W4P.NoErr . W4P.Partial (W4I.truePred sym) <$> concToSym sym iFns tp v
+
+-- | Helper, not exported
+concToSym :: 
+  W4I.IsExprBuilder sym =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  TypeRepr tp ->
+  ConcRegValue sym tp ->
+  IO (RegValue sym tp)
+concToSym sym iFns tp v =
+  case tp of
+    -- Base types
+    BoolRepr -> W4GE.groundToSym sym BaseBoolRepr v
+    BVRepr width -> W4GE.groundToSym sym (BaseBVRepr width) v
+    ComplexRealRepr -> W4GE.groundToSym sym BaseComplexRepr v
+    FloatRepr _ -> fail "TODO"
+    IEEEFloatRepr fpp -> W4GE.groundToSym sym (BaseFloatRepr fpp) v
+    IntegerRepr -> W4GE.groundToSym sym BaseIntegerRepr v
+    NatRepr -> W4I.integerToNat sym =<< W4GE.groundToSym sym BaseIntegerRepr v
+    RealValRepr -> W4GE.groundToSym sym BaseRealRepr v
+    StringRepr si -> W4GE.groundToSym sym (BaseStringRepr si) v
+    SymbolicArrayRepr idxs tp' -> W4GE.groundToSym sym (BaseArrayRepr idxs tp') v
+    SymbolicStructRepr tys -> W4GE.groundToSym sym (BaseStructRepr tys) v
+
+    -- Trivial cases
+    UnitRepr -> pure ()
+    CharRepr -> pure v
+
+    -- Simple recursive cases
+    RecursiveRepr symb tyCtx ->
+      RV.RolledType <$> concToSym sym iFns (unrollType symb tyCtx) v
+    StructRepr tps ->
+      Ctx.zipWithM (\tp' (ConcRV' v') -> RV.RV <$> concToSym sym iFns tp' v') tps v
+    VectorRepr tp' ->
+      traverse (concToSym sym iFns tp' . unConcRV') v
+
+    -- Cases with helper functions
+    AnyRepr -> concToSymAny sym iFns v
+    MaybeRepr tp' -> concToSymMaybe sym iFns tp' v
+    FunctionHandleRepr args ret -> concToSymFn sym iFns args ret v
+    IntrinsicRepr nm tyCtx -> concToSymIntrinsic sym iFns nm tyCtx v
+    -- ReferenceRepr _ -> _
+    -- SequenceRepr tp' -> _
+    -- StringMapRepr tp' -> _
+    -- VariantRepr tps -> _
+
+    -- -- Incomplete cases
+    -- WordMapRepr _ _ -> _
+
+