Allow logically reborrowing through derefs of ghost and indexing things

creusot-contracts/src/ghost.rs

@@ -11,6 +11,7 @@ impl<T: ?Sized> Deref for Ghost<T> {
     #[trusted]
     #[ghost]
     #[open(self)]
+    #[rustc_diagnostic_item = "ghost_deref"]
     #[creusot::builtins = "prelude.Ghost.inner"]
     fn deref(&self) -> &Self::Target {
         pearlite! { absurd }
@@ -47,6 +48,7 @@ impl<T: ?Sized> Ghost<T> {
     #[trusted]
     #[ghost]
     #[open(self)]
+    #[rustc_diagnostic_item = "ghost_inner"]
     #[creusot::builtins = "prelude.Ghost.inner"]
     pub fn inner(self) -> T
     where

creusot-contracts/src/logic/ops.rs

@@ -6,6 +6,7 @@ pub trait IndexLogic<I> {
     type Item;
 
     #[ghost]
+    #[rustc_diagnostic_item = "index_logic_method"]
     fn index_logic(self, idx: I) -> Self::Item;
 }
 

creusot/src/translation/pearlite.rs

@@ -5,12 +5,16 @@
 // Transforms THIR into a Term which may be serialized in Creusot metadata files for usage by dependent crates
 // The `lower` module then transforms a `Term` into a WhyML expression.
 
-use std::collections::HashSet;
+use std::{
+    collections::HashSet,
+    fmt::{Display, Formatter},
+    unreachable,
+};
 
 use crate::{
     error::{CrErr, CreusotResult, Error},
     translation::TranslationCtx,
-    util,
+    util::{self, is_ghost_ty},
 };
 use itertools::Itertools;
 use log::*;
@@ -27,8 +31,8 @@ use rustc_middle::{
         AdtExpr, ArmId, Block, ClosureExpr, ExprId, ExprKind, Pat, PatKind, StmtId, StmtKind, Thir,
     },
     ty::{
-        int_ty, subst::SubstsRef, uint_ty, Ty, TyCtxt, TyKind, TypeFoldable, TypeVisitable,
-        UpvarSubsts,
+        int_ty, subst::SubstsRef, uint_ty, GenericArg, Ty, TyCtxt, TyKind, TypeFoldable,
+        TypeVisitable, UpvarSubsts,
     },
 };
 use rustc_serialize::{Decodable, Decoder, Encodable, Encoder};
@@ -485,7 +489,11 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                     }
                 }
             }
-            ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg } => self.expr_term(arg),
+            ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg } => {
+                let mut e = self.expr_term(arg)?;
+                e.ty = ty;
+                Ok(e)
+            }
             ExprKind::Borrow { arg, .. } => {
                 let t = self.logical_reborrow(arg)?;
                 Ok(Term { ty, span, kind: t })
@@ -798,6 +806,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
         if let ExprKind::Deref { arg } = self.thir[rebor_id].kind {
             return Ok(self.expr_term(arg)?.kind);
         };
+        // eprintln!("{}", PrintExpr(self.thir, rebor_id));
         // Handle every other case.
         let (cur, fin) = self.logical_reborrow_inner(rebor_id)?;
 
@@ -822,22 +831,77 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                 ))
             }
             ExprKind::Deref { arg } => {
+                // Detect * ghost_deref & and treat that as a single 'projection'
+                if self.is_ghost_deref(*arg) {
+                    let ExprKind::Call { args, .. } = &self.thir[*arg].kind else { unreachable!() };
+                    let ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg } = self.thir[args[0]].kind else { unreachable!() };
+
+                    let (cur, fin) = self.logical_reborrow_inner(arg)?;
+                    let deref_method =
+                        self.ctx.get_diagnostic_item(Symbol::intern("ghost_inner")).unwrap();
+                    // Extract the `T` from `Ghost<T>`
+                    let TyKind::Adt(_, subst) = self.thir[arg].ty.peel_refs().kind() else {unreachable!()};
+                    return Ok((
+                        Term::call(self.ctx.tcx, deref_method, subst, vec![cur]),
+                        Term::call(self.ctx.tcx, deref_method, subst, vec![fin]),
+                    ));
+                };
+
                 let inner = self.expr_term(*arg)?;
-                if let TermKind::Var(_) = inner.kind {}
-                let ty = inner.ty.builtin_deref(false).expect("expected reference type").ty;
 
