diff --git a/crucible/src/Lang/Crucible/Concretize.hs b/crucible/src/Lang/Crucible/Concretize.hs index 5ece1aa60..0efea24b1 100644 --- a/crucible/src/Lang/Crucible/Concretize.hs +++ b/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" diff --git a/crucible/src/Lang/Crucible/Simulator/SymSequence.hs b/crucible/src/Lang/Crucible/Simulator/SymSequence.hs index f714a7d37..8d9c250ae 100644 --- a/crucible/src/Lang/Crucible/Simulator/SymSequence.hs +++ b/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 -> diff --git a/dependencies/what4 b/dependencies/what4 index 8c9401b5d..494ac6416 160000 --- a/dependencies/what4 +++ b/dependencies/what4 @@ -1 +1 @@ -Subproject commit 8c9401b5d21d20451d224d4834bd611fc83b850b +Subproject commit 494ac6416ed01eab6ae5d1be427d0aaae4c4bb91