Merge pull request #1039 from hacspec/fix-914

Fix 914

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 }

frontend/exporter/src/constant_utils.rs

@@ -62,6 +62,7 @@ pub enum ConstantExprKind {
         id: GlobalIdent,
         generics: Vec<GenericArg>,
         trait_refs: Vec<ImplExpr>,
+        variant_information: Option<VariantInformations>,
     },
     /// 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));

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)),
+    }
+}

frontend/exporter/src/types/thir.rs

@@ -190,7 +190,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> 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<S, Expr> for thir::Expr<'tcx> {
                         let params: Vec<rustc_middle::ty::Ty> =
                         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<VariantInformations>,
     },
     UpvarRef {
         closure_def_id: DefId,

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
+'''

tests/Cargo.toml

@@ -35,5 +35,6 @@ members = [
         "guards",
         "cyclic-modules",
         "unsafe",
+        "constructor-as-closure",
 ]
 resolver = "2"

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" }

tests/constructor-as-closure/src/lib.rs

@@ -0,0 +1,15 @@
+struct Test(i32);
+impl Test {
+    pub fn test(x: Option<i32>) -> Option<Test> {
+        x.map(Self)
+    }
+}
+pub enum Context {
+    A(i32),
+    B(i32),
+}
+impl Context {
+    pub fn test(x: Option<i32>) -> Option<Context> {
+        x.map(Self::B)
+    }
+}