Add basic support for RPIT

creusot/src/backend/clone_map.rs

@@ -94,7 +94,8 @@ pub(crate) trait Namer<'tcx> {
             }
             DefKind::AssocTy => Ty::new_projection(self.tcx(), def_id, subst),
             DefKind::Closure => Ty::new_closure(self.tcx(), def_id, subst),
-            _ => unreachable!(),
+            DefKind::OpaqueTy => Ty::new_opaque(self.tcx(), def_id, subst),
+            k => unreachable!("{k:?}"),
         };
 
         self.insert(Dependency::Type(ty)).qname()
@@ -143,11 +144,7 @@ pub(crate) trait Namer<'tcx> {
         self.insert(Dependency::Promoted(def_id, prom)).qname()
     }
 
-    fn normalize<T: TypeFoldable<TyCtxt<'tcx>> + Copy>(
-        &self,
-        ctx: &TranslationCtx<'tcx>,
-        ty: T,
-    ) -> T;
+    fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, ctx: &TranslationCtx<'tcx>, ty: T) -> T;
 
     fn import_prelude_module(&mut self, module: PreludeModule) {
         self.insert(Dependency::Builtin(module));
@@ -162,11 +159,7 @@ pub(crate) trait Namer<'tcx> {
 
 impl<'tcx> Namer<'tcx> for CloneNames<'tcx> {
     // TODO: get rid of this. It feels like it should be unnecessary
-    fn normalize<T: TypeFoldable<TyCtxt<'tcx>> + Copy>(
-        &self,
-        _: &TranslationCtx<'tcx>,
-        ty: T,
-    ) -> T {
+    fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, _: &TranslationCtx<'tcx>, ty: T) -> T {
         self.tcx().normalize_erasing_regions(self.typing_env, ty)
     }
 
@@ -191,11 +184,7 @@ impl<'tcx> Namer<'tcx> for CloneNames<'tcx> {
 }
 
 impl<'tcx> Namer<'tcx> for Dependencies<'tcx> {
-    fn normalize<T: TypeFoldable<TyCtxt<'tcx>> + Copy>(
-        &self,
-        ctx: &TranslationCtx<'tcx>,
-        ty: T,
-    ) -> T {
+    fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, ctx: &TranslationCtx<'tcx>, ty: T) -> T {
         self.tcx().normalize_erasing_regions(ctx.typing_env(self.self_id), ty)
     }
 

creusot/src/backend/clone_map/elaborator.rs

@@ -63,11 +63,7 @@ struct ExpansionProxy<'a, 'tcx> {
 }
 
 impl<'a, 'tcx> Namer<'tcx> for ExpansionProxy<'a, 'tcx> {
-    fn normalize<T: TypeFoldable<TyCtxt<'tcx>> + Copy>(
-        &self,
-        ctx: &TranslationCtx<'tcx>,
-        ty: T,
-    ) -> T {
+    fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, ctx: &TranslationCtx<'tcx>, ty: T) -> T {
         self.namer.normalize(ctx, ty)
     }
 
@@ -238,6 +234,8 @@ fn expand_ty_inv_axiom<'tcx>(
 
 struct TyElab;
 
+use rustc_middle::ty::AliasTyKind;
+
 impl DepElab for TyElab {
     fn expand<'tcx>(
         elab: &mut Expander<'_, 'tcx>,
@@ -252,6 +250,13 @@ impl DepElab for TyElab {
                 ty_name: names.ty_param(ty).as_ident(),
                 ty_params: vec![],
             })],
