machine_check_gui/
backend.rs

1use std::{borrow::Cow, ffi::OsStr, path::Path};
2
3use http::{header::CONTENT_TYPE, Method};
4use include_dir::{include_dir, Dir};
5use log::{debug, error};
6use machine_check_common::{
7    iir::{description::IMachine, property::IProperty},
8    ExecError, PropertyMacros,
9};
10use machine_check_exec::{Framework, Strategy};
11use mck::concr::FullMachine;
12use sync::BackendSync;
13use window::Window;
14use workspace::Workspace;
15use wry::WebViewId;
16
17use crate::shared::{BackendSpaceInfo, Request};
18
19mod sync;
20mod window;
21mod workspace;
22
23const FAVICON_ICO: &[u8] = include_bytes!("../content/favicon.ico");
24
25/// Runs the Graphical User Interface backend.
26pub fn run<M: FullMachine, D: Send + 'static>(
27    abstract_system: M::Abstr,
28    machine: IMachine,
29    property: Option<IProperty>,
30    property_macros: PropertyMacros<D>,
31    strategy: Strategy,
32) -> Result<(), ExecError> {
33    // TODO: allow setting custom titles instead of relying on the binary name
34    let exec_name = std::env::current_exe()
35        .ok()
36        .as_ref()
37        .map(Path::new)
38        .and_then(Path::file_stem)
39        .and_then(OsStr::to_str)
40        .map(String::from)
41        .unwrap_or(String::from("Unknown executable"));
42
43    // create the backend
44    let backend = Backend::new(
45        Workspace::<M, D>::new(
46            Framework::new(abstract_system, machine, strategy),
47            property,
48            property_macros,
49        ),
50        exec_name.clone(),
51    );
52    let response_fn = move |_web_view_id: WebViewId, request: http::Request<Vec<u8>>| {
53        backend.get_http_response(request)
54    };
55
56    // initialise the GUI
57    let gui = match Window::new(response_fn, &exec_name) {
58        Ok(ok) => ok,
59        Err(err) => {
60            error!("Cannot create GUI: {}", err);
61            return Err(ExecError::GuiError(err.to_string()));
62        }
63    };
64    // run the GUI, never returns
65    gui.run()
66}
67
68/// The backend structure.
69struct Backend {
70    sync: BackendSync,
71}
72
73/// Simple stats that are provided to the frontend upon request.
74///
75/// These are provided even if the backend is working and cannot
76/// generate a snapshot.
77struct BackendStats {
78    should_cancel: bool,
79    space_info: BackendSpaceInfo,
80}
81
82impl BackendStats {
83    fn new<M: FullMachine>(framework: &mut Framework<M>) -> Self {
84        Self {
85            should_cancel: false,
86            space_info: extract_space_info(framework),
87        }
88    }
89}
90
91fn extract_space_info<M: FullMachine>(framework: &mut Framework<M>) -> BackendSpaceInfo {
92    let num_refinements = framework.info().num_refinements;
93    let num_states = framework.info().num_final_states;
94    let num_transitions = framework.info().num_final_transitions;
95    BackendSpaceInfo {
96        num_refinements,
97        num_states,
98        num_transitions,
99    }
100}
101
102struct BackendSettings {
103    exec_name: String,
104}
105
106const CONTENT_DIR: Dir = include_dir!("content");
107
108impl Backend {
109    /// Constructs the backend.
110    pub fn new<M: FullMachine, D: Send + 'static>(
111        mut workspace: Workspace<M, D>,
112        exec_name: String,
113    ) -> Self {
114        let stats = BackendStats::new(&mut workspace.framework);
115        let settings = BackendSettings { exec_name };
116        let sync = BackendSync::new(workspace, stats, settings);
117        Self { sync }
118    }
119
120    /// Provides a response to an HTTP request from the frontend.
121    ///
122    /// This is done using the custom WebView protocol, but still is in the HTTP format.
123    fn get_http_response(
124        &self,
125        request: http::Request<Vec<u8>>,
126    ) -> http::Response<Cow<'static, [u8]>> {
127        // handle errors by printing them and sending 500
128        self.get_http_response_or_error(request)
129            .unwrap_or_else(|err| {
130                error!("Cannot produce a response to frontend: {}", err);
131                let response = http::Response::builder()
132                    .header(CONTENT_TYPE, "text/plain")
133                    .status(500)
134                    .body(Cow::Borrowed("Internal Server Error".as_bytes()))
135                    .expect("Internal server error response should be constructable");
136                response
137            })
138    }
139
140    fn get_http_response_or_error(
141        &self,
142        request: http::Request<Vec<u8>>,
143    ) -> Result<http::Response<Cow<'static, [u8]>>, Box<dyn std::error::Error>> {
144        // read URI path
145        let uri_path = request.uri().path();
146        let method = request.method();
147        debug!("Serving: {}", uri_path);
148
149        // strip the leading slash
150        // also accept empty path
151        let path = match uri_path.strip_prefix('/') {
152            Some(path) => path,
153            None => {
154                if uri_path.is_empty() {
155                    ""
156                } else {
157                    return Err(anyhow::anyhow!(
158                        "Path not empty or starting with slash: {}",
159                        uri_path
160                    )
161                    .into());
162                }
163            }
164        };
165
166        // if the stripped path is empty, serve index.html
167        let path = if path.is_empty() { "index.html" } else { path };
168
169        if path == "api" {
170            // API call
171            if method != Method::POST {
172                return Err(anyhow::anyhow!("API method must be POST").into());
173            }
174
175            self.get_api_response(request)
176        } else {
177            // not an API call, return content
178            if method != Method::GET {
179                return Err(anyhow::anyhow!("Expected method GET: {}", path).into());
180            }
181
182            Self::get_content_response(path)
183        }
184    }
185
186    fn get_content_response(
187        path: &str,
188    ) -> Result<http::Response<Cow<'static, [u8]>>, Box<dyn std::error::Error>> {
189        let content = match CONTENT_DIR.get_file(path) {
190            Some(file) => file.contents(),
191            None => return Err(anyhow::anyhow!("Not found: {}", path).into()),
192        };
193
194        let content_type: Cow<str> = Cow::Owned(
195            mime_guess::from_path(path)
196                .first()
197                .expect("Content should have known content type")
198                .to_string(),
199        );
200
201        http::Response::builder()
202            .header(CONTENT_TYPE, content_type.as_ref())
203            .body(Cow::Borrowed(content))
204            .map_err(Into::into)
205    }
206
207    fn get_api_response(
208        &self,
209        request: http::Request<Vec<u8>>,
210    ) -> Result<http::Response<Cow<'static, [u8]>>, Box<dyn std::error::Error>> {
211        // as posting the request content in the body seems buggy (we can encounter
212        // an empty body instead), the request body is instead sent in the header
213        // X-Body, encoded into a hex
214        let x_body = request
215            .headers()
216            .get("X-Body")
217            .ok_or(anyhow::anyhow!("Request has no X-Body header"))?;
218        let x_body = x_body
219            .to_str()
220            .map_err(|_| anyhow::anyhow!("Request X-Body header is not ASCII"))?;
221        let decoded_body = hex::decode(x_body).map_err(|err| {
222            anyhow::anyhow!("Request X-Body header does not contain hex: {}", err)
223        })?;
224        let request: Request = rmp_serde::from_slice(&decoded_body).map_err(|err| {
225            anyhow::anyhow!(
226                "Request X-Body header does not contain valid MessagePack data: {}",
227                err
228            )
229        })?;
230
231        // create the response
232        let response = self.sync.command(request);
233
234        // msgpack the response
235        let content_msgpack = rmp_serde::to_vec(&response)?;
236        http::Response::builder()
237            .header(CONTENT_TYPE, "application/vnd.msgpack")
238            .body(Cow::Owned(content_msgpack))
239            .map_err(Into::into)
240    }
241}