new_mut_refs: distinguish copies from moves in pattern binders

Author: tjhance

source/rust_verify/src/rust_to_vir_expr.rs

@@ -562,6 +562,7 @@ pub(crate) fn pattern_to_vir_unadjusted<'tcx>(
                 mutable,
                 by_ref: vir_by_ref,
                 typ: var_typ.clone(),
+                copy: bctx.is_copy(bctx.types.node_type(pat.hir_id)),
             };
             match subpat {
                 None => PatternX::Var(binding),

source/rust_verify/src/rust_to_vir_func.rs

@@ -1202,6 +1202,7 @@ pub(crate) fn check_item_fn<'tcx>(
                     mutable: true,
                     by_ref: vir::ast::ByRef::No,
                     typ: typ.clone(),
+                    copy: false,
                 }),
             );
             let new_init_expr =

source/rust_verify_test/tests/mut_refs_patterns.rs

@@ -2035,3 +2035,139 @@ test_verify_one_file_with_options! {
         }
     } => Err(err) => assert_fails(err, 2)
 }
+
+test_verify_one_file_with_options! {
+    #[test] binders_in_pattern_copy_vs_no_copy ["new-mut-ref"] => verus_code! {
+        enum Option<A> {
+            Some(A),
+            None,
+        }
+        use crate::Option::Some;
+        use crate::Option::None;
+
+        fn consume<X>(x: X) { }
+
+        fn test_copy<X: Copy>(x: X, y: X) {
+            let t = (x, y);
+
+            match t {
+                (x, _) => { consume(x); }
+            }
+
+            assert(has_resolved(t));
+        }
+
+        fn test_no_copy<X>(x: X, y: X) {
+            let t = (x, y);
+
+            match t {
+                (x, _) => { consume(x); }
+            }
+
+            assert(has_resolved(t)); // FAILS
+        }
+
+        fn test_option_copy<X: Copy>(x: X, y: X) {
+            let t = Some((x, y));
+
+            match t {
+                Some((x, _)) => { consume(x); }
+                None => { }
+            }
+
+            assert(has_resolved(t));
+        }
+
+        fn test_option_no_copy<X>(x: X, y: X) {
+            let t = Some((x, y));
+
+            match t {
+                Some((x, _)) => { consume(x); }
+                None => { }
+            }
+
+            assert(has_resolved(t)); // FAILS
+        }
+
+        fn test_let_copy<X: Copy>(x: X, y: X) {
+            let t = (x, y);
+
+            let (x, _) = t;
+            consume(x);
+
+            assert(has_resolved(t));
+        }
+
+        fn test_let_no_copy<X>(x: X, y: X) {
+            let t = (x, y);
+
+            let (x, _) = t;
+            consume(x);
+
+            assert(has_resolved(t)); // FAILS
+        }
+
+
+
+
+        fn atbinder_test_copy<X: Copy>(x: X, y: X) {
+            let t = (x, y);
+
+            match t {
+                x @ (_, _) => { consume(x); }
+            }
+
+            assert(has_resolved(t));
+        }
+
+        fn atbinder_test_no_copy<X>(x: X, y: X) {
+            let t = (x, y);
+
+            match t {
+                x @ (_, _) => { consume(x); }
+            }
+
+            assert(has_resolved(t)); // FAILS
+        }
+
+        fn atbinder_test_option_copy<X: Copy>(x: X, y: X) {
+            let t = Some((x, y));
+
+            match t {
+                Some(x @ (_, _)) => { consume(x); }
+                None => { }
+            }
+
+            assert(has_resolved(t));
+        }
+
+        fn atbinder_test_option_no_copy<X>(x: X, y: X) {
+            let t = Some((x, y));
+
+            match t {
+                Some(x @ (_, _)) => { consume(x); }
+                None => { }
+            }
+
+            assert(has_resolved(t)); // FAILS
+        }
+
+        fn atbinder_test_let_copy<X: Copy>(x: X, y: X) {
+            let t = (x, y);
+
+            let x @ (_, _) = t;
+            consume(x);
+
+            assert(has_resolved(t));
+        }
+
+        fn atbinder_test_let_no_copy<X>(x: X, y: X) {
+            let t = (x, y);
+
+            let x @ (_, _) = t;
+            consume(x);
+
+            assert(has_resolved(t)); // FAILS
+        }
+    } => Err(err) => assert_fails(err, 6)
+}

