diff --git a/src/3d/InterpreterTarget.fst b/src/3d/InterpreterTarget.fst index 9974ed2fb..73b3d91f4 100644 --- a/src/3d/InterpreterTarget.fst +++ b/src/3d/InterpreterTarget.fst @@ -43,6 +43,7 @@ type disj_pre = | Disj_triv : disj_pre | Disj_pair : eloc -> eloc -> disj_pre | Disj_conj : disj_pre -> disj_pre -> disj_pre + | Disj_name : A.ident -> list expr -> disj_pre let rec subst_eloc subst (e:eloc) : eloc @@ -67,12 +68,14 @@ let rec subst_disj_index subst (d:disj_pre) | Disj_conj d1 d2 -> Disj_conj (subst_disj_index subst d1) (subst_disj_index subst d2) + | Disj_name hd args -> + Disj_name hd (List.Tot.map (T.subst_expr subst) args) -let disj_conj d0 d1 = - match d0, d1 with - | Disj_triv, d - | d, Disj_triv -> d - | _, _ -> Disj_conj d0 d1 +let disj_conj d0 d1 = Disj_conj d0 d1 + // match d0, d1 with + // | Disj_triv, d + // | d, Disj_triv -> d + // | _, _ -> Disj_conj d0 d1 noeq type on_success = @@ -84,9 +87,19 @@ let typ_indexes = inv & eloc & disj_pre & on_success let typ_indexes_nil = Inv_true, Eloc_none, Disj_triv, On_success false let typ_indexes_union (i, e, d, b) (i', e', d', b') = Inv_conj i i', Eloc_union e e', disj_conj d d', On_success_union b b' -let typ_indexes_name_except_disj hd args = +let typ_indexes_union_l_bias (i, e, d, b) (i', e', d', b') = + if not (Disj_triv? d) + then failwith "Unexpected disjunctive index in typ_indexes_union_l_bias" + else Inv_conj i i', Eloc_union e e', d', On_success_union b b' +let typ_indexes_union_r_bias (i, e, d, b) (i', e', d', b') = + if not (Disj_triv? d') + then failwith "Unexpected disjunctive index in typ_indexes_union_r_bias" + else Inv_conj i i', Eloc_union e e', d, On_success_union b b' + +let typ_indexes_name hd args = Inv_name hd args, Eloc_name hd args, + Disj_name hd args, On_success_named hd args let env = H.t A.ident' type_decl @@ -271,23 +284,24 @@ let rec typ_indexes_of_parser (en:env) (p:T.parser) | Some td -> td | _ -> failwith (Printf.sprintf "Type decl not found for %s" (A.ident_to_string hd)) in - let _, _, disj_index_p, _ = td.typ_indexes in - let subst = - match T.mk_subst td.name.td_params args with - | None -> - failwith (Printf.sprintf "Unexpected number of arguments to type %s" (A.ident_to_string td.name.td_name)) - | Some s -> s - in - let disj_index = subst_disj_index subst disj_index_p in - let i, e, r = typ_indexes_name_except_disj hd (filter_args_for_inv args td) in - i, e, disj_index, r + // let _, _, disj_index_p, _ = td.typ_indexes in + // let subst = + // match T.mk_subst td.name.td_params args with + // | None -> + // failwith (Printf.sprintf "Unexpected number of arguments to type %s" (A.ident_to_string td.name.td_name)) + // | Some s -> s + // in + // let disj_index = subst_disj_index subst disj_index_p in + typ_indexes_name hd (filter_args_for_inv args td) end | T.Parse_if_else _ p q - | T.Parse_pair _ p q + | T.Parse_pair _ p q -> + typ_indexes_union (typ_indexes_of_parser p) (typ_indexes_of_parser q) + | T.Parse_dep_pair _ p (_, q) | T.Parse_dep_pair_with_refinement _ p _ (_, q) -> - typ_indexes_union (typ_indexes_of_parser p) (typ_indexes_of_parser q) + typ_indexes_union_l_bias (typ_indexes_of_parser p) (typ_indexes_of_parser q) | T.Parse_weaken_left p _ | T.Parse_weaken_right p _ @@ -300,18 +314,20 @@ let rec typ_indexes_of_parser (en:env) (p:T.parser) | T.Parse_dep_pair_with_action p (_, a) (_, q) | T.Parse_dep_pair_with_refinement_and_action _ p _ (_, a) (_, q) -> - typ_indexes_union (typ_indexes_of_parser p) - (typ_indexes_union (typ_indexes_of_action a) (typ_indexes_of_parser q)) + typ_indexes_union_l_bias (typ_indexes_of_parser p) + (typ_indexes_union_l_bias (typ_indexes_of_action a) (typ_indexes_of_parser q)) + + | T.Parse_with_action _ p a -> + typ_indexes_union_r_bias (typ_indexes_of_parser p) (typ_indexes_of_action a) - | T.Parse_with_action _ p a | T.Parse_with_dep_action _ p (_, a) -> - typ_indexes_union (typ_indexes_of_parser p) (typ_indexes_of_action a) + typ_indexes_union_l_bias (typ_indexes_of_parser p) (typ_indexes_of_action a) | T.Parse_string p _ -> typ_indexes_nil | T.Parse_refinement_with_action n p f (_, a) -> - typ_indexes_union (typ_indexes_of_parser p) (typ_indexes_of_action a) + typ_indexes_union_l_bias (typ_indexes_of_parser p) (typ_indexes_of_action a) | T.Parse_with_probe p _ _ dest -> let i, l, d, s = typ_indexes_of_parser p in @@ -773,12 +789,12 @@ let rec print_eloc mname (e:eloc) let rec print_disj mname (d:disj_pre) : ML string = match d with - | Disj_triv -> "None" - | Disj_pair i j -> Printf.sprintf "(Some (A.disjoint %s %s))" (print_eloc mname i) (print_eloc mname j) + | Disj_triv -> "disj_none" + | Disj_pair i j -> Printf.sprintf "(A.disjoint %s %s)" (print_eloc mname i) (print_eloc mname j) | Disj_conj i j -> Printf.sprintf "(join_disj %s %s)" (print_disj mname i) (print_disj mname j) - // | Disj_name hd args -> Printf.sprintf "(%s %s)" (print_derived_name mname "disj" hd) (print_args mname args) + | Disj_name hd args -> Printf.sprintf "(%s %s)" (print_derived_name mname "disj" hd) (print_args mname args) -let print_td_iface is_entrypoint mname root_name binders args typ_indexes_binders typ_indexes_args disj_index ar pk_wk pk_nz = +let print_td_iface is_entrypoint mname root_name binders args typ_indexes_binders typ_indexes_args ar pk_wk pk_nz = let kind_t = Printf.sprintf "[@@noextract_to \"krml\"]\n\ inline_for_extraction\n\ @@ -795,6 +811,13 @@ let print_td_iface is_entrypoint mname root_name binders args typ_indexes_binder root_name typ_indexes_binders in + let disj_t = + Printf.sprintf "[@@noextract_to \"krml\"]\n\ + noextract\n\ + val disj_%s %s : disj_index" + root_name + typ_indexes_binders + in let eloc_t = Printf.sprintf "[@@noextract_to \"krml\"]\n\ noextract\n\ @@ -805,12 +828,12 @@ let print_td_iface is_entrypoint mname root_name binders args typ_indexes_binder let def'_t = Printf.sprintf "[@@noextract_to \"krml\"]\n\ noextract\n\ - val def'_%s %s: typ kind_%s (inv_%s %s) (%s) (eloc_%s %s) %b" + val def'_%s %s: typ kind_%s (inv_%s %s) (disj_%s %s) (eloc_%s %s) %b" root_name binders root_name root_name typ_indexes_args - disj_index //root_name typ_indexes_args + root_name typ_indexes_args root_name typ_indexes_args ar in @@ -829,7 +852,7 @@ let print_td_iface is_entrypoint mname root_name binders args typ_indexes_binder binders root_name args in - String.concat "\n\n" [kind_t; inv_t; eloc_t; def'_t; validator_t; dtyp_t] + String.concat "\n\n" [kind_t; inv_t; disj_t; eloc_t; def'_t; validator_t; dtyp_t] let print_binders mname binders = List.map (print_param mname) binders |> @@ -906,14 +929,15 @@ let print_binding mname (td:type_decl) (T.print_kind mname k)] in let print_inv_or_eloc_or_disj = print_inv_or_eloc_or_disj mname tdn root_name binders in - let typ_indexes_of_binding, disj_index, fv_binders, fv_args = + let typ_indexes_of_binding, fv_binders, fv_args = let inv, eloc, disj, _ = td.typ_indexes in let fvs1 = free_vars_of_inv inv in let fvs2 = free_vars_of_disj disj in let fvs3 = free_vars_of_eloc eloc in let s0, _, _ = print_inv_or_eloc_or_disj "inv" None "A.slice_inv" (print_inv mname inv) (fvs1@fvs2@fvs3) in + let s1, _, _ = print_inv_or_eloc_or_disj "disj" None "disj_index" (print_disj mname disj) (fvs1@fvs2@fvs3) in let s2, fvb, fva = print_inv_or_eloc_or_disj "eloc" None "A.eloc" (print_eloc mname eloc) (fvs1@fvs2@fvs3) in - s0 ^ s2, print_disj mname disj, fvb, fva + s0 ^ s1 ^ s2, fvb, fva in let def' = OS.format @@ -1035,7 +1059,7 @@ let print_binding mname (td:type_decl) let iface = print_td_iface td.name.td_entrypoint mname root_name binders args - fv_binders fv_args disj_index td.allow_reading + fv_binders fv_args td.allow_reading weak_kind k.pk_nz in impl, iface diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst index 78a74f550..9c54a91a9 100644 --- a/src/3d/prelude/EverParse3d.Interpreter.fst +++ b/src/3d/prelude/EverParse3d.Interpreter.fst @@ -208,20 +208,15 @@ let leaf_reader #nz #wk (#k: P.parser_kind nz wk) #t (p:P.parser k t) (* Now, we can define the type of an environment *) module T = FStar.Tactics -let disj_index = option A.disjointness_pre - +let disj_index = A.disjointness_pre +let disj_none = A.disjointness_trivial [@@specialize] -let interp_disj_index = function - | None -> A.disjointness_trivial - | Some d -> d +let interp_disj_index x = x [@@specialize] let join_disj (d0 d1:disj_index) : disj_index - = match d0, d1 with - | None, d - | d, None -> d - | Some d0, Some d1 -> Some (A.conj_disjointness d0 d1) + = A.conj_disjointness d0 d1 (* global_binding: @@ -323,7 +318,7 @@ type dtyp dtyp (parser_kind_of_itype i) (allow_reader_of_itype i) A.true_inv - None + disj_none A.eloc_none | DT_App: @@ -460,45 +455,45 @@ type atomic_action | Action_return: #a:Type0 -> x:a -> - atomic_action A.true_inv None A.eloc_none false a + atomic_action A.true_inv disj_none A.eloc_none false a | Action_abort: - atomic_action A.true_inv None A.eloc_none false bool + atomic_action A.true_inv disj_none A.eloc_none false bool | Action_field_pos_64: - atomic_action A.true_inv None A.eloc_none false U64.t + atomic_action A.true_inv disj_none A.eloc_none false U64.t | Action_field_pos_32: squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagBuffer) -> - atomic_action A.true_inv None A.eloc_none false U32.t + atomic_action A.true_inv disj_none A.eloc_none false U32.t | Action_field_ptr: squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagBuffer) -> - atomic_action A.true_inv None A.eloc_none true A.___PUINT8 + atomic_action A.true_inv disj_none A.eloc_none true A.___PUINT8 | Action_field_ptr_after: squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagExtern) -> (sz: FStar.UInt64.t) -> write_to: A.bpointer A.___PUINT8 -> - atomic_action (A.ptr_inv write_to) None (A.ptr_loc write_to) false bool + atomic_action (A.ptr_inv write_to) disj_none (A.ptr_loc write_to) false bool | Action_field_ptr_after_with_setter: squash (EverParse3d.Actions.BackendFlag.backend_flag == A.BackendFlagExtern) -> (sz: FStar.UInt64.t) -> (#out_loc: A.eloc) -> write_to: (A.___PUINT8 -> Tot (A.external_action out_loc)) -> - atomic_action A.true_inv None out_loc false bool + atomic_action A.true_inv disj_none out_loc false bool | Action_deref: #a:Type0 -> x:A.bpointer a -> - atomic_action (A.ptr_inv x) None A.eloc_none false a + atomic_action (A.ptr_inv x) disj_none A.eloc_none false a | Action_assignment: #a:Type0 -> x:A.bpointer a -> rhs:a -> - atomic_action (A.ptr_inv x) None (A.ptr_loc x) false unit + atomic_action (A.ptr_inv x) disj_none (A.ptr_loc x) false unit | Action_call: #inv:A.slice_inv -> @@ -506,7 +501,7 @@ type atomic_action #b:bool -> #t:Type0 -> action_binding inv loc b t -> - atomic_action inv None loc b t + atomic_action inv disj_none loc b t | Action_probe_then_validate: #nz:bool -> @@ -522,7 +517,7 @@ type atomic_action dest:CP.copy_buffer_t -> probe:CP.probe_fn -> atomic_action (A.conj_inv inv (A.copy_buffer_inv dest)) - (join_disj disj (Some (A.disjoint (A.copy_buffer_loc dest) l))) + (join_disj disj (A.disjoint (A.copy_buffer_loc dest) l)) (A.eloc_union l (A.copy_buffer_loc dest)) true bool @@ -573,24 +568,24 @@ type action action i d l b t | Action_seq: - #i0:_ -> #l0:_ -> #b0:_ -> hd:atomic_action i0 None l0 b0 unit -> - #i1:_ -> #l1:_ -> #b1:_ -> #t:_ -> tl:action i1 None l1 b1 t -> - action (A.conj_inv i0 i1) None (A.eloc_union l0 l1) (b0 || b1) t + #i0:_ -> #l0:_ -> #b0:_ -> hd:atomic_action i0 disj_none l0 b0 unit -> + #i1:_ -> #l1:_ -> #b1:_ -> #t:_ -> tl:action i1 disj_none l1 b1 t -> + action (A.conj_inv i0 i1) disj_none (A.eloc_union l0 l1) (b0 || b1) t | Action_ite : hd:bool -> - #i0:_ -> #l0:_ -> #b0:_ -> #t:_ -> then_:(_:squash hd -> action i0 None l0 b0 t) -> - #i1:_ -> #l1:_ -> #b1:_ -> else_:(_:squash (not hd) -> action i1 None l1 b1 t) -> - action (A.conj_inv i0 i1) None (A.eloc_union l0 l1) (b0 || b1) t + #i0:_ -> #l0:_ -> #b0:_ -> #t:_ -> then_:(_:squash hd -> action i0 disj_none l0 b0 t) -> + #i1:_ -> #l1:_ -> #b1:_ -> else_:(_:squash (not hd) -> action i1 disj_none l1 b1 t) -> + action (A.conj_inv i0 i1) disj_none (A.eloc_union l0 l1) (b0 || b1) t | Action_let: - #i0:_ -> #l0:_ -> #b0:_ -> #t0:_ -> head:atomic_action i0 None l0 b0 t0 -> - #i1:_ -> #l1:_ -> #b1:_ -> #t1:_ -> k:(t0 -> action i1 None l1 b1 t1) -> - action (A.conj_inv i0 i1) None (A.eloc_union l0 l1) (b0 || b1) t1 + #i0:_ -> #l0:_ -> #b0:_ -> #t0:_ -> head:atomic_action i0 disj_none l0 b0 t0 -> + #i1:_ -> #l1:_ -> #b1:_ -> #t1:_ -> k:(t0 -> action i1 disj_none l1 b1 t1) -> + action (A.conj_inv i0 i1) disj_none (A.eloc_union l0 l1) (b0 || b1) t1 | Action_act: - #i0:_ -> #l0:_ -> #b0:_ -> act:action i0 None l0 b0 unit -> - action i0 None l0 b0 bool + #i0:_ -> #l0:_ -> #b0:_ -> act:action i0 disj_none l0 b0 unit -> + action i0 disj_none l0 b0 bool let _inv_implies_refl (inv: A.slice_inv) : Lemma (inv `A.inv_implies` inv) @@ -679,7 +674,7 @@ type typ Type = | T_false: fieldname:string -> - typ P.impos_kind A.true_inv None A.eloc_none true + typ P.impos_kind A.true_inv disj_none A.eloc_none true | T_denoted : fieldname:string -> @@ -708,7 +703,7 @@ type typ #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> #i2:_ -> #d2:_ -> #l2:_ -> #b2:bool -> //the first component is a pre-denoted type with a reader - t1:dtyp pk1 true i1 None l1 -> + t1:dtyp pk1 true i1 disj_none l1 -> //the second component is a function from denotations of t1 //that's why it's a small type, so that we can speak about its //denotation here @@ -737,7 +732,7 @@ type typ #i2:_ -> #l2:_ -> #b2:_ -> base:dtyp pk1 true i1 d1 l1 -> refinement:(dtyp_as_type base -> bool) -> - act:(dtyp_as_type base -> action i2 None l2 b2 bool) -> + act:(dtyp_as_type base -> action i2 disj_none l2 b2 bool) -> typ (P.filter_kind pk1) (A.conj_inv i1 i2) d1 (A.eloc_union l1 l2) false | T_dep_pair_with_refinement: @@ -752,7 +747,7 @@ type typ #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> //the first component is a pre-denoted type with a reader - base:dtyp pk1 true i1 None l1 -> + base:dtyp pk1 true i1 disj_none l1 -> //the second component is a function from denotations of base refinement:(dtyp_as_type base -> bool) -> k:(x:dtyp_as_type base { refinement x } -> typ pk2 i2 d2 l2 b2) -> @@ -769,9 +764,9 @@ type typ #nz2:_ -> #wk2:_ -> #pk2:P.parser_kind nz2 wk2 -> #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> #i3:_ -> #l3:_ -> #b3:_ -> - base:dtyp pk1 true i1 None l1 -> + base:dtyp pk1 true i1 disj_none l1 -> k:(x:dtyp_as_type base -> typ pk2 i2 d2 l2 b2) -> - act:(dtyp_as_type base -> action i3 None l3 b3 bool) -> + act:(dtyp_as_type base -> action i3 disj_none l3 b3 bool) -> typ (P.and_then_kind pk1 pk2) (A.conj_inv i1 (A.conj_inv i3 i2)) d2 @@ -791,11 +786,11 @@ type typ #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> #i3:_ -> #l3:_ -> #b3:_ -> //the first component is a pre-denoted type with a reader - base:dtyp pk1 true i1 None l1 -> + base:dtyp pk1 true i1 disj_none l1 -> //the second component is a function from denotations of base refinement:(dtyp_as_type base -> bool) -> k:(x:dtyp_as_type base { refinement x } -> typ pk2 i2 d2 l2 b2) -> - act:(dtyp_as_type base -> action i3 None l3 b3 bool) -> + act:(dtyp_as_type base -> action i3 disj_none l3 b3 bool) -> typ (P.and_then_kind (P.filter_kind pk1) pk2) (A.conj_inv i1 (A.conj_inv i3 i2)) d2 @@ -835,7 +830,7 @@ type typ #l1:_ -> #i1:_ -> #d1:_ -> #b1:_ -> #l2:_ -> #i2:_ -> #b2:_ -> base:typ pk i1 d1 l1 b1 -> - act:action i2 None l2 b2 bool -> + act:action i2 disj_none l2 b2 bool -> typ pk (A.conj_inv i1 i2) d1 (A.eloc_union l1 l2) false | T_with_dep_action: @@ -843,7 +838,7 @@ type typ #nz1:_ -> #pk1:P.parser_kind nz1 P.WeakKindStrongPrefix -> #i1:_ -> #l1:_ -> #i2:_ -> #d2:_ -> #l2:_ -> #b2:_ -> - head:dtyp pk1 true i1 None l1 -> + head:dtyp pk1 true i1 disj_none l1 -> act:(dtyp_as_type head -> action i2 d2 l2 b2 bool) -> typ pk1 (A.conj_inv i1 i2) d2 (A.eloc_union l1 l2) false @@ -882,9 +877,9 @@ type typ | T_string: fieldname:string -> #pk1:P.parser_kind true P.WeakKindStrongPrefix -> - element_type:dtyp pk1 true A.true_inv None A.eloc_none -> + element_type:dtyp pk1 true A.true_inv disj_none A.eloc_none -> terminator:dtyp_as_type element_type -> - typ P.parse_string_kind A.true_inv None A.eloc_none false + typ P.parse_string_kind A.true_inv disj_none A.eloc_none false [@@specialize] @@ -908,7 +903,7 @@ let t_probe_then_validate (td:dtyp pk has_reader i disj l) : typ (parser_kind_of_itype UInt64) (A.conj_inv i (A.copy_buffer_inv dest)) - (join_disj disj (Some (A.disjoint (A.copy_buffer_loc dest) l))) + (join_disj disj ( (A.disjoint (A.copy_buffer_loc dest) l))) (A.eloc_union l (A.copy_buffer_loc dest)) false = let t = diff --git a/src/3d/tests/Probe.3d b/src/3d/tests/Probe.3d index b78957344..e35521b18 100644 --- a/src/3d/tests/Probe.3d +++ b/src/3d/tests/Probe.3d @@ -1,6 +1,5 @@ extern probe ProbeAndCopy -export typedef struct _T { UINT32 x { x >= 17 }; UINT32 y { y >= x };