From 467bed55b2d4469011b4da45491b26bcbd0796db Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 21 Nov 2024 17:25:54 -0800 Subject: [PATCH] Improve the treatment of abstract, polymorphic functions that are used with array types --- bin/main.ml | 4 +--- lib/Cleanup2.ml | 46 ---------------------------------------------- 2 files changed, 1 insertion(+), 49 deletions(-) diff --git a/bin/main.ml b/bin/main.ml index 85b84ab..9e81177 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -214,7 +214,6 @@ Supported options:|} Eurydice.Logging.log "Phase2.2" "%a" pfiles files; (* Sanity check for the big rewriting above. *) let errors, files = Krml.Checker.check_everything ~warn:true files in - Eurydice.Logging.log "Phase2.25" "%a" pfiles files; if errors then fail __FILE__ __LINE__; let files = Krml.Inlining.drop_unused files in @@ -230,12 +229,11 @@ Supported options:|} let files = Eurydice.Cleanup2.remove_trivial_into#visit_files () files in let files = Krml.Structs.pass_by_ref files in Eurydice.Logging.log "Phase2.5" "%a" pfiles files; - let files = Eurydice.Cleanup2.detect_array_returning_builtins#visit_files () files in + Eurydice.Logging.log "Phase2.6" "%a" pfiles files; let files = Eurydice.Cleanup2.remove_literals#visit_files () files in (* Eurydice does something more involved than krml and performs a conservative approximation of functions that are known to be pure readonly (i.e., functions that do not write to memory). *) - Eurydice.Logging.log "Phase2.6" "%a" pfiles files; fill_readonly_table files; let files = Krml.Simplify.optimize_lets files in (* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *) diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 7e60be9..ffd6129 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -618,52 +618,6 @@ let resugar_loops = end [@ocamlformat "disable"] -(* So I'm not entirely clear on the meaning of this phase, but I think two - things are simultaneously true: - - builtins (externals) have only one signature (duh), so if the pass_by_ref - phase rewrites the signature of an external like slice_index, then we're - toast! this will be a type error, so we need to undo some of the work of - pass_by_ref (this could be conceivably fixed on the krml side) - - MIR is aware of what in C is called array decay, and for instance, if x has - type &[[T; N]], then let y = &x[0] generates a simple index into x where y - has type T* (not type [T; N]) -- if there is a [T; N] involved, this is - represented in MIR by an &x[i] followed by an array-assignment, meaning - that there is nothing smart to be done here for slice indices, this is - already handled. - So, that's two good reasons to not bother rewriting the signature of - slice_index, even if the type of elements is an array. (Note: a previous - version of this wasn't aware of the second point and had a variant called - slice_index_outparam. Turns out this isn't necessary.) *) -let detect_array_returning_builtins = - object - inherit [_] map as super - - method! visit_ELet ((), _ as env) b e1 e2 = - match e1.node, e2.node with - (* let ret = $any; - Eurydice_slice_index (e_slice, e_index, ret); - e2 *) - | EAny, ESequence [ - { node = EApp ( - { node = ETApp ({ node = EQualified (["Eurydice"], "slice_index"); _ }, [], [], [ t_elements ]) as hd; _ }, - [ e_slice; e_index; { node = EBound 0; _ } ]); _ }; - e2 - ] -> - (* ret does not appear in the first two arguments of slice_index -- - shift them above the ret *) - let shift1 = Krml.DeBruijn.subst Krml.Helpers.eunit 0 in - let e_slice = shift1 e_slice in - let e_index = shift1 e_index in - let t_hd = Krml.DeBruijn.subst_t t_elements 0 Builtin.slice_index.typ in - let e_slice_index = with_type t_elements (EApp (with_type t_hd hd, [ e_slice; e_index ])) in - (* now substitute *) - (Krml.DeBruijn.subst e_slice_index 0 e2).node - - | _ -> - super#visit_ELet env b e1 e2 -end -[@ocamlformat "disable"] - let improve_names files = let renamed = Hashtbl.create 41 in let allocated = Hashtbl.create 41 in