Merge remote-tracking branch 'origin/protz_better_debug' into protz_c…

…omments

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) ();