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

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

mod model_check;
mod precision;
mod proposition;
mod refinery;
mod space;

use log::{error, info, log_enabled, trace};
use machine_check_common::{ExecError, ExecResult};
use mck::concr::FullMachine;

use clap::{ArgGroup, Parser};
use proposition::Proposition;
use refinery::Refinery;

#[derive(Parser, Debug)]
#[clap(group(ArgGroup::new("property-group")
.required(true)
.multiple(true)
.args(&["property", "inherent"]),
))]
struct Args {
    #[arg(short, long)]
    batch: bool,

    #[arg(short, long, action = clap::ArgAction::Count)]
    verbose: u8,

    #[arg(long)]
    property: Option<String>,

    #[arg(long)]
    inherent: bool,

    #[arg(long)]
    use_decay: bool,
}

pub fn run<M: FullMachine>(system: M) {
    run_with_args(system, std::env::args())
}

pub fn run_with_args<M: FullMachine>(system: M, args: impl Iterator<Item = String>) {
    if let Err(err) = run_inner(system, args) {
        // log root error
        error!("{:#?}", err);
        // terminate with non-success code
        std::process::exit(-1);
    }
    // terminate successfully, the information is in stdout
}

fn run_inner<M: FullMachine>(
    system: M,
    args: impl Iterator<Item = String>,
) -> Result<ExecResult, anyhow::Error> {
    let args = Args::parse_from(args);
    // logging to stderr, stdout will contain the result in batch mode
    let filter_level = match args.verbose {
        0 => log::LevelFilter::Info,
        1 => log::LevelFilter::Debug,
        _ => log::LevelFilter::Trace,
    };
    env_logger::builder().filter_level(filter_level).init();

    info!("Starting verification.");

    let verification_result = verify(system, args.property.as_ref(), args.use_decay);

    if log_enabled!(log::Level::Trace) {
        trace!("Verification result: {:?}", verification_result);
    }

    if log_enabled!(log::Level::Info) {
        // the result will be propagated, just inform that we ended somehow
        match verification_result.result {
            Ok(_) => info!("Verification ended."),
            Err(_) => error!("Verification failed."),
        }
    }

    // serialize the verification result to stdout
    serde_json::to_writer(std::io::stdout(), &verification_result)?;
    Ok(verification_result)
}

fn verify<M: FullMachine>(system: M, property: Option<&String>, use_decay: bool) -> ExecResult {
    let mut refinery = Refinery::<M>::new(system, use_decay);
    let proposition = select_proposition(property);
    let result = match proposition {
        Ok(proposition) => refinery.verify_property(&proposition),
        Err(err) => Err(err),
    };

    ExecResult {
        result,
        stats: refinery.info(),
    }
}

fn select_proposition(property: Option<&String>) -> Result<Proposition, ExecError> {
    if let Some(property_str) = property {
        Proposition::parse(property_str)
    } else {
        // check for inherent panics without really checking a property, use constant true
        Ok(Proposition::Const(true))
    }
}