machine_check_compile/
verify.rs

1mod build;
2mod execute;
3
4use std::time::Instant;
5
6use camino::{Utf8Path, Utf8PathBuf};
7use log::{debug, info, warn};
8use machine_check_common::ExecResult;
9use serde::{Deserialize, Serialize};
10use std::io::Write;
11use tempdir::TempDir;
12
13use crate::Error;
14
15pub struct Config {
16    pub abstract_machine: syn::File,
17    pub machine_path: Option<Utf8PathBuf>,
18    pub preparation_path: Option<Utf8PathBuf>,
19    pub batch: bool,
20    pub gui: bool,
21    pub property: Option<String>,
22    pub verbose: u8,
23    pub use_decay: bool,
24}
25
26#[derive(Debug, Serialize, Deserialize)]
27pub struct Stats {
28    pub transcription_time: Option<f64>,
29    pub build_time: Option<f64>,
30    pub execution_time: Option<f64>,
31    pub prepared: Option<bool>,
32}
33
34pub fn verify(config: Config) -> Result<ExecResult, Error> {
35    let mut stats = Stats {
36        transcription_time: None,
37        build_time: None,
38        execution_time: None,
39        prepared: None,
40    };
41
42    info!("Transcribing the system into a machine.");
43    let map_err = std::env::current_dir().map_err(Error::WorkDir);
44    let cwd = map_err?;
45    debug!("Current working directory is {:?}.", cwd);
46
47    let transcription_start = Instant::now();
48    let (machine_package_dir_path, machine_package_temp_dir) = write_machine(&config)?;
49    stats.transcription_time = Some(transcription_start.elapsed().as_secs_f64());
50
51    info!("Building a machine verifier.");
52    let build_start = Instant::now();
53    let artifact_path = build::build(&config, &mut stats, &machine_package_dir_path)?;
54    stats.build_time = Some(build_start.elapsed().as_secs_f64());
55
56    info!("Executing the machine verifier.");
57
58    let execution_start = Instant::now();
59    let exec_result = execute::execute(&config, &artifact_path)?;
60
61    stats.execution_time = Some(execution_start.elapsed().as_secs_f64());
62
63    info!("Stats: {:?}", stats);
64
65    // warn on error to close the temporary directory, it is not critical
66    if let Some(temp_dir) = machine_package_temp_dir {
67        debug!("Deleting temporary directory {:?}", temp_dir.path());
68        if let Err(err) = temp_dir.close() {
69            warn!(
70                "Could not close temporary directory for machine: {:#?}",
71                err
72            );
73        }
74    }
75
76    Ok(exec_result)
77}
78
79fn write_machine(arguments: &Config) -> Result<(Utf8PathBuf, Option<TempDir>), Error> {
80    // the machine package directory path can be given
81    // we will write the machine into a temporary directory if it is not given
82    // do not drop temporary directory too early
83    let (machine_package_dir_path, machine_package_temp_dir) = match &arguments.machine_path {
84        Some(path) => (path.clone(), None),
85        None => {
86            let temp_dir = TempDir::new("machine_check_machine_").map_err(Error::CreateTempDir)?;
87            let temp_dir_path = temp_dir.path().to_path_buf();
88            let temp_dir_path = Utf8PathBuf::try_from(temp_dir_path.clone())
89                .map_err(|err| Error::PathToUtf8(temp_dir_path, err))?;
90            (temp_dir_path, Some(temp_dir))
91        }
92    };
93
94    let src_dir_path = machine_package_dir_path.join("src");
95    std::fs::create_dir_all(&src_dir_path)
96        .map_err(|err| Error::CreateDir(src_dir_path.clone(), err))?;
97    let main_path = src_dir_path.join("main.rs");
98
99    write_syn_file(&main_path, &arguments.abstract_machine)?;
100    Ok((machine_package_dir_path, machine_package_temp_dir))
101}
102
103fn write_syn_file(filename: &Utf8Path, file: &syn::File) -> Result<(), Error> {
104    let mut fs_file = std::fs::File::create(filename)
105        .map_err(|err| Error::OpenFile(filename.to_path_buf(), err))?;
106
107    let pretty_machine = prettyplease::unparse(file);
108
109    fs_file
110        .write_all(pretty_machine.as_bytes())
111        .map_err(|err| Error::WriteFile(filename.to_path_buf(), err))
112}
machine_check_compile/verify.rs

machine_check_compile/
verify.rs
