hax_types/
driver_api.rs

1use crate::prelude::*;
2
3pub const HAX_DRIVER_STDERR_PREFIX: &str = "::hax-driver::";
4
5#[derive_group(Serializers)]
6#[derive(Debug, Clone)]
7pub struct EmitHaxMetaMessage {
8    pub working_dir: PathBuf,
9    pub manifest_dir: PathBuf,
10    pub path: PathBuf,
11}
12#[derive_group(Serializers)]
13#[derive(Debug, Clone)]
14pub enum HaxDriverMessage {
15    EmitHaxMeta(EmitHaxMetaMessage),
16}
17
18#[derive_group(Serializers)]
19#[derive(Debug, Clone)]
20pub struct HaxMeta<Body: hax_frontend_exporter::IsBody> {
21    pub crate_name: String,
22    pub cg_metadata: String,
23    pub externs: Vec<PathBuf>,
24    pub items: Vec<hax_frontend_exporter::Item<Body>>,
25    pub impl_infos: Vec<(
26        hax_frontend_exporter::DefId,
27        hax_frontend_exporter::ImplInfos,
28    )>,
29    pub def_ids: Vec<hax_frontend_exporter::DefId>,
30    pub comments: Vec<(hax_frontend_exporter::Span, String)>,
31    pub hax_version: String,
32}
33
34use hax_frontend_exporter::id_table;
35
36impl<Body: hax_frontend_exporter::IsBody> HaxMeta<Body>
37where
38    Body: serde::Serialize + for<'de> serde::Deserialize<'de>,
39{
40    #[tracing::instrument(level = "trace", skip(self, write, id_table))]
41    pub fn write(self, write: &mut impl std::io::Write, id_table: id_table::Table) {
42        let mut write = zstd::stream::write::Encoder::new(write, 0).unwrap();
43
44        id_table::WithTable::run(id_table, self, |with_table| {
45            serde_brief::to_writer(with_table, &mut write).unwrap();
46            write.finish().unwrap();
47        })
48    }
49    #[tracing::instrument(level = "trace", skip(reader))]
50    pub fn read(reader: impl std::io::Read) -> (Self, id_table::Table) {
51        let reader = zstd::stream::read::Decoder::new(reader).unwrap();
52        let reader = std::io::BufReader::new(reader);
53        let haxmeta = id_table::WithTable::<HaxMeta<Body>>::destruct(
54            serde_brief::from_reader(reader).unwrap(),
55        );
56        if haxmeta.0.hax_version != crate::HAX_VERSION {
57            let version = haxmeta.0.hax_version;
58            let expected = crate::HAX_VERSION;
59            panic!(
60                "An invariant was broken: `*.haxmeta` was produced by hax version `{version}` while the current version of hax is `{expected}`. Please report this to https://github.com/hacspec/hax/issues."
61            );
62        };
63        haxmeta
64    }
65}
66
67#[macro_export]
68macro_rules! with_kind_type {
69    ($kind:expr, <$t:ident>|| $body:expr) => {{
70        mod from {
71            pub use hax_types::cli_options::ExportBodyKind::{MirBuilt as MB, Thir as T};
72        }
73        mod to {
74            pub type T = hax_frontend_exporter::ThirBody;
75            pub type MB = hax_frontend_exporter::MirBody<hax_frontend_exporter::mir_kinds::Built>;
76        }
77        let mut kind: Vec<::hax_types::cli_options::ExportBodyKind> = $kind;
78        kind.sort();
79        kind.dedup();
80        match kind.as_slice() {
81            [from::MB] => {
82                type $t = to::MB;
83                $body
84            }
85            [from::T] => {
86                type $t = to::T;
87                $body
88            }
89            [from::T, from::MB] => {
90                type $t = (to::MB, to::T);
91                $body
92            }
93            [] => {
94                type $t = ();
95                $body
96            }
97            _ => panic!("Unsupported kind {:#?}", kind),
98        }
99    }};
100}
101pub use with_kind_type;
hax_types/driver_api.rs

hax_types/
driver_api.rs