+            TyKind::Alias(AliasTyKind::Opaque, _) => {
+                let (def_id, subst) = dep.did().unwrap();
+                vec![Decl::TyDecl(TyDecl::Opaque {
+                    ty_name: names.ty(def_id, subst).as_ident(),
+                    ty_params: vec![],
+                })]
+            }
             TyKind::Alias(_, _) => {
                 let (def_id, subst) = dep.did().unwrap();
                 assert_eq!(

creusot/src/backend/dependency.rs

@@ -40,6 +40,7 @@ impl<'tcx> Dependency<'tcx> {
                 TyKind::Adt(def, substs) => Some((def.did(), substs)),
                 TyKind::Closure(id, substs) => Some((*id, substs)),
                 TyKind::Alias(AliasTyKind::Projection, aty) => Some((aty.def_id, aty.args)),
+                TyKind::Alias(AliasTyKind::Opaque, aty) => Some((aty.def_id, aty.args)),
                 _ => None,
             },
             _ => None,
@@ -57,9 +58,13 @@ impl<'tcx> Dependency<'tcx> {
                 TyKind::Adt(def, _) if !def.is_box() => {
                     Some(item_symb(tcx, def.did(), rustc_hir::def::Namespace::TypeNS))
                 }
-                TyKind::Alias(_, aty) => {
-                    Some(Symbol::intern(&type_name(tcx.item_name(aty.def_id).as_str())))
-                }
+                TyKind::Alias(AliasTyKind::Opaque, aty) => Some(Symbol::intern(&format!(
+                    "opaque{}",
+                    tcx.def_path(aty.def_id).data.last().unwrap().disambiguator
+                ))),
+                TyKind::Alias(_, aty) => Some(Symbol::intern(&type_name(
+                    tcx.opt_item_name(aty.def_id).unwrap_or(Symbol::intern("synthetic")).as_str(),
+                ))),
                 TyKind::Closure(def_id, _) => Some(Symbol::intern(&format!(
                     "closure{}",
                     tcx.def_path(*def_id).data.last().unwrap().disambiguator

creusot/src/backend/signature.rs

@@ -78,7 +78,10 @@ fn lower_condition<'tcx, N: Namer<'tcx>>(
     names: &mut N,
     cond: Condition<'tcx>,
 ) -> why3::declaration::Condition {
-    why3::declaration::Condition { exp: lower_pure(ctx, names, &cond.term), expl: cond.expl }
+    why3::declaration::Condition {
+        exp: lower_pure(ctx, names, &names.normalize(ctx, cond.term)),
+        expl: cond.expl,
+    }
 }
 
 fn contract_to_why3<'tcx, N: Namer<'tcx>>(

creusot/src/backend/ty.rs

@@ -63,6 +63,10 @@ pub(crate) fn translate_ty<'tcx, N: Namer<'tcx>>(
         }
         Param(_) => MlT::TConstructor(names.ty_param(ty)),
         Alias(AliasTyKind::Projection, pty) => translate_projection_ty(ctx, names, pty),
+        Alias(AliasTyKind::Opaque, AliasTy { args, def_id, .. }) => {
+            let name = names.ty(*def_id, args);
+            MlT::TConstructor(name)
+        }
         Ref(_, ty, borkind) => {
             use rustc_ast::Mutability::*;
             names.import_prelude_module(PreludeModule::Borrow);

creusot/src/backend/ty_inv.rs

@@ -101,8 +101,6 @@ impl<'a, 'tcx> InvariantElaborator<'a, 'tcx> {
 
         let mut use_imples = false;
 
-        matches!(ty.kind(), TyKind::Alias(..) | TyKind::Param(_));
-
         let mut rhs = Term::mk_true(self.ctx.tcx);
 
         match resolve_user_inv(self.ctx.tcx, ty, self.typing_env) {

creusot/src/ctx.rs

@@ -444,7 +444,12 @@ impl<'tcx> TranslationCtx<'tcx> {
     pub(crate) fn typing_env(&self, def_id: DefId) -> TypingEnv<'tcx> {
         // FIXME: is it correct to pretend we are doing a non-body analysis?
         let param_env = self.param_env(def_id);
-        TypingEnv { typing_mode: TypingMode::non_body_analysis(), param_env }
+        let mode = if self.is_mir_available(def_id) && def_id.is_local() {
+            TypingMode::post_borrowck_analysis(self.tcx, def_id.as_local().unwrap())
+        } else {
+            TypingMode::non_body_analysis()
+        };
+        TypingEnv { typing_mode: mode, param_env }
     }
 
     pub(crate) fn has_body(&mut self, def_id: DefId) -> bool {

creusot/src/translation/function/terminator.rs

@@ -84,7 +84,9 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             }
             Unreachable => term = Terminator::Abort(terminator.source_info.span),
             Call { func, args, destination, mut target, fn_span, .. } => {
-                let (fun_def_id, subst) = func_defid(func).expect("expected call with function");
+                let Some((fun_def_id, subst)) = func_defid(func) else {
+                    self.ctx.fatal_error(*fn_span, "unsupported function call type").emit()
+                };
                 if let Some((need, resolved)) = resolved_during.take() {
                     self.resolve_before_assignment(need, &resolved, location, *destination)
                 }
@@ -436,7 +438,7 @@ fn resolve_function<'tcx>(
 
 // Try to extract a function defid from an operand
 fn func_defid<'tcx>(op: &Operand<'tcx>) -> Option<(DefId, GenericArgsRef<'tcx>)> {
-    let fun_ty = op.constant().unwrap().const_.ty();
+    let fun_ty = op.constant()?.const_.ty();
     if let ty::TyKind::FnDef(def_id, subst) = fun_ty.kind() {
         Some((*def_id, subst))
     } else {

creusot/tests/should_succeed/syntax/15_impl_trait.rs

@@ -0,0 +1,24 @@
+extern crate creusot_contracts;
+
+use creusot_contracts::*;
+
+pub trait MyTrait {
+    fn a(&self) -> bool;
+}
+
+impl MyTrait for () {
+    fn a(&self) -> bool {
+        true
+    }
+}
+
+pub fn returns_iterator() -> impl MyTrait {
+    ()
+}
+
+#[ensures(true)]
+pub fn main() {
+    let x = returns_iterator().a();
+
+    proof_assert!(x);
+}