handle impl function with different param names than the trait fn dec…

…laration

fixes #278

source/rust_verify_test/tests/regression.rs

@@ -281,23 +281,6 @@ test_verify_one_file! {
     } => Err(err) => assert_vir_error_msg(err, "cannot call function with mode spec")
 }
 
-test_verify_one_file! {
-    #[ignore] #[test] trait_argument_names_issue278 verus_code! {
-        trait T {
-            fn f(&self, a: usize) -> (res: usize)
-                ensures res == a;
-        }
-
-        struct S { }
-
-        impl T for S {
-            fn f(&self, b: usize) -> usize {
-                b
-            }
-        }
-    } => Ok(())
-}
-
 test_verify_one_file! {
     #[test] reveal_non_opaque_issue236_1 verus_code! {
         spec fn is_true(a: bool) -> bool { a }

source/rust_verify_test/tests/traits.rs

@@ -1866,3 +1866,54 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] trait_argument_names_issue278_1 verus_code! {
+        trait T {
+            fn f(&self, a: usize) -> (res: usize)
+                ensures res == a;
+        }
+
+        struct S { }
+
+        impl T for S {
+            fn f(&self, b: usize) -> usize {
+                b
+            }
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] trait_argument_names_issue278_2 verus_code! {
+        trait T {
+            fn f(&self, a: usize) -> (res: usize)
+                ensures res == a;
+        }
+
+        struct S { }
+
+        impl T for S {
+            fn f(&self, b: usize) -> (result: usize) {
+                b
+            }
+        }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] trait_argument_names_issue278_3 verus_code! {
+        trait T {
+            fn f(&self, a: usize) -> (res: usize)
+                ensures res == a; // FAILS
+        }
+
+        struct S { }
+
+        impl T for S {
+            fn f(&self, b: usize) -> (result: usize) {
+                0
+            }
+        }
+    } => Err(err) => assert_one_fails(err)
+}

source/vir/src/func_to_air.rs

@@ -3,6 +3,7 @@ use crate::ast::{
     TypX, Typs, VirErr,
 };
 use crate::ast_util::QUANT_FORALL;
+use crate::ast_visitor;
 use crate::context::Ctx;
 use crate::def::{
     new_internal_qid, prefix_ensures, prefix_fuel_id, prefix_fuel_nat, prefix_pre_var,
@@ -761,12 +762,24 @@ pub fn func_def_to_air(
                 state.declare_new_var(&param.x.name, &param.x.typ, param.x.is_mut, false);
             }
 
+            let req_ens_e_rename: HashMap<_, _> = req_ens_function
+                .x
+                .params
+                .iter()
+                .zip(function.x.params.iter())
+                .map(|(p1, p2)| (p1.x.name.clone(), p2.x.name.clone()))
+                .collect();
+
             let mut req_stms: Vec<Stm> = Vec::new();
             let mut reqs: Vec<Exp> = Vec::new();
             for e in req_ens_function.x.require.iter() {
+                let e_with_req_ens_params = map_expr_rename_vars(e, &req_ens_e_rename)?;
                 if ctx.checking_recommends() {
-                    let (stms, exp) =
-                        crate::ast_to_sst::expr_to_pure_exp_check(ctx, &mut state, e)?;
+                    let (stms, exp) = crate::ast_to_sst::expr_to_pure_exp_check(
+                        ctx,
+                        &mut state,
+                        &e_with_req_ens_params,
+                    )?;
                     req_stms.extend(stms);
                     req_stms.push(Spanned::new(exp.span.clone(), StmX::Assume(exp)));
                 } else {
@@ -775,23 +788,27 @@ pub fn func_def_to_air(
                         diagnostics,
                         &state.fun_ssts,
                         &req_pars,
-                        e,
+                        &e_with_req_ens_params,
                     )?);
                 }
             }
             let mut ens_recommend_stms: Vec<Stm> = Vec::new();
             let mut enss: Vec<Exp> = Vec::new();
             for e in req_ens_function.x.ensure.iter() {
+                let e_with_req_ens_params = map_expr_rename_vars(e, &req_ens_e_rename)?;
                 if ctx.checking_recommends() {
-                    ens_recommend_stms
-                        .extend(crate::ast_to_sst::check_pure_expr(ctx, &mut state, e)?);
+                    ens_recommend_stms.extend(crate::ast_to_sst::check_pure_expr(
+                        ctx,
+                        &mut state,
+                        &e_with_req_ens_params,
+                    )?);
                 } else {
                     enss.push(crate::ast_to_sst::expr_to_exp(
                         ctx,
                         diagnostics,
                         &state.fun_ssts,
                         &ens_pars,
-                        e,
+                        &e_with_req_ens_params,
                     )?);
                 }
             }
@@ -887,3 +904,31 @@ pub fn func_def_to_air(
         }
     }
 }
+
+fn map_expr_rename_vars(
+    e: &Arc<SpannedTyped<crate::ast::ExprX>>,
+    req_ens_e_rename: &HashMap<Arc<String>, Arc<String>>,
+) -> Result<Arc<SpannedTyped<crate::ast::ExprX>>, Arc<air::messages::MessageX>> {
+    ast_visitor::map_expr_visitor_env(
+        e,
+        &mut air::scope_map::ScopeMap::new(),
+        &mut (),
+        &|_state, _, expr| {
+            use crate::ast::ExprX;
+            Ok(match &expr.x {
+                ExprX::Var(i) => {
+                    expr.new_x(ExprX::Var(req_ens_e_rename.get(i).unwrap_or(i).clone()))
+                }
+                ExprX::VarLoc(i) => {
+                    expr.new_x(ExprX::VarLoc(req_ens_e_rename.get(i).unwrap_or(i).clone()))
+                }
+                ExprX::VarAt(i, at) => {
+                    expr.new_x(ExprX::VarAt(req_ens_e_rename.get(i).unwrap_or(i).clone(), *at))
+                }
+                _ => expr.clone(),
+            })
+        },
+        &|_state, _, stmt| Ok(vec![stmt.clone()]),
+        &|_state, typ| Ok(typ.clone()),
+    )
+}