machine_check_exec/
lib.rs

1#![doc = include_str!("../README.md")]
2
3mod framework;
4mod model_check;
5mod precision;
6mod proposition;
7mod space;
8
9use log::{error, info, log_enabled, trace};
10use machine_check_common::ExecResult;
11use mck::concr::FullMachine;
12
13use clap::{ArgGroup, Args, Parser};
14use framework::{Framework, Strategy};
15use proposition::Proposition;
16
17/// Arguments for executing machine-check.
18#[derive(Parser, Debug)]
19#[clap(group(ArgGroup::new("property-group")
20.required(true)
21.multiple(true)
22.args(&["property", "inherent"]),
23))]
24#[clap(group(ArgGroup::new("verbosity-group")
25.required(false)
26.multiple(false)
27.args(&["silent", "verbose"]),
28))]
29#[clap(group(ArgGroup::new("assume-inherent-group")
30.required(false)
31.multiple(false)
32.conflicts_with("inherent")
33.args(&["assume_inherent"]),
34))]
35pub struct ExecArgs {
36    #[arg(long)]
37    pub silent: bool,
38
39    #[arg(short, long, action = clap::ArgAction::Count)]
40    pub verbose: u8,
41
42    #[arg(long)]
43    pub batch: bool,
44
45    #[arg(long)]
46    pub property: Option<String>,
47
48    #[arg(long)]
49    pub inherent: bool,
50
51    // experimental flags
52    #[arg(long)]
53    pub naive_inputs: bool,
54    #[arg(long)]
55    pub use_decay: bool,
56    #[arg(long)]
57    pub assume_inherent: bool,
58}
59
60#[derive(Parser, Debug)]
61struct ProgramArgs<A: Args> {
62    #[clap(flatten)]
63    run_args: ExecArgs,
64    #[clap(flatten)]
65    system_args: A,
66}
67
68/// Parses machine-check and user-defined arguments.
69///
70/// Returns arguments parsed to `machine-check` and system-specific argument definitions.
71/// The arguments can be later used in [`execute`].
72pub fn parse_args<A: Args>(args: impl Iterator<Item = String>) -> (ExecArgs, A) {
73    let parsed_args = ProgramArgs::<A>::parse_from(args);
74    (parsed_args.run_args, parsed_args.system_args)
75}
76
77/// Executes machine-check with system environment arguments.
78///
79/// Is supposed to be used for simple systems that do not take arguments.
80pub fn run<M: FullMachine>(system: M) -> ExecResult {
81    let parsed_args = ExecArgs::parse_from(std::env::args());
82    execute(system, parsed_args)
83}
84
85/// Executes machine-check with parsed arguments.
86///
87/// The arguments can be parsed using [`parse_args`].
88pub fn execute<M: FullMachine>(system: M, exec_args: ExecArgs) -> ExecResult {
89    // logging to stderr, stdout will contain the result in batch mode
90    let silent = exec_args.silent;
91    let batch = exec_args.batch;
92    let mut filter_level = match exec_args.verbose {
93        0 => log::LevelFilter::Info,
94        1 => log::LevelFilter::Debug,
95        _ => log::LevelFilter::Trace,
96    };
97    if silent {
98        filter_level = log::LevelFilter::Off;
99    }
100
101    // initialize logger, but do not panic if it was already initialized
102    let _ = env_logger::builder().filter_level(filter_level).try_init();
103
104    info!("Starting verification.");
105
106    let verification_result = verify(system, exec_args);
107
108    if log_enabled!(log::Level::Trace) {
109        trace!("Verification result: {:?}", verification_result);
110    }
111
112    if log_enabled!(log::Level::Info) {
113        // the result will be propagated, just inform that we ended somehow
114        match verification_result.result {
115            Ok(_) => info!("Verification ended."),
116            Err(_) => error!("Verification failed."),
117        }
118    }
119
120    if !silent {
121        if batch {
122            // serialize the verification result to stdout
123            if let Err(err) = serde_json::to_writer(std::io::stdout(), &verification_result) {
124                panic!("Could not serialize verification result: {:?}", err);
125            }
126        } else {
127            // TODO: nicer result printing
128            info!("Verification result: {:?}", verification_result);
129        }
130    }
131    verification_result
132}
133
134/// Verifies the given system with given arguments.
135fn verify<M: FullMachine>(system: M, run_args: ExecArgs) -> ExecResult {
136    let strategy = Strategy {
137        naive_inputs: run_args.naive_inputs,
138        use_decay: run_args.use_decay,
139    };
140    let mut refinery = Framework::<M>::new(system, strategy);
141
142    let result = if let Some(property_str) = run_args.property {
143        Proposition::parse(&property_str).map(Some)
144    } else {
145        // check for inherent panics without really checking a property, use constant true
146        Ok(None)
147    };
148    let result = result
149        .and_then(|proposition| refinery.verify_property(&proposition, run_args.assume_inherent));
150
151    ExecResult {
152        result,
153        stats: refinery.info(),
154    }
155}
machine_check_exec/lib.rs

machine_check_exec/
lib.rs
