machine-check-hw 0.7.1

System crate for machine-check for verification of BTOR2 files
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

#![doc = include_str!("../README.md")]

use camino::Utf8PathBuf;
use clap::{Parser, Subcommand};
use machine_check_common::ExecError;
use thiserror::Error;

pub mod prepare;
mod translate;
pub mod verify;

#[derive(Parser, Clone, Debug)]
#[command(author, version, about, long_about = None)]
pub struct Cli {
    /// Batch mode, prints result JSON to standard output.
    #[arg(global = true, short, long)]
    pub batch: bool,
    /// Verbose mode, one use enables debug, two uses enable trace.
    #[arg(global = true, short, long, action = clap::ArgAction::Count)]
    pub verbose: u8,
    /// Subcommand to execute.
    #[command(subcommand)]
    pub command: CliSubcommand,
}

#[derive(Debug, Clone, Subcommand)]
pub enum CliSubcommand {
    /// Prepare libraries used to build machines for faster verification.
    Prepare(prepare::Cli),
    /// Verify system properties.
    Verify(verify::Cli),
}

pub fn run(args: Cli) -> Result<(), CheckError> {
    let command = args.command.clone();
    match command {
        CliSubcommand::Prepare(prepare) => prepare::prepare(args, prepare),
        CliSubcommand::Verify(verify) => verify::run(args, verify),
    }
}

#[derive(Debug, Error)]
pub enum CheckError {
    #[error("{0}")]
    Machine(String),
    #[error("{0}")]
    Translate(String),
    #[error(transparent)]
    Compile(#[from] machine_check_compile::Error),
    #[error(transparent)]
    ExecError(#[from] ExecError),
    #[error("could not open file {0}")]
    OpenFile(Utf8PathBuf, #[source] std::io::Error),
    #[error("could not read file {0}")]
    ReadFile(Utf8PathBuf, #[source] std::io::Error),
    #[error("unknown system type: {0}")]
    SystemType(String),
}