Add support for the sequence type to crucible-syntax.

Add a very basic test case.

crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs

@@ -19,7 +19,6 @@ import Control.Applicative
 import Data.Char
 import Data.Functor
 import Data.Ratio
-import Data.Semigroup ( (<>) )
 import Data.Text (Text)
 import qualified Data.Text as T
 
@@ -50,7 +49,7 @@ data Keyword = Defun | DefBlock | DefGlobal
  | Just_ | Nothing_ | FromJust
  | Inj | Proj
  | AnyT | UnitT | BoolT | NatT | IntegerT | RealT | ComplexRealT | CharT | StringT
- | BitvectorT | VectorT | FPT | FunT | MaybeT | VariantT | StructT | RefT
+ | BitvectorT | VectorT | SequenceT | FPT | FunT | MaybeT | VariantT | StructT | RefT
  | Half_ | Float_ | Double_ | Quad_ | X86_80_ | DoubleDouble_
  | Unicode_ | Char8_ | Char16_
  | The
@@ -65,6 +64,9 @@ data Keyword = Defun | DefBlock | DefGlobal
  | VectorLit_ | VectorReplicate_ | VectorIsEmpty_ | VectorSize_
  | VectorGetEntry_ | VectorSetEntry_ | VectorCons_
  | MkStruct_ | GetField_ | SetField_
+ | SequenceNil_ | SequenceCons_ | SequenceAppend_
+ | SequenceIsNil_ | SequenceLength_
+ | SequenceHead_ | SequenceTail_ | SequenceUncons_
  | Deref | Ref | EmptyRef
  | Jump_ | Return_ | Branch_ | MaybeBranch_ | TailCall_ | Error_ | Output_ | Case
  | Print_ | PrintLn_
@@ -131,6 +133,7 @@ keywords =
  , ("String" , StringT)
  , ("Bitvector" , BitvectorT)
  , ("Vector", VectorT)
+ , ("Sequence", SequenceT)
  , ("->", FunT)
  , ("Maybe", MaybeT)
  , ("Variant", VariantT)
@@ -203,6 +206,16 @@ keywords =
  , ("vector-set", VectorSetEntry_)
  , ("vector-cons", VectorCons_)
 
+ -- Sequences
+ , ("seq-nil", SequenceNil_)
+ , ("seq-cons", SequenceCons_)
+ , ("seq-append", SequenceAppend_)
+ , ("seq-nil?", SequenceIsNil_)
+ , ("seq-length", SequenceLength_)
+ , ("seq-head", SequenceHead_)
+ , ("seq-tail", SequenceTail_)
+ , ("seq-uncons", SequenceUncons_)
+
  -- strings
  , ("show", Show)
  , ("string-concat", StringConcat_)

crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs

@@ -244,16 +244,16 @@ repUntilLast sp = describe "zero or more followed by one" $ repUntilLast' sp
  (cons p emptyList <&> \(x, ()) -> ([], x)) <|>
  (cons p (repUntilLast' p) <&> \(x, (xs, lst)) -> (x:xs, lst))
 
-isBaseType :: MonadSyntax Atomic m => m (Some BaseTypeRepr)
-isBaseType =
+_isBaseType :: MonadSyntax Atomic m => m (Some BaseTypeRepr)
+_isBaseType =
  describe "base type" $
  do Some tp <- isType
  case asBaseType tp of
  NotBaseType -> empty
  AsBaseType bt -> return (Some bt)
 
-isFloatingType :: MonadSyntax Atomic m => m (Some FloatInfoRepr)
-isFloatingType =
+_isFloatingType :: MonadSyntax Atomic m => m (Some FloatInfoRepr)
+_isFloatingType =
  describe "floating-point type" $
  do Some tp <- isType
  case tp of
@@ -288,7 +288,7 @@ stringSort =
 isType :: MonadSyntax Atomic m => m (Some TypeRepr)
 isType =
  describe "type" $ call
- (atomicType <|> stringT <|> vector <|> ref <|> bv <|> fp <|> fun <|> maybeT <|> var <|> struct)
+ (atomicType <|> stringT <|> vector <|> seqt <|> ref <|> bv <|> fp <|> fun <|> maybeT <|> var <|> struct)
 
  where
  atomicType =
@@ -303,6 +303,7 @@ isType =
  , kw CharT $> Some CharRepr
  ]
  vector = unary VectorT isType <&> \(Some t) -> Some (VectorRepr t)
+ seqt = unary SequenceT isType <&> \(Some t) -> Some (SequenceRepr t)
  ref = unary RefT isType <&> \(Some t) -> Some (ReferenceRepr t)
  bv :: MonadSyntax Atomic m => m (Some TypeRepr)
  bv = do BoundedNat len <- unary BitvectorT posNat
@@ -442,6 +443,8 @@ synthExpr typeHint =
  just <|> nothing <|> fromJust_ <|> injection <|> projection <|>
  vecLit <|> vecCons <|> vecRep <|> vecLen <|> vecEmptyP <|> vecGet <|> vecSet <|>
  struct <|> getField <|> setField <|>
+ seqNil <|> seqCons <|> seqAppend <|> seqNilP <|> seqLen <|>
+ seqHead <|> seqTail <|> seqUncons <|>
  ite <|> intLit <|> rationalLit <|> intp <|>
  binaryToFp <|> fpToBinary <|> realToFp <|> fpToReal <|>
  ubvToFloat <|> floatToUBV <|> sbvToFloat <|> floatToSBV <|>
@@ -961,6 +964,92 @@ synthExpr typeHint =
  pure $ SomeE (StructRepr ts) $ EApp $ SetStruct ts e idx v)
  _ -> pure $ Left $ ("struct type, but got " <> T.pack (show tp))))
 
