From 4b94427271ed66fd5f4332c12265f0c88261fd37 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Wed, 14 Jun 2023 16:01:24 +0200 Subject: [PATCH] Address comments --- creusot-contracts/src/invariant.rs | 8 -------- creusot/src/backend/clone_map.rs | 17 ++++------------- creusot/src/backend/constant.rs | 2 +- creusot/src/backend/dependency.rs | 10 +++++++++- creusot/src/backend/interface.rs | 2 +- creusot/src/backend/logic.rs | 8 ++++---- creusot/src/backend/program.rs | 4 ++-- creusot/src/backend/traits.rs | 4 ++-- creusot/src/backend/ty.rs | 4 ++-- creusot/src/backend/ty_inv.rs | 6 +++--- 10 files changed, 28 insertions(+), 37 deletions(-) diff --git a/creusot-contracts/src/invariant.rs b/creusot-contracts/src/invariant.rs index df6d8d14f0..119798e40e 100644 --- a/creusot-contracts/src/invariant.rs +++ b/creusot-contracts/src/invariant.rs @@ -44,14 +44,6 @@ impl UserInv for T { } } -impl UserInv for i32 { - #[predicate] - #[open] - fn user_inv(self) -> bool { - pearlite! { self@ > 0 } - } -} - impl<'a, T: Invariant + ?Sized> Invariant for &'a T { #[predicate] #[open] diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs index 8787b2f404..9a3bb8eb78 100644 --- a/creusot/src/backend/clone_map.rs +++ b/creusot/src/backend/clone_map.rs @@ -210,15 +210,7 @@ impl<'tcx> CloneInfo { } impl<'tcx> CloneMap<'tcx> { - pub(crate) fn new(tcx: TyCtxt<'tcx>, self_id: DefId, clone_level: CloneLevel) -> Self { - Self::new_with_tid(tcx, TransId::Item(self_id), clone_level) - } - - pub(crate) fn new_with_tid( - tcx: TyCtxt<'tcx>, - self_id: TransId, - clone_level: CloneLevel, - ) -> Self { + pub(crate) fn new(tcx: TyCtxt<'tcx>, self_id: TransId, clone_level: CloneLevel) -> Self { let mut names = IndexMap::new(); let self_id = match self_id { @@ -233,7 +225,7 @@ impl<'tcx> CloneMap<'tcx> { CloneNode::new(tcx, (self_id, subst)).erase_regions(tcx) } - TransId::TyInv(inv_kind) => CloneNode::TyInv(inv_kind.to_ty(tcx)), + TransId::TyInv(inv_kind) => CloneNode::TyInv(inv_kind.to_skeleton_ty(tcx)), }; debug!("cloning self: {:?}", self_id); @@ -295,8 +287,7 @@ impl<'tcx> CloneMap<'tcx> { }; } - let base = if let CloneNode::TyInv(ty) = key { - let inv_kind = TyInvKind::from_ty(ty); + let base = if let Some(inv_kind) = key.ty_inv_kind() { Symbol::intern(&*inv_module_name(self.tcx, inv_kind)) } else { let did = key.did().unwrap().0; @@ -457,7 +448,7 @@ impl<'tcx> CloneMap<'tcx> { } let inv_kind = TyInvKind::from_ty(ty); - if let CloneNode::TyInv(self_ty) = self.self_id && TyInvKind::from_ty(self_ty) == inv_kind { + if self.self_id.ty_inv_kind().is_some_and(|self_kind| self_kind == inv_kind) { return; } diff --git a/creusot/src/backend/constant.rs b/creusot/src/backend/constant.rs index fdfafea946..602ff59c02 100644 --- a/creusot/src/backend/constant.rs +++ b/creusot/src/backend/constant.rs @@ -28,7 +28,7 @@ impl<'tcx> Why3Generator<'tcx> { let param_env = self.param_env(def_id); let span = self.def_span(def_id); let res = from_ty_const(&mut self.ctx, constant, param_env, span); - let mut names = CloneMap::new(self.tcx, def_id, CloneLevel::Body); + let mut names = CloneMap::new(self.tcx, def_id.into(), CloneLevel::Body); let res = res.to_why(self, &mut names, &LocalDecls::new()); let sig = signature_of(self, &mut names, def_id); let mut decls: Vec<_> = closure_generic_decls(self.tcx, def_id).collect(); diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs index 7b3f281e1a..2a8a6b148d 100644 --- a/creusot/src/backend/dependency.rs +++ b/creusot/src/backend/dependency.rs @@ -9,7 +9,7 @@ use crate::{ util::{self, ItemType}, }; -use super::ty_inv; +use super::ty_inv::{self, TyInvKind}; /// Dependencies between items and the resolution logic to find the 'monomorphic' forms accounting /// for various Creusot hacks like the handling of closures. @@ -57,6 +57,14 @@ impl<'tcx> Dependency<'tcx> { } } + pub(crate) fn ty_inv_kind(self) -> Option { + if let Dependency::TyInv(ty) = self { + Some(TyInvKind::from_ty(ty)) + } else { + None + } + } + pub(crate) fn is_inv(&self) -> bool { matches!(self, Dependency::TyInv(_)) } diff --git a/creusot/src/backend/interface.rs b/creusot/src/backend/interface.rs index d8ffb5a0aa..03d75747c4 100644 --- a/creusot/src/backend/interface.rs +++ b/creusot/src/backend/interface.rs @@ -21,7 +21,7 @@ pub(crate) fn interface_for<'tcx>( def_id: DefId, ) -> (Module, CloneSummary<'tcx>) { debug!("interface_for: {def_id:?}"); - let mut names = CloneMap::new(ctx.tcx, def_id, CloneLevel::Stub); + let mut names = CloneMap::new(ctx.tcx, def_id.into(), CloneLevel::Stub); let mut sig = signature_of(ctx, &mut names, def_id); sig.contract.variant = Vec::new(); diff --git a/creusot/src/backend/logic.rs b/creusot/src/backend/logic.rs index eae2678db3..723db00ff6 100644 --- a/creusot/src/backend/logic.rs +++ b/creusot/src/backend/logic.rs @@ -65,7 +65,7 @@ fn builtin_body<'tcx>( ctx: &mut Why3Generator<'tcx>, def_id: DefId, ) -> (Module, CloneSummary<'tcx>) { - let mut names = CloneMap::new(ctx.tcx, def_id, CloneLevel::Stub); + let mut names = CloneMap::new(ctx.tcx, def_id.into(), CloneLevel::Stub); let mut sig = signature_of(ctx, &mut names, def_id); let (val_args, val_binders) = binders_to_args(ctx, sig.args); sig.args = val_binders; @@ -133,7 +133,7 @@ pub(crate) fn val_decl<'tcx>( } fn body_module<'tcx>(ctx: &mut Why3Generator<'tcx>, def_id: DefId) -> (Module, CloneSummary<'tcx>) { - let mut names = CloneMap::new(ctx.tcx, def_id, CloneLevel::Stub); + let mut names = CloneMap::new(ctx.tcx, def_id.into(), CloneLevel::Stub); let mut sig = signature_of(ctx, &mut names, def_id); let mut val_sig = sig.clone(); @@ -198,7 +198,7 @@ fn body_module<'tcx>(ctx: &mut Why3Generator<'tcx>, def_id: DefId) -> (Module, C } pub(crate) fn stub_module(ctx: &mut Why3Generator, def_id: DefId) -> Module { - let mut names = CloneMap::new(ctx.tcx, def_id, CloneLevel::Stub); + let mut names = CloneMap::new(ctx.tcx, def_id.into(), CloneLevel::Stub); let mut sig = signature_of(ctx, &mut names, def_id); if util::is_predicate(ctx.tcx, def_id) { @@ -225,7 +225,7 @@ fn proof_module(ctx: &mut Why3Generator, def_id: DefId) -> Option { return None; } - let mut names = CloneMap::new(ctx.tcx, def_id, CloneLevel::Body); + let mut names = CloneMap::new(ctx.tcx, def_id.into(), CloneLevel::Body); let mut sig = signature_of(ctx, &mut names, def_id); diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs index c1dc2b509b..1e638c5c18 100644 --- a/creusot/src/backend/program.rs +++ b/creusot/src/backend/program.rs @@ -37,7 +37,7 @@ use why3::{ use super::signature::sig_to_why3; fn closure_ty<'tcx>(ctx: &mut Why3Generator<'tcx>, def_id: DefId) -> Module { - let mut names = CloneMap::new(ctx.tcx, def_id, CloneLevel::Body); + let mut names = CloneMap::new(ctx.tcx, def_id.into(), CloneLevel::Body); let mut decls = Vec::new(); let TyKind::Closure(_, subst) = ctx.tcx.type_of(def_id).subst_identity().kind() else { unreachable!() }; @@ -152,7 +152,7 @@ pub(crate) fn translate_function<'tcx, 'sess>( def_id: DefId, ) -> Option { let tcx = ctx.tcx; - let mut names = CloneMap::new(tcx, def_id, CloneLevel::Body); + let mut names = CloneMap::new(tcx, def_id.into(), CloneLevel::Body); let body_ids = collect_body_ids(ctx, def_id)?; let body = to_why(ctx, &mut names, body_ids[0]); diff --git a/creusot/src/backend/traits.rs b/creusot/src/backend/traits.rs index 40e35ce5f3..d3e13499d9 100644 --- a/creusot/src/backend/traits.rs +++ b/creusot/src/backend/traits.rs @@ -16,7 +16,7 @@ pub(crate) fn lower_impl<'tcx>(ctx: &mut Why3Generator<'tcx>, def_id: DefId) -> let tcx = ctx.tcx; let data = ctx.trait_impl(def_id).clone(); - let mut names = CloneMap::new(ctx.tcx, def_id, CloneLevel::Body); + let mut names = CloneMap::new(ctx.tcx, def_id.into(), CloneLevel::Body); let mut impl_decls = Vec::new(); for refn in &data.refinements { @@ -41,7 +41,7 @@ impl<'tcx> Why3Generator<'tcx> { pub(crate) fn translate_assoc_ty(&mut self, def_id: DefId) -> (Module, CloneSummary<'tcx>) { assert_eq!(util::item_type(self.tcx, def_id), ItemType::AssocTy); - let mut names = CloneMap::new(self.tcx, def_id, CloneLevel::Interface); + let mut names = CloneMap::new(self.tcx, def_id.into(), CloneLevel::Interface); let mut decls: Vec<_> = all_generic_decls_for(self.tcx, def_id).collect(); let name = item_name(self.tcx, def_id, Namespace::TypeNS); diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs index c99c0e7334..91bf627e64 100644 --- a/creusot/src/backend/ty.rs +++ b/creusot/src/backend/ty.rs @@ -291,7 +291,7 @@ pub(crate) fn translate_tydecl( return None; } - let mut names = CloneMap::new(ctx.tcx, repr, CloneLevel::Stub); + let mut names = CloneMap::new(ctx.tcx, repr.into(), CloneLevel::Stub); let name = module_name(ctx.tcx, repr); let span = ctx.def_span(repr); @@ -432,7 +432,7 @@ pub(crate) fn translate_accessor( let substs = InternalSubsts::identity_for_item(ctx.tcx, adt_did); let repr = ctx.representative_type(adt_did); - let mut names = CloneMap::new(ctx.tcx, repr, CloneLevel::Stub); + let mut names = CloneMap::new(ctx.tcx, repr.into(), CloneLevel::Stub); // UGLY hack to ensure that we don't explicitly use/clone the members of a binding group let bg = ctx.binding_group(repr).clone(); diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs index a5e1d62e29..ce23d77ee9 100644 --- a/creusot/src/backend/ty_inv.rs +++ b/creusot/src/backend/ty_inv.rs @@ -38,7 +38,7 @@ impl TyInvKind { } } - pub(crate) fn to_ty<'tcx>(self, tcx: TyCtxt<'tcx>) -> Ty<'tcx> { + pub(crate) fn to_skeleton_ty<'tcx>(self, tcx: TyCtxt<'tcx>) -> Ty<'tcx> { match self { TyInvKind::Trivial => tcx.mk_ty_param(0, Symbol::intern("T")), TyInvKind::Borrow => { @@ -82,7 +82,7 @@ pub(crate) fn build_inv_module<'tcx>( ctx: &mut Why3Generator<'tcx>, inv_kind: TyInvKind, ) -> (Module, CloneSummary<'tcx>) { - let mut names = CloneMap::new_with_tid(ctx.tcx, TransId::TyInv(inv_kind), CloneLevel::Stub); + let mut names = CloneMap::new(ctx.tcx, TransId::TyInv(inv_kind), CloneLevel::Stub); let generics = inv_kind.generics(ctx.tcx); let inv_axiom = build_inv_axiom(ctx, &mut names, inv_kind); @@ -119,7 +119,7 @@ fn build_inv_axiom<'tcx>( let param_env = if let TyInvKind::Adt(did) = inv_kind { ctx.param_env(did) } else { ParamEnv::empty() }; - let ty = inv_kind.to_ty(ctx.tcx); + let ty = inv_kind.to_skeleton_ty(ctx.tcx); let lhs: Exp = Exp::impure_qvar(names.ty_inv(ty)).app_to(Exp::pure_var("self".into())); let rhs = if TyInvKind::Trivial == inv_kind { Exp::mk_true()