Add attributes #[skip] and refinement attributes

Cargo.toml

@@ -10,7 +10,7 @@ members = [
      "cli/driver",
      "test-harness",
 ]
-exclude = ["tests"]
+exclude = ["tests", "hax-lib-macros"]
 resolver = "2"
 
 [workspace.dependencies]

cli/driver/src/callbacks_wrapper.rs

@@ -0,0 +1,46 @@
+use const_format::formatcp;
+use hax_cli_options::{Command, ENV_VAR_OPTIONS_FRONTEND};
+
+use rustc_driver::{Callbacks, Compilation};
+use rustc_interface::{interface, Queries};
+use rustc_span::symbol::Symbol;
+
+/// Wraps a [Callbacks] structure, and injects some cache-related
+/// configuration in the `config` phase of rustc
+pub struct CallbacksWrapper<'a> {
+    pub sub: &'a mut (dyn Callbacks + Send + 'a),
+    pub options: hax_cli_options::Options,
+}
+impl<'a> Callbacks for CallbacksWrapper<'a> {
+    fn config(&mut self, config: &mut interface::Config) {
+        let options = self.options.clone();
+        config.parse_sess_created = Some(Box::new(move |parse_sess| {
+            parse_sess.env_depinfo.get_mut().insert((
+                Symbol::intern(hax_cli_options::ENV_VAR_OPTIONS_FRONTEND),
+                Some(Symbol::intern(&serde_json::to_string(&options).unwrap())),
+            ));
+        }));
+        self.sub.config(config)
+    }
+    fn after_parsing<'tcx>(
+        &mut self,
+        compiler: &interface::Compiler,
+        queries: &'tcx Queries<'tcx>,
+    ) -> Compilation {
+        self.sub.after_parsing(compiler, queries)
+    }
+    fn after_expansion<'tcx>(
+        &mut self,
+        compiler: &interface::Compiler,
+        queries: &'tcx Queries<'tcx>,
+    ) -> Compilation {
+        self.sub.after_expansion(compiler, queries)
+    }
+    fn after_analysis<'tcx>(
+        &mut self,
+        compiler: &interface::Compiler,
+        queries: &'tcx Queries<'tcx>,
+    ) -> Compilation {
+        self.sub.after_analysis(compiler, queries)
+    }
+}

cli/driver/src/driver.rs

@@ -7,11 +7,13 @@
 #![allow(unreachable_code)]
 #![allow(dead_code)]
 #![feature(macro_metavar_expr)]
+#![feature(internal_output_capture)]
 
 extern crate rustc_ast;
 extern crate rustc_data_structures;
 extern crate rustc_driver;
 extern crate rustc_errors;
+extern crate rustc_feature;
 extern crate rustc_hir;
 extern crate rustc_hir_analysis;
 extern crate rustc_index;
@@ -24,12 +26,20 @@ extern crate rustc_target;
 extern crate rustc_type_ir;
 
 mod exporter;
+
+use std::collections::HashSet;
+
 use exporter::ExtractionCallbacks;
 use hax_lint::Type;
 
 mod linter;
 use linter::LinterCallbacks;
 
+mod callbacks_wrapper;
+mod features;
+use callbacks_wrapper::*;
+use features::*;
+
 use const_format::formatcp;
 use hax_cli_options::{Command, ENV_VAR_OPTIONS_FRONTEND};
 
@@ -47,46 +57,6 @@ fn rustc_sysroot() -> String {
         .unwrap()
 }
 
