From db9a347b10029f1b3d6b38be2ffdd4cc27ba237c Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 21 Feb 2025 09:52:29 +0000 Subject: [PATCH 1/6] Add `monomorphize` flag --- charon-ml/src/NameMatcher.ml | 2 +- charon-ml/src/PrintTypes.ml | 2 +- charon-ml/src/generated/Generated_GAst.ml | 1 + .../src/generated/Generated_GAstOfJson.ml | 3 ++ charon/src/options.rs | 8 ++- charon/src/transform/mod.rs | 3 ++ charon/src/transform/monomorphize.rs | 49 +++++++++++++++++++ 7 files changed, 65 insertions(+), 3 deletions(-) create mode 100644 charon/src/transform/monomorphize.rs diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 62d1de95..2b654072 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -1029,7 +1029,7 @@ and const_generic_to_pattern (ctx : ctx) (c : to_pat_config) (m : constraints) and generic_args_to_pattern (ctx : ctx) (c : to_pat_config) (m : constraints) (generics : T.generic_args) : generic_args = - let { regions; types; const_generics; trait_refs = _ } : T.generic_args = + let ({ regions; types; const_generics; trait_refs = _ } : T.generic_args) = generics in let regions = List.map (region_to_pattern m) regions in diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 19259dd9..19f64493 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -371,7 +371,7 @@ let trait_clause_to_string (env : 'a fmt_env) (clause : trait_clause) : string = let generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) : string list * string list = - let { regions; types; const_generics; trait_clauses; _ } : generic_params = + let ({ regions; types; const_generics; trait_clauses; _ } : generic_params) = generics in let regions = List.map region_var_to_string regions in diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml index 2367b668..24c12236 100644 --- a/charon-ml/src/generated/Generated_GAst.ml +++ b/charon-ml/src/generated/Generated_GAst.ml @@ -399,6 +399,7 @@ and cli_options = { skip_borrowck : bool; (** If activated, this skips borrow-checking of the crate. *) no_code_duplication : bool; + monomorphize : bool; extract_opaque_bodies : bool; (** Usually we skip the bodies of foreign methods and structs with private fields. When this flag is on, we don't. diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index ce06c2e4..eeb56b73 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -1611,6 +1611,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : ("use_polonius", use_polonius); ("skip_borrowck", skip_borrowck); ("no_code_duplication", no_code_duplication); + ("monomorphize", monomorphize); ("extract_opaque_bodies", extract_opaque_bodies); ("translate_all_methods", translate_all_methods); ("include", include_); @@ -1643,6 +1644,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : let* use_polonius = bool_of_json ctx use_polonius in let* skip_borrowck = bool_of_json ctx skip_borrowck in let* no_code_duplication = bool_of_json ctx no_code_duplication in + let* monomorphize = bool_of_json ctx monomorphize in let* extract_opaque_bodies = bool_of_json ctx extract_opaque_bodies in let* translate_all_methods = bool_of_json ctx translate_all_methods in let* included = list_of_json string_of_json ctx include_ in @@ -1678,6 +1680,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : use_polonius; skip_borrowck; no_code_duplication; + monomorphize; extract_opaque_bodies; translate_all_methods; included; diff --git a/charon/src/options.rs b/charon/src/options.rs index 5f47804d..ec85b060 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -88,7 +88,7 @@ pub struct CliOpts { b0: switch x [true -> goto b1; false -> goto b2] b1: y := 0; goto b3 b2: y := 1; goto b3 - b3: return y + b3: return y ``` We want to reconstruct the control-flow as: @@ -120,6 +120,9 @@ pub struct CliOpts { "))] #[serde(default)] pub no_code_duplication: bool, + #[clap(long = "monomorphize")] + #[serde(default)] + pub monomorphize: bool, /// Usually we skip the bodies of foreign methods and structs with private fields. When this /// flag is on, we don't. #[clap(long = "extract-opaque-bodies")] @@ -285,6 +288,8 @@ pub struct TranslateOptions { /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show /// up. pub hide_marker_traits: bool, + /// Monomorphize functions. + pub monomorphize: bool, /// Do not merge the chains of gotos. pub no_merge_goto_chains: bool, /// Print the llbc just after control-flow reconstruction. @@ -365,6 +370,7 @@ impl TranslateOptions { mir_level, no_code_duplication: options.no_code_duplication, hide_marker_traits: options.hide_marker_traits, + monomorphize: options.monomorphize, no_merge_goto_chains: options.no_merge_goto_chains, print_built_llbc: options.print_built_llbc, item_opacities, diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index e5271c4d..8b9bc769 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -13,6 +13,7 @@ pub mod inline_local_panic_functions; pub mod insert_assign_return_unit; pub mod lift_associated_item_clauses; pub mod merge_goto_chains; +pub mod monomorphize; pub mod ops_to_function_calls; pub mod prettify_cfg; pub mod reconstruct_asserts; @@ -127,6 +128,8 @@ pub static ULLBC_PASSES: &[Pass] = &[ // # Micro-pass: remove the drops of locals whose type is `Never` (`!`). This // is in preparation of the next transformation. UnstructuredBody(&remove_drop_never::Transform), + // Monomorphize the functions and types. + UnstructuredBody(&monomorphize::Transform), ]; /// Body cleanup passes after control flow reconstruction. diff --git a/charon/src/transform/monomorphize.rs b/charon/src/transform/monomorphize.rs new file mode 100644 index 00000000..23408350 --- /dev/null +++ b/charon/src/transform/monomorphize.rs @@ -0,0 +1,49 @@ +//! # Micro-pass: monomorphize all functions and types; at the end of this pass, all functions and types are monomorphic. + +use crate::transform::TransformCtx; +use crate::ullbc_ast::*; + +use super::ctx::UllbcPass; + +pub struct Transform; +impl UllbcPass for Transform { + fn transform_ctx(&self, ctx: &mut TransformCtx) { + // Check the option which instructs to ignore this pass + if !ctx.options.monomorphize { + return; + } + + // From https://doc.rust-lang.org/nightly/nightly-rustc/rustc_monomorphize/collector/index.html#general-algorithm + // + // The purpose of the algorithm implemented in this module is to build the mono item + // graph for the current crate. It runs in two phases: + // 1. Discover the roots of the graph by traversing the HIR of the crate. + // 2. Starting from the roots, find uses by inspecting the MIR representation of the + // item corresponding to a given node, until no more new nodes are found. + // + // The roots of the mono item graph correspond to the public non-generic syntactic + // items in the source code. We find them by walking the HIR of the crate, and whenever + // we hit upon a public function, method, or static item, we create a mono item + // consisting of the items DefId and, since we only consider non-generic items, an + // empty type-parameters set. + // + // Given a mono item node, we can discover uses by inspecting its MIR. We walk the MIR + // to find other mono items used by each mono item. Since the mono item we are + // currently at is always monomorphic, we also know the concrete type arguments of its + // used mono items. The specific forms a use can take in MIR are quite diverse: it + // includes calling functions/methods, taking a reference to a function/method, drop + // glue, and unsizing casts. + + // In our version of the algorithm, we do the following: + // 1. Find all the roots, adding them to the worklist. + // 2. For each item in the worklist: + // a. Find all the items it uses, adding them to the worklist and the generic + // arguments to the item. + // b. Mark the item as visited + + } + + fn name(&self) -> &str { + "monomorphize" + } +} From 51a298be28be9d13ee67354866d4eeaf6035d3b4 Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 21 Feb 2025 09:53:57 +0000 Subject: [PATCH 2/6] Add maintainers (dune warning) --- charon.opam | 3 +++ dune-project | 7 +++++++ name_matcher_parser.opam | 3 +++ 3 files changed, 13 insertions(+) diff --git a/charon.opam b/charon.opam index 1401f1d5..2d784208 100644 --- a/charon.opam +++ b/charon.opam @@ -9,6 +9,9 @@ description: """ Charon. Charon acts as an interface between the rustc compiler and program verification projects. Its purpose is to process Rust .rs files and convert them into files easy to handle by program verifiers.""" +maintainer: [ + "Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard" +] authors: ["Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"] license: "Apache-2.0" homepage: "https://github.com/AeneasVerif/charon" diff --git a/dune-project b/dune-project index 8a83af48..bec6ee39 100644 --- a/dune-project +++ b/dune-project @@ -21,6 +21,13 @@ "Aymeric Fromherz" "Sidney Congard") + +(maintainers + "Son Ho" + "Jonathan Protzenko" + "Aymeric Fromherz" + "Sidney Congard") + (license Apache-2.0) (package diff --git a/name_matcher_parser.opam b/name_matcher_parser.opam index 2593df0a..1080bdfa 100644 --- a/name_matcher_parser.opam +++ b/name_matcher_parser.opam @@ -3,6 +3,9 @@ opam-version: "2.0" version: "0.1" synopsis: "Parser to define name matchers" description: "" +maintainer: [ + "Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard" +] authors: ["Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"] license: "Apache-2.0" homepage: "https://github.com/AeneasVerif/charon" From c39230a7849df7ec7fb7cb59a0cb79c5cc8fbe05 Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 21 Feb 2025 10:51:08 +0000 Subject: [PATCH 3/6] Basic monomorphized copies --- charon/src/transform/monomorphize.rs | 164 +++++++++++++++++++++++++++ 1 file changed, 164 insertions(+) diff --git a/charon/src/transform/monomorphize.rs b/charon/src/transform/monomorphize.rs index 23408350..915ac4d7 100644 --- a/charon/src/transform/monomorphize.rs +++ b/charon/src/transform/monomorphize.rs @@ -1,10 +1,74 @@ //! # Micro-pass: monomorphize all functions and types; at the end of this pass, all functions and types are monomorphic. +use std::collections::{HashMap, HashSet}; use crate::transform::TransformCtx; use crate::ullbc_ast::*; use super::ctx::UllbcPass; +struct PassData { + // Map of (poly item, generic args) -> mono item + // None indicates the item hasn't been monomorphized yet + items: HashMap<(AnyTransId, GenericArgs), Option>, + worklist: Vec, + visited: HashSet, +} + +impl PassData { + fn new() -> Self { + PassData { + items: HashMap::new(), + worklist: Vec::new(), + visited: HashSet::new(), + } + } +} + +fn find_uses_in_body(data: &mut PassData, body: &ExprBody) { + body.locals.vars.iter().for_each(|var| match var.ty.kind() { + TyKind::Adt(TypeId::Adt(id), gargs) => { + if gargs.is_empty() { + return; + } + + let key = (AnyTransId::Type(*id), gargs.clone()); + data.items.entry(key).or_insert(None); + } + TyKind::Adt(TypeId::Tuple, _) => {} + TyKind::Literal(_) => {} + ty => warn!("Unhandled type kind {:?}", ty), + }); + + body.body.iter().for_each(|block| { + block + .statements + .iter() + .for_each(|stmt| match &stmt.content { + RawStatement::Call(Call { + func: FnOperand::Regular(FnPtr { func, generics }), + .. + }) => match func { + FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)) => { + let key = (AnyTransId::Fun(*fun_id), generics.clone()); + data.items.entry(key).or_insert(None); + } + FunIdOrTraitMethodRef::Trait(..) => { + warn!("Monomorphization doesn't reach traits yet.") + } + // These can't be monomorphized, since they're builtins + FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => {} + }, + _ => {} + }); + }); +} + +fn find_uses_in_type(_data: &mut PassData, _ty: &TypeDeclKind) {} + +fn path_for_generics(gargs: &GenericArgs) -> PathElem { + PathElem::Ident(gargs.to_string(), Disambiguator::ZERO) +} + pub struct Transform; impl UllbcPass for Transform { fn transform_ctx(&self, ctx: &mut TransformCtx) { @@ -41,6 +105,106 @@ impl UllbcPass for Transform { // arguments to the item. // b. Mark the item as visited + // Final list of monomorphized items: { (poly item, generic args) -> mono item } + let mut data = PassData::new(); + + let empty_gargs = GenericArgs::empty(GenericsSource::Other); + + // Find the roots of the mono item graph + for (id, item) in ctx.translated.all_items_with_ids() { + match item { + AnyTransItem::Fun(f) if f.signature.generics.is_empty() => { + data.items.insert((id, empty_gargs.clone()), Some(id)); + data.worklist.push(id); + } + _ => {} + } + } + + // Iterate over worklist -- these items are always monomorphic! + while let Some(id) = data.worklist.pop() { + if data.visited.contains(&id) { + continue; + } + data.visited.insert(id); + + // 1. Find new uses + let Some(item) = ctx.translated.get_item(id) else { + continue; + }; + match item { + AnyTransItem::Fun(f) => { + // assert!( + // f.signature.generics.is_empty(), + // "Non-monomorphic item in worklist" + // ); + let Ok(body) = f + .body + .as_ref() + .map(|body| body.as_unstructured().unwrap()) + .map_err(|opaque| *opaque) + else { + continue; + }; + + find_uses_in_body(&mut data, body) + } + AnyTransItem::Type(t) => { + // assert!(t.generics.is_empty(), "Non-monomorphic item in worklist"); + find_uses_in_type(&mut data, &t.kind) + } + item => todo!("Unhandled monomorphisation target: {:?}", item), + }; + + // 2. Iterate through all newly discovered uses + for ((id, gargs), mono) in data.items.iter_mut() { + if mono.is_some() { + continue; + } + + // a. Monomorphize the items if they're polymorphic, add them to the worklist + let new_mono = match id { + AnyTransId::Fun(fun_id) => 'id_match: { + let fun = ctx.translated.fun_decls.get(*fun_id).unwrap(); + + if gargs.is_empty() { + break 'id_match AnyTransId::Fun(*fun_id); + } + + let mut fun_sub = fun.clone().substitute(gargs); + fun_sub.signature.generics = GenericParams::empty(); + + let fun_id_sub = ctx.translated.fun_decls.reserve_slot(); + fun_sub.def_id = fun_id_sub; + ctx.translated.fun_decls.set_slot(fun_id_sub, fun_sub); + + AnyTransId::Fun(fun_id_sub) + } + AnyTransId::Type(typ_id) => 'id_match: { + let typ = ctx.translated.type_decls.get(*typ_id).unwrap(); + + if gargs.is_empty() { + break 'id_match AnyTransId::Type(*typ_id); + } + + let mut typ_sub = typ.clone().substitute(gargs); + typ_sub.generics = GenericParams::empty(); + typ_sub.item_meta.name.name.push(path_for_generics(gargs)); + + let typ_id_sub = ctx.translated.type_decls.reserve_slot(); + typ_sub.def_id = typ_id_sub; + ctx.translated.type_decls.set_slot(typ_id_sub, typ_sub); + + AnyTransId::Type(typ_id_sub) + } + _ => todo!("Unhandled monomorphization target ID {:?}", id), + }; + *mono = Some(new_mono); + data.worklist.push(new_mono); + } + + // 3. Substitute all generics with the monomorphized versions + } } fn name(&self) -> &str { From 54d9c7e39b2d994b970b9b5e60791cb7b9d95a95 Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 21 Feb 2025 11:50:09 +0000 Subject: [PATCH 4/6] Small functioning monomorphization --- charon/src/ids/vector.rs | 11 ++++ charon/src/transform/monomorphize.rs | 96 ++++++++++++++++++++++++++-- 2 files changed, 103 insertions(+), 4 deletions(-) diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs index 24dd1083..dbc354e2 100644 --- a/charon/src/ids/vector.rs +++ b/charon/src/ids/vector.rs @@ -264,6 +264,17 @@ where self.vector.indices() } + pub fn retain(&mut self, mut f: impl FnMut(&mut T) -> bool) { + self.vector.iter_mut().for_each(|opt| { + if let Some(x) = opt { + if !f(x) { + *opt = None; + self.elem_count -= 1; + } + } + }); + } + /// Like `Vec::split_off`. pub fn split_off(&mut self, at: usize) -> Self { let mut ret = Self { diff --git a/charon/src/transform/monomorphize.rs b/charon/src/transform/monomorphize.rs index 915ac4d7..904d02a2 100644 --- a/charon/src/transform/monomorphize.rs +++ b/charon/src/transform/monomorphize.rs @@ -27,10 +27,6 @@ impl PassData { fn find_uses_in_body(data: &mut PassData, body: &ExprBody) { body.locals.vars.iter().for_each(|var| match var.ty.kind() { TyKind::Adt(TypeId::Adt(id), gargs) => { - if gargs.is_empty() { - return; - } - let key = (AnyTransId::Type(*id), gargs.clone()); data.items.entry(key).or_insert(None); } @@ -65,6 +61,68 @@ fn find_uses_in_body(data: &mut PassData, body: &ExprBody) { fn find_uses_in_type(_data: &mut PassData, _ty: &TypeDeclKind) {} +// Akin to find_uses_in_body, but substitutes all uses of generics with the monomorphized versions +// This is a two-step process, because we can't mutate the translation context with new definitions +// while also mutating the existing definitions. +fn subst_uses_in_body(data: &PassData, body: &mut ExprBody) { + body.locals.vars.iter_mut().for_each(|var| { + subst_uses_in_type(data, &mut var.ty); + }); + + body.body.iter_mut().for_each(|block| { + block + .statements + .iter_mut() + .for_each(|stmt| match &mut stmt.content { + RawStatement::Call(Call { + func: FnOperand::Regular(FnPtr { func, generics }), + .. + }) => match func { + FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)) => { + let key = (AnyTransId::Fun(*fun_id), generics.clone()); + let subst = data.items.get(&key).unwrap(); + let Some(AnyTransId::Fun(subst_id)) = subst else { + panic!("Substitution missing for {:?}", key); + }; + *fun_id = *subst_id; + *generics = GenericArgs::empty(GenericsSource::Other); + } + FunIdOrTraitMethodRef::Trait(..) => { + warn!("Monomorphization doesn't reach traits yet.") + } + // These can't be monomorphized, since they're builtins + FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => {} + }, + _ => {} + }); + }); +} + +fn subst_uses_in_fn_sig(data: &PassData, sig: &mut FunSig) { + sig.inputs.iter_mut().for_each(|arg| { + subst_uses_in_type(data, arg); + }) +} + +fn subst_uses_in_type(data: &PassData, ty: &mut Ty) { + ty.with_kind_mut(|k| match k { + TyKind::Adt(TypeId::Adt(id), gargs) => { + let key = (AnyTransId::Type(*id), gargs.clone()); + let subst = data.items.get(&key).unwrap(); + let Some(AnyTransId::Type(subst_id)) = subst else { + panic!("Substitution missing for {:?}", key); + }; + *id = *subst_id; + *gargs = GenericArgs::empty(GenericsSource::Other); + } + TyKind::Adt(TypeId::Tuple, _) => {} + TyKind::Literal(_) => {} + ty => warn!("Unhandled type kind {:?}", ty), + }) +} + +fn subst_uses_in_type_decl(_data: &PassData, _ty: &mut TypeDeclKind) {} + fn path_for_generics(gargs: &GenericArgs) -> PathElem { PathElem::Ident(gargs.to_string(), Disambiguator::ZERO) } @@ -204,7 +262,37 @@ impl UllbcPass for Transform { } // 3. Substitute all generics with the monomorphized versions + let Some(item) = ctx.translated.get_item_mut(id) else { + continue; + }; + match item { + AnyTransItemMut::Fun(f) => { + let Ok(body) = f + .body + .as_mut() + .map(|body| body.as_unstructured_mut().unwrap()) + .map_err(|opaque| *opaque) + else { + continue; + }; + + subst_uses_in_body(&data, body); + subst_uses_in_fn_sig(&data, &mut f.signature) + } + AnyTransItemMut::Type(t) => { + // assert!(t.generics.is_empty(), "Non-monomorphic item in worklist"); + subst_uses_in_type_decl(&data, &mut t.kind) + } + item => todo!("Unhandled monomorphisation target: {:?}", item), + }; } + + // Now, remove all polymorphic items from the translation context, as all their + // uses have been monomorphized and substituted + ctx.translated + .fun_decls + .retain(|f| f.signature.generics.is_empty()); + ctx.translated.type_decls.retain(|t| t.generics.is_empty()); } fn name(&self) -> &str { From 66b68a1f1e1f9a8e82532bda7aac38942c87b94d Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 21 Feb 2025 17:58:52 +0000 Subject: [PATCH 5/6] Use visitor for substitutions! --- charon/src/transform/check_generics.rs | 2 +- charon/src/transform/monomorphize.rs | 151 +++++++++++++------------ 2 files changed, 81 insertions(+), 72 deletions(-) diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 9acb0d60..f3ee9a40 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -237,7 +237,7 @@ impl VisitAst for CheckGenericsVisitor<'_> { } GenericsSource::Builtin => return, GenericsSource::Other => { - self.error("`GenericsSource::Other` should now exist in the charon AST"); + self.error("`GenericsSource::Other` should not exist in the charon AST"); return; } }; diff --git a/charon/src/transform/monomorphize.rs b/charon/src/transform/monomorphize.rs index 904d02a2..5c53398e 100644 --- a/charon/src/transform/monomorphize.rs +++ b/charon/src/transform/monomorphize.rs @@ -1,5 +1,7 @@ //! # Micro-pass: monomorphize all functions and types; at the end of this pass, all functions and types are monomorphic. +use derive_generic_visitor::*; use std::collections::{HashMap, HashSet}; +use std::ops::ControlFlow::Continue; use crate::transform::TransformCtx; use crate::ullbc_ast::*; @@ -61,67 +63,89 @@ fn find_uses_in_body(data: &mut PassData, body: &ExprBody) { fn find_uses_in_type(_data: &mut PassData, _ty: &TypeDeclKind) {} -// Akin to find_uses_in_body, but substitutes all uses of generics with the monomorphized versions +// Akin to find_uses_in_*, but substitutes all uses of generics with the monomorphized versions // This is a two-step process, because we can't mutate the translation context with new definitions // while also mutating the existing definitions. -fn subst_uses_in_body(data: &PassData, body: &mut ExprBody) { - body.locals.vars.iter_mut().for_each(|var| { - subst_uses_in_type(data, &mut var.ty); - }); - - body.body.iter_mut().for_each(|block| { - block - .statements - .iter_mut() - .for_each(|stmt| match &mut stmt.content { - RawStatement::Call(Call { - func: FnOperand::Regular(FnPtr { func, generics }), - .. - }) => match func { - FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)) => { - let key = (AnyTransId::Fun(*fun_id), generics.clone()); - let subst = data.items.get(&key).unwrap(); - let Some(AnyTransId::Fun(subst_id)) = subst else { - panic!("Substitution missing for {:?}", key); - }; - *fun_id = *subst_id; - *generics = GenericArgs::empty(GenericsSource::Other); - } - FunIdOrTraitMethodRef::Trait(..) => { - warn!("Monomorphization doesn't reach traits yet.") - } - // These can't be monomorphized, since they're builtins - FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => {} - }, - _ => {} - }); - }); +#[derive(Visitor)] +struct SubstVisitor<'a> { + data: &'a PassData, } +impl VisitAstMut for SubstVisitor<'_> { + // fn visit<'a, T: AstVisitable>(&'a mut self, x: &mut T) -> ControlFlow { + // x.drive(self)?; + // Continue(()) + // } + // + + fn visit_aggregate_kind(&mut self, kind: &mut AggregateKind) -> ControlFlow { + match kind { + AggregateKind::Adt(TypeId::Adt(id), _, _, gargs) => { + let key = (AnyTransId::Type(*id), gargs.clone()); + let subst = self.data.items.get(&key).unwrap(); + let Some(AnyTransId::Type(subst_id)) = subst else { + panic!("Substitution missing for {:?}", key); + }; + *id = *subst_id; + *gargs = GenericArgs::empty(GenericsSource::Builtin); + } + AggregateKind::Closure(fun_id, gargs) => { + let key = (AnyTransId::Fun(*fun_id), gargs.clone()); + let subst = self.data.items.get(&key).unwrap(); + let Some(AnyTransId::Fun(subst_id)) = subst else { + panic!("Substitution missing for {:?}", key); + }; + *fun_id = *subst_id; + *gargs = GenericArgs::empty(GenericsSource::Builtin); + } + _ => {} + } -fn subst_uses_in_fn_sig(data: &PassData, sig: &mut FunSig) { - sig.inputs.iter_mut().for_each(|arg| { - subst_uses_in_type(data, arg); - }) -} + Continue(()) + } -fn subst_uses_in_type(data: &PassData, ty: &mut Ty) { - ty.with_kind_mut(|k| match k { - TyKind::Adt(TypeId::Adt(id), gargs) => { - let key = (AnyTransId::Type(*id), gargs.clone()); - let subst = data.items.get(&key).unwrap(); - let Some(AnyTransId::Type(subst_id)) = subst else { - panic!("Substitution missing for {:?}", key); - }; - *id = *subst_id; - *gargs = GenericArgs::empty(GenericsSource::Other); + fn visit_ty_kind(&mut self, kind: &mut TyKind) -> ControlFlow { + match kind { + TyKind::Adt(TypeId::Adt(id), gargs) => { + let key = (AnyTransId::Type(*id), gargs.clone()); + let subst = self.data.items.get(&key).unwrap(); + let Some(AnyTransId::Type(subst_id)) = subst else { + panic!("Substitution missing for {:?}", key); + }; + *id = *subst_id; + *gargs = GenericArgs::empty(GenericsSource::Builtin); + } + TyKind::Adt(TypeId::Tuple, _) => {} + TyKind::Literal(_) => {} + ty => warn!("Unhandled type kind {:?}", ty), } - TyKind::Adt(TypeId::Tuple, _) => {} - TyKind::Literal(_) => {} - ty => warn!("Unhandled type kind {:?}", ty), - }) + Continue(()) + } + + fn visit_fn_ptr(&mut self, fn_ptr: &mut FnPtr) -> ControlFlow { + match &mut fn_ptr.func { + FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)) => { + let key = (AnyTransId::Fun(*fun_id), fn_ptr.generics.clone()); + let subst = self.data.items.get(&key).unwrap(); + let Some(AnyTransId::Fun(subst_id)) = subst else { + panic!("Substitution missing for {:?}", key); + }; + *fun_id = *subst_id; + fn_ptr.generics = GenericArgs::empty(GenericsSource::Builtin); + } + FunIdOrTraitMethodRef::Trait(..) => { + warn!("Monomorphization doesn't reach traits yet.") + } + // These can't be monomorphized, since they're builtins + FunIdOrTraitMethodRef::Fun(FunId::Builtin(..)) => {} + } + Continue(()) + } } -fn subst_uses_in_type_decl(_data: &PassData, _ty: &mut TypeDeclKind) {} +fn subst_uses(data: &PassData, item: &mut T) { + let mut visitor = SubstVisitor { data }; + item.drive_mut(&mut visitor); +} fn path_for_generics(gargs: &GenericArgs) -> PathElem { PathElem::Ident(gargs.to_string(), Disambiguator::ZERO) @@ -166,7 +190,7 @@ impl UllbcPass for Transform { // Final list of monomorphized items: { (poly item, generic args) -> mono item } let mut data = PassData::new(); - let empty_gargs = GenericArgs::empty(GenericsSource::Other); + let empty_gargs = GenericArgs::empty(GenericsSource::Builtin); // Find the roots of the mono item graph for (id, item) in ctx.translated.all_items_with_ids() { @@ -266,23 +290,8 @@ impl UllbcPass for Transform { continue; }; match item { - AnyTransItemMut::Fun(f) => { - let Ok(body) = f - .body - .as_mut() - .map(|body| body.as_unstructured_mut().unwrap()) - .map_err(|opaque| *opaque) - else { - continue; - }; - - subst_uses_in_body(&data, body); - subst_uses_in_fn_sig(&data, &mut f.signature) - } - AnyTransItemMut::Type(t) => { - // assert!(t.generics.is_empty(), "Non-monomorphic item in worklist"); - subst_uses_in_type_decl(&data, &mut t.kind) - } + AnyTransItemMut::Fun(f) => subst_uses(&data, f), + AnyTransItemMut::Type(t) => subst_uses(&data, t), item => todo!("Unhandled monomorphisation target: {:?}", item), }; } From 7c80d5980866a6c47c51f828ea6a5214083bec39 Mon Sep 17 00:00:00 2001 From: N1ark Date: Mon, 24 Feb 2025 20:55:27 +0000 Subject: [PATCH 6/6] Substitute types in discriminants --- charon/src/transform/monomorphize.rs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/charon/src/transform/monomorphize.rs b/charon/src/transform/monomorphize.rs index 5c53398e..a75d41c0 100644 --- a/charon/src/transform/monomorphize.rs +++ b/charon/src/transform/monomorphize.rs @@ -77,6 +77,27 @@ impl VisitAstMut for SubstVisitor<'_> { // } // + fn visit_ullbc_statement(&mut self, stt: &mut Statement) -> ControlFlow { + stt.content.drive_mut(self); + match &mut stt.content { + RawStatement::Assign(_, Rvalue::Discriminant(Place { ty, .. }, id)) => { + match ty.as_adt() { + Some((TypeId::Adt(new_enum_id), _)) => { + // Small trick; the discriminant doesn't carry the information on the + // generics of the enum, since it's irrelevant, but we need it to do + // the substitution, so we look at the type of the place we read from + *id = new_enum_id; + } + _ => {} + } + () + } + _ => (), + } + + Continue(()) + } + fn visit_aggregate_kind(&mut self, kind: &mut AggregateKind) -> ControlFlow { match kind { AggregateKind::Adt(TypeId::Adt(id), _, _, gargs) => {