Use the new trait solver.

creusot-args/src/lib.rs

@@ -11,6 +11,7 @@ pub const CREUSOT_RUSTC_ARGS: &[&str] = &[
     "-Zcrate-attr=feature(proc_macro_hygiene)",
     "-Zcrate-attr=feature(rustc_attrs)",
     "-Zcrate-attr=feature(unsized_fn_params)",
+    "-Znext-solver=globally",
     "--allow=internal_features",
     "--cfg",
     "creusot",

creusot-contracts/src/std/ops.rs

@@ -5,7 +5,9 @@ pub use ::std::ops::*;
 /// `FnOnceExt` is an extension trait for the `FnOnce` trait, used for
 /// adding a specification to closures. It should not be used directly.
 #[rustc_diagnostic_item = "fn_once_spec"]
-pub trait FnOnceExt<Args: Tuple>: FnOnce<Args> {
+pub trait FnOnceExt<Args: Tuple> {
+    type Output;
+
     #[predicate]
     fn precondition(self, a: Args) -> bool;
 
@@ -16,7 +18,7 @@ pub trait FnOnceExt<Args: Tuple>: FnOnce<Args> {
 /// `FnMutExt` is an extension trait for the `FnMut` trait, used for
 /// adding a specification to closures. It should not be used directly.
 #[rustc_diagnostic_item = "fn_mut_spec"]
-pub trait FnMutExt<Args: Tuple>: FnMut<Args> + FnOnceExt<Args> {
+pub trait FnMutExt<Args: Tuple>: FnOnceExt<Args> {
     #[predicate]
     fn postcondition_mut(&mut self, _: Args, _: Self::Output) -> bool;
 
@@ -48,7 +50,7 @@ pub trait FnMutExt<Args: Tuple>: FnMut<Args> + FnOnceExt<Args> {
 /// `FnExt` is an extension trait for the `Fn` trait, used for
 /// adding a specification to closures. It should not be used directly.
 #[rustc_diagnostic_item = "fn_spec"]
-pub trait FnExt<Args: Tuple>: Fn<Args> + FnMutExt<Args> {
+pub trait FnExt<Args: Tuple>: FnMutExt<Args> {
     #[predicate]
     fn postcondition(&self, _: Args, _: Self::Output) -> bool;
 
@@ -64,6 +66,8 @@ pub trait FnExt<Args: Tuple>: Fn<Args> + FnMutExt<Args> {
 }
 
 impl<Args: Tuple, F: FnOnce<Args>> FnOnceExt<Args> for F {
+    type Output = <Self as FnOnce<Args>>::Output;
+
     #[predicate]
     #[trusted]
     #[rustc_diagnostic_item = "fn_once_impl_precond"]
@@ -140,21 +144,19 @@ impl<Args: Tuple, F: Fn<Args>> FnExt<Args> for F {
 extern_spec! {
     mod std {
         mod ops {
-            // FIXME: we should not need the `Self :` bounds, because they are implied by the main trait bound.
-            // But if we remove them, some test fail.
-            trait FnOnce<Args> where Self : FnOnceExt<Args>, Args : Tuple {
+            trait FnOnce<Args> where Args : Tuple {
                 #[requires(self.precondition(arg))]
                 #[ensures(self.postcondition_once(arg, result))]
                 fn call_once(self, arg: Args) -> Self::Output;
             }
 
-            trait FnMut<Args> where Self : FnMutExt<Args>, Args : Tuple {
+            trait FnMut<Args> where Args : Tuple {
                 #[requires((*self).precondition(arg))]
                 #[ensures(self.postcondition_mut(arg, result))]
                 fn call_mut(&mut self, arg: Args) -> Self::Output;
             }
 
-            trait Fn<Args> where Self : FnExt<Args>, Args : Tuple {
+            trait Fn<Args> where Args : Tuple {
                 #[requires((*self).precondition(arg))]
                 #[ensures(self.postcondition(arg, result))]
                 fn call(&self, arg: Args) -> Self::Output;

creusot/src/backend/clone_map/elaborator.rs

@@ -498,8 +498,8 @@ pub fn term<'tcx>(
             } else if is_resolve_function(ctx.tcx, def_id) {
                 resolve_term(ctx, param_env, def_id, subst)
             } else if is_structural_resolve(ctx.tcx, def_id) {
-                let sig = ctx.sig(def_id).clone();
-                structural_resolve(ctx, sig.inputs[0].0, subst.type_at(0))
+                let subj = ctx.sig(def_id).inputs[0].0;
+                structural_resolve(ctx, subj, subst.type_at(0))
             } else {
                 let term = ctx.ctx.term(def_id).unwrap().clone();
                 let term = normalize(

creusot/src/backend/term.rs

@@ -203,10 +203,10 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 let mut binders = Vec::new();
                 let sig = self.ctx.sig(*id).clone();
                 let sig = EarlyBinder::bind(sig).instantiate(self.ctx.tcx, subst);
-                // FIXME: normalize sig
                 for arg in sig.inputs.iter().skip(1) {
-                    binders
-                        .push(Binder::typed(Ident::build(&arg.0.to_string()), self.lower_ty(arg.2)))
+                    let nm = Ident::build(&arg.0.to_string());
+                    let ty = self.names.normalize(self.ctx, arg.2);
+                    binders.push(Binder::typed(nm, self.lower_ty(ty)))
                 }
 
                 Exp::Abs(binders, Box::new(body))

creusot/src/ctx.rs

@@ -32,6 +32,7 @@ use rustc_hir::{
     def::DefKind,
     def_id::{DefId, LocalDefId},
 };
+use rustc_infer::traits::ObligationCause;
 use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::{
     mir::{Body, Promoted, TerminatorKind},
@@ -41,6 +42,7 @@ use rustc_middle::{
     },
 };
 use rustc_span::{Span, Symbol};
+use rustc_trait_selection::traits::normalize_param_env_or_error;
 use std::{collections::HashMap, ops::Deref};
 
 pub(crate) use crate::{backend::clone_map::*, translated_item::*};
@@ -398,15 +400,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
                 .collect::<Vec<_>>();
             let res =
                 ParamEnv::new(self.mk_clauses(&clauses), rustc_infer::traits::Reveal::UserFacing);
-            // FIXME: param envs should be normalized (this is an invariant of the trait solver),
-            // but calling this function here causes an overflow in the handling of PartialEq::eq
-            // I see two solutions:
-            //    1- Wait for the next trait solver that does not need this (I think).
-            //    2- Allow adding new generic type variables in extern specs, so that we could write
-            //             Self: DeepModel<DeepModelTy = T>,
-            //             Rhs: DeepModel<DeepModelTy = T>;
-            //
-            // let res = normalize_param_env_or_error(self.tcx, res, ObligationCause::dummy());
+            let res = normalize_param_env_or_error(self.tcx, res, ObligationCause::dummy());
             res
         } else {
             self.tcx.param_env(def_id)

creusot/src/translation/specification.rs

@@ -377,12 +377,17 @@ pub(crate) fn contract_of<'tcx>(
         let mut contract =
             extern_spec.contract.get_pre(ctx, fn_name).instantiate(ctx.tcx, extern_spec.subst);
         contract.subst(&extern_spec.arg_subst.iter().cloned().collect());
-        contract.normalize(ctx.tcx, ctx.param_env(def_id))
+        // We do NOT normalize the contract here. See below.
+        contract
     } else if let Some((parent_id, subst)) = inherited_extern_spec(ctx, def_id) {
         let spec = ctx.extern_spec(parent_id).cloned().unwrap();
         let mut contract = spec.contract.get_pre(ctx, fn_name).instantiate(ctx.tcx, subst);
         contract.subst(&spec.arg_subst.iter().cloned().collect());
-        contract.normalize(ctx.tcx, ctx.param_env(def_id))
+        // We do NOT normalize the contract here: indeed, we do not have a valid non-redundant param
+        // env for doing this. This is still valid because this contract is going to be substituted
+        // and normalized in the caller context (such extern specs are only evaluated in the context
+        // of a specific call).
+        contract
     } else {
         let subst = erased_identity_for_item(ctx.tcx, def_id);
         let mut contract = contract_clauses_of(ctx, def_id)
@@ -546,7 +551,7 @@ pub(crate) fn pre_sig_of<'tcx>(
         }
     }
 
-    PreSignature { inputs, output, contract }.normalize(ctx.tcx, param_env)
+    PreSignature { inputs, output, contract }
 }
 
 fn inputs_and_output<'tcx>(