Account for use statements when resolving paths in kani::stub attributes

kani-compiler/src/kani_middle/resolve.rs

@@ -10,8 +10,8 @@
 use std::collections::VecDeque;
 
 use rustc_hir::def::{DefKind, Res};
-use rustc_hir::def_id::{DefId, LocalDefId, CRATE_DEF_INDEX};
-use rustc_hir::ItemKind;
+use rustc_hir::def_id::{DefId, LocalDefId, CRATE_DEF_INDEX, LOCAL_CRATE};
+use rustc_hir::{ItemKind, UseKind};
 use rustc_middle::ty::TyCtxt;
 
 /// Attempts to resolve a simple path (in the form of a string) to a `DefId`.
@@ -196,12 +196,9 @@ fn resolve_in_foreign_module(
                     return resolve_in_foreign_module(tcx, inner_mod_id, segments);
                 }
             }
-            Res::Def(DefKind::Struct, type_id) | Res::Def(DefKind::Enum, type_id) => {
+            Res::Def(DefKind::Struct | DefKind::Enum | DefKind::Union, type_id) => {
                 if first == child.ident.as_str() && segments.len() == 2 {
-                    let maybe_resolved = resolve_in_inherent_impls(tcx, type_id, &segments[1]);
-                    if maybe_resolved.is_some() {
-                        return maybe_resolved;
-                    }
+                    return resolve_in_type(tcx, type_id, &segments[1]);
                 }
             }
             _ => {}
@@ -215,30 +212,34 @@ fn resolve_in_foreign_module(
     None
 }
 
+/// Generates a more friendly string representation of a local module's name
+/// (the default representation for the crate root is the empty string).
+fn module_to_string(tcx: TyCtxt, current_module: LocalDefId) -> String {
+    let def_id = current_module.to_def_id();
+    if def_id.is_crate_root() {
+        format!("module `{}`", tcx.crate_name(LOCAL_CRATE))
+    } else {
+        format!("module `{}`", tcx.def_path_str(def_id))
+    }
+}
+
 /// Resolves a path relative to a local module.
 fn resolve_relative(
     tcx: TyCtxt,
     current_module: LocalDefId,
     mut segments: Segments,
 ) -> Option<DefId> {
-    let current_module_string = || -> String {
-        let def_id = current_module.to_def_id();
-        if def_id.is_crate_root() {
-            "crate root".to_string()
-        } else {
-            format!("module `{}`", tcx.def_path_str(def_id))
-        }
-    };
     tracing::debug!(
         "Resolving `{}` in local {}",
         segments_to_string(&segments),
-        current_module_string()
+        module_to_string(tcx, current_module)
     );
 
     let first = segments.front().or_else(|| {
         tracing::debug!("Unable to resolve the empty path");
         None
     })?;
+    let mut glob_imports = Vec::new();
     for item_id in tcx.hir().module_items(current_module) {
         let item = tcx.hir().item(item_id);
         let def_id = item.owner_id.def_id.to_def_id();
@@ -247,7 +248,7 @@ fn resolve_relative(
                 if first == item.ident.as_str() && segments.len() == 1 {
                     tracing::debug!(
                         "Resolved `{first}` as a function in local {}",
-                        current_module_string()
+                        module_to_string(tcx, current_module)
                     );
                     return Some(def_id);
                 }
@@ -258,41 +259,139 @@ fn resolve_relative(
                     return resolve_relative(tcx, def_id.expect_local(), segments);
                 }
             }
-            ItemKind::Enum(..) | ItemKind::Struct(..) => {
+            ItemKind::Enum(..) | ItemKind::Struct(..) | ItemKind::Union(..) => {
                 if first == item.ident.as_str() && segments.len() == 2 {
-                    let maybe_resolved = resolve_in_inherent_impls(tcx, def_id, &segments[1]);
-                    if maybe_resolved.is_some() {
-                        return maybe_resolved;
+                    return resolve_in_type(tcx, def_id, &segments[1]);
+                }
+            }
+            ItemKind::Use(use_path, UseKind::Single) => {
+                if first == item.ident.as_str() {
+                    segments.pop_front();
+                    return resolve_in_use(tcx, use_path, segments);
+                }
+            }
+            ItemKind::Use(use_path, UseKind::Glob) => {
+                // Do not immediately try to resolve the path using this glob,
+                // since paths resolved via non-globs take precedence.
+                glob_imports.push(use_path);
+            }
+            ItemKind::ExternCrate(orig_name_opt) => {
+                if first == item.ident.as_str() {
+                    if let Some(orig_name) = orig_name_opt {
+                        segments[0] = orig_name.to_string();
                     }
+                    return resolve_external(tcx, segments);
                 }
             }
             _ => (),
         }
     }
 
-    tracing::debug!("Unable to resolve `{first}` as an item in local {}", current_module_string());
+    resolve_in_glob_uses(tcx, current_module, glob_imports, &segments).or_else(|| {
+        tracing::debug!(
+            "Unable to resolve `{first}` as an item in local {}",
+            module_to_string(tcx, current_module)
+        );
+        None
+    })
+}
+
+/// Resolves a path relative to a local or foreign module.
+fn resolve_in_module(tcx: TyCtxt, current_module: DefId, segments: Segments) -> Option<DefId> {
+    match current_module.as_local() {
+        None => resolve_in_foreign_module(tcx, current_module, segments),
+        Some(local_id) => resolve_relative(tcx, local_id, segments),
+    }
+}
+
+/// Resolves a path by exploring a non-glob use statement.
+fn resolve_in_use(tcx: TyCtxt, use_path: &rustc_hir::Path, segments: Segments) -> Option<DefId> {
+    if let Res::Def(def_kind, def_id) = use_path.res {
+        tracing::debug!(
+            "Resolving `{}` via `use` import of `{}`",
+            segments_to_string(&segments),
+            tcx.def_path_str(def_id)
+        );
+        match def_kind {
+            DefKind::Fn => {
+                if segments.is_empty() {
+                    tracing::debug!(
+                        "Resolved `{}` to a function via `use` import of `{}`",
+                        segments_to_string(&segments),
+                        tcx.def_path_str(def_id)
+                    );
+                    return Some(def_id);
+                }
+            }
+            DefKind::Mod => return resolve_in_module(tcx, def_id, segments),
+            DefKind::Struct | DefKind::Enum | DefKind::Union => {
+                if segments.len() == 1 {
+                    return resolve_in_type(tcx, def_id, &segments[0]);
+                }
+            }
+            _ => (),
+        }
+    }
+    tracing::debug!("Unable to resolve `{}` via `use` import", segments_to_string(&segments));
     None
 }
 
-/// Resolves a name in an `impl` block.
-fn resolve_in_impl(tcx: TyCtxt, impl_id: DefId, name: &str) -> Option<DefId> {
-    tracing::debug!("Resolving `{name}` in impl block `{}`", tcx.def_path_str(impl_id));
-    for assoc_item in tcx.associated_item_def_ids(impl_id) {
-        let item_path = tcx.def_path_str(*assoc_item);
-        let last = item_path.split("::").last().unwrap();
-        if last == name {
-            tracing::debug!("Resolved `{name}` in impl block `{}`", tcx.def_path_str(impl_id));
-            return Some(*assoc_item);
+/// Resolves a path by exploring glob use statements.
+fn resolve_in_glob_uses(
+    tcx: TyCtxt,
+    current_module: LocalDefId,
+    glob_imports: Vec<&rustc_hir::Path>,
+    segments: &Segments,
+) -> Option<DefId> {
+    let glob_resolves = glob_imports
+        .iter()
+        .filter_map(|use_path| {
+            let span = tracing::span!(tracing::Level::DEBUG, "glob_resolution");
+            let _enter = span.enter();
+            resolve_in_glob_use(tcx, use_path, segments.clone())
+        })
+        .collect::<Vec<_>>();
+    if glob_resolves.len() == 1 {
+        return glob_resolves.first().copied();
+    }
+    if glob_resolves.len() > 1 {
+        // Raise an error if it's ambiguous which glob import a function comes
+        // from. rustc will also raise an error in this case if the ambiguous
+        // function is present in code (and not just as an attribute argument).
+        // TODO: We should make this consistent with error handling for other
+        // cases (see <https://github.com/model-checking/kani/issues/2013>).
+        let location = module_to_string(tcx, current_module);
+        let mut msg = format!(
+            "glob imports in local {location} make it impossible to \
+            unambiguously resolve path; the possibilities are:"
+        );
+        for def_id in glob_resolves {
+            msg.push_str("\n\t");
+            msg.push_str(&tcx.def_path_str(def_id));
         }
+        tcx.sess.err(msg);
     }
-    tracing::debug!("Unable to resolve `{name}` in impl block `{}`", tcx.def_path_str(impl_id));
     None
 }
 
-/// Resolves a name in the inherent `impl` blocks of a type (i.e., non-trait
-/// `impl`s).
-fn resolve_in_inherent_impls(tcx: TyCtxt, type_id: DefId, name: &str) -> Option<DefId> {
+/// Resolves a path by exploring a glob use statement.
+fn resolve_in_glob_use(
+    tcx: TyCtxt,
+    use_path: &rustc_hir::Path,
+    segments: Segments,
+) -> Option<DefId> {
+    if let Res::Def(DefKind::Mod, def_id) = use_path.res {
+        resolve_in_module(tcx, def_id, segments)
+    } else {
+        None
+    }
+}
+
+/// Resolves a method in a type. It currently does not resolve trait methods
+/// (see <https://github.com/model-checking/kani/issues/1997>).
+fn resolve_in_type(tcx: TyCtxt, type_id: DefId, name: &str) -> Option<DefId> {
     tracing::debug!("Resolving `{name}` in type `{}`", tcx.def_path_str(type_id));
+    // Try the inherent `impl` blocks (i.e., non-trait `impl`s).
     for impl_ in tcx.inherent_impls(type_id) {
         let maybe_resolved = resolve_in_impl(tcx, *impl_, name);
         if maybe_resolved.is_some() {
@@ -303,6 +402,21 @@ fn resolve_in_inherent_impls(tcx: TyCtxt, type_id: DefId, name: &str) -> Option<
     None
 }
 
+/// Resolves a name in an `impl` block.
+fn resolve_in_impl(tcx: TyCtxt, impl_id: DefId, name: &str) -> Option<DefId> {
+    tracing::debug!("Resolving `{name}` in impl block `{}`", tcx.def_path_str(impl_id));
+    for assoc_item in tcx.associated_item_def_ids(impl_id) {
+        let item_path = tcx.def_path_str(*assoc_item);
+        let last = item_path.split("::").last().unwrap();
+        if last == name {
+            tracing::debug!("Resolved `{name}` in impl block `{}`", tcx.def_path_str(impl_id));
+            return Some(*assoc_item);
+        }
+    }
+    tracing::debug!("Unable to resolve `{name}` in impl block `{}`", tcx.def_path_str(impl_id));
+    None
+}
+
 /// Does the current module have a (direct) submodule with the given name?
 fn has_submodule_with_name(tcx: TyCtxt, current_module: LocalDefId, name: &str) -> bool {
     for item_id in tcx.hir().module_items(current_module) {

tests/cargo-kani/stubbing-do-not-resolve/other_crate1/src/lib.rs

@@ -1,4 +1,4 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-fn mock() {}
+pub fn mock() {}

tests/cargo-kani/stubbing-do-not-resolve/other_crate2/src/lib.rs

@@ -1,4 +1,4 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-fn mock() {}
+pub fn mock() {}

tests/cargo-kani/stubbing-do-not-resolve/src/lib.rs

@@ -6,8 +6,11 @@
 //! matches the name of a local module -- to external functions that match that
 //! path.
 
-use other_crate1;
-use other_crate2;
+// Pull these crates into the compiler.
+mod ignore_me {
+    use other_crate1;
+    use other_crate2;
+}
 
 mod my_mod {
 

tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml

@@ -0,0 +1,14 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "stubbing-do-not-resolve"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+other_crate = { path = "other_crate" }
+
+[package.metadata.kani]
+flags = { enable-unstable=true, enable-stubbing=true }

tests/cargo-kani/stubbing-resolve-extern-crate-as/harness.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/stubbing-resolve-extern-crate-as/other_crate/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "other_crate"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/cargo-kani/stubbing-resolve-extern-crate-as/other_crate/src/lib.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn magic_number13() -> u32 {
+    13
+}
+
+pub mod inner_mod {
+    pub fn magic_number42() -> u32 {
+        42
+    }
+}
+
+pub struct MyType {}
+
+impl MyType {
+    pub fn magic_number101() -> u32 {
+        101
+    }
+}

tests/cargo-kani/stubbing-resolve-extern-crate-as/src/lib.rs

@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This tests whether we take into account `extern crate XXX as YYY;`
+//! statements when resolving paths in `kani::stub` attributes.
+
+extern crate other_crate as foo;
+
+#[kani::proof]
+#[kani::stub(zero, foo::magic_number13)]
+#[kani::stub(one, foo::inner_mod::magic_number42)]
+#[kani::stub(two, foo::MyType::magic_number101)]
+fn harness() {
+    assert_eq!(zero(), foo::magic_number13());
+    assert_eq!(one(), foo::inner_mod::magic_number42());
+    assert_eq!(two(), foo::MyType::magic_number101());
+}
+
+fn zero() -> u32 {
+    0
+}
+
+fn one() -> u32 {
+    1
+}
+
+fn two() -> u32 {
+    2
+}

tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "stubbing-use-as-foreign"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+other_crate = { path = "other_crate" }
+
+[package.metadata.kani]
+flags = { enable-unstable=true, enable-stubbing=true }

tests/cargo-kani/stubbing-use-as-foreign/harness.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/stubbing-use-as-foreign/other_crate/Cargo.toml

@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "other_crate"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]