diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index f19449c2b..7af3249f8 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -518,7 +518,7 @@ end) : EXPR = struct let f = let f = c_expr fun' in match (trait, fun'.contents) with - | Some _, GlobalName { id } -> + | Some _, GlobalName { id; _ } -> { f with e = GlobalVar (def_id (AssociatedItem Value) id) } | _ -> f in @@ -638,7 +638,15 @@ end) : EXPR = struct trait = None (* TODO: see issue #328 *); bounds_impls = []; } - | GlobalName { id } -> GlobalVar (def_id Value id) + | GlobalName { id; constructor } -> + let kind = + match constructor with + | Some { kind = Struct _; _ } -> + Concrete_ident.Kind.Constructor { is_struct = true } + | Some _ -> Concrete_ident.Kind.Constructor { is_struct = false } + | None -> Concrete_ident.Kind.Value + in + GlobalVar (def_id kind id) | UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident Expr id) | Borrow { arg; borrow_kind = kind } -> let e' = c_expr arg in @@ -824,7 +832,8 @@ end) : EXPR = struct Array { fields = List.map ~f:constant_expr_to_expr fields } | Tuple { fields } -> Tuple { fields = List.map ~f:constant_expr_to_expr fields } - | GlobalName { id; _ } -> GlobalName { id } + | GlobalName { id; variant_information; _ } -> + GlobalName { id; constructor = variant_information } | Borrow arg -> Borrow { arg = constant_expr_to_expr arg; borrow_kind = Thir.Shared } | ConstRef { id } -> ConstRef { id } diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index a8e2afbf6..acaa7d0d7 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -62,6 +62,7 @@ pub enum ConstantExprKind { id: GlobalIdent, generics: Vec, trait_refs: Vec, + variant_information: Option, }, /// A trait constant /// @@ -181,7 +182,11 @@ mod rustc { id, generics: _, trait_refs: _, - } => ExprKind::GlobalName { id }, + variant_information, + } => ExprKind::GlobalName { + id, + constructor: variant_information, + }, Borrow(e) => ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg: e.into(), @@ -288,6 +293,7 @@ mod rustc { id: did.sinto(s), generics: Vec::new(), trait_refs: Vec::new(), + variant_information: None, }, GlobalAlloc::Memory(alloc) => { let values = alloc.inner().get_bytes_unchecked( @@ -442,6 +448,7 @@ mod rustc { id, generics, trait_refs, + variant_information: None, } } } else { @@ -452,6 +459,7 @@ mod rustc { id, generics: vec![], trait_refs: vec![], + variant_information: None, } }; let cv = kind.decorate(ty.sinto(s), span.sinto(s)); diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs index cb24dffca..8d4c56628 100644 --- a/frontend/exporter/src/rustc_utils.rs +++ b/frontend/exporter/src/rustc_utils.rs @@ -257,3 +257,16 @@ pub fn inline_macro_invocations<'t, S: BaseState<'t>, Body: IsBody>( }) .collect() } + +/// Gets the closest ancestor of `id` that is the id of a type. +pub fn get_closest_parent_type( + tcx: &ty::TyCtxt, + id: rustc_span::def_id::DefId, +) -> rustc_span::def_id::DefId { + match tcx.def_kind(id) { + rustc_hir::def::DefKind::Union + | rustc_hir::def::DefKind::Struct + | rustc_hir::def::DefKind::Enum => id, + _ => get_closest_parent_type(tcx, tcx.parent(id)), + } +} diff --git a/frontend/exporter/src/types/thir.rs b/frontend/exporter/src/types/thir.rs index 3c579297a..959ea3739 100644 --- a/frontend/exporter/src/types/thir.rs +++ b/frontend/exporter/src/types/thir.rs @@ -190,7 +190,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto for thir::Expr<'tcx> { return cexpr.into(); } thir::ExprKind::ZstLiteral { .. } => match ty.kind() { - rustc_middle::ty::TyKind::FnDef(def, _generics) => { + rustc_middle::ty::TyKind::FnDef(def_id, _generics) => { /* TODO: translate generics let tcx = s.base().tcx; let sig = &tcx.fn_sig(*def).instantiate(tcx, generics); @@ -201,8 +201,24 @@ impl<'tcx, S: ExprState<'tcx>> SInto for thir::Expr<'tcx> { let params: Vec = params.map(|i| tcx.erase_late_bound_regions(i)).collect(); */ + let tcx = s.base().tcx; + let constructor = if tcx.is_constructor(*def_id) { + let adt_def = + tcx.adt_def(rustc_utils::get_closest_parent_type(&tcx, *def_id)); + let variant_index = adt_def.variant_index_with_id(tcx.parent(*def_id)); + Some(rustc_utils::get_variant_information( + &adt_def, + variant_index, + s, + )) + } else { + None + }; return Expr { - contents: Box::new(ExprKind::GlobalName { id: def.sinto(s) }), + contents: Box::new(ExprKind::GlobalName { + id: def_id.sinto(s), + constructor, + }), span: self.span.sinto(s), ty: ty.sinto(s), hir_id, @@ -577,7 +593,8 @@ pub enum ExprKind { let (hir_id, attributes) = e.hir_id_and_attributes(gstate); let hir_id = hir_id.map(|hir_id| hir_id.index()); let contents = Box::new(ExprKind::GlobalName { - id: def_id.sinto(gstate) + id: def_id.sinto(gstate), + constructor: None }); let mut translated_generics = generics.sinto(gstate); let tcx = gstate.base().tcx; @@ -755,6 +772,7 @@ pub enum ExprKind { #[disable_mapping] GlobalName { id: GlobalIdent, + constructor: Option, }, UpvarRef { closure_def_id: DefId, diff --git a/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap new file mode 100644 index 000000000..6f8919b71 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap @@ -0,0 +1,46 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: fstar + info: + name: constructor-as-closure + manifest: constructor-as-closure/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Constructor_as_closure.fst" = ''' +module Constructor_as_closure +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_Context = + | Context_A : i32 -> t_Context + | Context_B : i32 -> t_Context + +type t_Test = | Test : i32 -> t_Test + +let impl__Test__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Test = + Core.Option.impl__map #i32 #t_Test x Test + +let impl__Context__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context = + Core.Option.impl__map #i32 #t_Context x Context_B +''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 2c6d55fa9..09cd8e14b 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -1,6 +1,6 @@ # This file is automatically @generated by Cargo. # It is not intended for manual editing. -version = 3 +version = 4 [[package]] name = "abstract_integers" @@ -150,6 +150,10 @@ dependencies = [ "os_str_bytes", ] +[[package]] +name = "constructor-as-closure" +version = "0.1.0" + [[package]] name = "criterion" version = "0.4.0" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 10969e04d..df3b03ffa 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -35,5 +35,6 @@ members = [ "guards", "cyclic-modules", "unsafe", + "constructor-as-closure", ] resolver = "2" diff --git a/tests/constructor-as-closure/Cargo.toml b/tests/constructor-as-closure/Cargo.toml new file mode 100644 index 000000000..523a0ff06 --- /dev/null +++ b/tests/constructor-as-closure/Cargo.toml @@ -0,0 +1,9 @@ +[package] +name = "constructor-as-closure" +version = "0.1.0" +edition = "2021" + +[dependencies] + +[package.metadata.hax-tests] +into."fstar" = { broken = false, snapshot = "stdout", issue_id = "914" } diff --git a/tests/constructor-as-closure/src/lib.rs b/tests/constructor-as-closure/src/lib.rs new file mode 100644 index 000000000..5d11085fe --- /dev/null +++ b/tests/constructor-as-closure/src/lib.rs @@ -0,0 +1,15 @@ +struct Test(i32); +impl Test { + pub fn test(x: Option) -> Option { + x.map(Self) + } +} +pub enum Context { + A(i32), + B(i32), +} +impl Context { + pub fn test(x: Option) -> Option { + x.map(Self::B) + } +}