diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 8 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 12 |
2 files changed, 15 insertions, 5 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 2e46b120..9cc7c226 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -29,6 +29,7 @@ module SimpleNameOrd = struct end module SimpleNameMap = Collections.MakeMap (SimpleNameOrd) +module SimpleNameSet = Collections.MakeSet (SimpleNameOrd) (** Small utility to memoize some computations *) let mk_memoized (f : unit -> 'a) : unit -> 'a = @@ -374,6 +375,13 @@ let mk_builtin_funs_map () = let builtin_funs_map = mk_memoized mk_builtin_funs_map +let builtin_non_fallible_funs = + [ "alloc::boxed::Box::deref"; "alloc::boxed::Box::deref_mut" ] + +let builtin_non_fallible_funs_set = + SimpleNameSet.of_list + (List.map string_to_simple_name builtin_non_fallible_funs) + type builtin_trait_decl_info = { rust_name : string; extract_name : string; diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index a326d19e..f3e6cbe2 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1544,20 +1544,22 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl = | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> ( (* Lookup the function name *) let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in - match (Names.name_to_string def.name, rg_id) with - | "alloc::box::Boxed::deref", None -> + 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::box::Boxed::deref", Some _ -> + | "alloc::boxed::Box::deref", Some _ -> (* [Box::deref] backward is [()] (doesn't give back anything) *) assert (args = []); mk_unit_rvalue - | "alloc::box::Boxed::deref_mut", None -> + | "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::box::Boxed::deref_mut", Some _ -> + | "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 * *) |