1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
//! This module implements an interface to the OCaml hax engine. Via this
//! interface, the rust engine can communicate with the OCaml engine, and reuse
//! some of its components.
use std::{io::BufRead, sync::OnceLock};
use hax_frontend_exporter::{
ThirBody,
id_table::{Table, WithTable},
};
use hax_types::engine_api::protocol::{FromEngine, ToEngine};
use serde::Deserialize;
/// A query for the OCaml engine
#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
pub struct Query {
#[serde(flatten)]
meta: Meta,
/// The kind of query we want to send to the engine
kind: QueryKind,
}
/// The metadata required to perform a query.
#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
pub struct Meta {
/// The version of hax currently used
pub hax_version: String,
/// Dictionary from `DefId`s to `impl_infos`
pub impl_infos: Vec<(
hax_frontend_exporter::DefId,
hax_frontend_exporter::ImplInfos,
)>,
/// Enable debugging of phases in the OCaml engine
pub debug_bind_phase: bool,
/// Enable profiling in the OCaml engine
pub profiling: bool,
}
static STATE: OnceLock<Meta> = OnceLock::new();
/// Initialize query metadata.
pub fn initialize(meta: Meta) {
STATE
.set(meta)
.expect("`ocaml_engine::initialize` was called more than once")
}
/// The payload of the query. [`Response`] below mirrors this enum to represent
/// the response from the engine.
#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
pub enum QueryKind {
/// Ask the OCaml engine to import the given THIR from the frontend
ImportThir {
/// The input THIR items
input: Vec<hax_frontend_exporter::Item<ThirBody>>,
/// Translation options which contains include clauses (items filtering)
translation_options: hax_types::cli_options::TranslationOptions,
},
/// Ask the OCaml engine to run given phases on given items
ApplyPhases {
/// The phases to run. See `untyped_phases.ml`.
phases: Vec<String>,
/// The items on which the phases will be applied.
input: Vec<crate::ast::Item>,
},
/// Ask the OCaml engine to call an OCaml printer
Print {
/// Which printer to use
printer: hax_types::cli_options::Backend<()>,
/// The items after applying the phases.
input: Vec<crate::ast::Item>,
},
}
/// A Response after a [`Query`]
#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
pub enum Response {
/// Return imported THIR as an internal AST from Rust engine
ImportThir {
/// The output Rust AST items
output: Vec<crate::ast::Item>,
},
/// Return items after phase application
ApplyPhases {
/// The output Rust AST items after phases
output: Vec<crate::ast::Item>,
},
/// Printing was done successfully
PrintOk,
}
/// Extends the common `FromEngine` messages with one extra case: `Response`.
#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
#[serde(untagged)]
pub enum ExtendedFromEngine {
/// A standard `FromEngine` message
FromEngine(FromEngine),
/// A `Response`
Response(Response),
}
impl QueryKind {
/// Execute the query synchronously.
pub fn execute(self, table: Option<Table>) -> Option<Response> {
let query = Query {
meta: STATE
.get()
.expect("`ocaml_engine::initialize` should be called first")
.clone(),
kind: self,
};
use std::io::Write;
use std::process::Command;
macro_rules! send {
($where: expr, $value:expr) => {
serde_json::to_writer(&mut $where, $value).unwrap();
$where.write_all(b"\n").unwrap();
$where.flush().unwrap();
};
}
let mut engine_subprocess =
Command::new(std::env::var("HAX_ENGINE_BINARY").unwrap_or("hax-engine".into()))
.arg("driver_rust_engine")
.stdin(std::process::Stdio::piped())
.stdout(std::process::Stdio::piped())
.spawn()
.unwrap();
let mut stdin = std::io::BufWriter::new(
engine_subprocess
.stdin
.as_mut()
.expect("Could not write on stdin"),
);
if let Some(table) = table {
WithTable::run(table, query, |with_table| {
send!(stdin, with_table);
});
} else {
send!(stdin, &(vec![] as Vec<()>, query));
}
let mut response = None;
let stdout = std::io::BufReader::new(engine_subprocess.stdout.take().unwrap());
// TODO: this should be streaming (i.e. use a `LineAsEOF` reader wrapper that consumes a reader until `\n` occurs)
// See https://github.com/cryspen/hax/issues/1537.
for slice in stdout.split(b'\n') {
let msg = (|| {
let slice = slice.ok()?;
let mut de = serde_json::Deserializer::from_slice(&slice);
de.disable_recursion_limit();
let de = serde_stacker::Deserializer::new(&mut de);
let msg = ExtendedFromEngine::deserialize(de);
msg.ok()
})()
.expect(
"Hax engine sent an invalid json value. \
This might be caused by debug messages on stdout, \
which is reserved for JSON communication with cargo-hax",
);
match msg {
ExtendedFromEngine::Response(res) => response = Some(res),
ExtendedFromEngine::FromEngine(FromEngine::Exit) => break,
// Proxy messages from the OCaml engine
ExtendedFromEngine::FromEngine(from_engine) => {
crate::hax_io::write(&from_engine);
if from_engine.requires_response() {
let response: ToEngine = crate::hax_io::read_to_engine_message();
send!(stdin, &response);
}
}
}
}
drop(stdin);
let exit_status = engine_subprocess.wait().unwrap();
if !exit_status.success() {
panic!("ocaml engine crashed");
}
response
}
}