machine_check_common/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use std::collections::HashMap;
4
5use proc_macro2::TokenStream;
6use serde::{Deserialize, Serialize};
7use thiserror::Error;
8
9pub mod check;
10pub mod iir;
11pub mod ir_common;
12
13mod node_id;
14
15pub use mck::{KnownParamValuation, ParamValuation, ThreeValued};
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 constructed.
52    #[error("property '{0}' could not be constructed: {1}")]
53    PropertyNotConstructible(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/// Type of function that computes a property macro result.
119///
120/// The function is called with a reference to custom input data
121/// and the token stream it is called with. It should return a token stream
122/// it will be replaced with or alternatively an error.
123///
124/// For example, a macro with name `example` can be called within properties
125/// as `example!(example_data)`. The input token stream will then contain `example_data`.
126/// The macro can then return `example_result` and will be replaced by this result
127/// before further processing. Alternatively, it can return an error, which will result
128/// in property verification failure.
129pub type PropertyMacroFn<D> = fn(&D, TokenStream) -> Result<TokenStream, anyhow::Error>;
130
131#[doc(hidden)]
132pub struct PropertyMacros<D> {
133    pub macros: HashMap<String, PropertyMacroFn<D>>,
134    pub data: D,
135}
136
137#[doc(hidden)]
138impl PropertyMacros<()> {
139    pub fn empty() -> Self {
140        Self {
141            macros: HashMap::new(),
142            data: (),
143        }
144    }
145}
machine_check_common/lib.rs

machine_check_common/
lib.rs
