machine_check_common/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use serde::{Deserialize, Serialize};
4use std::{fmt::Display, ops::Not};
5use thiserror::Error;
6
7pub mod check;
8mod node_id;
9pub mod property;
10
11pub use node_id::{NodeId, StateId};
12
13/// Execution error that occured during **machine-check** execution.
14#[derive(Error, Debug, Serialize, Deserialize, Clone)]
15#[non_exhaustive]
16pub enum ExecError {
17    /// The verification result could not be obtained as the abstraction is too coarse.
18    ///  
19    /// Currently, this should never happen, as only three-valued abstraction is supported.
20    #[error("incomplete verification")]
21    Incomplete,
22    /// The specified property field was not found in the system.
23    #[error("field '{0}' not found")]
24    FieldNotFound(String),
25    /// The used index was invalid.
26    ///
27    /// This can happen either due to the field not being indexable
28    /// or the index being too high.
29    #[error("index {0} is invalid for the field '{1}'")]
30    IndexInvalid(u64, String),
31    /// The use of an index is required to use the field in an operation.
32    ///
33    /// This happens because an array type was used where a bit-vector type
34    /// was expected.
35    #[error("indexing is required for the field '{0}'")]
36    IndexRequired(String),
37    /// The signedness of the field was required for a comparison, but not estabilished.
38    ///
39    /// Currently, if needed, the signedness must be forced by `as_unsigned` or `as_signed`,
40    /// as field signedness currently does not yet propagate to property verification.
41    #[error("signedness of the use of field '{0}' was not estabilished")]
42    SignednessNotEstabilished(String),
43    /// The specified property is invalid and could not be lexed into tokens.
44    #[error("property '{0}' could not be lexed: {1}")]
45    PropertyNotLexable(String, String),
46    /// The specified property is invalid and could not be parsed.
47    #[error("property '{0}' could not be parsed: {1}")]
48    PropertyNotParseable(String, String),
49    /// Verification of a standard property was requested, but the inherent property does not hold.
50    #[error("inherent panic")]
51    InherentPanic,
52    /// It was requested to verify an inherent property while assuming that it holds.
53    #[error("cannot verify inherent property while assuming it")]
54    VerifiedInherentAssumed,
55    /// The Graphical User Interface emitted an error.
56    #[error("GUI error: {0}")]
57    GuiError(String),
58    /// No verification was requested, so there is no verification result.
59    #[error("no result")]
60    NoResult,
61    /// Other error.
62    #[error("{0}")]
63    OtherError(String),
64}
65
66/// Execution result of **machine-check**.
67#[derive(Debug, Serialize, Deserialize, Clone)]
68pub struct ExecResult {
69    /// The verification result.
70    ///
71    /// A non-error result says whether the property holds or not.
72    pub result: Result<bool, ExecError>,
73    /// Execution statistics.
74    pub stats: ExecStats,
75}
76
77/// Execution statistics.
78#[derive(Debug, Serialize, Deserialize, Clone, Default)]
79pub struct ExecStats {
80    /// Total number of refinements performed.
81    pub num_refinements: usize,
82    /// Total number of generated states.
83    pub num_generated_states: usize,
84    /// Number of states currently in the state space.
85    pub num_final_states: usize,
86    /// Total number of generated transitions.
87    pub num_generated_transitions: usize,
88    /// Number of transitions currently in the state space.
89    pub num_final_transitions: usize,
90    /// If present, the message of the panic causes inherent property violation.
91    pub inherent_panic_message: Option<String>,
92}
93
94/// An extension of a Boolean to three-valued logic.
95#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
96pub enum ThreeValued {
97    // Known false.
98    False,
99    // Known true.
100    True,
101    // Either false or true, but it is unknown which one.
102    Unknown,
103}
104
105impl ThreeValued {
106    /// Whether the value is unknown, i.e. neither false nor true.
107    pub fn is_unknown(&self) -> bool {
108        matches!(self, ThreeValued::Unknown)
109    }
110
111    /// Whether the value is known, i.e. false or true.
112    pub fn is_known(&self) -> bool {
113        !self.is_unknown()
114    }
115
116    /// Whether the value is definitely false.
117    pub fn is_false(&self) -> bool {
118        matches!(self, ThreeValued::False)
119    }
120
121    /// Whether the value is definitely true.
122    pub fn is_true(&self) -> bool {
123        matches!(self, ThreeValued::True)
124    }
125}
126
127impl Not for ThreeValued {
128    type Output = Self;
129
130    fn not(self) -> Self {
131        match self {
132            ThreeValued::False => ThreeValued::True,
133            ThreeValued::True => ThreeValued::False,
134            ThreeValued::Unknown => ThreeValued::Unknown,
135        }
136    }
137}
138
139impl Display for ThreeValued {
140    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
141        let str = match self {
142            ThreeValued::False => "false",
143            ThreeValued::True => "true",
144            ThreeValued::Unknown => "unknown",
145        };
146        write!(f, "{}", str)
147    }
148}
149
150/// Signedness of a bit-vector type.
151///
152/// In **machine-check**, bit-vectors can have no signedness,
153/// as the interpretation of its value may completely depend on the operation performed.
154#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
155pub enum Signedness {
156    None,
157    Unsigned,
158    Signed,
159}
machine_check_common/lib.rs

machine_check_common/
lib.rs
