Merge pull request #1054 from Nadrieril/intern-defid

Intern `DefId`s

engine/lib/concrete_ident/concrete_ident.ml

@@ -27,7 +27,7 @@ module Imported = struct
   [@@deriving show, yojson, compare, sexp, eq, hash]
 
   let of_def_path_item : Types.def_path_item -> def_path_item = function
-    | CrateRoot -> CrateRoot
+    | CrateRoot _ -> CrateRoot
     | Impl -> Impl
     | ForeignMod -> ForeignMod
     | Use -> Use
@@ -50,7 +50,8 @@ module Imported = struct
       disambiguator = MyInt64.to_int_exn disambiguator;
     }
 
-  let of_def_id Types.{ krate; path; _ } =
+  let of_def_id
+      ({ contents = { value = { krate; path; _ }; _ } } : Types.def_id) =
     { krate; path = List.map ~f:of_disambiguated_def_path_item path }
 
   let parent { krate; path; _ } = { krate; path = List.drop_last_exn path }
@@ -279,7 +280,7 @@ module View = struct
           namespace
         |> some_if_true
       in
-      let* last = List.last def_id.path in
+      let* last = List.last def_id.contents.value.path in
       let* () = some_if_true Int64.(last.disambiguator = zero) in
       last.data |> Imported.of_def_path_item |> string_of_def_path_item
       |> Option.map ~f:escape
@@ -387,7 +388,7 @@ module View = struct
                   namespace
            in
            let* typ = simple_ty_to_string ~namespace typ in
-           let* trait = List.last trait.path in
+           let* trait = List.last trait.contents.value.path in
            let* trait =
              Imported.of_def_path_item trait.data |> string_of_def_path_item
            in

engine/lib/import_thir.ml

@@ -1310,7 +1310,7 @@ let make ~krate : (module EXPR) =
   (module M)
 
 let c_trait_item (item : Thir.trait_item) : trait_item =
-  let open (val make ~krate:item.owner_id.krate : EXPR) in
+  let open (val make ~krate:item.owner_id.contents.value.krate : EXPR) in
   let { params; constraints } = c_generics item.generics in
   (* TODO: see TODO in impl items *)
   let ti_ident = Concrete_ident.of_def_id Field item.owner_id in
@@ -1449,7 +1449,7 @@ let rec c_item ~ident ~drop_body (item : Thir.item) : item list =
     [ make_hax_error_item span ident error ]
 
 and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
-  let open (val make ~krate:item.owner_id.krate : EXPR) in
+  let open (val make ~krate:item.owner_id.contents.value.krate : EXPR) in
   if should_skip item.attributes then []
   else
     let span = Span.of_thir item.span in
@@ -1758,15 +1758,21 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
         (* TODO: is this DUMMY thing really needed? there's a `Use` segment (see #272) *)
         let def_id = item.owner_id in
         let def_id : Types.def_id =
-          {
-            def_id with
-            path =
-              def_id.path
-              @ [
-                  Types.
-                    { data = ValueNs "DUMMY"; disambiguator = MyInt64.of_int 0 };
-                ];
-          }
+          let value =
+            {
+              def_id.contents.value with
+              path =
+                def_id.contents.value.path
+                @ [
+                    Types.
+                      {
+                        data = ValueNs "DUMMY";
+                        disambiguator = MyInt64.of_int 0;
+                      };
+                  ];
+            }
+          in
+          { contents = { def_id.contents with value } }
         in
         [ { span; v; ident = Concrete_ident.of_def_id Value def_id; attrs } ]
     | Union _ ->

engine/names/extract/build.rs

@@ -10,6 +10,25 @@ use std::process::{Command, Stdio};
 mod hax_frontend_exporter_def_id;
 use hax_frontend_exporter_def_id::*;
 
+mod id_table {
+    //! Shim to make `def_id.rs` build. Replaces the `id_table` interner with a plain `Arc`.
+    use serde::{Deserialize, Serialize};
+    use std::sync::Arc;
+
+    #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
+    pub struct Node<T> {
+        value: Arc<T>,
+        cache_id: u32,
+    }
+
+    impl<T> std::ops::Deref for Node<T> {
+        type Target = T;
+        fn deref(&self) -> &Self::Target {
+            self.value.as_ref()
+        }
+    }
+}
+
 /// Name of the current crate
 const HAX_ENGINE_NAMES_CRATE: &str = "hax_engine_names";
 /// Path `a::b` needs to be compiled to a OCaml variant name, `::` is
@@ -40,7 +59,7 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
         | DefPathItem::ValueNs(s)
         | DefPathItem::MacroNs(s)
         | DefPathItem::LifetimeNs(s) => s,
-        DefPathItem::CrateRoot => "CrateRoot".into(),
+        DefPathItem::CrateRoot { name } => uppercase_first_letter(&name),
         DefPathItem::Impl => "Impl".into(),
         DefPathItem::ForeignMod => "ForeignMod".into(),
         DefPathItem::Use => "Use".into(),
@@ -53,23 +72,29 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
     }
 }
 
