Add a new Crucible type for representing sequence values.

Unlike vectors, sequences are explicitly represented as cons-lists
and are designed to be merged effeciently, even at different lengths.

crucible/crucible.cabal

@@ -110,6 +110,7 @@ library
     Lang.Crucible.Simulator.RegMap
     Lang.Crucible.Simulator.RegValue
     Lang.Crucible.Simulator.SimError
+    Lang.Crucible.Simulator.SymSequence
     Lang.Crucible.Syntax
     Lang.Crucible.Types
     Lang.Crucible.Vector

crucible/src/Lang/Crucible/CFG/Expr.hs

@@ -487,6 +487,50 @@ data App (ext :: Type) (f :: CrucibleType -> Type) (tp :: CrucibleType) where
                 -> !(f (RecursiveType nm ctx))
                 -> App ext f (UnrollType nm ctx)
 
+  ----------------------------------------------------------------------
+  -- Sequences
+
+  -- Create an empty sequence
+  SequenceNil :: !(TypeRepr tp) -> App ext f (SequenceType tp)
+
+  -- Add a new value to the front of a sequence
+  SequenceCons :: !(TypeRepr tp)
+               -> !(f tp)
+               -> !(f (SequenceType tp))
+               -> App ext f (SequenceType tp)
+
+  -- Append two sequences
+  SequenceAppend :: !(TypeRepr tp)
+                 -> !(f (SequenceType tp))
+                 -> !(f (SequenceType tp))
+                 -> App ext f (SequenceType tp)
+
+  -- Test if a sequence is nil
+  SequenceIsNil :: !(TypeRepr tp)
+                -> !(f (SequenceType tp))
+                -> App ext f BoolType
+
+  -- Return the length of a sequence
+  SequenceLength :: !(TypeRepr tp)
+                 -> !(f (SequenceType tp))
+                 -> App ext f NatType
+
+  -- Return the head of a sesquence, if it is non-nil.
+  SequenceHead :: !(TypeRepr tp)
+               -> !(f (SequenceType tp))
+               -> App ext f (MaybeType tp)
+
+  -- Return the tail of a sequence, if it is non-nil.
+  SequenceTail :: !(TypeRepr tp)
+               -> !(f (SequenceType tp))
+               -> App ext f (MaybeType (SequenceType tp))
+
+  -- Deconstruct a sequence.  Return nothing if nil,
+  -- return the head and tail if non-nil.
+  SequenceUncons :: !(TypeRepr tp)
+                 -> !(f (SequenceType tp))
+                 -> App ext f (MaybeType (StructType (EmptyCtx ::> tp ::> SequenceType tp)))
+
   ----------------------------------------------------------------------
   -- Vector
 
@@ -1173,6 +1217,18 @@ instance TypeApp (ExprExtension ext) => TypeApp (App ext) where
     VectorSetEntry  tp _ _ _ -> VectorRepr tp
     VectorCons      tp _ _   -> VectorRepr tp
 
+    ----------------------------------------------------------------------
+    -- Sequence
+    SequenceNil tpr -> SequenceRepr tpr
+    SequenceCons tpr _ _ -> SequenceRepr tpr
+    SequenceAppend tpr _ _ -> SequenceRepr tpr
+    SequenceIsNil _ _ -> knownRepr
+    SequenceHead tpr _ -> MaybeRepr tpr
+    SequenceUncons tpr _ ->
+      MaybeRepr (StructRepr (Ctx.Empty Ctx.:> tpr Ctx.:> SequenceRepr tpr))
+    SequenceLength{} -> knownRepr
+    SequenceTail tpr _ -> MaybeRepr (SequenceRepr tpr)
+
     ----------------------------------------------------------------------
     -- SymbolicArrayType
 

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

@@ -66,6 +66,7 @@ import           Lang.Crucible.CFG.Expr
 import           Lang.Crucible.Simulator.Intrinsics
 import           Lang.Crucible.Simulator.RegMap
 import           Lang.Crucible.Simulator.SimError
