Create kani_middle module to host backend agnostic code (#1833)

For now I just moved the reachability code to this new module. As a follow up PR, I am planning to move the unsized coercion related code into a separate module so it can be used to refactor and fix codegen casting logic (related issues #1531, #566, and #1528) .

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -3,8 +3,8 @@
 
 //! This file contains the code necessary to interface with the compiler backend
 
-use crate::codegen_cprover_gotoc::reachability::{collect_reachable_items, filter_crate_items};
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use bitflags::_core::any::Any;
 use cbmc::goto_program::{symtab_transformer, Location};
 use cbmc::{InternedString, MachineModel};

kani-compiler/src/codegen_cprover_gotoc/mod.rs

@@ -5,7 +5,6 @@ mod codegen;
 mod compiler_interface;
 mod context;
 mod overrides;
-mod reachability;
 mod utils;
 
 pub use compiler_interface::GotocCodegenBackend;

kani-compiler/src/kani_middle/mod.rs

@@ -0,0 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains code that are backend agnostic. For example, MIR analysis
+//! and transformations.
+pub mod reachability;

kani-compiler/src/main.rs

@@ -28,6 +28,7 @@ extern crate rustc_target;
 
 #[cfg(feature = "cprover")]
 mod codegen_cprover_gotoc;
+mod kani_middle;
 mod parser;
 mod session;
 mod unsound_experiments;