hax_rust_engine/
ocaml_engine.rs

1//! This module implements an interface to the OCaml hax engine. Via this
2//! interface, the rust engine can communicate with the OCaml engine, and reuse
3//! some of its components.
4
5use std::io::BufRead;
6
7use hax_frontend_exporter::ThirBody;
8use hax_types::engine_api::{
9    EngineOptions,
10    protocol::{FromEngine, ToEngine},
11};
12use serde::Deserialize;
13
14/// A query for the OCaml engine
15#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
16pub struct Query {
17    /// The version of hax currently used
18    pub hax_version: String,
19    /// Dictionary from `DefId`s to `impl_infos`
20    pub impl_infos: Vec<(
21        hax_frontend_exporter::DefId,
22        hax_frontend_exporter::ImplInfos,
23    )>,
24    /// The kind of query we want to send to the engine
25    pub kind: QueryKind,
26}
27
28/// The payload of the query. [`Response`] below mirrors this enum to represent
29/// the response from the engine.
30#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
31pub enum QueryKind {
32    /// Ask the OCaml engine to import the given THIR from the frontend
33    ImportThir {
34        /// The input THIR items
35        input: Vec<hax_frontend_exporter::Item<ThirBody>>,
36        /// Temporary option to enable a set of default phases
37        apply_phases: bool,
38        /// Translation options which contains include clauses (items filtering)
39        translation_options: hax_types::cli_options::TranslationOptions,
40    },
41}
42
43/// A Response after a [`Query`]
44#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
45pub enum Response {
46    /// Return imported THIR as an internal AST from Rust engine
47    ImportThir {
48        /// The output Rust AST items
49        output: Vec<crate::ast::Item>,
50    },
51}
52
53/// Extends the common `ToEngine` messages with one extra case: `Query`.
54#[derive(::serde::Deserialize, ::serde::Serialize)]
55#[serde(untagged)]
56pub enum ExtendedToEngine {
57    /// A standard `ToEngine` message
58    ToEngine(ToEngine),
59    /// A `Query`
60    Query(Box<hax_frontend_exporter::id_table::WithTable<EngineOptions>>),
61}
62
63/// Extends the common `FromEngine` messages with one extra case: `Response`.
64#[derive(Debug, Clone, ::schemars::JsonSchema, ::serde::Deserialize, ::serde::Serialize)]
65#[serde(untagged)]
66pub enum ExtendedFromEngine {
67    /// A standard `FromEngine` message
68    FromEngine(FromEngine),
69    /// A `Response`
70    Response(Response),
71}
72
73impl Query {
74    /// Execute the query synchronously.
75    pub fn execute(&self) -> Option<Response> {
76        use std::io::Write;
77        use std::process::Command;
78
79        macro_rules! send {
80            ($where: expr, $value:expr) => {
81                serde_json::to_writer(&mut $where, $value).unwrap();
82                $where.write_all(b"\n").unwrap();
83                $where.flush().unwrap();
84            };
85        }
86
87        let mut engine_subprocess = Command::new("hax-engine")
88            .arg("driver_rust_engine")
89            .stdin(std::process::Stdio::piped())
90            .stdout(std::process::Stdio::piped())
91            .spawn()
92            .unwrap();
93
94        let mut stdin = std::io::BufWriter::new(
95            engine_subprocess
96                .stdin
97                .as_mut()
98                .expect("Could not write on stdin"),
99        );
100
101        // TODO: send a table here (see https://github.com/cryspen/hax/issues/1536)
102        send!(stdin, self);
103
104        let mut response = None;
105        let stdout = std::io::BufReader::new(engine_subprocess.stdout.take().unwrap());
106        // TODO: this should be streaming (i.e. use a `LineAsEOF` reader wrapper that consumes a reader until `\n` occurs)
107        //       See https://github.com/cryspen/hax/issues/1537.
108        for slice in stdout.split(b'\n') {
109            let msg = (|| {
110                let slice = slice.ok()?;
111                let mut de = serde_json::Deserializer::from_slice(&slice);
112                de.disable_recursion_limit();
113                let de = serde_stacker::Deserializer::new(&mut de);
114                let msg = ExtendedFromEngine::deserialize(de);
115                msg.ok()
116            })()
117            .expect(
118                "Hax engine sent an invalid json value. \
119                                This might be caused by debug messages on stdout, \
120                                which is reserved for JSON communication with cargo-hax",
121            );
122
123            match msg {
124                ExtendedFromEngine::Response(res) => response = Some(res),
125                ExtendedFromEngine::FromEngine(FromEngine::Exit) => break,
126                // Proxy messages from the OCaml engine
127                ExtendedFromEngine::FromEngine(from_engine) => {
128                    crate::hax_io::write(&from_engine);
129                    if from_engine.requires_response() {
130                        let ExtendedToEngine::ToEngine(response) = crate::hax_io::read() else {
131                            panic!(
132                                "The frontend sent an incorrect message: expected `ExtendedToEngine::ToEngine` since we sent a `ExtendedFromEngine::FromEngine`."
133                            )
134                        };
135                        send!(stdin, &response);
136                    }
137                }
138            }
139        }
140        drop(stdin);
141
142        let exit_status = engine_subprocess.wait().unwrap();
143        if !exit_status.success() {
144            panic!("ocaml engine crashed");
145        }
146
147        response
148    }
149}
hax_rust_engine/ocaml_engine.rs

hax_rust_engine/
ocaml_engine.rs
