Validate function/method stubs (rust-lang#1920)

Author: aaronbembenek-aws

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -4,7 +4,7 @@
 //! This file contains the code necessary to interface with the compiler backend
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use crate::kani_middle::mir_transform;
+use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_closures_in_const_crate_items, filter_crate_items,
 };
@@ -58,11 +58,11 @@ impl CodegenBackend for GotocCodegenBackend {
     }
 
     fn provide(&self, providers: &mut Providers) {
-        mir_transform::provide(providers);
+        provide::provide(providers, &self.queries);
     }
 
     fn provide_extern(&self, providers: &mut ty::query::ExternProviders) {
-        mir_transform::provide_extern(providers);
+        provide::provide_extern(providers);
     }
 
     fn codegen_crate(

kani-compiler/src/kani_middle/mir_transform.rs

@@ -4,6 +4,6 @@
 //! and transformations.
 pub mod attributes;
 pub mod coercion;
-pub mod mir_transform;
+pub mod provide;
 pub mod reachability;
 pub mod stubbing;

kani-compiler/src/kani_middle/mod.rs

@@ -0,0 +1,74 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains an interface for setting custom query implementations
+//! to run during code generation. For example, this can be used to hook up
+//! custom MIR transformations.
+
+use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
+use crate::kani_middle::stubbing;
+use kani_queries::{QueryDb, UserInput};
+use rustc_hir::def_id::DefId;
+use rustc_interface;
+use rustc_middle::ty::query::query_stored::collect_and_partition_mono_items;
+use rustc_middle::{
+    mir::Body,
+    ty::{query::ExternProviders, query::Providers, TyCtxt},
+};
+
+/// Sets up rustc's query mechanism to apply Kani's custom queries to code from
+/// the present crate.
+pub fn provide(providers: &mut Providers, queries: &QueryDb) {
+    providers.optimized_mir = run_mir_passes::<false>;
+    if queries.get_stubbing_enabled() {
+        providers.collect_and_partition_mono_items = collect_and_partition_mono_items;
+    }
+}
+
+/// Sets up rustc's query mechanism to apply Kani's custom queries to code from
+/// external crates.
+pub fn provide_extern(providers: &mut ExternProviders) {
+    providers.optimized_mir = run_mir_passes::<true>;
+}
+
+/// Returns the optimized code for the function associated with `def_id` by
+/// running rustc's optimization passes followed by Kani-specific passes.
+fn run_mir_passes<'tcx, const EXTERN: bool>(tcx: TyCtxt<'tcx>, def_id: DefId) -> &Body<'tcx> {
+    tracing::debug!(?def_id, "Run rustc transformation passes");
+    let optimized_mir = if EXTERN {
+        rustc_interface::DEFAULT_EXTERN_QUERY_PROVIDERS.optimized_mir
+    } else {
+        rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir
+    };
+    let body = optimized_mir(tcx, def_id);
+
+    run_kani_mir_passes(tcx, def_id, body)
+}
+
+/// Returns the optimized code for the function associated with `def_id` by
+/// running Kani-specific passes. The argument `body` should be the optimized
+/// code rustc generates for this function.
+fn run_kani_mir_passes<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    def_id: DefId,
+    body: &'tcx Body<'tcx>,
+) -> &'tcx Body<'tcx> {
+    tracing::debug!(?def_id, "Run Kani transformation passes");
+    stubbing::transform(tcx, def_id, body)
+}
+
+/// Runs a reachability analysis before running the default
+/// `collect_and_partition_mono_items` query. The reachability analysis finds
+/// trait mismatches introduced by stubbing and performs a graceful exit in
+/// these cases. Left to its own devices, the default query panics.
+/// This is an issue when compiling a library, since the crate metadata is
+/// generated (using this query) before code generation begins (which is
+/// when we normally run the reachability analysis).
+fn collect_and_partition_mono_items(tcx: TyCtxt, key: ()) -> collect_and_partition_mono_items {
+    let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
+    let local_reachable = filter_crate_items(tcx, |_, def_id| {
+        tcx.is_reachable_non_generic(def_id) || entry_fn == Some(def_id)
+    });
+    // We do not actually need the value returned here.
+    collect_reachable_items(tcx, &local_reachable);
+    (rustc_interface::DEFAULT_QUERY_PROVIDERS.collect_and_partition_mono_items)(tcx, key)
+}

kani-compiler/src/kani_middle/provide.rs