-fn disambiguated_def_path_item_to_str(defpath: DisambiguatedDefPathItem) -> String {
-    let data = def_path_item_to_str(defpath.data);
+fn disambiguated_def_path_item_to_str(defpath: &DisambiguatedDefPathItem) -> String {
+    let data = def_path_item_to_str(defpath.data.clone());
     let disambiguator = disambiguator_to_str(defpath.disambiguator);
     format!("{data}{disambiguator}")
 }
 
-fn def_id_to_str(DefId { krate, path, .. }: &mut DefId) -> String {
-    if krate == HAX_ENGINE_NAMES_CRATE {
-        *krate = "rust_primitives".into();
+fn def_id_to_str(def_id: &DefId) -> (Value, String) {
+    let crate_name = if def_id.krate == HAX_ENGINE_NAMES_CRATE {
+        "rust_primitives"
+    } else {
+        &def_id.krate
     };
-    let path = path
-        .clone()
+    // Update the crate name in the json output as well.
+    let mut json = serde_json::to_value(def_id).unwrap();
+    json["contents"]["value"]["krate"] = Value::String(crate_name.to_owned());
+
+    let crate_name = uppercase_first_letter(crate_name);
+    let path = [crate_name]
         .into_iter()
-        .map(disambiguated_def_path_item_to_str)
+        .chain(def_id.path.iter().map(disambiguated_def_path_item_to_str))
         .collect::<Vec<String>>()
         .join(SEPARATOR);
-    format!("{}{SEPARATOR}{path}", uppercase_first_letter(&krate))
+    (json, path)
 }
 
 fn reader_to_str(s: String) -> String {
@@ -82,9 +107,9 @@ fn reader_to_str(s: String) -> String {
 
     let def_ids = def_ids
         .into_iter()
-        .map(|mut did| {
-            let krate_name = def_id_to_str(&mut did);
-            (serde_json::to_string(&did).unwrap(), krate_name)
+        .map(|did| {
+            let (json, krate_name) = def_id_to_str(&did);
+            (serde_json::to_string(&json).unwrap(), krate_name)
         })
         .collect::<Vec<_>>();
 

engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js

@@ -538,8 +538,8 @@ function run(str){
 [@@@warning "-A"]`;
 
     let items = Object.entries(definitions)
-        .map(([name, def]) =>
-            [name == 'Node_for_TyKind' ? 'node_for_ty_kind_generated' : name, def])
+        .map(([name, def]) => ['Node_for_TyKind' == name ? 'node_for_ty_kind_generated' : name, def])
+        .map(([name, def]) => ['Node_for_DefIdContents' == name ? 'node_for_def_id_contents_generated' : name, def])
         .map(
             ([name, def]) => export_definition(name, def)
         ).filter(x => x instanceof Object);
@@ -573,44 +573,69 @@ open ParseError
     );
     impl += `
 and node_for__ty_kind = node_for_ty_kind_generated
+and node_for__def_id_contents = node_for_def_id_contents_generated
 
-let cache_map: (int64, ${"[ `TyKind of ty_kind | `JSON of Yojson.Safe.t ]"}) Base.Hashtbl.t = Base.Hashtbl.create (module Base.Int64)
+type map_types = ${"[`TyKind of ty_kind | `DefIdContents of def_id_contents]"}
+let cache_map: (int64, ${"[ `Value of map_types | `JSON of Yojson.Safe.t ]"}) Base.Hashtbl.t = Base.Hashtbl.create (module Base.Int64)
 
-`;
-    impl += ('');
-    impl += ('let rec ' + items.map(({name, type, parse}) =>
-        `parse_${name} (o: Yojson.Safe.t): ${name} = ${parse}`
-    ).join('\nand '));
-    impl += `
-and parse_node_for__ty_kind (o: Yojson.Safe.t): node_for__ty_kind = match o with
+let parse_table_id_node (type t) (name: string) (encode: t -> map_types) (decode: map_types -> t option) (parse: Yojson.Safe.t -> t) (o: Yojson.Safe.t): (t * int64) =
+    let label = "parse_table_id_node:" ^ name ^ ": " in
+    match o with
     | \`Assoc alist -> begin
-          let id = match List.assoc "cache_id" alist with
-            | \`Int id -> Base.Int.to_int64 id
-            | \`Intlit lit -> (try Base.Int64.of_string lit with | _ -> failwith ("Base.Int64.of_string failed for " ^ lit))
-            | bad_json -> failwith ("parse_node_for__ty_kind: id was expected to be an int, got: " ^ Yojson.Safe.pretty_to_string bad_json ^ "\n\n\nfull json: " ^ Yojson.Safe.pretty_to_string o)
+          let id = match List.assoc_opt "cache_id" alist with
+            | Some (\`Int id) -> Base.Int.to_int64 id
+            | Some (\`Intlit lit) -> (try Base.Int64.of_string lit with | _ -> failwith (label ^ "Base.Int64.of_string failed for " ^ lit))
+            | Some bad_json -> failwith (label ^ "id was expected to be an int, got: " ^ Yojson.Safe.pretty_to_string bad_json ^ "\n\n\nfull json: " ^ Yojson.Safe.pretty_to_string o)
+            | None -> failwith (label ^ " could not find the key 'cache_id' in the following json: " ^ Yojson.Safe.pretty_to_string o)
           in
+          let decode v = decode v |> Base.Option.value_exn ~message:(label ^ "could not decode value (wrong type)") in
           match List.assoc_opt "value" alist with
           | Some json when (match json with \`Null -> false | _ -> true) ->
-            let value = parse_ty_kind json in
-            {value; id}
+            (parse json, id)
           | _ ->
             let value = match Base.Hashtbl.find cache_map id with
-            | None -> failwith ("parse_node_for__ty_kind: failed to lookup id " ^ Base.Int64.to_string id)
-            | Some (\`TyKind v) -> v
+            | None -> failwith (label ^ "failed to lookup id " ^ Base.Int64.to_string id)
+            | Some (\`Value v) -> decode v
             | Some (\`JSON json) ->
-                let v = parse_ty_kind json in
-                Base.Hashtbl.set cache_map ~key:id ~data:(\`TyKind v);
-                v
-            in {value; id}
+                let value = parse json in
+                Base.Hashtbl.set cache_map ~key:id ~data:(\`Value (encode value));
+                value
+            in (value, id)
        end
-    | _ -> failwith "parse_node_for__ty_kind: expected Assoc"
+    | _ -> failwith (label ^ "expected Assoc")
+
+`;
+    impl += ('');
+    impl += ('let rec ' + items.map(({name, type, parse}) =>
+        `parse_${name} (o: Yojson.Safe.t): ${name} = ${parse}`
+    ).join('\nand '));
+    impl += `
+and parse_node_for__ty_kind (o: Yojson.Safe.t): node_for__ty_kind =
+   let (value, id) =
+       parse_table_id_node "TyKind"
+           (fun value -> \`TyKind value)
+           (function | \`TyKind value -> Some value | _ -> None)
+           parse_ty_kind
+           o
+   in
+   {value; id}
+and parse_node_for__def_id_contents (o: Yojson.Safe.t): node_for__def_id_contents =
+   let (value, id) =
+       parse_table_id_node "DefIdContents"
+           (fun value -> \`DefIdContents value)
+           (function | \`DefIdContents value -> Some value | _ -> None)
+           parse_def_id_contents
+           o
+   in
+   {value; id}
 `;
     impl += ('');
     impl += ('let rec ' + items.map(({name, type, parse, to_json}) =>
         `to_json_${name} (o: ${name}): Yojson.Safe.t = ${to_json}`
     ).join('\nand '));
     impl += `
 and to_json_node_for__ty_kind {value; id} = to_json_node_for_ty_kind_generated {value; id}
+and to_json_node_for__def_id_contents {value; id} = to_json_node_for_def_id_contents_generated {value; id}
 `;
 
 

frontend/exporter/src/id_table.rs

@@ -47,6 +47,7 @@ impl Session {
 #[derive(Debug, Clone, Deserialize, Serialize)]
 pub enum Value {
     Ty(Arc<TyKind>),
+    DefId(Arc<DefIdContents>),
 }
 
 impl SupportedType<Value> for TyKind {
@@ -56,6 +57,19 @@ impl SupportedType<Value> for TyKind {
     fn from_types(t: &Value) -> Option<Arc<Self>> {
         match t {
             Value::Ty(value) => Some(value.clone()),
+            _ => None,
+        }
+    }
+}
+
+impl SupportedType<Value> for DefIdContents {
+    fn to_types(value: Arc<Self>) -> Value {
+        Value::DefId(value)
+    }
+    fn from_types(t: &Value) -> Option<Arc<Self>> {
+        match t {
+            Value::DefId(value) => Some(value.clone()),
+            _ => None,
         }
     }
 }
@@ -69,6 +83,13 @@ pub struct Node<T: 'static + SupportedType<Value>> {
     value: Arc<T>,
 }
 
+impl<T: SupportedType<Value>> std::ops::Deref for Node<T> {
+    type Target = T;
+    fn deref(&self) -> &Self::Target {
+        self.value.as_ref()
+    }
+}
+
 /// Hax relies on hashes being deterministic for predicates
 /// ids. Identifiers are not deterministic: we implement hash for
 /// `Node` manually, discarding the field `id`.
@@ -158,13 +179,14 @@ impl Session {
     }
 }
 
-impl<T: Sync + Send + Clone + 'static + SupportedType<Value>> Node<T> {
+impl<T: Sync + Send + 'static + SupportedType<Value>> Node<T> {
     pub fn new(value: T, session: &mut Session) -> Self {
         let id = session.fresh_id();
-        let kind = Arc::new(value);
-        session.table.0.insert(id.clone(), kind.clone());
-        Self { id, value: kind }
+        let value = Arc::new(value);
+        session.table.0.insert(id.clone(), value.clone());
+        Self { id, value }
     }
+
     pub fn inner(&self) -> &Arc<T> {
         &self.value
     }

frontend/exporter/src/rustc_utils.rs

@@ -39,19 +39,16 @@ pub(crate) fn get_variant_information<'s, S: UnderOwnerState<'s>>(
         typ: constructs_type.clone(),
         variant: variant.sinto(s),
         kind,
-        type_namespace: DefId {
-            path: match constructs_type.path.as_slice() {
-                [init @ .., _] => init.to_vec(),
-                _ => {
-                    let span = s.base().tcx.def_span(variant);
-                    fatal!(
-                        s[span],
-                        "Type {:#?} appears to have no path",
-                        constructs_type
-                    )
-                }
-            },
-            ..constructs_type.clone()
+        type_namespace: match &constructs_type.parent {
+            Some(parent) => parent.clone(),
+            None => {
+                let span = s.base().tcx.def_span(variant);
+                fatal!(
+                    s[span],
+                    "Type {:#?} appears to have no parent",
+                    constructs_type
+                )
+            }
         },
     }
 }