Improve documentation and naming schema

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -237,8 +237,10 @@ impl CodegenBackend for GotocCodegenBackend {
         let ret_val = rustc_internal::run(tcx, || {
             super::utils::init();
 
-            // Any changes to queries from this point on is just related to caching;
-            // the cached information will not outlive the stable-mir `run` scope.
+            // Any changes to queries from this point on is just related to caching information
+            // needed for generating code to the given crate.
+            // The cached information mut not outlive the stable-mir `run` scope.
+            // See [QueryDb::kani_functions] for more information.
             let queries = self.queries.lock().unwrap().clone();
 
             check_target(tcx.sess);

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -48,9 +48,12 @@ pub trait GotocHook {
 /// <https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0003-cover-statement.md>
 /// for more details.
 struct Cover;
+
+const UNEXPECTED_CALL: &str = "Hooks from kani library handled as a map";
+
 impl GotocHook for Cover {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -85,7 +88,7 @@ impl GotocHook for Cover {
 struct Assume;
 impl GotocHook for Assume {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -109,7 +112,7 @@ impl GotocHook for Assume {
 struct Assert;
 impl GotocHook for Assert {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -149,7 +152,7 @@ impl GotocHook for Assert {
 struct Check;
 impl GotocHook for Check {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -185,7 +188,7 @@ struct Nondet;
 
 impl GotocHook for Nondet {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -248,7 +251,7 @@ impl GotocHook for Panic {
 struct IsAllocated;
 impl GotocHook for IsAllocated {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -285,7 +288,7 @@ impl GotocHook for IsAllocated {
 struct PointerObject;
 impl GotocHook for PointerObject {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -321,7 +324,7 @@ impl GotocHook for PointerObject {
 struct PointerOffset;
 impl GotocHook for PointerOffset {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -467,7 +470,7 @@ struct UntrackedDeref;
 
 impl GotocHook for UntrackedDeref {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -515,7 +518,7 @@ struct InitContracts;
 /// ```
 impl GotocHook for InitContracts {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
-        unreachable!("Hooks from kani library handled as a map")
+        unreachable!("{UNEXPECTED_CALL}")
     }
 
     fn handle(
@@ -616,7 +619,7 @@ impl GotocHook for LoopInvariantRegister {
 }
 
 pub fn fn_hooks() -> GotocHooks {
-    let kani_hooks: [(KaniHook, Rc<dyn GotocHook>); 11] = [
+    let kani_lib_hooks: [(KaniHook, Rc<dyn GotocHook>); 11] = [
         (KaniHook::Assert, Rc::new(Assert)),
         (KaniHook::Assume, Rc::new(Assume)),
         (KaniHook::Panic, Rc::new(Panic)),
@@ -630,27 +633,31 @@ pub fn fn_hooks() -> GotocHooks {
         (KaniHook::InitContracts, Rc::new(InitContracts)),
     ];
     GotocHooks {
-        rustc_hooks: vec![
+        kani_lib_hooks: HashMap::from(kani_lib_hooks),
+        other_hooks: vec![
             Rc::new(Panic),
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(LoopInvariantRegister),
         ],
-        kani_hooks: HashMap::from(kani_hooks),
     }
 }
 
 pub struct GotocHooks {
-    rustc_hooks: Vec<Rc<dyn GotocHook>>,
-    kani_hooks: HashMap<KaniHook, Rc<dyn GotocHook>>,
+    /// Match functions that are unique and defined in the Kani library, which we can prefetch
+    /// using `KaniFunctions`.
+    kani_lib_hooks: HashMap<KaniHook, Rc<dyn GotocHook>>,
+    /// Match functions that are not defined in the Kani library, which we cannot prefetch
+    /// beforehand.
+    other_hooks: Vec<Rc<dyn GotocHook>>,
 }
 
 impl GotocHooks {
     pub fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> Option<Rc<dyn GotocHook>> {
         if let Ok(KaniFunction::Hook(hook)) = KaniFunction::try_from(instance) {
-            Some(self.kani_hooks[&hook].clone())
+            Some(self.kani_lib_hooks[&hook].clone())
         } else {
-            for h in &self.rustc_hooks {
+            for h in &self.other_hooks {
                 if h.hook_applies(tcx, instance) {
                     return Some(h.clone());
                 }

kani-compiler/src/kani_middle/attributes.rs

@@ -1067,6 +1067,7 @@ fn pretty_type_path(path: &TypePath) -> String {
     }
 }
 
+/// Retrieve the value of the `fn_marker` attribute for the given definition if it has one.
 pub(crate) fn fn_marker<T: CrateDef>(def: T) -> Option<String> {
     let fn_marker: [SymbolStable; 2] = ["kanitool".into(), "fn_marker".into()];
     let marker = def.attrs_by_path(&fn_marker).pop()?;

kani-compiler/src/kani_middle/kani_functions.rs

@@ -3,16 +3,16 @@
 //! This module contains code for handling special functions from the Kani library.
 //!
 //! There are three types of functions today:
-//!    1. Kani intrinsics: These are functions whose body is generated during
-//!       compilation time. Their body usually requires some extra knowledge about the given types
+//!    1. Kani intrinsics: These are functions whose MIR body is generated during compilation time.
+//!       Their body usually requires some extra knowledge about the given types
 //!       that's only available during compilation.
-//!    2. Kani models: These are functions that model a specific behavior but that cannot be used
-//!       directly by the user. For example, retrieving information about memory initialization.
-//!       Kani compiler determines when and where to use these models, but the logic itself is
-//!       encoded in Rust.
-//!    3. Kani hooks: These are similar to Kani intrinsics but their code generation depends
-//!       on some backend specific logic. From a Kani library perspective, there is no difference
-//!       between hooks and intrinsics.
+//!    2. Kani models: These are functions that model a specific behavior that is of interest of
+//!       the compiler. The body of the model is kept as is, and the compiler may invoke the model
+//!       to perform some operation, such as, retrieving information about memory initialization.
+//!    3. Kani hooks: These are similar to Kani intrinsics in a sense that their body will be
+//!       generated by the compiler. However, their body exposes some backend specific logic, thus,
+//!       their bodies are generated as part of the codegen stage.
+//!       From a Kani library perspective, there is no difference between hooks and intrinsics.
 //!       This is a compiler implementation detail, but for simplicity we use the "Hook" suffix
 //!       in their names.
 //!
@@ -214,6 +214,12 @@ pub fn find_kani_functions() -> HashMap<KaniFunction, FnDef> {
 }
 
 /// Ensure we have the valid definitions.
+///
+/// This is a utility function used to ensure that we have found all the expected functions, as well
+/// as to ensure that the cached IDs are up-to-date.
+///
+/// The second condition is to ensure the cached StableMIR `FnDef` objects are still valid, i.e.:,
+/// that we are not storing them past the StableMIR `run` context.
 pub fn validate_kani_functions(kani_funcs: &HashMap<KaniFunction, FnDef>) {
     let mut missing = 0u8;
     for func in KaniIntrinsic::iter()

kani-compiler/src/kani_queries/mod.rs

@@ -38,12 +38,21 @@ impl QueryDb {
     /// For `kani_core`, those definitions live in the `core` library.
     ///
     /// We cache these definitions to avoid doing the lookup every time it is needed.
-    /// The cache should be invalidated if the `stable_mir` context changes.
-    /// Since that doesn't occur today, we just run a sanity check to ensure all definitions
-    /// are still correct, and abort otherwise.
+    /// The cache should not be used after the `stable_mir` context ends.
+    /// For example, in the goto backend, we run the entire crate codegen under the same StableMIR
+    /// context, which is defined by the scope of the StableMIR `run` callback.
+    /// See the `codegen_crate` function in [crate::codegen_cprover_gotoc::compiler_interface].
+    /// It is OK to set the cache and use it inside the callback scope, however, the cache should
+    /// not be accessible after that.
+    ///
+    /// For that, users should create a new QueryDb that does not outlive the callback scope.
+    ///
+    /// To ensure we don't accidentally use the cache outside of the callback context, we run a
+    /// sanity check if we are reusing the cache.
     pub fn kani_functions(&self) -> &HashMap<KaniFunction, FnDef> {
         if let Some(kani_functions) = self.kani_functions.get() {
-            // Sanity check the values stored in case someone misused this API.
+            // Sanity check the values stored to ensure the cache is being within the StableMIR
+            // context used to populate the cache.
             validate_kani_functions(kani_functions);
             kani_functions
         } else {