hax_rust_engine/
debugger.rs

1//! An interactive debugger server for the rust engine.
2
3use crate::ast::span::Span;
4use crate::ast::*;
5use crate::phase::Phase as _;
6use crate::phase::PhaseKind;
7use crate::printer::SourceMap;
8
9macro_rules! declare_printers {
10    {$($name:ident = $printer:expr),*$(,)?} => {
11        /// Enumeration of all declared printers.
12        #[derive(Clone, Debug, Copy, serde::Serialize, serde::Deserialize)]
13        pub enum Printer {
14            $($name,)*
15            /// The printer of a backend
16            Backend(Backend),
17        }
18
19        impl Printer {
20            fn print_items(self, items: Vec<Item>) -> (String, SourceMap) {
21                let module = Module {
22                    ident: crate::names::rust_primitives::hax,
23                    items,
24                    meta: Metadata {
25                        span: Span::dummy(),
26                        attributes: vec![],
27                    },
28                };
29                match self {
30                    $(Self::$name => {
31                        $printer.print(module)
32                    }),*
33                    Self::Backend(backend) => backend.print_module(module),
34                }
35            }
36        }
37    };
38}
39macro_rules! declare_backends {
40    {$($name:ident = $backend:expr),*$(,)?} => {
41        /// Enumeration of all declared backends.
42        #[derive(Clone, Debug, Copy, serde::Serialize, serde::Deserialize)]
43        pub enum Backend {
44            $(
45                #[doc = concat!("The ", stringify!($name), " backend.")]
46                $name,
47            )*
48        }
49
50        impl Backend {
51            fn phases(self) -> Vec<PhaseKind> {
52                use crate::backends::Backend;
53                match self {
54                    $(
55                        Self::$name => $backend.phases(),
56                    )*
57                }
58            }
59            fn print_module(self, module: Module) -> (String, SourceMap) {
60                use crate::backends::Backend;
61                use crate::printer::Print;
62                let item_graph = crate::attributes::LinkedItemGraph::new(&module.items, crate::ast::diagnostics::Context::Debugger) ;
63                match self {
64                    $(
65                        Self::$name => $backend.printer(std::rc::Rc::new(item_graph)).print(module),
66                    )*
67                }
68            }
69        }
70    };
71}
72
73declare_backends! {
74    Lean = crate::backends::lean::LeanBackend,
75}
76
77declare_printers! {}
78
79/// A request to send to the debugger.
80#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
81pub enum Request {
82    /// Apply a given phase to the current items.
83    ApplyPhase(PhaseKind),
84    /// List the phases applied by a backend.
85    ListPhases(Backend),
86    /// Print the items with a given printer.
87    Print(Printer),
88    /// Dump the AST of the current items.
89    DumpAst(DumpAstOptions),
90}
91
92/// Options one can set when dumping ASTs.
93#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
94pub struct DumpAstOptions {
95    /// Sort the items via their global id. The order is not alphabetical, it is just deterministic.
96    pub sort_items_by_global_id: bool,
97    /// Drop `Use` items.
98    pub drop_use_items: bool,
99    /// Drop `RustModule` items.
100    pub drop_rust_modules_items: bool,
101    /// Drop `NotImplementedYet` items.
102    pub drop_not_implemented_yet_items: bool,
103    /// Drop every attributes in the AST.
104    pub drop_attributes: bool,
105    /// Erases spans, replacing them by `"erased"`.
106    /// Setting this to true will return untyped JSON.
107    pub erase_spans: bool,
108    /// Erases indices (e.g. local variable indices).
109    /// Setting this to true will return untyped JSON.
110    pub erase_indices: bool,
111}
112
113impl Default for DumpAstOptions {
114    fn default() -> Self {
115        Self {
116            sort_items_by_global_id: true,
117            drop_use_items: true,
118            drop_rust_modules_items: true,
119            drop_not_implemented_yet_items: true,
120            drop_attributes: true,
121            erase_spans: true,
122            erase_indices: true,
123        }
124    }
125}
126
127/// Response given by the debugger.
128#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
129pub enum Response {
130    /// Response for `Request::ApplyPhase`: a phase have been applied.
131    PhaseApplied(PhaseKind),
132    /// Response for `Request::ListPhase`: list the phases for a backend.
133    ListedPhases(Vec<PhaseKind>),
134    /// Response for `Request::Print`: items have been printed.
135    Printed {
136        /// The rendered printed items.
137        rendered: String,
138        /// The sourcemap.
139        source_map: SourceMap,
140    },
141    /// One of the possible response for `Request::DumpAst`. A AST was dumped as a typed JSON.
142    TypedDumpedAst(Vec<Item>),
143    /// One of the possible response for `Request::DumpAst`. A AST was dumped as an untyped JSON.
144    DumpedAst(serde_json::Value),
145    /// An error occured.
146    Error(String),
147}
148
149/// The state against which the debugger is working.
150pub struct State {
151    /// An immutable vector of items.
152    pub initial_items: Vec<Item>,
153    /// A sequence of requests.
154    pub requests: Vec<Request>,
155}
156
157impl State {
158    /// Compute the items at the current state
159    fn items(&self) -> Vec<Item> {
160        let mut items = self.initial_items.clone();
161        let phases = self.requests.iter().flat_map(|msg| match msg {
162            Request::ApplyPhase(phase) => Some(*phase),
163            _ => None,
164        });
165        for phase in phases {
166            phase.apply(&mut items);
167        }
168        items
169    }
170
171    /// Apply the request on a state.
172    pub fn apply(&mut self, req: Request) -> Response {
173        let mut items = self.items();
174        match req {
175            Request::ApplyPhase(phase) => {
176                phase.apply(&mut items);
177                Response::PhaseApplied(phase)
178            }
179            Request::Print(printer) => {
180                let (rendered, source_map) = printer.print_items(items);
181                Response::Printed {
182                    rendered,
183                    source_map,
184                }
185            }
186            Request::DumpAst(options) => {
187                let mut items: Vec<_> = items
188                    .into_iter()
189                    .filter(|it| {
190                        let drop = match &it.kind {
191                            ItemKind::Use { .. } => options.drop_use_items,
192                            ItemKind::RustModule => options.drop_rust_modules_items,
193                            ItemKind::NotImplementedYet => options.drop_not_implemented_yet_items,
194                            _ => false,
195                        };
196                        !drop
197                    })
198                    .collect();
199                if options.sort_items_by_global_id {
200                    items.sort_by_key(|item| serde_json::to_string_pretty(&item.ident).ok());
201                }
202                if options.drop_attributes {
203                    struct DropAttributes;
204                    use crate::ast::visitors::AstVisitorMut;
205                    impl AstVisitorMut for DropAttributes {
206                        fn visit_metadata(&mut self, x: &mut Metadata) {
207                            x.attributes = vec![];
208                        }
209                        fn visit_param(&mut self, x: &mut Param) {
210                            x.attributes = vec![];
211                        }
212                        fn visit_variant(&mut self, x: &mut Variant) {
213                            x.attributes = vec![];
214                        }
215                    }
216                    DropAttributes.visit(&mut items);
217                }
218                if options.erase_indices || options.erase_spans {
219                    let mut items = match serde_json::to_value(items) {
220                        Ok(value) => value,
221                        Err(err) => return Response::Error(err.to_string()),
222                    };
223                    use serde_json::Value;
224
225                    fn visit_json<F>(value: &mut Value, f: &F)
226                    where
227                        F: Fn(&mut Value),
228                    {
229                        f(value);
230
231                        match value {
232                            Value::Array(arr) => {
233                                for v in arr {
234                                    visit_json(v, f);
235                                }
236                            }
237                            Value::Object(map) => {
238                                for (_k, v) in map {
239                                    visit_json(v, f);
240                                }
241                            }
242                            Value::Null | Value::Bool(_) | Value::Number(_) | Value::String(_) => {}
243                        }
244                    }
245
246                    let erased = || Value::String("<erased>".to_string());
247                    visit_json(&mut items, &|value| {
248                        let Value::Object(map) = value else { return };
249                        if options.erase_indices {
250                            map.iter_mut()
251                                .filter(|(k, _)| matches!(k.as_str(), "id" | "index"))
252                                .for_each(|(_, value)| {
253                                    *value = erased();
254                                });
255                        }
256                        if options.erase_spans
257                            && map.contains_key("data")
258                            && map.contains_key("owner_hint")
259                            && map.contains_key("id")
260                        {
261                            *value = erased();
262                        }
263                    });
264
265                    Response::DumpedAst(items)
266                } else {
267                    Response::TypedDumpedAst(items)
268                }
269            }
270            Request::ListPhases(backend) => Response::ListedPhases(backend.phases()),
271        }
272    }
273}
274
275/// Entrypoint for the interactive HTTP debugger.
276pub fn http_interactive_debugger(items: Vec<Item>) {
277    use axum::{Json, Router, extract, routing::post};
278    use std::sync::Arc;
279
280    async fn process(
281        extract::State(items): extract::State<Arc<Vec<Item>>>,
282        Json((messages, message)): Json<(Vec<Request>, Request)>,
283    ) -> Json<Response> {
284        let mut state = State {
285            initial_items: items.to_vec(),
286            requests: messages,
287        };
288
289        Json(state.apply(message))
290    }
291
292    async fn serve(items: Vec<Item>) {
293        let state = Arc::new(items);
294
295        let app = Router::new()
296            .route("/process", post(process))
297            .with_state(state);
298        let listener = tokio::net::TcpListener::bind("127.0.0.1:0").await.unwrap();
299        let addr: std::net::SocketAddr = listener.local_addr().unwrap();
300        eprintln!("Listening on http://{addr}");
301        axum::serve(listener, app).await.unwrap();
302    }
303
304    let rt = tokio::runtime::Builder::new_current_thread()
305        .enable_all()
306        .build()
307        .unwrap();
308
309    rt.block_on(serve(items));
310}
hax_rust_engine/debugger.rs

hax_rust_engine/
debugger.rs
