feat(cli): add a list-names verb, accept "raw" paths

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",

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::<hax_frontend_exporter::ThirBody>(
+ &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,

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<InclusionClause>,
 }
 
@@ -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(

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)

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 }
 

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

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<NamespaceChunk>,
+pub struct NamespacePattern {
+ chunks: Vec<NamespaceChunk>,
+}
+#[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<String> 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<String> for NamespacePattern {
  fn from(s: String) -> Self {
  Self {
  chunks: s
@@ -41,7 +58,7 @@ impl std::convert::From<String> for Namespace {
  }
 }
 
-impl Namespace {
+impl NamespacePattern {
  pub fn matches(&self, path: &Vec<String>) -> bool {
  fn aux(pattern: &[NamespaceChunk], path: &[String]) -> bool {
  match (pattern, path) {

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 == &macro_ident,
+ }) {
  Some((macro_ident, expn_data_ret))
  } else {
  None

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<H: std::hash::Hasher>(&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<S, DefId> for rustc_hir::def_id::DefId {
  fn sinto(&self, s: &S) -> DefId {

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<DisambiguatedDefPathItem>,
@@ -53,3 +53,138 @@ pub enum DefPathItem {
  ImplTrait,
  ImplTraitAssocTy,
 }
+
+impl std::hash::Hash for DefId {
+ fn hash<H: std::hash::Hasher>(&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<Self> {
+ const DUMMY_INDEX: (u32, u32) = (0, 0);
+ match s.split("::").collect::<Vec<_>>().as_slice() {
+ [krate, path @ ..] => Some(Self {
+ krate: krate.to_string(),
+ path: path
+ .iter()
+ .map(|item| DisambiguatedDefPathItem::deserialize_compact(item))
+ .collect::<Option<Vec<_>>>()?,
+ 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<Self> {
+ let mut disambiguator = 0;
+ let mut data_string = s;
+ if let Some((s, num)) = s.split_once("#") {
+ if let Ok(num) = num.parse::<u32>() {
+ 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<Self> {
+ 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?
+ })
+ }
+}