+import           Lang.Crucible.Simulator.SymSequence
 import           Lang.Crucible.Types
 import           Lang.Crucible.Utils.MuxTree
 
@@ -470,6 +471,27 @@ evalApp sym itefns _logFn evalExt (evalSub :: forall tp. f tp -> IO (RegValue sy
       v <- evalSub v_expr
       return $ V.cons e v
 
+    --------------------------------------------------------------------
+    -- Sequence
+
+    SequenceNil _tpr -> nilSymSequence sym
+    SequenceCons _tpr x xs ->
+      join $ consSymSequence sym <$> evalSub x <*> evalSub xs
+    SequenceAppend _tpr xs ys ->
+      join $ appendSymSequence sym <$> evalSub xs <*> evalSub ys
+    SequenceIsNil _tpr xs ->
+      isNilSymSequence sym =<< evalSub xs
+    SequenceLength _tpr xs ->
+      lengthSymSequence sym =<< evalSub xs
+    SequenceHead tpr xs ->
+      headSymSequence sym (muxRegForType sym itefns tpr) =<< evalSub xs
+    SequenceTail _tpr xs ->
+      tailSymSequence sym =<< evalSub xs
+    SequenceUncons tpr xs ->
+      do xs' <- evalSub xs
+         mu <- unconsSymSequence sym (muxRegForType sym itefns tpr) xs'
+         traverse (\ (h,tl) -> pure (Ctx.Empty Ctx.:> RV h Ctx.:> RV tl)) mu
+
     --------------------------------------------------------------------
     -- Symbolic Arrays
 

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

@@ -233,6 +233,7 @@ muxRegForType s itefns p =
 
      MaybeRepr r          -> mergePartExpr s (muxRegForType s itefns r)
      VectorRepr r         -> muxVector s (muxRegForType s itefns r)
+     SequenceRepr _r      -> muxSymSequence s
      StringMapRepr r      -> muxStringMap s (muxRegForType s itefns r)
      SymbolicArrayRepr{}         -> arrayIte s
      SymbolicStructRepr{}        -> structIte s

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

@@ -25,15 +25,17 @@ module Lang.Crucible.Simulator.RegValue
   ( RegValue
   , CanMux(..)
   , RegValue'(..)
-  , VariantBranch(..)
-  , injectVariant
   , MuxFn
 
     -- * Register values
   , AnyValue(..)
   , FnVal(..)
   , fnValType
   , RolledType(..)
+  , SymSequence(..)
+
+  , VariantBranch(..)
+  , injectVariant
 
     -- * Value mux functions
   , ValMuxFn
@@ -44,6 +46,7 @@ module Lang.Crucible.Simulator.RegValue
   , muxStruct
   , muxVariant
   , muxVector
+  , muxSymSequence
   , muxHandle
   ) where
 
@@ -70,6 +73,7 @@ import           What4.WordMap
 import           Lang.Crucible.FunctionHandle
 import           Lang.Crucible.Simulator.Intrinsics
 import           Lang.Crucible.Simulator.SimError
+import           Lang.Crucible.Simulator.SymSequence
 import           Lang.Crucible.Types
 import           Lang.Crucible.Utils.MuxTree
 import           Lang.Crucible.Backend
@@ -87,6 +91,7 @@ type family RegValue (sym :: Type) (tp :: CrucibleType) :: Type where
   RegValue sym (FunctionHandleType a r) = FnVal sym a r
   RegValue sym (MaybeType tp) = PartExpr (Pred sym) (RegValue sym tp)
   RegValue sym (VectorType tp) = V.Vector (RegValue sym tp)
+  RegValue sym (SequenceType tp) = SymSequence sym (RegValue sym tp)
   RegValue sym (StructType ctx) = Ctx.Assignment (RegValue' sym) ctx
   RegValue sym (VariantType ctx) = Ctx.Assignment (VariantBranch sym) ctx
   RegValue sym (ReferenceType tp) = MuxTree sym (RefCell tp)