Bump rustc version

engine/backends/coq/dune

@@ -22,4 +22,4 @@
 (env
  (_
   (flags
-   (:standard -w +A))))
+   (:standard -w +A-4-40-42-44))))

engine/bin/dune

@@ -37,4 +37,4 @@
 (env
  (_
   (flags
-   (:standard -g -warn-error -A -warn-error +8))))
+   (:standard -g -warn-error -A -warn-error +8 -w -33))))

engine/bin/lib.ml

@@ -1,5 +1,6 @@
 open Hax_engine
 open Base
+open Stdio
 
 let read_options_from_stdin (yojson_from_string : string -> Yojson.Safe.t) :
     Types.engine_options =

engine/lib/import_thir.ml

@@ -80,7 +80,6 @@ let c_mutability (witness : 'a) : bool -> 'a Ast.mutability = function
 let c_borrow_kind span : Thir.borrow_kind -> borrow_kind = function
   | Shared -> Shared
   | Shallow -> unimplemented [ span ] "Shallow borrows"
-  | Unique -> Unique
   | Mut _ -> Mut W.mutable_reference
 
 let c_binding_mode span : Thir.binding_mode -> binding_mode = function

frontend/exporter/src/rustc_utils.rs

@@ -16,7 +16,7 @@ impl<'tcx, T: ty::TypeFoldable<ty::TyCtxt<'tcx>>> ty::Binder<'tcx, T> {
 impl<'tcx> ty::Binder<'tcx, ty::PredicateKind<'tcx>> {
     fn as_poly_trait_predicate(self) -> Option<ty::PolyTraitPredicate<'tcx>> {
         self.try_map_bound(|kind| match kind {
-            ty::PredicateKind::Clause(ty::Clause::Trait(trait_pred)) => Ok(trait_pred),
+            ty::PredicateKind::Clause(ty::ClauseKind::Trait(trait_pred)) => Ok(trait_pred),
             _ => Err(()),
         })
         .ok()
@@ -26,6 +26,7 @@ impl<'tcx> ty::Binder<'tcx, ty::PredicateKind<'tcx>> {
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct AnnotatedPredicate<'tcx> {
     pub is_extra_self_predicate: bool,
+    /// Note: they are all actually `Clause`s.
     pub predicate: ty::Predicate<'tcx>,
     pub span: rustc_span::Span,
 }
