diff --git a/Cargo.toml b/Cargo.toml index 335a13c54..52409c1ac 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -53,7 +53,7 @@ schemars = "0.8" which = "4.4" serde = { version = "1.0", features = ["derive"] } serde_json = "1.0" -clap = { version = "4.0", features = ["derive"] } +clap = { version = "4.0", features = ["derive", "env"] } syn = { version = "1.0.107", features = [ "derive", "printing", diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index c7b5aee1a..9feaeb9c2 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -2,6 +2,7 @@ use hax_cli_options::{Backend, PathOrDash, ENV_VAR_OPTIONS_FRONTEND}; use hax_frontend_exporter; use hax_frontend_exporter::state::{ExportedSpans, LocalContextS}; use hax_frontend_exporter::SInto; +use itertools::Itertools; use rustc_driver::{Callbacks, Compilation}; use rustc_interface::interface; use rustc_interface::{interface::Compiler, Queries}; @@ -106,7 +107,6 @@ fn precompute_local_thir_bodies<'tcx>( } } - use itertools::Itertools; hir.body_owners() .filter(|ldid| { match tcx.def_kind(ldid.to_def_id()) { @@ -317,6 +317,40 @@ impl Callbacks for ExtractionCallbacks { queries.global_ctxt().unwrap().enter(|tcx| { use hax_cli_options::ExporterCommand; match self.command.clone() { + ExporterCommand::ListNames { + include_current_crate_names, + as_include_ns_flag, + } => { + let (_, mut def_ids, _, _) = convert_thir::( + &self.clone().into(), + self.macro_calls.clone(), + tcx, + ); + use std::io::{BufWriter, Write}; + if !include_current_crate_names { + let current_crate = tcx.crate_name(rustc_span::def_id::LOCAL_CRATE); + let current_crate = current_crate.as_str(); + def_ids.retain(|def_id| def_id.krate != current_crate); + } + let mut dest = BufWriter::new(std::io::stdout()); + let mut first = true; + for def_id in def_ids + .iter() + .map(|def_id| def_id.serialize_compact()) + .sorted() + { + let _ = if as_include_ns_flag { + if !first { + let _ = write!(dest, " "); + } + write!(dest, "+{}", def_id) + } else { + writeln!(dest, "{}", def_id) + }; + first = false; + } + } + ExporterCommand::JSON { output_file, mut kind, diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index a71c6045e..3b7b2fdf3 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -280,6 +280,7 @@ pub struct TranslationOptions { value_delimiter = ' ', )] #[arg(short, allow_hyphen_values(true))] + #[arg(env = "HAX_INCLUDE_NAMESPACES")] include_namespaces: Vec, } @@ -352,6 +353,19 @@ pub enum ExporterCommand { #[arg(short = 'E', long = "include-extra", default_value = "false")] include_extra: bool, }, + + /// List the names of all items the selected crate(s) uses + ListNames { + /// Print as a string that can be passed to the `-i` flag of + /// `cargo hax into`. + #[arg(short = 'i', long = "as-include-ns-flag", default_value = "false")] + as_include_ns_flag: bool, + + /// Include the names of the crate being extracted (by default + /// only external names are included) + #[arg(long = "include-self", default_value = "false")] + include_current_crate_names: bool, + }, } #[derive( diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 2ec0f58d8..240d7df31 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1394,10 +1394,14 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items let namespace = clause.namespace in (* match anything under that **module** namespace *) let namespace = - { - namespace with - chunks = namespace.chunks @ [ Glob One; Glob Many ]; - } + match namespace with + | Pattern namespace -> + Types.Pattern + { + namespace with + chunks = namespace.chunks @ [ Glob One; Glob Many ]; + } + | _ -> namespace in Concrete_ident.matches_namespace namespace item.ident) |> Option.map ~f:(fun (clause : Types.inclusion_clause) -> clause.kind) diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index 9f5407891..dbbdff941 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -563,7 +563,7 @@ module DefaultNamePolicy = struct let struct_constructor_name_transform = Fn.id end -let matches_namespace (ns : Types.namespace) (did : t) : bool = +let matches_namespace_pattern (ns : Types.namespace_pattern) (did : t) : bool = let did = did.def_id in let path : string option list = Some did.krate @@ -585,6 +585,14 @@ let matches_namespace (ns : Types.namespace) (did : t) : bool = in aux ns.chunks path +let matches_namespace (ns : Types.namespace) (did : t) : bool = + match ns with + | Pattern pattern -> matches_namespace_pattern pattern did + | Exact did' -> + let did' = Imported.of_def_id did' in + let did = did.def_id in + [%eq: Imported.def_id] did did' + module Create = struct let parent (id : t) : t = { id with def_id = Imported.parent id.def_id } diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 97e8488a6..f2087f5c8 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -256,10 +256,15 @@ module Make (F : Features.T) = struct | Shallow -> "+~" | None' -> "+!")) ^ "[" - ^ (List.map - ~f:(function Glob One -> "*" | Glob Many -> "**" | Exact s -> s) - namespace.chunks - |> String.concat ~sep:"::") + ^ (match namespace with + | Pattern pattern -> + List.map + ~f:(function Glob One -> "*" | Glob Many -> "**" | Exact s -> s) + pattern.chunks + |> String.concat ~sep:"::" + | Exact did -> + Concrete_ident.DefaultViewAPI.show + (Concrete_ident.of_def_id Value did)) ^ "]" in let items_drop_body = Hash_set.create (module Concrete_ident) in diff --git a/frontend/exporter/src/options.rs b/frontend/exporter/src/options.rs index 786496f26..7af41dbc4 100644 --- a/frontend/exporter/src/options.rs +++ b/frontend/exporter/src/options.rs @@ -24,11 +24,28 @@ impl std::convert::From<&str> for NamespaceChunk { } #[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)] -pub struct Namespace { - pub chunks: Vec, +pub struct NamespacePattern { + chunks: Vec, +} +#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)] +pub enum Namespace { + /// A pattern that matches `DefId`s + Pattern(NamespacePattern), + /// An exact `DefId` + Exact(crate::DefId), } impl std::convert::From for Namespace { + fn from(s: String) -> Self { + if let Some(def_id) = crate::DefId::deserialize_compact(&s) { + Self::Exact(def_id) + } else { + Self::Pattern(s.into()) + } + } +} + +impl std::convert::From for NamespacePattern { fn from(s: String) -> Self { Self { chunks: s @@ -41,7 +58,7 @@ impl std::convert::From for Namespace { } } -impl Namespace { +impl NamespacePattern { pub fn matches(&self, path: &Vec) -> bool { fn aux(pattern: &[NamespaceChunk], path: &[String]) -> bool { match (pattern, path) { diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs index c9621a65c..cd32027ec 100644 --- a/frontend/exporter/src/rustc_utils.rs +++ b/frontend/exporter/src/rustc_utils.rs @@ -245,11 +245,10 @@ pub(crate) fn raw_macro_invocation_of_span<'t, S: BaseState<'t>>( { let macro_ident: DefId = mac_def_id.sinto(state); let path = Path::from(macro_ident.clone()); - if opts - .inline_macro_calls - .iter() - .any(|pattern| pattern.matches(&path)) - { + if opts.inline_macro_calls.iter().any(|pattern| match pattern { + crate::options::Namespace::Pattern(pattern) => pattern.matches(&path), + crate::options::Namespace::Exact(def_id) => def_id == ¯o_ident, + }) { Some((macro_ident, expn_data_ret)) } else { None diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index b236e2ab2..77f7380ab 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -5,18 +5,6 @@ use crate::rustc_middle::query::Key; #[cfg(feature = "full")] use rustc_middle::ty; -impl std::hash::Hash for DefId { - fn hash(&self, state: &mut H) { - let DefId { - krate, - path, - index: _, // intentionally discarding index - } = self; - krate.hash(state); - path.hash(state); - } -} - #[cfg(feature = "full")] impl<'s, S: BaseState<'s>> SInto for rustc_hir::def_id::DefId { fn sinto(&self, s: &S) -> DefId { diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index 2704cf4c5..01a6fa741 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -17,7 +17,7 @@ pub struct DisambiguatedDefPathItem { } /// Reflects [`rustc_hir::def_id::DefId`] -#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, JsonSchema)] +#[derive(Clone, Debug, Serialize, Deserialize, Eq, PartialOrd, Ord, JsonSchema)] pub struct DefId { pub krate: String, pub path: Vec, @@ -53,3 +53,138 @@ pub enum DefPathItem { ImplTrait, ImplTraitAssocTy, } + +impl std::hash::Hash for DefId { + fn hash(&self, state: &mut H) { + let DefId { + krate, + path, + index: _, // intentionally discarding index + } = self; + krate.hash(state); + path.hash(state); + } +} + +impl std::cmp::PartialEq for DefId { + fn eq(&self, other: &Self) -> bool { + self.krate.eq(&other.krate) && self.path.eq(&other.path) + } +} + +impl DefId { + pub fn serialize_compact(&self) -> String { + use itertools::Itertools; + [self.krate.clone()] + .into_iter() + .chain(self.path.iter().map(|item| item.serialize_compact())) + .join("::") + } + pub fn deserialize_compact(s: &str) -> Option { + const DUMMY_INDEX: (u32, u32) = (0, 0); + match s.split("::").collect::>().as_slice() { + [krate, path @ ..] => Some(Self { + krate: krate.to_string(), + path: path + .iter() + .map(|item| DisambiguatedDefPathItem::deserialize_compact(item)) + .collect::>>()?, + index: DUMMY_INDEX, + }), + _ => None, + } + } +} +impl DisambiguatedDefPathItem { + fn serialize_compact(&self) -> String { + let data = self.data.serialize_compact(); + if self.disambiguator == 0 { + data + } else { + format!("{data}#{}", self.disambiguator) + } + } + fn deserialize_compact(s: &str) -> Option { + let mut disambiguator = 0; + let mut data_string = s; + if let Some((s, num)) = s.split_once("#") { + if let Ok(num) = num.parse::() { + disambiguator = num; + data_string = s; + } + } + Some(DisambiguatedDefPathItem { + data: DefPathItem::deserialize_compact(data_string)?, + disambiguator, + }) + } +} + +mod tags { + #![allow(non_upper_case_globals)] + pub const CrateRoot: &str = "CrateRoot"; + pub const Impl: &str = "Impl"; + pub const ForeignMod: &str = "ForeignMod"; + pub const Use: &str = "Use"; + pub const GlobalAsm: &str = "GlobalAsm"; + pub const TypeNs: &str = "ty"; + pub const ValueNs: &str = "val"; + pub const MacroNs: &str = "macro"; + pub const LifetimeNs: &str = "lt"; + pub const ClosureExpr: &str = "Closure"; + pub const Ctor: &str = "Ctor"; + pub const AnonConst: &str = "AnonConst"; + pub const ImplTrait: &str = "ImplTrait"; + pub const ImplTraitAssocTy: &str = "ImplTraitAssocTy"; +} +const SEP: &str = "~"; +impl DefPathItem { + fn serialize_compact(&self) -> String { + match self { + Self::CrateRoot => format!("{}{SEP}", tags::CrateRoot), + Self::Impl => format!("{}{SEP}", tags::Impl), + Self::ForeignMod => format!("{}{SEP}", tags::ForeignMod), + Self::Use => format!("{}{SEP}", tags::Use), + Self::GlobalAsm => format!("{}{SEP}", tags::GlobalAsm), + Self::TypeNs(s) => format!("{}{SEP}{s}", tags::TypeNs), + Self::ValueNs(s) => format!("{}{SEP}{s}", tags::ValueNs), + Self::MacroNs(s) => format!("{}{SEP}{s}", tags::MacroNs), + Self::LifetimeNs(s) => format!("{}{SEP}{s}", tags::LifetimeNs), + Self::ClosureExpr => format!("{}{SEP}", tags::ClosureExpr), + Self::Ctor => format!("{}{SEP}", tags::Ctor), + Self::AnonConst => format!("{}{SEP}", tags::AnonConst), + Self::ImplTrait => format!("{}{SEP}", tags::ImplTrait), + Self::ImplTraitAssocTy => format!("{}{SEP}", tags::ImplTraitAssocTy), + } + } + fn deserialize_compact(s: &str) -> Option { + Some(if let Some((tag, s)) = s.split_once(SEP) { + if s.is_empty() { + match tag { + tags::CrateRoot => Self::CrateRoot, + tags::Impl => Self::Impl, + tags::ForeignMod => Self::ForeignMod, + tags::Use => Self::Use, + tags::GlobalAsm => Self::GlobalAsm, + tags::ClosureExpr => Self::ClosureExpr, + tags::Ctor => Self::Ctor, + tags::AnonConst => Self::AnonConst, + tags::ImplTrait => Self::ImplTrait, + tags::ImplTraitAssocTy => Self::ImplTraitAssocTy, + _ => None?, + } + } else { + let s = s.to_string(); + match tag { + tags::ValueNs => Self::ValueNs(s), + tags::TypeNs => Self::TypeNs(s), + tags::MacroNs => Self::MacroNs(s), + tags::LifetimeNs => Self::LifetimeNs(s), + _ => None?, + } + } + } else { + None? + }) + } +}