Merge pull request #553 from hacspec/charon_traits_merge

Charon traits merge

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)

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

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

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<GenericArg>,
+        /// The implementation expressions for every generic bounds
+        /// ```text
+        /// fn foo<T : Bar>(...)
+        ///            ^^^
+        /// ```
+        generics_impls: Vec<ImplExpr>,
+        /// If the function is a method of trait `Foo`, `method_impl`
+        /// is an implementation of `Foo`
+        method_impl: Option<ImplExpr>,
+    },
     Todo(String),
 }
 
@@ -125,6 +150,10 @@ impl From<ConstantExpr> 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<Self> {
         Decorated {
@@ -266,6 +310,7 @@ impl ConstantExprKind {
 }
 
 pub enum TranslateUnevalRes<T> {
+    // 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<Self> {
         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))
         }
     }
 }

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

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<Base<'tcx>, (), (), ()> {
     }
 }
 
-impl<'tcx> State<Base<'tcx>, (), Rc<rustc_middle::mir::Body<'tcx>>, ()> {
+impl<'tcx> State<Base<'tcx>, (), (), rustc_hir::def_id::DefId> {
+    pub fn new_from_state_and_id<S: BaseState<'tcx>>(s: &S, id: rustc_hir::def_id::DefId) -> Self {
+        State {
+            thir: (),
+            mir: (),
+            owner_id: id,
+            base: s.base().clone(),
+        }
+    }
+}
+impl<'tcx> State<Base<'tcx>, (), Rc<rustc_middle::mir::Body<'tcx>>, 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),
         }
     }

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