Merge pull request #1722 from cryspen/cargo-hax-haxmeta-verb

W95Psp · web-flow · commit 740e676add72 · 2025-09-30T13:22:05.000Z
feat(cli): support `haxmeta` explicit file manipulation
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -35,6 +35,7 @@ Changes to the frontend:
 
 Change to cargo-hax:
 - Improve the caching of rustc when using `cargo hax` commands (#1719)
+- Add hidden commands and flags to explicitly manipulate `haxmeta` files (#1722)
 
 Changes to hax-lib:
 - New behavior for `hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag.
diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
@@ -152,11 +152,12 @@ impl Callbacks for ExtractionCallbacks {
         let manifest_dir = std::path::Path::new(&manifest_dir);
 
         let data = hax_types::driver_api::EmitHaxMetaMessage {
-            manifest_dir: manifest_dir.to_path_buf(),
-            working_dir: opts
-                .working_dir
-                .to_path(rustc_span::FileNameDisplayPreference::Local)
-                .to_path_buf(),
+            manifest_dir: Some(manifest_dir.to_path_buf()),
+            working_dir: Some(
+                opts.working_dir
+                    .to_path(rustc_span::FileNameDisplayPreference::Local)
+                    .to_path_buf(),
+            ),
             path: haxmeta_path,
         };
         eprintln!(
diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs
@@ -169,9 +169,12 @@ impl HaxMessage {
             } => {
                 let mut _rctx = None;
                 let rctx = rctx.unwrap_or_else(|| _rctx.get_or_insert(ReportCtx::default()));
-                diagnostic.with_message(rctx, &working_dir, Level::Error, |msg| {
-                    eprintln!("{}", renderer.render(msg))
-                });
+                diagnostic.with_message(
+                    rctx,
+                    working_dir.as_ref().map(PathBuf::as_path),
+                    Level::Error,
+                    |msg| eprintln!("{}", renderer.render(msg)),
+                );
             }
             Self::EngineNotFound {
                 is_opam_setup_correctly,
@@ -258,8 +261,8 @@ impl HaxMessage {
 fn run_engine(
     haxmeta: HaxMeta<hax_frontend_exporter::ThirBody>,
     id_table: id_table::Table,
-    working_dir: PathBuf,
-    manifest_dir: PathBuf,
+    working_dir: Option<PathBuf>,
+    manifest_dir: Option<PathBuf>,
     backend: &BackendOptions<()>,
     message_format: MessageFormat,
 ) -> bool {
@@ -326,7 +329,9 @@ fn run_engine(
             ]
             .iter()
             .collect();
-            manifest_dir.join(&relative_path)
+            manifest_dir
+                .map(|manifest_dir| manifest_dir.join(&relative_path))
+                .unwrap_or(relative_path)
         });
 
         let stdout = std::io::BufReader::new(engine_subprocess.stdout.take().unwrap());
@@ -371,10 +376,12 @@ fn run_engine(
                                 .iter()
                                 .map(PathBuf::from)
                                 .map(|path| {
-                                    if path.is_absolute() {
-                                        path
-                                    } else {
+                                    if let Some(working_dir) = working_dir.as_ref()
+                                        && path.is_relative()
+                                    {
                                         working_dir.join(path).to_path_buf()
+                                    } else {
+                                        path
                                     }
                                 })
                                 .map(|path| fs::read_to_string(path).ok())
@@ -640,9 +647,29 @@ fn run_command(options: &Options, haxmeta_files: Vec<EmitHaxMetaMessage>) -> boo
                 path,
             } in haxmeta_files
             {
-                let (haxmeta, id_table): (HaxMeta<Body>, _) =
+                let (mut haxmeta, id_table): (HaxMeta<Body>, _) =
                     HaxMeta::read(fs::File::open(&path).unwrap());
 
+                if let Some(root_module) = &backend.prune_haxmeta {
+                    use hax_frontend_exporter::{DefPathItem, DisambiguatedDefPathItem, IsBody};
+
+                    /// Remove every item from an `HaxMeta` whose path is not `*::<root_module>::**`, where `root_module` is a string.
+                    fn prune_haxmeta<B: IsBody>(haxmeta: &mut HaxMeta<B>, root_module: &str) {
+                        haxmeta.items.retain(|item| match &item.owner_id.path[..] {
+                            [] => true,
+                            [
+                                DisambiguatedDefPathItem {
+                                    data: DefPathItem::TypeNs(s),
+                                    disambiguator: 0,
+                                },
+                                ..,
+                            ] => s == root_module,
+                            _ => false,
+                        })
+                    }
+                    prune_haxmeta(&mut haxmeta, root_module.as_str())
+                }
+
                 error = error
                     || run_engine(
                         haxmeta,
@@ -655,6 +682,12 @@ fn run_command(options: &Options, haxmeta_files: Vec<EmitHaxMetaMessage>) -> boo
             }
             error
         }
+        Command::Serialize { .. } => {
+            for EmitHaxMetaMessage { path, .. } in haxmeta_files {
+                HaxMessage::ProducedFile { path, wrote: true }.report(options.message_format, None);
+            }
+            false
+        }
     }
 }
 
@@ -679,7 +712,20 @@ fn main() {
     };
     options.normalize_paths();
 
-    let (haxmeta_files, exit_code) = compute_haxmeta_files(&options);
+    let (haxmeta_files, exit_code) = options
+        .haxmeta
+        .clone()
+        .map(|path| {
+            (
+                vec![EmitHaxMetaMessage {
+                    working_dir: None,
+                    manifest_dir: None,
+                    path,
+                }],
+                0,
+            )
+        })
+        .unwrap_or_else(|| compute_haxmeta_files(&options));
     let error = run_command(&options, haxmeta_files);
 
     std::process::exit(if exit_code == 0 && error {
diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs
@@ -341,6 +341,14 @@ pub struct BackendOptions<E: Extension> {
     #[arg(long)]
     pub profile: bool,
 
+    /// Prune Rust items that are not under the provided top-level module name.
+    /// This will effectively remove all items that don't match `*::<prune_haxmetadata>::**`.
+    /// This prunning occurs directly on the `haxmeta` file, in the frontend.
+    /// This is independent from any engine options.
+    #[arg(long)]
+    #[clap(hide = true)]
+    pub prune_haxmeta: Option<String>,
+
     /// Enable engine debugging: dumps the AST at each phase.
     ///
     /// The value of `<DEBUG_ENGINE>` can be either:
@@ -423,6 +431,29 @@ pub enum Command<E: Extension> {
         include_extra: bool,
     },
 
+    /// Serialize to a `haxmeta` file, the internal binary format used by hax to
+    /// store the ASTs produced by the hax exporter.
+    #[clap(hide = true)]
+    Serialize {
+        /// Whether the bodies are exported as THIR, built MIR, const
+        /// MIR, or a combination. Repeat this option to extract a
+        /// combination (e.g. `-k thir -k mir-built`). Pass `--kind`
+        /// alone with no value to disable body extraction.
+        #[arg(
+            value_enum,
+            short,
+            long = "kind",
+            num_args = 0..=3,
+            default_values_t = [ExportBodyKind::Thir]
+        )]
+        kind: Vec<ExportBodyKind>,
+
+        /// When extracting to a given backend, the exporter is called with different `cfg` options.
+        /// This option allows to set the same flags as `cargo hax into` would pick.
+        #[arg(short)]
+        backend: Option<BackendName>,
+    },
+
     #[command(flatten)]
     CliExtension(E::Command),
 }
@@ -431,7 +462,16 @@ impl<E: Extension> Command<E> {
     pub fn body_kinds(&self) -> Vec<ExportBodyKind> {
         match self {
             Command::JSON { kind, .. } => kind.clone(),
-            _ => vec![ExportBodyKind::Thir],
+            Command::Serialize { kind, .. } => kind.clone(),
+            Command::Backend { .. } | Command::CliExtension { .. } => vec![ExportBodyKind::Thir],
+        }
+    }
+    pub fn backend_name(&self) -> Option<BackendName> {
+        match self {
+            Command::Backend(backend_options) => Some((&backend_options.backend).into()),
+            Command::JSON { .. } => None,
+            Command::Serialize { backend, .. } => backend.clone(),
+            Command::CliExtension(_) => None,
         }
     }
 }
@@ -475,6 +515,12 @@ pub struct ExtensibleOptions<E: Extension> {
     #[arg(long = "deps")]
     pub deps: bool,
 
+    /// Provide a precomputed haxmeta file explicitly.
+    /// Setting this option bypasses rustc and the exporter altogether.
+    #[arg(long)]
+    #[clap(hide = true)]
+    pub haxmeta: Option<PathBuf>,
+
     /// By default, hax uses `$CARGO_TARGET_DIR/hax` as target folder,
     /// to avoid recompilation when working both with `cargo hax` and
     /// `cargo build` (or, e.g. `rust-analyzer`). This option disables
@@ -540,7 +586,7 @@ pub struct ExporterOptions {
 }
 
 #[derive_group(Serializers)]
-#[derive(JsonSchema, Debug, Clone, Copy)]
+#[derive(JsonSchema, ValueEnum, Debug, Clone, Copy)]
 pub enum BackendName {
     Fstar,
     Coq,
@@ -570,22 +616,17 @@ impl fmt::Display for BackendName {
 
 impl From<&Options> for ExporterOptions {
     fn from(options: &Options) -> Self {
-        let backend = match &options.command {
-            Command::Backend(backend_options) => Some((&backend_options.backend).into()),
-            _ => None,
-        };
-        let body_kinds = options.command.body_kinds();
         ExporterOptions {
             deps: options.deps,
             force_cargo_build: options.force_cargo_build.clone(),
-            backend,
-            body_kinds,
+            backend: options.command.backend_name(),
+            body_kinds: options.command.body_kinds(),
         }
     }
 }
 
-impl From<&Backend<()>> for BackendName {
-    fn from(backend: &Backend<()>) -> Self {
+impl<E: Extension> From<&Backend<E>> for BackendName {
+    fn from(backend: &Backend<E>) -> Self {
         match backend {
             Backend::Fstar { .. } => BackendName::Fstar,
             Backend::Coq { .. } => BackendName::Coq,
diff --git a/hax-types/src/diagnostics/message.rs b/hax-types/src/diagnostics/message.rs
@@ -7,7 +7,7 @@ use crate::prelude::*;
 pub enum HaxMessage {
     Diagnostic {
         diagnostic: super::Diagnostics,
-        working_dir: PathBuf,
+        working_dir: Option<PathBuf>,
     } = 254,
     EngineNotFound {
         is_opam_setup_correctly: bool,
diff --git a/hax-types/src/diagnostics/report.rs b/hax-types/src/diagnostics/report.rs
@@ -42,7 +42,7 @@ impl Diagnostics {
     pub fn with_message<R, F: for<'a> FnMut(Message<'a>) -> R>(
         &self,
         report_ctx: &mut ReportCtx,
-        working_dir: &Path,
+        working_dir: Option<&Path>,
         level: Level,
         mut then: F,
     ) -> R {
@@ -52,7 +52,9 @@ impl Diagnostics {
             if let Some(path) = span.filename.to_path() {
                 let source = {
                     let mut path = path.to_path_buf();
-                    if path.is_relative() {
+                    if let Some(working_dir) = working_dir
+                        && path.is_relative()
+                    {
                         path = working_dir.join(&path);
                     };
                     report_ctx.file_contents(path)
diff --git a/hax-types/src/driver_api.rs b/hax-types/src/driver_api.rs
@@ -5,8 +5,8 @@ pub const HAX_DRIVER_STDERR_PREFIX: &str = "::hax-driver::";
 #[derive_group(Serializers)]
 #[derive(Debug, Clone)]
 pub struct EmitHaxMetaMessage {
-    pub working_dir: PathBuf,
-    pub manifest_dir: PathBuf,
+    pub working_dir: Option<PathBuf>,
+    pub manifest_dir: Option<PathBuf>,
     pub path: PathBuf,
 }
 #[derive_group(Serializers)]
