From a7cbdd14bcbcf5ff081db90f7ff71aaf91dbbf7d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Thu, 2 Jan 2025 14:47:13 +0100
Subject: [PATCH] refactor shims

---
 rr_frontend/translation/src/lib.rs            |  63 ++---
 rr_frontend/translation/src/shims/flat.rs     | 235 ++++++++++++++++++
 rr_frontend/translation/src/shims/mod.rs      |  50 ++++
 .../{shim_registry.rs => shims/registry.rs}   |  37 ++-
 .../translation/src/traits/requirements.rs    |   6 +-
 rr_frontend/translation/src/utils.rs          | 214 ----------------
 6 files changed, 318 insertions(+), 287 deletions(-)
 create mode 100644 rr_frontend/translation/src/shims/flat.rs
 create mode 100644 rr_frontend/translation/src/shims/mod.rs
 rename rr_frontend/translation/src/{shim_registry.rs => shims/registry.rs} (96%)

diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index ac51c59..942c4c6 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -1,4 +1,4 @@
-// © 2023, The RefinedRust Developers and Contributors
+// © 2023, The RefinedRust Develcpers and Contributors
 //
 // This Source Code Form is subject to the terms of the BSD-3-clause License.
 // If a copy of the BSD-3-clause license was not distributed with this
@@ -17,7 +17,7 @@ mod force_matches_macro;
 mod function_body;
 mod inclusion_tracker;
 mod regions;
-mod shim_registry;
+mod shims;
 mod spec_parsers;
 mod traits;
 mod types;
@@ -39,6 +39,7 @@ use typed_arena::Arena;
 
 use crate::environment::Environment;
 use crate::function_body::{ConstScope, FunctionTranslator, ProcedureMode, ProcedureScope};
+use crate::shims::registry as shim_registry;
 use crate::spec_parsers::const_attr_parser::{ConstAttrParser, VerboseConstAttrParser};
 use crate::spec_parsers::crate_attr_parser::{CrateAttrParser, VerboseCrateAttrParser};
 use crate::spec_parsers::module_attr_parser::{ModuleAttrParser, ModuleAttrs, VerboseModuleAttrParser};
@@ -92,7 +93,7 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
 
     coq_path_prefix: String,
     dune_package: Option<String>,
-    shim_registry: shim_registry::ShimRegistry<'rcx>,
+    shim_registry: shims::registry::SR<'rcx>,
 
     /// trait implementations we generated
     trait_impls: HashMap<DefId, radium::TraitImplSpec<'rcx>>,
@@ -100,12 +101,12 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
 
 impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
     fn get_path_for_shim(&self, did: DefId) -> Vec<&str> {
-        let path = utils::get_export_path_for_did(self.env, did);
+        let path = shims::flat::get_export_path_for_did(self.env, did);
         let interned_path = self.shim_registry.intern_path(path);
         interned_path
     }
 
