Merge pull request #1213 from langston-barrett/lb/conc-sym-seq

Use `Seq` instead of lists when concretizing `SymSequence`

crucible/CHANGELOG.md

@@ -1,3 +1,7 @@
+# next
+
+* Deprecate `concreteizeSymSequence` in favor of `concretizeSymSequence`
+
 # 0.7 -- 2024-02-05
 
 * Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to

crucible/src/Lang/Crucible/Concretize.hs

@@ -42,11 +42,13 @@ module Lang.Crucible.Concretize
   , concToSym
   ) where
 
+import qualified Data.Foldable as F
 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.Sequence (Seq)
 import           Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Data.Vector as V
@@ -101,7 +103,7 @@ type family ConcRegValue sym tp where
   ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r
   ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp)
   ConcRegValue sym (VectorType tp) = V.Vector (ConcRV' sym tp)
-  ConcRegValue sym (SequenceType tp) = [ConcRV' sym tp]
+  ConcRegValue sym (SequenceType tp) = Seq (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) = NonEmpty (RefCell tp)
@@ -300,17 +302,11 @@ concSymSequence ::
   ConcCtx sym t ->
   TypeRepr tp ->
   SymSeq.SymSequence sym (RegValue sym tp) ->
-  IO [ConcRV' sym tp]
+  IO (Seq (ConcRV' sym tp))
 concSymSequence ctx tp =
-  \case
-    SymSeq.SymSequenceNil -> pure []
-    SymSeq.SymSequenceCons _nonce v rest -> do
-      v' <- concRegValue ctx tp v
-      (ConcRV' v' :) <$> concSymSequence ctx tp rest
-    SymSeq.SymSequenceAppend _nonce xs ys ->
-      (++) <$> concSymSequence ctx tp xs <*> concSymSequence ctx tp ys
-    SymSeq.SymSequenceMerge _nonce p ts fs ->
-      concSymSequence ctx tp =<< ite ctx p ts fs
+  SymSeq.concretizeSymSequence
+    (ground ctx)
+    (fmap ConcRV' . concRegValue ctx tp)
 
 ---------------------------------------------------------------------
 -- * StringMap
@@ -589,8 +585,9 @@ concToSym sym iFns fm tp v =
     -- Simple recursive cases
     RecursiveRepr symb tyCtx ->
       RV.RolledType <$> concToSym sym iFns fm (unrollType symb tyCtx) v
-    SequenceRepr tp' ->
-      SymSeq.fromListSymSequence sym =<< traverse (concToSym sym iFns fm tp' . unConcRV') v
+    SequenceRepr tp' -> do
+      l <- traverse (concToSym sym iFns fm tp' . unConcRV') (F.toList v)
+      SymSeq.fromListSymSequence sym l
     StringMapRepr tp' ->
       traverse (fmap (W4P.justPartExpr sym) . concToSym sym iFns fm tp' . unConcRV') v
     StructRepr tps ->

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

@@ -24,6 +24,7 @@ module Lang.Crucible.Simulator.SymSequence
 , unconsSymSequence
 , traverseSymSequence
 , concreteizeSymSequence
+, concretizeSymSequence
 , prettySymSequence
 
   -- * Low-level evaluation primitives
@@ -41,6 +42,8 @@ import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Parameterized.Nonce
 import qualified Data.Parameterized.Map as MapF
+import           Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
 import           Prettyprinter (Doc)
 import qualified Prettyprinter as PP
 
@@ -410,6 +413,24 @@ concreteizeSymSequence conc eval = loop
     loop (SymSequenceMerge _ p xs ys) =
       do b <- conc p
          if b then loop xs else loop ys
+{-# DEPRECATED concreteizeSymSequence "Use concretizeSymSequence instead" #-} 
+
+-- | Using the given evaluation function for booleans, and an evaluation
+--   function for values, compute a concrete sequence corresponding
+--   to the given symbolic sequence.
+concretizeSymSequence ::
+  (Pred sym -> IO Bool) {- ^ evaluation for booleans -} ->
+  (a -> IO b) {- ^ evaluation for values -} ->
+  SymSequence sym a ->
+  IO (Seq b)
+concretizeSymSequence conc eval = loop
+  where
+    loop SymSequenceNil = pure Seq.empty
+    loop (SymSequenceCons _ v tl) = (Seq.<|) <$> eval v <*> loop tl
+    loop (SymSequenceAppend _ xs ys) = (Seq.><) <$> loop xs <*> loop ys
+    loop (SymSequenceMerge _ p xs ys) =
+      do b <- conc p
+         if b then loop xs else loop ys
 
 instance (IsExpr (SymExpr sym), PP.Pretty a) => PP.Pretty (SymSequence sym a) where
   pretty = prettySymSequence PP.pretty