@@ -59,31 +60,31 @@ impl<'tcx> ty::TyCtxt<'tcx> {
         let with_self = self.predicates_of(did);
         let parent = with_self.parent;
         let with_self = {
-            let extra_predicates = if rustc_hir::def::DefKind::OpaqueTy == self.def_kind(did) {
-                // An opaque type (e.g. `impl Trait`) provides
-                // predicates by itself: we need to account for them.
-                self.explicit_item_bounds(did)
-                    .skip_binder()
-                    .iter()
-                    .collect()
-            } else {
-                vec![]
-            }
-            .into_iter()
-            .cloned();
-            with_self.predicates.iter().cloned().chain(extra_predicates)
+            let extra_predicates: Vec<(ty::Clause<'_>, rustc_span::Span)> =
+                if rustc_hir::def::DefKind::OpaqueTy == self.def_kind(did) {
+                    // An opaque type (e.g. `impl Trait`) provides
+                    // predicates by itself: we need to account for them.
+                    self.explicit_item_bounds(did)
+                        .skip_binder()
+                        .iter()
+                        .copied()
+                        .collect()
+                } else {
+                    vec![]
+                };
+            with_self.predicates.iter().copied().chain(extra_predicates)
         };
-        let without_self: Vec<ty::Predicate> = self
+        let without_self: Vec<ty::Clause<'_>> = self
             .predicates_defined_on(did)
             .predicates
-            .into_iter()
-            .cloned()
-            .map(|(pred, _)| pred)
+            .iter()
+            .copied()
+            .map(|(clause, _)| clause)
             .collect();
         (
-            with_self.map(move |(predicate, span)| AnnotatedPredicate {
-                is_extra_self_predicate: !without_self.contains(&predicate),
-                predicate,
+            with_self.map(move |(clause, span)| AnnotatedPredicate {
+                is_extra_self_predicate: !without_self.contains(&clause),
+                predicate: clause.as_predicate(),
                 span,
             }),
             parent,

frontend/exporter/src/state.rs

@@ -250,7 +250,7 @@ impl ImplInfos {
             .predicates_defined_on(did)
             .predicates
             .iter()
-            .map(|(x, _)| x.sinto(s))
+            .map(|(clause, _)| clause.as_predicate().sinto(s))
             .collect();
         Self {
             generics: tcx.generics_of(did).sinto(s),

frontend/exporter/src/traits.rs

@@ -178,10 +178,10 @@ mod search_clause {
                 .filter(|item| item.kind == AssocKind::Type)
                 .copied()
                 .map(|item| {
-                    let bounds = tcx.item_bounds(item.def_id).map_bound(|predicates| {
+                    let bounds = tcx.item_bounds(item.def_id).map_bound(|clauses| {
                         predicates_to_poly_trait_predicates(
                             tcx,
-                            predicates.into_iter(),
+                            clauses.into_iter().map(|clause| clause.as_predicate()),
                             self.skip_binder().trait_ref.substs,
                         )
                         .enumerate()
@@ -397,13 +397,14 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
     }
 }
 
-/// Given a predicate `pred` in the context of some impl. block
-/// `impl_did`, susbts correctly `Self` from `pred` and (1) derive a
+/// Given a clause `clause` in the context of some impl. block
+/// `impl_did`, susbts correctly `Self` from `clause` and (1) derive a
 /// `Clause` and (2) resolve an `ImplExpr`.
-pub fn super_predicate_to_clauses_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
+pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
     impl_did: rustc_span::def_id::DefId,
-    (pred, span): &(rustc_middle::ty::Predicate<'tcx>, rustc_span::Span),
+    clause: rustc_middle::ty::Clause<'tcx>,
+    span: rustc_span::Span,
 ) -> Option<(Clause, ImplExpr, Span)> {
     let tcx = s.base().tcx;
     let impl_trait_ref = tcx
@@ -412,56 +413,54 @@ pub fn super_predicate_to_clauses_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
     let original_clause_id = {
         // We don't want the id of the substituted clause id, but the
         // original clause id (with, i.e., `Self`)
-        let rustc_middle::ty::PredicateKind::Clause(clause) = pred.kind().skip_binder() else {
-            None?
-        };
         let s = &with_owner_id(s.base(), (), (), impl_trait_ref.def_id());
-        use rustc_middle::ty::ToPredicate;
-        clause_id_of_predicate(s, clause.clone().to_predicate(s.base().tcx))
-    };
-    let pred = pred.subst_supertrait(tcx, &impl_trait_ref);
-    // TODO: use `let clause = pred.as_clause()?;` when upgrading rustc
-    let rustc_middle::ty::PredicateKind::Clause(clause) = pred.kind().skip_binder() else {
-        None?
+        // We compute the id of the clause without binder.
+        let clause: Clause = clause.kind().skip_binder().sinto(s);
+        clause.id
     };
-    let impl_expr = pred
+    let new_clause = clause.subst_supertrait(tcx, &impl_trait_ref);
+    let impl_expr = new_clause
+        .as_predicate()
         .to_opt_poly_trait_pred()?
         .impl_expr(s, get_param_env(s));
-    let mut clause: Clause = clause.sinto(s);
-    clause.id = original_clause_id;
-    Some((clause, impl_expr, span.sinto(s)))
+    // Build the new clause, again without binder.
+    let mut new_clause_no_binder: Clause = new_clause.kind().skip_binder().sinto(s);
+    new_clause_no_binder.id = original_clause_id;
+    Some((new_clause_no_binder, impl_expr, span.sinto(s)))
+}
+
+fn deterministic_hash<T: std::hash::Hash>(x: &T) -> u64 {
+    use crate::deterministic_hash::DeterministicHasher;
+    use std::collections::hash_map::DefaultHasher;
+    use std::hash::Hasher;
+    let mut hasher = DeterministicHasher::new(DefaultHasher::new());
+    x.hash(&mut hasher);
+    hasher.finish()
 }
 
 /// Crafts a unique identifier for a predicate by hashing it. The hash
 /// is non-trivial because we need stable identifiers: two hax
 /// extraction of a same predicate should result in the same
 /// identifier. Rustc's stable hash is not doing what we want here: it
 /// is sensible to the environment. Instead, we convert the (rustc)
-/// predicate to `crate::Predicate` and hash from there, taking care
-/// of not translating directly the `Clause` case, which otherwise
-/// would call `clause_id_of_predicate` as well.
+/// predicate to `crate::Predicate` and hash from there.
 #[tracing::instrument(level = "trace", skip(s))]
 pub fn clause_id_of_predicate<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
     predicate: rustc_middle::ty::Predicate<'tcx>,
 ) -> u64 {
-    use crate::deterministic_hash::DeterministicHasher;
-    use std::collections::hash_map::DefaultHasher;
-    use std::hash::{Hash, Hasher};
-    let mut hasher = DeterministicHasher::new(DefaultHasher::new());
-
-    let binder = predicate.kind();
-    if let rustc_middle::ty::PredicateKind::Clause(ck) = binder.skip_binder() {
-        let bvs: Vec<BoundVariableKind> = binder.bound_vars().sinto(s);
-        let ck: ClauseKind = ck.sinto(s);
-        hasher.write_u8(0);
-        bvs.hash(&mut hasher);
-        ck.hash(&mut hasher);
-    } else {
-        hasher.write_u8(1);
-        predicate.sinto(s).hash(&mut hasher);
+    let predicate = predicate.sinto(s);
+    match &predicate.value {
+        // Instead of recursively hashing the clause, we reuse the already-computed id.
+        PredicateKind::Clause(clause) => clause.id,
+        _ => deterministic_hash(&(1u8, predicate)),
     }
-    hasher.finish()
+}
+
+/// Used when building a `crate::Clause`. See [`clause_id_of_predicate`] for what we're doing here.
+#[tracing::instrument(level = "trace")]
+pub fn clause_id_of_bound_clause_kind(binder: &Binder<ClauseKind>) -> u64 {
+    deterministic_hash(&(0u8, binder))
 }
 
 #[tracing::instrument(level = "trace", skip(s))]

frontend/exporter/src/types/copied.rs

@@ -1,5 +1,6 @@
 use crate::prelude::*;
 use crate::rustc_middle::query::Key;
+use rustc_middle::ty;
 
 /// Reflects [`rustc_hir::definitions::DisambiguatedDefPathData`]
 #[derive(
@@ -1960,8 +1961,19 @@ pub enum PointerCast {
 pub enum BorrowKind {
     Shared,
     Shallow,
-    Unique,
-    Mut { allow_two_phase_borrow: bool },
+    Mut { kind: MutBorrowKind },
+}
+
+/// Reflects [`rustc_middle::mir::MutBorrowKind`]
+#[derive(AdtInto)]
+#[args(<S>, from: rustc_middle::mir::MutBorrowKind, state: S as _s)]
+#[derive(
+    Copy, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub enum MutBorrowKind {
+    Default,
+    TwoPhaseBorrow,
+    ClosureCapture,
 }
 
 /// Reflects [`rustc_ast::ast::StrStyle`]
@@ -2709,8 +2721,9 @@ pub enum ImplItemKind<Body: IsBody> {
             let impl_did = assoc_item.impl_container(tcx).unwrap();
             tcx.explicit_item_bounds(assoc_item.trait_item_def_id.unwrap())
                 .skip_binder()
-                .into_iter()
-                .flat_map(|x| super_predicate_to_clauses_and_impl_expr(s, impl_did, x))
+                .iter()
+                .copied()
+                .filter_map(|(clause, span)| super_clause_to_clause_and_impl_expr(s, impl_did, clause, span))
                 .collect::<Vec<_>>()
         };
         ImplItemKind::Type {
@@ -2770,8 +2783,9 @@ pub struct Impl<Body: IsBody> {
         if let Some(trait_did) = trait_did {
             tcx.super_predicates_of(trait_did)
                 .predicates
-                .into_iter()
-                .flat_map(|x| super_predicate_to_clauses_and_impl_expr(s, owner_id, x))
+                .iter()
+                .copied()
+                .filter_map(|(clause, span)| super_clause_to_clause_and_impl_expr(s, owner_id, clause, span))
                 .collect::<Vec<_>>()
         } else {
             vec![]
@@ -3244,9 +3258,9 @@ impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto<S, ProjectionPredicate>
     }
 }
 
-/// Reflects [`rustc_middle::ty::Clause`]
+/// Reflects [`rustc_middle::ty::ClauseKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::Clause<'tcx>, state: S as tcx)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::ClauseKind<'tcx>, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -3258,9 +3272,10 @@ pub enum ClauseKind {
     ConstArgHasType(ConstantExpr, Ty),
     WellFormed(GenericArg),
     ConstEvaluatable(ConstantExpr),
+    TypeWellFormedFromEnv(Ty),
 }
 
-/// Reflects [`rustc_middle::ty::Clause`]
+/// Reflects [`rustc_middle::ty::ClauseKind`] and adds a hash-consed clause identifier.
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -3269,16 +3284,29 @@ pub struct Clause {
     pub id: u64,
 }
 
-impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for rustc_middle::ty::Clause<'tcx> {
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause>
+    for rustc_middle::ty::Binder<'tcx, rustc_middle::ty::ClauseKind<'tcx>>
+{
     fn sinto(&self, s: &S) -> Clause {
-        use rustc_middle::ty::ToPredicate;
+        // FIXME: `ClauseKind::sinto` uses a dummy binder. We need it because `Predicate::sinto()`
+        // doesn't propagate the binder to the `ClauseKind`. This might cause inconsistencies. It
+        // might be that we don't want to hash the binder at all.
+        let binder: Binder<ClauseKind> = self.sinto(s);
+        let id = clause_id_of_bound_clause_kind(&binder);
         Clause {
-            id: clause_id_of_predicate(s, self.clone().to_predicate(s.base().tcx)),
-            kind: self.sinto(s),
+            kind: binder.value,
+            id,
         }
     }
 }
 
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for rustc_middle::ty::ClauseKind<'tcx> {
+    fn sinto(&self, s: &S) -> Clause {
+        // FIXME: this is dangerous.
+        rustc_middle::ty::Binder::dummy(self.clone()).sinto(s)
+    }
+}
+
 /// Reflects [`rustc_middle::ty::BoundVariableKind`]
 #[derive(AdtInto)]
 #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::BoundVariableKind, state: S as tcx)]
@@ -3302,12 +3330,14 @@ pub struct Binder<T> {
 
 /// Reflects [`rustc_middle::ty::GenericPredicates`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::GenericPredicates<'tcx>, state: S as tcx)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::GenericPredicates<'tcx>, state: S as s)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
 pub struct GenericPredicates {
     pub parent: Option<DefId>,
+    // FIXME: Switch from `Predicate` to `Clause` (will require correct handling of binders).
+    #[value(self.predicates.iter().map(|(clause, span)| (clause.as_predicate().sinto(s), span.sinto(s))).collect())]
     pub predicates: Vec<(Predicate, Span)>,
 }
 
@@ -3391,7 +3421,6 @@ pub enum PredicateKind {
     Subtype(SubtypePredicate),
     Coerce(CoercePredicate),
     ConstEquate(ConstantExpr, ConstantExpr),
-    TypeWellFormedFromEnv(Ty),
     Ambiguous,
     AliasRelate(Term, Term, AliasRelationDirection),
 }
@@ -3425,20 +3454,25 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene
         }
     };
 
-    let predicates: Vec<_> = if use_item_bounds {
-        let list = tcx.item_bounds(s.owner_id()).subst_identity();
-        let span = list.default_span(tcx);
-        list.into_iter().map(|x| (x, span)).collect()
+    let clauses: Vec<ty::Clause<'tcx>> = if use_item_bounds {
+        tcx.item_bounds(s.owner_id())
+            .subst_identity()
+            .iter()
+            .collect()
     } else {
         tcx.predicates_defined_on(s.owner_id())
             .predicates
-            .into_iter()
-            .cloned()
+            .iter()
+            .map(|(x, _span)| x)
+            .copied()
             .collect()
     };
-    predicates
+    clauses
         .iter()
-        .map(|(pred, _span)| tcx.erase_late_bound_regions(pred.clone().kind()).sinto(s))
+        .map(|clause| {
+            tcx.erase_late_bound_regions(clause.as_predicate().kind())
+                .sinto(s)
+        })
         .collect()
 }