machine_check_common/property/
atomic.rs

1use std::fmt::Display;
2
3use serde::{Deserialize, Serialize};
4
5use crate::Signedness;
6
7/// A field name, potentially with indexing and forced signedness.
8#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
9pub struct ValueExpression {
10    pub(crate) name: String,
11    pub(crate) index: Option<u64>,
12    pub(crate) forced_signedness: Signedness,
13}
14
15impl ValueExpression {
16    pub fn name(&self) -> &str {
17        &self.name
18    }
19
20    pub fn index(&self) -> Option<u64> {
21        self.index
22    }
23
24    pub fn forced_signedness(&self) -> Signedness {
25        self.forced_signedness
26    }
27}
28
29/// An atomic property of Computation Tree Logic.
30///
31/// In our case, this is usually a field compared to a number.
32#[derive(Clone, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
33pub struct AtomicProperty {
34    pub(crate) left: ValueExpression,
35    pub(crate) comparison_type: ComparisonType,
36    pub(crate) right_number: i64,
37}
38
39impl AtomicProperty {
40    pub fn new(
41        left: ValueExpression,
42        comparison_type: ComparisonType,
43        right_number: i64,
44    ) -> AtomicProperty {
45        AtomicProperty {
46            left,
47            comparison_type,
48            right_number,
49        }
50    }
51
52    pub fn left(&self) -> &ValueExpression {
53        &self.left
54    }
55
56    pub fn comparison_type(&self) -> &ComparisonType {
57        &self.comparison_type
58    }
59
60    pub fn right_number_unsigned(&self) -> u64 {
61        self.right_number as u64
62    }
63
64    pub fn right_number_signed(&self) -> i64 {
65        self.right_number
66    }
67}
68
69/// A type of comparison.
70#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, Serialize, Deserialize)]
71pub enum ComparisonType {
72    Eq,
73    Ne,
74    Lt,
75    Le,
76    Gt,
77    Ge,
78}
79
80impl Display for AtomicProperty {
81    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
82        write!(
83            f,
84            "{} {} {}",
85            self.left, self.comparison_type, self.right_number
86        )
87    }
88}
89
90impl Display for ValueExpression {
91    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
92        let add_closing_parenthesis = match self.forced_signedness {
93            Signedness::Unsigned => {
94                write!(f, "as_unsigned(")?;
95                true
96            }
97            Signedness::Signed => {
98                write!(f, "as_signed(")?;
99                true
100            }
101            Signedness::None => false,
102        };
103
104        write!(f, "{}", self.name)?;
105
106        if let Some(index) = self.index {
107            write!(f, "[{}]", index)?;
108        }
109        if add_closing_parenthesis {
110            write!(f, ")")?;
111        }
112        Ok(())
113    }
114}
115
116impl Display for ComparisonType {
117    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
118        let str = match self {
119            ComparisonType::Eq => "==",
120            ComparisonType::Ne => "!=",
121            ComparisonType::Lt => "<",
122            ComparisonType::Le => "<=",
123            ComparisonType::Gt => ">",
124            ComparisonType::Ge => ">=",
125        };
126
127        write!(f, "{}", str)
128    }
129}
machine_check_common/property/atomic.rs

machine_check_common/property/
atomic.rs
