From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/PureMicroPasses.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index f3e6cbe2..d62a028e 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -791,7 +791,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) let id0 = match id0 with | FunId fun_id -> fun_id - | TraitMethod (_, _, fun_decl_id) -> Regular fun_decl_id + | TraitMethod (_, _, fun_decl_id) -> FRegular fun_decl_id in LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls in @@ -1527,7 +1527,7 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = * could have: [box_new f x]) * *) match fun_id with - | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (FAssumed aid), _lp_id, rg_id)) -> ( match (aid, rg_id) with | BoxNew, _ -> assert (rg_id = None); @@ -1541,7 +1541,7 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | ArrayRepeat | SliceLen ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in match @@ -2050,7 +2050,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) : let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in assert (Option.is_some decl.loop_id); - let fun_id = (E.Regular decl.def_id, decl.loop_id) in + let fun_id = (E.FRegular decl.def_id, decl.loop_id) in let set_used vid = used := List.map (fun (vid', b) -> (vid', b || vid = vid')) !used @@ -2134,7 +2134,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) : (* We then apply the filtering to all the function definitions at once *) let filter_in_one (decl : fun_decl) : fun_decl = (* Filter the function signature *) - let fun_id = (E.Regular decl.def_id, decl.loop_id) in + let fun_id = (E.FRegular decl.def_id, decl.loop_id) in let decl = match FunLoopIdMap.find_opt fun_id !used_map with | None -> (* Nothing to filter *) decl -- cgit v1.2.3 From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:04:11 +0100 Subject: Prefix variants related to types with "T" --- compiler/PureMicroPasses.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index d62a028e..8872571f 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -582,7 +582,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = match app.e with | Qualif { - id = AdtCons { adt_id = AdtId adt_id; variant_id = None }; + id = AdtCons { adt_id = TAdtId adt_id; variant_id = None }; generics = _; } -> (* Lookup the def *) @@ -606,7 +606,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = (!Config.backend <> Lean && !Config.backend <> Coq) || not is_rec then - let struct_id = AdtId adt_id in + let struct_id = TAdtId adt_id in let init = None in let updates = FieldId.mapi @@ -1085,7 +1085,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = match app.e with | Qualif { - id = AdtCons { adt_id = AdtId adt_id; variant_id = None }; + id = AdtCons { adt_id = TAdtId adt_id; variant_id = None }; generics; } -> (* This is a struct *) @@ -1114,7 +1114,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = | ( Qualif { id = - Proj { adt_id = AdtId proj_adt_id; field_id }; + Proj { adt_id = TAdtId proj_adt_id; field_id }; generics = proj_generics; }, Var v ) -> @@ -1157,13 +1157,13 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = match (proj.e, x.e) with | ( Qualif { - id = Proj { adt_id = AdtId proj_adt_id; field_id }; + id = Proj { adt_id = TAdtId proj_adt_id; field_id }; generics = _; }, Var v ) -> (* We check that this is the proper ADT, and the proper field *) if - AdtId proj_adt_id = struct_id + TAdtId proj_adt_id = struct_id && field_id = fid && x.ty = adt_ty then Some v else None -- cgit v1.2.3 From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 13 Nov 2023 13:27:02 +0100 Subject: Add RegionsHierarchy.ml --- compiler/PureMicroPasses.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 8872571f..d2747a4b 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -786,18 +786,19 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) if rg_id0 = rg_id1 then true else (* We need to use the regions hierarchy *) - (* First, lookup the signature of the LLBC function *) - let sg = + let regions_hierarchy = let id0 = match id0 with | FunId fun_id -> fun_id | TraitMethod (_, _, fun_decl_id) -> FRegular fun_decl_id in - LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls + LlbcAstUtils.FunIdMap.find id0 + ctx.fun_ctx.regions_hierarchies in (* Compute the set of ancestors of the function in call1 *) let call1_ancestors = - LlbcAstUtils.list_ancestor_region_groups sg rg_id1 + LlbcAstUtils.list_ancestor_region_groups regions_hierarchy + rg_id1 in (* Check if the function used in call0 is inside *) T.RegionGroupId.Set.mem rg_id0 call1_ancestors -- cgit v1.2.3 From a27efd1ed08bc9583752445d9eda7a693c0c7379 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Nov 2023 10:13:28 +0100 Subject: Finish propagating the changes to the names and cleaning --- compiler/PureMicroPasses.ml | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index d2747a4b..2106c206 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -3,10 +3,13 @@ open Pure open PureUtils open TranslateCore -module V = Values (** The local logger *) -let log = L.pure_micro_passes_log +let log = Logging.pure_micro_passes_log + +let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = + let fmt = trans_ctx_to_pure_fmt_env ctx in + PrintPure.fun_decl_to_string fmt def (** Small utility. @@ -597,8 +600,8 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = match TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls_groups with - | NonRec _ -> false - | Rec _ -> true + | NonRecGroup _ -> false + | RecGroup _ -> true in (* Convert, if possible - note that for now for Lean and Coq we don't support the structure syntax on recursive structures *) @@ -1420,14 +1423,15 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let loop_body = { inputs; inputs_lvs; body = loop_body } in - let loop_def = + let loop_def : fun_decl = { def_id = def.def_id; kind = def.kind; num_loops; loop_id = Some loop.loop_id; back_id = def.back_id; - basename = def.basename; + llbc_name = def.llbc_name; + name = def.name; signature = loop_sig; is_global_decl_body = def.is_global_decl_body; body = Some loop_body; @@ -1539,10 +1543,12 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = mk_unit_rvalue | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut - | ArrayRepeat | SliceLen ), + | ArrayRepeat ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( + | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> + failwith "TODO" + (* (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in match @@ -1570,7 +1576,8 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | _ -> raise (Failure "Unreachable") in mk_apps arg args - | _ -> super#visit_texpression env e) + | _ -> super#visit_texpression env e + *) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end @@ -1918,9 +1925,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : (* Debug *) log#ldebug (lazy - ("PureMicroPasses.apply_passes_to_def: " - ^ Print.fun_name_to_string def.basename - ^ " (" + ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " (" ^ Print.option_to_string T.RegionGroupId.to_string def.back_id ^ ")")); -- cgit v1.2.3 From 9ab6a034aaadacac62d241474af3cf28bf6ac928 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 16 Nov 2023 10:52:28 +0100 Subject: Update SymbolicToPure.eliminate_box_functions --- compiler/PureMicroPasses.ml | 75 +++++++++++++++++++++++++++------------------ 1 file changed, 45 insertions(+), 30 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 2106c206..50a50815 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1546,38 +1546,53 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | ArrayRepeat ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> - failwith "TODO" - (* + | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( + (* TODO: use a more general matching mechanism *) (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in - match - (Names.name_no_disambiguators_to_string def.name, rg_id) - with - | "alloc::boxed::Box::deref", None -> - (* [Box::deref] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "alloc::boxed::Box::deref", Some _ -> - (* [Box::deref] backward is [()] (doesn't give back anything) *) - assert (args = []); - mk_unit_rvalue - | "alloc::boxed::Box::deref_mut", None -> - (* [Box::deref_mut] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "alloc::boxed::Box::deref_mut", Some _ -> - (* [Box::deref_mut] back is almost the identity: - * let box_deref_mut (x_init : t) (x_back : t) : t = x_back - * *) - let arg, args = - match args with - | _ :: given_back :: args -> (given_back, args) - | _ -> raise (Failure "Unreachable") - in - mk_apps arg args - | _ -> super#visit_texpression env e - *) + (* We first need to check if the name is "alloc::boxed::Box::_" *) + match def.name with + | [ + PeIdent ("alloc", _); + PeIdent ("boxed", _); + PeImpl impl; + PeIdent (fname, _); + ] -> ( + match impl.ty with + | TAdt + ( TAssumed TBox, + { + regions = []; + types = [ TVar _ ]; + const_generics = []; + trait_refs = []; + } ) -> ( + match (fname, rg_id) with + | "deref", None -> + (* [Box::deref] forward is the identity *) + let arg, args = Collections.List.pop args in + mk_apps arg args + | "deref", Some _ -> + (* [Box::deref] backward is [()] (doesn't give back anything) *) + assert (args = []); + mk_unit_rvalue + | "deref_mut", None -> + (* [Box::deref_mut] forward is the identity *) + let arg, args = Collections.List.pop args in + mk_apps arg args + | "deref_mut", Some _ -> + (* [Box::deref_mut] back is almost the identity: + * let box_deref_mut (x_init : t) (x_back : t) : t = x_back + * *) + let arg, args = + match args with + | _ :: given_back :: args -> (given_back, args) + | _ -> raise (Failure "Unreachable") + in + mk_apps arg args + | _ -> super#visit_texpression env e) + | _ -> super#visit_texpression env e) + | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end -- cgit v1.2.3 From 5aa37b3a0a539f9ae37a119b9ce7c8dee504125e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 22:38:58 +0100 Subject: Fix minor issues --- compiler/PureMicroPasses.ml | 66 +++++++++------------------------------------ 1 file changed, 13 insertions(+), 53 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 50a50815..96421925 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1250,6 +1250,7 @@ let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option = !Config.filter_useless_functions && Option.is_some def.back_id && def.signature.output = mk_result_ty mk_unit_ty + || def.signature.output = mk_unit_ty then None else Some def @@ -1508,8 +1509,8 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl = let body = Some { body with body = body_exp; inputs_lvs } in { def with body } -(** Eliminate the box functions like [Box::new], [Box::deref], etc. Most of them - are translated to identity, and [Box::free] is translated to [()]. +(** Eliminate the box functions like [Box::new] (which is translated to the + identity) and [Box::free] (which is translated to [()]). Note that the box types have already been eliminated during the translation from symbolic to pure. @@ -1518,7 +1519,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl = function calls, and when translating end abstractions. Here, we can do something simpler, in one micro-pass. *) -let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = +let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = (* The map visitor *) let obj = object @@ -1546,53 +1547,6 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | ArrayRepeat ), _ ) -> super#visit_texpression env e) - | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> ( - (* TODO: use a more general matching mechanism *) - (* Lookup the function name *) - let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in - (* We first need to check if the name is "alloc::boxed::Box::_" *) - match def.name with - | [ - PeIdent ("alloc", _); - PeIdent ("boxed", _); - PeImpl impl; - PeIdent (fname, _); - ] -> ( - match impl.ty with - | TAdt - ( TAssumed TBox, - { - regions = []; - types = [ TVar _ ]; - const_generics = []; - trait_refs = []; - } ) -> ( - match (fname, rg_id) with - | "deref", None -> - (* [Box::deref] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "deref", Some _ -> - (* [Box::deref] backward is [()] (doesn't give back anything) *) - assert (args = []); - mk_unit_rvalue - | "deref_mut", None -> - (* [Box::deref_mut] forward is the identity *) - let arg, args = Collections.List.pop args in - mk_apps arg args - | "deref_mut", Some _ -> - (* [Box::deref_mut] back is almost the identity: - * let box_deref_mut (x_init : t) (x_back : t) : t = x_back - * *) - let arg, args = - match args with - | _ :: given_back :: args -> (given_back, args) - | _ -> raise (Failure "Unreachable") - in - mk_apps arg args - | _ -> super#visit_texpression env e) - | _ -> super#visit_texpression env e) - | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e) | _ -> super#visit_texpression env e end @@ -1966,11 +1920,17 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : * Note that the calls to those functions should already have been removed, * when translating from symbolic to pure. Here, we remove the definitions * altogether, because they are now useless *) - let def = filter_if_backward_with_no_outputs def in + let name = def.name ^ PrintPure.fun_suffix def.loop_id def.back_id in + let opt_def = filter_if_backward_with_no_outputs def in - match def with - | None -> None + match opt_def with + | None -> + log#ldebug (lazy ("filtered (backward with no outputs): " ^ name ^ "\n")); + None | Some def -> + log#ldebug + (lazy ("not filtered (not backward with no outputs): " ^ name ^ "\n")); + (* Extract the loop definitions by removing the {!Loop} node *) let def, loops = decompose_loops def in -- cgit v1.2.3 From e94cd72ffa63dbc5fc40c7c1a422c1a70ba4a7e5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 13:55:46 +0100 Subject: Add an `is_local` field to declarations --- compiler/PureMicroPasses.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 96421925..1565f252 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1427,6 +1427,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let loop_def : fun_decl = { def_id = def.def_id; + is_local = def.is_local; kind = def.kind; num_loops; loop_id = Some loop.loop_id; -- cgit v1.2.3 From 77ba13b371cccbe8098e432ebd287108d5373666 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 14:43:12 +0100 Subject: Add span information to the generated code --- compiler/PureMicroPasses.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 1565f252..8463f56c 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -391,7 +391,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | Switch (scrut, body) -> update_switch_body scrut body ctx | Loop loop -> update_loop loop ctx | StructUpdate supd -> update_struct_update supd ctx - | Meta (meta, e) -> update_meta meta e ctx + | Meta (meta, e) -> update_emeta meta e ctx in (ctx, { e; ty }) (* *) @@ -449,6 +449,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let { fun_end; loop_id; + meta; fuel0; fuel; input_state; @@ -467,6 +468,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = { fun_end; loop_id; + meta; fuel0; fuel; input_state; @@ -490,7 +492,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let supd = { struct_id; init; updates } in (ctx, StructUpdate supd) (* *) - and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) : + and update_emeta (meta : emeta) (e : texpression) (ctx : pn_ctx) : pn_ctx * expression = let ctx = match meta with @@ -516,7 +518,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | Tag _ -> ctx in let ctx, e = update_texpression e ctx in - let e = mk_meta meta e in + let e = mk_emeta meta e in (ctx, e.e) in @@ -1428,6 +1430,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = { def_id = def.def_id; is_local = def.is_local; + meta = loop.meta; kind = def.kind; num_loops; loop_id = Some loop.loop_id; -- cgit v1.2.3 From ba66f35a0e196c17757e06187cf2563abec253e5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 22 Nov 2023 09:09:46 +0100 Subject: Improve further the generation of parent clause/trait clause names --- compiler/PureMicroPasses.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'compiler/PureMicroPasses.ml') diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 8463f56c..d0741b29 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1364,6 +1364,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let loop_sig = { generics = fun_sig.generics; + llbc_generics = fun_sig.llbc_generics; preds = fun_sig.preds; inputs = inputs_tys; output; @@ -2127,7 +2128,8 @@ let filter_loop_inputs (transl : pure_fun_translation list) : let num_filtered = List.length (List.filter (fun b -> not b) used_info) in - let { generics; preds; inputs; output; doutputs; info } = + let { generics; llbc_generics; preds; inputs; output; doutputs; info } + = decl.signature in let { @@ -2155,7 +2157,9 @@ let filter_loop_inputs (transl : pure_fun_translation list) : effect_info; } in - let signature = { generics; preds; inputs; output; doutputs; info } in + let signature = + { generics; llbc_generics; preds; inputs; output; doutputs; info } + in { decl with signature } in -- cgit v1.2.3