diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index 78e386b4..e5ee7951 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -16,6 +16,52 @@ module K = Constant concrete type arguments `ts` and expression arguments `cgs`, this module picks a name and records that information in a global state. *) +let explanation = {|Some debug info to figure out what the hash codes correspond to... + +"trait impl" means that the charon-provided name includes the name of the trait +implementation block that this function was defined in -- this is typically a +rather long name, so here we simply feed the string through a hash function to +compute a unique two-byte code that allows shortening the function name +(otherwise, the C code would be pretty unreadable) + +the other case is for parameterized types and functions +- for types, we need to monomorphize a type according to the choice of type and + const generic arguments; to avoid a long name, we simply feed those arguments + into a hash function and take a two-byte unique suffix +- for functions, we need to monomorphize the function according to the choice of + type, const generic arguments, and the choice of trait implementation (which + internally amounts to passing a function pointer for each one of the + implementation methods in the chosen trait); those are also fed into the hash + function to compute a two-byte unique suffix + +because of this, the suffixes are identical if, say, two functions rely on the +same set of monomorphization parameters, or originate from the same trait impl + +-------------------------------------------------------------------------------- + +|} + + +let maybe_debug_hash = + let oc = ref None in + let seen = Hashtbl.create 41 in + let printed_info = ref false in + let open_out () = + match !oc with + | Some oc -> oc + | None -> let s = open_out_bin "hash_map" in oc := Some s; s + in + fun hash pretty -> + if Options.debug "hashes" && not (Hashtbl.mem seen hash) then begin + if not !printed_info then + output_string (open_out ()) explanation; + printed_info := true; + KPrint.bfprintf (open_out ()) "%02x --> %a\n\n" + (hash land 0xFF) + PrintCommon.pdoc (Lazy.force pretty); + Hashtbl.add seen hash () + end + module NameGen = struct open PPrint @@ -72,14 +118,32 @@ module NameGen = struct in Common.Comment (KPrint.bsprintf "%a" PrintCommon.pdoc comment) - let gen_lid lid ts extra = + let gen_lid lid ts (extra: extra) = if !short_names then if lid = tuple_lid && List.for_all ((=) (List.hd ts)) ts then let n = KPrint.bsprintf "%a_x%d" ptyp (List.hd ts) (List.length ts) in ([], n), [ Common.AutoGenerated ] else let m, n = if lid = tuple_lid then [], "tuple" else lid in - let hash = Hashtbl.hash (ts, extra) in + (* Skip binders that are there for debugging only. *) + let hash = match extra with + | Cg cgs -> Hashtbl.hash (ts, cgs) + | Expr (n_cgs, cgs, _) -> Hashtbl.hash (ts, (n_cgs, cgs)) + in + (* Big debug smorgasbord *) + maybe_debug_hash hash (lazy ( + let open PPrint in + let open PrintAst in + string "type arguments" ^^ hardline ^^ + (if ts = [] then string "no types" else separate_map hardline print_typ ts) ^^ hardline ^^ + match extra with + | Expr (n_cgs, es, _bs) -> + string "(expr)" ^/^ string (string_of_int n_cgs) ^/^ string "const generics, followed by trait method impl arguments" ^^ hardline ^^ + separate_map hardline print_expr es + | Cg cgs -> + string "(type) const generics" ^^ hardline ^^ separate_map hardline print_cg cgs + )); + (* Actual Logic *) let n = Printf.sprintf "%s_%02x" n (hash land 0xFF) in let n = Idents.mk_fresh n (fun n -> Hashtbl.mem seen (m, n)) in Hashtbl.add seen (m, n) ();