machine_check_common/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use serde::{Deserialize, Serialize};
4use thiserror::Error;
5
6pub mod check;
7pub mod property;
8
9mod node_id;
10mod value;
11
12pub use value::{param_valuation::ParamValuation, three_valued::ThreeValued};
13
14pub use node_id::{NodeId, StateId};
15
16use crate::check::KnownConclusion;
17
18/// Execution error that occured during **machine-check** execution.
19#[derive(Error, Debug, Serialize, Deserialize, Clone)]
20#[non_exhaustive]
21pub enum ExecError {
22    /// The verification result could not be obtained as the abstraction is too coarse.
23    ///  
24    /// Currently, this should never happen, as only three-valued abstraction is supported.
25    #[error("incomplete verification")]
26    Incomplete,
27    /// The specified property field was not found in the system.
28    #[error("field '{0}' not found")]
29    FieldNotFound(String),
30    /// The used index was invalid.
31    ///
32    /// This can happen either due to the field not being indexable
33    /// or the index being too high.
34    #[error("index {0} is invalid for the field '{1}'")]
35    IndexInvalid(u64, String),
36    /// The use of an index is required to use the field in an operation.
37    ///
38    /// This happens because an array type was used where a bit-vector type
39    /// was expected.
40    #[error("indexing is required for the field '{0}'")]
41    IndexRequired(String),
42    /// The signedness of the field was required for a comparison, but not estabilished.
43    ///
44    /// Currently, if needed, the signedness must be forced by `as_unsigned` or `as_signed`,
45    /// as field signedness currently does not yet propagate to property verification.
46    #[error("signedness of the use of field '{0}' was not estabilished")]
47    SignednessNotEstabilished(String),
48    /// The specified property is invalid and could not be lexed into tokens.
49    #[error("property '{0}' could not be lexed: {1}")]
50    PropertyNotLexable(String, String),
51    /// The specified property is invalid and could not be parsed.
52    #[error("property '{0}' could not be parsed: {1}")]
53    PropertyNotParseable(String, String),
54    /// Verification of a standard property was requested, but the inherent property does not hold.
55    #[error("inherent panic")]
56    InherentPanic,
57    /// Verification of a standard property was requested, but the inherent property is dependent on parameters.
58    #[error("inherent panic possible depending on parameters")]
59    InherentPanicDependent,
60    /// Verification of a mu-calculus property encountered a non-monotone change.
61    ///
62    /// This is prohibited as it can lead to infinite verification loops.
63    #[error("non-monotone property")]
64    NonMonotoneProperty,
65    /// It was requested to verify an inherent property while assuming that it holds.
66    #[error("cannot verify inherent property while assuming it")]
67    VerifiedInherentAssumed,
68    /// The Graphical User Interface emitted an error.
69    #[error("GUI error: {0}")]
70    GuiError(String),
71    /// No verification was requested, so there is no verification result.
72    #[error("no result")]
73    NoResult,
74    /// Other error.
75    #[error("{0}")]
76    OtherError(String),
77}
78
79/// Execution result of **machine-check**.
80#[derive(Debug, Serialize, Deserialize, Clone)]
81pub struct ExecResult {
82    /// The verification result.
83    ///
84    /// A non-error result says whether the property holds or not.
85    pub result: Result<KnownConclusion, ExecError>,
86    /// Execution statistics.
87    pub stats: ExecStats,
88}
89
90/// Execution statistics.
91#[derive(Debug, Serialize, Deserialize, Clone, Default)]
92pub struct ExecStats {
93    /// Total number of refinements performed.
94    pub num_refinements: usize,
95    /// Total number of generated states.
96    pub num_generated_states: usize,
97    /// Number of states currently in the state space.
98    pub num_final_states: usize,
99    /// Total number of generated transitions.
100    pub num_generated_transitions: usize,
101    /// Number of transitions currently in the state space.
102    pub num_final_transitions: usize,
103    /// If present, the message of the panic causes inherent property violation.
104    pub inherent_panic_message: Option<String>,
105}
106
107/// Signedness of a bit-vector type.
108///
109/// In **machine-check**, bit-vectors can have no signedness,
110/// as the interpretation of its value may completely depend on the operation performed.
111#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
112pub enum Signedness {
113    None,
114    Unsigned,
115    Signed,
116}
117
118/// Number of the message that signifies no panic.
119///
120/// This is only an implementation detail and should be removed later.
121pub const PANIC_NUM_NO_PANIC: u64 = 0;
122
123/// Number of the message that signifies a panic due to a division by zero.
124///
125/// This is only an implementation detail and should be removed later.
126pub const PANIC_NUM_DIV_BY_ZERO: u64 = 1;
127
128/// Message that signifies a panic due to a division by zero.
129///
130/// This is only an implementation detail and should be removed later.
131pub const PANIC_MSG_DIV_BY_ZERO: &str = "attempt to divide by zero";
132
133/// Number of the message that signifies a panic due to a division by zero
134/// when computing the remainder.
135///
136/// This is only an implementation detail and should be removed later.
137pub const PANIC_NUM_REM_BY_ZERO: u64 = 2;
138
139/// Message that signifies a panic due to a division by zero when computing the remainder.
140///
141/// This is only an implementation detail and should be removed later.
142pub const PANIC_MSG_REM_BY_ZERO: &str = "attempt to calculate the remainder with a divisor of zero";
143
144/// Number of the first custom message that signifies a panic.
145///
146/// This is only an implementation detail and should be removed later.
147pub const PANIC_NUM_FIRST_CUSTOM: u64 = 3;
machine_check_common/lib.rs

machine_check_common/
lib.rs
