From 766cae6ca70243940829b25d577dbc2da8dbec06 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Thu, 2 Jan 2025 15:31:58 +0100
Subject: [PATCH] clean up utils
---
rr_frontend/translation/src/attrs.rs | 82 ++++
rr_frontend/translation/src/base.rs | 9 +
.../translation/src/environment/mod.rs | 12 +-
rr_frontend/translation/src/function_body.rs | 17 +-
rr_frontend/translation/src/lib.rs | 40 +-
rr_frontend/translation/src/search.rs | 323 +++++++++++++++
rr_frontend/translation/src/shims/flat.rs | 12 +-
.../translation/src/traits/registry.rs | 14 +-
.../translation/src/traits/requirements.rs | 12 +-
rr_frontend/translation/src/types/local.rs | 4 +-
rr_frontend/translation/src/types/mod.rs | 6 +-
rr_frontend/translation/src/types/scope.rs | 8 +-
.../translation/src/types/translator.rs | 30 +-
rr_frontend/translation/src/utils.rs | 390 +-----------------
14 files changed, 496 insertions(+), 463 deletions(-)
create mode 100644 rr_frontend/translation/src/attrs.rs
create mode 100644 rr_frontend/translation/src/search.rs
diff --git a/rr_frontend/translation/src/attrs.rs b/rr_frontend/translation/src/attrs.rs
new file mode 100644
index 0000000..43040e5
--- /dev/null
+++ b/rr_frontend/translation/src/attrs.rs
@@ -0,0 +1,82 @@
+// © 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
+// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
+
+//! Utility functions for obtaining relevant attributes.
+
+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::{force_matches, types, Environment};
+
+/// Check if `<tool>::<name>` is among the attributes, where `tool` is determined by the
+/// `spec_hotword` config.
+/// Any arguments of the attribute are ignored.
+pub fn has_tool_attr(attrs: &[ast::Attribute], name: &str) -> bool {
+ get_tool_attr(attrs, name).is_some()
+}
+
+/// Get the arguments for a tool attribute, if it exists.
+pub fn get_tool_attr<'a>(attrs: &'a [ast::Attribute], name: &str) -> Option<&'a ast::AttrArgs> {
+ attrs.iter().find_map(|attr| match &attr.kind {
+ ast::AttrKind::Normal(na) => {
+ let segments = &na.item.path.segments;
+ let args = &na.item.args;
+ (segments.len() == 2
+ && segments[0].ident.as_str() == rrconfig::spec_hotword().as_str()
+ && segments[1].ident.as_str() == name)
+ .then_some(args)
+ },
+ _ => None,
+ })
+}
+
+/// Check if `<tool>::name` is among the filtered attributes.
+pub fn has_tool_attr_filtered(attrs: &[&ast::AttrItem], name: &str) -> bool {
+ attrs.iter().any(|item| {
+ let segments = &item.path.segments;
+ segments.len() == 2
+ && segments[0].ident.as_str() == rrconfig::spec_hotword().as_str()
+ && segments[1].ident.as_str() == name
+ })
+}
+
+/// Check if any attribute starting with `<tool>` is among the attributes.
+pub fn has_any_tool_attr(attrs: &[ast::Attribute]) -> bool {
+ attrs.iter().any(|attr| match &attr.kind {
+ ast::AttrKind::Normal(na) => {
+ let segments = &na.item.path.segments;
+ segments[0].ident.as_str() == rrconfig::spec_hotword().as_str()
+ },
+ _ => false,
+ })
+}
+
+/// Get all tool attributes, i.e. attributes of the shape `<tool>::attr`, where `tool` is
+/// determined by the `spec_hotword` config.
+pub fn filter_for_tool(attrs: &[ast::Attribute]) -> Vec<&ast::AttrItem> {
+ attrs
+ .iter()
+ .filter_map(|attr| match &attr.kind {
+ ast::AttrKind::Normal(na) => {
+ let item = &na.item;
+
+ let seg = item.path.segments.get(0)?;
+
+ (seg.ident.name.as_str() == rrconfig::spec_hotword()).then_some(item)
+ },
+ _ => None,
+ })
+ .collect()
+}
diff --git a/rr_frontend/translation/src/base.rs b/rr_frontend/translation/src/base.rs
index d4ef60a..2d61977 100644
--- a/rr_frontend/translation/src/base.rs
+++ b/rr_frontend/translation/src/base.rs
@@ -13,6 +13,15 @@ use rr_rustc_interface::polonius_engine::FactTypes;
use crate::environment::borrowck::facts;
use crate::traits;
+/// Strip symbols from an identifier to be compatible with Coq.
+/// In particular things like ' or ::.
+pub fn strip_coq_ident(s: &str) -> String {
+ String::from(s)
+ .replace('\'', "")
+ .replace("::", "_")
+ .replace(|c: char| !(c.is_alphanumeric() || c == '_'), "")
+}
+
pub type Region = <RustcFacts as FactTypes>::Origin;
pub type Loan = <RustcFacts as FactTypes>::Loan;
pub type PointIndex = <RustcFacts as FactTypes>::Point;
diff --git a/rr_frontend/translation/src/environment/mod.rs b/rr_frontend/translation/src/environment/mod.rs
index e46f060..65f8997 100644
--- a/rr_frontend/translation/src/environment/mod.rs
+++ b/rr_frontend/translation/src/environment/mod.rs
@@ -32,13 +32,13 @@ use rr_rustc_interface::span::Span;
use rr_rustc_interface::trait_selection::infer::{InferCtxtExt, TyCtxtInferExt};
use rr_rustc_interface::{ast, span};
+use crate::attrs;
use crate::data::ProcedureDefId;
use crate::environment::borrowck::facts;
use crate::environment::collect_closure_defs_visitor::CollectClosureDefsVisitor;
use crate::environment::collect_prusti_spec_visitor::CollectPrustiSpecVisitor;
use crate::environment::loops::{PlaceAccess, PlaceAccessKind, ProcedureLoops};
use crate::environment::procedure::{BasicBlockIndex, Procedure};
-use crate::utils;
/// Facade to the Rust compiler.
// #[derive(Copy, Clone)]
@@ -211,7 +211,7 @@ impl<'tcx> Environment<'tcx> {
pub fn has_tool_attribute(&self, def_id: ProcedureDefId, name: &str) -> bool {
let tcx = self.tcx();
// TODO: migrate to get_attrs
- utils::has_tool_attr(tcx.get_attrs_unchecked(def_id), name)
+ attrs::has_tool_attr(tcx.get_attrs_unchecked(def_id), name)
}
/// Find whether the procedure has a particular `[tool]::<name>` attribute; if so, return its
@@ -219,14 +219,14 @@ impl<'tcx> Environment<'tcx> {
pub fn get_tool_attribute<'a>(&'a self, def_id: ProcedureDefId, name: &str) -> Option<&'a ast::AttrArgs> {
let tcx = self.tcx();
// TODO: migrate to get_attrs
- utils::get_tool_attr(tcx.get_attrs_unchecked(def_id), name)
+ attrs::get_tool_attr(tcx.get_attrs_unchecked(def_id), name)
}
/// Check whether the procedure has any `[tool]` attribute.
pub fn has_any_tool_attribute(&self, def_id: ProcedureDefId) -> bool {
let tcx = self.tcx();
// TODO: migrate to get_attrs
- utils::has_any_tool_attr(tcx.get_attrs_unchecked(def_id))
+ attrs::has_any_tool_attr(tcx.get_attrs_unchecked(def_id))
}
/// Get the attributes of an item (e.g. procedures).
@@ -245,11 +245,11 @@ impl<'tcx> Environment<'tcx> {
F: for<'a> Fn(&'a ast::ast::AttrItem) -> bool,
{
let attrs = self.get_attributes(did);
- let mut filtered_attrs = utils::filter_tool_attrs(attrs);
+ let mut filtered_attrs = attrs::filter_for_tool(attrs);
// also add selected attributes from the surrounding impl
if let Some(impl_did) = self.tcx().impl_of_method(did) {
let impl_attrs = self.get_attributes(impl_did);
- let filtered_impl_attrs = utils::filter_tool_attrs(impl_attrs);
+ let filtered_impl_attrs = attrs::filter_for_tool(impl_attrs);
filtered_attrs.extend(filtered_impl_attrs.into_iter().filter(|x| propagate_from_impl(x)));
}
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index e1b0fb6..2a1f4b3 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -35,7 +35,7 @@ use crate::spec_parsers::verbose_function_spec_parser::{
ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
};
use crate::traits::{registry, resolution};
-use crate::{regions, traits, types, utils};
+use crate::{base, regions, search, traits, types};
/// Get the syntypes of function arguments for a procedure call.
pub fn get_arg_syntypes_for_procedure_call<'tcx, 'def>(
@@ -950,7 +950,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
match *r {
ty::RegionKind::ReEarlyBound(r) => {
- let name = utils::strip_coq_ident(r.name.as_str());
+ let name = base::strip_coq_ident(r.name.as_str());
universal_lifetimes.insert(next_id, format!("ulft_{}", name));
lifetime_names.insert(name, next_id);
},
@@ -981,7 +981,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
match r {
ty::BoundRegionKind::BrNamed(_, sym) => {
- let mut region_name = utils::strip_coq_ident(sym.as_str());
+ let mut region_name = base::strip_coq_ident(sym.as_str());
if region_name == "_" {
region_name = next_id.as_usize().to_string();
universal_lifetimes.insert(next_id, format!("ulft_{}", region_name));
@@ -1351,7 +1351,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
.trait_registry
.lookup_trait(trait_did)
.ok_or_else(|| TranslationError::TraitResolution(format!("{trait_did:?}")))?;
- let fn_name = utils::strip_coq_ident(self.env.tcx().item_name(self.proc.get_id()).as_str());
+ let fn_name = base::strip_coq_ident(self.env.tcx().item_name(self.proc.get_id()).as_str());
let trait_info = self.trait_registry.get_trait_impl_info(impl_did)?;
//self.trait_registry.lookup_impl(impl_did)?;
@@ -1403,7 +1403,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
/// `used_names` keeps track of the Rust source code names that have already been used.
fn make_local_name(mir_body: &Body<'tcx>, local: Local, used_names: &mut HashSet<String>) -> String {
if let Some(mir_name) = Self::find_name_for_local(mir_body, local, used_names) {
- let name = utils::strip_coq_ident(&mir_name);
+ let name = base::strip_coq_ident(&mir_name);
used_names.insert(mir_name);
name
} else {
@@ -2159,7 +2159,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
};
if let Some(panic_id_std) =
- utils::try_resolve_did(self.env.tcx(), &["std", "panicking", "begin_panic"])
+ search::try_resolve_did(self.env.tcx(), &["std", "panicking", "begin_panic"])
{
if panic_id_std == *did {
return true;
@@ -2168,7 +2168,8 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
warn!("Failed to determine DefId of std::panicking::begin_panic");
}
- if let Some(panic_id_core) = utils::try_resolve_did(self.env.tcx(), &["core", "panicking", "panic"]) {
+ if let Some(panic_id_core) = search::try_resolve_did(self.env.tcx(), &["core", "panicking", "panic"])
+ {
if panic_id_core == *did {
return true;
}
@@ -2183,7 +2184,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
#[allow(clippy::unused_self)]
const fn register_drop_shim_for(&self, _ty: Ty<'tcx>) {
// TODO!
- //let drop_in_place_did: DefId = utils::try_resolve_did(self.env.tcx(), &["std", "ptr",
+ //let drop_in_place_did: DefId = search::try_resolve_did(self.env.tcx(), &["std", "ptr",
// "drop_in_place"]).unwrap();
//let x: ty::InstanceDef = ty::InstanceDef::DropGlue(drop_in_place_did, Some(ty));
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 942c4c6..00cefaa 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -9,6 +9,7 @@
#![feature(let_chains)]
#![feature(rustc_private)]
mod arg_folder;
+mod attrs;
mod base;
mod checked_op_analysis;
mod data;
@@ -17,6 +18,7 @@ mod force_matches_macro;
mod function_body;
mod inclusion_tracker;
mod regions;
+mod search;
mod shims;
mod spec_parsers;
mod traits;
@@ -124,7 +126,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let is_method = self.env.tcx().impl_of_method(did).is_some();
let interned_path = self.get_path_for_shim(did);
- let name = utils::strip_coq_ident(&self.env.get_item_name(did));
+ let name = base::strip_coq_ident(&self.env.get_item_name(did));
info!("Found function path {:?} for did {:?} with name {:?}", interned_path, did, name);
Some(shim_registry::FunctionShim {
@@ -193,7 +195,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
};
let method_ident = ident.as_str().to_owned();
- let name = utils::strip_coq_ident(&self.env.get_item_name(did));
+ let name = base::strip_coq_ident(&self.env.get_item_name(did));
trace!("leave make_shim_trait_method_entry (success)");
Some(shim_registry::TraitMethodImplShim {
@@ -296,7 +298,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
if did.is_local() && ty::Visibility::Public == self.env.tcx().visibility(did) {
// only export public items
let interned_path = self.get_path_for_shim(did);
- let name = utils::strip_coq_ident(&self.env.get_item_name(did));
+ let name = base::strip_coq_ident(&self.env.get_item_name(did));
info!("Found adt path {:?} for did {:?} with name {:?}", interned_path, did, name);
@@ -913,9 +915,9 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
fn register_shims<'tcx>(vcx: &mut VerificationCtxt<'tcx, '_>) -> Result<(), base::TranslationError<'tcx>> {
for shim in vcx.shim_registry.get_function_shims() {
let did = if shim.is_method {
- utils::try_resolve_method_did(vcx.env.tcx(), &shim.path)
+ search::try_resolve_method_did(vcx.env.tcx(), &shim.path)
} else {
- utils::try_resolve_did(vcx.env.tcx(), &shim.path)
+ search::try_resolve_did(vcx.env.tcx(), &shim.path)
};
match did {
@@ -936,7 +938,7 @@ fn register_shims<'tcx>(vcx: &mut VerificationCtxt<'tcx, '_>) -> Result<(), base
}
for shim in vcx.shim_registry.get_adt_shims() {
- let Some(did) = utils::try_resolve_did(vcx.env.tcx(), &shim.path) else {
+ let Some(did) = search::try_resolve_did(vcx.env.tcx(), &shim.path) else {
println!("Warning: cannot find defid for shim {:?}, skipping", shim.path);
continue;
};
@@ -956,7 +958,7 @@ fn register_shims<'tcx>(vcx: &mut VerificationCtxt<'tcx, '_>) -> Result<(), base
}
for shim in vcx.shim_registry.get_trait_shims() {
- if let Some(did) = utils::try_resolve_did(vcx.env.tcx(), &shim.path) {
+ if let Some(did) = search::try_resolve_did(vcx.env.tcx(), &shim.path) {
let assoc_tys = vcx.trait_registry.get_associated_type_names(did);
let spec = radium::LiteralTraitSpec {
assoc_tys,
@@ -994,7 +996,7 @@ fn register_shims<'tcx>(vcx: &mut VerificationCtxt<'tcx, '_>) -> Result<(), base
continue;
};
- let trait_impl_did = utils::try_resolve_trait_impl_did(vcx.env.tcx(), trait_did, &args, for_type);
+ let trait_impl_did = search::try_resolve_trait_impl_did(vcx.env.tcx(), trait_did, &args, for_type);
let Some(did) = trait_impl_did else {
println!(
@@ -1056,19 +1058,19 @@ fn get_most_restrictive_function_mode(
let attrs = vcx.env.get_attributes_of_function(did, &propagate_method_attr_from_impl);
// check if this is a purely spec function; if so, skip.
- if utils::has_tool_attr_filtered(attrs.as_slice(), "shim") {
+ if attrs::has_tool_attr_filtered(attrs.as_slice(), "shim") {
return function_body::ProcedureMode::Shim;
}
- if utils::has_tool_attr_filtered(attrs.as_slice(), "trust_me") {
+ if attrs::has_tool_attr_filtered(attrs.as_slice(), "trust_me") {
return function_body::ProcedureMode::TrustMe;
}
- if utils::has_tool_attr_filtered(attrs.as_slice(), "only_spec") {
+ if attrs::has_tool_attr_filtered(attrs.as_slice(), "only_spec") {
return function_body::ProcedureMode::OnlySpec;
}
- if utils::has_tool_attr_filtered(attrs.as_slice(), "ignore") {
+ if attrs::has_tool_attr_filtered(attrs.as_slice(), "ignore") {
info!("Function {:?} will be ignored", did);
return function_body::ProcedureMode::Ignore;
}
@@ -1086,7 +1088,7 @@ fn register_functions<'tcx>(
if mode == function_body::ProcedureMode::Shim {
// TODO better error message
let attrs = vcx.env.get_attributes(f.to_def_id());
- let v = utils::filter_tool_attrs(attrs);
+ let v = attrs::filter_for_tool(attrs);
let annot = spec_parsers::get_shim_attrs(v.as_slice()).unwrap();
info!(
@@ -1114,7 +1116,7 @@ fn register_functions<'tcx>(
mode = function_body::ProcedureMode::Prove;
}
- let fname = utils::strip_coq_ident(&vcx.env.get_item_name(f.to_def_id()));
+ let fname = base::strip_coq_ident(&vcx.env.get_item_name(f.to_def_id()));
let spec_name = format!("type_of_{}", fname);
let meta = function_body::ProcedureMeta::new(spec_name, fname, mode);
@@ -1273,7 +1275,7 @@ pub fn register_consts<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) -> Re
for s in &statics {
let ty: ty::EarlyBinder<ty::Ty<'tcx>> = vcx.env.tcx().type_of(s.to_def_id());
- let const_attrs = utils::filter_tool_attrs(vcx.env.get_attributes(s.to_def_id()));
+ let const_attrs = attrs::filter_for_tool(vcx.env.get_attributes(s.to_def_id()));
if const_attrs.is_empty() {
continue;
}
@@ -1282,7 +1284,7 @@ pub fn register_consts<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) -> Re
let scope = scope::Params::default();
match vcx.type_translator.translate_type_in_scope(&scope, ty).map_err(|x| format!("{:?}", x)) {
Ok(translated_ty) => {
- let _full_name = utils::strip_coq_ident(&vcx.env.get_item_name(s.to_def_id()));
+ let _full_name = base::strip_coq_ident(&vcx.env.get_item_name(s.to_def_id()));
let mut const_parser = VerboseConstAttrParser::new();
let const_spec = const_parser.parse_const_attrs(*s, &const_attrs)?;
@@ -1377,7 +1379,7 @@ fn register_trait_impls(vcx: &VerificationCtxt<'_, '_>) -> Result<(), String> {
}
// make names for the spec and inclusion proof
- let base_name = utils::strip_coq_ident(&vcx.env.get_item_name(did));
+ let base_name = base::strip_coq_ident(&vcx.env.get_item_name(did));
let spec_name = format!("{base_name}_spec");
let spec_params_name = format!("{base_name}_spec_params");
let spec_attrs_name = format!("{base_name}_spec_attrs");
@@ -1459,7 +1461,7 @@ pub fn get_module_attributes(env: &Environment<'_>) -> Result<HashMap<LocalDefId
info!("collected modules: {:?}", modules);
for m in &modules {
- let module_attrs = utils::filter_tool_attrs(env.get_attributes(m.to_def_id()));
+ let module_attrs = attrs::filter_for_tool(env.get_attributes(m.to_def_id()));
let mut module_parser = VerboseModuleAttrParser::new();
let module_spec = module_parser.parse_module_attrs(*m, &module_attrs)?;
attrs.insert(*m, module_spec);
@@ -1478,7 +1480,7 @@ where
// get crate attributes
let crate_attrs = tcx.hir().krate_attrs();
- let crate_attrs = utils::filter_tool_attrs(crate_attrs);
+ let crate_attrs = attrs::filter_for_tool(crate_attrs);
info!("Found crate attributes: {:?}", crate_attrs);
// parse crate attributes
let mut crate_parser = VerboseCrateAttrParser::new();
diff --git a/rr_frontend/translation/src/search.rs b/rr_frontend/translation/src/search.rs
new file mode 100644
index 0000000..82d7381
--- /dev/null
+++ b/rr_frontend/translation/src/search.rs
@@ -0,0 +1,323 @@
+// These functions have been adapted from Miri (https://github.com/rust-lang/miri/blob/31fb32e49f42df19b45baccb6aa80c3d726ed6d5/src/helpers.rs#L48) under the MIT license.
+
+//! Utility functions for finding Rust source objects.
+
+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::{force_matches, types, Environment};
+
+/// 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>
+where
+ T: AsRef<str>,
+{
+ tcx.crates(())
+ .iter()
+ .find(|&&krate| tcx.crate_name(krate).as_str() == path[0].as_ref())
+ .and_then(|krate| {
+ let krate = DefId {
+ krate: *krate,
+ index: CRATE_DEF_INDEX,
+ };
+
+ 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: &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());
+ }
+
+ items = tcx.module_children(item.res.def_id());
+ break;
+ }
+ }
+ }
+ None
+ })
+}
+
+pub fn try_resolve_did<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
+where
+ T: AsRef<str>,
+{
+ if let Some(did) = try_resolve_did_direct(tcx, path) {
+ return Some(did);
+ }
+
+ // if the first component is "std", try if we can replace it with "alloc" or "core"
+ if path[0].as_ref() == "std" {
+ let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_owned()).collect();
+ components[0] = "core".to_owned();
+ if let Some(did) = try_resolve_did_direct(tcx, &components) {
+ return Some(did);
+ }
+ // try "alloc"
+ components[0] = "alloc".to_owned();
+ try_resolve_did_direct(tcx, &components)
+ } else {
+ None
+ }
+}
+
+/// Determine whether the two argument lists match for the type positions (ignoring consts and regions).
+/// The first argument is the authority determining which argument positions are types.
+/// The second argument may contain `None` for non-type positions.
+fn args_match_types<'tcx>(
+ reference: &[ty::GenericArg<'tcx>],
+ compare: &[Option<ty::GenericArg<'tcx>>],
+) -> bool {
+ if reference.len() != compare.len() {
+ return false;
+ }
+
+ for (arg1, arg2) in reference.iter().zip(compare.iter()) {
+ if let Some(ty1) = arg1.as_type() {
+ if let Some(arg2) = arg2 {
+ if let Some(ty2) = arg2.as_type() {
+ if ty1 != ty2 {
+ return false;
+ }
+ } else {
+ return false;
+ }
+ } else {
+ return false;
+ }
+ }
+ }
+ true
+}
+
+/// Try to resolve the `DefId` of an implementation of a trait for a particular type.
+/// Note that this does not, in general, find a unique solution, in case there are complex things
+/// with different where clauses going on.
+pub fn try_resolve_trait_impl_did<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ trait_did: DefId,
+ trait_args: &[Option<ty::GenericArg<'tcx>>],
+ for_type: ty::Ty<'tcx>,
+) -> Option<DefId> {
+ // get all impls of this trait
+ let impls: &ty::trait_def::TraitImpls = tcx.trait_impls_of(trait_did);
+
+ 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);
+
+ let mut solution = None;
+ for did in defs {
+ let impl_self_ty: ty::Ty<'tcx> = tcx.type_of(did).instantiate_identity();
+ let impl_self_ty = types::normalize_in_function(*did, tcx, impl_self_ty).unwrap();
+
+ // check if this is an implementation for the right type
+ // TODO: is this the right way to compare the types?
+ if impl_self_ty == for_type {
+ let impl_ref: Option<ty::EarlyBinder<ty::TraitRef<'_>>> = tcx.impl_trait_ref(did);
+
+ if let Some(impl_ref) = impl_ref {
+ let impl_ref = types::normalize_in_function(*did, tcx, impl_ref.skip_binder()).unwrap();
+
+ let this_impl_args = impl_ref.args;
+ // filter by the generic instantiation for the trait
+ info!("found impl with args {:?}", this_impl_args);
+ // args has self at position 0 and generics of the trait at position 1..
+
+ // check if the generic argument types match up
+ if !args_match_types(&this_impl_args.as_slice()[1..], trait_args) {
+ continue;
+ }
+
+ info!("found impl {:?}", impl_ref);
+ if solution.is_some() {
+ println!(
+ "Warning: Ambiguous resolution for impl of trait {:?} on type {:?}; solution {:?} but found also {:?}",
+ trait_did,
+ for_type,
+ solution.unwrap(),
+ impl_ref.def_id,
+ );
+ } else {
+ solution = Some(*did);
+ }
+ }
+ }
+ }
+
+ solution
+}
+
+/// Try to resolve the `DefId` of a method in an implementation of a trait for a particular type.
+/// Note that this does not, in general, find a unique solution, in case there are complex things
+/// with different where clauses going on.
+pub fn try_resolve_trait_method_did<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ trait_did: DefId,
+ trait_args: &[Option<ty::GenericArg<'tcx>>],
+ method_name: &str,
+ for_type: ty::Ty<'tcx>,
+) -> Option<DefId> {
+ // get all impls of this trait
+ let impls: &ty::trait_def::TraitImpls = tcx.trait_impls_of(trait_did);
+
+ 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);
+
+ let mut solution = None;
+ for did in defs {
+ let impl_self_ty: ty::Ty<'tcx> = tcx.type_of(did).instantiate_identity();
+ let impl_self_ty = types::normalize_in_function(*did, tcx, impl_self_ty).unwrap();
+
+ // check if this is an implementation for the right type
+ // TODO: is this the right way to compare the types?
+ if impl_self_ty == for_type {
+ let impl_ref: Option<ty::EarlyBinder<ty::TraitRef<'_>>> = tcx.impl_trait_ref(did);
+
+ if let Some(impl_ref) = impl_ref {
+ let impl_ref = types::normalize_in_function(*did, tcx, impl_ref.skip_binder()).unwrap();
+
+ let this_impl_args = impl_ref.args;
+ // filter by the generic instantiation for the trait
+ info!("found impl with args {:?}", this_impl_args);
+ // args has self at position 0 and generics of the trait at position 1..
+
+ // check if the generic argument types match up
+ if !args_match_types(&this_impl_args.as_slice()[1..], trait_args) {
+ continue;
+ }
+
+ let impl_assoc_items: &ty::AssocItems = tcx.associated_items(did);
+ // find the right item
+ if let Some(item) = impl_assoc_items.find_by_name_and_kind(
+ tcx,
+ span::symbol::Ident::from_str(method_name),
+ ty::AssocKind::Fn,
+ trait_did,
+ ) {
+ info!("found impl {:?} with item {:?}", impl_ref, item);
+ if solution.is_some() {
+ println!(
+ "Warning: Ambiguous resolution for method {method_name} of trait {:?} on type {:?}; solution {:?} but found also {:?}",
+ trait_did,
+ for_type,
+ solution.unwrap(),
+ item.def_id
+ );
+ } else {
+ solution = Some(item.def_id);
+ }
+ }
+ }
+ }
+ }
+
+ solution
+}
+
+/// Try to get a defid of a method at the given path.
+/// This does not handle trait methods.
+/// This also does not handle overlapping method definitions/specialization well.
+pub fn try_resolve_method_did_direct<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
+where
+ T: AsRef<str>,
+{
+ tcx.crates(())
+ .iter()
+ .find(|&&krate| tcx.crate_name(krate).as_str() == path[0].as_ref())
+ .and_then(|krate| {
+ let krate = DefId {
+ krate: *krate,
+ index: CRATE_DEF_INDEX,
+ };
+
+ 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: &middle::metadata::ModChild = item;
+
+ if item.ident.name.as_str() != segment.as_ref() {
+ continue;
+ }
+
+ info!("taking path: {:?}", segment.as_ref());
+ if path_it.peek().is_none() {
+ return Some(item.res.def_id());
+ }
+
+ // just the method remaining
+ if path_it.len() != 1 {
+ items = tcx.module_children(item.res.def_id());
+ break;
+ }
+
+ let did: DefId = item.res.def_id();
+ let impls: &[DefId] = tcx.inherent_impls(did);
+ info!("trying to find method among impls {:?}", impls);
+
+ let find = path_it.next().unwrap();
+ for impl_did in impls {
+ //let ty = tcx.type_of(*impl_did);
+ //info!("type of impl: {:?}", ty);
+ let items: &ty::AssocItems = tcx.associated_items(impl_did);
+ //info!("items here: {:?}", items);
+ // TODO more robust error handling if there are multiple matches.
+ for item in items.in_definition_order() {
+ //info!("comparing: {:?} with {:?}", item.name.as_str(), find);
+ if item.name.as_str() == find.as_ref() {
+ return Some(item.def_id);
+ }
+ }
+ //info!("impl items: {:?}", items);
+ }
+
+ //info!("inherent impls for {:?}: {:?}", did, impls);
+ return None;
+ }
+ }
+
+ None
+ })
+}
+
+pub fn try_resolve_method_did<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
+where
+ T: AsRef<str>,
+{
+ if let Some(did) = try_resolve_method_did_direct(tcx, path) {
+ return Some(did);
+ }
+
+ // if the first component is "std", try if we can replace it with "alloc" or "core"
+ if path[0].as_ref() == "std" {
+ let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_owned()).collect();
+ components[0] = "core".to_owned();
+ if let Some(did) = try_resolve_method_did_direct(tcx, &components) {
+ return Some(did);
+ }
+ // try "alloc"
+ components[0] = "alloc".to_owned();
+ try_resolve_method_did_direct(tcx, &components)
+ } else {
+ None
+ }
+}
diff --git a/rr_frontend/translation/src/shims/flat.rs b/rr_frontend/translation/src/shims/flat.rs
index 3700acc..2d792f0 100644
--- a/rr_frontend/translation/src/shims/flat.rs
+++ b/rr_frontend/translation/src/shims/flat.rs
@@ -18,7 +18,7 @@ use rr_rustc_interface::{hir, middle, span};
use serde::{Deserialize, Serialize};
use crate::spec_parsers::get_export_as_attr;
-use crate::{types, utils, Environment};
+use crate::{attrs, search, types, Environment};
/// An item path that receives generic arguments.
#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
@@ -33,7 +33,7 @@ pub struct PathWithArgs {
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 did = search::try_resolve_did(tcx, self.path.as_slice())?;
let mut ty_args = Vec::new();
@@ -208,8 +208,8 @@ fn extract_def_path(path: &hir::definitions::DefPath) -> Vec<String> {
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);
+ if attrs::has_tool_attr(attrs, "export_as") {
+ let filtered_attrs = attrs::filter_for_tool(attrs);
return get_export_as_attr(filtered_attrs.as_slice()).unwrap();
}
@@ -218,8 +218,8 @@ pub fn get_export_path_for_did(env: &Environment, did: DefId) -> Vec<String> {
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);
+ if attrs::has_tool_attr(attrs, "export_as") {
+ let filtered_attrs = attrs::filter_for_tool(attrs);
let mut path_prefix = get_export_as_attr(filtered_attrs.as_slice()).unwrap();
// push the last component of this path
diff --git a/rr_frontend/translation/src/traits/registry.rs b/rr_frontend/translation/src/traits/registry.rs
index 882d67e..43aaee3 100644
--- a/rr_frontend/translation/src/traits/registry.rs
+++ b/rr_frontend/translation/src/traits/registry.rs
@@ -24,7 +24,7 @@ use crate::spec_parsers::propagate_method_attr_from_impl;
use crate::spec_parsers::trait_attr_parser::{TraitAttrParser, VerboseTraitAttrParser};
use crate::spec_parsers::trait_impl_attr_parser::{TraitImplAttrParser, VerboseTraitImplAttrParser};
use crate::types::scope;
-use crate::{traits, types, utils};
+use crate::{attrs, base, traits, types};
pub struct TR<'tcx, 'def> {
/// environment
@@ -185,10 +185,10 @@ impl<'tcx, 'def> TR<'tcx, 'def> {
let mut param_scope = scope::Params::from(trait_generics.params.as_slice());
param_scope.add_param_env(did.to_def_id(), self.env, self.type_translator, self)?;
- let trait_name = utils::strip_coq_ident(&self.env.get_absolute_item_name(did.to_def_id()));
+ let trait_name = base::strip_coq_ident(&self.env.get_absolute_item_name(did.to_def_id()));
// parse trait spec
- let trait_attrs = utils::filter_tool_attrs(self.env.get_attributes(did.into()));
+ let trait_attrs = attrs::filter_for_tool(self.env.get_attributes(did.into()));
// As different attributes of the spec may depend on each other, we need to pass a closure
// determining under which Coq name we are going to introduce them
// Note: This needs to match up with `radium::LiteralTraitSpec.make_spec_attr_name`!
@@ -219,7 +219,7 @@ impl<'tcx, 'def> TR<'tcx, 'def> {
// get function name
let method_name =
self.env.get_assoc_item_name(c.def_id).ok_or(Error::NotATraitMethod(c.def_id))?;
- let method_name = utils::strip_coq_ident(&method_name);
+ let method_name = base::strip_coq_ident(&method_name);
let name = format!("{trait_name}_{method_name}");
let spec_name = format!("{name}_base_spec");
@@ -241,7 +241,7 @@ impl<'tcx, 'def> TR<'tcx, 'def> {
// get name
let type_name =
self.env.get_assoc_item_name(c.def_id).ok_or(Error::NotATraitMethod(c.def_id))?;
- let type_name = utils::strip_coq_ident(&type_name);
+ let type_name = base::strip_coq_ident(&type_name);
let lit = radium::LiteralTyParam::new(&type_name, &type_name);
assoc_types.push(lit);
}
@@ -563,7 +563,7 @@ impl<'tcx, 'def> TR<'tcx, 'def> {
param_scope.add_param_env(trait_impl_did, self.env, self.type_translator, self)?;
// parse specification
- let trait_impl_attrs = utils::filter_tool_attrs(self.env.get_attributes(trait_impl_did));
+ let trait_impl_attrs = attrs::filter_for_tool(self.env.get_attributes(trait_impl_did));
let mut attr_parser = VerboseTraitImplAttrParser::new(¶m_scope);
let impl_spec = attr_parser
.parse_trait_impl_attrs(&trait_impl_attrs)
@@ -660,7 +660,7 @@ impl<'def> GenericTraitUse<'def> {
let ty_name = env.get_assoc_item_name(*ty_did).unwrap();
let trait_use_ref = self.trait_use.borrow();
let trait_use = trait_use_ref.as_ref().unwrap();
- let lit = trait_use.make_assoc_type_use(&utils::strip_coq_ident(&ty_name));
+ let lit = trait_use.make_assoc_type_use(&base::strip_coq_ident(&ty_name));
assoc_tys.push(lit);
}
assoc_tys
diff --git a/rr_frontend/translation/src/traits/requirements.rs b/rr_frontend/translation/src/traits/requirements.rs
index c9667e3..1d4875d 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::{shims, utils};
+use crate::{search, shims};
/// Get non-trivial trait requirements of a `ParamEnv`,
/// ordered deterministically.
@@ -58,15 +58,15 @@ pub fn get_nontrivial<'tcx>(
/// Check if this is a built-in trait
fn is_builtin_trait(tcx: ty::TyCtxt<'_>, trait_did: DefId) -> Option<bool> {
- let sized_did = utils::try_resolve_did(tcx, &["core", "marker", "Sized"])?;
+ let sized_did = search::try_resolve_did(tcx, &["core", "marker", "Sized"])?;
// TODO: for these, should instead require the primitive encoding of our Coq formalization
- let send_did = utils::try_resolve_did(tcx, &["core", "marker", "Send"])?;
- let sync_did = utils::try_resolve_did(tcx, &["core", "marker", "Sync"])?;
- let copy_did = utils::try_resolve_did(tcx, &["core", "marker", "Copy"])?;
+ let send_did = search::try_resolve_did(tcx, &["core", "marker", "Send"])?;
+ let sync_did = search::try_resolve_did(tcx, &["core", "marker", "Sync"])?;
+ let copy_did = search::try_resolve_did(tcx, &["core", "marker", "Copy"])?;
// used for closures
- let tuple_did = utils::try_resolve_did(tcx, &["core", "marker", "Tuple"])?;
+ let tuple_did = search::try_resolve_did(tcx, &["core", "marker", "Tuple"])?;
Some(
trait_did == sized_did
diff --git a/rr_frontend/translation/src/types/local.rs b/rr_frontend/translation/src/types/local.rs
index 7b65af8..daa9aeb 100644
--- a/rr_frontend/translation/src/types/local.rs
+++ b/rr_frontend/translation/src/types/local.rs
@@ -24,7 +24,7 @@ use crate::traits::resolution;
use crate::types::translator::*;
use crate::types::tyvars::*;
use crate::types::{self, scope};
-use crate::{regions, traits, utils};
+use crate::{base, regions, traits};
/// Information we compute when calling a function from another function.
/// Determines how to specialize the callee's generics in our spec assumption.
@@ -257,7 +257,7 @@ impl<'def, 'tcx> LocalTX<'def, 'tcx> {
// get name of the method
let method_name = env.get_assoc_item_name(trait_method_did).unwrap();
let mangled_method_name =
- types::mangle_name_with_args(&utils::strip_coq_ident(&method_name), method_args.as_slice());
+ types::mangle_name_with_args(&base::strip_coq_ident(&method_name), method_args.as_slice());
let method_loc_name = trait_spec_use.make_loc_name(&mangled_method_name);
diff --git a/rr_frontend/translation/src/types/mod.rs b/rr_frontend/translation/src/types/mod.rs
index 6738373..77ab789 100644
--- a/rr_frontend/translation/src/types/mod.rs
+++ b/rr_frontend/translation/src/types/mod.rs
@@ -19,7 +19,7 @@ use rr_rustc_interface::middle::ty;
pub use scope::{generate_args_inst_key, GenericsKey};
pub use translator::{AdtState, CalleeState, FunctionState, STInner, ST, TX};
-use crate::utils;
+use crate::base;
/// Mangle a name by appending type parameters to it.
pub fn mangle_name_with_tys(method_name: &str, args: &[ty::Ty<'_>]) -> String {
@@ -28,7 +28,7 @@ pub fn mangle_name_with_tys(method_name: &str, args: &[ty::Ty<'_>]) -> String {
for arg in args {
mangled_name.push_str(format!("_{}", arg).as_str());
}
- utils::strip_coq_ident(&mangled_name)
+ base::strip_coq_ident(&mangled_name)
}
/// Mangle a name by appending generic args to it.
@@ -36,7 +36,7 @@ pub fn mangle_name_with_args(name: &str, args: &[ty::GenericArg<'_>]) -> String
let mut mangled_base = name.to_owned();
for arg in args {
if let ty::GenericArgKind::Type(ty) = arg.unpack() {
- write!(mangled_base, "_{}", utils::strip_coq_ident(&format!("{ty}"))).unwrap();
+ write!(mangled_base, "_{}", base::strip_coq_ident(&format!("{ty}"))).unwrap();
}
}
mangled_base
diff --git a/rr_frontend/translation/src/types/scope.rs b/rr_frontend/translation/src/types/scope.rs
index 9734296..5ed043e 100644
--- a/rr_frontend/translation/src/types/scope.rs
+++ b/rr_frontend/translation/src/types/scope.rs
@@ -15,6 +15,7 @@ use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::ty;
use rr_rustc_interface::middle::ty::TypeFoldable;
+use crate::base;
use crate::base::*;
use crate::environment::Environment;
use crate::spec_parsers::parse_utils::ParamLookup;
@@ -22,7 +23,6 @@ use crate::traits::registry::GenericTraitUse;
use crate::traits::{self, registry};
use crate::types::translator::*;
use crate::types::tyvars::*;
-use crate::utils::strip_coq_ident;
/// Key used for resolving early-bound parameters for function calls.
/// Invariant: All regions contained in these types should be erased, as type parameter instantiation is
@@ -178,7 +178,7 @@ impl<'tcx, 'def> Params<'tcx, 'def> {
if let Some(r) = p.as_region() {
if let Some(name) = r.get_name() {
lft_names.insert(name.as_str().to_owned(), scope.len());
- scope.push(Param::Region(strip_coq_ident(name.as_str())));
+ scope.push(Param::Region(base::strip_coq_ident(name.as_str())));
} else {
let name = format!("ulft_{region_count}");
region_count += 1;
@@ -187,7 +187,7 @@ impl<'tcx, 'def> Params<'tcx, 'def> {
} else if let Some(ty) = p.as_type() {
if let ty::TyKind::Param(x) = ty.kind() {
ty_names.insert(x.name.as_str().to_owned(), scope.len());
- let name = strip_coq_ident(x.name.as_str());
+ let name = base::strip_coq_ident(x.name.as_str());
let lit = if let Some((tcx, of_did)) = with_origin {
let origin = Self::determine_origin_of_param(of_did, tcx, *x);
@@ -494,7 +494,7 @@ impl<'a, 'tcx, 'def> From<&'a [ty::GenericParamDef]> for Params<'tcx, 'def> {
let mut lft_names = HashMap::new();
for p in x {
- let name = strip_coq_ident(p.name.as_str());
+ let name = base::strip_coq_ident(p.name.as_str());
match p.kind {
ty::GenericParamDefKind::Const { .. } => {
scope.push(Param::Const);
diff --git a/rr_frontend/translation/src/types/translator.rs b/rr_frontend/translation/src/types/translator.rs
index 753ad77..9cdf7ab 100644
--- a/rr_frontend/translation/src/types/translator.rs
+++ b/rr_frontend/translation/src/types/translator.rs
@@ -29,7 +29,7 @@ use crate::spec_parsers::struct_spec_parser::{self, InvariantSpecParser, StructF
use crate::traits::{self, registry};
use crate::types::scope;
use crate::types::tyvars::*;
-use crate::utils;
+use crate::{attrs, base, search};
/// A scope tracking the type translation state when translating the body of a function.
/// This also includes the state needed for tracking trait constraints, as type translation for
@@ -285,7 +285,7 @@ impl<'a, 'def, 'tcx> STInner<'a, 'def, 'tcx> {
// TODO: ?
if region.has_name() {
let name = region.name.as_str();
- return Ok(format!("ulft_{}", utils::strip_coq_ident(name)));
+ return Ok(format!("ulft_{}", base::strip_coq_ident(name)));
}
return Err(TranslationError::UnknownEarlyRegion(*region));
},
@@ -954,14 +954,14 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
let struct_def_init = self.struct_arena.alloc(OnceCell::new());
let tcx = self.env.tcx();
- let struct_name = utils::strip_coq_ident(&ty.ident(tcx).to_string());
+ let struct_name = base::strip_coq_ident(&ty.ident(tcx).to_string());
self.variant_registry
.borrow_mut()
.insert(ty.def_id, (struct_name, struct_def_init, ty, false, None));
let translate_adt = || {
- let struct_name = utils::strip_coq_ident(&ty.ident(tcx).to_string());
+ let struct_name = base::strip_coq_ident(&ty.ident(tcx).to_string());
let (variant_def, invariant_def) =
self.make_adt_variant(&struct_name, ty, adt, AdtState::new(&mut deps, &scope, ¶m_env))?;
@@ -1021,10 +1021,10 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
let expect_refinement;
let mut invariant_spec;
- if utils::has_tool_attr(outer_attrs, "refined_by") {
- let outer_attrs = utils::filter_tool_attrs(outer_attrs);
+ if attrs::has_tool_attr(outer_attrs, "refined_by") {
+ let outer_attrs = attrs::filter_for_tool(outer_attrs);
let mut spec_parser = struct_spec_parser::VerboseInvariantSpecParser::new(adt_deps.scope);
- let ty_name = utils::strip_coq_ident(format!("{}_inv_t", struct_name).as_str());
+ let ty_name = base::strip_coq_ident(format!("{}_inv_t", struct_name).as_str());
let res = spec_parser
.parse_invariant_spec(&ty_name, &outer_attrs)
.map_err(TranslationError::FatalError)?;
@@ -1043,7 +1043,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
let f_name = f.ident(tcx).to_string();
let attrs = self.env.get_attributes(f.did);
- let attrs = utils::filter_tool_attrs(attrs);
+ let attrs = attrs::filter_for_tool(attrs);
let f_ty = self.env.tcx().type_of(f.did).instantiate_identity();
let mut ty = self.translate_type_in_state(
@@ -1176,7 +1176,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
}
fn does_did_match(&self, did: DefId, path: &[&str]) -> bool {
- let lookup_did = utils::try_resolve_did(self.env.tcx(), path);
+ let lookup_did = search::try_resolve_did(self.env.tcx(), path);
if let Some(lookup_did) = lookup_did {
if lookup_did == did {
return true;
@@ -1286,7 +1286,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
let enum_def_init = self.enum_arena.alloc(OnceCell::new());
// TODO: currently a hack, I don't know how to query the name properly
- let enum_name = utils::strip_coq_ident(format!("{:?}", def).as_str());
+ let enum_name = base::strip_coq_ident(format!("{:?}", def).as_str());
// first thing: figure out the generics we are using here.
// we need to search all of the variant types for that.
@@ -1315,7 +1315,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
// now generate the variant
let struct_def_init = self.struct_arena.alloc(OnceCell::new());
- let struct_name = utils::strip_coq_ident(format!("{}_{}", enum_name, v.ident(tcx)).as_str());
+ let struct_name = base::strip_coq_ident(format!("{}_{}", enum_name, v.ident(tcx)).as_str());
self.variant_registry
.borrow_mut()
.insert(v.def_id, (struct_name.clone(), &*struct_def_init, v, true, None));
@@ -1334,7 +1334,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
// also remember the attributes for additional processing
let outer_attrs = self.env.get_attributes(v.def_id);
- let outer_attrs = utils::filter_tool_attrs(outer_attrs);
+ let outer_attrs = attrs::filter_for_tool(outer_attrs);
variant_attrs.push(outer_attrs);
// finalize the definition
@@ -1368,7 +1368,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
enum_spec = spec;
} else if self.env.has_tool_attribute(def.did(), "refined_by") {
let attributes = self.env.get_attributes(def.did());
- let attributes = utils::filter_tool_attrs(attributes);
+ let attributes = attrs::filter_for_tool(attributes);
let mut parser = VerboseEnumSpecParser::new(&scope);
@@ -1398,7 +1398,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
// now build the enum itself
for v in def.variants() {
let (variant_ref, _) = self.lookup_adt_variant(v.def_id)?;
- let variant_name = utils::strip_coq_ident(&v.ident(tcx).to_string());
+ let variant_name = base::strip_coq_ident(&v.ident(tcx).to_string());
let discriminant = discrs[&variant_name];
enum_builder.add_variant(&variant_name, variant_ref, discriminant);
}
@@ -1608,7 +1608,7 @@ impl<'def, 'tcx: 'def> TX<'def, 'tcx> {
.env
.get_assoc_item_name(alias_ty.def_id)
.ok_or(traits::Error::NotAnAssocType(alias_ty.def_id))?;
- let assoc_type = trait_use.make_assoc_type_use(&utils::strip_coq_ident(&type_name));
+ let assoc_type = trait_use.make_assoc_type_use(&base::strip_coq_ident(&type_name));
info!("Resolved projection to {assoc_type:?}");
diff --git a/rr_frontend/translation/src/utils.rs b/rr_frontend/translation/src/utils.rs
index ac0ecc2..58af65e 100644
--- a/rr_frontend/translation/src/utils.rs
+++ b/rr_frontend/translation/src/utils.rs
@@ -1,10 +1,9 @@
-// Except for the exceptions specified below, this code is © 2019, ETH Zurich
+// © 2019, ETH Zurich
// This Source Code Form is subject to the terms of the Mozilla Public
// 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/.
-//
-// The following functions have been adapted from Miri (https://github.com/rust-lang/miri/blob/31fb32e49f42df19b45baccb6aa80c3d726ed6d5/src/helpers.rs#L48) under the MIT license;
-// - `try_resolve_did`
+
+//! Utility functions for manipulating places.
use std::mem;
@@ -20,328 +19,6 @@ use serde::{Deserialize, Serialize};
use crate::spec_parsers::get_export_as_attr;
use crate::{force_matches, types, Environment};
-/// Strip symbols from an identifier to be compatible with Coq.
-/// In particular things like ' or ::.
-pub fn strip_coq_ident(s: &str) -> String {
- String::from(s)
- .replace('\'', "")
- .replace("::", "_")
- .replace(|c: char| !(c.is_alphanumeric() || c == '_'), "")
-}
-
-/// 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>
-where
- T: AsRef<str>,
-{
- tcx.crates(())
- .iter()
- .find(|&&krate| tcx.crate_name(krate).as_str() == path[0].as_ref())
- .and_then(|krate| {
- let krate = DefId {
- krate: *krate,
- index: CRATE_DEF_INDEX,
- };
-
- 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: &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());
- }
-
- items = tcx.module_children(item.res.def_id());
- break;
- }
- }
- }
- None
- })
-}
-
-pub fn try_resolve_did<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
-where
- T: AsRef<str>,
-{
- if let Some(did) = try_resolve_did_direct(tcx, path) {
- return Some(did);
- }
-
- // if the first component is "std", try if we can replace it with "alloc" or "core"
- if path[0].as_ref() == "std" {
- let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_owned()).collect();
- components[0] = "core".to_owned();
- if let Some(did) = try_resolve_did_direct(tcx, &components) {
- return Some(did);
- }
- // try "alloc"
- components[0] = "alloc".to_owned();
- try_resolve_did_direct(tcx, &components)
- } else {
- None
- }
-}
-
-/// Determine whether the two argument lists match for the type positions (ignoring consts and regions).
-/// The first argument is the authority determining which argument positions are types.
-/// The second argument may contain `None` for non-type positions.
-fn args_match_types<'tcx>(
- reference: &[ty::GenericArg<'tcx>],
- compare: &[Option<ty::GenericArg<'tcx>>],
-) -> bool {
- if reference.len() != compare.len() {
- return false;
- }
-
- for (arg1, arg2) in reference.iter().zip(compare.iter()) {
- if let Some(ty1) = arg1.as_type() {
- if let Some(arg2) = arg2 {
- if let Some(ty2) = arg2.as_type() {
- if ty1 != ty2 {
- return false;
- }
- } else {
- return false;
- }
- } else {
- return false;
- }
- }
- }
- true
-}
-
-// Useful queries:
-//tcx.trait_id_of_impl
-//tcx.associated_items
-//tcx.impl_trait_parent
-//tcx.implementations_of_trait
-//tcx.trait_impls_of
-//tcx.trait_impls_in_crate
-/// Try to resolve the `DefId` of an implementation of a trait for a particular type.
-/// Note that this does not, in general, find a unique solution, in case there are complex things
-/// with different where clauses going on.
-pub fn try_resolve_trait_impl_did<'tcx>(
- tcx: TyCtxt<'tcx>,
- trait_did: DefId,
- trait_args: &[Option<ty::GenericArg<'tcx>>],
- for_type: ty::Ty<'tcx>,
-) -> Option<DefId> {
- // get all impls of this trait
- let impls: &ty::trait_def::TraitImpls = tcx.trait_impls_of(trait_did);
-
- 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);
-
- let mut solution = None;
- for did in defs {
- let impl_self_ty: ty::Ty<'tcx> = tcx.type_of(did).instantiate_identity();
- let impl_self_ty = types::normalize_in_function(*did, tcx, impl_self_ty).unwrap();
-
- // check if this is an implementation for the right type
- // TODO: is this the right way to compare the types?
- if impl_self_ty == for_type {
- let impl_ref: Option<ty::EarlyBinder<ty::TraitRef<'_>>> = tcx.impl_trait_ref(did);
-
- if let Some(impl_ref) = impl_ref {
- let impl_ref = types::normalize_in_function(*did, tcx, impl_ref.skip_binder()).unwrap();
-
- let this_impl_args = impl_ref.args;
- // filter by the generic instantiation for the trait
- info!("found impl with args {:?}", this_impl_args);
- // args has self at position 0 and generics of the trait at position 1..
-
- // check if the generic argument types match up
- if !args_match_types(&this_impl_args.as_slice()[1..], trait_args) {
- continue;
- }
-
- info!("found impl {:?}", impl_ref);
- if solution.is_some() {
- println!(
- "Warning: Ambiguous resolution for impl of trait {:?} on type {:?}; solution {:?} but found also {:?}",
- trait_did,
- for_type,
- solution.unwrap(),
- impl_ref.def_id,
- );
- } else {
- solution = Some(*did);
- }
- }
- }
- }
-
- solution
-}
-
-/// Try to resolve the `DefId` of a method in an implementation of a trait for a particular type.
-/// Note that this does not, in general, find a unique solution, in case there are complex things
-/// with different where clauses going on.
-pub fn try_resolve_trait_method_did<'tcx>(
- tcx: TyCtxt<'tcx>,
- trait_did: DefId,
- trait_args: &[Option<ty::GenericArg<'tcx>>],
- method_name: &str,
- for_type: ty::Ty<'tcx>,
-) -> Option<DefId> {
- // get all impls of this trait
- let impls: &ty::trait_def::TraitImpls = tcx.trait_impls_of(trait_did);
-
- 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);
-
- let mut solution = None;
- for did in defs {
- let impl_self_ty: ty::Ty<'tcx> = tcx.type_of(did).instantiate_identity();
- let impl_self_ty = types::normalize_in_function(*did, tcx, impl_self_ty).unwrap();
-
- // check if this is an implementation for the right type
- // TODO: is this the right way to compare the types?
- if impl_self_ty == for_type {
- let impl_ref: Option<ty::EarlyBinder<ty::TraitRef<'_>>> = tcx.impl_trait_ref(did);
-
- if let Some(impl_ref) = impl_ref {
- let impl_ref = types::normalize_in_function(*did, tcx, impl_ref.skip_binder()).unwrap();
-
- let this_impl_args = impl_ref.args;
- // filter by the generic instantiation for the trait
- info!("found impl with args {:?}", this_impl_args);
- // args has self at position 0 and generics of the trait at position 1..
-
- // check if the generic argument types match up
- if !args_match_types(&this_impl_args.as_slice()[1..], trait_args) {
- continue;
- }
-
- let impl_assoc_items: &ty::AssocItems = tcx.associated_items(did);
- // find the right item
- if let Some(item) = impl_assoc_items.find_by_name_and_kind(
- tcx,
- span::symbol::Ident::from_str(method_name),
- ty::AssocKind::Fn,
- trait_did,
- ) {
- info!("found impl {:?} with item {:?}", impl_ref, item);
- if solution.is_some() {
- println!(
- "Warning: Ambiguous resolution for method {method_name} of trait {:?} on type {:?}; solution {:?} but found also {:?}",
- trait_did,
- for_type,
- solution.unwrap(),
- item.def_id
- );
- } else {
- solution = Some(item.def_id);
- }
- }
- }
- }
- }
-
- solution
-}
-
-/// Try to get a defid of a method at the given path.
-/// This does not handle trait methods.
-/// This also does not handle overlapping method definitions/specialization well.
-pub fn try_resolve_method_did_direct<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
-where
- T: AsRef<str>,
-{
- tcx.crates(())
- .iter()
- .find(|&&krate| tcx.crate_name(krate).as_str() == path[0].as_ref())
- .and_then(|krate| {
- let krate = DefId {
- krate: *krate,
- index: CRATE_DEF_INDEX,
- };
-
- 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: &middle::metadata::ModChild = item;
-
- if item.ident.name.as_str() != segment.as_ref() {
- continue;
- }
-
- info!("taking path: {:?}", segment.as_ref());
- if path_it.peek().is_none() {
- return Some(item.res.def_id());
- }
-
- // just the method remaining
- if path_it.len() != 1 {
- items = tcx.module_children(item.res.def_id());
- break;
- }
-
- let did: DefId = item.res.def_id();
- let impls: &[DefId] = tcx.inherent_impls(did);
- info!("trying to find method among impls {:?}", impls);
-
- let find = path_it.next().unwrap();
- for impl_did in impls {
- //let ty = tcx.type_of(*impl_did);
- //info!("type of impl: {:?}", ty);
- let items: &ty::AssocItems = tcx.associated_items(impl_did);
- //info!("items here: {:?}", items);
- // TODO more robust error handling if there are multiple matches.
- for item in items.in_definition_order() {
- //info!("comparing: {:?} with {:?}", item.name.as_str(), find);
- if item.name.as_str() == find.as_ref() {
- return Some(item.def_id);
- }
- }
- //info!("impl items: {:?}", items);
- }
-
- //info!("inherent impls for {:?}: {:?}", did, impls);
- return None;
- }
- }
-
- None
- })
-}
-
-pub fn try_resolve_method_did<T>(tcx: TyCtxt<'_>, path: &[T]) -> Option<DefId>
-where
- T: AsRef<str>,
-{
- if let Some(did) = try_resolve_method_did_direct(tcx, path) {
- return Some(did);
- }
-
- // if the first component is "std", try if we can replace it with "alloc" or "core"
- if path[0].as_ref() == "std" {
- let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_owned()).collect();
- components[0] = "core".to_owned();
- if let Some(did) = try_resolve_method_did_direct(tcx, &components) {
- return Some(did);
- }
- // try "alloc"
- components[0] = "alloc".to_owned();
- try_resolve_method_did_direct(tcx, &components)
- } else {
- None
- }
-}
-
/// Check if the place `potential_prefix` is a prefix of `place`. For example:
///
/// + `is_prefix(x.f, x.f) == true`
@@ -569,64 +246,3 @@ impl<'tcx> VecPlace<'tcx> {
self.components.len()
}
}
-
-/// Check if `<tool>::<name>` is among the attributes, where `tool` is determined by the
-/// `spec_hotword` config.
-/// Any arguments of the attribute are ignored.
-pub fn has_tool_attr(attrs: &[ast::Attribute], name: &str) -> bool {
- get_tool_attr(attrs, name).is_some()
-}
-
-/// Get the arguments for a tool attribute, if it exists.
-pub fn get_tool_attr<'a>(attrs: &'a [ast::Attribute], name: &str) -> Option<&'a ast::AttrArgs> {
- attrs.iter().find_map(|attr| match &attr.kind {
- ast::AttrKind::Normal(na) => {
- let segments = &na.item.path.segments;
- let args = &na.item.args;
- (segments.len() == 2
- && segments[0].ident.as_str() == rrconfig::spec_hotword().as_str()
- && segments[1].ident.as_str() == name)
- .then_some(args)
- },
- _ => None,
- })
-}
-
-/// Check if `<tool>::name` is among the filtered attributes.
-pub fn has_tool_attr_filtered(attrs: &[&ast::AttrItem], name: &str) -> bool {
- attrs.iter().any(|item| {
- let segments = &item.path.segments;
- segments.len() == 2
- && segments[0].ident.as_str() == rrconfig::spec_hotword().as_str()
- && segments[1].ident.as_str() == name
- })
-}
-
-/// Check if any attribute starting with `<tool>` is among the attributes.
-pub fn has_any_tool_attr(attrs: &[ast::Attribute]) -> bool {
- attrs.iter().any(|attr| match &attr.kind {
- ast::AttrKind::Normal(na) => {
- let segments = &na.item.path.segments;
- segments[0].ident.as_str() == rrconfig::spec_hotword().as_str()
- },
- _ => false,
- })
-}
-
-/// Get all tool attributes, i.e. attributes of the shape `<tool>::attr`, where `tool` is
-/// determined by the `spec_hotword` config.
-pub fn filter_tool_attrs(attrs: &[ast::Attribute]) -> Vec<&ast::AttrItem> {
- attrs
- .iter()
- .filter_map(|attr| match &attr.kind {
- ast::AttrKind::Normal(na) => {
- let item = &na.item;
-
- let seg = item.path.segments.get(0)?;
-
- (seg.ident.name.as_str() == rrconfig::spec_hotword()).then_some(item)
- },
- _ => None,
- })
- .collect()
-}
--
GitLab