source/vir/src/ast.rs

@@ -641,6 +641,9 @@ pub struct PatternBinding {
     pub by_ref: ByRef,
     pub typ: Typ,
     pub mutable: bool,
+    /// True if the type of this variable is copy.
+    /// This is used by resolution analysis; it is meaningless post-simplification.
+    pub copy: bool,
 }
 
 /// Patterns for match expressions

source/vir/src/ast_simplify.rs

@@ -264,6 +264,7 @@ fn pattern_to_decls_with_no_initializer(pattern: &Pattern, stmts: &mut Vec<Stmt>
                 mutable: binding.mutable,
                 by_ref: ByRef::No,
                 typ: binding.typ.clone(),
+                copy: false,
             });
             let v_pattern = SpannedTyped::new(&pattern.span, &binding.typ, v_patternx);
             stmts.push(Spanned::new(
@@ -711,9 +712,13 @@ fn tuple_get_field_expr(
 fn simplify_one_stmt(ctx: &GlobalCtx, state: &mut State, stmt: &Stmt) -> Result<Vec<Stmt>, VirErr> {
     match &stmt.x {
         StmtX::Decl { pattern, mode: _, init: None, els: None } => match &pattern.x {
-            PatternX::Var(PatternBinding { by_ref: ByRef::No, name: _, mutable: _, typ: _ }) => {
-                Ok(vec![stmt.clone()])
-            }
+            PatternX::Var(PatternBinding {
+                by_ref: ByRef::No,
+                name: _,
+                mutable: _,
+                typ: _,
+                copy: _,
+            }) => Ok(vec![stmt.clone()]),
             _ => {
                 let mut stmts: Vec<Stmt> = Vec::new();
                 pattern_to_decls_with_no_initializer(pattern, &mut stmts);
@@ -727,7 +732,13 @@ fn simplify_one_stmt(ctx: &GlobalCtx, state: &mut State, stmt: &Stmt) -> Result<
         StmtX::Decl { pattern, mode: _, init: Some(_init), els: None }
             if matches!(
                 pattern.x,
-                PatternX::Var(PatternBinding { by_ref: ByRef::No, name: _, mutable: _, typ: _ })
+                PatternX::Var(PatternBinding {
+                    by_ref: ByRef::No,
+                    name: _,
+                    mutable: _,
+                    typ: _,
+                    copy: _
+                })
             ) =>
         {
             Ok(vec![stmt.clone()])

source/vir/src/ast_to_sst.rs

@@ -2728,9 +2728,13 @@ fn stmt_to_stm(
                 panic!("let-else should be simplified in ast_simpllify {:?}.", stmt)
             }
             let (name, mutable, typ) = match &pattern.x {
-                PatternX::Var(PatternBinding { name, mutable, by_ref: ByRef::No, typ }) => {
-                    (name, mutable, typ)
-                }
+                PatternX::Var(PatternBinding {
+                    name,
+                    mutable,
+                    by_ref: ByRef::No,
+                    typ,
+                    copy: _,
+                }) => (name, mutable, typ),
                 _ => panic!("internal error: Decl should have been simplified by ast_simplify"),
             };
 

source/vir/src/ast_util.rs

@@ -1373,7 +1373,7 @@ fn place_to_expr_rec(place: &Place, loc: bool) -> Expr {
 
 impl PatternX {
     /// Returns a Pattern Var that is valid post-simplification.
-    pub fn simple_var(name: VarIdent, mutable: bool, span: &Span, typ: &Typ) -> Pattern {
+    pub(crate) fn simple_var(name: VarIdent, mutable: bool, span: &Span, typ: &Typ) -> Pattern {
         SpannedTyped::new(
             span,
             typ,
@@ -1382,6 +1382,7 @@ impl PatternX {
                 mutable,
                 by_ref: ByRef::No,
                 typ: typ.clone(),
+                copy: false,
             }),
         )
     }

source/vir/src/ast_visitor.rs

@@ -704,13 +704,14 @@ pub(crate) trait AstVisitor<R: Returner, Err, Scope: Scoper> {
         &mut self,
         pb: &PatternBinding,
     ) -> Result<R::Ret<PatternBinding>, Err> {
-        let PatternBinding { name, by_ref, typ, mutable } = pb;
+        let PatternBinding { name, by_ref, typ, mutable, copy } = pb;
         let typ = self.visit_typ(typ)?;
         R::ret(|| PatternBinding {
             name: name.clone(),
             by_ref: *by_ref,
             typ: R::get(typ),
             mutable: *mutable,
+            copy: *copy,
         })
     }
 
@@ -955,11 +956,11 @@ where
 fn insert_pattern_vars(map: &mut VisitorScopeMap, pattern: &Pattern, init: bool) {
     match &pattern.x {
         PatternX::Wildcard(_) => {}
-        PatternX::Var(PatternBinding { name, mutable, by_ref: _, typ }) => {
+        PatternX::Var(PatternBinding { name, mutable, by_ref: _, typ, copy: _ }) => {
             let _ = map.insert(name.clone(), ScopeEntry::new(typ, *mutable, init));
         }
         PatternX::Binding {
-            binding: PatternBinding { name, mutable, by_ref: _, typ },
+            binding: PatternBinding { name, mutable, by_ref: _, typ, copy: _ },
             sub_pat,
         } => {
             insert_pattern_vars(map, sub_pat, init);

source/vir/src/modes.rs

@@ -481,13 +481,13 @@ fn add_pattern_rec(
 
     match &pattern.x {
         PatternX::Wildcard(_dd) => Ok(()),
-        PatternX::Var(PatternBinding { name: x, mutable: _, by_ref: _, typ: _ }) => {
+        PatternX::Var(PatternBinding { name: x, mutable: _, by_ref: _, typ: _, copy: _ }) => {
             // TODO(new_mut_ref): disallow ByRef::Mut in spec code
             decls.push(PatternBoundDecl { span: pattern.span.clone(), name: x.clone(), mode });
             Ok(())
         }
         PatternX::Binding {
-            binding: PatternBinding { name: x, mutable: _, by_ref: _, typ: _ },
+            binding: PatternBinding { name: x, mutable: _, by_ref: _, typ: _, copy: _ },
             sub_pat,
         } => {
             add_pattern_rec(ctxt, record, typing, decls, mode, sub_pat, false)?;
@@ -1813,7 +1813,13 @@ fn check_stmt(
             // in Rust as "let xl; ... { let pat ... xl = xr; }".
             match (&pattern.x, init) {
                 (
-                    PatternX::Var(PatternBinding { name: x, mutable: _, by_ref: _, typ: _ }),
+                    PatternX::Var(PatternBinding {
+                        name: x,
+                        mutable: _,
+                        by_ref: _,
+                        typ: _,
+                        copy: _,
+                    }),
                     None,
                 ) => {
                     typing.insert_var_mode(x, VarMode::Infer(pattern.span.clone()));

source/vir/src/patterns.rs

@@ -198,13 +198,12 @@ fn pattern_to_exprs_rec(
     }
 }
 
-// TODO(new_mut_ref): account for Copy types
 pub(crate) fn pattern_has_move(pattern: &Pattern) -> bool {
     match &pattern.x {
         PatternX::Wildcard(_) => false,
-        PatternX::Var(binding) => matches!(binding.by_ref, ByRef::No),
+        PatternX::Var(binding) => !binding.copy && matches!(binding.by_ref, ByRef::No),
         PatternX::Binding { binding, sub_pat } => {
-            matches!(binding.by_ref, ByRef::No) || pattern_has_move(sub_pat)
+            (!binding.copy && matches!(binding.by_ref, ByRef::No)) || pattern_has_move(sub_pat)
         }
         PatternX::Constructor(_path, _variant, patterns) => {
             for binder in patterns.iter() {