make trait method resolution more exhaustive, fixes #1312 (#1341)

verus-lang · Dec 3, 2024 · 893e0c2 · 893e0c2
1 parent 12b857f
commit 893e0c2
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 10 deletions.
diff --git a/source/rust_verify/src/fn_call_to_vir.rs b/source/rust_verify/src/fn_call_to_vir.rs
@@ -22,7 +22,7 @@ use air::ast_util::str_ident;
 use rustc_ast::LitKind;
 use rustc_hir::def::Res;
 use rustc_hir::{Expr, ExprKind, Node, QPath};
-use rustc_middle::ty::{GenericArg, GenericArgKind, TyKind};
+use rustc_middle::ty::{GenericArg, GenericArgKind, Instance, InstanceDef, TyKind};
 use rustc_span::def_id::DefId;
 use rustc_span::source_map::Spanned;
 use rustc_span::Span;
@@ -193,13 +193,15 @@ pub(crate) fn fn_call_to_vir<'tcx>(
     let target_kind = if tcx.trait_of_item(f).is_none() {
         vir::ast::CallTargetKind::Static
     } else {
-        let mut target_kind = vir::ast::CallTargetKind::Dynamic;
         let param_env = tcx.param_env(bctx.fun_id);
         let normalized_substs = tcx.normalize_erasing_regions(param_env, node_substs);
-        let inst = rustc_middle::ty::Instance::resolve(tcx, param_env, f, normalized_substs);
-        if let Ok(Some(inst)) = inst {
-            if let rustc_middle::ty::InstanceDef::Item(did) = inst.def {
-                let typs = mk_typ_args(bctx, &inst.args, did, expr.span)?;
+        let inst = Instance::resolve(tcx, param_env, f, normalized_substs);
+        let Ok(inst) = inst else {
+            return err_span(expr.span, "Verus internal error: Instance::resolve");
+        };
+        match inst {
+            Some(Instance { def: InstanceDef::Item(did), args }) => {
+                let typs = mk_typ_args(bctx, args, did, expr.span)?;
                 let mut f =
                     Arc::new(FunX { path: def_id_to_vir_path(tcx, &bctx.ctxt.verus_items, did) });
                 record_name = f.clone();
@@ -214,7 +216,7 @@ pub(crate) fn fn_call_to_vir<'tcx>(
                     is_trait_default = true;
                     remove_self_trait_bound = Some((trait_id, &mut self_trait_impl_path));
                 }
-                let impl_paths = get_impl_paths(bctx, did, &inst.args, remove_self_trait_bound);
+                let impl_paths = get_impl_paths(bctx, did, args, remove_self_trait_bound);
                 if tcx.trait_of_item(did).is_some() {
                     if let Some(vir::ast::ImplPath::TraitImplPath(impl_path)) = self_trait_impl_path
                     {
@@ -226,15 +228,21 @@ pub(crate) fn fn_call_to_vir<'tcx>(
                         );
                     }
                 }
-                target_kind = vir::ast::CallTargetKind::DynamicResolved {
+                vir::ast::CallTargetKind::DynamicResolved {
                     resolved: f,
                     typs,
                     impl_paths,
                     is_trait_default,
-                };
+                }
+            }
+            Some(inst) => {
+                unsupported_err!(expr.span, format!("instance {:?}", &inst.def));
+            }
+            None => {
+                // Method is generic
+                vir::ast::CallTargetKind::Dynamic
             }
         }
-        target_kind
     };
 
     record_call(bctx, expr, ResolvedCall::Call(record_name, autospec_usage));

diff --git a/source/rust_verify_test/tests/std.rs b/source/rust_verify_test/tests/std.rs
@@ -490,3 +490,14 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_fails(err, 2)
 }
+
+test_verify_one_file! {
+    #[test] tuple_clone_not_supported verus_code! {
+        use vstd::*;
+
+        fn stuff(a: (u8, u8)) {
+            let b = a.clone();
+            assert(a == b); // FAILS
+        }
+    } => Err(err) => assert_vir_error_msg(err, "The verifier does not yet support the following Rust feature: instance")
+}