mut_ref cleanup: remove is_mut params from VIR (#2407)

Author: tjhance

source/rust_verify/src/rust_to_vir_func.rs

@@ -170,12 +170,6 @@ fn handle_autospec<'tcx>(
 
         let mut spec_params = vec![];
         for p in functionx.params.iter() {
-            if p.x.is_mut {
-                return err_span(
-                    span,
-                    format!("allow_in_spec not supported for function with &mut param"),
-                );
-            }
             if p.x.unwrapped_info.is_some() {
                 return err_span(
                     span,
@@ -190,7 +184,6 @@ fn handle_autospec<'tcx>(
                     name: p.x.name.clone(),
                     typ: p.x.typ.clone(),
                     mode: Mode::Spec,
-                    is_mut: false,
                     unwrapped_info: None,
                     user_mut: false,
                 },
@@ -203,7 +196,6 @@ fn handle_autospec<'tcx>(
                 name: air_unique_var(RETURN_VALUE),
                 typ: ret_param.x.typ.clone(),
                 mode: Mode::Spec,
-                is_mut: false,
                 unwrapped_info: None,
                 user_mut: false,
             },
@@ -1708,7 +1700,6 @@ pub(crate) fn check_item_fn<'tcx>(
                 name: name.clone(),
                 typ: typ.clone(),
                 mode: param_mode,
-                is_mut: false,
                 unwrapped_info: None,
                 user_mut: is_mut_var,
             },
@@ -1906,7 +1897,6 @@ pub(crate) fn check_item_fn<'tcx>(
             name: ret_name.clone(),
             typ: ret_typ,
             mode: ret_mode,
-            is_mut: false,
             user_mut: false,
             unwrapped_info: None,
         },
@@ -1923,7 +1913,6 @@ pub(crate) fn check_item_fn<'tcx>(
                         .0
                         .clone(),
                     mode: ret_mode,
-                    is_mut: false,
                     unwrapped_info: None,
                     user_mut: false,
                 },
@@ -2340,7 +2329,6 @@ fn param_names_for_async_func<'tcx>(
                 name: async_body_modes[&param.x.name].clone(),
                 typ: param.x.typ.clone(),
                 mode: param.x.mode,
-                is_mut: param.x.is_mut,
                 unwrapped_info: param.x.unwrapped_info.clone(),
                 user_mut: param.x.user_mut,
             },
@@ -2431,10 +2419,6 @@ fn check_generics_for_invariant_fn<'tcx>(
     }
 }
 
-// &mut T => Some(T, None)
-// Ghost<&mut T> => Some(T, Some(Spec))
-// Tracked<&mut T> => Some(T, Some(Proof))
-// _ => None
 fn is_mut_ty<'tcx>(
     ctxt: &Context<'tcx>,
     ty: rustc_middle::ty::Ty<'tcx>,
@@ -2869,7 +2853,6 @@ pub(crate) fn check_item_const_or_static<'tcx>(
             name: ret_name,
             typ: typ.clone(),
             mode: ret_mode,
-            is_mut: false,
             user_mut: false,
             unwrapped_info: None,
         },
@@ -2995,20 +2978,11 @@ pub(crate) fn check_foreign_item_fn<'tcx>(
     assert!(idents.len() == inputs.len());
     for (param, input) in idents.iter().zip(inputs.iter()) {
         let name = no_body_param_to_var(param);
-        let is_mut = is_mut_ty(ctxt, *input);
-        let typ =
-            ctxt.mid_ty_to_vir(id, param.span, is_mut.map(|(t, _)| t).unwrap_or(input), None)?;
+        let typ = ctxt.mid_ty_to_vir(id, param.span, input, None)?;
         // REVIEW: the parameters don't have attributes, so we use the overall mode
         let vir_param = ctxt.spanned_new(
             param.span,
-            ParamX {
-                name,
-                typ,
-                mode,
-                is_mut: is_mut.is_some(),
-                unwrapped_info: None,
-                user_mut: false,
-            },
+            ParamX { name, typ, mode, unwrapped_info: None, user_mut: false },
         );
         vir_params.push(vir_param);
     }
