new-mut-ref: move/copy info for struct update tails

source/rust_verify/src/rust_to_vir_expr.rs

@@ -2480,7 +2480,11 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
         ExprKind::Struct(qpath, fields, struct_tail) => {
             let update = match struct_tail {
                 // Some(update) => Some(expr_to_vir(bctx, update, modifier)?),
-                StructTailExpr::Base(expr) => Some(expr_to_vir(bctx, expr, modifier)?.to_place()),
+                StructTailExpr::Base(tail_expr) => {
+                    let place = expr_to_vir(bctx, tail_expr, modifier)?.to_place();
+                    let tf = ctor_tail_get_taken_fields(bctx, expr)?;
+                    Some(vir::ast::CtorUpdateTail { place: place, taken_fields: tf })
+                }
                 StructTailExpr::DefaultFields(..) => {
                     unsupported_err!(
                         expr.span,
@@ -3695,3 +3699,44 @@ pub(crate) fn borrow_mut_vir(
     let typ = Arc::new(TypX::MutRef(place.typ.clone()));
     bctx.spanned_typed_new(span, &typ, x)
 }
+
+fn ctor_tail_get_taken_fields<'tcx>(
+    bctx: &BodyCtxt<'tcx>,
+    expr: &Expr<'tcx>,
+) -> Result<Arc<Vec<(vir::ast::Ident, UnfinalizedReadKind)>>, VirErr> {
+    let ExprKind::Struct(_, fields, _) = &expr.kind else {
+        crate::internal_err!(
+            expr.span,
+            "ctor_tail_get_taken_fields should only be called for ExprKind::Struct"
+        );
+    };
+
+    let ty = bctx.types.node_type(expr.hir_id);
+    let TyKind::Adt(adt_def, args) = ty.kind() else {
+        crate::internal_err!(expr.span, "Expected TyKind::Adt for struct expression");
+    };
+
+    if !adt_def.is_struct() {
+        crate::internal_err!(expr.span, "Expected struct for struct expression with tail");
+    }
+    let variant_def = adt_def.non_enum_variant();
+
+    let mut taken_fields = vec![];
+    // Iterate over all fields that are NOT present in the given struct expression.
+    for field_def in variant_def.fields.iter() {
+        if fields.iter().any(|f| f.ident.name == field_def.name) {
+            continue;
+        }
+        let ty = field_def.ty(bctx.ctxt.tcx, args);
+        let rk = if bctx.is_copy(ty) { vir::ast::ReadKind::Copy } else { vir::ast::ReadKind::Move };
+        let rk = UnfinalizedReadKind { preliminary_kind: rk, id: bctx.ctxt.unique_read_kind_id() };
+        let ident = field_ident_from_rust(field_def.name.as_str());
+        taken_fields.push((ident, rk));
+    }
+
+    if fields.len() + taken_fields.len() != variant_def.fields.len() {
+        crate::internal_err!(expr.span, "ctor_tail_get_taken_fields: field counts are wrong");
+    }
+
+    Ok(Arc::new(taken_fields))
+}

source/rust_verify_test/tests/modes.rs

@@ -1527,3 +1527,37 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::foo` with mode exec")
 }
+
+test_verify_one_file! {
+    #[test] fine_grained_checking_for_ctor_with_update verus_code! {
+        #[verifier::external_body]
+        tracked struct X { }
+
+        tracked struct Foo {
+            tracked tr: X,
+            ghost gh: X,
+        }
+
+        proof fn test(foo: Foo, tracked x: X) {
+            // This is ok because we only need the ghost field off of foo
+            let tracked foo2 = Foo { tr: x, .. foo };
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] fine_grained_checking_for_ctor_with_update2 verus_code! {
+        #[verifier::external_body]
+        tracked struct X { }
+
+        tracked struct Foo {
+            tracked tr: X,
+            ghost gh: X,
+        }
+
+        proof fn test(foo: Foo, tracked x: X) {
+            // not ok, needs a tracked field of foo
+            let tracked foo2 = Foo { gh: x, .. foo };
+        }
+    } => Err(err) => assert_vir_error_msg(err, "expression has mode spec, expected mode proof")
+}

source/rust_verify_test/tests/mut_refs.rs

@@ -2549,3 +2549,127 @@ test_verify_one_file_with_options! {
         }
     } => Err(err) => assert_fails(err, 4)
 }
+
+test_verify_one_file_with_options! {
+    #[test] ctor_with_update_tail ["new-mut-ref"] => verus_code! {
+        tracked struct TTPair<A, B> {
+            tracked a: A,
+            tracked b: B,
+        }
+
+        fn test1() {
+            let mut g1: Ghost<int> = Ghost(1);
+            let mut g2: Ghost<int> = Ghost(2);
+            let mut g3: Ghost<int> = Ghost(3);
+
+            let tracked p = TTPair {
+                a: &mut g1,
+                b: &mut g2,
+            };
+
+            proof {
+                *p.a.borrow_mut() = 4;
+                *p.b.borrow_mut() = 5;
+            }
+
+            let tracked p2 = TTPair {
+                a: &mut g3,
+                .. p
+            };
+
+            assert(has_resolved(p.b)); // FAILS
+
+            proof {
+                *p2.b.borrow_mut() = 4;
+            }
+        }
+
+        fn test2() {
+            let mut g1: Ghost<int> = Ghost(1);
+            let mut g2: Ghost<int> = Ghost(2);
+            let mut g3: Ghost<int> = Ghost(3);
+
+            let tracked p = TTPair {
+                a: &mut g1,
+                b: &mut g2,
+            };
+
+            proof {
+                *p.a.borrow_mut() = 4;
+                *p.b.borrow_mut() = 5;
+            }
+
+            let tracked p2 = TTPair {
+                a: &mut g3,
+                .. p
+            };
+
+            // ok, p.a was not moved
+            assert(has_resolved(p.a));
+
+            proof {
+                *p2.b.borrow_mut() = 4;
+            }
+        }
+
+        fn test3() {
+            let mut g1: Ghost<int> = Ghost(1);
+            let mut g2: Ghost<int> = Ghost(2);
+            let mut g3: Ghost<int> = Ghost(3);
+
+            let tracked p = TTPair {
+                a: &mut g1,
+                b: &mut g2,
+            };
+
+            proof {
+                *p.a.borrow_mut() = 4;
+                *p.b.borrow_mut() = 5;
+            }
+
+            let tracked p2 = TTPair {
+                a: &mut g3,
+                .. p
+            };
+
+            proof {
+                *p.a.borrow_mut() = 4;
+                *p2.a.borrow_mut() = 5;
+                *p2.b.borrow_mut() = 6;
+            }
+
+            assert(g1@ == 4);
+            assert(g3@ == 5);
+            assert(g2@ == 6);
+
+            assert(false); // FAILS
+        }
+
+        spec fn id<A>(a: A) -> A { a }
+
+        fn test4() {
+            let mut g1: Ghost<int> = Ghost(1);
+            let mut g2: Ghost<int> = Ghost(2);
+            let mut g3: Ghost<int> = Ghost(3);
+
+            let tracked p = TTPair {
+                a: &mut g1,
+                b: &mut g2,
+            };
+
+            proof {
+                *p.a.borrow_mut() = 4;
+                *p.b.borrow_mut() = 5;
+            }
+
+            let tracked ref_g3 = &mut g3;
+            // this doesn't do any moves because it's ghost mode:
+            let ghost p2 = TTPair {
+                a: id(ref_g3),
+                .. p
+            };
+
+            assert(has_resolved(p.b));
+        }
+    } => Err(err) => assert_fails(err, 2)
+}

source/vir/src/ast.rs

@@ -854,6 +854,17 @@ pub enum AutospecUsage {
     Final,
 }
 
+/// Represents the expression after the '..' in a "ctor update"
+/// like the `foo` in `{ a: e1, b: e2, .. foo }`.
+#[derive(Clone, Debug, Serialize, Deserialize, ToDebugSNode)]
+pub struct CtorUpdateTail {
+    pub place: Place,
+    /// This list needs to contain all the fields that are NOT explicitly listed.
+    /// i.e., this is all the fields that are moved or copied out of the input struct.
+    /// This information is needed by resolution analysis.
+    pub taken_fields: Arc<Vec<(Ident, UnfinalizedReadKind)>>,
+}
+
 /// Expression, similar to rustc_hir::Expr
 pub type Expr = Arc<SpannedTyped<ExprX>>;
 pub type Exprs = Arc<Vec<Expr>>;
@@ -883,7 +894,7 @@ pub enum ExprX {
     /// with field initializers Binders<Expr> and an optional ".." update expression.
     /// For tuple-style variants, the fields are named "_0", "_1", etc.
     /// Fields can appear **in any order** even for tuple variants.
-    Ctor(Dt, Ident, Binders<Expr>, Option<Place>),
+    Ctor(Dt, Ident, Binders<Expr>, Option<CtorUpdateTail>),
     /// Primitive 0-argument operation
     NullaryOpr(NullaryOpr),
     /// Primitive unary operation

source/vir/src/ast_simplify.rs

@@ -8,11 +8,11 @@ use crate::ast::VarBinders;
 use crate::ast::VarIdent;
 use crate::ast::{
     AssocTypeImpl, AutospecUsage, BinaryOp, Binder, BuiltinSpecFun, ByRef, CallTarget, ChainedOp,
-    Constant, CtorPrintStyle, Datatype, DatatypeTransparency, DatatypeX, Dt, Expr, ExprX, Exprs,
-    Field, FieldOpr, Fun, Function, FunctionKind, Ident, InequalityOp, IntRange, ItemKind, Krate,
-    KrateX, Mode, MultiOp, Path, Pattern, PatternBinding, PatternX, Place, PlaceX, SpannedTyped,
-    Stmt, StmtX, TraitImpl, Typ, TypX, UnaryOp, UnaryOpr, Variant, VariantCheck, VirErr,
-    Visibility,
+    Constant, CtorPrintStyle, CtorUpdateTail, Datatype, DatatypeTransparency, DatatypeX, Dt, Expr,
+    ExprX, Exprs, Field, FieldOpr, Fun, Function, FunctionKind, Ident, InequalityOp, IntRange,
+    ItemKind, Krate, KrateX, Mode, MultiOp, Path, Pattern, PatternBinding, PatternX, Place, PlaceX,
+    SpannedTyped, Stmt, StmtX, TraitImpl, Typ, TypX, UnaryOp, UnaryOpr, Variant, VariantCheck,
+    VirErr, Visibility,
 };
 use crate::ast_util::{
     conjoin, disjoin, if_then_else, mk_eq, mk_ineq, place_to_expr, typ_args_for_datatype_typ,
@@ -471,7 +471,8 @@ fn simplify_one_expr(
             Ok(SpannedTyped::new(&expr.span, &expr.typ, call))
         }
         ExprX::Ctor(name, variant, partial_binders, Some(update)) => {
-            let (temp_decl, update) = small_or_temp(state, &place_to_expr(update));
+            let CtorUpdateTail { place, taken_fields: _ } = update;
+            let (temp_decl, update) = small_or_temp(state, &place_to_expr(place));
             let mut decls: Vec<Stmt> = Vec::new();
             let mut binders: Vec<Binder<Expr>> = Vec::new();
             if temp_decl.len() == 0 {

source/vir/src/ast_visitor.rs

@@ -1,10 +1,10 @@
 use crate::ast::{
     Arm, ArmX, Arms, AssocTypeImpl, AssocTypeImplX, BinaryOpr, CallTarget, CallTargetKind,
-    Datatype, DatatypeX, Expr, ExprX, Exprs, Field, Function, FunctionKind, FunctionX,
-    GenericBound, GenericBoundX, LoopInvariant, LoopInvariants, MaskSpec, NullaryOpr, Param,
-    ParamX, Params, Pattern, PatternBinding, PatternX, Place, PlaceX, SpannedTyped, Stmt, StmtX,
-    Trait, TraitImpl, TraitImplX, TraitX, Typ, TypDecorationArg, TypX, Typs, UnaryOpr, UnwindSpec,
-    VarBinder, VarBinderX, VarBinders, VarIdent, Variant, VirErr,
+    CtorUpdateTail, Datatype, DatatypeX, Expr, ExprX, Exprs, Field, Function, FunctionKind,
+    FunctionX, GenericBound, GenericBoundX, LoopInvariant, LoopInvariants, MaskSpec, NullaryOpr,
+    Param, ParamX, Params, Pattern, PatternBinding, PatternX, Place, PlaceX, SpannedTyped, Stmt,
+    StmtX, Trait, TraitImpl, TraitImplX, TraitX, Typ, TypDecorationArg, TypX, Typs, UnaryOpr,
+    UnwindSpec, VarBinder, VarBinderX, VarBinders, VarIdent, Variant, VirErr,
 };
 use crate::def::Spanned;
 use crate::messages::Span;
@@ -315,9 +315,9 @@ pub(crate) trait AstVisitor<R: Returner, Err, Scope: Scoper> {
                 let oe = self.visit_opt_expr(opt_e)?;
                 R::ret(|| expr_new(ExprX::Call(R::get(ct), R::get_vec_a(es), R::get_opt(oe))))
             }
-            ExprX::Ctor(dt, id, binders, opt_e) => {
+            ExprX::Ctor(dt, id, binders, opt_tail) => {
                 let bs = self.visit_binders_expr(binders)?;
-                let oe = self.visit_opt_place(opt_e)?;
+                let oe = R::map_opt(opt_tail, &mut |p| self.visit_ctor_update_tail(p))?;
                 R::ret(|| {
                     expr_new(ExprX::Ctor(dt.clone(), id.clone(), R::get_vec_a(bs), R::get_opt(oe)))
                 })
@@ -650,6 +650,15 @@ pub(crate) trait AstVisitor<R: Returner, Err, Scope: Scoper> {
         }
     }
 
+    fn visit_ctor_update_tail(
+        &mut self,
+        tail: &CtorUpdateTail,
+    ) -> Result<R::Ret<CtorUpdateTail>, Err> {
+        let CtorUpdateTail { place, taken_fields } = tail;
+        let place = self.visit_place(place)?;
+        R::ret(|| CtorUpdateTail { place: R::get(place), taken_fields: taken_fields.clone() })
+    }
+
     fn visit_arms(&mut self, arms: &Arms) -> Result<R::Vec<Arm>, Err> {
         R::map_vec(arms, &mut |e| self.visit_arm(e))
     }