Inject concrete values back into symbolic expressions

crucible/src/Lang/Crucible/Concretize.hs

@@ -37,9 +37,14 @@ module Lang.Crucible.Concretize
   , concRegValue
   , concRegEntry
   , concRegMap
+    -- * There and back again
+  , IntrinsicConcToSymFn(..)
+  , concToSym
   ) where
 
 import           Data.Kind (Type)
+import           Data.List.NonEmpty (NonEmpty)
+import qualified Data.List.NonEmpty as NE
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Text (Text)
@@ -98,9 +103,9 @@ type family ConcRegValue sym tp where
   ConcRegValue sym (SequenceType tp) = [ConcRV' sym tp]
   ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRV' sym) ctx
   ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx
-  ConcRegValue sym (ReferenceType tp) = [RefCell tp]
+  ConcRegValue sym (ReferenceType tp) = NonEmpty (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)
 
@@ -268,8 +273,14 @@ concMux ::
   W4I.IsExprBuilder sym =>
   ConcCtx sym t ->
   MuxTree.MuxTree sym a ->
-  IO [a]
-concMux ctx = go . MuxTree.viewMuxTree
+  IO (NonEmpty a)
+concMux ctx mt = do
+  l <- go (MuxTree.viewMuxTree mt)
+  case NE.nonEmpty l of
+    -- This is impossible because the only way to make a MuxTree is with
+    -- `toMuxTree`, which uses `truePred`.
+    Nothing -> fail "Impossible: Mux tree had no feasible branches?"
+    Just ne -> pure ne
   where
     go [] = pure []
     go ((val, p):xs) = do
@@ -429,3 +440,155 @@ 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.justPartExpr sym <$> concToSym sym iFns tp v
+
+-- | Helper, not exported
+concToSymRef ::
+  W4I.IsExprBuilder sym =>
+  sym ->
+  ConcRegValue sym (ReferenceType tp) ->
+  IO (RegValue sym (ReferenceType tp))
+concToSymRef sym (v NE.:| _) = pure (MuxTree.toMuxTree sym v)
+
+-- | Helper, not exported
+concToSymVariant ::
+  forall sym tps.
+  W4I.IsExprBuilder sym =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  CtxRepr tps ->
+  ConcRegValue sym (VariantType tps) ->
+  IO (RegValue sym (VariantType tps))
+concToSymVariant sym iFns tps v = Ctx.zipWithM go tps v
+  where
+    go :: forall tp. TypeRepr tp -> ConcVariantBranch sym tp -> IO (RV.VariantBranch sym tp)
+    go tp (ConcVariantBranch b) =
+      case b of
+        Nothing -> pure (RV.VB (W4P.Err ()))
+        Just (ConcRV' v') ->
+          RV.VB . W4P.justPartExpr 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 "concToSym does not yet support floats"
+    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
+    SequenceRepr tp' ->
+      SymSeq.fromListSymSequence sym =<< traverse (concToSym sym iFns tp' . unConcRV') v
+    StringMapRepr tp' ->
+      traverse (fmap (W4P.justPartExpr sym) . concToSym sym iFns tp' . unConcRV') 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 _tp' -> concToSymRef sym v
+    VariantRepr tps -> concToSymVariant sym iFns tps v
+
+    -- Incomplete cases
+    WordMapRepr _ _ -> fail "concToSym does not yet support WordMap"

crucible/src/Lang/Crucible/Simulator/SymSequence.hs

@@ -14,6 +14,7 @@ module Lang.Crucible.Simulator.SymSequence
 ( SymSequence(..)
 , nilSymSequence
 , consSymSequence
+, fromListSymSequence
 , appendSymSequence
 , muxSymSequence
 , isNilSymSequence
@@ -167,6 +168,12 @@ consSymSequence _sym x xs =
   do n <- freshNonce globalNonceGenerator
      pure (SymSequenceCons n x xs)
 
+fromListSymSequence :: sym -> [a] -> IO (SymSequence sym a)
+fromListSymSequence sym =
+  \case
+    [] -> nilSymSequence sym
+    (x:xs) -> consSymSequence sym x =<< fromListSymSequence sym xs
+
 -- | Append two sequences
 appendSymSequence ::
   sym ->