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!("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.");
60        };
61        haxmeta
62    }
63}
64
65#[macro_export]
66macro_rules! with_kind_type {
67    ($kind:expr, <$t:ident>|| $body:expr) => {{
68        mod from {
69            pub use hax_types::cli_options::ExportBodyKind::{MirBuilt as MB, Thir as T};
70        }
71        mod to {
72            pub type T = hax_frontend_exporter::ThirBody;
73            pub type MB = hax_frontend_exporter::MirBody<hax_frontend_exporter::mir_kinds::Built>;
74        }
75        let mut kind: Vec<::hax_types::cli_options::ExportBodyKind> = $kind;
76        kind.sort();
77        kind.dedup();
78        match kind.as_slice() {
79            [from::MB] => {
80                type $t = to::MB;
81                $body
82            }
83            [from::T] => {
84                type $t = to::T;
85                $body
86            }
87            [from::T, from::MB] => {
88                type $t = (to::MB, to::T);
89                $body
90            }
91            [] => {
92                type $t = ();
93                $body
94            }
95            _ => panic!("Unsupported kind {:#?}", kind),
96        }
97    }};
98}
99pub use with_kind_type;
hax_types/driver_api.rs

hax_types/
driver_api.rs
