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

machine_check_gui/
backend.rs
