Change reachability module to use StableMIR

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 were 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 instantiate all types and resolve 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 by 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 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)
 }