driver_hax_frontend_exporter/
exporter.rs

1use hax_frontend_exporter::SInto;
2use hax_frontend_exporter::state::LocalContextS;
3use hax_types::cli_options::{Backend, ENV_VAR_OPTIONS_FRONTEND, PathOrDash};
4use rustc_driver::{Callbacks, Compilation};
5use rustc_interface::interface;
6use rustc_interface::interface::Compiler;
7use rustc_middle::middle::region::Scope;
8use rustc_middle::ty::TyCtxt;
9use rustc_middle::{
10    thir,
11    thir::{Block, BlockId, Expr, ExprId, ExprKind, Pat, PatKind, Stmt, StmtId, StmtKind, Thir},
12};
13use rustc_span::symbol::Symbol;
14use serde::Serialize;
15use std::cell::RefCell;
16use std::collections::{HashMap, HashSet};
17use std::rc::Rc;
18
19/// Browse a crate and translate every item from HIR+THIR to "THIR'"
20/// (I call "THIR'" the AST described in this crate)
21#[tracing::instrument(skip_all)]
22fn convert_thir<'tcx, Body: hax_frontend_exporter::IsBody>(
23    options: &hax_frontend_exporter_options::Options,
24    tcx: TyCtxt<'tcx>,
25) -> (
26    Vec<rustc_span::Span>,
27    Vec<hax_frontend_exporter::DefId>,
28    Vec<(
29        hax_frontend_exporter::DefId,
30        hax_frontend_exporter::ImplInfos,
31    )>,
32    Vec<hax_frontend_exporter::Item<Body>>,
33    hax_frontend_exporter::id_table::Table,
34) {
35    use hax_frontend_exporter::WithGlobalCacheExt;
36    let state = hax_frontend_exporter::state::State::new(tcx, options.clone());
37
38    let result = tcx
39        .hir_free_items()
40        .map(|id| tcx.hir_item(id).sinto(&state))
41        .collect();
42    let impl_infos = hax_frontend_exporter::impl_def_ids_to_impled_types_and_bounds(&state)
43        .into_iter()
44        .collect();
45    let exported_spans = state.with_global_cache(|cache| cache.spans.keys().copied().collect());
46    let exported_def_ids = state.with_global_cache(|cache| {
47        cache
48            .per_item
49            .values()
50            .filter_map(|per_item_cache| per_item_cache.def_id.clone())
51            .collect()
52    });
53    let cache_map = state.with_global_cache(|cache| cache.id_table_session.table().clone());
54
55    (
56        exported_spans,
57        exported_def_ids,
58        impl_infos,
59        result,
60        cache_map,
61    )
62}
63
64/// Callback for extraction
65#[derive(Debug, Clone, Serialize)]
66pub(crate) struct ExtractionCallbacks {
67    pub body_types: Vec<hax_types::cli_options::ExportBodyKind>,
68}
69
70impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
71    fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter_options::Options {
72        hax_frontend_exporter_options::Options {
73            inline_anon_consts: true,
74            bounds_options: hax_frontend_exporter_options::BoundsOptions {
75                resolve_drop: false,
76                prune_sized: true,
77            },
78        }
79    }
80}
81
82impl Callbacks for ExtractionCallbacks {
83    fn config(&mut self, config: &mut rustc_interface::interface::Config) {
84        config.override_queries = Some(|_sess, providers| {
85            hax_frontend_exporter::override_queries_store_body(providers);
86        });
87    }
88    fn after_expansion<'tcx>(&mut self, compiler: &Compiler, tcx: TyCtxt<'tcx>) -> Compilation {
89        use std::ops::{Deref, DerefMut};
90
91        use hax_frontend_exporter::ThirBody;
92        use hax_types::cli_options::Command;
93        use rustc_session::config::CrateType;
94        use serde::{Deserialize, Serialize};
95        use std::fs::File;
96        use std::io::BufWriter;
97
98        use std::path::PathBuf;
99
100        let opts = &compiler.sess.opts;
101        let externs: Vec<_> = opts
102            .externs
103            .iter()
104            .flat_map(|(_, ext)| match &ext.location {
105                rustc_session::config::ExternLocation::ExactPaths(set) => set
106                    .iter()
107                    .map(|cp| cp.canonicalized())
108                    .collect::<Vec<_>>()
109                    .into_iter(),
110                _ => vec![].into_iter(),
111            })
112            .map(|path| path.with_extension("haxmeta"))
113            .collect();
114
115        let cg_metadata = opts.cg.metadata[0].clone();
116        let crate_name = opts.crate_name.clone().unwrap();
117
118        let output_dir = compiler.sess.io.output_dir.clone().unwrap();
119        let haxmeta_path = output_dir.join(format!("{crate_name}-{cg_metadata}.haxmeta",));
120
121        let mut file = BufWriter::new(File::create(&haxmeta_path).unwrap());
122
123        use hax_types::driver_api::{HaxMeta, with_kind_type};
124        with_kind_type!(
125            self.body_types.clone(),
126            <Body>|| {
127                let (spans, def_ids, impl_infos, items, cache_map) =
128                    convert_thir(&self.clone().into(), tcx);
129                let files: HashSet<PathBuf> = HashSet::from_iter(
130                    items
131                        .iter()
132                        .flat_map(|item| item.span.filename.to_path().map(|path| path.to_path_buf()))
133                );
134                let haxmeta: HaxMeta<Body> = HaxMeta {
135                    crate_name,
136                    cg_metadata,
137                    externs,
138                    impl_infos,
139                    items,
140                    comments: files.into_iter()
141                        .flat_map(|path|hax_frontend_exporter::comments::comments_of_file(path).ok())
142                        .flatten()
143                        .collect(),
144                    def_ids,
145                    hax_version: hax_types::HAX_VERSION.into(),
146                };
147                haxmeta.write(&mut file, cache_map);
148            }
149        );
150
151        let manifest_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap();
152        let manifest_dir = std::path::Path::new(&manifest_dir);
153
154        let data = hax_types::driver_api::EmitHaxMetaMessage {
155            manifest_dir: manifest_dir.to_path_buf(),
156            working_dir: opts
157                .working_dir
158                .to_path(rustc_span::FileNameDisplayPreference::Local)
159                .to_path_buf(),
160            path: haxmeta_path,
161        };
162        eprintln!(
163            "{}{}",
164            hax_types::driver_api::HAX_DRIVER_STDERR_PREFIX,
165            &serde_json::to_string(&hax_types::driver_api::HaxDriverMessage::EmitHaxMeta(data))
166                .unwrap()
167        );
168
169        Compilation::Stop
170    }
171}
driver_hax_frontend_exporter/exporter.rs

driver_hax_frontend_exporter/
exporter.rs