@@ -3021,7 +2995,6 @@ pub(crate) fn check_foreign_item_fn<'tcx>(
         name: air_unique_var(RETURN_VALUE),
         typ: ret_typ,
         mode: ret_mode,
-        is_mut: false,
         user_mut: false,
         unwrapped_info: None,
     };

source/vir/src/ast.rs

@@ -1376,8 +1376,6 @@ pub struct ParamX {
     pub mode: Mode,
     /// Marked 'mut' at the source level?
     pub user_mut: bool,
-    /// An &mut parameter (only used outside new-mut-ref)
-    pub is_mut: bool,
     /// If the parameter uses a Ghost(x) or Tracked(x) pattern to unwrap the value, this is
     /// the mode of the resulting unwrapped x variable (Spec for Ghost(x), Proof for Tracked(x)).
     /// We also save a copy of the original wrapped name for lifetime_generate

source/vir/src/ast_simplify.rs

@@ -1197,7 +1197,6 @@ fn simplify_function(
             typ: Arc::new(TypX::Int(IntRange::Int)),
             mode: Mode::Spec,
             user_mut: false,
-            is_mut: false,
             unwrapped_info: None,
         };
         param_names.push(paramx.name.clone());

source/vir/src/ast_to_sst.rs

@@ -57,8 +57,6 @@ pub(crate) enum PreLocalDeclKind {
     ExecClosureParam,
     /// StmtLet (mutability to be inferred)
     StmtLet,
-    /// Param, always consider mut
-    MutParam,
 }
 
 #[derive(Clone)]
@@ -529,7 +527,6 @@ impl PreLocalDeclKind {
                 Ok(LocalDeclKind::ExecClosureParam { mutable: mutbl.is_some() })
             }
             PreLocalDeclKind::StmtLet => Ok(LocalDeclKind::StmtLet { mutable: mutbl.is_some() }),
-            PreLocalDeclKind::MutParam => Ok(LocalDeclKind::Param { mutable: true }),
         }
     }
 }

source/vir/src/ast_to_sst_func.rs

@@ -94,55 +94,28 @@ pub fn mk_fun_ctx<F: FunctionCommon>(
     mk_fun_ctx_dec(f, checking_spec_preconditions, false)
 }
 
