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: Option<PathBuf>,
9    pub manifest_dir: Option<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(JsonSchema, Debug, Clone)]
20pub enum Items<Body: hax_frontend_exporter::IsBody> {
21    FullDef(Vec<hax_frontend_exporter::FullDef<Body>>),
22    Legacy(Vec<hax_frontend_exporter::Item<Body>>),
23}
24
25#[derive_group(Serializers)]
26#[derive(Debug, Clone)]
27pub struct HaxMeta<Body: hax_frontend_exporter::IsBody> {
28    pub crate_name: String,
29    pub cg_metadata: String,
30    pub externs: Vec<PathBuf>,
31    pub items: Items<Body>,
32    pub impl_infos: Vec<(
33        hax_frontend_exporter::DefId,
34        hax_frontend_exporter::ImplInfos,
35    )>,
36    pub def_ids: Vec<hax_frontend_exporter::DefId>,
37    pub comments: Vec<(hax_frontend_exporter::Span, String)>,
38    pub hax_version: String,
39}
40
41use hax_frontend_exporter::id_table;
42
43impl<Body: hax_frontend_exporter::IsBody> HaxMeta<Body>
44where
45    Body: serde::Serialize + for<'de> serde::Deserialize<'de>,
46{
47    #[tracing::instrument(level = "trace", skip(self, write, id_table))]
48    pub fn write(self, write: &mut impl std::io::Write, id_table: id_table::Table) {
49        let mut write = zstd::stream::write::Encoder::new(write, 0).unwrap();
50
51        id_table::WithTable::run(id_table, self, |with_table| {
52            serde_brief::to_writer(with_table, &mut write).unwrap();
53            write.finish().unwrap();
54        })
55    }
56    #[tracing::instrument(level = "trace", skip(reader))]
57    pub fn read(reader: impl std::io::Read) -> (Self, id_table::Table) {
58        let reader = zstd::stream::read::Decoder::new(reader).unwrap();
59        let reader = std::io::BufReader::new(reader);
60        let haxmeta = id_table::WithTable::<HaxMeta<Body>>::destruct(
61            serde_brief::from_reader(reader).unwrap(),
62        );
63        if haxmeta.0.hax_version != crate::HAX_VERSION {
64            let version = haxmeta.0.hax_version;
65            let expected = crate::HAX_VERSION;
66            panic!(
67                "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."
68            );
69        };
70        haxmeta
71    }
72}
73
74#[macro_export]
75macro_rules! with_kind_type {
76    ($kind:expr, <$t:ident>|| $body:expr) => {{
77        mod from {
78            pub use hax_types::cli_options::ExportBodyKind::{MirBuilt as MB, Thir as T};
79        }
80        mod to {
81            pub type T = hax_frontend_exporter::ThirBody;
82            pub type MB = hax_frontend_exporter::MirBody<hax_frontend_exporter::mir_kinds::Built>;
83        }
84        let mut kind: Vec<::hax_types::cli_options::ExportBodyKind> = $kind;
85        kind.sort();
86        kind.dedup();
87        match kind.as_slice() {
88            [from::MB] => {
89                type $t = to::MB;
90                $body
91            }
92            [from::T] => {
93                type $t = to::T;
94                $body
95            }
96            [from::T, from::MB] => {
97                type $t = (to::MB, to::T);
98                $body
99            }
100            [] => {
101                type $t = ();
102                $body
103            }
104            _ => panic!("Unsupported kind {:#?}", kind),
105        }
106    }};
107}
108pub use with_kind_type;
hax_types/driver_api.rs

hax_types/
driver_api.rs
