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)