fix parsing of array whose elements do not have a fixed size, avoidin…

…g a blocked compile-time specialization

src/3d/InterpreterTarget.fst

@@ -227,7 +227,7 @@ let tag_of_parser p
     match p.p_parser with
     | Parse_return _ -> "Parse_return"
     | Parse_app _ _ -> "Parse_app"
-    | Parse_nlist _ _ -> "Parse_nlist"
+    | Parse_nlist _ _ _ -> "Parse_nlist"
     | Parse_t_at_most _ _ -> "Parse_t_at_most"
     | Parse_t_exact _ _ -> "Parse_t_exact"
     | Parse_pair _ _ _ -> "Parse_pair"
@@ -348,7 +348,7 @@ let rec typ_indexes_of_parser (en:env) (p:T.parser)
     | T.Parse_weaken_right p _
     | T.Parse_refinement _ p _
     | T.Parse_with_comment p _
-    | T.Parse_nlist _ p
+    | T.Parse_nlist _ _ p
     | T.Parse_t_at_most _ p
     | T.Parse_t_exact _ p ->
       typ_indexes_of_parser p
@@ -424,8 +424,8 @@ let typ_of_parser (en: env) : Tot (T.parser -> ML typ)
     | T.Parse_with_comment p c ->
       T_with_comment fn (typ_of_parser p) (String.concat "; " c)
 
-    | T.Parse_nlist n p ->
-      T_nlist fn n (typ_of_parser p)
+    | T.Parse_nlist fixed_size n p ->
+      T_nlist fn fixed_size n (typ_of_parser p)
 
     | T.Parse_t_at_most n p ->
       T_at_most fn n (typ_of_parser p)
@@ -813,7 +813,7 @@ let rec print_typ (mname:string) (t:typ)
                      (print_typ mname t)
                      c
 
-    | T_nlist fn n t ->
+    | T_nlist fn fixed_size n t ->
       let rec as_constant n =
         let open T in
         match fst n with
@@ -846,9 +846,10 @@ let rec print_typ (mname:string) (t:typ)
         | None -> false, n
         | Some m -> true, (T.Constant m, snd n)
       in
-      Printf.sprintf "(T_nlist \"%s\" %b %s %s)"
+      Printf.sprintf "(T_nlist \"%s\" %b %b %s %s)"
                      fn
                      is_const
+                     fixed_size
                      (T.print_expr mname n)
                      (print_typ mname t)
 

src/3d/InterpreterTarget.fsti

@@ -156,6 +156,7 @@ type typ : Type =
 
   | T_nlist:
       fn:non_empty_string ->
+      fixed_size_t:bool -> //does t have a fixed size?
       n:expr ->
       t:typ ->
       typ

src/3d/Target.fsti

@@ -165,7 +165,7 @@ type parser_kind' =
 and parser_kind = {
   pk_kind : parser_kind';
   pk_weak_kind : A.weak_kind ;
-  pk_nz: bool
+  pk_nz: bool;
 }
 
 val expr_eq (e1 e1:expr) : bool
@@ -177,7 +177,7 @@ noeq
 type parser' =
   | Parse_return    : v:expr -> parser'
   | Parse_app       : hd:A.ident -> args:list index -> parser'
-  | Parse_nlist     : n:expr -> t:parser -> parser'
+  | Parse_nlist     : t_size_constant:bool -> n:expr -> t:parser -> parser'
   | Parse_t_at_most : n:expr -> t:parser -> parser'
   | Parse_t_exact   : n:expr -> t:parser -> parser'
   | Parse_pair      : n1: A.ident -> p:parser -> q:parser -> parser'

src/3d/TranslateForInterpreter.fst

@@ -373,6 +373,18 @@ let rec translate_typ (t:A.typ) : ML (T.typ & T.decls) =
     let args, decls = args |> List.map translate_typ_param |> List.split in
     T.T_app hd b (List.map Inr args), List.flatten decls
 
+let rec is_fixed_size_array_payload (env:global_env) (t:T.typ)
+: ML bool
+= match t with
+  | T.T_false -> true
+  | T.T_app hd _ _ -> 
+    let size = TypeSizes.size_of_typename env.size_env hd in
+    TS.Fixed? size
+  | T.T_pointer _ -> true
+  | T.T_refine base _ -> is_fixed_size_array_payload env base
+  | T.T_with_comment t _ -> is_fixed_size_array_payload env t
+  | _ -> false
+
 let translate_probe_entrypoint
   (p: A.probe_entrypoint)
 : ML T.probe_entrypoint
@@ -466,11 +478,12 @@ let rec parse_typ (env:global_env)
 
   | T.T_app {v={name="nlist"}} KindSpec [Inr e; Inl t] ->
     let pt = parse_typ env typename (extend_fieldname "element") t in
+    let t_size_constant = is_fixed_size_array_payload env t in
     mk_parser pk_list
               t
               typename
               fieldname
-              (T.Parse_nlist e pt)
+              (T.Parse_nlist t_size_constant e pt)
 
   | T.T_app {v={name="t_at_most"}} KindSpec [Inr e; Inl t] ->
     let pt = parse_typ env typename (extend_fieldname "element") t in
@@ -695,7 +708,7 @@ let rec parser_is_constant_size_without_actions
     -> true
   | T.Parse_app hd _
     -> parser_kind_is_constant_size env hd
