Merge pull request #116 from project-everest/_taramana_3d_consume_all

3d: allow fields that consume all input

src/3d/Ast.fst

@@ -466,6 +466,7 @@ type field_array_t =
   | FieldScalar
   | FieldArrayQualified of (expr & array_qualifier) //array size in bytes, the qualifier indicates whether this is a variable-length suffix or not
   | FieldString of (option expr)
+  | FieldConsumeAll // [:consume-all]
 
 [@@ PpxDerivingYoJson ]
 noeq
@@ -774,6 +775,7 @@ let mk_prim_t x = with_dummy_range (Type_app (with_dummy_range (to_ident' x)) Ki
 let tbool = mk_prim_t "Bool"
 let tunit = mk_prim_t "unit"
 let tuint8 = mk_prim_t "UINT8"
+let tuint8be = mk_prim_t "UINT8BE"
 let puint8 = mk_prim_t "PUINT8"
 let tuint16 = mk_prim_t "UINT16"
 let tuint32 = mk_prim_t "UINT32"
@@ -850,6 +852,7 @@ let subst_field_array (s:subst) (f:field_array_t) : ML field_array_t =
   | FieldScalar -> f
   | FieldArrayQualified (e, q) -> FieldArrayQualified (subst_expr s e, q)
   | FieldString sz -> FieldString (map_opt (subst_expr s) sz)
+  | FieldConsumeAll -> f
 let rec subst_field (s:subst) (ff:field) : ML field =
   match ff.v with
   | AtomicField f -> {ff with v = AtomicField (subst_atomic_field s f)}
@@ -1102,6 +1105,7 @@ and print_atomic_field (f:atomic_field) : ML string =
       end
     | FieldString None -> Printf.sprintf "[::zeroterm]"
     | FieldString (Some sz) -> Printf.sprintf "[:zeroterm-b-te-size-at-most %s]" (print_expr sz)
+    | FieldConsumeAll -> Printf.sprintf "[:consume-all]"
   in
   let sf = f.v in
     Printf.sprintf "%s%s %s%s%s%s;"

src/3d/Binding.fst

@@ -1096,6 +1096,13 @@ let check_atomic_field (env:env) (extend_scope: bool) (f:atomic_field)
     | FieldScalar -> FieldScalar
     | FieldArrayQualified (e, b) -> FieldArrayQualified (check_annot e, b)
     | FieldString sz -> FieldString (map_opt check_annot sz)
+    | FieldConsumeAll ->
+      if
+        if eq_typ env sf.field_type tuint8
+        then true
+        else eq_typ env sf.field_type tuint8be
+      then FieldConsumeAll
+      else error (Printf.sprintf "This ':consume-all field returns %s instead of UINT8 or UINT8BE" (print_typ sf.field_type)) f.range
     in
     let fc = sf.field_constraint |> map_opt (fun e ->
         add_local env sf.field_ident sf.field_type;

src/3d/Deps.fst

@@ -147,7 +147,9 @@ let scan_deps (fn:string) : ML scan_deps_t =
     match fa with
     | FieldScalar -> []
     | FieldArrayQualified (e, _) -> deps_of_expr e
-    | FieldString eopt -> deps_of_opt deps_of_expr eopt in
+    | FieldString eopt -> deps_of_opt deps_of_expr eopt
+    | FieldConsumeAll -> []
+  in
 
   let deps_of_atomic_field (af:atomic_field) : ML (list string) =
       let af = af.v in

src/3d/Desugar.fst

@@ -329,6 +329,7 @@ let resolve_field_array_t (env:qenv) (farr:field_array_t) : ML field_array_t =
     FieldArrayQualified (resolve_expr env e, aq)
   | FieldString None -> farr
   | FieldString (Some e) -> FieldString (Some (resolve_expr env e))
+  | FieldConsumeAll -> farr
 
 let rec resolve_field (env:qenv) (ff:field) : ML (field & qenv) =
   match ff.v with

src/3d/Simplify.fst

@@ -111,6 +111,7 @@ let simplify_field_array (env:T.env_t) (f:field_array_t) : ML field_array_t =
   | FieldScalar -> FieldScalar
   | FieldArrayQualified (e, b) -> FieldArrayQualified (simplify_expr env e, b)
   | FieldString sz -> FieldString (map_opt (simplify_expr env) sz)
+  | FieldConsumeAll -> FieldConsumeAll
 
 let simplify_atomic_field (env:T.env_t) (f:atomic_field)
   : ML atomic_field

src/3d/TranslateForInterpreter.fst

@@ -887,6 +887,7 @@ let translate_atomic_field (f:A.atomic_field) : ML (T.struct_field & T.decls) =
           | None -> str
           | Some e -> mk_at_most str e
           end
+        | FieldConsumeAll -> T.T_app (with_range (to_ident' "all_bytes") sf.field_type.range) KindSpec []
     in
     let t =
       match sf.field_constraint with

src/3d/ocaml/lexer.mll

@@ -147,6 +147,7 @@ rule token =
   | "[:byte-size-single-element-array"        { locate lexbuf LBRACK_SINGLE_ELEMENT_BYTESIZE }
   | "[:zeroterm"     { locate lexbuf LBRACK_STRING }
   | "[:zeroterm-byte-size-at-most"     { locate lexbuf LBRACK_STRING_AT_MOST }
+  | "[:consume-all"  { locate lexbuf LBRACK_CONSUME_ALL }
   | "["                          { locate lexbuf LBRACK (* intended for use with UINT8 arrays only, interpreted as [:byte-size] *)}
   | "]"                          { locate lexbuf RBRACK }
   | "[="           { deprecation_warning lexbuf "[:byte-size-single-element-array";

src/3d/ocaml/parser.mly

@@ -55,6 +55,7 @@
 %token          DEFINE LPAREN RPAREN LBRACE RBRACE DOT RARROW COMMA SEMICOLON COLON_COLON COLON QUESTION
 %token          STAR DIV MINUS PLUS LEQ LESS_THAN GEQ GREATER_THAN WHERE REQUIRES IF ELSE
 %token          LBRACK RBRACK LBRACK_LEQ LBRACK_EQ LBRACK_BYTESIZE LBRACK_BYTESIZE_AT_MOST LBRACK_SINGLE_ELEMENT_BYTESIZE
+%token          LBRACK_CONSUME_ALL
 %token          LBRACK_STRING LBRACK_STRING_AT_MOST
 %token          MUTABLE LBRACE_ONSUCCESS LBRACE_ACT LBRACE_CHECK FIELD_POS_64 FIELD_POS_32 FIELD_PTR FIELD_PTR_AFTER VAR ABORT RETURN
 %token          REM SHIFT_LEFT SHIFT_RIGHT BITWISE_AND BITWISE_OR BITWISE_XOR BITWISE_NOT AS
@@ -253,6 +254,7 @@ array_annot:
   | a=array_size { FieldArrayQualified a }
   | LBRACK_STRING RBRACK { FieldString None }
   | LBRACK_STRING_AT_MOST e=expr RBRACK { FieldString (Some e) }
+  | LBRACK_CONSUME_ALL RBRACK { FieldConsumeAll }
 
 bitwidth:
   | COLON i=INT { Inl (with_range (Z.of_string i) $startpos(i)) }

src/3d/tests/FAILAllBytesCompose.3d

@@ -0,0 +1,13 @@
+entrypoint
+typedef struct _test1 {
+  UINT32 a;
+  UINT16 b;
+  UINT8 c;
+  UINT8 remainder[:consume-all];
+} test1;
+
+entrypoint
+typedef struct _test2 {
+  test1 should_not_be_here;
+  UINT8 c;
+} test2;

src/3d/tests/FAILAllBytesNotLast.3d

@@ -0,0 +1,7 @@
+entrypoint
+typedef struct _test1 {
+  UINT32 a;
+  UINT16 b;
+  UINT8 remainder[:consume-all];
+  UINT8 c;
+} test1;

src/3d/tests/FAILAllBytesType.3d

@@ -0,0 +1,7 @@
+entrypoint
+typedef struct _test1 {
+  UINT32 a;
+  UINT16 b;
+  UINT8 c;
+  UINT16 remainder[:consume-all];
+} test1;

src/3d/tests/TestAllBytes.3d

@@ -0,0 +1,28 @@
+entrypoint
+typedef struct _test1 {
+  UINT32 a;
+  UINT16 b;
+  UINT8 c;
+  UINT8 remainder[:consume-all];
+} test1;
+
+entrypoint
+typedef struct _test2 {
+  UINT32BE a;
+  UINT16BE b;
+  UINT8BE c;
+  UINT8BE remainder[:consume-all];
+} test2;
+
+entrypoint
+typedef struct _test3 {
+  UINT32 size1;
+  test1 mytest1[:byte-size-single-element-array size1];
+  test1 mytest1_at_most[:byte-size-single-element-array-at-most size1];
+  test1 mytest1_array[:byte-size size1]; // in practice, this array will only have one element (or zero, if size1 == 0); 
+  UINT32 size2;
+  test2 mytest2[:byte-size-single-element-array size2];
+  test2 mytest2_at_most[:byte-size-single-element-array-at-most size2];
+  test2 mytest2_array[:byte-size size2]; // in practice, this array will only have one element (or zero, if size2 == 0); 
+  UINT16 something_else;
+} test3;