From e0f01d823667a6c7e58994016d9d2d68a04a67b0 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 17 Oct 2024 13:00:03 -0700 Subject: [PATCH] fix parsing of array whose elements do not have a fixed size, avoiding a blocked compile-time specialization --- src/3d/InterpreterTarget.fst | 13 ++++++------ src/3d/InterpreterTarget.fsti | 1 + src/3d/Target.fsti | 4 ++-- src/3d/TranslateForInterpreter.fst | 17 +++++++++++++-- src/3d/Z3TestGen.fst | 4 ++-- src/3d/prelude/EverParse3d.Actions.Base.fst | 22 +++++++++++++------- src/3d/prelude/EverParse3d.Actions.Base.fsti | 1 + src/3d/prelude/EverParse3d.Interpreter.fst | 13 ++++++------ 8 files changed, 49 insertions(+), 26 deletions(-) diff --git a/src/3d/InterpreterTarget.fst b/src/3d/InterpreterTarget.fst index 045c67260..7df445085 100644 --- a/src/3d/InterpreterTarget.fst +++ b/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) diff --git a/src/3d/InterpreterTarget.fsti b/src/3d/InterpreterTarget.fsti index 08c67f1de..194c1289f 100644 --- a/src/3d/InterpreterTarget.fsti +++ b/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 diff --git a/src/3d/Target.fsti b/src/3d/Target.fsti index 3495b679e..7681dd24e 100644 --- a/src/3d/Target.fsti +++ b/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' diff --git a/src/3d/TranslateForInterpreter.fst b/src/3d/TranslateForInterpreter.fst index cc4ea426f..b8302f72a 100644 --- a/src/3d/TranslateForInterpreter.fst +++ b/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 diff --git a/src/3d/Z3TestGen.fst b/src/3d/Z3TestGen.fst index 3b44b3fa5..b212a2133 100644 --- a/src/3d/Z3TestGen.fst +++ b/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 diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fst b/src/3d/prelude/EverParse3d.Actions.Base.fst index 7e68e3734..e44aad8c5 100644 --- a/src/3d/prelude/EverParse3d.Actions.Base.fst +++ b/src/3d/prelude/EverParse3d.Actions.Base.fst @@ -1316,6 +1316,7 @@ 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) @@ -1323,14 +1324,19 @@ let validate_nlist_constant_size_without_actions (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 diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fsti b/src/3d/prelude/EverParse3d.Actions.Base.fsti index 6aedd39c8..c28aa2031 100644 --- a/src/3d/prelude/EverParse3d.Actions.Base.fsti +++ b/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) diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst index 74c303f2e..9e6dc347f 100644 --- a/src/3d/prelude/EverParse3d.Interpreter.fst +++ b/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));