+ seqNil :: m (SomeExpr s)
+ seqNil =
+ do Some t <- unary SequenceNil_ isType
+ return $ SomeE (SequenceRepr t) $ EApp $ SequenceNil t
+ <|>
+ kw SequenceNil_ *>
+ case typeHint of
+ Just (Some (SequenceRepr t)) ->
+ return $ SomeE (SequenceRepr t) $ EApp $ SequenceNil t
+ Just (Some t) ->
+ later $ describe ("value of type " <> T.pack (show t)) empty
+ Nothing ->
+ later $ describe ("unambiguous nil value") empty
+
+ seqCons :: m (SomeExpr s)
+ seqCons =
+ do let newhint = case typeHint of
+ Just (Some (SequenceRepr t)) -> Just (Some t)
+ _ -> Nothing
+ (a, d) <- binary SequenceCons_ (later (synthExpr newhint)) (later (synthExpr typeHint))
+ let g Nothing = Nothing
+ g (Just (Some t)) = Just (Some (SequenceRepr t))
+ case join (find isJust [ typeHint, g (someExprType a), someExprType d ]) of
+ Just (Some (SequenceRepr t)) ->
+ SomeE (SequenceRepr t) . EApp <$> (SequenceCons t <$> evalSomeExpr t a <*> evalSomeExpr (SequenceRepr t) d)
+ _ -> later $ describe "unambiguous sequence cons (add a type ascription to disambiguate)" empty
+
+ seqAppend :: m (SomeExpr s)
+ seqAppend =
+ do (x, y) <- binary SequenceAppend_ (later (synthExpr typeHint)) (later (synthExpr typeHint))
+ case join (find isJust [ typeHint, someExprType x, someExprType y ]) of
+ Just (Some (SequenceRepr t)) ->
+ SomeE (SequenceRepr t) . EApp <$>
+ (SequenceAppend t <$> evalSomeExpr (SequenceRepr t) x <*> evalSomeExpr (SequenceRepr t) y)
+ _ -> later $ describe "unambiguous sequence append (add a type ascription to disambiguate)" empty
+
+ seqNilP :: m (SomeExpr s)
+ seqNilP =
+ do Pair t e <- unary SequenceIsNil_ synth
+ case t of
+ SequenceRepr t' -> return $ SomeE BoolRepr $ EApp $ SequenceIsNil t' e
+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+ seqLen :: m (SomeExpr s)
+ seqLen =
+ do Pair t e <- unary SequenceLength_ synth
+ case t of
+ SequenceRepr t' -> return $ SomeE NatRepr $ EApp $ SequenceLength t' e
+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+ seqHead :: m (SomeExpr s)
+ seqHead =
+ do let newhint = case typeHint of
+ Just (Some (MaybeRepr t)) -> Just (Some (SequenceRepr t))
+ _ -> Nothing
+ (Pair t e) <-
+ unary SequenceHead_ (forceSynth =<< synthExpr newhint)
+ case t of
+ SequenceRepr elemT -> return $ SomeE (MaybeRepr elemT) $ EApp $ SequenceHead elemT e
+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+ seqTail :: m (SomeExpr s)
+ seqTail =
+ do let newhint = case typeHint of
+ Just (Some (MaybeRepr t)) -> Just (Some t)
+ _ -> Nothing
+ (Pair t e) <-
+ unary SequenceTail_ (forceSynth =<< synthExpr newhint)
+ case t of
+ SequenceRepr elemT -> return $ SomeE (MaybeRepr (SequenceRepr elemT)) $ EApp $ SequenceTail elemT e
+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+ seqUncons :: m (SomeExpr s)
+ seqUncons =
+ do let newhint = case typeHint of
+ Just (Some (MaybeRepr (StructRepr (Ctx.Empty Ctx.:> t Ctx.:> _)))) ->
+ Just (Some (SequenceRepr t))
+ _ -> Nothing
+ (Pair t e) <-
+ unary SequenceUncons_ (forceSynth =<< synthExpr newhint)
+ case t of
+ SequenceRepr elemT ->
+ return $ SomeE (MaybeRepr (StructRepr (Ctx.Empty Ctx.:> elemT Ctx.:> SequenceRepr elemT))) $
+ EApp $ SequenceUncons elemT e
+ other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
  showExpr :: m (SomeExpr s)
  showExpr =
  do Pair t1 e <- unary Show synth

crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs

@@ -28,7 +28,6 @@ import Lang.Crucible.Backend
 import Lang.Crucible.Types
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
-import Lang.Crucible.Simulator.SimError (ppSimError)
 
 
 setupOverrides ::

crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs

@@ -106,13 +106,13 @@ simulateProgram fn theInput outh profh opts setup =
  case find isMain cs of
  Just (ACFG Ctx.Empty retType mn) ->
  do let mainHdl = cfgHandle mn
- let fnBindings = fnBindingsFromList
+ let fns = fnBindingsFromList
  [ case toSSA g of
  C.SomeCFG ssa ->
  FnBinding (cfgHandle g) (UseCFG ssa (postdomInfo ssa))
  | ACFG _ _ g <- cs
  ]
- let simCtx = initSimContext sym emptyIntrinsicTypes ha outh fnBindings emptyExtensionImpl ()
+ let simCtx = initSimContext sym emptyIntrinsicTypes ha outh fns emptyExtensionImpl ()
  let simSt = InitialState simCtx emptyGlobals defaultAbortHandler retType $
  runOverrideSim retType $
  do mapM_ (registerFnBinding . fst) ovrs

crucible-syntax/test-data/simulator-tests/seq-test1.cbl

@@ -0,0 +1,32 @@
+(defun @main () Unit
+ (start start:
+ (let n (the (Sequence Nat) seq-nil))
+ (assert! (seq-nil? n) "nil test")
+ (assert! (equal? 0 (seq-length n)) "nil length test")
+
+ (let s1 (seq-cons 5 n))
+
+ (assert! (not (seq-nil? s1)) "cons test")
+ (assert! (equal? 1 (seq-length s1)) "cons length test")
+
+ (let v (from-just (seq-head s1) "head s1"))
+ (let t (from-just (seq-tail s1) "tail s1"))
+ (let u (from-just (seq-uncons s1) "uncons s1"))
+
+ (let v2 (get-field 0 u))
+ (let t2 (get-field 1 u))
+
+ (assert! (equal? 5 v) "head value test")
+ (assert! (equal? v v2) "head equal test")
+ (assert! (seq-nil? t) "tail nil test")
+ (assert! (seq-nil? t2) "uncons tail nil test")
+
+ (let s2 (seq-append s1 (seq-cons 42 (seq-nil Nat))))
+ (assert! (equal? 2 (seq-length s2)) "append length")
+ (assert! (not (seq-nil? s2)) "append non-nil")
+
+ (let v3 (from-just (seq-head (from-just (seq-tail s2) "cdr s2")) "cadr s2"))
+ (assert! (equal? 42 v3) "cadr s2 test")
+
+ (return ()))
+)

crucible-syntax/test-data/simulator-tests/seq-test1.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====