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

machine_check_common/
lib.rs
