From f8ba4577bfe4828fdc3a4565a9d2cb25d1615950 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Tue, 28 May 2024 00:26:03 +0200
Subject: [PATCH] chore(rr_rustc_interface): Remove crate own import

---
 rr_frontend/Cargo.lock                        |  1 +
 rr_frontend/attribute_parse/Cargo.toml        |  2 +
 rr_frontend/attribute_parse/src/lib.rs        |  4 -
 rr_frontend/attribute_parse/src/parse.rs      |  6 +-
 rr_frontend/clippy.toml                       | 41 ++++----
 .../src/bin/refinedrust-rustc.rs              | 42 ++++-----
 rr_frontend/rr_rustc_interface/src/lib.rs     | 18 ++--
 rr_frontend/translation/src/arg_folder.rs     | 16 ++--
 rr_frontend/translation/src/base.rs           |  6 +-
 .../translation/src/checked_op_analysis.rs    |  6 +-
 rr_frontend/translation/src/data.rs           |  2 +-
 .../src/environment/borrowck/facts.rs         | 11 ++-
 .../src/environment/borrowck/place_regions.rs |  2 +-
 .../collect_closure_defs_visitor.rs           | 10 +-
 .../collect_prusti_spec_visitor.rs            | 10 +-
 .../src/environment/dump_borrowck_info.rs     | 17 ++--
 .../translation/src/environment/loops.rs      | 13 ++-
 .../src/environment/mir_storage.rs            |  6 +-
 .../src/environment/mir_utils/all_places.rs   |  2 +-
 .../src/environment/mir_utils/args_for_mir.rs |  4 +-
 .../src/environment/mir_utils/mir_place.rs    |  2 +-
 .../src/environment/mir_utils/real_edges.rs   |  4 +-
 .../mir_utils/split_aggregate_assignment.rs   |  2 +-
 .../mir_utils/statement_as_assign.rs          |  2 +-
 .../src/environment/mir_utils/statement_at.rs |  2 +-
 .../mir_utils/tuple_items_for_ty.rs           |  2 +-
 .../src/environment/mir_utils/ty_as_ty_ref.rs |  4 +-
 .../translation/src/environment/mod.rs        | 19 ++--
 .../src/environment/polonius_info.rs          | 19 ++--
 .../translation/src/environment/procedure.rs  |  6 +-
 rr_frontend/translation/src/function_body.rs  | 31 ++++---
 rr_frontend/translation/src/lib.rs            | 31 ++-----
 .../src/spec_parsers/const_attr_parser.rs     |  4 +-
 .../src/spec_parsers/crate_attr_parser.rs     |  2 +-
 .../src/spec_parsers/enum_spec_parser.rs      |  2 +-
 .../translation/src/spec_parsers/mod.rs       |  2 +-
 .../src/spec_parsers/module_attr_parser.rs    |  4 +-
 .../src/spec_parsers/struct_spec_parser.rs    |  2 +-
 .../verbose_function_spec_parser.rs           |  4 +-
 rr_frontend/translation/src/traits.rs         | 23 ++---
 .../translation/src/type_translator.rs        | 93 ++++++++++---------
 rr_frontend/translation/src/tyvars.rs         |  4 +-
 rr_frontend/translation/src/utils.rs          | 30 +++---
 43 files changed, 244 insertions(+), 269 deletions(-)