@@ -33,6 +33,7 @@ use rustc_middle::ty::{
 };
 
 use crate::kani_middle::coercion;
+use crate::kani_middle::stubbing::get_stub_name;
 
 /// Collect all reachable items starting from the given starting points.
 pub fn collect_reachable_items<'tcx>(
@@ -45,6 +46,7 @@ pub fn collect_reachable_items<'tcx>(
     for item in starting_points {
         collector.collect(*item);
     }
+    tcx.sess.abort_if_errors();
 
     // Sort the result so code generation follows deterministic order.
     // This helps us to debug the code, but it also provides the user a good experience since the
@@ -396,15 +398,47 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
 
         let tcx = self.tcx;
         match terminator.kind {
-            TerminatorKind::Call { ref func, .. } => {
+            TerminatorKind::Call { ref func, ref args, .. } => {
                 let callee_ty = func.ty(self.body, tcx);
                 let fn_ty = self.monomorphize(callee_ty);
                 if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() {
-                    let instance =
+                    let instance_opt =
                         Instance::resolve(self.tcx, ParamEnv::reveal_all(), def_id, substs)
-                            .unwrap()
                             .unwrap();
-                    self.collect_instance(instance, true);
+                    match instance_opt {
+                        None => {
+                            let caller = tcx.def_path_str(self.instance.def_id());
+                            let callee = tcx.def_path_str(def_id);
+                            // Check if the current function has been stubbed.
+                            if let Some(stub) = get_stub_name(tcx, self.instance.def_id()) {
+                                // During the MIR stubbing transformation, we do not
+                                // force type variables in the stub's signature to
+                                // implement the same traits as those in the
+                                // original function/method. A trait mismatch shows
+                                // up here, when we try to resolve a trait method
+                                let generic_ty = args[0].ty(self.body, tcx).peel_refs();
+                                let receiver_ty = tcx.subst_and_normalize_erasing_regions(
+                                    substs,
+                                    ParamEnv::reveal_all(),
+                                    generic_ty,
+                                );
+                                let sep = callee.rfind("::").unwrap();
+                                let trait_ = &callee[..sep];
+                                tcx.sess.span_err(
+                                    terminator.source_info.span,
+                                    format!(
+                                        "`{receiver_ty}` doesn't implement \
+                                        `{trait_}`. The function `{caller}` \
+                                        cannot be stubbed by `{stub}` due to \
+                                        generic bounds not being met."
+                                    ),
+                                );
+                            } else {
+                                panic!("unable to resolve call to `{callee}` in `{caller}`")
+                            }
+                        }
+                        Some(instance) => self.collect_instance(instance, true),
+                    };
                 } else {
                     assert!(
                         matches!(fn_ty.kind(), TyKind::FnPtr(..)),

kani-compiler/src/kani_middle/reachability.rs

@@ -12,25 +12,107 @@ use rustc_data_structures::fx::FxHashMap;
 use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_middle::{mir::Body, ty::TyCtxt};
 
+/// Returns the name of the stub for the function/method identified by `def_id`,
+/// and `None` if the function/method is not stubbed.
+pub fn get_stub_name(tcx: TyCtxt, def_id: DefId) -> Option<String> {
+    let mapping = get_stub_mapping(tcx)?;
+    let name = tcx.def_path_str(def_id);
+    mapping.get(&name).map(String::clone)
+}
+
 /// Returns the new body of a function/method if it has been stubbed out;
-/// otherwise, returns `None`.
-pub fn transform(tcx: TyCtxt, def_id: DefId) -> Option<&Body> {
-    if let Some(mapping) = get_stub_mapping(tcx) {
-        let name = tcx.def_path_str(def_id);
-        if let Some(replacement) = mapping.get(&name) {
-            if let Some(replacement_id) = get_def_id(tcx, replacement) {
-                // TODO: We need to perform validation here (e.g., check that
-                // the replacement is compatible with the original function).
-                // <https://github.com/model-checking/kani/issues/1892>
-                let new_body = tcx.optimized_mir(replacement_id).clone();
-                return Some(tcx.arena.alloc(new_body));
+/// otherwise, returns the old body.
+pub fn transform<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    def_id: DefId,
+    old_body: &'tcx Body<'tcx>,
+) -> &'tcx Body<'tcx> {
+    if let Some(replacement) = get_stub_name(tcx, def_id) {
+        if let Some(replacement_id) = get_def_id(tcx, &replacement) {
+            let new_body = tcx.optimized_mir(replacement_id).clone();
+            if check_compatibility(tcx, def_id, old_body, replacement_id, &new_body) {
+                return tcx.arena.alloc(new_body);
+            }
+        } else {
+            tcx.sess
+                .span_err(tcx.def_span(def_id), format!("unable to find stub: `{}`", replacement));
+        };
+    }
+    old_body
+}
+
+/// Checks whether the stub is compatible with the original function/method: do
+/// the arities and types (of the parameters and return values) match up? This
+/// does **NOT** check whether the type variables are constrained to implement
+/// the same traits; trait mismatches are checked during monomorphization.
+fn check_compatibility<'a, 'tcx>(
+    tcx: TyCtxt,
+    old_def_id: DefId,
+    old_body: &'a Body<'tcx>,
+    stub_def_id: DefId,
+    stub_body: &'a Body<'tcx>,
+) -> bool {
+    // Check whether the arities match.
+    if old_body.arg_count != stub_body.arg_count {
+        tcx.sess.span_err(
+            tcx.def_span(stub_def_id),
+            format!(
+                "arity mismatch: original function/method `{}` takes {} argument(s), stub `{}` takes {}",
+                tcx.def_path_str(old_def_id),
+                old_body.arg_count,
+                tcx.def_path_str(stub_def_id),
+                stub_body.arg_count
+            ),
+        );
+        return false;
+    }
+    // Check whether the numbers of generic parameters match.
+    let old_num_generics = tcx.generics_of(old_def_id).count();
+    let stub_num_generics = tcx.generics_of(stub_def_id).count();
+    if old_num_generics != stub_num_generics {
+        tcx.sess.span_err(
+            tcx.def_span(stub_def_id),
+            format!(
+                "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}",
+                tcx.def_path_str(old_def_id),
+                old_num_generics,
+                tcx.def_path_str(stub_def_id),
+                stub_num_generics
+            ),
+        );
+        return false;
+    }
+    // Check whether the types match. Index 0 refers to the returned value,
+    // indices [1, `arg_count`] refer to the parameters.
+    // TODO: We currently force generic parameters in the stub to have exactly
+    // the same names as their counterparts in the original function/method;
+    // instead, we should be checking for the equivalence of types up to the
+    // renaming of generic parameters.
+    // <https://github.com/model-checking/kani/issues/1953>
+    let mut matches = true;
+    for i in 0..=old_body.arg_count {
+        let old_arg = old_body.local_decls.get(i.into()).unwrap();
+        let new_arg = stub_body.local_decls.get(i.into()).unwrap();
+        if old_arg.ty != new_arg.ty {
+            let prefix = if i == 0 {
+                "return type differs".to_string()
             } else {
-                tcx.sess
-                    .span_err(tcx.def_span(def_id), format!("Unable to find stub: {replacement}"));
+                format!("type of parameter {} differs", i - 1)
             };
+            tcx.sess.span_err(
+                new_arg.source_info.span,
+                format!(
+                    "{prefix}: stub `{}` has type `{}` where original function/method `{}` has type `{}`",
+                    tcx.def_path_str(stub_def_id),
+                    new_arg.ty,
+                    tcx.def_path_str(old_def_id),
+                    old_arg.ty
+                ),
+            );
+            matches = false;
         }
     }
-    None
+    matches
 }
 
 /// The prefix we will use when serializing the stub mapping as a rustc argument.

kani-compiler/src/kani_middle/stubbing/transform.rs

@@ -1,4 +1,4 @@
-error: Unable to find stub: other_crate::PubType::the_answer
-error: Unable to find stub: other_crate::PubType::the_answer
-error: Unable to find stub: other_crate::PrivType::the_answer
+error: unable to find stub: `other_crate::PubType::the_answer`
+error: unable to find stub: `other_crate::PubType::the_answer`
+error: unable to find stub: `other_crate::PrivType::the_answer`
 error: could not compile `foreign-function-stubbing` due to 3 previous errors

tests/cargo-kani/stubbing-foreign-method/expected

@@ -1,3 +1,3 @@
-error: Unable to find stub: other_crate::pub_mod::priv_mod::the_answer
-error: Unable to find stub: other_crate::the_answer
+error: unable to find stub: `other_crate::pub_mod::priv_mod::the_answer`
+error: unable to find stub: `other_crate::the_answer`
 error: could not compile `foreign-function-stubbing` due to 2 previous errors

tests/cargo-kani/stubbing-private-foreign-function/expected

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

tests/cargo-kani/stubbing-validate-random/Cargo.toml

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