From 70d54c9bfd6c942696fba4bea4264f50930d9bc4 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 24 Oct 2024 16:48:53 +0200 Subject: [PATCH 1/4] Fix for constructors passed as closure. --- engine/lib/import_thir.ml | 15 ++++++++++++--- frontend/exporter/src/constant_utils.rs | 10 +++++++++- frontend/exporter/src/rustc_utils.rs | 12 ++++++++++++ frontend/exporter/src/types/thir.rs | 25 +++++++++++++++++++++++-- 4 files changed, 56 insertions(+), 6 deletions(-) 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..4f3bd539c 100644 --- a/frontend/exporter/src/rustc_utils.rs +++ b/frontend/exporter/src/rustc_utils.rs @@ -257,3 +257,15 @@ pub fn inline_macro_invocations<'t, S: BaseState<'t>, Body: IsBody>( }) .collect() } + +pub fn 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, + _ => 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..9c2fe9398 100644 --- a/frontend/exporter/src/types/thir.rs +++ b/frontend/exporter/src/types/thir.rs @@ -201,8 +201,27 @@ 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 id: DefId = def.clone().sinto(s); + let rustc_id = (&id).into(); + let constructor = if tcx.is_constructor(rustc_id) { + let adt_def = + tcx.adt_def(rustc_utils::closest_parent_type(&tcx, rustc_id)); + let variant_id = tcx.parent(rustc_id); + let variant_index = adt_def.variant_index_with_id(variant_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.sinto(s), + constructor, + }), span: self.span.sinto(s), ty: ty.sinto(s), hir_id, @@ -577,7 +596,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 +775,7 @@ pub enum ExprKind { #[disable_mapping] GlobalName { id: GlobalIdent, + constructor: Option, }, UpvarRef { closure_def_id: DefId, From 7f82e378011997434da2cbc3d429374908eba2bd Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 24 Oct 2024 17:03:10 +0200 Subject: [PATCH 2/4] Add tests for constructor as closure. --- tests/Cargo.lock | 6 +++++- tests/Cargo.toml | 1 + tests/constructor-as-closure/Cargo.toml | 9 +++++++++ tests/constructor-as-closure/src/lib.rs | 15 +++++++++++++++ 4 files changed, 30 insertions(+), 1 deletion(-) create mode 100644 tests/constructor-as-closure/Cargo.toml create mode 100644 tests/constructor-as-closure/src/lib.rs 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) + } +} From 5bc769e7ad851c43d4b5219237018b48c26f6997 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 24 Oct 2024 17:18:33 +0200 Subject: [PATCH 3/4] Correct style. --- frontend/exporter/src/rustc_utils.rs | 5 +++-- frontend/exporter/src/types/thir.rs | 13 +++++-------- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs index 4f3bd539c..8d4c56628 100644 --- a/frontend/exporter/src/rustc_utils.rs +++ b/frontend/exporter/src/rustc_utils.rs @@ -258,7 +258,8 @@ pub fn inline_macro_invocations<'t, S: BaseState<'t>, Body: IsBody>( .collect() } -pub fn closest_parent_type( +/// 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 { @@ -266,6 +267,6 @@ pub fn closest_parent_type( rustc_hir::def::DefKind::Union | rustc_hir::def::DefKind::Struct | rustc_hir::def::DefKind::Enum => id, - _ => closest_parent_type(tcx, tcx.parent(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 9c2fe9398..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); @@ -202,13 +202,10 @@ impl<'tcx, S: ExprState<'tcx>> SInto for thir::Expr<'tcx> { params.map(|i| tcx.erase_late_bound_regions(i)).collect(); */ let tcx = s.base().tcx; - let id: DefId = def.clone().sinto(s); - let rustc_id = (&id).into(); - let constructor = if tcx.is_constructor(rustc_id) { + let constructor = if tcx.is_constructor(*def_id) { let adt_def = - tcx.adt_def(rustc_utils::closest_parent_type(&tcx, rustc_id)); - let variant_id = tcx.parent(rustc_id); - let variant_index = adt_def.variant_index_with_id(variant_id); + 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, @@ -219,7 +216,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto for thir::Expr<'tcx> { }; return Expr { contents: Box::new(ExprKind::GlobalName { - id: def.sinto(s), + id: def_id.sinto(s), constructor, }), span: self.span.sinto(s), From f3c98241eb347326ed9ea5c4d8073097a60b6f1d Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 24 Oct 2024 17:19:26 +0200 Subject: [PATCH 4/4] Add test snapshot for constructor-as-closure. --- ...in__constructor-as-closure into-fstar.snap | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap 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 +'''