Skip to content
Snippets Groups Projects
Verified Commit a7cbdd14 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

refactor shims

parent 7f55bf30
No related branches found
No related tags found
1 merge request!61Refactor translation crate
Pipeline #113640 passed
// © 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. // 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 // If a copy of the BSD-3-clause license was not distributed with this
...@@ -17,7 +17,7 @@ mod force_matches_macro; ...@@ -17,7 +17,7 @@ mod force_matches_macro;
mod function_body; mod function_body;
mod inclusion_tracker; mod inclusion_tracker;
mod regions; mod regions;
mod shim_registry; mod shims;
mod spec_parsers; mod spec_parsers;
mod traits; mod traits;
mod types; mod types;
...@@ -39,6 +39,7 @@ use typed_arena::Arena; ...@@ -39,6 +39,7 @@ use typed_arena::Arena;
use crate::environment::Environment; use crate::environment::Environment;
use crate::function_body::{ConstScope, FunctionTranslator, ProcedureMode, ProcedureScope}; 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::const_attr_parser::{ConstAttrParser, VerboseConstAttrParser};
use crate::spec_parsers::crate_attr_parser::{CrateAttrParser, VerboseCrateAttrParser}; use crate::spec_parsers::crate_attr_parser::{CrateAttrParser, VerboseCrateAttrParser};
use crate::spec_parsers::module_attr_parser::{ModuleAttrParser, ModuleAttrs, VerboseModuleAttrParser}; use crate::spec_parsers::module_attr_parser::{ModuleAttrParser, ModuleAttrs, VerboseModuleAttrParser};
...@@ -92,7 +93,7 @@ pub struct VerificationCtxt<'tcx, 'rcx> { ...@@ -92,7 +93,7 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
coq_path_prefix: String, coq_path_prefix: String,
dune_package: Option<String>, dune_package: Option<String>,
shim_registry: shim_registry::ShimRegistry<'rcx>, shim_registry: shims::registry::SR<'rcx>,
/// trait implementations we generated /// trait implementations we generated
trait_impls: HashMap<DefId, radium::TraitImplSpec<'rcx>>, trait_impls: HashMap<DefId, radium::TraitImplSpec<'rcx>>,
...@@ -100,12 +101,12 @@ pub struct VerificationCtxt<'tcx, 'rcx> { ...@@ -100,12 +101,12 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
fn get_path_for_shim(&self, did: DefId) -> Vec<&str> { 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); let interned_path = self.shim_registry.intern_path(path);
interned_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 { let Some(mode) = self.procedure_registry.lookup_function_mode(did) else {
return None; return None;
}; };
...@@ -175,11 +176,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { ...@@ -175,11 +176,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let impl_for = args[0].expect_ty(); let impl_for = args[0].expect_ty();
// flatten the trait reference // 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); trace!("got trait path: {:?}", trait_path);
// flatten the self type. // 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; return None;
}; };
...@@ -236,11 +237,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { ...@@ -236,11 +237,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let impl_for = args[0].expect_ty(); let impl_for = args[0].expect_ty();
// flatten the trait reference // 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); trace!("got trait path: {:?}", trait_path);
// flatten the self type. // 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)"); trace!("leave make_impl_shim_entry (failed transating self type)");
return None; return None;
}; };
...@@ -407,7 +408,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { ...@@ -407,7 +408,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
info!("Generated module summary functions: {:?}", function_shims); info!("Generated module summary functions: {:?}", function_shims);
let interface_file = File::create(path).unwrap(); let interface_file = File::create(path).unwrap();
shim_registry::write_shims( shims::registry::write_shims(
interface_file, interface_file,
module_path, module_path,
module, module,
...@@ -1397,7 +1398,7 @@ fn register_trait_impls(vcx: &VerificationCtxt<'_, '_>) -> Result<(), String> { ...@@ -1397,7 +1398,7 @@ fn register_trait_impls(vcx: &VerificationCtxt<'_, '_>) -> Result<(), String> {
Ok(()) Ok(())
} }
/// Generate trait instances /// Generate trait instances.
fn assemble_trait_impls<'tcx, 'rcx>( fn assemble_trait_impls<'tcx, 'rcx>(
vcx: &mut VerificationCtxt<'tcx, 'rcx>, vcx: &mut VerificationCtxt<'tcx, 'rcx>,
) -> Result<(), base::TranslationError<'tcx>> { ) -> Result<(), base::TranslationError<'tcx>> {
...@@ -1467,42 +1468,6 @@ pub fn get_module_attributes(env: &Environment<'_>) -> Result<HashMap<LocalDefId ...@@ -1467,42 +1468,6 @@ pub fn get_module_attributes(env: &Environment<'_>) -> Result<HashMap<LocalDefId
Ok(attrs) 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. /// Translate a crate, creating a `VerificationCtxt` in the process.
pub fn generate_coq_code<'tcx, F>(tcx: ty::TyCtxt<'tcx>, continuation: F) -> Result<(), String> pub fn generate_coq_code<'tcx, F>(tcx: ty::TyCtxt<'tcx>, continuation: F) -> Result<(), String>
where where
...@@ -1568,12 +1533,12 @@ where ...@@ -1568,12 +1533,12 @@ where
); );
let procedure_registry = ProcedureScope::new(); let procedure_registry = ProcedureScope::new();
let shim_string_arena = Arena::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 // add includes to the shim registry
let library_load_paths = rrconfig::lib_load_paths(); let library_load_paths = rrconfig::lib_load_paths();
info!("Loading libraries from {:?}", library_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); info!("Found the following RefinedRust libraries in the loadpath: {:?}", found_libs);
for incl in &includes { for incl in &includes {
......
// © 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)
}
// © 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)
}
...@@ -4,10 +4,11 @@ ...@@ -4,10 +4,11 @@
// If a copy of the BSD-3-clause license was not distributed with this // 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/. // 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}; 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::fs::File;
use std::io::{BufReader, BufWriter}; use std::io::{BufReader, BufWriter};
...@@ -16,6 +17,7 @@ use radium::coq; ...@@ -16,6 +17,7 @@ use radium::coq;
use serde::{Deserialize, Serialize}; use serde::{Deserialize, Serialize};
use typed_arena::Arena; use typed_arena::Arena;
use crate::shims::flat;
use crate::utils::*; use crate::utils::*;
type Path<'a> = Vec<&'a str>; type Path<'a> = Vec<&'a str>;
...@@ -62,9 +64,9 @@ struct ShimTraitEntry { ...@@ -62,9 +64,9 @@ struct ShimTraitEntry {
#[derive(Serialize, Deserialize)] #[derive(Serialize, Deserialize)]
struct ShimTraitImplEntry { struct ShimTraitImplEntry {
/// The rustc path for the trait /// The rustc path for the trait
trait_path: PathWithArgs, trait_path: flat::PathWithArgs,
/// for which type is this implementation? /// for which type is this implementation?
for_type: FlatType, for_type: flat::Type,
// TODO: additional constraints like the required clauses for disambiguation // TODO: additional constraints like the required clauses for disambiguation
/// a kind: always "trait_impl" /// a kind: always "trait_impl"
kind: String, kind: String,
...@@ -86,9 +88,9 @@ struct ShimTraitImplEntry { ...@@ -86,9 +88,9 @@ struct ShimTraitImplEntry {
#[derive(Serialize, Deserialize)] #[derive(Serialize, Deserialize)]
struct ShimTraitMethodImplEntry { struct ShimTraitMethodImplEntry {
/// The rustc path for the trait /// The rustc path for the trait
trait_path: PathWithArgs, trait_path: flat::PathWithArgs,
/// for which type is this implementation? /// for which type is this implementation?
for_type: FlatType, for_type: flat::Type,
// TODO: additional constraints like the required clauses for disambiguation // TODO: additional constraints like the required clauses for disambiguation
/// The method identifier /// The method identifier
method_ident: String, method_ident: String,
...@@ -146,8 +148,8 @@ impl<'a> From<FunctionShim<'a>> for ShimFunctionEntry { ...@@ -146,8 +148,8 @@ impl<'a> From<FunctionShim<'a>> for ShimFunctionEntry {
#[derive(Clone, Eq, PartialEq, Debug)] #[derive(Clone, Eq, PartialEq, Debug)]
pub struct TraitImplShim { pub struct TraitImplShim {
pub trait_path: PathWithArgs, pub trait_path: flat::PathWithArgs,
pub for_type: FlatType, pub for_type: flat::Type,
pub method_specs: HashMap<String, (String, String)>, pub method_specs: HashMap<String, (String, String)>,
...@@ -173,9 +175,9 @@ impl From<TraitImplShim> for ShimTraitImplEntry { ...@@ -173,9 +175,9 @@ impl From<TraitImplShim> for ShimTraitImplEntry {
#[derive(Clone, Eq, PartialEq, Debug)] #[derive(Clone, Eq, PartialEq, Debug)]
pub struct TraitMethodImplShim { pub struct TraitMethodImplShim {
pub trait_path: PathWithArgs, pub trait_path: flat::PathWithArgs,
pub method_ident: String, pub method_ident: String,
pub for_type: FlatType, pub for_type: flat::Type,
pub name: String, pub name: String,
pub spec_name: String, pub spec_name: String,
} }
...@@ -243,16 +245,9 @@ impl<'a> From<AdtShim<'a>> for ShimAdtEntry { ...@@ -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 /// Registry of function shims loaded by the user. Substitutes path to the function/method with a
/// code definition name and a spec name. /// code definition name and a spec name.
pub struct ShimRegistry<'a> { pub struct SR<'a> {
arena: &'a Arena<String>, arena: &'a Arena<String>,
/// function/method shims /// function/method shims
...@@ -277,7 +272,7 @@ pub struct ShimRegistry<'a> { ...@@ -277,7 +272,7 @@ pub struct ShimRegistry<'a> {
dependencies: Vec<coq::module::DirPath>, dependencies: Vec<coq::module::DirPath>,
} }
impl<'a> ShimRegistry<'a> { impl<'a> SR<'a> {
fn get_shim_kind(v: &serde_json::Value) -> Result<ShimKind, String> { 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 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())?; let vk = obj.get("kind").ok_or_else(|| "object does not have \"kind\" attribute".to_owned())?;
...@@ -316,7 +311,7 @@ impl<'a> ShimRegistry<'a> { ...@@ -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); let mut reg = Self::empty(arena);
match rrconfig::shim_file() { match rrconfig::shim_file() {
......
...@@ -12,7 +12,7 @@ use log::{info, trace}; ...@@ -12,7 +12,7 @@ use log::{info, trace};
use rr_rustc_interface::hir::def_id::DefId; use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::ty; use rr_rustc_interface::middle::ty;
use crate::utils; use crate::{shims, utils};
/// Get non-trivial trait requirements of a `ParamEnv`, /// Get non-trivial trait requirements of a `ParamEnv`,
/// ordered deterministically. /// ordered deterministically.
...@@ -137,8 +137,8 @@ fn cmp_trait_ref<'tcx>( ...@@ -137,8 +137,8 @@ fn cmp_trait_ref<'tcx>(
} }
} }
let path_a = utils::get_cleaned_def_path(tcx, a.def_id); let path_a = shims::flat::get_cleaned_def_path(tcx, a.def_id);
let path_b = utils::get_cleaned_def_path(tcx, b.def_id); let path_b = shims::flat::get_cleaned_def_path(tcx, b.def_id);
let path_cmp = path_a.cmp(&path_b); let path_cmp = path_a.cmp(&path_b);
info!("cmp_trait_ref: comparing paths {path_a:?} and {path_b:?}"); info!("cmp_trait_ref: comparing paths {path_a:?} and {path_b:?}");
......
...@@ -29,220 +29,6 @@ pub fn strip_coq_ident(s: &str) -> String { ...@@ -29,220 +29,6 @@ pub fn strip_coq_ident(s: &str) -> String {
.replace(|c: char| !(c.is_alphanumeric() || c == '_'), "") .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. /// Gets an instance for a path.
/// Taken from Miri <https://github.com/rust-lang/miri/blob/31fb32e49f42df19b45baccb6aa80c3d726ed6d5/src/helpers.rs#L48>. /// 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> pub fn try_resolve_did_direct<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment