driver_hax_frontend_exporter/
driver.rs

1#![feature(rustc_private)]
2#![feature(box_patterns)]
3#![feature(trait_alias)]
4#![allow(unused_imports)]
5#![allow(unused_variables)]
6#![allow(unreachable_code)]
7#![allow(dead_code)]
8#![feature(macro_metavar_expr)]
9#![feature(internal_output_capture)]
10
11extern crate rustc_ast;
12extern crate rustc_borrowck;
13extern crate rustc_data_structures;
14extern crate rustc_driver;
15extern crate rustc_errors;
16extern crate rustc_feature;
17extern crate rustc_hashes;
18extern crate rustc_hir;
19extern crate rustc_hir_analysis;
20extern crate rustc_index;
21extern crate rustc_interface;
22extern crate rustc_middle;
23extern crate rustc_mir_build;
24extern crate rustc_session;
25extern crate rustc_span;
26extern crate rustc_target;
27extern crate rustc_type_ir;
28
29mod exporter;
30
31use std::collections::HashSet;
32
33use exporter::ExtractionCallbacks;
34
35mod callbacks_wrapper;
36mod features;
37use callbacks_wrapper::*;
38use features::*;
39
40use hax_types::cli_options::{BackendOptions, Command, ENV_VAR_OPTIONS_FRONTEND};
41
42use rustc_driver::{Callbacks, Compilation};
43use rustc_interface::interface;
44use rustc_span::symbol::Symbol;
45
46fn rustc_sysroot() -> String {
47    std::process::Command::new("rustc")
48        .args(["--print", "sysroot"])
49        .output()
50        .ok()
51        .and_then(|out| String::from_utf8(out.stdout).ok())
52        .map(|s| s.trim().to_string())
53        .unwrap()
54}
55
56fn setup_logging() {
57    use tracing_subscriber::prelude::*;
58    let enable_colors = {
59        /* Respect [never] in [RUST_LOG_STYLE] */
60        !std::env::var("RUST_LOG_STYLE").is_ok_and(|style| style == "never")
61    };
62    let subscriber = tracing_subscriber::Registry::default()
63        .with(tracing_subscriber::EnvFilter::from_default_env())
64        .with(
65            tracing_tree::HierarchicalLayer::new(2)
66                .with_ansi(enable_colors)
67                .with_indent_lines(true),
68        );
69    tracing::subscriber::set_global_default(subscriber).unwrap();
70}
71
72const HAX_VANILLA_RUSTC: &str = "HAX_VANILLA_RUSTC";
73
74fn main() {
75    setup_logging();
76
77    let options: hax_types::cli_options::Options = serde_json::from_str(
78        &std::env::var(ENV_VAR_OPTIONS_FRONTEND).unwrap_or_else(|_| {
79            panic!(
80                "Cannot find environnement variable {}",
81                ENV_VAR_OPTIONS_FRONTEND
82            )
83        }),
84    )
85    .unwrap_or_else(|_| {
86        panic!(
87            "Invalid value for the environnement variable {}",
88            ENV_VAR_OPTIONS_FRONTEND
89        )
90    });
91
92    let mut rustc_args: Vec<String> = std::env::args().skip(1).collect();
93    // add [--sysroot] if not present
94    if !rustc_args.iter().any(|arg| arg.starts_with("--sysroot")) {
95        rustc_args.extend(vec!["--sysroot".into(), rustc_sysroot()])
96    };
97
98    // When `HAX_FEATURES_DETECTION_MODE` is set, we just detect
99    // features for the current crate, output them in JSON on stderr
100    // and exit immediately
101    if std::env::var("HAX_FEATURES_DETECTION_MODE").is_ok() {
102        use std::io::BufWriter;
103        return serde_json::to_writer(
104            BufWriter::new(std::io::stderr()),
105            &Features::detect(&options, &rustc_args),
106        )
107        .unwrap();
108    }
109
110    let (vanilla_rustc, vanilla_rustc_never) = {
111        let vanilla_rustc = std::env::var(HAX_VANILLA_RUSTC);
112        let vanilla_rustc_never = vanilla_rustc == Ok("never".into());
113        (
114            !vanilla_rustc_never && vanilla_rustc.is_ok(),
115            vanilla_rustc_never,
116        )
117    };
118
119    // fetch the correct callback structure given the command, and
120    // coerce options
121    let is_primary_package = std::env::var("CARGO_PRIMARY_PACKAGE").is_ok();
122    let is_build_script = std::env::var("CARGO_CRATE_NAME") == Ok("build_script_build".to_string()); // FIXME: is there a more robust way to do this?
123    let translate_package =
124        !vanilla_rustc && !is_build_script && (options.deps || is_primary_package);
125    let mut callbacks: Box<dyn Callbacks + Send> = if translate_package {
126        Box::new(exporter::ExtractionCallbacks {
127            body_types: options.command.body_kinds(),
128        })
129    } else {
130        struct CallbacksNoop;
131        impl Callbacks for CallbacksNoop {}
132        Box::new(CallbacksNoop)
133    };
134
135    if translate_package {
136        // We want to enable certain features, but only if the crate
137        // itself doesn't enable those
138        let features = Features {
139            adt_const_params: false,    // not useful for now
140            generic_const_exprs: false, // not useful for now
141            register_tool: true,
142            registered_tools: HashSet::from_iter(vec![hax_lib_macros_types::HAX_TOOL.into()]),
143            auto_traits: true,
144            negative_impls: true,
145        } - Features::detect_forking();
146        rustc_args = [rustc_args[0].clone()]
147            .into_iter()
148            .chain([
149                "--cfg".into(),
150                hax_lib_macros_types::HAX_CFG_OPTION_NAME.into(),
151            ])
152            .chain(match &options.command {
153                Command::Backend(BackendOptions { backend, .. }) => {
154                    vec!["--cfg".into(), format!("hax_backend_{backend}")]
155                }
156                _ => vec![],
157            })
158            .chain(features.into_iter().map(|s| format!("-Zcrate-attr={}", s)))
159            .chain(rustc_args[1..].iter().cloned())
160            .collect();
161    };
162
163    let mut callbacks = CallbacksWrapper {
164        sub: &mut *callbacks,
165        options: {
166            let mut options = options.clone();
167            options.force_cargo_build = if translate_package {
168                options.force_cargo_build
169            } else {
170                hax_types::cli_options::ForceCargoBuild::default()
171            };
172            options
173        },
174    };
175
176    let exit_code = rustc_driver::catch_with_exit_code({
177        let rustc_args = rustc_args.clone();
178        move || rustc_driver::run_compiler(&rustc_args, &mut callbacks)
179    });
180
181    std::process::exit(
182        if !vanilla_rustc_never && translate_package && exit_code == 0 {
183            // When the hax translation is successful, we need to re-run
184            // rustc. Indeed, hax translation doesn't actually build a
185            // package: no `rlib` will be written on disk.
186            self::vanilla_rustc()
187        } else {
188            exit_code
189        },
190    )
191}
192
193/// Re-run rustc without doing any hax translation. This ensures a
194/// `rlib` is produced (when the crate compiles correctly).
195fn vanilla_rustc() -> i32 {
196    use std::process::{Command, Stdio};
197    let output = Command::new(std::env::args().next().unwrap())
198        .args(std::env::args().skip(1))
199        .env(HAX_VANILLA_RUSTC, "1")
200        .stdout(Stdio::piped())
201        .stderr(Stdio::piped())
202        .spawn()
203        .unwrap()
204        .wait_with_output()
205        .unwrap();
206    if output.status.success() {
207        0
208    } else {
209        let stdout = &std::str::from_utf8(&output.stdout).unwrap();
210        let stderr = &std::str::from_utf8(&output.stderr).unwrap();
211        println!("{stdout}");
212        eprintln!("{stderr}");
213        output.status.code().unwrap_or(1)
214    }
215}
driver_hax_frontend_exporter/driver.rs

driver_hax_frontend_exporter/
driver.rs
