diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index 6a9c839a2..a406d8345 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -305,14 +305,14 @@ module View = struct | Float F32 -> Some "f32" | Float F64 -> Some "f64" | Tuple [] -> Some "unit" - | Adt { def_id; generic_args = [] } -> adt def_id + | Adt { def_id; generic_args = []; _ } -> adt def_id | _ -> None in let apply left right = left ^ "_of_" ^ right in let rec arity1 = function | Types.Slice sub -> arity1 sub |> Option.map ~f:(apply "slice") | Ref (_, sub, _) -> arity1 sub |> Option.map ~f:(apply "ref") - | Adt { def_id; generic_args = [ Type arg ] } -> + | Adt { def_id; generic_args = [ Type arg ]; _ } -> let* adt = adt def_id in let* arg = arity1 arg in Some (apply adt arg) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 30ef7c73d..4edc4209f 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -738,6 +738,8 @@ end) : EXPR = struct | Borrow arg -> Borrow { arg = constant_expr_to_expr arg; borrow_kind = Thir.Shared } | ConstRef { id } -> ConstRef { id } + | TraitConst _ | FnPtr _ -> + unimplemented [ span ] "constant_lit_to_lit: TraitConst | FnPtr" | Todo _ -> unimplemented [ span ] "ConstantExpr::Todo" and constant_lit_to_lit (l : Thir.constant_literal) : Thir.lit_kind * bool = match l with @@ -889,7 +891,7 @@ end) : EXPR = struct else List.map ~f:(c_ty span) inputs in TArrow (inputs, c_ty span output) - | Adt { def_id = id; generic_args } -> + | Adt { def_id = id; generic_args; _ } -> let ident = def_id Type id in let args = List.map ~f:(c_generic_value span) generic_args in TApp { ident; args } @@ -909,12 +911,14 @@ end) : EXPR = struct | Tuple types -> let types = List.map ~f:(fun ty -> GType (c_ty span ty)) types in TApp { ident = `TupleType (List.length types); args = types } - | Alias (_kind, { trait_def_id = Some (_did, impl_expr); def_id; _ }) -> + | Alias { kind = Projection { assoc_item = _; impl_expr }; def_id; _ } -> let impl = c_impl_expr span impl_expr in let item = Concrete_ident.of_def_id (AssociatedItem Type) def_id in TAssociatedType { impl; item } - | Alias (_kind, { def_id; trait_def_id = None; _ }) -> + | Alias { kind = Opaque; def_id; _ } -> TOpaque (Concrete_ident.of_def_id Type def_id) + | Alias { kind = Inherent; _ } -> + unimplemented [ span ] "type Alias::Inherent" | Param { index; name } -> (* TODO: [id] might not unique *) TParam { name; id = Local_ident.mk_id Typ (MyInt64.to_int_exn index) } diff --git a/frontend/exporter/src/body.rs b/frontend/exporter/src/body.rs index f322f4ac3..89cb57c89 100644 --- a/frontend/exporter/src/body.rs +++ b/frontend/exporter/src/body.rs @@ -44,6 +44,11 @@ pub fn body_from_id<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>( id: rustc_hir::BodyId, s: &S, ) -> Body { + // **Important:** + // We need a local id here, and we get it from the owner id, which must + // be local. It is safe to do so, because if we have access to HIR objects, + // it necessarily means we are exploring a local item (we don't have + // access to the HIR of external objects, only their MIR). Body::body(s.base().tcx.hir().body_owner_def_id(id), s) } diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index 73ee2f6c4..6e8d441f6 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -38,10 +38,35 @@ pub enum ConstantExprKind { GlobalName { id: GlobalIdent, }, + /// A trait constant + /// + /// Ex.: + /// ```text + /// impl Foo for Bar { + /// const C : usize = 32; // <- + /// } + /// ``` + TraitConst { + impl_expr: ImplExpr, + name: String, + }, Borrow(ConstantExpr), ConstRef { id: ParamConst, }, + FnPtr { + def_id: DefId, + generics: Vec, + /// The implementation expressions for every generic bounds + /// ```text + /// fn foo(...) + /// ^^^ + /// ``` + generics_impls: Vec, + /// If the function is a method of trait `Foo`, `method_impl` + /// is an implementation of `Foo` + method_impl: Option, + }, Todo(String), } @@ -125,6 +150,10 @@ impl From for Expr { Tuple { fields } => ExprKind::Tuple { fields: fields.into_iter().map(|field| field.into()).collect(), }, + kind @ (FnPtr { .. } | TraitConst { .. }) => { + // SH: I see the `Closure` kind, but it's not the same as function pointer? + ExprKind::Todo(format!("FnPtr or TraitConst. kind={:#?}", kind)) + } Todo(msg) => ExprKind::Todo(msg), }; Decorated { @@ -253,6 +282,21 @@ pub(crate) fn is_anon_const<'tcx>( ) } +fn trait_const_to_constant_expr_kind<'tcx, S: BaseState<'tcx> + HasOwnerId>( + s: &S, + _const_def_id: rustc_hir::def_id::DefId, + substs: rustc_middle::ty::SubstsRef<'tcx>, + assoc: &rustc_middle::ty::AssocItem, +) -> ConstantExprKind { + assert!(assoc.trait_item_def_id.is_some()); + let name = assoc.name.to_string(); + + // Retrieve the trait information + let impl_expr = get_trait_info(s, substs, assoc); + + ConstantExprKind::TraitConst { impl_expr, name } +} + impl ConstantExprKind { pub fn decorate(self, ty: Ty, span: Span) -> Decorated { Decorated { @@ -266,6 +310,7 @@ impl ConstantExprKind { } pub enum TranslateUnevalRes { + // TODO: rename GlobalName(ConstantExprKind), EvaluatedConstant(T), } @@ -279,7 +324,7 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { fn translate_uneval( &self, s: &impl UnderOwnerState<'tcx>, - ucv: rustc_middle::ty::UnevaluatedConst, + ucv: rustc_middle::ty::UnevaluatedConst<'tcx>, ) -> TranslateUnevalRes { let tcx = s.base().tcx; if is_anon_const(ucv.def, tcx) { @@ -288,8 +333,17 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { supposely_unreachable_fatal!(s, "TranslateUneval"; {self, ucv}); })) } else { - let id = ucv.def.sinto(s); - TranslateUnevalRes::GlobalName(ConstantExprKind::GlobalName { id }) + let cv = if let Some(assoc) = s.base().tcx.opt_associated_item(ucv.def) && + assoc.trait_item_def_id.is_some() { + // This must be a trait declaration constant + trait_const_to_constant_expr_kind(s, ucv.def, ucv.substs, &assoc) + } + else { + // Top-level constant or a constant appearing in an impl block + let id = ucv.def.sinto(s); + ConstantExprKind::GlobalName { id } + }; + TranslateUnevalRes::GlobalName(cv) } } } @@ -466,12 +520,36 @@ pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( .decorate(ty.sinto(s), span.sinto(s)) } ConstValue::ZeroSized { .. } => { - let ty = ty.sinto(s); - let is_ty_unit = matches!(&ty, Ty::Tuple(tys) if tys.is_empty()); - if !is_ty_unit { - supposely_unreachable_fatal!(s[span], "ExpectedTyUnit"; {val, ty}); - } - (ConstantExprKind::Tuple { fields: vec![] }).decorate(ty, span.sinto(s)) + // Should be unit + let hty = ty.sinto(s); + let cv = match &hty { + Ty::Tuple(tys) if tys.is_empty() => ConstantExprKind::Tuple { fields: Vec::new() }, + Ty::Arrow(_) => match ty.kind() { + rustc_middle::ty::TyKind::FnDef(def_id, substs) => { + let (def_id, generics, generics_impls, method_impl) = + get_function_from_def_id_and_substs(s, *def_id, substs); + + ConstantExprKind::FnPtr { + def_id, + generics, + generics_impls, + method_impl, + } + } + kind => { + fatal!(s[span], "Unexpected:"; {kind}) + } + }, + _ => { + fatal!( + s[span], + "Expected the type to be tuple or arrow"; + {val, ty} + ) + } + }; + + cv.decorate(hty, span.sinto(s)) } } } diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs index 644895281..8496ba73c 100644 --- a/frontend/exporter/src/rustc_utils.rs +++ b/frontend/exporter/src/rustc_utils.rs @@ -196,6 +196,7 @@ pub fn translate_span(span: rustc_span::Span, sess: &rustc_session::Session) -> lo: lo.into(), hi: hi.into(), filename: filename.sinto(&()), + rust_span_data: Some(span.data()), } } diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 0f5394be6..3f58508cd 100644 --- a/frontend/exporter/src/state.rs +++ b/frontend/exporter/src/state.rs @@ -139,7 +139,7 @@ mod types { options: hax_frontend_exporter_options::Options, ) -> Self { Self { - tcx: tcx.clone(), + tcx, macro_infos: Rc::new(HashMap::new()), cached_thirs: Rc::new(HashMap::new()), options: Rc::new(options), @@ -185,16 +185,27 @@ impl<'tcx> State, (), (), ()> { } } -impl<'tcx> State, (), Rc>, ()> { +impl<'tcx> State, (), (), rustc_hir::def_id::DefId> { + pub fn new_from_state_and_id>(s: &S, id: rustc_hir::def_id::DefId) -> Self { + State { + thir: (), + mir: (), + owner_id: id, + base: s.base().clone(), + } + } +} +impl<'tcx> State, (), Rc>, rustc_hir::def_id::DefId> { pub fn new_from_mir( tcx: rustc_middle::ty::TyCtxt<'tcx>, options: hax_frontend_exporter_options::Options, mir: rustc_middle::mir::Body<'tcx>, + owner_id: rustc_hir::def_id::DefId, ) -> Self { Self { thir: (), mir: Rc::new(mir), - owner_id: (), + owner_id, base: Base::new(tcx, options), } } diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 211dd69e5..09ea00209 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -127,7 +127,11 @@ mod search_clause { let tcx = s.base().tcx; let x = tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x); let y = tcx.try_normalize_erasing_regions(param_env, y).unwrap_or(y); - let result = format!("{:?}", x) == format!("{:?}", y); + // Below: "~const " may appear in the string, and comes from the way the + // trait ref is internalized by rustc. We remove such occurrences (yes, this is sad). + let sx = format!("{:?}", x).replace("~const ", ""); + let sy = format!("{:?}", y).replace("~const ", ""); + let result = sx == sy; const DEBUG: bool = false; if DEBUG && result { use crate::{Predicate, SInto}; diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index ccac8cdca..3e4060d1a 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -247,6 +247,9 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto } } +// For ConstantKind we merge all the cases (Ty, Val, Unevaluated) into one +pub type ConstantKind = ConstantExpr; + impl SInto for rustc_middle::mir::interpret::AllocId { fn sinto(&self, _: &S) -> u64 { self.0.get() @@ -803,16 +806,48 @@ pub struct ExpnData { } /// Reflects [`rustc_span::Span`] -#[derive( - Clone, Debug, Serialize, Deserialize, JsonSchema, PartialEq, Eq, Hash, PartialOrd, Ord, -)] +#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema, Eq, Ord)] pub struct Span { pub lo: Loc, pub hi: Loc, pub filename: FileName, + /// Original rustc span; can be useful for reporting rustc + /// diagnostics (this is used in Charon) + #[serde(skip)] + pub rust_span_data: Option, // expn_backtrace: Vec, } +const _: () = { + // `rust_span_data` is a metadata that should *not* be taken into + // account while hashing or comparing + + impl std::hash::Hash for Span { + fn hash(&self, state: &mut H) { + self.lo.hash(state); + self.hi.hash(state); + self.filename.hash(state); + } + } + impl PartialEq for Span { + fn eq(&self, other: &Self) -> bool { + self.lo == other.lo && self.hi == other.hi && self.filename == other.filename + } + } + + impl PartialOrd for Span { + fn partial_cmp(&self, other: &Self) -> Option { + Some( + self.lo.partial_cmp(&other.lo)?.then( + self.hi + .partial_cmp(&other.hi)? + .then(self.filename.partial_cmp(&other.filename)?), + ), + ) + } + } +}; + impl Into for rustc_span::Loc { fn into(self) -> Loc { Loc { @@ -961,41 +996,6 @@ pub struct Block { pub safety_mode: BlockSafety, } -/// Reflects [`rustc_middle::ty::AliasTy`] -#[derive( - Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, -)] -pub struct AliasTy { - pub substs: Vec, - pub trait_def_id: Option<(DefId, ImplExpr)>, - /// If the alias is a projection (e.g. `>::N<...>`), - /// `trait_def_id` contains the identifier for `Trait` and the - /// impl expressions that satisfies `Ty: Trait<...>`. - pub def_id: DefId, -} - -impl<'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_middle::ty::AliasTy<'tcx> { - fn sinto(&self, s: &S) -> AliasTy { - let tcx = s.base().tcx; - use rustc_hir::def::DefKind::*; - let trait_def_id = matches!( - tcx.def_kind(self.def_id), - AssocTy | AssocConst | ImplTraitPlaceholder - ) - .then(|| { - ( - self.trait_def_id(tcx).sinto(s), - self.trait_ref(tcx).impl_expr(s, get_param_env(s)), - ) - }); - AliasTy { - substs: self.substs.sinto(s), - trait_def_id, - def_id: self.def_id.sinto(s), - } - } -} - /// Reflects [`rustc_middle::thir::BindingMode`] #[derive(AdtInto)] #[args(, from: rustc_middle::thir::BindingMode, state: S as s)] @@ -1535,18 +1535,56 @@ pub struct TyGenerics { pub has_late_bound_regions: Option, } -/// Reflects [`rustc_type_ir::sty::AliasKind`] -#[derive(AdtInto)] -#[args(, from: rustc_type_ir::sty::AliasKind, state: S as _s)] +/// This type merges the information from +/// `rustc_type_ir::sty::AliasKind` and `rustc_middle::ty::AliasTy` +#[derive( + Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, +)] +pub struct Alias { + pub kind: AliasKind, + pub substs: Vec, + pub def_id: DefId, +} + #[derive( Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, )] pub enum AliasKind { - Projection, + /// The projection of a trait type: `>::N<...>` + Projection { + assoc_item: AssocItem, + impl_expr: ImplExpr, + }, Inherent, Opaque, } +impl Alias { + fn from<'tcx, S: BaseState<'tcx> + HasOwnerId>( + s: &S, + alias_kind: &rustc_type_ir::sty::AliasKind, + alias_ty: &rustc_middle::ty::AliasTy<'tcx>, + ) -> Self { + use rustc_type_ir::sty::AliasKind as RustAliasKind; + let kind = match alias_kind { + RustAliasKind::Projection => { + let tcx = s.base().tcx; + AliasKind::Projection { + assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s), + impl_expr: alias_ty.trait_ref(tcx).impl_expr(s, get_param_env(s)), + } + } + RustAliasKind::Inherent => AliasKind::Inherent, + RustAliasKind::Opaque => AliasKind::Opaque, + }; + Alias { + kind, + substs: alias_ty.substs.sinto(s), + def_id: alias_ty.def_id.sinto(s), + } + } +} + /// Reflects [`rustc_middle::ty::TyKind`] #[derive(AdtInto)] #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::TyKind<'tcx>, state: S as state)] @@ -1597,7 +1635,12 @@ pub enum Ty { Generator(DefId, Vec, Movability), Never, Tuple(Vec), - Alias(AliasKind, AliasTy), + #[custom_arm( + rustc_middle::ty::TyKind::Alias(alias_kind, alias_ty) => { + Ty::Alias(Alias::from(state, alias_kind, alias_ty)) + }, + )] + Alias(Alias), Param(ParamTy), Bound(DebruijnIndex, BoundTy), Placeholder(PlaceholderType), @@ -2412,6 +2455,11 @@ pub type ThirBody = Expr; impl<'x, 'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_hir::Ty<'x> { fn sinto(self: &rustc_hir::Ty<'x>, s: &S) -> Ty { + // **Important:** + // We need a local id here, and we get it from the owner id, which must + // be local. It is safe to do so, because if we have access to a HIR ty, + // it necessarily means we are exploring a local item (we don't have + // access to the HIR of external objects, only their MIR). let ctx = rustc_hir_analysis::collect::ItemCtxt::new(s.base().tcx, s.owner_id().expect_local()); ctx.to_ty(self).sinto(s) @@ -3094,15 +3142,48 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_middle::ty::Term<' } } -/// Reflects [`rustc_middle::ty::ProjectionPredicate`] -#[derive(AdtInto)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::ProjectionPredicate<'tcx>, state: S as tcx)] +/// Expresses a constraints over an associated type. +/// +/// For instance: +/// ```text +/// fn f>(...) +/// ^^^^^^^^^^ +/// ``` +/// (provided the trait `Foo` has an associated type `S`). #[derive( Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, )] pub struct ProjectionPredicate { - pub projection_ty: AliasTy, - pub term: Term, + pub impl_expr: ImplExpr, + pub assoc_item: AssocItem, + pub ty: Ty, +} + +impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto + for rustc_middle::ty::ProjectionPredicate<'tcx> +{ + fn sinto(&self, s: &S) -> ProjectionPredicate { + let AliasKind::Projection { + impl_expr, + assoc_item, + } = Alias::from( + s, + &rustc_middle::ty::AliasKind::Projection, + &self.projection_ty, + ) + .kind + else { + unreachable!() + }; + let Term::Ty(ty) = self.term.sinto(s) else { + unreachable!() + }; + ProjectionPredicate { + impl_expr, + assoc_item, + ty, + } + } } /// Reflects [`rustc_middle::ty::Clause`] diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 43013e1b3..8a5fb84b6 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -1,4 +1,5 @@ use crate::prelude::*; +use tracing::trace; #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] #[args(, from: rustc_middle::mir::MirPhase, state: S as s)] @@ -112,7 +113,7 @@ pub use mir_kinds::IsMirKind; pub struct Constant { pub span: Span, pub user_ty: Option, - pub literal: ConstantExpr, + pub literal: TypedConstantKind, } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] @@ -194,7 +195,7 @@ impl Operand { pub(crate) fn ty(&self) -> &Ty { match self { Operand::Copy(p) | Operand::Move(p) => &p.ty, - Operand::Constant(c) => &c.literal.ty, + Operand::Constant(c) => &c.literal.typ, } } } @@ -206,15 +207,100 @@ pub struct Terminator { pub kind: TerminatorKind, } +pub(crate) fn get_function_from_def_id_and_substs<'tcx, S: BaseState<'tcx> + HasOwnerId>( + s: &S, + def_id: rustc_hir::def_id::DefId, + substs: rustc_middle::ty::subst::SubstsRef<'tcx>, +) -> (DefId, Vec, Vec, Option) { + let tcx = s.base().tcx; + let param_env = tcx.param_env(s.owner_id()); + + // Retrieve the trait requirements for the **method**. + // For instance, if we write: + // ``` + // fn foo(...) + // ^^^ + // ``` + let trait_refs = solve_item_traits(s, param_env, def_id, substs, None); + + // Check if this is a trait method call: retrieve the trait source if + // it is the case (i.e., where does the method come from? Does it refer + // to a top-level implementation? Or the method of a parameter? etc.). + // At the same time, retrieve the trait obligations for this **trait**. + // Remark: the trait obligations for the method are not the same as + // the trait obligations for the trait. More precisely: + // + // ``` + // trait Foo { + // ^^^^^ + // trait level trait obligation + // fn baz(...) where T : ... { + // ... ^^^ + // method level trait obligation + // } + // } + // ``` + // + // Also, a function doesn't need to belong to a trait to have trait + // obligations: + // ``` + // fn foo(...) + // ^^^ + // method level trait obligation + // ``` + let (substs, source) = if let Some(assoc) = tcx.opt_associated_item(def_id) && + assoc.container == rustc_middle::ty::AssocItemContainer::TraitContainer { + // There is an associated item, and it is a trait + use tracing::*; + trace!("def_id: {:?}", def_id); + trace!("assoc: def_id: {:?}", assoc.def_id); + + // Retrieve the trait information + let impl_expr = get_trait_info(s, substs, &assoc); + + // Compute the list of generic arguments applied to the *method* itself. + // + // For instance, if we have: + // ``` + // trait Foo { + // fn baz(...) { ... } + // } + // + // fn test(x: T) { + // x.baz(...); + // ... + // } + // ``` + // The substs will be the concatenation: `` + // We count how many generic parameters the trait declaration has, + // and truncate the substitution to get the parameters which apply + // to the method (here, ``) + let trait_def_id : rustc_span::def_id::DefId = + (&impl_expr.r#trait.def_id).into(); + let params_info = get_params_info(s, trait_def_id); + let num_trait_generics = params_info.num_generic_params; + let all_generics: Vec = substs.sinto(s); + let truncated_substs = all_generics[num_trait_generics..].into(); + + // Return + (truncated_substs, Option::Some(impl_expr)) + } else { + // Regular function call + (substs.sinto(s), Option::None) + }; + + (def_id.sinto(s), substs, trait_refs, source) +} + /// Return the [DefId] of the function referenced by an operand, with the /// parameters substitution. /// The [Operand] comes from a [TerminatorKind::Call]. /// Only supports calls to top-level functions (which are considered as constants /// by rustc); doesn't support closures for now. -fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx>>( +fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>( s: &S, func: &rustc_middle::mir::Operand<'tcx>, -) -> (DefId, Vec) { +) -> (FunOperand, Vec, Vec, Option) { use std::ops::Deref; // Match on the func operand: it should be a constant as we don't support // closures for now. @@ -222,15 +308,16 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx>>( use rustc_middle::ty::TyKind; match func { Operand::Constant(c) => { + // Regular function case let c = c.deref(); - match &c.literal { + let (def_id, substs) = match &c.literal { ConstantKind::Ty(c) => { // The type of the constant should be a FnDef, allowing // us to retrieve the function's identifier and instantiation. let c_ty = c.ty(); assert!(c_ty.is_fn()); match c_ty.kind() { - TyKind::FnDef(def_id, subst) => (def_id.sinto(s), subst.sinto(s)), + TyKind::FnDef(def_id, substs) => (*def_id, *substs), _ => { unreachable!(); } @@ -240,7 +327,7 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx>>( // Same as for the `Ty` case above assert!(c_ty.is_fn()); match c_ty.kind() { - TyKind::FnDef(def_id, subst) => (def_id.sinto(s), subst.sinto(s)), + TyKind::FnDef(def_id, substs) => (*def_id, *substs), _ => { unreachable!(); } @@ -249,19 +336,82 @@ fn get_function_from_operand<'tcx, S: UnderOwnerState<'tcx>>( ConstantKind::Unevaluated(_, _) => { unimplemented!(); } - } + }; + + let (fun_id, substs, trait_refs, trait_info) = + get_function_from_def_id_and_substs(s, def_id, substs); + (FunOperand::Id(fun_id), substs, trait_refs, trait_info) } - Operand::Move(_place) | Operand::Copy(_place) => { - unimplemented!(); + Operand::Move(place) => { + // Closure case. + // The closure can not have bound variables nor trait references, + // so we don't need to extract generics, trait refs, etc. + let body = s.mir(); + let ty = func.ty(&body.local_decls, s.base().tcx); + trace!("type: {:?}", ty); + trace!("type kind: {:?}", ty.kind()); + let sig = match ty.kind() { + rustc_middle::ty::TyKind::FnPtr(sig) => sig, + _ => unreachable!(), + }; + trace!("FnPtr: {:?}", sig); + let place = place.sinto(s); + + (FunOperand::Move(place), Vec::new(), Vec::new(), None) + } + Operand::Copy(_place) => { + unimplemented!("{:?}", func); + } + } +} + +fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasOwnerId>( + s: &S, + terminator: &rustc_middle::mir::TerminatorKind<'tcx>, +) -> TerminatorKind { + if let rustc_middle::mir::TerminatorKind::Call { + func, + args, + destination, + target, + unwind, + from_hir_call, + fn_span, + } = terminator + { + let (fun, substs, trait_refs, trait_info) = get_function_from_operand(s, func); + + TerminatorKind::Call { + fun, + substs, + args: args.sinto(s), + destination: destination.sinto(s), + target: target.sinto(s), + unwind: unwind.sinto(s), + from_hir_call: from_hir_call.sinto(s), + fn_span: fn_span.sinto(s), + trait_refs, + trait_info, } + } else { + unreachable!() } } +// We don't use the LitIntType on purpose (we don't want the "unsuffixed" case) +#[derive( + Clone, Copy, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, +)] +pub enum IntUintTy { + Int(IntTy), + Uint(UintTy), +} + #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub struct ScalarInt { /// Little-endian representation of the integer pub data_le_bytes: [u8; 16], - pub int_ty: IntTy, + pub int_ty: IntUintTy, } // TODO: naming conventions: is "translate" ok? @@ -276,39 +426,39 @@ fn translate_switch_targets<'tcx, S: UnderOwnerState<'tcx>>( match switch_ty { Ty::Bool => { - // This is an: `if ... then ... else ...`. We are matching - // on a boolean casted to an integer: `false` is `0`, - // `true` is `1`. Thus the `otherwise` branch correspond - // to the `then` branch. - const FALSE: u128 = false as u128; - let [(FALSE, else_branch)] = targets_vec.as_slice() else { - supposely_unreachable_fatal!(s, "MirSwitchBool"; {targets_vec, switch_ty}); - }; + // This is an: `if ... then ... else ...` + assert!(targets_vec.len() == 1); + // It seems the block targets are inverted + let (test_val, otherwise_block) = targets_vec[0]; - SwitchTargets::If { - then_branch: targets.otherwise().sinto(s), - else_branch: *else_branch, - } + assert!(test_val == 0); + + // It seems the block targets are inverted + let if_block = targets.otherwise().sinto(s); + + SwitchTargets::If(if_block, otherwise_block) } - Ty::Int(int_ty) => { + Ty::Int(_) | Ty::Uint(_) => { + let int_ty = match switch_ty { + Ty::Int(ty) => IntUintTy::Int(*ty), + Ty::Uint(ty) => IntUintTy::Uint(*ty), + _ => unreachable!(), + }; + // This is a: switch(int). // Convert all the test values to the proper values. - SwitchTargets::SwitchInt { - scrutinee_type: *int_ty, - branches: targets_vec - .into_iter() - .map(|(v, tgt)| { - ( - ScalarInt { - data_le_bytes: v.to_le_bytes(), - int_ty: *int_ty, - }, - tgt, - ) - }) - .collect(), - otherwise_branch: targets.otherwise().sinto(s), + let mut targets_map: Vec<(ScalarInt, BasicBlock)> = Vec::new(); + for (v, tgt) in targets_vec { + // We need to reinterpret the bytes (`v as i128` is not correct) + let v = ScalarInt { + data_le_bytes: v.to_le_bytes(), + int_ty, + }; + targets_map.push((v, tgt)); } + let otherwise_block = targets.otherwise().sinto(s); + + SwitchTargets::SwitchInt(int_ty, targets_map, otherwise_block) } _ => { fatal!(s, "Unexpected switch_ty: {:?}", switch_ty) @@ -318,18 +468,20 @@ fn translate_switch_targets<'tcx, S: UnderOwnerState<'tcx>>( #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub enum SwitchTargets { - If { - then_branch: BasicBlock, - else_branch: BasicBlock, - }, + /// Gives the `if` block and the `else` block + If(BasicBlock, BasicBlock), /// Gives the integer type, a map linking values to switch branches, and the /// otherwise block. Note that matches over enumerations are performed by /// switching over the discriminant, which is an integer. - SwitchInt { - scrutinee_type: IntTy, - branches: Vec<(ScalarInt, BasicBlock)>, - otherwise_branch: BasicBlock, - }, + SwitchInt(IntUintTy, Vec<(ScalarInt, BasicBlock)>, BasicBlock), +} + +#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] +pub enum FunOperand { + /// Call to a top-level function designated by its id + Id(DefId), + /// Use of a closure + Move(Place), } #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] @@ -362,12 +514,16 @@ pub enum TerminatorKind { unwind: UnwindAction, replace: bool, }, - #[use_field(func)] - #[prepend(let (fun_id, substs) = get_function_from_operand(s, func);)] + #[custom_arm( + x @ rustc_middle::mir::TerminatorKind::Call { .. } => { + translate_terminator_kind_call(s, x) + } + )] Call { - #[value(fun_id)] - fun_id: DefId, - #[value(substs)] + fun: FunOperand, + /// We truncate the substitution so as to only include the arguments + /// relevant to the method (and not the trait) if it is a trait method + /// call. See [ParamsInfo] for the full details. substs: Vec, args: Vec, destination: Place, @@ -375,6 +531,8 @@ pub enum TerminatorKind { unwind: UnwindAction, from_hir_call: bool, fn_span: Span, + trait_refs: Vec, + trait_info: Option, }, Assert { cond: Operand, @@ -458,9 +616,11 @@ pub enum ProjectionElemFieldKind { Tuple(FieldIdx), Adt { typ: DefId, - variant_info: VariantInformations, + variant: Option, index: FieldIdx, }, + /// Get access to one of the fields of the state of a closure + ClosureState(FieldIdx), } #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] @@ -497,26 +657,27 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto use rustc_middle::mir::ProjectionElem::*; let cur_ty = current_ty.clone(); let cur_kind = current_kind.clone(); + use rustc_middle::ty::TyKind; let mk_field = |index: &rustc_abi::FieldIdx, variant_idx: Option| { ProjectionElem::Field(match cur_ty.kind() { - rustc_middle::ty::TyKind::Adt(adt_def, _) => { - let variant_info = - get_variant_information(adt_def, rustc_abi::FIRST_VARIANT, s); + TyKind::Adt(adt_def, _) => { + assert!( + (adt_def.is_struct() && variant_idx.is_none()) + || (adt_def.is_enum() && variant_idx.is_some()) + ); ProjectionElemFieldKind::Adt { typ: adt_def.did().sinto(s), + variant: variant_idx.map(|id| id.sinto(s)), index: index.sinto(s), - variant_info, } } - rustc_middle::ty::TyKind::Tuple(_types) => { - ProjectionElemFieldKind::Tuple(index.sinto(s)) - } + TyKind::Tuple(_types) => ProjectionElemFieldKind::Tuple(index.sinto(s)), ty_kind => { supposely_unreachable_fatal!( s, "ProjectionElemFieldBadType"; - {index, variant_idx, ty_kind, &cur_ty, &cur_kind} - ) + {index, ty_kind, variant_idx, &cur_ty, &cur_kind} + ); } }) }; @@ -543,17 +704,30 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto ProjectionElem::Deref } Field(index, ty) => { - let r = mk_field(index, None); - current_ty = ty.clone(); - r + if let TyKind::Closure(_, substs) = cur_ty.kind() { + // We get there when we access one of the fields + // of the the state captured by a closure. + use crate::rustc_index::Idx; + let substs = substs.as_closure(); + let upvar_tys: Vec<_> = substs.upvar_tys().collect(); + current_ty = upvar_tys[index.sinto(s).index()].clone(); + ProjectionElem::Field(ProjectionElemFieldKind::ClosureState( + index.sinto(s), + )) + } else { + let r = mk_field(index, None); + current_ty = ty.clone(); + r + } } Index(local) => { let (TyKind::Slice(ty) | TyKind::Array(ty, _)) = current_ty.kind() else { supposely_unreachable_fatal!( - s, "PlaceIndexNotSlice"; + s, + "PlaceIndexNotSlice"; {current_ty, current_kind, elem} - ) + ); }; current_ty = ty.clone(); ProjectionElem::Index(local.sinto(s)) @@ -610,18 +784,57 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto } } +#[derive( + Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, +)] +pub struct MirFnSig { + pub inputs: Vec, + pub output: Ty, + pub c_variadic: bool, + pub unsafety: Unsafety, + pub abi: Abi, +} + +pub type MirPolyFnSig = Binder; + +impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto for rustc_middle::ty::FnSig<'tcx> { + fn sinto(&self, s: &S) -> MirFnSig { + let inputs = self.inputs().sinto(s); + let output = self.output().sinto(s); + MirFnSig { + inputs, + output, + c_variadic: self.c_variadic, + unsafety: self.unsafety.sinto(s), + abi: self.abi.sinto(s), + } + } +} + +// TODO: we need this function because sometimes, Rust doesn't infer the proper +// typeclass instance. +pub(crate) fn poly_fn_sig_to_mir_poly_fn_sig<'tcx, S: BaseState<'tcx> + HasOwnerId>( + sig: &rustc_middle::ty::PolyFnSig<'tcx>, + s: &S, +) -> MirPolyFnSig { + sig.sinto(s) +} + #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)] #[args(<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>, from: rustc_middle::mir::AggregateKind<'tcx>, state: S as s)] pub enum AggregateKind { Array(Ty), Tuple, - #[custom_arm(rustc_middle::mir::AggregateKind::Adt(def_id, vid, args, annot, fid) => { + #[custom_arm(rustc_middle::mir::AggregateKind::Adt(def_id, vid, substs, annot, fid) => { let adt_kind = s.base().tcx.adt_def(def_id).adt_kind().sinto(s); + let param_env = s.base().tcx.param_env(s.owner_id()); + let trait_refs = solve_item_traits(s, param_env, *def_id, substs, None); AggregateKind::Adt( def_id.sinto(s), vid.sinto(s), adt_kind, - args.sinto(s), + substs.sinto(s), + trait_refs, annot.sinto(s), fid.sinto(s)) })] @@ -630,10 +843,33 @@ pub enum AggregateKind { VariantIdx, AdtKind, Vec, + Vec, Option, Option, ), - Closure(DefId, Vec), + #[custom_arm(rustc_middle::mir::AggregateKind::Closure(rust_id, substs) => { + let def_id : DefId = rust_id.sinto(s); + // The substs is meant to be converted to a function signature. Note + // that Rustc does its job: the PolyFnSig binds the captured local + // type, regions, etc. variables, which means we can treat the local + // closure like any top-level function. + let closure = substs.as_closure(); + let sig = closure.sig(); + let sig = poly_fn_sig_to_mir_poly_fn_sig(&sig, s); + + // Solve the trait obligations. Note that we solve the parent + let tcx = s.base().tcx; + let param_env = tcx.param_env(s.owner_id()); + let parent_substs = closure.parent_substs(); + let substs = tcx.mk_substs(parent_substs); + // Retrieve the predicates from the parent (i.e., the function which calls + // the closure). + let predicates = tcx.predicates_defined_on(tcx.generics_of(rust_id).parent.unwrap()); + + let trait_refs = solve_item_traits(s, param_env, *rust_id, substs, Some(predicates)); + AggregateKind::Closure(def_id, parent_substs.sinto(s), trait_refs, sig) + })] + Closure(DefId, Vec, Vec, MirPolyFnSig), Generator(DefId, Vec, Movability), } @@ -665,6 +901,12 @@ pub enum NullOp { #[args(<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>, from: rustc_middle::mir::Rvalue<'tcx>, state: S as s)] pub enum Rvalue { Use(Operand), + #[custom_arm( + rustc_middle::mir::Rvalue::Repeat(op, ce) => { + let op = op.sinto(s); + Rvalue::Repeat(op, ce.sinto(s)) + }, + )] Repeat(Operand, ConstantExpr), Ref(Region, BorrowKind, Place), ThreadLocalRef(DefId), diff --git a/frontend/exporter/src/types/mir_traits.rs b/frontend/exporter/src/types/mir_traits.rs new file mode 100644 index 000000000..320fe1c82 --- /dev/null +++ b/frontend/exporter/src/types/mir_traits.rs @@ -0,0 +1,302 @@ +use crate::prelude::*; + +/// Retrieve the trait information, typically for a function call. +/// TODO: rename +pub fn get_trait_info<'tcx, S: UnderOwnerState<'tcx>>( + s: &S, + substs: rustc_middle::ty::SubstsRef<'tcx>, + assoc: &rustc_middle::ty::AssocItem, +) -> ImplExpr { + let tcx = s.base().tcx; + let param_env = tcx.param_env(s.owner_id()); + + // Retrieve the trait + let tr_def_id = tcx.trait_of_item(assoc.def_id).unwrap(); + + // Create the reference to the trait + use rustc_middle::ty::TraitRef; + let tr_ref = TraitRef::new(tcx, tr_def_id, substs); + let tr_ref = rustc_middle::ty::Binder::dummy(tr_ref); + + // Solve + solve_trait(s, param_env, tr_ref) +} + +pub fn solve_trait<'tcx, S: BaseState<'tcx> + HasOwnerId>( + s: &S, + param_env: rustc_middle::ty::ParamEnv<'tcx>, + trait_ref: rustc_middle::ty::PolyTraitRef<'tcx>, +) -> ImplExpr { + let mut impl_expr = trait_ref.impl_expr(s, param_env); + // TODO: this is a bug in hax: in case of method calls, the trait ref + // contains the generics for the trait ref + the generics for the method + let trait_def_id: rustc_hir::def_id::DefId = (&impl_expr.r#trait.def_id).into(); + let params_info = get_params_info(s, trait_def_id); + impl_expr + .r#trait + .generic_args + .truncate(params_info.num_generic_params); + impl_expr +} + +/// Solve the trait obligations for a specific item use (for example, a method +/// call, an ADT, etc.). +/// +/// [predicates]: optional predicates, in case we want to solve custom predicates +/// (instead of the ones returned by [TyCtxt::predicates_defined_on]. +pub fn solve_item_traits<'tcx, S: UnderOwnerState<'tcx>>( + s: &S, + param_env: rustc_middle::ty::ParamEnv<'tcx>, + def_id: rustc_hir::def_id::DefId, + substs: rustc_middle::ty::subst::SubstsRef<'tcx>, + predicates: Option>, +) -> Vec { + let tcx = s.base().tcx; + + let mut impl_exprs = Vec::new(); + + // Lookup the predicates and iter through them: we want to solve all the + // trait requirements. + // IMPORTANT: we use [TyCtxt::predicates_defined_on] and not [TyCtxt::predicated_of] + let predicates = match predicates { + None => tcx.predicates_defined_on(def_id), + Some(preds) => preds, + }; + for (pred, _) in predicates.predicates { + // Apply the substitution + let pred_kind = subst_binder(tcx, substs, param_env, pred.kind(), true); + + // Just explore the trait predicates + use rustc_middle::ty::{Clause, PredicateKind}; + if let PredicateKind::Clause(Clause::Trait(trait_pred)) = pred_kind { + // SH: We also need to introduce a binder here. I'm not sure what we + // whould bind this with: the variables to bind with are those + // given by the definition we are exploring, and they should already + // be in the param environment. So I just wrap in a dummy binder + // (this also seems to work so far). + // + // Also, we can't wrap in a dummy binder if there are escaping bound vars. + // For now, we fail if there are escaping bound vars. + // **SH:** I encountered this issue several times, but the "error" + // clause never made it to the final code. I think it is because it + // was introduced when computing the "full trait ref" information. + let trait_ref = trait_pred.trait_ref; + use crate::rustc_middle::ty::TypeVisitableExt; + let impl_expr = if trait_ref.has_escaping_bound_vars() { + supposely_unreachable_fatal!(s, "mir_traits: has escaping bound vars"; { + trait_ref, def_id + }) + } else { + // Ok + let trait_ref = rustc_middle::ty::Binder::dummy(trait_pred.trait_ref); + solve_trait(s, param_env, trait_ref) + }; + + impl_exprs.push(impl_expr); + } + } + impl_exprs +} + +/// Small helper +/// +/// Introducing this to make sure all binders are handled in a consistent manner. +pub(crate) fn subst_early_binder<'tcx, T>( + tcx: rustc_middle::ty::TyCtxt<'tcx>, + param_substs: rustc_middle::ty::SubstsRef<'tcx>, + param_env: rustc_middle::ty::ParamEnv<'tcx>, + value: rustc_middle::ty::EarlyBinder, + normalize_erase: bool, +) -> T +where + T: rustc_middle::ty::TypeFoldable>, +{ + // SH: Not sure this is the proper way, but it seems to work so far. My reasoning: + // - I don't know how to get rid of the Binder, because there is no + // Binder::subst method. + // - However I notice that EarlyBinder is just a wrapper (it doesn't + // contain any information) and comes with substitution methods. + // So I skip the Binder, wrap the value in an EarlyBinder and apply + // the substitution. + // Remark: there is also EarlyBinder::subst(...) + + // Apply the substitution. + // + // **Remark:** we used to always call [TyCtxt::subst_and_normalize_erasing_regions], + // but this normalizes the types, leading to issues. For instance here: + // ``` + // pub fn f, U: Foo>() {} + // ``` + // The issue is that T refers `U : Foo` before the clause is + // defined. If we normalize the types in the items of `T : Foo`, + // when exploring the items of `Foo` we find the clause + // `Sized` (instead of `Sized`) because `T::S` has + // been normalized to `U::S`. This can be problematic when + // solving the parameters. + if normalize_erase { + tcx.subst_and_normalize_erasing_regions(param_substs, param_env, value) + } else { + // Remark: in more recent versions of the compiler: [instantiate] + value.subst(tcx, param_substs) + } +} + +/// Small helper. +/// +/// Introducing this to make sure all binders are handled in a consistent manner. +/// +/// [normalize_erase]: should we normalize the types and erase the regions? +pub(crate) fn subst_binder<'tcx, T>( + tcx: rustc_middle::ty::TyCtxt<'tcx>, + param_substs: rustc_middle::ty::SubstsRef<'tcx>, + param_env: rustc_middle::ty::ParamEnv<'tcx>, + value: rustc_middle::ty::Binder<'tcx, T>, + normalize_erase: bool, +) -> T +where + T: rustc_middle::ty::TypeFoldable>, +{ + // SH: Not sure this is the proper way, but it seems to work so far. My reasoning: + // - I don't know how to get rid of the Binder, because there is no + // Binder::subst method. + // - However I notice that EarlyBinder is just a wrapper (it doesn't + // contain any information) and comes with substitution methods. + // So I skip the Binder, wrap the value in an EarlyBinder and apply + // the substitution. + // Remark: there is also EarlyBinder::subst(...) + let value = rustc_middle::ty::EarlyBinder::bind(value.skip_binder()); + subst_early_binder(tcx, param_substs, param_env, value, normalize_erase) +} + +/// We use this to store information about the parameters in parent blocks. +/// This is necessary because when querying the generics of a definition, +/// rustc gives us *all* the generics used in this definition, including +/// those coming from the outer impl block. +/// +/// For instance: +/// ```text +/// impl Foo { +/// ^^^ +/// outer block generics +/// fn bar(...) { ... } +/// ^^^ +/// generics local to the function bar +/// } +/// ``` +/// +/// `TyCtxt.generics_of(bar)` gives us: `[T, U]`. +/// +/// We however sometimes need to make a distinction between those two kinds +/// of generics, in particular when manipulating trait instances. For instance: +/// +/// ```text +/// impl Foo for Bar { +/// fn baz(...) { ... } +/// } +/// +/// fn test(...) { +/// // Here: +/// x.baz(...); +/// // We should refer to this call as: +/// // > Foo::baz(...) +/// // +/// // If baz hadn't been a method implementation of a trait, +/// // we would have refered to it as: +/// // > baz(...) +/// // +/// // The reason is that with traits, we refer to the whole +/// // trait implementation (as if it were a structure), then +/// // pick a specific method inside (as if projecting a field +/// // from a structure). +/// } +/// ``` +/// +/// **Remark**: Rust only allows refering to the generics of the **immediately** +/// outer block. For this reason, when we need to store the information about +/// the generics of the outer block(s), we need to do it only for one level +/// (this definitely makes things simpler). +/// **Additional remark**: it is not possible to directly write an impl block +/// or a trait definition inside an impl/trait block. However it is possible +/// to define an impl/trait inside a function, which can itself be inside a +/// block, leading to nested impl blocks. +#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] +pub struct ParamsInfo { + /// The total number of generic parameters (regions + types + consts). + /// We do not consider the trait clauses as generic parameters. + pub num_generic_params: usize, + pub num_region_params: usize, + pub num_type_params: usize, + pub num_const_generic_params: usize, + pub num_trait_clauses: usize, + pub num_regions_outlive: usize, + pub num_types_outlive: usize, + pub num_trait_type_constraints: usize, +} + +/// Compute the parameters information for a definition. See [ParamsInfo]. +pub fn get_params_info<'tcx, S: BaseState<'tcx> + HasOwnerId>( + s: &S, + def_id: rustc_hir::def_id::DefId, +) -> ParamsInfo { + let tcx = s.base().tcx; + + // Compute the number of generics + let mut num_region_params = 0; + let mut num_type_params = 0; + let mut num_const_generic_params = 0; + let mut num_regions_outlive = 0; + let mut num_types_outlive = 0; + let mut num_trait_type_constraints = 0; + + let generics = tcx.generics_of(def_id); + let num_generic_params = generics.params.len(); + use rustc_middle::ty::GenericParamDefKind; + for param in &generics.params { + match param.kind { + GenericParamDefKind::Lifetime => num_region_params += 1, + GenericParamDefKind::Type { .. } => num_type_params += 1, + GenericParamDefKind::Const { .. } => num_const_generic_params += 1, + } + } + + // Compute the number of trait clauses + let mut num_trait_clauses = 0; + // **IMPORTANT**: we do NOT want to [TyCtxt::predicates_of]. + // If we use [TyCtxt::predicates_of] on a trait `Foo`, we get an + // additional predicate `Self : Foo` (i.e., the trait requires itself), + // which is not what we want. + let preds = tcx.predicates_defined_on(def_id); + for (pred, _) in preds.predicates { + use rustc_middle::ty::{Clause, PredicateKind}; + match &pred.kind().skip_binder() { + PredicateKind::Clause(Clause::Trait(_)) => num_trait_clauses += 1, + PredicateKind::Clause(Clause::RegionOutlives(_)) => num_regions_outlive += 1, + PredicateKind::Clause(Clause::TypeOutlives(_)) => num_types_outlive += 1, + PredicateKind::Clause(Clause::Projection(_)) => num_trait_type_constraints += 1, + _ => (), + } + } + + ParamsInfo { + num_generic_params, + num_region_params, + num_type_params, + num_const_generic_params, + num_trait_clauses, + num_regions_outlive, + num_types_outlive, + num_trait_type_constraints, + } +} + +/// Compute the parameters information for a definition's parent. See [ParamsInfo]. +pub fn get_parent_params_info<'tcx, S: BaseState<'tcx> + HasOwnerId>( + s: &S, + def_id: rustc_hir::def_id::DefId, +) -> Option { + s.base() + .tcx + .generics_of(def_id) + .parent + .map(|parent_id| get_params_info(s, parent_id)) +} diff --git a/frontend/exporter/src/types/mod.rs b/frontend/exporter/src/types/mod.rs index f7d384609..64c149415 100644 --- a/frontend/exporter/src/types/mod.rs +++ b/frontend/exporter/src/types/mod.rs @@ -1,6 +1,7 @@ mod copied; mod index; mod mir; +mod mir_traits; mod new; mod replaced; mod todo; @@ -8,6 +9,7 @@ mod todo; pub use copied::*; pub use index::*; pub use mir::*; +pub use mir_traits::*; pub use new::*; pub use replaced::*; pub use todo::*; diff --git a/frontend/exporter/src/types/new.rs b/frontend/exporter/src/types/new.rs index bfaa141d1..e67658032 100644 --- a/frontend/exporter/src/types/new.rs +++ b/frontend/exporter/src/types/new.rs @@ -1,5 +1,16 @@ use crate::prelude::*; +impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto + for rustc_middle::mir::ConstantKind<'tcx> +{ + fn sinto(&self, s: &S) -> TypedConstantKind { + TypedConstantKind { + typ: self.ty().sinto(s), + constant_kind: self.sinto(s), + } + } +} + #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub struct ItemAttributes { attributes: Vec, @@ -15,6 +26,12 @@ impl ItemAttributes { } } +#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] +pub struct TypedConstantKind { + pub typ: Ty, + pub constant_kind: ConstantExpr, +} + lazy_static::lazy_static! { pub static ref CORE_EXTRACTION_MODE: bool = std::env::var_os("HAX_CORE_EXTRACTION_MODE") == Some("on".into()); diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 308c62d19..d54cf41d4 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -73,8 +73,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 = class t_Foo (v_Self: Type) = { f_AssocType:Type; - f_AssocType_6857934811705287863:t_SuperTrait f_AssocType; - f_AssocType_1499648403794240798:Core.Clone.t_Clone f_AssocType; + f_AssocType_886671949818196346:t_SuperTrait f_AssocType; + f_AssocType_8151908989361665585:Core.Clone.t_Clone f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> bool; f_assoc_f_post:Prims.unit -> Prims.unit -> bool; @@ -121,7 +121,7 @@ let g (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; - f_AssocType_6857934811705287863 = FStar.Tactics.Typeclasses.solve (); + f_AssocType_886671949818196346 = FStar.Tactics.Typeclasses.solve (); f_N = sz 32; f_assoc_f = () <: Prims.unit; f_method_f_pre = (fun (self: Prims.unit) -> true);