Address comments

creusot-rs · Jun 14, 2023 · 4b94427 · 4b94427
1 parent 0ebf1dc
commit 4b94427
Show file tree

Hide file tree

Showing 10 changed files with 28 additions and 37 deletions.
diff --git a/creusot-contracts/src/invariant.rs b/creusot-contracts/src/invariant.rs
@@ -44,14 +44,6 @@ impl<T> 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
@@ -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
@@ -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
@@ -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<TyInvKind> {
+        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
@@ -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
@@ -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<Module> {
         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
@@ -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<Module> {
     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
@@ -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
@@ -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
@@ -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()