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 iir;
8pub mod ir_common;
9
10mod node_id;
11
12pub use mck::{KnownParamValuation, ParamValuation, 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 constructed.
49    #[error("property '{0}' could not be constructed: {1}")]
50    PropertyNotConstructible(String, String),
51    /// Verification of a standard property was requested, but the inherent property does not hold.
52    #[error("inherent panic")]
53    InherentPanic,
54    /// Verification of a standard property was requested, but the inherent property is dependent on parameters.
55    #[error("inherent panic possible depending on parameters")]
56    InherentPanicDependent,
57    /// Verification of a mu-calculus property encountered a non-monotone change.
58    ///
59    /// This is prohibited as it can lead to infinite verification loops.
60    #[error("non-monotone property")]
61    NonMonotoneProperty,
62    /// It was requested to verify an inherent property while assuming that it holds.
63    #[error("cannot verify inherent property while assuming it")]
64    VerifiedInherentAssumed,
65    /// The Graphical User Interface emitted an error.
66    #[error("GUI error: {0}")]
67    GuiError(String),
68    /// No verification was requested, so there is no verification result.
69    #[error("no result")]
70    NoResult,
71    /// Other error.
72    #[error("{0}")]
73    OtherError(String),
74}
75
76/// Execution result of **machine-check**.
77#[derive(Debug, Serialize, Deserialize, Clone)]
78pub struct ExecResult {
79    /// The verification result.
80    ///
81    /// A non-error result says whether the property holds or not.
82    pub result: Result<KnownConclusion, ExecError>,
83    /// Execution statistics.
84    pub stats: ExecStats,
85}
86
87/// Execution statistics.
88#[derive(Debug, Serialize, Deserialize, Clone, Default)]
89pub struct ExecStats {
90    /// Total number of refinements performed.
91    pub num_refinements: usize,
92    /// Total number of generated states.
93    pub num_generated_states: usize,
94    /// Number of states currently in the state space.
95    pub num_final_states: usize,
96    /// Total number of generated transitions.
97    pub num_generated_transitions: usize,
98    /// Number of transitions currently in the state space.
99    pub num_final_transitions: usize,
100    /// If present, the message of the panic causes inherent property violation.
101    pub inherent_panic_message: Option<String>,
102}
103
104/// Signedness of a bit-vector type.
105///
106/// In **machine-check**, bit-vectors can have no signedness,
107/// as the interpretation of its value may completely depend on the operation performed.
108#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
109pub enum Signedness {
110    None,
111    Unsigned,
112    Signed,
113}
machine_check_common/lib.rs

machine_check_common/
lib.rs
