hax_rust_engine/ast/identifiers/global_id/
generated_names.rs

1/// We allow:
2///  - `unused`: we don't use all the names present in the `engine/names` crate.
3///    Filtering which `DefId` should be exposed would be complicated, and
4///    dependent library may use some names. (for instance, the backend for
5///    ProVerif may use names from `hax_lib_protocol` that are not needed
6///    anywhere else in the engine)
7///  - `non_snake_case`: we produce faithful names with respect to their
8///    original definitions in Rust. We generate for instance `fn Some() ->
9///    DefID {...}` that provides the `DefId` for the
10///    `std::option::Option::Some`. We want the function to be named `Some`
11///    here, not `some`.
12///  - `broken_intra_doc_links`: we produce documentation that link the function
13///    providing the `DefId` of a item to the item itself. Sometimes, we refer
14///    to private items, to re-exported items or to items that are not in the
15///    dependency closure of the engine: in such cases, `rustdoc` cannot link
16///    properly.
17#[allow(
18    unused,
19    non_snake_case,
20    rustdoc::broken_intra_doc_links,
21    missing_docs,
22    clippy::module_inception,
23    unused_qualifications,
24    non_upper_case_globals
25)]
26pub mod root {
27    include!("generated.rs");
28}
29
30/// Global identifiers are built around `DefId` that comes out of the hax
31/// frontend. We use the Rust engine itself to produce the names: we run hax on
32/// the `engine/names` crate, we extract identifiers from the resulting AST, and
33/// we expose them back as Rust functions here.
34pub mod codegen {
35    use itertools::*;
36    use std::iter;
37
38    use crate::ast::Item;
39    use crate::ast::identifiers::{
40        GlobalId,
41        global_id::{ExplicitDefId, compact_serialization},
42    };
43    use hax_frontend_exporter::DefKind;
44
45    use std::collections::{HashMap, HashSet};
46
47    /// Replace the crate name `"hax_engine_names"` with `"rust_primitives"` in the given `DefId`.
48    fn rename_krate(def_id: &mut ExplicitDefId) {
49        if def_id.def_id.krate == "hax_engine_names" {
50            def_id.rename_krate("rust_primitives");
51        }
52    }
53
54    /// Visit items and collect all the `DefId`s
55    fn collect_def_ids(items: Vec<Item>) -> Vec<ExplicitDefId> {
56        #[derive(Default)]
57        struct DefIdCollector(HashSet<ExplicitDefId>);
58        use crate::ast::visitors::*;
59        impl AstVisitor for DefIdCollector {
60            fn visit_global_id(&mut self, x: &GlobalId) {
61                let mut current = x.0.explicit_def_id();
62                while let Some(def_id) = current {
63                    self.0.insert(def_id.clone());
64                    current = def_id.parent();
65                }
66            }
67        }
68
69        // Collect names
70        let mut names: Vec<_> = DefIdCollector::default()
71            .visit_by_val(&items)
72            .0
73            .into_iter()
74            .collect();
75
76        // In the OCaml engine, `hax_engine_names` is renamed to `rust_primitives`.
77        names.iter_mut().for_each(rename_krate);
78
79        // We consume names after import by the OCaml engine. Thus, the OCaml
80        // engine may have introduced already some hax-specific Rust names,
81        // directly in `rust_primitives`. After renaming from `hax_engine_names`
82        // to `rust_primitives`, such names may be duplicated. For instance,
83        // that's the case of `unsize`: the crate `hax_engine_names` contains
84        // expression with implicit unsize operations, thus the OCaml engine
85        // inserts `rust_primitives::unsize`. In the same time,
86        // `hax_engine_names::unsize` exists and was renamed to
87        // `rust_primitives::unsize`. Whence the need to dedup here.
88        names.sort();
89        names.dedup();
90        names
91    }
92
93    /// Crafts a docstring for a `DefId`, hopefully (rustdoc) linking it back to
94    /// its origin.
95    fn docstring(explicit_id: &ExplicitDefId) -> String {
96        let id = &explicit_id.def_id;
97        let path = path_of_def_id(explicit_id);
98        let (parent_path, def) = match &path[..] {
99            [init @ .., last] => (init, last.clone()),
100            _ => (&[] as &[_], id.krate.to_string()),
101        };
102        let parent_path_str = format!("::{}", parent_path.join("::"));
103        let path_str = format!("::{}", path_of_def_id(explicit_id).join("::"));
104        let subject = match &id.kind {
105            DefKind::Mod => format!("module [`{path_str}`]"),
106            DefKind::Struct => format!("struct [`{path_str}`]"),
107            DefKind::Union => format!("union [`{path_str}`]"),
108            DefKind::Enum => format!("enum [`{path_str}`]"),
109            DefKind::Variant => format!("variant [`{path_str}`]"),
110            DefKind::Trait => format!("trait [`{path_str}`]"),
111            DefKind::TyAlias => format!("type alias [`{path_str}`]"),
112            DefKind::ForeignTy => format!("foreign type [`{path_str}`]"),
113            DefKind::TraitAlias => format!("trait alias [`{path_str}`]"),
114            DefKind::AssocTy => format!("associated type [`{path_str}`]"),
115            DefKind::TyParam => format!("type parameter from [`{parent_path_str}`]"),
116            DefKind::Fn => format!("function [`{path_str}`]"),
117            DefKind::Const => format!("const [`{path_str}`]"),
118            DefKind::ConstParam => format!("const parameter from [`{parent_path_str}`]"),
119            DefKind::Static { .. } => format!("static [`{path_str}`]"),
120            DefKind::Ctor { .. } => format!("constructor for [`{parent_path_str}`]"),
121            DefKind::AssocFn => format!("associated function [`{path_str}`]"),
122            DefKind::AssocConst => format!("associated constant [`{path_str}`]"),
123            DefKind::Macro { .. } => format!("macro [`{path_str}`]"),
124            DefKind::ExternCrate => format!("extern crate [`{path_str}`]"),
125            DefKind::Use => format!("use item [`{path_str}`]"),
126            DefKind::ForeignMod => format!("foreign module [`{path_str}`]"),
127            DefKind::AnonConst => return "This is an anonymous constant.".to_string(),
128            DefKind::PromotedConst | DefKind::InlineConst => {
129                format!("This is an inline const from [`{parent_path_str}`]")
130            }
131            DefKind::OpaqueTy => {
132                return format!("This is an opaque type for [`{parent_path_str}`]");
133            }
134            DefKind::Field => format!("field [`{def}`] from {parent_path_str}"),
135            DefKind::LifetimeParam => return "This is a lifetime parameter.".to_string(),
136            DefKind::GlobalAsm => return "This is a global ASM block.".to_string(),
137            DefKind::Impl { .. } => return "This is an impl block.".to_string(),
138            DefKind::Closure => return "This is a closure.".to_string(),
139            DefKind::SyntheticCoroutineBody => return "This is a coroutine body.".to_string(),
140        };
141        format!("This is the {subject}.")
142    }
143
144    /// Computes a string path for a `DefId`.
145    fn path_of_def_id(explicit_id: &ExplicitDefId) -> Vec<String> {
146        let id = &explicit_id.def_id;
147        fn name_to_string(mut s: String) -> String {
148            if s == "_" {
149                s = "_anonymous".into();
150            };
151            if s.parse::<i32>().is_ok() {
152                s = format!("_{s}");
153            }
154            s
155        }
156        iter::once(id.krate.to_string())
157            .chain(id.path.iter().map(|item| {
158                let data = match item.data.clone() {
159                    hax_frontend_exporter::DefPathItem::CrateRoot { name } => name,
160                    hax_frontend_exporter::DefPathItem::TypeNs(s)
161                    | hax_frontend_exporter::DefPathItem::ValueNs(s)
162                    | hax_frontend_exporter::DefPathItem::MacroNs(s)
163                    | hax_frontend_exporter::DefPathItem::LifetimeNs(s) => s,
164                    data => format!("{data:?}"),
165                };
166                if item.disambiguator == 0 {
167                    data
168                } else {
169                    format!("{data}__{}", item.disambiguator)
170                }
171            }))
172            .chain(if explicit_id.is_constructor {
173                Some("Constructor".to_string())
174            } else {
175                None
176            })
177            .chain(if matches!(id.kind, DefKind::Ctor(..)) {
178                // TODO: get rid of `ctor` #1657
179                Some("ctor".to_string())
180            } else {
181                None
182            })
183            .map(name_to_string)
184            .collect()
185    }
186
187    /// Given a list of `DefId`, this will create a Rust code source that provides those names.
188    ///
189    /// For example, given `krate::module::f` and `krate::g`, this will produce something like:
190    /// ```rust,ignore
191    /// mod krate {
192    ///    mod module {
193    ///       fn f() -> DefId {...}
194    ///    }
195    ///    fn g() -> DefId {...}
196    /// }
197    /// ```
198    fn generate_names_hierachy(def_ids: Vec<ExplicitDefId>) -> String {
199        /// Helper struct: a graph of module and definitions.
200        #[derive(Debug, Default)]
201        struct Module {
202            attached_def_id: Option<ExplicitDefId>,
203            submodules: HashMap<String, Module>,
204            definitions: Vec<(String, ExplicitDefId)>,
205        }
206        impl Module {
207            fn new(def_ids: Vec<ExplicitDefId>) -> Self {
208                let mut node = Self::default();
209                for def_id in &def_ids {
210                    node.insert(def_id);
211                }
212                for def_id in def_ids {
213                    let modpath = path_of_def_id(&def_id);
214                    if let Some(module) = node.find_module(&modpath) {
215                        module.attached_def_id = Some(def_id.clone());
216                    }
217                }
218                node
219            }
220            /// Insert a `DefId` in our module tree
221            fn insert(&mut self, def_id: &ExplicitDefId) {
222                let fullpath = path_of_def_id(def_id);
223                let [modpath @ .., def] = &fullpath[..] else {
224                    return;
225                };
226
227                let mut node = self;
228                for chunk in modpath {
229                    node = node.submodules.entry(chunk.clone()).or_default();
230                }
231
232                node.definitions.push((def.clone(), def_id.clone()));
233            }
234            /// Get a mutable borrow to the submodule denoted by `modpath`, if it exists
235            fn find_module(&mut self, modpath: &Vec<String>) -> Option<&mut Self> {
236                let mut node = self;
237                for chunk in modpath {
238                    node = node.submodules.get_mut(chunk)?;
239                }
240                Some(node)
241            }
242            /// Render the module tree as a string
243            fn render(self, path: String, indexes: &HashMap<ExplicitDefId, usize>) -> String {
244                /// Computes the visibility restriction for a given path.
245                fn restriction(path: &str) -> &'static str {
246                    // Tuples are encoded directly in `GlobalIdInner::Tuple`.
247                    // The names here exist so that tuple identifiers can be handled in the exact same way as other identifiers.
248                    // But the canonical representation of tuples is not `names::rust_primitives::hax::Tuple*`.
249                    // Whence this visibility restriction.
250                    if path.starts_with("::rust_primitives::hax::Tuple") {
251                        "(in crate::ast::identifiers::global_id)"
252                    } else {
253                        ""
254                    }
255                }
256                let Self {
257                    submodules,
258                    definitions,
259                    attached_def_id,
260                } = self;
261                let submodules = submodules
262                    .into_iter()
263                    .sorted_by(|(a, _), (b, _)| a.cmp(b))
264                    .map(|(name, contents)| {
265                        let path = format!("{path}::{name}");
266                        let restriction = restriction(&path);
267                        format!(
268                            r###"pub{restriction} mod {name} {{ {} }}"###,
269                            contents.render(path, indexes)
270                        )
271                    });
272                let definitions = definitions
273                    .into_iter()
274                    .sorted_by(|(a, _), (b, _)| a.cmp(b))
275                    .map(|(name, def_id)| {
276                        let docstring = docstring(&def_id);
277                        let index = indexes.get(&def_id).unwrap();
278                        let restriction = restriction(&format!("{path}::{name}"));
279                        format!(r###"
280                            #[doc = r##"{docstring}"##]
281                            pub{restriction} const {name}: crate::ast::identifiers::global_id::GlobalId = crate::ast::identifiers::global_id::GlobalId(root::INTERNED_GLOBAL_IDS[{index}]);
282                        "###)
283                    });
284                let docstring = attached_def_id
285                    .iter()
286                    .map(docstring)
287                    .map(|s| format!(r###"#![doc=r##"{s}"##]"###));
288                docstring
289                    .chain(iter::once("use super::root;".to_string()))
290                    .chain(submodules)
291                    .chain(definitions)
292                    .collect::<Vec<_>>()
293                    .join("\n")
294            }
295        }
296        let enumerated_def_ids = def_ids
297            .iter()
298            .cloned()
299            .enumerate()
300            .map(|(n, def_id)| (def_id, n))
301            .collect::<Vec<_>>();
302        let indexes = HashMap::from_iter(enumerated_def_ids.iter().cloned());
303        let tree = Module::new(def_ids).render(String::new(), &indexes);
304        let functions = {
305            enumerated_def_ids.iter().map(|(did, i)| {
306                let serialized = compact_serialization::serialize(did);
307                let parent = did.parent().as_ref().map(|parent| *indexes.get(parent).unwrap()).map(|parent| format!("Some(did_{parent}())")).unwrap_or("None".into());
308                format!(r###"fn did_{i}() -> ExplicitDefId {{deserialize(r##"{serialized}"##, {parent})}}"###)
309            }).collect::<Vec<_>>().join("\n")
310        };
311        let array_literal = enumerated_def_ids
312            .iter()
313            .map(|(_, i)| format!("did_{i}().into_global_id_inner()"))
314            .collect::<Vec<_>>()
315            .join(",");
316        let n = indexes.len();
317        format!(
318            r#"// This file was generated by `cargo hax into generate-rust-engine-names`.
319// To regenerate it, please use `just regenerate-names`. Under the hood, `cargo
320// hax into generate-rust-engine-names` runs the Rust engine, which in turn
321// calls `rust_engine::names::export_def_ids_to_mod`.
322
323static TABLE_AND_INTERNED_GLOBAL_IDS: (crate::interning::LazyLockNewWithValue<crate::ast::identifiers::global_id::GlobalIdInner, {n}>, [crate::interning::Interned<crate::ast::identifiers::global_id::GlobalIdInner>; {n}]) = {{
324    crate::interning::InterningTable::new_with_values(|| {{
325        use crate::ast::identifiers::global_id::ExplicitDefId;
326        use crate::ast::identifiers::global_id::compact_serialization::deserialize;
327        {functions}
328        [{array_literal}]
329    }})
330}};
331
332static INTERNED_GLOBAL_IDS: [crate::interning::Interned<crate::ast::identifiers::global_id::GlobalIdInner>; {n}] = TABLE_AND_INTERNED_GLOBAL_IDS.1;
333
334impl crate::interning::Internable for crate::ast::identifiers::global_id::GlobalIdInner {{
335    fn interning_table() -> &'static std::sync::Mutex<crate::interning::InterningTable<Self>> {{
336        &TABLE_AND_INTERNED_GLOBAL_IDS.0
337    }}
338}}
339
340{tree}
341"#
342        )
343    }
344
345    /// Finds all `DefId`s in `items`, and produce a Rust module exposing them.
346    pub fn export_def_ids_to_mod(items: Vec<Item>) -> String {
347        generate_names_hierachy(collect_def_ids(items))
348    }
349}
hax_rust_engine/ast/identifiers/global_id/generated_names.rs

hax_rust_engine/ast/identifiers/global_id/
generated_names.rs