-  | T.Parse_nlist array_size parse_elem
+  | T.Parse_nlist _ array_size parse_elem
     -> begin match fst array_size with
       | T.Constant (A.Int _ array_size) -> parser_is_constant_size_without_actions env parse_elem
       | _ -> false

src/3d/Z3TestGen.fst

@@ -923,7 +923,7 @@ let rec typ_depth (t: I.typ) : GTot nat
   | I.T_with_comment _ t' _
   | I.T_at_most _ _ t'
   | I.T_exact _ _ t'
-  | I.T_nlist _ _ t'
+  | I.T_nlist _ _ _ t'
     -> 1 + typ_depth t'
   | I.T_with_dep_action _ _ _
   | I.T_refine _ _ _
@@ -955,7 +955,7 @@ let rec parse_typ (t : I.typ) : Tot (parser not_reading)
   | I.T_at_most _ size body -> parse_at_most (fun _ -> mk_expr size) (parse_typ body)
   | I.T_exact _ size body -> parse_exact (fun _ -> mk_expr size) (parse_typ body)
   | I.T_string _ elt terminator -> parse_string (parse_readable_dtyp elt) (fun _ -> mk_expr terminator)
-  | I.T_nlist _ size body ->
+  | I.T_nlist _ _ size body ->
     if match body with
     | I.T_denoted _ (I.DT_IType i) -> Some? (itype_byte_size i)
     | _ -> false

src/3d/prelude/EverParse3d.Actions.Base.fst

@@ -1316,21 +1316,27 @@ noextract
 inline_for_extraction
 let validate_nlist_constant_size_without_actions
     (n_is_const: bool)
+    (payload_is_constant_size: bool)
     (n:U32.t)
     #wk
     (#k:parser_kind true wk)
     #t (#p:parser k t) #inv #disj #l #ar
     (v: validate_with_action_t p inv disj l ar)
 : Tot (validate_with_action_t (parse_nlist n p) inv disj l false)
 = 
-  if
-    let open LP in
-    k.parser_kind_subkind = Some ParserStrong &&
-    k.parser_kind_high = Some k.parser_kind_low &&
-    k.parser_kind_metadata = Some ParserKindMetadataTotal &&
-    k.parser_kind_low < 4294967296
-  then
-    validate_drop (validate_nlist_total_constant_size n_is_const n p inv disj l)
+  if payload_is_constant_size
+  then (
+    if
+      let open LP in
+      k.parser_kind_subkind = Some ParserStrong &&
+      k.parser_kind_high = Some k.parser_kind_low &&
+      k.parser_kind_metadata = Some ParserKindMetadataTotal &&
+      k.parser_kind_low < 4294967296
+    then
+      validate_drop (validate_nlist_total_constant_size n_is_const n p inv disj l)
+    else
+      validate_nlist n v
+  )
   else
     validate_nlist n v
 

src/3d/prelude/EverParse3d.Actions.Base.fsti

@@ -553,6 +553,7 @@ val validate_nlist
 noextract inline_for_extraction
 val validate_nlist_constant_size_without_actions
        (n_is_const: bool)
+       (payload_is_constant_size:bool)
        (n:U32.t)
        (#wk: _)
        (#k:parser_kind true wk)

src/3d/prelude/EverParse3d.Interpreter.fst

@@ -902,6 +902,7 @@ type typ
       #wk:_ -> #pk:P.parser_kind true wk ->
       #i:_ -> #l:_ -> #d:_ -> #b:_ ->
       n_is_constant:bool ->
+      payload_is_constant_size:bool ->
       n:U32.t ->
       t:typ pk i d l b ->
       typ P.kind_nlist i d l false
@@ -1007,7 +1008,7 @@ let rec as_type
     | T_with_dep_action _ i _ ->
       dtyp_as_type i
 
-    | T_nlist _ _ n t ->
+    | T_nlist _ _ _ n t ->
       P.nlist n (as_type t)
 
     | T_at_most _ n t ->
@@ -1096,7 +1097,7 @@ let rec as_parser
       //assert_norm (as_type g (T_with_comment t c) == as_type g t);
       as_parser t
 
-    | T_nlist _ _ n t ->
+    | T_nlist _ _ _ n t ->
       P.parse_nlist n (as_parser t)
 
     | T_at_most _ n t ->
@@ -1302,11 +1303,11 @@ let rec as_validator
       assert_norm (as_parser (T_with_comment fn t c) == as_parser t);
       A.validate_with_comment c (as_validator typename t)
 
-    | T_nlist fn n_is_const n t ->
-      assert_norm (as_type (T_nlist fn n_is_const n t) == P.nlist n (as_type t));
-      assert_norm (as_parser (T_nlist fn n_is_const n t) == P.parse_nlist n (as_parser t));
+    | T_nlist fn n_is_const payload_is_constant_size n t ->
+      assert_norm (as_type (T_nlist fn n_is_const payload_is_constant_size n t) == P.nlist n (as_type t));
+      assert_norm (as_parser (T_nlist fn n_is_const payload_is_constant_size n t) == P.parse_nlist n (as_parser t));
       A.validate_with_error_handler typename fn 
-        (A.validate_nlist_constant_size_without_actions n_is_const n (as_validator typename t))
+        (A.validate_nlist_constant_size_without_actions n_is_const payload_is_constant_size n (as_validator typename t))
 
     | T_at_most fn n t ->
       assert_norm (as_type (T_at_most fn n t) == P.t_at_most n (as_type t));