Change reachability module to use StableMIR (#2894)

Rewrite the reachability module to use Stable APIs wherever possible.
Note that in StableMIR the instance body is already monomorphized and
constants are already evaluated, which simplifies the code for most of
it, except to handle stubbing issue #2589.

For the stubbing issue, we still use a mix of stable and internal APIs
to detect an invalid monomorphization.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

docs/src/dev-documentation.md

@@ -14,6 +14,7 @@ developers (including external contributors):
  3. [Development setup recommendations for working with `cbmc`](./cbmc-hacks.md).
  4. [Development setup recommendations for working with `rustc`](./rustc-hacks.md).
  5. [Guide for testing in Kani](./testing.md).
+ 6. [Transition to StableMIR](./stable_mir.md).
 
 > **NOTE**: The developer documentation is intended for Kani developers and not
 users. At present, the project is under heavy development and some items

docs/src/stable_mir.md

@@ -0,0 +1,94 @@
+# Transition to StableMIR
+
+We have partnered with the Rust compiler team in the initiative to introduce stable
+APIs to the compiler that can be used by third-party tools, which is known as the
+[Stable MIR Project](https://github.com/rust-lang/project-stable-mir), or just StableMIR.
+This means that we are starting to use the new APIs introduced by this project as is,
+despite them not being stable yet.
+
+### StableMIR APIs
+
+For now, the StableMIR APIs are exposed as a crate in the compiler named `stable_mir`.
+This crate includes the definition of structures and methods to be stabilized,
+which are expected to become the stable APIs in the compiler.
+To reduce the migration burden, these APIs are somewhat close to the original compiler interfaces.
+However, some changes have been made to make these APIs cleaner and easier to use.
+
+For example:
+1. The usage of the compiler context (aka `TyCtxt`) is transparent to the user.
+   The StableMIR implementation caches this context in a thread local variable,
+   and retrieves it whenever necessary.
+    - Because of that, code that uses the StableMIR has to be invoked inside a `run` call.
+2. The `DefId` has been specialized into multiple types,
+   making its usage less error prone. E.g.:
+   `FnDef` represents the definition of a function,
+   while `StaticDef` is the definition of a static variable.
+   - Note that the same `DefId` may be mapped to different definitions according to its context.
+     For example, an `InstanceDef` and a `FnDef` may represent the same function definition.
+3. Methods that used to be exposed as part of `TyCtxt` are now part of a type.
+   Example, the function `TyCtxt.instance_mir` is now `Instance::body`.
+4. There is no need for explicit instantiation (monomorphization) of items from an`Instance::body`.
+   This method already instantiates all types and resolves all constants before converting
+   it to stable APIs.
+
+
+### Performance
+
+Since the new APIs require converting internal data to a stable representation,
+the APIs were also designed to avoid needless conversions,
+and to allow extra information to be retrieved on demand.
+
+For example, `Ty` is just an identifier, while `TyKind` is a structure that can be retrieved via `Ty::kind` method.
+The `TyKind` is a more structured object, thus,
+it is only generated when the `kind` method is invoked.
+Since this translation is not cached,
+many of the functions that the rust compiler used to expose in `Ty`,
+is now only part of `TyKind`.
+The reason being that there is no cache for the `TyKind`,
+and users should do the caching themselves to avoid needless translations.
+
+From our initial experiments with the transition of the reachability algorithm to use StableMIR,
+there is a small penalty of using StableMIR over internal rust compiler APIs.
+However, they are still fairly efficient and it did not impact the overall compilation time.
+
+### Interface with internal APIs
+
+To reduce the burden of migrating to StableMIR,
+and to allow StableMIR to be used together with internal APIs,
+there are two helpful methods to convert StableMIR constructs to internal rustc and back:
+  - `rustc_internal::internal()`: Convert a Stable item into an internal one.
+  - `rustc_internal::stable()`: Convert an internal item into a Stable one.
+
+Both of these methods are inside `rustc_smir` crate in the `rustc_internal`
+module inside the compiler.
+Note that there is no plan to stabilize any of these methods,
+and there's also no guarantee on its support and coverage.
+
+The conversion is not implemented for all items, and some conversions may be incomplete.
+Please proceed with caution when using these methods.
+
+Besides that, do not invoke any other `rustc_smir` methods, except for `run`.
+This crate's methods are not meant to be invoked externally.
+Note that, the method `run` will also eventually be replaced by a Stable driver.
+
+### Creating and modifying StableMIR items
+
+For now, StableMIR should only be used to get information from the compiler.
+Do not try to create or modify items directly, as it may not work.
+This may result in incorrect behavior or an internal compiler error (ICE).
+
+## Naming conventions in Kani
+
+As we adopt StableMIR, we would like to introduce a few conventions to make it easier to maintain the code.
+Whenever there is a name conflict, for example, `Ty` or `codegen_ty`,
+use a suffix to indicate which API you are using.
+`Stable` for StableMIR and `Internal` for `rustc` internal APIs.
+
+A module should either default its naming to Stable APIs or Internal APIs.
+I.e.: Modules that have been migrated to StableMIR don't need to add the `Stable` suffix to stable items.
+While those that haven't been migrated, should add `Stable`, but no `Internal` is needed.
+
+For example, the `codegen::typ` module will likely include methods:
+
+`codegen_ty(&mut self, Ty)` and `codegen_ty_stable(&mut, TyStable)` to handle
+internal and stable APIs.

kani-compiler/src/kani_compiler.rs

@@ -34,6 +34,7 @@ use rustc_hir::definitions::DefPathHash;
 use rustc_interface::Config;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::{ErrorOutputType, OutputType};
+use rustc_smir::rustc_internal;
 use rustc_span::ErrorGuaranteed;
 use std::collections::{BTreeMap, HashMap};
 use std::fs::File;
@@ -400,9 +401,12 @@ impl Callbacks for KaniCompiler {
     ) -> Compilation {
         if self.stage.is_init() {
             self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| {
-                check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm);
-                self.process_harnesses(tcx)
-            });
+                rustc_internal::run(tcx, || {
+                    check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm);
+                    self.process_harnesses(tcx)
+                })
+                .unwrap()
+            })
         }
 
         self.prepare_codegen()

kani-compiler/src/kani_middle/provide.rs

@@ -76,11 +76,14 @@ fn collect_and_partition_mono_items(
     tcx: TyCtxt,
     key: (),
 ) -> queries::collect_and_partition_mono_items::ProvidedValue {
-    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_smir::rustc_internal::run(tcx, || {
+        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);
+    })
+    .unwrap();
     (rustc_interface::DEFAULT_QUERY_PROVIDERS.collect_and_partition_mono_items)(tcx, key)
 }