-    fn make_shim_function_entry(&self, did: DefId, spec_name: &str) -> Option<shim_registry::FunctionShim> {
+    fn make_shim_function_entry(&self, did: DefId, spec_name: &str) -> Option<shims::registry::FunctionShim> {
         let Some(mode) = self.procedure_registry.lookup_function_mode(did) else {
             return None;
         };
@@ -175,11 +176,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
                 let impl_for = args[0].expect_ty();
 
                 // flatten the trait reference
-                let trait_path = utils::PathWithArgs::from_item(self.env, trait_did, trait_args)?;
+                let trait_path = shims::flat::PathWithArgs::from_item(self.env, trait_did, trait_args)?;
                 trace!("got trait path: {:?}", trait_path);
 
                 // flatten the self type.
-                let Some(for_type) = utils::convert_ty_to_flat_type(self.env, impl_for) else {
+                let Some(for_type) = shims::flat::convert_ty_to_flat_type(self.env, impl_for) else {
                     return None;
                 };
 
@@ -236,11 +237,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
         let impl_for = args[0].expect_ty();
 
         // flatten the trait reference
-        let trait_path = utils::PathWithArgs::from_item(self.env, trait_did, trait_args)?;
+        let trait_path = shims::flat::PathWithArgs::from_item(self.env, trait_did, trait_args)?;
         trace!("got trait path: {:?}", trait_path);
 
         // flatten the self type.
-        let Some(for_type) = utils::convert_ty_to_flat_type(self.env, impl_for) else {
+        let Some(for_type) = shims::flat::convert_ty_to_flat_type(self.env, impl_for) else {
             trace!("leave make_impl_shim_entry (failed transating self type)");
             return None;
         };
@@ -407,7 +408,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
         info!("Generated module summary functions: {:?}", function_shims);
 
         let interface_file = File::create(path).unwrap();
-        shim_registry::write_shims(
+        shims::registry::write_shims(
             interface_file,
             module_path,
             module,
@@ -1397,7 +1398,7 @@ fn register_trait_impls(vcx: &VerificationCtxt<'_, '_>) -> Result<(), String> {
     Ok(())
 }
 
-/// Generate trait instances
+/// Generate trait instances.
 fn assemble_trait_impls<'tcx, 'rcx>(
     vcx: &mut VerificationCtxt<'tcx, 'rcx>,
 ) -> Result<(), base::TranslationError<'tcx>> {
@@ -1467,42 +1468,6 @@ pub fn get_module_attributes(env: &Environment<'_>) -> Result<HashMap<LocalDefId
     Ok(attrs)
 }
 
-/// Find `RefinedRust` modules in the given loadpath.
-fn scan_loadpath(path: &Path, storage: &mut HashMap<String, PathBuf>) -> io::Result<()> {
-    if path.is_dir() {
-        for entry in fs::read_dir(path)? {
-            let entry = entry?;
-            let path = entry.path();
-            if path.is_dir() {
-                scan_loadpath(path.as_path(), storage)?;
-            } else if path.is_file() {
-                if let Some(ext) = path.extension() {
-                    if Some("rrlib") == ext.to_str() {
-                        // try to open this rrlib file
-                        let f = File::open(path.clone())?;
-                        if let Some(name) = shim_registry::is_valid_refinedrust_module(f) {
-                            storage.insert(name, path);
-                        }
-                    }
-                }
-            }
-        }
-    }
-
-    Ok(())
-}
-
-/// Find `RefinedRust` modules in the given loadpaths.
-fn scan_loadpaths(paths: &[PathBuf]) -> io::Result<HashMap<String, PathBuf>> {
-    let mut found_lib_files: HashMap<String, PathBuf> = HashMap::new();
-
-    for path in paths {
-        scan_loadpath(path, &mut found_lib_files)?;
-    }
-
-    Ok(found_lib_files)
-}
-
 /// Translate a crate, creating a `VerificationCtxt` in the process.
 pub fn generate_coq_code<'tcx, F>(tcx: ty::TyCtxt<'tcx>, continuation: F) -> Result<(), String>
 where
@@ -1568,12 +1533,12 @@ where
     );
     let procedure_registry = ProcedureScope::new();
     let shim_string_arena = Arena::new();
-    let mut shim_registry = shim_registry::ShimRegistry::empty(&shim_string_arena);
+    let mut shim_registry = shim_registry::SR::empty(&shim_string_arena);
 
     // add includes to the shim registry
     let library_load_paths = rrconfig::lib_load_paths();
     info!("Loading libraries from {:?}", library_load_paths);
-    let found_libs = scan_loadpaths(&library_load_paths).map_err(|e| e.to_string())?;
+    let found_libs = shims::scan_loadpaths(&library_load_paths).map_err(|e| e.to_string())?;
     info!("Found the following RefinedRust libraries in the loadpath: {:?}", found_libs);
 
     for incl in &includes {
diff --git a/rr_frontend/translation/src/shims/flat.rs b/rr_frontend/translation/src/shims/flat.rs
new file mode 100644
index 0000000..3700acc
--- /dev/null
+++ b/rr_frontend/translation/src/shims/flat.rs
@@ -0,0 +1,235 @@
+// © 2024, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+//! Provides a flat representation of types that is stable across compilations.
+
+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 serde::{Deserialize, Serialize};
+
+use crate::spec_parsers::get_export_as_attr;
+use crate::{types, utils, Environment};
+
+/// An item path that receives generic arguments.
+#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
+pub struct PathWithArgs {
+    path: Vec<String>,
+    /// An encoding of the GenericArgs for this definition.
+    /// This is `Some(ty)` if:
+    /// - the argument represents a type (not a constant or region)
+    /// - and the arg is not the trivial identity arg (in case of ADTs)
+    args: Vec<Option<Type>>,
+}
+
+impl PathWithArgs {
+    pub fn to_item<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<(DefId, Vec<Option<ty::GenericArg<'tcx>>>)> {
+        let did = utils::try_resolve_did(tcx, self.path.as_slice())?;
+
+        let mut ty_args = Vec::new();
+
+        for arg in &self.args {
+            if let Some(arg) = arg {
+                let ty = arg.to_type(tcx)?;
+                ty_args.push(Some(ty::GenericArg::from(ty)));
+            } else {
+                ty_args.push(None);
+            }
+        }
+
+        Some((did, ty_args))
+    }
+
+    /// `args` should be normalized already.
+    pub fn from_item<'tcx>(
+        env: &Environment<'tcx>,
+        did: DefId,
+        args: &[ty::GenericArg<'tcx>],
+    ) -> Option<Self> {
+        let path = get_export_path_for_did(env, did);
+        let mut flattened_args = Vec::new();
+        // TODO: how to represent type variables in case the definition is open?
+        let mut index = 0;
+        info!("flattening args {:?}", args);
+        for arg in args {
+            if let Some(ty) = arg.as_type() {
+                // TODO not quite right yet (see above)
+                if !ty.is_param(index) {
+                    let flattened_ty = convert_ty_to_flat_type(env, ty)?;
+                    flattened_args.push(Some(flattened_ty));
+                }
+                index += 1;
+            } else {
+                flattened_args.push(None);
+            }
+        }
+        Some(Self {
+            path,
+            args: flattened_args,
+        })
+    }
+}
+
+#[derive(Serialize, Deserialize)]
+#[serde(remote = "ty::IntTy")]
+pub enum IntTyDef {
+    Isize,
+    I8,
+    I16,
+    I32,
+    I64,
+    I128,
+}
+#[derive(Serialize, Deserialize)]
+#[serde(remote = "ty::UintTy")]
+pub enum UintTyDef {
+    Usize,
+    U8,
+    U16,
+    U32,
+    U64,
+    U128,
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
+/// A "flattened" representation of types that should be suitable serialized storage, and should be
+/// stable enough to resolve to the same actual type across compilations.
+/// Currently mostly geared to our trait resolution needs.
+pub enum Type {
+    /// Path + generic args
+    /// empty args represents the identity substitution
+    Adt(PathWithArgs),
+    #[serde(with = "IntTyDef")]
+    Int(ty::IntTy),
+    #[serde(with = "UintTyDef")]
+    Uint(ty::UintTy),
+    Char,
+    Bool,
+    // TODO: more cases
+}
+
+impl Type {
+    /// Try to convert a flat type to a type.
+    pub fn to_type<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<ty::Ty<'tcx>> {
+        match self {
+            Self::Adt(path_with_args) => {
+                let (did, flat_args) = path_with_args.to_item(tcx)?;
+
+                let ty: ty::EarlyBinder<ty::Ty<'tcx>> = tcx.type_of(did);
+                let ty::TyKind::Adt(_, args) = ty.skip_binder().kind() else {
+                    return None;
+                };
+
+                // build substitution
+                let mut substs = Vec::new();
+                for (ty_arg, flat_arg) in args.iter().zip(flat_args.into_iter()) {
+                    match ty_arg.unpack() {
+                        ty::GenericArgKind::Type(_) => {
+                            if let Some(flat_arg) = flat_arg {
+                                substs.push(flat_arg);
+                            }
+                        },
+                        _ => {
+                            substs.push(ty_arg);
+                        },
+                    }
+                }
+
+                // substitute
+                info!("substituting {:?} with {:?}", ty, substs);
+                let subst_ty =
+                    if substs.is_empty() { ty.instantiate_identity() } else { ty.instantiate(tcx, &substs) };
+
+                Some(subst_ty)
+            },
+            Self::Bool => Some(tcx.mk_ty_from_kind(ty::TyKind::Bool)),
+            Self::Char => Some(tcx.mk_ty_from_kind(ty::TyKind::Char)),
+            Self::Int(it) => Some(tcx.mk_ty_from_kind(ty::TyKind::Int(it.to_owned()))),
+            Self::Uint(it) => Some(tcx.mk_ty_from_kind(ty::TyKind::Uint(it.to_owned()))),
+        }
+    }
+}
+
+/// Try to convert a type to a flat type. Assumes the type has been normalized already.
+pub fn convert_ty_to_flat_type<'tcx>(env: &Environment<'tcx>, ty: ty::Ty<'tcx>) -> Option<Type> {
+    match ty.kind() {
+        ty::TyKind::Adt(def, args) => {
+            let did = def.did();
+            // TODO: if this is downcast to a variant, this might not work
+            let path_with_args = PathWithArgs::from_item(env, did, args.as_slice())?;
+            Some(Type::Adt(path_with_args))
+        },
+        ty::TyKind::Bool => Some(Type::Bool),
+        ty::TyKind::Char => Some(Type::Char),
+        ty::TyKind::Int(it) => Some(Type::Int(it.to_owned())),
+        ty::TyKind::Uint(it) => Some(Type::Uint(it.to_owned())),
+        _ => None,
+    }
+}
+
+pub fn get_cleaned_def_path(tcx: TyCtxt<'_>, did: DefId) -> Vec<String> {
+    let def_path = tcx.def_path_str(did);
+    // we clean this up a bit and segment it
+    let mut components = Vec::new();
+    for i in def_path.split("::") {
+        if i.starts_with('<') && i.ends_with('>') {
+            // this is a generic specialization, skip
+            continue;
+        }
+        components.push(i.to_owned());
+    }
+    info!("split def path {:?} to {:?}", def_path, components);
+
+    components
+}
+
+// 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: &hir::definitions::DefPath) -> Vec<String> {
+    let mut components = Vec::new();
+    for p in &path.data {
+        if let Some(name) = p.data.get_opt_name() {
+            components.push(name.as_str().to_owned());
+        }
+    }
+    components
+}
+
+/// Get the path we should export an item at.
+pub fn get_export_path_for_did(env: &Environment, did: DefId) -> Vec<String> {
+    let attrs = env.get_attributes(did);
+
+    if utils::has_tool_attr(attrs, "export_as") {
+        let filtered_attrs = utils::filter_tool_attrs(attrs);
+
+        return get_export_as_attr(filtered_attrs.as_slice()).unwrap();
+    }
+
+    // Check for an annotation on the surrounding impl
+    if let Some(impl_did) = env.tcx().impl_of_method(did) {
+        let attrs = env.get_attributes(impl_did);
+
+        if utils::has_tool_attr(attrs, "export_as") {
+            let filtered_attrs = utils::filter_tool_attrs(attrs);
+            let mut path_prefix = get_export_as_attr(filtered_attrs.as_slice()).unwrap();
+
+            // push the last component of this path
+            //let def_path = env.tcx().def_path(did);
+            let mut this_path = get_cleaned_def_path(env.tcx(), did);
+            path_prefix.push(this_path.pop().unwrap());
+
+            return path_prefix;
+        }
+    }
+
+    get_cleaned_def_path(env.tcx(), did)
+}
diff --git a/rr_frontend/translation/src/shims/mod.rs b/rr_frontend/translation/src/shims/mod.rs
new file mode 100644
index 0000000..2d0d3cc
--- /dev/null
+++ b/rr_frontend/translation/src/shims/mod.rs
@@ -0,0 +1,50 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+pub mod flat;
+pub mod registry;
+
+use std::collections::{HashMap, HashSet};
+use std::fs::File;
+use std::io::{Read, Write};
+use std::path::{Path, PathBuf};
+use std::{fs, io, process};
+
+/// Find `RefinedRust` modules in the given loadpath.
+fn scan_loadpath(path: &Path, storage: &mut HashMap<String, PathBuf>) -> io::Result<()> {
+    if path.is_dir() {
+        for entry in fs::read_dir(path)? {
+            let entry = entry?;
+            let path = entry.path();
+            if path.is_dir() {
+                scan_loadpath(path.as_path(), storage)?;
+            } else if path.is_file() {
+                if let Some(ext) = path.extension() {
+                    if Some("rrlib") == ext.to_str() {
+                        // try to open this rrlib file
+                        let f = File::open(path.clone())?;
+                        if let Some(name) = registry::is_valid_refinedrust_module(f) {
+                            storage.insert(name, path);
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    Ok(())
+}
+
+/// Find `RefinedRust` modules in the given loadpaths.
+pub fn scan_loadpaths(paths: &[PathBuf]) -> io::Result<HashMap<String, PathBuf>> {
+    let mut found_lib_files: HashMap<String, PathBuf> = HashMap::new();
+
+    for path in paths {
+        scan_loadpath(path, &mut found_lib_files)?;
+    }
+
+    Ok(found_lib_files)
+}
diff --git a/rr_frontend/translation/src/shim_registry.rs b/rr_frontend/translation/src/shims/registry.rs
similarity index 96%
rename from rr_frontend/translation/src/shim_registry.rs
rename to rr_frontend/translation/src/shims/registry.rs
index e6e0247..aed0374 100644
--- a/rr_frontend/translation/src/shim_registry.rs
+++ b/rr_frontend/translation/src/shims/registry.rs
@@ -4,10 +4,11 @@
 // 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/.
 
+//! Registry of shims for Rust functions that get mapped to custom `RefinedRust`
+//! implementations.
+//! Provides deserialization from a JSON file defining this registry.
+
 use std::collections::{HashMap, HashSet};
-/// Registry of shims for Rust functions that get mapped to custom `RefinedRust`
-/// implementations.
-/// Provides deserialization from a JSON file defining this registry.
 use std::fs::File;
 use std::io::{BufReader, BufWriter};
 
@@ -16,6 +17,7 @@ use radium::coq;
 use serde::{Deserialize, Serialize};
 use typed_arena::Arena;
 
+use crate::shims::flat;
 use crate::utils::*;
 
 type Path<'a> = Vec<&'a str>;
@@ -62,9 +64,9 @@ struct ShimTraitEntry {
 #[derive(Serialize, Deserialize)]
 struct ShimTraitImplEntry {
     /// The rustc path for the trait
-    trait_path: PathWithArgs,
+    trait_path: flat::PathWithArgs,
     /// for which type is this implementation?
-    for_type: FlatType,
+    for_type: flat::Type,
     // TODO: additional constraints like the required clauses for disambiguation
     /// a kind: always "trait_impl"
     kind: String,
@@ -86,9 +88,9 @@ struct ShimTraitImplEntry {
 #[derive(Serialize, Deserialize)]
 struct ShimTraitMethodImplEntry {
     /// The rustc path for the trait
-    trait_path: PathWithArgs,
+    trait_path: flat::PathWithArgs,
     /// for which type is this implementation?
-    for_type: FlatType,
+    for_type: flat::Type,
     // TODO: additional constraints like the required clauses for disambiguation
     /// The method identifier
     method_ident: String,
@@ -146,8 +148,8 @@ impl<'a> From<FunctionShim<'a>> for ShimFunctionEntry {
 
 #[derive(Clone, Eq, PartialEq, Debug)]
 pub struct TraitImplShim {
-    pub trait_path: PathWithArgs,
-    pub for_type: FlatType,
+    pub trait_path: flat::PathWithArgs,
+    pub for_type: flat::Type,
 
     pub method_specs: HashMap<String, (String, String)>,
 
@@ -173,9 +175,9 @@ impl From<TraitImplShim> for ShimTraitImplEntry {
 
 #[derive(Clone, Eq, PartialEq, Debug)]
 pub struct TraitMethodImplShim {
-    pub trait_path: PathWithArgs,
+    pub trait_path: flat::PathWithArgs,
     pub method_ident: String,
-    pub for_type: FlatType,
+    pub for_type: flat::Type,
     pub name: String,
     pub spec_name: String,
 }
@@ -243,16 +245,9 @@ impl<'a> From<AdtShim<'a>> for ShimAdtEntry {
     }
 }
 
-pub struct ModuleSummary<'a> {
-    /// function/method shims
-    function_shims: Vec<FunctionShim<'a>>,
-    /// adt shims
-    adt_shims: Vec<AdtShim<'a>>,
-}
-
 /// Registry of function shims loaded by the user. Substitutes path to the function/method with a
 /// code definition name and a spec name.
-pub struct ShimRegistry<'a> {
+pub struct SR<'a> {
     arena: &'a Arena<String>,
 
     /// function/method shims
@@ -277,7 +272,7 @@ pub struct ShimRegistry<'a> {
     dependencies: Vec<coq::module::DirPath>,
 }
 
-impl<'a> ShimRegistry<'a> {
+impl<'a> SR<'a> {
     fn get_shim_kind(v: &serde_json::Value) -> Result<ShimKind, String> {
         let obj = v.as_object().ok_or_else(|| "element is not an object".to_owned())?;
         let vk = obj.get("kind").ok_or_else(|| "object does not have \"kind\" attribute".to_owned())?;
@@ -316,7 +311,7 @@ impl<'a> ShimRegistry<'a> {
         }
     }
 
-    pub fn new(arena: &'a Arena<String>) -> Result<ShimRegistry<'a>, String> {
+    pub fn new(arena: &'a Arena<String>) -> Result<SR<'a>, String> {
         let mut reg = Self::empty(arena);
 
         match rrconfig::shim_file() {
diff --git a/rr_frontend/translation/src/traits/requirements.rs b/rr_frontend/translation/src/traits/requirements.rs
index 23fc766..c9667e3 100644
--- a/rr_frontend/translation/src/traits/requirements.rs
+++ b/rr_frontend/translation/src/traits/requirements.rs
@@ -12,7 +12,7 @@ use log::{info, trace};
 use rr_rustc_interface::hir::def_id::DefId;
 use rr_rustc_interface::middle::ty;
 
-use crate::utils;
+use crate::{shims, utils};
 
 /// Get non-trivial trait requirements of a `ParamEnv`,
 /// ordered deterministically.
@@ -137,8 +137,8 @@ fn cmp_trait_ref<'tcx>(
         }
     }
 
-    let path_a = utils::get_cleaned_def_path(tcx, a.def_id);
-    let path_b = utils::get_cleaned_def_path(tcx, b.def_id);
+    let path_a = shims::flat::get_cleaned_def_path(tcx, a.def_id);
+    let path_b = shims::flat::get_cleaned_def_path(tcx, b.def_id);
     let path_cmp = path_a.cmp(&path_b);
     info!("cmp_trait_ref: comparing paths {path_a:?} and {path_b:?}");
 
diff --git a/rr_frontend/translation/src/utils.rs b/rr_frontend/translation/src/utils.rs
index db890b1..ac0ecc2 100644
--- a/rr_frontend/translation/src/utils.rs
+++ b/rr_frontend/translation/src/utils.rs
@@ -29,220 +29,6 @@ pub fn strip_coq_ident(s: &str) -> String {
         .replace(|c: char| !(c.is_alphanumeric() || c == '_'), "")
 }
 
-/// An item path that receives generic arguments.
-#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
-pub struct PathWithArgs {
-    path: Vec<String>,
-    /// An encoding of the GenericArgs for this definition.
-    /// This is `Some(ty)` if:
-    /// - the argument represents a type (not a constant or region)
-    /// - and the arg is not the trivial identity arg (in case of ADTs)
-    args: Vec<Option<FlatType>>,
-}
-
-impl PathWithArgs {
-    pub fn to_item<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<(DefId, Vec<Option<ty::GenericArg<'tcx>>>)> {
-        let did = try_resolve_did(tcx, self.path.as_slice())?;
-
-        let mut ty_args = Vec::new();
-
-        for arg in &self.args {
-            if let Some(arg) = arg {
-                let ty = arg.to_type(tcx)?;
-                ty_args.push(Some(ty::GenericArg::from(ty)));
-            } else {
-                ty_args.push(None);
-            }
-        }
-
-        Some((did, ty_args))
-    }
-
-    /// `args` should be normalized already.
-    pub fn from_item<'tcx>(
-        env: &Environment<'tcx>,
-        did: DefId,
-        args: &[ty::GenericArg<'tcx>],
-    ) -> Option<Self> {
-        let path = get_export_path_for_did(env, did);
-        let mut flattened_args = Vec::new();
-        // TODO: how to represent type variables in case the definition is open?
-        let mut index = 0;
-        info!("flattening args {:?}", args);
-        for arg in args {
-            if let Some(ty) = arg.as_type() {
-                // TODO not quite right yet (see above)
-                if !ty.is_param(index) {
-                    let flattened_ty = convert_ty_to_flat_type(env, ty)?;
-                    flattened_args.push(Some(flattened_ty));
-                }
-                index += 1;
-            } else {
-                flattened_args.push(None);
-            }
-        }
-        Some(Self {
-            path,
-            args: flattened_args,
-        })
-    }
-}
-
-#[derive(Serialize, Deserialize)]
-#[serde(remote = "ty::IntTy")]
-pub enum IntTyDef {
-    Isize,
-    I8,
-    I16,
-    I32,
-    I64,
-    I128,
-}
-#[derive(Serialize, Deserialize)]
-#[serde(remote = "ty::UintTy")]
-pub enum UintTyDef {
-    Usize,
-    U8,
-    U16,
-    U32,
-    U64,
-    U128,
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
-/// A "flattened" representation of types that should be suitable serialized storage, and should be
-/// stable enough to resolve to the same actual type across compilations.
-/// Currently mostly geared to our trait resolution needs.
-pub enum FlatType {
-    /// Path + generic args
-    /// empty args represents the identity substitution
-    Adt(PathWithArgs),
-    #[serde(with = "IntTyDef")]
-    Int(ty::IntTy),
-    #[serde(with = "UintTyDef")]
-    Uint(ty::UintTy),
-    Char,
-    Bool,
-    // TODO: more cases
-}
-
-impl FlatType {
-    /// Try to convert a flat type to a type.
-    pub fn to_type<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<ty::Ty<'tcx>> {
-        match self {
-            Self::Adt(path_with_args) => {
-                let (did, flat_args) = path_with_args.to_item(tcx)?;
-
-                let ty: ty::EarlyBinder<ty::Ty<'tcx>> = tcx.type_of(did);
-                let ty::TyKind::Adt(_, args) = ty.skip_binder().kind() else {
-                    return None;
-                };
-
-                // build substitution
-                let mut substs = Vec::new();
-                for (ty_arg, flat_arg) in args.iter().zip(flat_args.into_iter()) {
-                    match ty_arg.unpack() {
-                        ty::GenericArgKind::Type(_) => {
-                            if let Some(flat_arg) = flat_arg {
-                                substs.push(flat_arg);
-                            }
-                        },
-                        _ => {
-                            substs.push(ty_arg);
-                        },
-                    }
-                }
-
-                // substitute
-                info!("substituting {:?} with {:?}", ty, substs);
-                let subst_ty =
-                    if substs.is_empty() { ty.instantiate_identity() } else { ty.instantiate(tcx, &substs) };
-
-                Some(subst_ty)
-            },
-            Self::Bool => Some(tcx.mk_ty_from_kind(ty::TyKind::Bool)),
-            Self::Char => Some(tcx.mk_ty_from_kind(ty::TyKind::Char)),
-            Self::Int(it) => Some(tcx.mk_ty_from_kind(ty::TyKind::Int(it.to_owned()))),
-            Self::Uint(it) => Some(tcx.mk_ty_from_kind(ty::TyKind::Uint(it.to_owned()))),
-        }
-    }
-}
-
-/// Try to convert a type to a flat type. Assumes the type has been normalized already.
-pub fn convert_ty_to_flat_type<'tcx>(env: &Environment<'tcx>, ty: ty::Ty<'tcx>) -> Option<FlatType> {
-    match ty.kind() {
-        ty::TyKind::Adt(def, args) => {
-            let did = def.did();
-            // TODO: if this is downcast to a variant, this might not work
-            let path_with_args = PathWithArgs::from_item(env, did, args.as_slice())?;
-            Some(FlatType::Adt(path_with_args))
-        },
-        ty::TyKind::Bool => Some(FlatType::Bool),
-        ty::TyKind::Char => Some(FlatType::Char),
-        ty::TyKind::Int(it) => Some(FlatType::Int(it.to_owned())),
-        ty::TyKind::Uint(it) => Some(FlatType::Uint(it.to_owned())),
-        _ => None,
-    }
-}
-
-pub fn get_cleaned_def_path(tcx: TyCtxt<'_>, did: DefId) -> Vec<String> {
-    let def_path = tcx.def_path_str(did);
-    // we clean this up a bit and segment it
-    let mut components = Vec::new();
-    for i in def_path.split("::") {
-        if i.starts_with('<') && i.ends_with('>') {
-            // this is a generic specialization, skip
-            continue;
-        }
-        components.push(i.to_owned());
-    }
-    info!("split def path {:?} to {:?}", def_path, components);
-
-    components
-}
-
-// 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: &hir::definitions::DefPath) -> Vec<String> {
-    let mut components = Vec::new();
-    for p in &path.data {
-        if let Some(name) = p.data.get_opt_name() {
-            components.push(name.as_str().to_owned());
-        }
-    }
-    components
-}
-
-/// Get the path we should export an item at.
-pub fn get_export_path_for_did(env: &Environment, did: DefId) -> Vec<String> {
-    let attrs = env.get_attributes(did);
-
-    if has_tool_attr(attrs, "export_as") {
-        let filtered_attrs = filter_tool_attrs(attrs);
-
-        return get_export_as_attr(filtered_attrs.as_slice()).unwrap();
-    }
-
-    // Check for an annotation on the surrounding impl
-    if let Some(impl_did) = env.tcx().impl_of_method(did) {
-        let attrs = env.get_attributes(impl_did);
-
-        if has_tool_attr(attrs, "export_as") {
-            let filtered_attrs = filter_tool_attrs(attrs);
-            let mut path_prefix = get_export_as_attr(filtered_attrs.as_slice()).unwrap();
-
-            // push the last component of this path
-            //let def_path = env.tcx().def_path(did);
-            let mut this_path = get_cleaned_def_path(env.tcx(), did);
-            path_prefix.push(this_path.pop().unwrap());
-
-            return path_prefix;
-        }
-    }
-
-    get_cleaned_def_path(env.tcx(), did)
-}
-
 /// Gets an instance for a path.
 /// Taken from Miri <https://github.com/rust-lang/miri/blob/31fb32e49f42df19b45baccb6aa80c3d726ed6d5/src/helpers.rs#L48>.
 pub fn try_resolve_did_direct<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
-- 
GitLab