Merge pull request #1559 from Nadrieril/upstream-pr

Merge frontend improvements

Author: W95Psp

CHANGELOG.md

@@ -15,6 +15,17 @@ Changes to the Rust Engine:
    expressions, pattern-matching) (#1623)
  - Update name rendering infrastructure in the Lean backend (#1623, #1624)
 
+Changes to the frontend:
+- Add an explicit `Self: Trait` clause to trait methods and consts (#1559)
+- Fix `ImplExpr::Builtin` that had some type errors (#1559)
+- Improve the translation of `Drop` information (#1559)
+- Add variance information to type parameters (#1559)
+- Cleanup the `State` infrastructure a little bit (#1559)
+- Add information about the metadata to use in unsize coercions (#1559)
+- Resolve `dyn Trait` predicates (#1559)
+- Many improvements to `FullDef` (#1559)
+- Add infrastructure to get a monomorphized `FullDef`; this is used in charon to monomorphize a crate graph (#1559)
+
 Miscellaneous:
  - A lean tutorial has been added to the hax website.
 

engine/backends/fstar/fstar_backend.ml

@@ -2003,6 +2003,42 @@ let unsize_as_identity =
   in
   visitor#visit_item ()
 
+(** Rewrites, in trait, local bounds refereing to `Self` into the impl expr of
+    kind `Self`. *)
+let local_self_bound_as_self (i : AST.item) : AST.item =
+  match i.v with
+  | Trait { name; generics; _ } ->
+      let generic_eq (param : generic_param) (value : generic_value) =
+        (let* id =
+           match (param.kind, value) with
+           | GPConst _, GConst { e = LocalVar id } -> Some id
+           | GPType, GType (TParam id) -> Some id
+           | GPLifetime _, GLifetime _ -> Some param.ident
+           | _ -> None
+         in
+         Some ([%eq: local_ident] id param.ident))
+        |> Option.value ~default:false
+      in
+      let generics_eq params values =
+        match List.for_all2 ~f:generic_eq params values with
+        | List.Or_unequal_lengths.Ok v -> v
+        | List.Or_unequal_lengths.Unequal_lengths -> false
+      in
+      (object
+         inherit [_] U.Visitors.map as super
+
+         method! visit_impl_expr () ie =
+           match ie with
+           | { kind = LocalBound _; goal = { args; trait } }
+             when [%eq: concrete_ident] trait name
+                  && generics_eq generics.params args ->
+               { ie with kind = Self }
+           | _ -> ie
+      end)
+        #visit_item
+        () i
+  | _ -> i
+
 let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) :
     AST.item list =
   let items =
@@ -2022,6 +2058,7 @@ let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) :
     TransformToInputLanguage.ditems items
     |> List.map ~f:unsize_as_identity
     |> List.map ~f:unsize_as_identity
+    |> List.map ~f:local_self_bound_as_self
     |> List.map ~f:U.Mappers.add_typ_ascription
   in
   items

engine/lib/import_thir.ml

@@ -547,7 +547,8 @@ end) : EXPR = struct
               {
                 item =
                   {
-                    value = { def_id = id; generic_args; impl_exprs; in_trait };
+                    value =
+                      { def_id = id; generic_args; impl_exprs; in_trait; _ };
                     _;
                   };
                 _;
@@ -1025,7 +1026,7 @@ end) : EXPR = struct
     | ClosureFnPointer Safe | ReifyFnPointer ->
         (* we have arrow types, we do not distinguish between top-level functions and closures *)
         (c_expr source).e
-    | Unsize ->
+    | Unsize _ ->
         (* https://doc.rust-lang.org/std/marker/trait.Unsize.html *)
         (U.call Rust_primitives__unsize [ c_expr source ] span typ).e
         (* let source = c_expr source in *)
@@ -1114,21 +1115,25 @@ end) : EXPR = struct
     | Error ->
         assertion_failure [ span ]
           "got type `Error`: Rust compilation probably failed."
-    | Dynamic (predicates, _region, Dyn) -> (
+    | Dynamic (_, predicates, _region) -> (
         let goals, non_traits =
           List.partition_map
-            ~f:(fun pred ->
-              match pred.value with
-              | Trait { args; def_id } ->
+            ~f:(fun ((clause, _span) : Types.clause * _) ->
+              match clause.kind.value with
+              | Trait { trait_ref; _ } ->
                   let goal : dyn_trait_goal =
                     {
-                      trait = Concrete_ident.of_def_id ~value:false def_id;
-                      non_self_args = List.map ~f:(c_generic_value span) args;
+                      trait =
+                        Concrete_ident.of_def_id ~value:false
+                          trait_ref.value.def_id;
+                      non_self_args =
+                        List.map ~f:(c_generic_value span)
+                          (List.tl_exn trait_ref.value.generic_args);
                     }
                   in
                   First goal
               | _ -> Second ())
-            predicates
+            predicates.predicates
         in
         match non_traits with
         | [] -> TDyn { witness = W.dyn; goals }
@@ -1150,7 +1155,7 @@ end) : EXPR = struct
 
   and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr =
     let goal = c_trait_ref span ie.trait.value in
-    let impl = { kind = c_impl_expr_atom span ie.impl; goal } in
+    let impl = { kind = c_impl_expr_atom span ie.impl goal; goal } in
     match ie.impl with
     | Concrete { value = { impl_exprs = []; _ }; _ } -> impl
     | Concrete { value = { impl_exprs; _ }; _ } ->
@@ -1163,7 +1168,7 @@ end) : EXPR = struct
     let args = List.map ~f:(c_generic_value span) tr.value.generic_args in
     { trait; args }
 
-  and c_impl_expr_atom (span : Thir.span) (ie : Thir.impl_expr_atom) :
+  and c_impl_expr_atom (span : Thir.span) (ie : Thir.impl_expr_atom) goal :
       impl_expr_kind =
     let browse_path (item_kind : impl_expr_kind)
         (chunk : Thir.impl_expr_path_chunk) =
@@ -1196,8 +1201,7 @@ end) : EXPR = struct
         List.fold ~init ~f:browse_path path
     | Dyn -> Dyn
     | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
-    | Builtin { trait; _ } -> Builtin (c_trait_ref span trait.value)
-    | Drop _ -> failwith @@ "impl_expr_atom: Drop"
+    | Builtin _ -> Builtin goal
     | Error str -> failwith @@ "impl_expr_atom: Error " ^ str
 
   and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value

frontend/exporter/src/body.rs

@@ -13,6 +13,7 @@ mod module {
         def_id::{DefId as RDefId, LocalDefId as RLocalDefId},
         hir_id::OwnerId as ROwnerId,
     };
+    use rustc_middle::ty;
 
     mod store {
         //! This module helps at store bodies to avoid stealing.
@@ -97,7 +98,7 @@ mod module {
     }
     pub use store::*;
 
-    pub fn get_thir<'tcx, S: UnderOwnerState<'tcx>>(
+    pub fn get_thir<'tcx, S: BaseState<'tcx>>(
         did: RLocalDefId,
         s: &S,
     ) -> (
@@ -122,7 +123,11 @@ mod module {
     }
 
     pub trait IsBody: Sized + std::fmt::Debug + Clone + 'static {
-        fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RDefId, s: &S) -> Option<Self>;
+        fn body<'tcx, S: UnderOwnerState<'tcx>>(
+            s: &S,
+            did: RDefId,
+            instantiate: Option<ty::GenericArgsRef<'tcx>>,
+        ) -> Option<Self>;
 
         /// Reuse a MIR body we already got. Panic if that's impossible.
         fn from_mir<'tcx, S: UnderOwnerState<'tcx>>(
@@ -133,7 +138,7 @@ mod module {
         }
     }
 
-    pub fn make_fn_def<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>(
+    pub fn make_fn_def<'tcx, Body: IsBody, S: BaseState<'tcx>>(
         fn_sig: &rustc_hir::FnSig,
         body_id: &rustc_hir::BodyId,
         s: &S,
@@ -142,11 +147,11 @@ mod module {
         let ldid = hir_id.owner.def_id;
 
         let (thir, expr_entrypoint) = get_thir(ldid, s);
-        let s = &with_owner_id(s.base(), thir.clone(), (), ldid.to_def_id());
+        let s = &s.with_owner_id(ldid.to_def_id()).with_thir(thir.clone());
         FnDef {
             params: thir.params.raw.sinto(s),
             ret: thir.exprs[expr_entrypoint].ty.sinto(s),
-            body: Body::body(ldid.to_def_id(), s).s_unwrap(s),
+            body: Body::body(s, ldid.to_def_id(), None).s_unwrap(s),
             sig_span: fn_sig.span.sinto(s),
             header: fn_sig.header.sinto(s),
         }
@@ -161,13 +166,17 @@ mod module {
         // 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).to_def_id(), s).s_unwrap(s)
+        Body::body(s, s.base().tcx.hir_body_owner_def_id(id).to_def_id(), None).s_unwrap(s)
     }
 
     mod implementations {
         use super::*;
         impl IsBody for () {
-            fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RDefId, _s: &S) -> Option<Self> {
+            fn body<'tcx, S: UnderOwnerState<'tcx>>(
+                _s: &S,
+                _did: RDefId,
+                _instantiate: Option<ty::GenericArgsRef<'tcx>>,
+            ) -> Option<Self> {
                 Some(())
             }
             fn from_mir<'tcx, S: UnderOwnerState<'tcx>>(
@@ -178,9 +187,15 @@ mod module {
             }
         }
         impl IsBody for ThirBody {
-            fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RDefId, s: &S) -> Option<Self> {
+            fn body<'tcx, S: BaseState<'tcx>>(
+                s: &S,
+                did: RDefId,
+                instantiate: Option<ty::GenericArgsRef<'tcx>>,
+            ) -> Option<Self> {
                 let did = did.as_local()?;
                 let (thir, expr) = get_thir(did, s);
+                assert!(instantiate.is_none(), "monomorphized thir isn't supported");
+                let s = &s.with_owner_id(did.to_def_id());
                 Some(if *CORE_EXTRACTION_MODE {
                     let expr = &thir.exprs[expr];
                     Decorated {
@@ -191,36 +206,41 @@ mod module {
                         span: expr.span.sinto(s),
                     }
                 } else {
-                    expr.sinto(&with_owner_id(s.base(), thir, (), did.to_def_id()))
+                    expr.sinto(&s.with_thir(thir))
                 })
             }
         }
 
         impl<A: IsBody, B: IsBody> IsBody for (A, B) {
-            fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RDefId, s: &S) -> Option<Self> {
-                Some((A::body(did, s)?, B::body(did, s)?))
+            fn body<'tcx, S: UnderOwnerState<'tcx>>(
+                s: &S,
+                did: RDefId,
+                instantiate: Option<ty::GenericArgsRef<'tcx>>,
+            ) -> Option<Self> {
+                Some((A::body(s, did, instantiate)?, B::body(s, did, instantiate)?))
             }
         }
 
         impl<MirKind: IsMirKind + Clone + 'static> IsBody for MirBody<MirKind> {
-            fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RDefId, s: &S) -> Option<Self> {
-                MirKind::get_mir(s.base().tcx, did, |body| {
-                    let body = Rc::new(body.clone());
-                    body.sinto(&with_owner_id(s.base(), (), body.clone(), did))
+            fn body<'tcx, S: UnderOwnerState<'tcx>>(
+                s: &S,
+                did: RDefId,
+                instantiate: Option<ty::GenericArgsRef<'tcx>>,
+            ) -> Option<Self> {
+                let tcx = s.base().tcx;
+                let typing_env = s.typing_env();
+                MirKind::get_mir(tcx, did, |body| {
+                    let body = substitute(tcx, typing_env, instantiate, body.clone());
+                    let body = Rc::new(body);
+                    body.sinto(&s.with_mir(body.clone()))
                 })
             }
             fn from_mir<'tcx, S: UnderOwnerState<'tcx>>(
                 s: &S,
                 body: rustc_middle::mir::Body<'tcx>,
             ) -> Option<Self> {
                 let body = Rc::new(body.clone());
-                let s = &State {
-                    base: s.base(),
-                    owner_id: s.owner_id(),
-                    mir: body.clone(),
-                    binder: (),
-                    thir: (),
-                };
+                let s = &s.with_mir(body.clone());
                 Some(body.sinto(s))
             }
         }

frontend/exporter/src/id_table.rs

@@ -24,7 +24,7 @@ use std::{
 
 /// Unique IDs in a ID table.
 #[derive_group(Serializers)]
-#[derive(Default, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[derive(Default, Clone, Copy, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
 #[serde(transparent)]
 pub struct Id {
     id: u32,
@@ -88,7 +88,7 @@ impl SupportedType<Value> for ItemRefContents {
 }
 
 /// A node is a bundle of an ID with a value.
-#[derive(Deserialize, Serialize, Debug, JsonSchema, PartialEq, Eq, PartialOrd, Ord)]
+#[derive(Deserialize, Serialize, Debug, JsonSchema, PartialOrd, Ord)]
 #[serde(into = "serde_repr::NodeRepr<T>")]
 #[serde(try_from = "serde_repr::NodeRepr<T>")]
 pub struct Node<T: 'static + SupportedType<Value>> {
@@ -111,6 +111,12 @@ impl<T: SupportedType<Value> + Hash> Hash for Node<T> {
         self.value.as_ref().hash(state);
     }
 }
+impl<T: SupportedType<Value> + Eq> Eq for Node<T> {}
+impl<T: SupportedType<Value> + PartialEq> PartialEq for Node<T> {
+    fn eq(&self, other: &Self) -> bool {
+        self.value == other.value
+    }
+}
 
 /// Manual implementation of `Clone` that doesn't require a `Clone`
 /// bound on `T`.
@@ -203,6 +209,10 @@ impl<T: Sync + Send + 'static + SupportedType<Value>> Node<T> {
     pub fn inner(&self) -> &Arc<T> {
         &self.value
     }
+
+    pub fn id(&self) -> Id {
+        self.id
+    }
 }
 
 /// Wrapper for a type `T` that creates a bundle containing both a ID