From 497e89bd674600e598a00a0656085d35840ffbf8 Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Sat, 8 Feb 2025 12:55:39 +0100 Subject: [PATCH 1/3] Add basic support for RPIT --- creusot/src/backend/clone_map.rs | 21 ++--- creusot/src/backend/clone_map/elaborator.rs | 15 ++-- creusot/src/backend/dependency.rs | 5 ++ creusot/src/backend/signature.rs | 5 +- creusot/src/backend/ty.rs | 4 + creusot/src/backend/ty_inv.rs | 2 - creusot/src/ctx.rs | 7 +- .../src/translation/function/terminator.rs | 6 +- .../syntax/01_idents/why3session.xml | 8 ++ .../syntax/01_idents/why3shapes.gz | Bin 0 -> 45 bytes .../should_succeed/syntax/15_impl_trait.coma | 77 ++++++++++++++++++ .../should_succeed/syntax/15_impl_trait.rs | 24 ++++++ .../syntax/15_impl_trait/why3session.xml | 30 +++++++ .../syntax/15_impl_trait/why3shapes.gz | Bin 0 -> 206 bytes 14 files changed, 177 insertions(+), 27 deletions(-) create mode 100644 creusot/tests/should_succeed/syntax/01_idents/why3session.xml create mode 100644 creusot/tests/should_succeed/syntax/01_idents/why3shapes.gz create mode 100644 creusot/tests/should_succeed/syntax/15_impl_trait.coma create mode 100644 creusot/tests/should_succeed/syntax/15_impl_trait.rs create mode 100644 creusot/tests/should_succeed/syntax/15_impl_trait/why3session.xml create mode 100644 creusot/tests/should_succeed/syntax/15_impl_trait/why3shapes.gz diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs index d8e2e5b67b..f24957c54c 100644 --- a/creusot/src/backend/clone_map.rs +++ b/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> + Copy>( - &self, - ctx: &TranslationCtx<'tcx>, - ty: T, - ) -> T; + fn normalize>>(&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> + Copy>( - &self, - _: &TranslationCtx<'tcx>, - ty: T, - ) -> T { + fn normalize>>(&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> + Copy>( - &self, - ctx: &TranslationCtx<'tcx>, - ty: T, - ) -> T { + fn normalize>>(&self, ctx: &TranslationCtx<'tcx>, ty: T) -> T { self.tcx().normalize_erasing_regions(ctx.typing_env(self.self_id), ty) } diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs index 66c99a7696..4aecccfdb6 100644 --- a/creusot/src/backend/clone_map/elaborator.rs +++ b/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> + Copy>( - &self, - ctx: &TranslationCtx<'tcx>, - ty: T, - ) -> T { + fn normalize>>(&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!( diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs index c62520eaa7..d3f156da08 100644 --- a/creusot/src/backend/dependency.rs +++ b/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,6 +58,10 @@ impl<'tcx> Dependency<'tcx> { TyKind::Adt(def, _) if !def.is_box() => { Some(item_symb(tcx, def.did(), rustc_hir::def::Namespace::TypeNS)) } + 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.item_name(aty.def_id).as_str()))) } diff --git a/creusot/src/backend/signature.rs b/creusot/src/backend/signature.rs index d424a70d83..f3f4175fea 100644 --- a/creusot/src/backend/signature.rs +++ b/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>>( diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs index 9f3001c392..3e98519e2a 100644 --- a/creusot/src/backend/ty.rs +++ b/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); diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs index bb5c896f80..f610cea585 100644 --- a/creusot/src/backend/ty_inv.rs +++ b/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) { diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index 0d6ca28461..b073a95a72 100644 --- a/creusot/src/ctx.rs +++ b/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 { diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs index 15bdb91e58..b504a7c417 100644 --- a/creusot/src/translation/function/terminator.rs +++ b/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 { diff --git a/creusot/tests/should_succeed/syntax/01_idents/why3session.xml b/creusot/tests/should_succeed/syntax/01_idents/why3session.xml new file mode 100644 index 0000000000..79a0328ad2 --- /dev/null +++ b/creusot/tests/should_succeed/syntax/01_idents/why3session.xml @@ -0,0 +1,8 @@ + + + + + + + diff --git a/creusot/tests/should_succeed/syntax/01_idents/why3shapes.gz b/creusot/tests/should_succeed/syntax/01_idents/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..8039d107e60d7999ed0f63df0240e8d413a7ba34 GIT binary patch literal 45 xcmb2|=3oGW|CcWWX`J)W@z4#^@YdBjcjo-&AcNowm!3RgVo;m=MqCo83IJJ{58wa* literal 0 HcmV?d00001 diff --git a/creusot/tests/should_succeed/syntax/15_impl_trait.coma b/creusot/tests/should_succeed/syntax/15_impl_trait.coma new file mode 100644 index 0000000000..a8e9dc9d21 --- /dev/null +++ b/creusot/tests/should_succeed/syntax/15_impl_trait.coma @@ -0,0 +1,77 @@ +module M_15_impl_trait__qyi17433463795637978863__a [#"15_impl_trait.rs" 10 4 10 23] (* <() as MyTrait> *) + let%span s15_impl_trait0 = "15_impl_trait.rs" 11 8 11 12 + + use prelude.prelude.Intrinsic + + use prelude.prelude.Borrow + + meta "compute_max_steps" 1000000 + + let rec a'0 (self:()) (return' (ret:bool))= (! bb0 + [ bb0 = s0 [ s0 = [ &_0 <- [%#s15_impl_trait0] true ] s1 | s1 = return' {_0} ] ] + ) [ & _0 : bool = any_l () ] [ return' (result:bool)-> (! return' {result}) ] +end +module M_15_impl_trait__returns_iterator [#"15_impl_trait.rs" 15 0 15 41] + let%span s15_impl_trait0 = "15_impl_trait.rs" 15 29 15 41 + + use prelude.prelude.Intrinsic + + predicate inv'0 (_1 : ()) + + axiom inv_axiom'0 [@rewrite] : forall x : () [inv'0 x] . inv'0 x = true + + meta "compute_max_steps" 1000000 + + let rec returns_iterator'0 (_1:()) (return' (ret:()))= (! bb0 [ bb0 = return' {_0} ] ) [ & _0 : () = any_l () ] + [ return' (result:())-> {[@expl:returns_iterator result type invariant] [%#s15_impl_trait0] inv'0 result} + (! return' {result}) ] + +end +module M_15_impl_trait__main [#"15_impl_trait.rs" 20 0 20 13] + let%span s15_impl_trait0 = "15_impl_trait.rs" 21 12 21 30 + let%span s15_impl_trait1 = "15_impl_trait.rs" 23 18 23 19 + let%span s15_impl_trait2 = "15_impl_trait.rs" 19 10 19 14 + let%span s15_impl_trait3 = "15_impl_trait.rs" 15 29 15 41 + let%span s15_impl_trait4 = "15_impl_trait.rs" 6 10 6 14 + let%span sinvariant5 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 + + type opaque0'0 + + predicate inv'0 (_1 : opaque0'0) + + let rec returns_iterator'0 (_1:()) (return' (ret:opaque0'0))= any + [ return' (result:opaque0'0)-> {[%#s15_impl_trait3] inv'0 result} (! return' {result}) ] + + + use prelude.prelude.Borrow + + predicate invariant'0 (self : opaque0'0) = + [%#sinvariant5] inv'0 self + + predicate inv'1 (_1 : opaque0'0) + + axiom inv_axiom'0 [@rewrite] : forall x : opaque0'0 [inv'1 x] . inv'1 x = invariant'0 x + + let rec a'0 (self:opaque0'0) (return' (ret:bool))= {[@expl:a 'self' type invariant] [%#s15_impl_trait4] inv'1 self} + any [ return' (result:bool)-> (! return' {result}) ] + + use prelude.prelude.Intrinsic + + meta "compute_max_steps" 1000000 + + let rec main'0 (_1:()) (return' (ret:()))= (! bb0 + [ bb0 = s0 + [ s0 = returns_iterator'0 {[%#s15_impl_trait0] ()} (fun (_ret':opaque0'0) -> [ &_4 <- _ret' ] s1) | s1 = bb1 ] + + | bb1 = s0 [ s0 = a'0 {_4} (fun (_ret':bool) -> [ &x <- _ret' ] s1) | s1 = bb2 ] + | bb2 = bb3 + | bb3 = s0 [ s0 = {[@expl:assertion] [%#s15_impl_trait1] x} s1 | s1 = return' {_0} ] ] + ) [ & _0 : () = any_l () | & x : bool = any_l () | & _4 : opaque0'0 = any_l () ] + [ return' (result:())-> {[@expl:main ensures] [%#s15_impl_trait2] true} (! return' {result}) ] + +end +module M_15_impl_trait__qyi17433463795637978863__a__refines [#"15_impl_trait.rs" 10 4 10 23] (* <() as MyTrait> *) + let%span s15_impl_trait0 = "15_impl_trait.rs" 10 4 10 23 + + goal refines : [%#s15_impl_trait0] true +end diff --git a/creusot/tests/should_succeed/syntax/15_impl_trait.rs b/creusot/tests/should_succeed/syntax/15_impl_trait.rs new file mode 100644 index 0000000000..08e607408d --- /dev/null +++ b/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); +} diff --git a/creusot/tests/should_succeed/syntax/15_impl_trait/why3session.xml b/creusot/tests/should_succeed/syntax/15_impl_trait/why3session.xml new file mode 100644 index 0000000000..a9c2aef0f9 --- /dev/null +++ b/creusot/tests/should_succeed/syntax/15_impl_trait/why3session.xml @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/syntax/15_impl_trait/why3shapes.gz b/creusot/tests/should_succeed/syntax/15_impl_trait/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..5e5f19891381120ab2276b066833dc4c2cb27111 GIT binary patch literal 206 zcmV;<05Sg`iwFP!00000|22%UZo@DPM0b6Kwzio_NsOcd9l99q9%KzjnL-Stu4_91 z^7l>ZWINowcdr{eA9>W-UUZuKpW)qZ?dHuaM!(19diWpB^2_~jd4WAN&tTTTJX{Ya z-kryjt{qQ356c}{C45SFmp=B6chgy$&qs$}k4J2balSZLNGj&8fD}jxDOazZ1SBUG zTQD8QLhP$cfK?!=WX(|`1rMYFZjf)C*?Q90iNxSi38|(inXo3sS|UTfVblim2d=H6 Ig#iHo0ITv{4*&oF literal 0 HcmV?d00001 From 5258e1d39280858309667d0d82b6d66c74b3d329 Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Sat, 8 Feb 2025 13:02:13 +0100 Subject: [PATCH 2/3] Very rudimentary support for synthetic types --- creusot/src/backend/dependency.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs index d3f156da08..dbe12ba3af 100644 --- a/creusot/src/backend/dependency.rs +++ b/creusot/src/backend/dependency.rs @@ -62,9 +62,9 @@ impl<'tcx> Dependency<'tcx> { "opaque{}", tcx.def_path(aty.def_id).data.last().unwrap().disambiguator ))), - TyKind::Alias(_, aty) => { - Some(Symbol::intern(&type_name(tcx.item_name(aty.def_id).as_str()))) - } + 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 From c7cb87e9b7d7cc7e11f6cb0fb840261693b4761c Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Sat, 8 Feb 2025 15:14:59 +0100 Subject: [PATCH 3/3] lol apit --- creusot/src/backend/dependency.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs index dbe12ba3af..539bd34715 100644 --- a/creusot/src/backend/dependency.rs +++ b/creusot/src/backend/dependency.rs @@ -69,7 +69,9 @@ impl<'tcx> Dependency<'tcx> { "closure{}", tcx.def_path(*def_id).data.last().unwrap().disambiguator ))), - TyKind::Param(p) => Some(Symbol::intern(&type_name(p.name.as_str()))), + TyKind::Param(p) => { + Some(Symbol::intern(&type_name(&p.name.as_str().replace(" ", "_")))) + } _ => None, }, Dependency::Item(did, _) => match tcx.def_kind(did) {