-                Ok((
-                    Term { ty, span, kind: TermKind::Cur { term: Box::new(inner.clone()) } },
-                    Term { ty, span, kind: TermKind::Fin { term: Box::new(inner) } },
-                ))
+                Ok((inner.clone().cur().span(span), inner.fin().span(span)))
+            }
+            ExprKind::Call { ty: fn_ty, args, .. } if fn_ty.is_fn() => {
+                let index_logic_method =
+                    self.ctx.get_diagnostic_item(Symbol::intern("index_logic_method")).unwrap();
+
+                let TyKind::FnDef(id,_) = fn_ty.kind() else { panic!("expected function type") };
+
+                let (cur, fin) = self.logical_reborrow_inner(args[0])?;
+
+                if id == &index_logic_method {
+                    let index = self.expr_term(args[1])?;
+
+                    let subst =
+                        self.ctx.mk_substs(&[GenericArg::from(cur.ty), GenericArg::from(index.ty)]);
+
+                    Ok((
+                        Term::call(
+                            self.ctx.tcx,
+                            index_logic_method,
+                            subst,
+                            vec![cur, index.clone()],
+                        ),
+                        Term::call(
+                            self.ctx.tcx,
+                            index_logic_method,
+                            subst,
+                            vec![fin, index.clone()],
+                        ),
+                    ))
+                } else {
+                    return Err(Error::new(span, format!("unsupported projection {id:?}")));
+                }
             }
-            _ => Err(Error::new(
+            e => Err(Error::new(
                 span,
-                "unsupported logical reborrow, only simple field projections are supproted, sorry",
+                format!("unsupported logical reborrow {e:?}, only simple field projections are supported"),
             )),
         }
     }
 
+    pub(crate) fn is_ghost_deref(&self, expr_id: ExprId) -> bool {
+        let ExprKind::Call { ty, .. } = &self.thir[expr_id].kind else {return false};
+
+        let TyKind::FnDef(id, sub) = ty.kind() else { panic!("expected function type") };
+
+        if Some(*id) != self.ctx.get_diagnostic_item(Symbol::intern("deref_method")) {
+            return false;
+        }
+
+        sub[0].as_type().map(|ty| is_ghost_ty(self.ctx.tcx, ty)).unwrap_or(false)
+    }
+
     fn mk_projection(&self, lhs: Term<'tcx>, name: FieldIdx) -> Result<TermKind<'tcx>, Error> {
         let pat = field_pattern(lhs.ty, name).expect("mk_projection: no term for field");
 
@@ -1121,6 +1185,27 @@ impl<'tcx> Term<'tcx> {
         Term { ty: tcx.types.bool, kind: TermKind::Lit(Literal::Bool(false)), span: DUMMY_SP }
     }
 
+    pub(crate) fn call(
+        tcx: TyCtxt<'tcx>,
+        def_id: DefId,
+        subst: SubstsRef<'tcx>,
+        args: Vec<Term<'tcx>>,
+    ) -> Self {
+        let ty = tcx.type_of(def_id).subst(tcx, subst);
+        let result = ty.fn_sig(tcx).skip_binder().output();
+        let fun = Term {
+            ty: tcx.type_of(def_id).subst(tcx, subst),
+            kind: TermKind::Item(def_id, subst),
+            span: DUMMY_SP,
+        };
+
+        Term {
+            ty: result,
+            span: DUMMY_SP,
+            kind: TermKind::Call { id: def_id, subst, fun: Box::new(fun.clone()), args },
+        }
+    }
+
     pub(crate) fn var(sym: Symbol, ty: Ty<'tcx>) -> Self {
         Term { ty, kind: TermKind::Var(sym), span: DUMMY_SP }
     }
@@ -1439,3 +1524,84 @@ impl<'tcx> Term<'tcx> {
         }
     }
 }
