machine_check/
lib.rs

1#![doc = include_str!("../README.md")]
2
3mod traits;
4mod types;
5
6pub use traits::Ext;
7pub use types::{Bitvector, BitvectorArray, Signed, Unsigned};
8
9/// Input to [`Machine`].
10pub use ::mck::concr::Input;
11
12/// State of [`Machine`].
13pub use ::mck::concr::State;
14
15/// Finite-state machine intended to be verifiable by **machine-check**.
16///
17/// To actually be verifiable by **machine-check**, further processing must be done by enclosing the structures
18/// and [`Input`], [`State`], and [`Machine`] implementations within the [`machine_description`] macro.
19///
20pub use ::mck::concr::Machine;
21
22/// Switch using a bitmask as scrutinee, useful for switching on processor instruction opcodes.
23///
24/// The switch is similar to a normal Rust match expression:
25/// ```
26/// use machine_check::{Bitvector, bitmask_switch};
27/// let opcode = Bitvector::<6>::new(0b10_1101);
28/// let mut foo = Bitvector::<2>::new(0);
29/// let mut bar = Bitvector::<2>::new(0);
30/// bitmask_switch!(opcode {
31///    "00_----" => {}
32///    "10_aabb" => {
33///         foo = a;
34///         bar = b;
35///    }
36///    "11_--cc" => {
37///         foo = c;
38///    }
39///    _ => {}
40/// });
41/// assert_eq!(foo, Bitvector::new(3));
42/// assert_eq!(bar, Bitvector::new(1));
43/// ```
44///
45/// Unlike Rust match, the scrutinee must be [`Bitvector`], and the non-default choices are string literals
46/// containing, for each bit of the bitvector, one of these:
47/// - '0' or '1': the bit must match,
48/// - dash ('-'): the bit can have any value (don't care),
49/// - ASCII letter: same as don't care, but a new variable is created containing the bits with given letter.
50/// Underscore ('_') can be used to visually separate the bits.
51///
52/// Unlike Rust match, overlapping choices are not permitted, so that it is certain which arm is taken.
53/// In case there is no default arm, there must be full coverage.
54///
55/// Currently, the macro cannot return values and there is no syntactic disjunction guarantee, i.e. that
56/// exactly one of the arms is taken. This may change in the future.
57///
58///
59pub use ::machine_check_macros::bitmask_switch;
60
61/// Processes a module so that it can be used in **machine-check** verification.
62///
63/// To efficiently verify a system with **machine-check**, verification equivalents of the system that allow
64/// more advanced reasoning (e.g. not caring about the value of some variable unless found to be necessary)
65/// must be created, which is done by enclosing the system code in a module and applying this macro on it.
66///
67/// In practice, everything used in [`Machine`] must be processed by this macro. System construction,
68/// however, can (and should) be done outside.
69///
70/// Note that, due to [a Rust issue](https://github.com/rust-lang/rust/issues/54726), procedural macros
71/// currently cannot be used as inner attributes, so this is the currently recommended way of
72/// using the macro:
73/// ```
74/// #[machine_check::machine_description]
75/// mod machine_module {
76///     // ... structs implementing Input, State, Machine ...
77/// }
78/// ```
79///
80/// The macro is currently rather limited in the subset of Rust code it can process, and errors may be cryptic.
81/// Improvements are planned in the future. For now, the examples in the crate show code processable without errors.
82///
83pub use ::machine_check_macros::machine_description;
84
85/// Runs **machine-check** with the given constructed system.
86///  
87/// The system must implement [`Machine`]. The system structures and [`Input`], [`State`], and [`Machine`]
88/// implementations must be enclosed within the [`machine_description`] macro, which processes them to enable
89/// fast and efficient formal verification.
90///
91/// The behaviour of machine-check is controlled by command-line arguments.
92pub use ::machine_check_exec::run;
93
94/// Parses arguments to run **machine-check** with custom clap arguments augmenting the ones used to run
95/// **machine-check**.
96pub use ::machine_check_exec::parse_args;
97
98pub use ::machine_check_common::ExecError;
99pub use ::machine_check_common::ExecResult;
100pub use ::machine_check_common::ExecStats;
101pub use ::machine_check_exec::ExecArgs;
102
103/// Runs **machine-check** with the given constructed system and parsed arguments.
104///
105/// Parsed arguments are used to run **machine-check**. Otherwise, this method behaves the same as [`run`].
106pub use ::machine_check_exec::execute;
107
108#[doc(hidden)]
109pub mod mck {
110    pub use mck::*;
111}
machine_check/lib.rs

machine_check/
lib.rs