diff --git a/rr_frontend/Cargo.lock b/rr_frontend/Cargo.lock
index cc48a06b..e5d11b89 100644
--- a/rr_frontend/Cargo.lock
+++ b/rr_frontend/Cargo.lock
@@ -93,6 +93,7 @@ dependencies = [
 name = "attribute_parse"
 version = "0.1.0"
 dependencies = [
+ "rr_rustc_interface",
  "unicode-xid",
 ]
 
diff --git a/rr_frontend/attribute_parse/Cargo.toml b/rr_frontend/attribute_parse/Cargo.toml
index 2d16da2c..130a24f2 100644
--- a/rr_frontend/attribute_parse/Cargo.toml
+++ b/rr_frontend/attribute_parse/Cargo.toml
@@ -8,6 +8,8 @@ repository.workspace = true
 version.workspace = true
 
 [dependencies]
+rr_rustc_interface.workspace = true
+
 unicode-xid.workspace = true
 
 [package.metadata.rust-analyzer]
diff --git a/rr_frontend/attribute_parse/src/lib.rs b/rr_frontend/attribute_parse/src/lib.rs
index 5ab46321..a39dba2a 100644
--- a/rr_frontend/attribute_parse/src/lib.rs
+++ b/rr_frontend/attribute_parse/src/lib.rs
@@ -1,7 +1,3 @@
 #![feature(rustc_private)]
 
-extern crate rustc_ast;
-extern crate rustc_driver;
-extern crate rustc_span;
-
 pub mod parse;
diff --git a/rr_frontend/attribute_parse/src/parse.rs b/rr_frontend/attribute_parse/src/parse.rs
index 65d38643..db0f78f8 100644
--- a/rr_frontend/attribute_parse/src/parse.rs
+++ b/rr_frontend/attribute_parse/src/parse.rs
@@ -29,9 +29,9 @@ use std::cell::Cell;
 use std::str::FromStr;
 use std::{fmt, result, vec};
 
-use rustc_ast::token::{BinOpToken, Lit, LitKind, TokenKind};
-use rustc_ast::tokenstream::{DelimSpan, TokenStream, TokenTree};
-use rustc_span::{Span, Symbol};
+use rr_rustc_interface::ast::token::{BinOpToken, Lit, LitKind, TokenKind};
+use rr_rustc_interface::ast::tokenstream::{DelimSpan, TokenStream, TokenTree};
+use rr_rustc_interface::span::{Span, Symbol};
 use unicode_xid::UnicodeXID;
 
 pub trait IntoSpans<S> {
diff --git a/rr_frontend/clippy.toml b/rr_frontend/clippy.toml
index 7b76b745..4b380a1d 100644
--- a/rr_frontend/clippy.toml
+++ b/rr_frontend/clippy.toml
@@ -1,28 +1,27 @@
 absolute-paths-allowed-crates = [
-  "hir",
   "polonius_engine",
   "radium",
   "rrconfig",
-  "rustc_abi",
-  "rustc_ast",
-  "rustc_ast",
-  "rustc_attr",
-  "rustc_borrowck",
-  "rustc_borrowck",
-  "rustc_data_structures",
-  "rustc_driver",
-  "rustc_errors",
-  "rustc_hir",
-  "rustc_index",
-  "rustc_infer",
-  "rustc_interface",
-  "rustc_middle",
-  "rustc_session",
-  "rustc_span",
-  "rustc_target",
-  "rustc_trait_selection",
-  "rustc_type_ir",
-  "serde_json"
+
+  # rustc
+  "abi",
+  "ast",
+  "attr",
+  "borrowck",
+  "data_structures",
+  "driver",
+  "errors",
+  "hir",
+  "index",
+  "infer",
+  "interface",
+  "middle",
+  "serde_json",
+  "session",
+  "span",
+  "target",
+  "trait_selection",
+  "type_ir"
 ]
 
 avoid-breaking-exported-api = false
diff --git a/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs b/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
index d84d10eb..291983a7 100644
--- a/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
+++ b/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
@@ -7,25 +7,19 @@
 
 #![feature(box_patterns)]
 #![feature(rustc_private)]
-extern crate rustc_borrowck;
-extern crate rustc_driver;
-extern crate rustc_hir;
-extern crate rustc_interface;
-extern crate rustc_middle;
-extern crate rustc_session;
-
 use std::path::PathBuf;
 use std::process::Command;
 use std::{env, process};
 
 use log::{debug, info};
-use rustc_driver::Compilation;
-use rustc_hir::def_id::LocalDefId;
-use rustc_interface::Config;
-use rustc_middle::query::queries::mir_borrowck;
-use rustc_middle::query::{ExternProviders, Providers};
-use rustc_middle::ty::TyCtxt;
-use rustc_session::Session;
+use rr_rustc_interface::driver::Compilation;
+use rr_rustc_interface::hir::def_id::LocalDefId;
+use rr_rustc_interface::interface::Config;
+use rr_rustc_interface::middle::query::queries::mir_borrowck;
+use rr_rustc_interface::middle::query::{ExternProviders, Providers};
+use rr_rustc_interface::middle::ty::TyCtxt;
+use rr_rustc_interface::session::Session;
+use rr_rustc_interface::{borrowck, driver, interface};
 use translation::environment::mir_storage;
 
 const BUG_REPORT_URL: &str = "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev/-/issues/new";
@@ -45,10 +39,10 @@ struct RRCompilerCalls;
 
 // From Prusti.
 fn mir_borrowck(tcx: TyCtxt<'_>, def_id: LocalDefId) -> mir_borrowck::ProvidedValue<'_> {
-    let body_with_facts = rustc_borrowck::consumers::get_body_with_borrowck_facts(
+    let body_with_facts = borrowck::consumers::get_body_with_borrowck_facts(
         tcx,
         def_id,
-        rustc_borrowck::consumers::ConsumerOptions::PoloniusOutputFacts,
+        borrowck::consumers::ConsumerOptions::PoloniusOutputFacts,
     );
     // SAFETY: This is safe because we are feeding in the same `tcx` that is
     // going to be used as a witness when pulling out the data.
@@ -56,7 +50,7 @@ fn mir_borrowck(tcx: TyCtxt<'_>, def_id: LocalDefId) -> mir_borrowck::ProvidedVa
         mir_storage::store_mir_body(tcx, def_id, body_with_facts);
     }
     let mut providers = Providers::default();
-    rustc_borrowck::provide(&mut providers);
+    borrowck::provide(&mut providers);
     let original_mir_borrowck = providers.mir_borrowck;
     original_mir_borrowck(tcx, def_id)
 }
@@ -113,7 +107,7 @@ pub fn analyze(tcx: TyCtxt<'_>) {
     }
 }
 
-impl rustc_driver::Callbacks for RRCompilerCalls {
+impl driver::Callbacks for RRCompilerCalls {
     fn config(&mut self, config: &mut Config) {
         assert!(config.override_queries.is_none());
         if !rrconfig::no_verify() {
@@ -123,8 +117,8 @@ impl rustc_driver::Callbacks for RRCompilerCalls {
 
     fn after_analysis<'tcx>(
         &mut self,
-        _: &rustc_interface::interface::Compiler,
-        queries: &'tcx rustc_interface::Queries<'tcx>,
+        _: &interface::interface::Compiler,
+        queries: &'tcx interface::Queries<'tcx>,
     ) -> Compilation {
         if rrconfig::no_verify() {
             // TODO: We also need this to properly compile deps.
@@ -142,11 +136,11 @@ impl rustc_driver::Callbacks for RRCompilerCalls {
 }
 
 fn main() {
-    rustc_driver::install_ice_hook(BUG_REPORT_URL, |_handler| ());
+    driver::install_ice_hook(BUG_REPORT_URL, |_handler| ());
 
     // If we should act like rustc, just run the main function of the driver
     if rrconfig::be_rustc() {
-        rustc_driver::main();
+        driver::main();
     }
 
     // otherwise, initialize our loggers
@@ -195,7 +189,7 @@ fn main() {
     }
     debug!("rustc arguments: {:?}", rustc_args);
 
-    let exit_code = rustc_driver::catch_with_exit_code(move || {
+    let exit_code = driver::catch_with_exit_code(move || {
         if rustc_args.get(1) == Some(&"-vV".to_owned()) {
             // When cargo queries the verbose rustc version,
             // also print the RR version to stdout.
@@ -243,7 +237,7 @@ fn main() {
 
         let mut callbacks = RRCompilerCalls {};
 
-        rustc_driver::RunCompiler::new(&rustc_args, &mut callbacks).run()
+        driver::RunCompiler::new(&rustc_args, &mut callbacks).run()
     });
 
     process::exit(exit_code)
diff --git a/rr_frontend/rr_rustc_interface/src/lib.rs b/rr_frontend/rr_rustc_interface/src/lib.rs
index 53cee0cf..f93222c3 100644
--- a/rr_frontend/rr_rustc_interface/src/lib.rs
+++ b/rr_frontend/rr_rustc_interface/src/lib.rs
@@ -11,23 +11,17 @@ pub extern crate polonius_engine as polonius_engine;
 pub extern crate rustc_abi as abi;
 pub extern crate rustc_ast as ast;
 pub extern crate rustc_attr as attr;
+pub extern crate rustc_borrowck as borrowck;
 pub extern crate rustc_data_structures as data_structures;
 pub extern crate rustc_driver as driver;
-pub extern crate rustc_errors as errors;
-//pub extern crate rustc_errors as errors;
-//pub extern crate rustc_index as index;
+pub extern crate rustc_hash as hash;
+pub extern crate rustc_hir as hir;
+pub extern crate rustc_index as index;
 pub extern crate rustc_infer as infer;
 pub extern crate rustc_interface as interface;
+pub extern crate rustc_middle as middle;
 pub extern crate rustc_session as session;
 pub extern crate rustc_span as span;
 pub extern crate rustc_target as target;
-
-// TODO use smir instead
-pub extern crate rustc_borrowck as borrowck;
-pub extern crate rustc_hir as hir;
-pub extern crate rustc_middle as middle;
-pub extern crate rustc_mir_dataflow as dataflow;
 pub extern crate rustc_trait_selection as trait_selection;
-
-//pub extern crate rustc_smir;
-//pub use rustc_smir::very_unstable::{borrowck, dataflow, hir, middle, trait_selection};
+pub extern crate rustc_type_ir as type_ir;
diff --git a/rr_frontend/translation/src/arg_folder.rs b/rr_frontend/translation/src/arg_folder.rs
index ad18e0f9..691b4484 100644
--- a/rr_frontend/translation/src/arg_folder.rs
+++ b/rr_frontend/translation/src/arg_folder.rs
@@ -1,10 +1,12 @@
-use rustc_middle::ty::visit::*;
-use rustc_middle::ty::{self, Binder, GenericArg, GenericArgKind, ParamConst, Ty, TyCtxt, TypeFolder};
-use rustc_type_ir::fold::{TypeFoldable, TypeSuperFoldable};
-use rustc_type_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitor};
-
-/// A version of the `ArgFolder` in `rustc_middle::src::ty::generic_args` that skips over `ReVar`
-/// (instead of triggering a bug).
+use rr_rustc_interface::middle::ty::visit::*;
+use rr_rustc_interface::middle::ty::{
+    self, Binder, GenericArg, GenericArgKind, ParamConst, Ty, TyCtxt, TypeFolder,
+};
+use rr_rustc_interface::type_ir::fold::{TypeFoldable, TypeSuperFoldable};
+use rr_rustc_interface::type_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitor};
+
+/// A version of the `ArgFolder` in `rr_rustc_interface::middle::src::ty::generic_args` that skips over
+/// `ReVar` (instead of triggering a bug).
 
 struct ArgFolder<'a, 'tcx> {
     tcx: TyCtxt<'tcx>,
diff --git a/rr_frontend/translation/src/base.rs b/rr_frontend/translation/src/base.rs
index 41d19f04..6aa4a5b4 100644
--- a/rr_frontend/translation/src/base.rs
+++ b/rr_frontend/translation/src/base.rs
@@ -4,9 +4,9 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-use polonius_engine::FactTypes;
-use rustc_borrowck::consumers::RustcFacts;
-use rustc_middle::mir::Location;
+use rr_rustc_interface::borrowck::consumers::RustcFacts;
+use rr_rustc_interface::middle::mir::Location;
+use rr_rustc_interface::polonius_engine::FactTypes;
 
 pub type Region = <RustcFacts as FactTypes>::Origin;
 pub type Loan = <RustcFacts as FactTypes>::Loan;
diff --git a/rr_frontend/translation/src/checked_op_analysis.rs b/rr_frontend/translation/src/checked_op_analysis.rs
index c88841c0..7d65da01 100644
--- a/rr_frontend/translation/src/checked_op_analysis.rs
+++ b/rr_frontend/translation/src/checked_op_analysis.rs
@@ -6,11 +6,11 @@
 
 use std::collections::{HashMap, HashSet};
 
-use rustc_middle::mir::tcx::PlaceTy;
-use rustc_middle::mir::{
+use rr_rustc_interface::middle::mir::tcx::PlaceTy;
+use rr_rustc_interface::middle::mir::{
     BasicBlock, BasicBlockData, Body, Local, Place, Rvalue, StatementKind, TerminatorKind,
 };
-use rustc_middle::ty::{Ty, TyCtxt};
+use rr_rustc_interface::middle::ty::{Ty, TyCtxt};
 
 /// Analysis for determining which locals are the temporaries used as the result of a checked-op.
 pub struct CheckedOpLocalAnalysis<'def, 'tcx> {
diff --git a/rr_frontend/translation/src/data.rs b/rr_frontend/translation/src/data.rs
index 6dc198fb..e79a0f85 100644
--- a/rr_frontend/translation/src/data.rs
+++ b/rr_frontend/translation/src/data.rs
@@ -7,7 +7,7 @@
 //! This module defines data structures exchanged between a verifier and
 //! its environment.
 
-use rustc_hir::def_id::DefId;
+use rr_rustc_interface::hir::def_id::DefId;
 
 /// A unique identifier of the Rust procedure.
 pub type ProcedureDefId = DefId;
diff --git a/rr_frontend/translation/src/environment/borrowck/facts.rs b/rr_frontend/translation/src/environment/borrowck/facts.rs
index b7354e52..4bd305d1 100644
--- a/rr_frontend/translation/src/environment/borrowck/facts.rs
+++ b/rr_frontend/translation/src/environment/borrowck/facts.rs
@@ -8,9 +8,10 @@ use std::cell::RefCell;
 use std::rc::Rc;
 use std::{cmp, fmt};
 
-use polonius_engine::FactTypes;
-use rustc_borrowck::consumers::{LocationTable, RichLocation, RustcFacts};
-use rustc_middle::mir;
+use rr_rustc_interface::borrowck;
+use rr_rustc_interface::borrowck::consumers::{LocationTable, RichLocation, RustcFacts};
+use rr_rustc_interface::middle::mir;
+use rr_rustc_interface::polonius_engine::FactTypes;
 
 pub type Region = <RustcFacts as FactTypes>::Origin;
 pub type Loan = <RustcFacts as FactTypes>::Loan;
@@ -18,8 +19,8 @@ pub type PointIndex = <RustcFacts as FactTypes>::Point;
 pub type Variable = <RustcFacts as FactTypes>::Variable;
 pub type Path = <RustcFacts as FactTypes>::Path;
 
-pub type AllInput = rustc_borrowck::consumers::PoloniusInput;
-pub type AllOutput = rustc_borrowck::consumers::PoloniusOutput;
+pub type AllInput = borrowck::consumers::PoloniusInput;
+pub type AllOutput = borrowck::consumers::PoloniusOutput;
 
 trait LocationTableExt {
     fn to_mir_location(self, point: PointIndex) -> mir::Location;
diff --git a/rr_frontend/translation/src/environment/borrowck/place_regions.rs b/rr_frontend/translation/src/environment/borrowck/place_regions.rs
index 018207af..73e99bf6 100644
--- a/rr_frontend/translation/src/environment/borrowck/place_regions.rs
+++ b/rr_frontend/translation/src/environment/borrowck/place_regions.rs
@@ -10,7 +10,7 @@ use std::collections::HashMap;
 use std::io;
 
 use log::{debug, trace};
-use rustc_middle::{mir, ty};
+use rr_rustc_interface::middle::{mir, ty};
 
 use crate::environment::borrowck::facts;
 
diff --git a/rr_frontend/translation/src/environment/collect_closure_defs_visitor.rs b/rr_frontend/translation/src/environment/collect_closure_defs_visitor.rs
index 3e3884a7..0f1a636e 100644
--- a/rr_frontend/translation/src/environment/collect_closure_defs_visitor.rs
+++ b/rr_frontend/translation/src/environment/collect_closure_defs_visitor.rs
@@ -1,9 +1,9 @@
 use log::trace;
-use rustc_hir as hir;
-use rustc_hir::def_id::LocalDefId;
-use rustc_hir::intravisit::{walk_expr, Visitor};
-use rustc_middle::hir::map::Map;
-use rustc_middle::hir::nested_filter::OnlyBodies;
+use rr_rustc_interface::hir;
+use rr_rustc_interface::hir::def_id::LocalDefId;
+use rr_rustc_interface::hir::intravisit::{walk_expr, Visitor};
+use rr_rustc_interface::middle::hir::map::Map;
+use rr_rustc_interface::middle::hir::nested_filter::OnlyBodies;
 
 use crate::environment::Environment;
 
diff --git a/rr_frontend/translation/src/environment/collect_prusti_spec_visitor.rs b/rr_frontend/translation/src/environment/collect_prusti_spec_visitor.rs
index 5d30586b..e8b884c8 100644
--- a/rr_frontend/translation/src/environment/collect_prusti_spec_visitor.rs
+++ b/rr_frontend/translation/src/environment/collect_prusti_spec_visitor.rs
@@ -5,10 +5,10 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 use log::trace;
-use rr_rustc_interface::hir;
-use rustc_hir::def_id::LocalDefId;
-use rustc_hir::intravisit::Visitor;
-use rustc_middle::ty::TyCtxt;
+use rr_rustc_interface::hir::def_id::LocalDefId;
+use rr_rustc_interface::hir::intravisit::Visitor;
+use rr_rustc_interface::middle::ty::TyCtxt;
+use rr_rustc_interface::{hir, middle};
 
 use crate::environment::Environment;
 
@@ -39,7 +39,7 @@ impl<'a, 'tcx> CollectPrustiSpecVisitor<'a, 'tcx> {
 
     pub fn run(&mut self) {
         //self.tcx.hir().visit_all_item_likes_in_crate
-        let it: &rustc_middle::hir::ModuleItems = self.tcx.hir_crate_items(());
+        let it: &middle::hir::ModuleItems = self.tcx.hir_crate_items(());
         for id in it.items() {
             self.visit_item(self.tcx.hir().item(id));
         }
diff --git a/rr_frontend/translation/src/environment/dump_borrowck_info.rs b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
index d694f888..a85be689 100644
--- a/rr_frontend/translation/src/environment/dump_borrowck_info.rs
+++ b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
@@ -11,11 +11,12 @@ use std::path::PathBuf;
 use std::{cell, fs, io};
 
 use log::{debug, trace};
-use rustc_hash::FxHashMap;
-use rustc_index::Idx;
-use rustc_middle::mir;
-use rustc_middle::ty::TyCtxt;
-use {rrconfig as config, rustc_hir as hir};
+use rr_rustc_interface::hash::FxHashMap;
+use rr_rustc_interface::index::Idx;
+use rr_rustc_interface::middle::mir;
+use rr_rustc_interface::middle::ty::TyCtxt;
+use rr_rustc_interface::{hir, middle};
+use rrconfig as config;
 
 use crate::data::ProcedureDefId;
 use crate::environment::borrowck::facts;
@@ -23,7 +24,7 @@ use crate::environment::mir_analyses::initialization::{
     compute_definitely_initialized, DefinitelyInitializedAnalysisResult,
 };
 use crate::environment::mir_utils::real_edges::RealEdges;
-use crate::environment::polonius_info::PoloniusInfo;
+use crate::environment::polonius_info::{graphviz, PoloniusInfo};
 use crate::environment::procedure::Procedure;
 use crate::environment::{loops, Environment};
 
@@ -217,7 +218,7 @@ impl<'a, 'tcx: 'a> InfoPrinter<'a, 'tcx> {
         //let loop_invariant_block = HashMap::new();
 
         // print polonius.dot
-        crate::environment::polonius_info::graphviz(self.env, &def_path, def_id, info).unwrap();
+        graphviz(self.env, &def_path, def_id, info).unwrap();
 
         // print graph.dot
         let mir_info_printer = MirInfoPrinter {
@@ -781,7 +782,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
     }
 
     fn visit_terminator(&self, bb: mir::BasicBlock, terminator: &mir::Terminator) -> Result<(), io::Error> {
-        use rustc_middle::mir::TerminatorKind;
+        use middle::mir::TerminatorKind;
         match &terminator.kind {
             TerminatorKind::Goto { target } => {
                 write_edge!(self, bb, target);
diff --git a/rr_frontend/translation/src/environment/loops.rs b/rr_frontend/translation/src/environment/loops.rs
index 2e759037..87a9882c 100644
--- a/rr_frontend/translation/src/environment/loops.rs
+++ b/rr_frontend/translation/src/environment/loops.rs
@@ -7,10 +7,11 @@
 use std::collections::{HashMap, HashSet};
 
 use log::{debug, info, trace};
-use rustc_data_structures::graph::dominators::{dominators, Dominators};
-use rustc_index::{Idx, IndexVec};
-use rustc_middle::mir;
-use rustc_middle::mir::visit::{PlaceContext, Visitor};
+use rr_rustc_interface::data_structures::graph::dominators::{dominators, Dominators};
+use rr_rustc_interface::index::{Idx, IndexVec};
+use rr_rustc_interface::middle;
+use rr_rustc_interface::middle::mir;
+use rr_rustc_interface::middle::mir::visit::{PlaceContext, Visitor};
 
 use crate::environment::mir_sets::place_set::PlaceSet;
 use crate::environment::mir_utils::real_edges::RealEdges;
@@ -378,9 +379,7 @@ impl ProcedureLoops {
     }
 
     #[must_use]
-    pub const fn get_back_edges(
-        &self,
-    ) -> &HashSet<(rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlock)> {
+    pub const fn get_back_edges(&self) -> &HashSet<(middle::mir::BasicBlock, middle::mir::BasicBlock)> {
         &self.back_edges
     }
 
diff --git a/rr_frontend/translation/src/environment/mir_storage.rs b/rr_frontend/translation/src/environment/mir_storage.rs
index 1a6d8e81..262dc8db 100644
--- a/rr_frontend/translation/src/environment/mir_storage.rs
+++ b/rr_frontend/translation/src/environment/mir_storage.rs
@@ -16,9 +16,9 @@ use std::cell::RefCell;
 use std::collections::HashMap;
 use std::{mem, thread_local};
 
-use rustc_borrowck::consumers::BodyWithBorrowckFacts;
-use rustc_hir::def_id::LocalDefId;
-use rustc_middle::ty::TyCtxt;
+use rr_rustc_interface::borrowck::consumers::BodyWithBorrowckFacts;
+use rr_rustc_interface::hir::def_id::LocalDefId;
+use rr_rustc_interface::middle::ty::TyCtxt;
 
 thread_local! {
     pub static SHARED_STATE:
diff --git a/rr_frontend/translation/src/environment/mir_utils/all_places.rs b/rr_frontend/translation/src/environment/mir_utils/all_places.rs
index 797e36c7..80b79619 100644
--- a/rr_frontend/translation/src/environment/mir_utils/all_places.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/all_places.rs
@@ -4,7 +4,7 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_middle::{mir, ty};
+use rr_rustc_interface::middle::{mir, ty};
 
 pub trait AllPlaces<'tcx> {
     /// Returns all places that are below the given local variable. Right now, this only handles
diff --git a/rr_frontend/translation/src/environment/mir_utils/args_for_mir.rs b/rr_frontend/translation/src/environment/mir_utils/args_for_mir.rs
index 3fae65bf..bc96700a 100644
--- a/rr_frontend/translation/src/environment/mir_utils/args_for_mir.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/args_for_mir.rs
@@ -4,8 +4,8 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_index::Idx;
-use rustc_middle::{mir, ty};
+use rr_rustc_interface::index::Idx;
+use rr_rustc_interface::middle::{mir, ty};
 
 pub trait ArgsForMir<'tcx> {
     fn get_args(&self) -> Vec<(mir::Local, ty::Ty<'tcx>)>;
diff --git a/rr_frontend/translation/src/environment/mir_utils/mir_place.rs b/rr_frontend/translation/src/environment/mir_utils/mir_place.rs
index 39780ff8..20aa6ea6 100644
--- a/rr_frontend/translation/src/environment/mir_utils/mir_place.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/mir_place.rs
@@ -4,7 +4,7 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_middle::mir;
+use rr_rustc_interface::middle::mir;
 
 #[derive(Clone, Eq, PartialEq, Hash, Debug)]
 pub struct MirPlace<'tcx> {
diff --git a/rr_frontend/translation/src/environment/mir_utils/real_edges.rs b/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
index a853c155..051484ca 100644
--- a/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
@@ -4,8 +4,8 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_index::IndexVec;
-use rustc_middle::mir::{self, TerminatorKind};
+use rr_rustc_interface::index::IndexVec;
+use rr_rustc_interface::middle::mir::{self, TerminatorKind};
 
 /// A data structure to store the non-virtual CFG edges of a MIR body.
 pub struct RealEdges {
diff --git a/rr_frontend/translation/src/environment/mir_utils/split_aggregate_assignment.rs b/rr_frontend/translation/src/environment/mir_utils/split_aggregate_assignment.rs
index dfef3b83..4ee10054 100644
--- a/rr_frontend/translation/src/environment/mir_utils/split_aggregate_assignment.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/split_aggregate_assignment.rs
@@ -4,7 +4,7 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_middle::{mir, ty};
+use rr_rustc_interface::middle::{mir, ty};
 
 use crate::environment::mir_utils::tuple_items_for_ty::TupleItemsForTy;
 
diff --git a/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs b/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs
index 54b42962..d64bb430 100644
--- a/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs
@@ -4,7 +4,7 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_middle::mir;
+use rr_rustc_interface::middle::mir;
 
 pub trait StatementAsAssign<'tcx> {
     /// If this statement is an assignment, returns the LHS and RHS. If not, returns `None`.
diff --git a/rr_frontend/translation/src/environment/mir_utils/statement_at.rs b/rr_frontend/translation/src/environment/mir_utils/statement_at.rs
index 831daec8..60dde627 100644
--- a/rr_frontend/translation/src/environment/mir_utils/statement_at.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/statement_at.rs
@@ -6,7 +6,7 @@
 
 use std::cmp::Ordering;
 
-use rustc_middle::mir;
+use rr_rustc_interface::middle::mir;
 
 pub trait StatementAt<'tcx> {
     fn statement_at(&self, location: mir::Location) -> Option<&mir::Statement<'tcx>>;
diff --git a/rr_frontend/translation/src/environment/mir_utils/tuple_items_for_ty.rs b/rr_frontend/translation/src/environment/mir_utils/tuple_items_for_ty.rs
index 5545446a..d9c5e951 100644
--- a/rr_frontend/translation/src/environment/mir_utils/tuple_items_for_ty.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/tuple_items_for_ty.rs
@@ -4,7 +4,7 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_middle::ty;
+use rr_rustc_interface::middle::ty;
 
 pub trait TupleItemsForTy<'tcx> {
     /// Tries to interpret the given `mir::Ty` as a tuple type. If this succeeds, it returns the
diff --git a/rr_frontend/translation/src/environment/mir_utils/ty_as_ty_ref.rs b/rr_frontend/translation/src/environment/mir_utils/ty_as_ty_ref.rs
index fe8c5c35..f82b9a8a 100644
--- a/rr_frontend/translation/src/environment/mir_utils/ty_as_ty_ref.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/ty_as_ty_ref.rs
@@ -4,8 +4,8 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use rustc_middle::mir::terminator::Mutability;
-use rustc_middle::ty::{Region, Ty, TyKind};
+use rr_rustc_interface::middle::mir::terminator::Mutability;
+use rr_rustc_interface::middle::ty::{Region, Ty, TyKind};
 
 pub trait TyAsRef<'tcx> {
     fn as_ty_ref(&self) -> Option<(Region<'tcx>, Ty<'tcx>, Mutability)>;
diff --git a/rr_frontend/translation/src/environment/mod.rs b/rr_frontend/translation/src/environment/mod.rs
index fda28c7d..cffbe283 100644
--- a/rr_frontend/translation/src/environment/mod.rs
+++ b/rr_frontend/translation/src/environment/mod.rs
@@ -22,14 +22,15 @@ use std::collections::{HashMap, HashSet};
 use std::path::PathBuf;
 use std::rc::Rc;
 
-use rustc_ast::ast::Attribute;
-use rustc_hir::def_id::{DefId, LocalDefId};
-use rustc_hir::hir_id::HirId;
-use rustc_middle::{mir, ty};
-use rustc_span::source_map::SourceMap;
-use rustc_span::symbol::Symbol;
-use rustc_span::Span;
-use rustc_trait_selection::infer::{InferCtxtExt, TyCtxtInferExt};
+use rr_rustc_interface::ast::ast::Attribute;
+use rr_rustc_interface::hir::def_id::{DefId, LocalDefId};
+use rr_rustc_interface::hir::hir_id::HirId;
+use rr_rustc_interface::middle::{mir, ty};
+use rr_rustc_interface::span;
+use rr_rustc_interface::span::source_map::SourceMap;
+use rr_rustc_interface::span::symbol::Symbol;
+use rr_rustc_interface::span::Span;
+use rr_rustc_interface::trait_selection::infer::{InferCtxtExt, TyCtxtInferExt};
 
 use crate::data::ProcedureDefId;
 use crate::environment::borrowck::facts;
@@ -73,7 +74,7 @@ impl<'tcx> Environment<'tcx> {
 
     /// Returns the name of the crate that is being compiled
     pub fn crate_name(&self) -> String {
-        self.tcx.crate_name(rustc_span::def_id::LOCAL_CRATE).to_string()
+        self.tcx.crate_name(span::def_id::LOCAL_CRATE).to_string()
     }
 
     /// Returns the typing context
diff --git a/rr_frontend/translation/src/environment/polonius_info.rs b/rr_frontend/translation/src/environment/polonius_info.rs
index 7790938c..ae3191bb 100644
--- a/rr_frontend/translation/src/environment/polonius_info.rs
+++ b/rr_frontend/translation/src/environment/polonius_info.rs
@@ -11,13 +11,14 @@ use std::io::Write;
 use std::path::PathBuf;
 
 use log::{debug, trace};
-use polonius_engine::{Algorithm, Output};
-use rustc_data_structures::fx::FxHashMap;
-use rustc_index::Idx;
-use rustc_middle::ty::fold::TypeFolder;
-use rustc_middle::{mir, ty};
-use rustc_span::def_id::DefId;
-use rustc_span::Span;
+use rr_rustc_interface::data_structures::fx::FxHashMap;
+use rr_rustc_interface::hir;
+use rr_rustc_interface::index::Idx;
+use rr_rustc_interface::middle::ty::fold::TypeFolder;
+use rr_rustc_interface::middle::{mir, ty};
+use rr_rustc_interface::polonius_engine::{Algorithm, Output};
+use rr_rustc_interface::span::def_id::DefId;
+use rr_rustc_interface::span::Span;
 
 use crate::environment::borrowck::facts::PointType;
 use crate::environment::borrowck::place_regions::PlaceRegions;
@@ -85,7 +86,7 @@ impl AtomicRegion {
     }
 }
 
-/// for an overview fo universal regions, see also `rustc_borrowck/src/universal_regions.rs`
+/// for an overview fo universal regions, see also `borrowck/src/universal_regions.rs`
 #[derive(Copy, Clone, Eq, PartialEq, Debug)]
 pub enum UniversalRegionKind {
     /// the static region
@@ -174,7 +175,7 @@ pub enum Error {
 
 pub fn graphviz<'tcx>(
     env: &Environment<'tcx>,
-    def_path: &rustc_hir::definitions::DefPath,
+    def_path: &hir::definitions::DefPath,
     def_id: DefId,
     info: &PoloniusInfo<'_, 'tcx>,
 ) -> io::Result<()> {
diff --git a/rr_frontend/translation/src/environment/procedure.rs b/rr_frontend/translation/src/environment/procedure.rs
index 58d5e164..0e56e280 100644
--- a/rr_frontend/translation/src/environment/procedure.rs
+++ b/rr_frontend/translation/src/environment/procedure.rs
@@ -8,9 +8,9 @@ use std::collections::{HashMap, HashSet};
 use std::rc::Rc;
 
 use log::{debug, trace};
-use rustc_middle::mir::{self, BasicBlock, Body as Mir, TerminatorKind};
-use rustc_middle::ty::{self, Ty, TyCtxt};
-use rustc_span::Span;
+use rr_rustc_interface::middle::mir::{self, BasicBlock, Body as Mir, TerminatorKind};
+use rr_rustc_interface::middle::ty::{self, Ty, TyCtxt};
+use rr_rustc_interface::span::Span;
 
 use crate::data::ProcedureDefId;
 use crate::environment::mir_utils::real_edges::RealEdges;
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index e548cb83..eab256b4 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -8,17 +8,18 @@ use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
 
 use log::{info, trace, warn};
 use radium::coq;
-use rustc_hir::def_id::DefId;
-use rustc_middle::mir::interpret::{ConstValue, Scalar};
-use rustc_middle::mir::tcx::PlaceTy;
-use rustc_middle::mir::{
+use rr_rustc_interface::hir::def_id::DefId;
+use rr_rustc_interface::middle::mir::interpret::{ConstValue, Scalar};
+use rr_rustc_interface::middle::mir::tcx::PlaceTy;
+use rr_rustc_interface::middle::mir::{
     BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, LocalKind, Location,
     Mutability, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator, TerminatorKind, UnOp,
     VarDebugInfoContents,
 };
-use rustc_middle::ty::fold::TypeFolder;
-use rustc_middle::ty::{ConstKind, Ty, TyKind, TypeFoldable};
-use rustc_middle::{mir, ty};
+use rr_rustc_interface::middle::ty::fold::TypeFolder;
+use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind, TypeFoldable};
+use rr_rustc_interface::middle::{mir, ty};
+use rr_rustc_interface::{abi, ast, middle};
 
 use crate::arg_folder::*;
 use crate::base::*;
@@ -215,7 +216,7 @@ pub struct FunctionTranslator<'a, 'def, 'tcx> {
     /// registry of consts
     const_registry: &'a ConstScope<'def>,
     /// attributes on this function
-    attrs: &'a [&'a rustc_ast::ast::AttrItem],
+    attrs: &'a [&'a ast::ast::AttrItem],
     /// polonius info for this function
     info: &'a PoloniusInfo<'a, 'tcx>,
     /// translator for types
@@ -342,7 +343,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
         env: &'def Environment<'tcx>,
         meta: &ProcedureMeta,
         proc: Procedure<'tcx>,
-        attrs: &'a [&'a rustc_ast::ast::AttrItem],
+        attrs: &'a [&'a ast::ast::AttrItem],
         ty_translator: &'def TypeTranslator<'def, 'tcx>,
         proc_registry: &'a ProcedureScope<'def>,
         const_registry: &'a ConstScope<'def>,
@@ -585,7 +586,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
         env: &'def Environment<'tcx>,
         meta: &ProcedureMeta,
         proc: Procedure<'tcx>,
-        attrs: &'a [&'a rustc_ast::ast::AttrItem],
+        attrs: &'a [&'a ast::ast::AttrItem],
         ty_translator: &'def TypeTranslator<'def, 'tcx>,
         proc_registry: &'a ProcedureScope<'def>,
         const_registry: &'a ConstScope<'def>,
@@ -1118,7 +1119,7 @@ struct BodyTranslator<'a, 'def, 'tcx> {
     /// scope of used consts
     const_registry: &'a ConstScope<'def>,
     /// attributes on this function
-    attrs: &'a [&'a rustc_ast::ast::AttrItem],
+    attrs: &'a [&'a ast::ast::AttrItem],
     /// polonius info for this function
     info: &'a PoloniusInfo<'a, 'tcx>,
     /// local lifetimes: the LHS is the lifetime name, the RHS are the super lifetimes
@@ -1887,7 +1888,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
         func: &Operand<'tcx>,
         args: &[Operand<'tcx>],
         destination: &Place<'tcx>,
-        target: Option<rustc_middle::mir::BasicBlock>,
+        target: Option<middle::mir::BasicBlock>,
         loc: Location,
         dying_loans: &[facts::Loan],
     ) -> Result<radium::Stmt, TranslationError> {
@@ -3466,7 +3467,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
             traits::TraitResolutionKind::Closure => {
                 // TODO: here, we should first generate an instance of the trait
                 //self.env.tcx().
-                // mir_shims(rustc_middle::ty::InstanceDef::Item(resolved_did));
+                // mir_shims(middle::ty::InstanceDef::Item(resolved_did));
                 // the args are just the closure args. We can ignore them.
                 let _clos_args = resolved_params.as_closure();
                 let param_name = self.register_use_procedure(resolved_did, ty::List::empty())?;
@@ -3532,7 +3533,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
                 Scalar::Ptr(pointer, _) => {
                     let glob_alloc = self.env.tcx().global_alloc(pointer.provenance);
                     match glob_alloc {
-                        rustc_middle::mir::interpret::GlobalAlloc::Static(did) => {
+                        middle::mir::interpret::GlobalAlloc::Static(did) => {
                             info!(
                                 "Found static GlobalAlloc {:?} for Ref scalar {:?} at type {:?}",
                                 did, sc, ty
@@ -3651,7 +3652,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
                     let name = self.ty_translator.translator.get_field_name_of(
                         *f,
                         cur_ty.ty,
-                        cur_ty.variant_index.map(rustc_abi::VariantIdx::as_usize),
+                        cur_ty.variant_index.map(abi::VariantIdx::as_usize),
                     )?;
 
                     acc_expr = radium::Expr::FieldOf {
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index b10d0340..bb8f4d4d 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -7,25 +7,6 @@
 #![feature(box_patterns)]
 #![feature(let_chains)]
 #![feature(rustc_private)]
-extern crate polonius_engine;
-extern crate rustc_abi;
-extern crate rustc_ast;
-extern crate rustc_attr;
-extern crate rustc_borrowck;
-extern crate rustc_data_structures;
-extern crate rustc_driver;
-extern crate rustc_errors;
-extern crate rustc_hir;
-extern crate rustc_index;
-extern crate rustc_infer;
-extern crate rustc_interface;
-extern crate rustc_middle;
-extern crate rustc_session;
-extern crate rustc_span;
-extern crate rustc_target;
-extern crate rustc_trait_selection;
-extern crate rustc_type_ir;
-
 mod arg_folder;
 mod base;
 mod checked_op_analysis;
@@ -49,8 +30,9 @@ use std::{fs, io, process};
 
 use log::{info, trace, warn};
 use radium::coq;
-use rustc_hir::def_id::{DefId, LocalDefId};
-use rustc_middle::ty;
+use rr_rustc_interface::hir::def_id::{DefId, LocalDefId};
+use rr_rustc_interface::middle::ty;
+use rr_rustc_interface::{ast, span};
 use topological_sort::TopologicalSort;
 use typed_arena::Arena;
 
@@ -614,8 +596,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
     /// Write Coq files for this verification unit.
     pub fn write_coq_files(&self) {
         // use the crate_name for naming
-        let crate_name: rustc_span::symbol::Symbol =
-            self.env.tcx().crate_name(rustc_span::def_id::LOCAL_CRATE);
+        let crate_name: span::symbol::Symbol = self.env.tcx().crate_name(span::def_id::LOCAL_CRATE);
         let stem = crate_name.as_str();
 
         // create output directory
@@ -985,7 +966,7 @@ fn register_functions(vcx: &mut VerificationCtxt<'_, '_>) -> Result<(), String>
     Ok(())
 }
 
-fn propagate_attr_from_impl(it: &rustc_ast::ast::AttrItem) -> bool {
+fn propagate_attr_from_impl(it: &ast::ast::AttrItem) -> bool {
     let Some(ident) = it.path.segments.get(1) else {
         return false;
     };
@@ -993,7 +974,7 @@ fn propagate_attr_from_impl(it: &rustc_ast::ast::AttrItem) -> bool {
     matches!(ident.ident.as_str(), "context")
 }
 
-fn get_attributes_of_function<'a>(env: &'a Environment, did: DefId) -> Vec<&'a rustc_ast::ast::AttrItem> {
+fn get_attributes_of_function<'a>(env: &'a Environment, did: DefId) -> Vec<&'a ast::ast::AttrItem> {
     let attrs = env.get_attributes(did);
     let mut filtered_attrs = utils::filter_tool_attrs(attrs);
     // also add selected attributes from the surrounding impl
diff --git a/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs
index 2c4a2b9c..6744cb71 100644
--- a/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs
@@ -5,8 +5,8 @@
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
 use attribute_parse::parse;
-use rustc_ast::ast::AttrItem;
-use rustc_hir::def_id::LocalDefId;
+use rr_rustc_interface::ast::ast::AttrItem;
+use rr_rustc_interface::hir::def_id::LocalDefId;
 
 use crate::spec_parsers::parse_utils::str_err;
 
diff --git a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
index 8fbc750a..7b161de0 100644
--- a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
@@ -6,7 +6,7 @@
 
 use attribute_parse::parse;
 use radium::{coq, specs};
-use rustc_ast::ast::AttrItem;
+use rr_rustc_interface::ast::ast::AttrItem;
 
 use crate::spec_parsers::parse_utils::{self, str_err};
 
diff --git a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
index fa782491..06f529d5 100644
--- a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
@@ -7,7 +7,7 @@
 use attribute_parse::{parse, MToken};
 use parse::{Parse, Peek};
 use radium::{coq, specs};
-use rustc_ast::ast::AttrItem;
+use rr_rustc_interface::ast::ast::AttrItem;
 
 use crate::spec_parsers::parse_utils::*;
 
diff --git a/rr_frontend/translation/src/spec_parsers/mod.rs b/rr_frontend/translation/src/spec_parsers/mod.rs
index e908dfbd..aee93f84 100644
--- a/rr_frontend/translation/src/spec_parsers/mod.rs
+++ b/rr_frontend/translation/src/spec_parsers/mod.rs
@@ -8,7 +8,7 @@ pub mod verbose_function_spec_parser;
 
 use attribute_parse::{parse, MToken};
 use parse::Parse;
-use rustc_ast::ast::AttrItem;
+use rr_rustc_interface::ast::ast::AttrItem;
 
 /// For parsing of `RustPaths`
 pub struct RustPath {
diff --git a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
index 366ea5a8..74356571 100644
--- a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
@@ -6,8 +6,8 @@
 
 use attribute_parse::parse;
 use radium::{coq, specs};
-use rustc_ast::ast::AttrItem;
-use rustc_hir::def_id::LocalDefId;
+use rr_rustc_interface::ast::ast::AttrItem;
+use rr_rustc_interface::hir::def_id::LocalDefId;
 
 use crate::spec_parsers::parse_utils::{self, str_err};
 
diff --git a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
index 93bc5357..5516a3a1 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -9,7 +9,7 @@ use attribute_parse::{parse, MToken};
 use log::info;
 use parse::{Parse, Peek};
 use radium::{coq, specs};
-use rustc_ast::ast::AttrItem;
+use rr_rustc_interface::ast::ast::AttrItem;
 
 use crate::spec_parsers::parse_utils::*;
 
diff --git a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
index 017ac64f..2db54b5a 100644
--- a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
@@ -10,8 +10,8 @@ use attribute_parse::{parse, MToken};
 use log::{info, warn};
 use parse::{Parse, Peek};
 use radium::{coq, push_str_list, specs};
-use rustc_ast::ast::AttrItem;
-use rustc_middle::ty;
+use rr_rustc_interface::ast::ast::AttrItem;
+use rr_rustc_interface::middle::ty;
 
 use crate::spec_parsers::parse_utils::{ParseMeta, *};
 
diff --git a/rr_frontend/translation/src/traits.rs b/rr_frontend/translation/src/traits.rs
index a0fe5d11..5a52d966 100644
--- a/rr_frontend/translation/src/traits.rs
+++ b/rr_frontend/translation/src/traits.rs
@@ -1,13 +1,14 @@
 /// Inspired by (in terms of rustc APIs used) by
 /// <https://github.com/xldenis/creusot/blob/9d8b1822cd0c43154a6d5d4d05460be56710399c/creusot/src/translation/traits.rs>
 use log::info;
-use rustc_hir::def_id::DefId;
-use rustc_infer::infer::TyCtxtInferExt;
-use rustc_middle::ty;
-use rustc_middle::ty::{
+use rr_rustc_interface::hir::def_id::DefId;
+use rr_rustc_interface::infer::infer::TyCtxtInferExt;
+use rr_rustc_interface::middle::ty;
+use rr_rustc_interface::middle::ty::{
     AssocItem, AssocItemContainer, GenericArgsRef, ParamEnv, TraitRef, TyCtxt, TypeVisitableExt,
 };
-use rustc_trait_selection::traits::{ImplSource, NormalizeExt};
+use rr_rustc_interface::trait_selection::traits::{ImplSource, NormalizeExt};
+use rr_rustc_interface::{middle, trait_selection};
 
 pub fn associated_items(tcx: TyCtxt, def_id: DefId) -> impl Iterator<Item = &AssocItem> {
     tcx.associated_items(def_id).in_definition_order()
@@ -18,14 +19,14 @@ pub fn normalize_type<'tcx, T>(
     tcx: TyCtxt<'tcx>,
     param_env: ParamEnv<'tcx>,
     ty: T,
-) -> Result<T, Vec<rustc_trait_selection::traits::FulfillmentError<'tcx>>>
+) -> Result<T, Vec<trait_selection::traits::FulfillmentError<'tcx>>>
 where
     T: ty::TypeFoldable<ty::TyCtxt<'tcx>>,
 {
     let infer_ctx = tcx.infer_ctxt().build();
-    rustc_trait_selection::traits::fully_normalize(
+    trait_selection::traits::fully_normalize(
         &infer_ctx,
-        rustc_middle::traits::ObligationCause::dummy(),
+        middle::traits::ObligationCause::dummy(),
         param_env,
         ty,
     )
@@ -138,7 +139,7 @@ pub fn resolve_assoc_item<'tcx>(
             // this is a user-defined trait, and we found the right impl
             // now map back to the item we were looking for
             let trait_did = tcx.trait_id_of_impl(impl_data.impl_def_id).unwrap();
-            let trait_def: &'tcx rustc_middle::ty::TraitDef = tcx.trait_def(trait_did);
+            let trait_def: &'tcx middle::ty::TraitDef = tcx.trait_def(trait_did);
 
             // Find the id of the actual associated method we will be running
             let ancestors = trait_def.ancestors(tcx, impl_data.impl_def_id).unwrap();
@@ -157,7 +158,7 @@ pub fn resolve_assoc_item<'tcx>(
 
             let param_env = param_env.with_reveal_all_normalized(tcx);
             let substs = substs.rebase_onto(tcx, trait_did, impl_data.args);
-            let substs = rustc_trait_selection::traits::translate_args(
+            let substs = trait_selection::traits::translate_args(
                 &infcx,
                 param_env,
                 impl_data.impl_def_id,
@@ -176,7 +177,7 @@ pub fn resolve_assoc_item<'tcx>(
         {
             match *substs[0].as_type().unwrap().kind() {
                 // try to get the body
-                rustc_middle::ty::Closure(closure_def_id, closure_substs) => {
+                middle::ty::Closure(closure_def_id, closure_substs) => {
                     Some((closure_def_id, closure_substs, TraitResolutionKind::Closure))
                 },
                 _ => unimplemented!(),
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 2a215b95..a0ea4e70 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -10,9 +10,10 @@ use std::fmt::Write;
 
 use log::{info, trace, warn};
 use radium::{self, coq, push_str_list};
-use rustc_hir::def_id::DefId;
-use rustc_middle::ty;
-use rustc_middle::ty::{IntTy, Ty, TyKind, TypeFoldable, UintTy};
+use rr_rustc_interface::hir::def_id::DefId;
+use rr_rustc_interface::middle::ty;
+use rr_rustc_interface::middle::ty::{IntTy, Ty, TyKind, TypeFoldable, UintTy};
+use rr_rustc_interface::{abi, ast, attr, middle, target};
 use typed_arena::Arena;
 
 use crate::base::*;
@@ -498,7 +499,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
     fn generate_structlike_use_internal<'a, 'b>(
         &self,
         ty: Ty<'tcx>,
-        variant: Option<rustc_target::abi::VariantIdx>,
+        variant: Option<target::abi::VariantIdx>,
         adt_deps: TranslationState<'a, 'b, 'def>,
     ) -> Result<radium::Type<'def>, TranslationError> {
         match ty.kind() {
@@ -672,7 +673,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
     fn generate_enum_variant_use_noshim<'a, 'b, F>(
         &self,
         adt_id: DefId,
-        variant_idx: rustc_target::abi::VariantIdx,
+        variant_idx: target::abi::VariantIdx,
         args: F,
         state: TranslationState<'a, 'b, 'def>,
     ) -> Result<radium::AbstractStructUse<'def>, TranslationError>
@@ -977,14 +978,14 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
         &self,
         did: DefId,
         env: &'a [ty::GenericArg<'tcx>],
-    ) -> rustc_middle::mir::interpret::GlobalId<'tcx> {
-        rustc_middle::mir::interpret::GlobalId {
+    ) -> middle::mir::interpret::GlobalId<'tcx> {
+        middle::mir::interpret::GlobalId {
             instance: ty::Instance::new(did, self.env.tcx().mk_args(env)),
             promoted: None,
         }
     }
 
-    fn try_scalar_int_to_i128(s: rustc_middle::ty::ScalarInt) -> Option<i128> {
+    fn try_scalar_int_to_i128(s: middle::ty::ScalarInt) -> Option<i128> {
         s.try_to_int(s.size()).ok()
     }
 
@@ -1387,7 +1388,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
                 };
 
                 match mutability {
-                    rustc_ast::ast::Mutability::Mut => Ok(radium::Type::MutRef(Box::new(translated_ty), lft)),
+                    ast::ast::Mutability::Mut => Ok(radium::Type::MutRef(Box::new(translated_ty), lft)),
                     _ => Ok(radium::Type::ShrRef(Box::new(translated_ty), lft)),
                 }
             },
@@ -1535,51 +1536,53 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
         }
     }
 
-    /// Translate a `rustc_attr::IntType` (this is different from the `rustc_ty` `IntType`).
-    const fn translate_int_type(it: rustc_attr::IntType) -> radium::IntType {
+    /// Translate a `attr::IntType` (this is different from the `ty`
+    /// `IntType`).
+    const fn translate_int_type(it: attr::IntType) -> radium::IntType {
         match it {
-            rustc_attr::IntType::SignedInt(it) => match it {
-                rustc_ast::IntTy::I8 => radium::IntType::I8,
-                rustc_ast::IntTy::I16 => radium::IntType::I16,
-                rustc_ast::IntTy::I32 => radium::IntType::I32,
-                rustc_ast::IntTy::I64 => radium::IntType::I64,
-                rustc_ast::IntTy::I128 => radium::IntType::I128,
-                rustc_ast::IntTy::Isize => radium::IntType::ISize,
+            attr::IntType::SignedInt(it) => match it {
+                ast::IntTy::I8 => radium::IntType::I8,
+                ast::IntTy::I16 => radium::IntType::I16,
+                ast::IntTy::I32 => radium::IntType::I32,
+                ast::IntTy::I64 => radium::IntType::I64,
+                ast::IntTy::I128 => radium::IntType::I128,
+                ast::IntTy::Isize => radium::IntType::ISize,
             },
-            rustc_attr::IntType::UnsignedInt(it) => match it {
-                rustc_ast::UintTy::U8 => radium::IntType::U8,
-                rustc_ast::UintTy::U16 => radium::IntType::U16,
-                rustc_ast::UintTy::U32 => radium::IntType::U32,
-                rustc_ast::UintTy::U64 => radium::IntType::U64,
-                rustc_ast::UintTy::U128 => radium::IntType::U128,
-                rustc_ast::UintTy::Usize => radium::IntType::USize,
+            attr::IntType::UnsignedInt(it) => match it {
+                ast::UintTy::U8 => radium::IntType::U8,
+                ast::UintTy::U16 => radium::IntType::U16,
+                ast::UintTy::U32 => radium::IntType::U32,
+                ast::UintTy::U64 => radium::IntType::U64,
+                ast::UintTy::U128 => radium::IntType::U128,
+                ast::UintTy::Usize => radium::IntType::USize,
             },
         }
     }
 
-    /// Translate a `rustc_attr::IntType` (this is different from the `rustc_ty` `IntType`).
-    const fn translate_integer_type(it: rustc_abi::IntegerType) -> radium::IntType {
+    /// Translate a `attr::IntType` (this is different from the `ty`
+    /// `IntType`).
+    const fn translate_integer_type(it: abi::IntegerType) -> radium::IntType {
         match it {
-            rustc_abi::IntegerType::Fixed(size, sign) => {
+            abi::IntegerType::Fixed(size, sign) => {
                 if sign {
                     match size {
-                        rustc_abi::Integer::I8 => radium::IntType::I8,
-                        rustc_abi::Integer::I16 => radium::IntType::I16,
-                        rustc_abi::Integer::I32 => radium::IntType::I32,
-                        rustc_abi::Integer::I64 => radium::IntType::I64,
-                        rustc_abi::Integer::I128 => radium::IntType::I128,
+                        abi::Integer::I8 => radium::IntType::I8,
+                        abi::Integer::I16 => radium::IntType::I16,
+                        abi::Integer::I32 => radium::IntType::I32,
+                        abi::Integer::I64 => radium::IntType::I64,
+                        abi::Integer::I128 => radium::IntType::I128,
                     }
                 } else {
                     match size {
-                        rustc_abi::Integer::I8 => radium::IntType::U8,
-                        rustc_abi::Integer::I16 => radium::IntType::U16,
-                        rustc_abi::Integer::I32 => radium::IntType::U32,
-                        rustc_abi::Integer::I64 => radium::IntType::U64,
-                        rustc_abi::Integer::I128 => radium::IntType::U128,
+                        abi::Integer::I8 => radium::IntType::U8,
+                        abi::Integer::I16 => radium::IntType::U16,
+                        abi::Integer::I32 => radium::IntType::U32,
+                        abi::Integer::I64 => radium::IntType::U64,
+                        abi::Integer::I128 => radium::IntType::U128,
                     }
                 }
             },
-            rustc_abi::IntegerType::Pointer(sign) => {
+            abi::IntegerType::Pointer(sign) => {
                 if sign {
                     radium::IntType::ISize
                 } else {
@@ -1592,7 +1595,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
     /// Get the name for a field of an ADT or tuple type
     pub fn get_field_name_of(
         &self,
-        f: rustc_target::abi::FieldIdx,
+        f: target::abi::FieldIdx,
         ty: Ty<'tcx>,
         variant: Option<usize>,
     ) -> Result<String, TranslationError> {
@@ -1601,13 +1604,13 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
             TyKind::Adt(def, _) => {
                 info!("getting field name of {:?} at {} (variant {:?})", f, ty, variant);
                 if def.is_struct() {
-                    let i = def.variants().get(rustc_target::abi::VariantIdx::from_usize(0)).unwrap();
+                    let i = def.variants().get(target::abi::VariantIdx::from_usize(0)).unwrap();
                     i.fields.get(f).map(|f| f.ident(tcx).to_string()).ok_or_else(|| {
                         TranslationError::UnknownError(format!("could not get field {:?} of {}", f, ty))
                     })
                 } else if def.is_enum() {
                     let variant = variant.unwrap();
-                    let i = def.variants().get(rustc_target::abi::VariantIdx::from_usize(variant)).unwrap();
+                    let i = def.variants().get(target::abi::VariantIdx::from_usize(variant)).unwrap();
                     i.fields.get(f).map(|f| f.ident(tcx).to_string()).ok_or_else(|| {
                         TranslationError::UnknownError(format!("could not get field {:?} of {}", f, ty))
                     })
@@ -1632,7 +1635,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
     /// Get the name of a variant of an enum.
     pub fn get_variant_name_of(
         ty: Ty<'tcx>,
-        variant: rustc_target::abi::VariantIdx,
+        variant: target::abi::VariantIdx,
     ) -> Result<String, TranslationError> {
         match ty.kind() {
             TyKind::Adt(def, _) => {
@@ -1684,7 +1687,7 @@ impl<'def, 'tcx> TypeTranslator<'def, 'tcx> {
     pub fn generate_structlike_use<'a>(
         &self,
         ty: Ty<'tcx>,
-        variant: Option<rustc_target::abi::VariantIdx>,
+        variant: Option<target::abi::VariantIdx>,
         scope: InFunctionState<'a, 'def>,
     ) -> Result<Option<radium::LiteralTypeUse<'def>>, TranslationError> {
         match ty.kind() {
@@ -1886,7 +1889,7 @@ impl<'a, 'def, 'tcx> LocalTypeTranslator<'a, 'def, 'tcx> {
     pub fn generate_structlike_use(
         &self,
         ty: Ty<'tcx>,
-        variant: Option<rustc_target::abi::VariantIdx>,
+        variant: Option<target::abi::VariantIdx>,
     ) -> Result<Option<radium::LiteralTypeUse<'def>>, TranslationError> {
         let mut scope = self.scope.borrow_mut();
         self.translator.generate_structlike_use(ty, variant, &mut scope)
diff --git a/rr_frontend/translation/src/tyvars.rs b/rr_frontend/translation/src/tyvars.rs
index 06fee40b..02994e21 100644
--- a/rr_frontend/translation/src/tyvars.rs
+++ b/rr_frontend/translation/src/tyvars.rs
@@ -6,8 +6,8 @@
 
 use std::collections::{HashMap, HashSet};
 
-use rustc_middle::ty;
-use rustc_middle::ty::{Ty, TyCtxt, TyKind};
+use rr_rustc_interface::middle::ty;
+use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind};
 use ty::TypeSuperFoldable;
 
 use crate::base::*;
diff --git a/rr_frontend/translation/src/utils.rs b/rr_frontend/translation/src/utils.rs
index d92f5748..0e1d7ccb 100644
--- a/rr_frontend/translation/src/utils.rs
+++ b/rr_frontend/translation/src/utils.rs
@@ -11,12 +11,13 @@
 use std::mem;
 
 use log::{info, trace};
+use rr_rustc_interface::ast::ast;
+use rr_rustc_interface::data_structures::fx::FxHashSet;
+use rr_rustc_interface::hir::def_id::{DefId, CRATE_DEF_INDEX};
+use rr_rustc_interface::middle::mir;
+use rr_rustc_interface::middle::ty::{self, TyCtxt};
+use rr_rustc_interface::{hir, middle, span};
 use rrconfig as config;
-use rustc_ast::ast;
-use rustc_data_structures::fx::FxHashSet;
-use rustc_hir::def_id::{DefId, CRATE_DEF_INDEX};
-use rustc_middle::mir;
-use rustc_middle::ty::{self, TyCtxt};
 use serde::{Deserialize, Serialize};
 
 use crate::spec_parsers::get_export_as_attr;
@@ -158,7 +159,7 @@ pub fn get_cleaned_def_path(tcx: TyCtxt<'_>, did: DefId) -> Vec<String> {
 
 // Alternative implementation of `get_cleaned_def_path`, but this doesn't always yield a rooted
 // path (but only a suffix of the full path)
-fn extract_def_path(path: &rustc_hir::definitions::DefPath) -> Vec<String> {
+fn extract_def_path(path: &hir::definitions::DefPath) -> Vec<String> {
     let mut components = Vec::new();
     for p in &path.data {
         if let Some(name) = p.data.get_opt_name() {
@@ -213,12 +214,12 @@ where
                 index: CRATE_DEF_INDEX,
             };
 
-            let mut items: &[rustc_middle::metadata::ModChild] = tcx.module_children(krate);
+            let mut items: &[middle::metadata::ModChild] = tcx.module_children(krate);
             let mut path_it = path.iter().skip(1).peekable();
 
             while let Some(segment) = path_it.next() {
                 for item in mem::take(&mut items) {
-                    let item: &rustc_middle::metadata::ModChild = item;
+                    let item: &middle::metadata::ModChild = item;
                     if item.ident.name.as_str() == segment.as_ref() {
                         if path_it.peek().is_none() {
                             return Some(item.res.def_id());
@@ -305,11 +306,8 @@ pub fn try_resolve_trait_method_did<'tcx>(
     // get all impls of this trait
     let impls: &ty::trait_def::TraitImpls = tcx.trait_impls_of(trait_did);
 
-    let simplified_type = rustc_middle::ty::fast_reject::simplify_type(
-        tcx,
-        for_type,
-        ty::fast_reject::TreatParams::AsCandidateKey,
-    )?;
+    let simplified_type =
+        middle::ty::fast_reject::simplify_type(tcx, for_type, ty::fast_reject::TreatParams::AsCandidateKey)?;
     let defs = impls.non_blanket_impls().get(&simplified_type)?;
     info!("found implementations: {:?}", impls);
 
@@ -340,7 +338,7 @@ pub fn try_resolve_trait_method_did<'tcx>(
                 // find the right item
                 if let Some(item) = impl_assoc_items.find_by_name_and_kind(
                     tcx,
-                    rustc_span::symbol::Ident::from_str(method_name),
+                    span::symbol::Ident::from_str(method_name),
                     ty::AssocKind::Fn,
                     trait_did,
                 ) {
@@ -380,13 +378,13 @@ where
                 index: CRATE_DEF_INDEX,
             };
 
-            let mut items: &[rustc_middle::metadata::ModChild] = tcx.module_children(krate);
+            let mut items: &[middle::metadata::ModChild] = tcx.module_children(krate);
             let mut path_it = path.iter().skip(1).peekable();
 
             while let Some(segment) = path_it.next() {
                 //info!("items to look at: {:?}", items);
                 for item in mem::take(&mut items) {
-                    let item: &rustc_middle::metadata::ModChild = item;
+                    let item: &middle::metadata::ModChild = item;
 
                     if item.ident.name.as_str() != segment.as_ref() {
                         continue;
-- 
GitLab