+
+struct PrintExpr<'a, 'tcx>(&'a Thir<'tcx>, ExprId);
+
+impl Display for PrintExpr<'_, '_> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        print_thir_expr(f, self.0, self.1)
+    }
+}
+
+fn print_thir_expr<'tcx>(
+    fmt: &mut Formatter,
+    thir: &Thir<'tcx>,
+    expr_id: ExprId,
+) -> std::fmt::Result {
+    match &thir[expr_id].kind {
+        ExprKind::Call { fun, args, .. } => {
+            print_thir_expr(fmt, thir, *fun)?;
+            write!(fmt, "(")?;
+            for a in args.iter() {
+                print_thir_expr(fmt, thir, *a)?;
+                write!(fmt, ",")?;
+            }
+            write!(fmt, ")")?;
+        }
+        ExprKind::Deref { arg } => {
+            write!(fmt, "* ")?;
+            print_thir_expr(fmt, thir, *arg)?;
+        }
+        ExprKind::Borrow { borrow_kind, arg } => {
+            match borrow_kind {
+                BorrowKind::Shared => write!(fmt, "& ")?,
+                BorrowKind::Shallow => write!(fmt, "&shallow ")?,
+                BorrowKind::Mut { .. } => write!(fmt, "&mut ")?,
+            };
+
+            print_thir_expr(fmt, thir, *arg)?;
+        }
+        ExprKind::Field { lhs, variant_index, name } => {
+            print_thir_expr(fmt, thir, *lhs)?;
+            let ty = thir[expr_id].ty;
+            let (var_name, field_name) = match ty.kind() {
+                TyKind::Adt(def, _) => {
+                    let var = &def.variants()[*variant_index];
+                    (var.name.to_string(), var.fields[*name].name.to_string())
+                }
+                TyKind::Tuple(_) => ("_".into(), format!("{name:?}")),
+                _ => unreachable!(),
+            };
+
+            write!(fmt, " as {var_name} . {field_name}")?;
+        }
+        ExprKind::Index { lhs, index } => {
+            print_thir_expr(fmt, thir, *lhs)?;
+            write!(fmt, "[")?;
+            print_thir_expr(fmt, thir, *index)?;
+            write!(fmt, "]")?;
+        }
+        ExprKind::ZstLiteral { .. } => match thir[expr_id].ty.kind() {
+            TyKind::FnDef(id, _) => write!(fmt, "{id:?}")?,
+            _ => write!(fmt, "zst")?,
+        },
+        ExprKind::Literal { lit, neg } => {
+            if *neg {
+                write!(fmt, "-")?;
+            }
+
+            write!(fmt, "{}", lit.node)?;
+        }
+        ExprKind::Use { source } => print_thir_expr(fmt, thir, *source)?,
+        ExprKind::VarRef { id } => {
+            write!(fmt, "{:?}", id.0)?;
+        }
+        ExprKind::Scope { value, .. } => {
+            print_thir_expr(fmt, thir, *value)?;
+        }
+        _ => {
+            write!(fmt, "{:?}", thir[expr_id])?;
+        }
+    }
+    Ok(())
+}

creusot/src/translation/specification.rs

@@ -304,6 +304,7 @@ pub(crate) fn is_overloaded_item(tcx: TyCtxt, def_id: DefId) -> bool {
         || def_path.ends_with("::ops::Neg::neg")
         || def_path.ends_with("::boxed::Box::<T>::new")
         || def_path.ends_with("::ops::Deref::deref")
+        || def_path.ends_with("::ops::DerefMut::deref_mut")
         || def_path.ends_with("Ghost::<T>::from_fn")
 }
 

creusot/tests/should_succeed/100doors.mlcfg

@@ -272,7 +272,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 

creusot/tests/should_succeed/bug/874.mlcfg

@@ -164,7 +164,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 

creusot/tests/should_succeed/bug/two_phase.mlcfg

@@ -218,7 +218,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 

creusot/tests/should_succeed/cell/02.mlcfg

@@ -417,7 +417,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 

creusot/tests/should_succeed/filter_positive.mlcfg

@@ -319,7 +319,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 

creusot/tests/should_succeed/hashmap.mlcfg

@@ -527,7 +527,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 
@@ -2368,7 +2368,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
 

creusot/tests/should_succeed/heapsort_generic.mlcfg

@@ -1004,7 +1004,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 
@@ -1221,7 +1221,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
 

creusot/tests/should_succeed/hillel.mlcfg

@@ -218,7 +218,7 @@ module CreusotContracts_Logic_Ops_Impl0_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 19 8 19 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 20 8 20 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : Alloc_Vec_Vec_Type.t_vec t a) (ix : int) : t
     ensures { result = index_logic self ix }
 
@@ -303,7 +303,7 @@ module CreusotContracts_Ghost_Impl1_ShallowModel
     type t = t,
     type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy
   function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy =
-    [#"../../../../creusot-contracts/src/ghost.rs" 26 20 26 48] ShallowModel0.shallow_model (Ghost.inner self)
+    [#"../../../../creusot-contracts/src/ghost.rs" 27 20 27 48] ShallowModel0.shallow_model (Ghost.inner self)
   val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy
     ensures { result = shallow_model self }
 
@@ -1337,7 +1337,7 @@ module CreusotContracts_Logic_Ops_Impl2_IndexLogic
     predicate Inv1.inv = Inv1.inv,
     axiom .
   function index_logic [@inline:trivial] (self : slice t) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 41 8 41 31] Seq.get (ShallowModel0.shallow_model self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 42 8 42 31] Seq.get (ShallowModel0.shallow_model self) ix
   val index_logic [@inline:trivial] (self : slice t) (ix : int) : t
     ensures { result = index_logic self ix }
 
@@ -1487,7 +1487,7 @@ module CreusotContracts_Logic_Ops_Impl6_IndexLogic
   use seq.Seq
   use prelude.Int
   function index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t =
-    [#"../../../../creusot-contracts/src/logic/ops.rs" 85 8 85 33] Seq.get (Ghost.inner self) ix
+    [#"../../../../creusot-contracts/src/logic/ops.rs" 86 8 86 33] Seq.get (Ghost.inner self) ix
   val index_logic [@inline:trivial] (self : Ghost.ghost_ty (Seq.seq t)) (ix : int) : t
     ensures { result = index_logic self ix }