-pub(crate) fn param_to_par(param: &Param, allow_is_mut: bool) -> Par {
+pub(crate) fn param_to_par(param: &Param) -> Par {
     param.map_x(|p| {
-        let ParamX { name, typ, mode, is_mut, user_mut: _, unwrapped_info: _ } = p;
-        if *is_mut && !allow_is_mut {
-            panic!("mut unexpected here");
-        }
-        ParX {
-            name: name.clone(),
-            typ: typ.clone(),
-            mode: *mode,
-            is_mut: *is_mut,
-            purpose: ParPurpose::Regular,
-        }
+        let ParamX { name, typ, mode, user_mut: _, unwrapped_info: _ } = p;
+        ParX { name: name.clone(), typ: typ.clone(), mode: *mode, purpose: ParPurpose::Regular }
     })
 }
 
-pub(crate) fn params_to_pars(params: &Params, allow_is_mut: bool) -> Pars {
-    Arc::new(vec_map(params, |p| param_to_par(p, allow_is_mut)))
+pub(crate) fn params_to_pars(params: &Params) -> Pars {
+    Arc::new(vec_map(params, |p| param_to_par(p)))
 }
 
-pub(crate) fn params_to_pre_post_pars(params: &Params, pre: bool) -> Pars {
+pub(crate) fn params_to_pre_post_pars(params: &Params) -> Pars {
     Arc::new(
         params
             .iter()
-            .flat_map(|param| {
-                let mut res = Vec::new();
-                if param.x.is_mut {
-                    res.push(param.map_x(|p| ParX {
-                        name: p.name.clone(),
-                        typ: p.typ.clone(),
-                        mode: p.mode,
-                        is_mut: p.is_mut,
-                        purpose: ParPurpose::MutPre,
-                    }));
-                }
-                if !(param.x.is_mut && pre) {
-                    res.push(param.map_x(|p| ParX {
-                        name: p.name.clone(),
-                        typ: p.typ.clone(),
-                        mode: p.mode,
-                        is_mut: p.is_mut,
-                        purpose: if param.x.is_mut {
-                            ParPurpose::MutPost
-                        } else {
-                            ParPurpose::Regular
-                        },
-                    }));
-                }
-                res
+            .map(|param| {
+                param.map_x(|p| ParX {
+                    name: p.name.clone(),
+                    typ: p.typ.clone(),
+                    mode: p.mode,
+                    purpose: ParPurpose::Regular,
+                })
             })
             .collect::<Vec<_>>(),
     )
@@ -155,7 +128,7 @@ fn func_body_to_sst(
     body: &Expr,
     verifying_owning_bucket: bool,
 ) -> Result<FuncSpecBodySst, VirErr> {
-    let pars = params_to_pars(&function.x.params, false);
+    let pars = params_to_pars(&function.x.params);
 
     // ast --> sst
     let mut state = State::new(diagnostics);
@@ -425,15 +398,14 @@ fn req_ens_to_sst(
     specs: &Vec<Expr>,
     pre: bool,
 ) -> Result<(Pars, Vec<Exp>), VirErr> {
-    let mut pars = params_to_pre_post_pars(&function.x.params, pre);
+    let mut pars = params_to_pre_post_pars(&function.x.params);
     let pars_mut = Arc::make_mut(&mut pars);
     if !pre && matches!(function.x.mode, Mode::Exec | Mode::Proof) && function.x.ens_has_return {
         if !function.x.attrs.is_async {
-            pars_mut.push(param_to_par(&function.x.ret, false));
+            pars_mut.push(param_to_par(&function.x.ret));
         } else {
             pars_mut.push(param_to_par(
                 &function.x.async_ret.as_ref().expect("Async function has no return type"),
-                false,
             ));
         }
     }
@@ -597,7 +569,7 @@ pub fn func_axioms_to_sst(
                 assert!(function.x.ensure.1.len() == 0);
                 let ens = crate::ast_util::conjoin(span, &*function.x.ensure.0);
                 let req_ens = crate::ast_util::mk_implies(span, &req, &ens);
-                let params = params_to_pre_post_pars(&function.x.params, false);
+                let params = params_to_pre_post_pars(&function.x.params);
                 // Use expr_to_bind_decls_exp_skip_checks, skipping checks on req_ens,
                 // because the requires/ensures are checked when the function itself is checked
                 let exp = expr_to_bind_decls_exp_skip_checks(ctx, diagnostics, &params, &req_ens)?;
@@ -864,15 +836,10 @@ pub fn func_def_to_sst(
         None
     };
     let ens_params = Arc::new(ens_params);
-    let ens_pars = params_to_pars(&ens_params, true);
+    let ens_pars = params_to_pars(&ens_params);
 
     for param in function.x.params.iter() {
-        state.declare_var_stm(
-            &param.x.name,
-            &param.x.typ,
-            if param.x.is_mut { PreLocalDeclKind::MutParam } else { PreLocalDeclKind::Param },
-            false,
-        );
+        state.declare_var_stm(&param.x.name, &param.x.typ, PreLocalDeclKind::Param, false);
     }
 
     // When emitting an expression that refers to input variables, but which is embedded
@@ -881,9 +848,7 @@ pub fn func_def_to_sst(
     // Collect all such vars here.
     let mut params_to_use_pre = HashSet::<VarIdent>::new();
     for param in function.x.params.iter() {
-        if !param.x.is_mut {
-            params_to_use_pre.insert(param.x.name.clone());
-        }
+        params_to_use_pre.insert(param.x.name.clone());
     }
     // We need to perform this translation on:
     //  - Postcondition
@@ -1140,8 +1105,8 @@ pub fn function_to_sst(
         opaqueness: function.x.opaqueness.clone(),
         typ_params: function.x.typ_params.clone(),
         typ_bounds: function.x.typ_bounds.clone(),
-        pars: params_to_pars(&function.x.params, true),
-        ret: param_to_par(&function.x.ret, true),
+        pars: params_to_pars(&function.x.params),
+        ret: param_to_par(&function.x.ret),
         ens_has_return: function.x.ens_has_return,
         item_kind: function.x.item_kind,
         attrs: function.x.attrs.clone(),
@@ -1152,7 +1117,7 @@ pub fn function_to_sst(
         recommends_check,
         safe_api_check,
         async_ret: match &function.x.async_ret {
-            Some(async_ret) => Some(param_to_par(async_ret, true)),
+            Some(async_ret) => Some(param_to_par(async_ret)),
             None => None,
         },
     };

source/vir/src/ast_util.rs

@@ -254,26 +254,9 @@ pub fn params_equal_opt(
     // the publicly visible parameters.
     // 'user_mut' also isn't important at this level since it is only used to determine
     // if mutation is allowed within the function
-    let ParamX {
-        name: name1,
-        typ: typ1,
-        mode: mode1,
-        is_mut: is_mut1,
-        unwrapped_info: _,
-        user_mut: _,
-    } = &param1.x;
-    let ParamX {
-        name: name2,
-        typ: typ2,
-        mode: mode2,
-        is_mut: is_mut2,
-        unwrapped_info: _,
-        user_mut: _,
-    } = &param2.x;
-    (!check_names || name1 == name2)
-        && types_equal(typ1, typ2)
-        && (!check_modes || mode1 == mode2)
-        && is_mut1 == is_mut2
+    let ParamX { name: name1, typ: typ1, mode: mode1, unwrapped_info: _, user_mut: _ } = &param1.x;
+    let ParamX { name: name2, typ: typ2, mode: mode2, unwrapped_info: _, user_mut: _ } = &param2.x;
+    (!check_names || name1 == name2) && types_equal(typ1, typ2) && (!check_modes || mode1 == mode2)
 }
 
 pub fn params_equal(param1: &Param, param2: &Param) -> bool {

source/vir/src/ast_visitor.rs

@@ -981,14 +981,13 @@ pub(crate) trait AstVisitor<R: Returner, Err, Scope: Scoper> {
     }
 
     fn visit_param(&mut self, param: &Param) -> Result<R::Ret<Param>, Err> {
-        let ParamX { name, typ, mode, is_mut, user_mut, unwrapped_info } = &param.x;
+        let ParamX { name, typ, mode, user_mut, unwrapped_info } = &param.x;
         let typ = self.visit_typ(typ)?;
         R::ret(|| {
             param.new_x(ParamX {
                 name: name.clone(),
                 typ: R::get(typ),
                 mode: *mode,
-                is_mut: *is_mut,
                 user_mut: *user_mut,
                 unwrapped_info: unwrapped_info.clone(),
             })

source/vir/src/datatype_to_air.rs

@@ -61,7 +61,6 @@ fn field_to_par(span: &Span, f: &Field) -> Par {
             name: crate::ast_util::str_unique_var(&("_".to_string() + &f.name), dis),
             typ: f.a.0.clone(),
             mode: f.a.1,
-            is_mut: false,
             purpose: ParPurpose::Regular,
         },
     )
@@ -185,7 +184,6 @@ fn datatype_or_fun_to_air_commands(
                 name: x.clone(),
                 typ: typ.clone(),
                 mode: Mode::Exec,
-                is_mut: false,
                 purpose: ParPurpose::Regular,
             },
         )
@@ -243,7 +241,6 @@ fn datatype_or_fun_to_air_commands(
                 name,
                 typ: vpolytyp.clone(),
                 mode: Mode::Exec,
-                is_mut: false,
                 purpose: ParPurpose::Regular,
             };
             params.push(Spanned::new(span.clone(), parx));