Use Place type everywhere in VIR AST (#1831)

Author: tjhance

source/rust_verify/src/automatic_derive.rs

@@ -3,7 +3,9 @@ use crate::verus_items::RustItem;
 use rustc_hir::HirId;
 use rustc_span::Span;
 use std::sync::Arc;
-use vir::ast::{BinaryOp, Expr, ExprX, FunctionX, Mode, SpannedTyped, VirErr, VirErrAs};
+use vir::ast::{
+    BinaryOp, Expr, ExprX, FunctionX, Mode, Place, PlaceX, SpannedTyped, VirErr, VirErrAs,
+};
 
 /// Traits with special handling
 #[derive(Clone, Copy, Debug)]
@@ -105,10 +107,16 @@ fn clone_add_post_condition<'tcx>(
 
     match &body.x {
         ExprX::Block(_stmts, Some(last_expr)) => match &last_expr.x {
-            ExprX::Var(id) if &*id.0 == "self" => {
-                uses_copy = true;
-                self_var = Some(last_expr.clone());
-            }
+            ExprX::ReadPlace(pl, _) => match &pl.x {
+                PlaceX::Local(id) if &*id.0 == "self" => {
+                    uses_copy = true;
+                    self_var = Some(last_expr.clone());
+                }
+                _ => {
+                    warn_unexpected();
+                    return Ok(());
+                }
+            },
             ExprX::Ctor { .. } => {
                 uses_copy = false;
                 self_var = None;
@@ -154,11 +162,20 @@ fn clone_add_post_condition<'tcx>(
 
 // TODO better place for this
 fn cleanup_span_ids<'tcx>(ctxt: &Context<'tcx>, span: Span, hir_id: HirId, expr: &Expr) -> Expr {
-    vir::ast_visitor::map_expr_visitor(expr, &|e: &Expr| {
-        let e = ctxt.spans.spanned_typed_new(span, &e.typ, e.x.clone());
-        let mut erasure_info = ctxt.erasure_info.borrow_mut();
-        erasure_info.hir_vir_ids.push((hir_id, e.span.id));
-        Ok(e)
-    })
+    vir::ast_visitor::map_expr_place_visitor(
+        expr,
+        &|e: &Expr| {
+            let e = ctxt.spans.spanned_typed_new(span, &e.typ, e.x.clone());
+            let mut erasure_info = ctxt.erasure_info.borrow_mut();
+            erasure_info.hir_vir_ids.push((hir_id, e.span.id));
+            Ok(e)
+        },
+        &|p: &Place| {
+            let p = ctxt.spans.spanned_typed_new(span, &p.typ, p.x.clone());
+            let mut erasure_info = ctxt.erasure_info.borrow_mut();
+            erasure_info.hir_vir_ids.push((hir_id, p.span.id));
+            Ok(p)
+        },
+    )
     .unwrap()
 }

source/rust_verify/src/context.rs

@@ -85,3 +85,14 @@ impl<'tcx> ContextX<'tcx> {
         r.bodies.push((local_def_id, c));
     }
 }
+
+impl<'tcx> BodyCtxt<'tcx> {
+    pub(crate) fn is_copy(&self, ty: rustc_middle::ty::Ty<'tcx>) -> bool {
+        let param_env = self.ctxt.tcx.param_env(self.fun_id);
+        let typing_env = rustc_middle::ty::TypingEnv {
+            param_env,
+            typing_mode: rustc_middle::ty::TypingMode::PostAnalysis,
+        };
+        self.ctxt.tcx.type_is_copy_modulo_regions(typing_env, ty)
+    }
+}

source/rust_verify/src/fn_call_to_vir.rs

@@ -57,7 +57,6 @@ pub mod lifetime;
 mod lifetime_ast;
 mod lifetime_emit;
 mod lifetime_generate;
-pub mod places;
 pub mod profiler;
 mod resolve_traits;
 pub mod reveal_hide;