machine-check-compile 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112

mod build;
mod execute;

use std::time::Instant;

use camino::{Utf8Path, Utf8PathBuf};
use log::{debug, info, warn};
use machine_check_common::ExecResult;
use serde::{Deserialize, Serialize};
use std::io::Write;
use tempdir::TempDir;

use crate::Error;

pub struct Config {
    pub abstract_machine: syn::File,
    pub machine_path: Option<Utf8PathBuf>,
    pub preparation_path: Option<Utf8PathBuf>,
    pub batch: bool,
    pub gui: bool,
    pub property: Option<String>,
    pub verbose: u8,
    pub use_decay: bool,
}

#[derive(Debug, Serialize, Deserialize)]
pub struct Stats {
    pub transcription_time: Option<f64>,
    pub build_time: Option<f64>,
    pub execution_time: Option<f64>,
    pub prepared: Option<bool>,
}

pub fn verify(config: Config) -> Result<ExecResult, Error> {
    let mut stats = Stats {
        transcription_time: None,
        build_time: None,
        execution_time: None,
        prepared: None,
    };

    info!("Transcribing the system into a machine.");
    let map_err = std::env::current_dir().map_err(Error::WorkDir);
    let cwd = map_err?;
    debug!("Current working directory is {:?}.", cwd);

    let transcription_start = Instant::now();
    let (machine_package_dir_path, machine_package_temp_dir) = write_machine(&config)?;
    stats.transcription_time = Some(transcription_start.elapsed().as_secs_f64());

    info!("Building a machine verifier.");
    let build_start = Instant::now();
    let artifact_path = build::build(&config, &mut stats, &machine_package_dir_path)?;
    stats.build_time = Some(build_start.elapsed().as_secs_f64());

    info!("Executing the machine verifier.");

    let execution_start = Instant::now();
    let exec_result = execute::execute(&config, &artifact_path)?;

    stats.execution_time = Some(execution_start.elapsed().as_secs_f64());

    info!("Stats: {:?}", stats);

    // warn on error to close the temporary directory, it is not critical
    if let Some(temp_dir) = machine_package_temp_dir {
        debug!("Deleting temporary directory {:?}", temp_dir.path());
        if let Err(err) = temp_dir.close() {
            warn!(
                "Could not close temporary directory for machine: {:#?}",
                err
            );
        }
    }

    Ok(exec_result)
}

fn write_machine(arguments: &Config) -> Result<(Utf8PathBuf, Option<TempDir>), Error> {
    // the machine package directory path can be given
    // we will write the machine into a temporary directory if it is not given
    // do not drop temporary directory too early
    let (machine_package_dir_path, machine_package_temp_dir) = match &arguments.machine_path {
        Some(path) => (path.clone(), None),
        None => {
            let temp_dir = TempDir::new("machine_check_machine_").map_err(Error::CreateTempDir)?;
            let temp_dir_path = temp_dir.path().to_path_buf();
            let temp_dir_path = Utf8PathBuf::try_from(temp_dir_path.clone())
                .map_err(|err| Error::PathToUtf8(temp_dir_path, err))?;
            (temp_dir_path, Some(temp_dir))
        }
    };

    let src_dir_path = machine_package_dir_path.join("src");
    std::fs::create_dir_all(&src_dir_path)
        .map_err(|err| Error::CreateDir(src_dir_path.clone(), err))?;
    let main_path = src_dir_path.join("main.rs");

    write_syn_file(&main_path, &arguments.abstract_machine)?;
    Ok((machine_package_dir_path, machine_package_temp_dir))
}

fn write_syn_file(filename: &Utf8Path, file: &syn::File) -> Result<(), Error> {
    let mut fs_file = std::fs::File::create(filename)
        .map_err(|err| Error::OpenFile(filename.to_path_buf(), err))?;

    let pretty_machine = prettyplease::unparse(file);

    fs_file
        .write_all(pretty_machine.as_bytes())
        .map_err(|err| Error::WriteFile(filename.to_path_buf(), err))
}