-/// Wraps a [Callbacks] structure, and injects some cache-related
-/// configuration in the `config` phase of rustc
-struct CallbacksWrapper<'a> {
-    sub: &'a mut (dyn Callbacks + Send + 'a),
-    options: hax_cli_options::Options,
-}
-impl<'a> Callbacks for CallbacksWrapper<'a> {
-    fn config(&mut self, config: &mut interface::Config) {
-        let options = self.options.clone();
-        config.parse_sess_created = Some(Box::new(move |parse_sess| {
-            parse_sess.env_depinfo.get_mut().insert((
-                Symbol::intern(hax_cli_options::ENV_VAR_OPTIONS_FRONTEND),
-                Some(Symbol::intern(&serde_json::to_string(&options).unwrap())),
-            ));
-        }));
-        self.sub.config(config)
-    }
-    fn after_parsing<'tcx>(
-        &mut self,
-        compiler: &interface::Compiler,
-        queries: &'tcx Queries<'tcx>,
-    ) -> Compilation {
-        self.sub.after_parsing(compiler, queries)
-    }
-    fn after_expansion<'tcx>(
-        &mut self,
-        compiler: &interface::Compiler,
-        queries: &'tcx Queries<'tcx>,
-    ) -> Compilation {
-        self.sub.after_expansion(compiler, queries)
-    }
-    fn after_analysis<'tcx>(
-        &mut self,
-        compiler: &interface::Compiler,
-        queries: &'tcx Queries<'tcx>,
-    ) -> Compilation {
-        self.sub.after_analysis(compiler, queries)
-    }
-}
-
 fn setup_logging() {
     use tracing_subscriber::prelude::*;
     let enable_colors = {
@@ -122,6 +92,18 @@ fn main() {
         rustc_args.extend(vec!["--sysroot".into(), rustc_sysroot()])
     };
 
+    // When `HAX_FEATURES_DETECTION_MODE` is set, we just detect
+    // features for the current crate, output them in JSON on stdout
+    // and exit immediately
+    if std::env::var("HAX_FEATURES_DETECTION_MODE").is_ok() {
+        use std::io::BufWriter;
+        return serde_json::to_writer(
+            BufWriter::new(std::io::stdout()),
+            &Features::detect(&options, &rustc_args),
+        )
+        .unwrap();
+    }
+
     // fetch the correct callback structure given the command, and
     // coerce options
     let is_primary_package = std::env::var("CARGO_PRIMARY_PACKAGE").is_ok();
@@ -152,6 +134,23 @@ fn main() {
         Box::new(CallbacksNoop)
     };
 
+    if translate_package {
+        // We want to enable certain features, but only if the crate
+        // itself doesn't enable those
+        let features = Features {
+            adt_const_params: false,    // not useful for now
+            generic_const_exprs: false, // not useful for now
+            register_tool: true,
+            registered_tools: HashSet::from_iter(vec!["_hax".to_string()].into_iter()),
+        } - Features::detect_forking();
+        rustc_args = [rustc_args[0].clone()]
+            .into_iter()
+            .chain(["--cfg".into(), "hax_compilation".into()])
+            .chain(features.into_iter().map(|s| format!("-Zcrate-attr={}", s)))
+            .chain(rustc_args[1..].iter().cloned())
+            .collect();
+    };
+
     let mut callbacks = CallbacksWrapper {
         sub: &mut *callbacks,
         options: hax_cli_options::Options {

cli/driver/src/features.rs

@@ -0,0 +1,130 @@
+use std::collections::HashSet;
+
+use rustc_driver::{Callbacks, Compilation};
+use rustc_interface::{interface, Queries};
+use rustc_span::symbol::Symbol;
+
+use crate::callbacks_wrapper::CallbacksWrapper;
+
+use serde::{Deserialize, Serialize};
+
+/// A subset of `rustc_feature::Features` that is relevant to us
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct Features {
+    pub adt_const_params: bool,
+    pub generic_const_exprs: bool,
+    pub register_tool: bool,
+    pub registered_tools: HashSet<String>,
+}
+
+impl From<&rustc_feature::Features> for Features {
+    fn from(rfeatures: &rustc_feature::Features) -> Self {
+        Features {
+            adt_const_params: rfeatures.adt_const_params,
+            generic_const_exprs: rfeatures.generic_const_exprs,
+            register_tool: rfeatures.register_tool,
+            registered_tools: HashSet::new(),
+        }
+    }
+}
+
+impl core::ops::Sub for Features {
+    type Output = Self;
+    fn sub(self, rhs: Self) -> Self {
+        fn sub(x: bool, y: bool) -> bool {
+            x & !y
+        }
+        Features {
+            adt_const_params: sub(self.adt_const_params, rhs.adt_const_params),
+            generic_const_exprs: sub(self.generic_const_exprs, rhs.generic_const_exprs),
+            register_tool: sub(self.register_tool, rhs.register_tool),
+            registered_tools: self
+                .registered_tools
+                .difference(&rhs.registered_tools)
+                .cloned()
+                .collect(),
+        }
+    }
+}
+
+impl Default for Features {
+    fn default() -> Self {
+        (&rustc_feature::Features::default()).into()
+    }
+}
+
+impl Features {
+    pub fn into_iter(&self) -> impl Iterator<Item = String> {
+        [
+            self.adt_const_params.then_some("adt_const_params"),
+            self.generic_const_exprs.then_some("generic_const_exprs"),
+            self.register_tool.then_some("register_tool"),
+        ]
+        .into_iter()
+        .flatten()
+        .map(|s| format!("feature({})", s))
+        .chain(
+            self.registered_tools
+                .clone()
+                .into_iter()
+                .map(|tool| format!("register_tool({})", tool)),
+        )
+    }
+    /// Runs Rustc with a driver that only collects which unstable
+    /// Rustc features are enabled
+    pub fn detect(options: &hax_cli_options::Options, rustc_args: &Vec<String>) -> Self {
+        struct CollectFeatures {
+            features: Features,
+        }
+        impl Callbacks for CollectFeatures {
+            fn after_expansion<'tcx>(
+                &mut self,
+                compiler: &interface::Compiler,
+                queries: &'tcx Queries<'tcx>,
+            ) -> Compilation {
+                queries.global_ctxt().unwrap().enter(|tcx| {
+                    self.features = tcx.features().into();
+                    self.features.registered_tools = tcx
+                        .registered_tools(())
+                        .iter()
+                        .map(|x| x.name.to_ident_string())
+                        .collect();
+                });
+                rustc_driver::Compilation::Stop
+            }
+        }
+        let mut callbacks = CollectFeatures {
+            features: Features::default(),
+        };
+        let success = rustc_driver::catch_with_exit_code(|| {
+            rustc_driver::RunCompiler::new(
+                &rustc_args,
+                &mut CallbacksWrapper {
+                    sub: &mut callbacks,
+                    options: options.clone(),
+                },
+            )
+            .run()
+        }) == 0;
+        callbacks.features.clone()
+    }
+
+    /// Just like `detect`, but wraps the call in a subprocess so that
+    /// we can capture `stdout` and `stderr`: we don't want the use to
+    /// see error message from Rustc twice, or Cargo to have to parse
+    /// Rustc messages twice.
+    pub fn detect_forking() -> Self {
+        use std::process::{Command, Stdio};
+        let stdout = Command::new(std::env::args().next().unwrap())
+            .args(std::env::args().skip(1))
+            .env("HAX_FEATURES_DETECTION_MODE", "1")
+            .stdout(Stdio::piped())
+            .stderr(Stdio::piped())
+            .spawn()
+            .unwrap()
+            .wait_with_output()
+            .unwrap()
+            .stdout;
+        serde_json::from_str(&std::str::from_utf8(&stdout).unwrap()).unwrap()
+    }
+}