machine-check-common 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

use serde::{Deserialize, Serialize};

#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum IrReference {
    Immutable,
    None,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub struct IrTypeArray {
    pub index_width: u32,
    pub element_width: u32,
}

#[derive(
    Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, strum::EnumString, strum::Display,
)]
pub enum IrMckUnaryOp {
    #[strum(to_string = "::mck::forward::Bitwise::bit_not")]
    Not,
    #[strum(to_string = "::std::ops::Neg::neg")]
    Neg,
}

#[derive(
    Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, strum::EnumString, strum::Display,
)]
pub enum IrMckBinaryOp {
    // bitwise
    #[strum(to_string = "::mck::forward::Bitwise::bit_and")]
    BitAnd,
    #[strum(to_string = "::mck::forward::Bitwise::bit_or")]
    BitOr,
    #[strum(to_string = "::mck::forward::Bitwise::bit_xor")]
    BitXor,
    // shifts
    #[strum(to_string = "::mck::forward::HwShift::logic_shl")]
    LogicShl,
    #[strum(to_string = "::mck::forward::HwShift::logic_shr")]
    LogicShr,
    #[strum(to_string = "::mck::forward::HwShift::arith_shr")]
    ArithShr,
    // arithmetic
    #[strum(to_string = "::mck::forward::HwArith::add")]
    Add,
    #[strum(to_string = "::mck::forward::HwArith::sub")]
    Sub,
    #[strum(to_string = "::mck::forward::HwArith::mul")]
    Mul,
    #[strum(to_string = "::mck::forward::HwArith::udiv")]
    Udiv,
    #[strum(to_string = "::mck::forward::HwArith::urem")]
    Urem,
    #[strum(to_string = "::mck::forward::HwArith::sdiv")]
    Sdiv,
    #[strum(to_string = "::mck::forward::HwArith::srem")]
    Srem,
    // equality
    #[strum(to_string = "::mck::forward::TypedEq::eq")]
    Eq,
    #[strum(to_string = "::mck::forward::TypedEq::ne")]
    Ne,
    // comparison
    #[strum(to_string = "::mck::forward::TypedCmp::ult")]
    Ult,
    #[strum(to_string = "::mck::forward::TypedCmp::ule")]
    Ule,
    #[strum(to_string = "::mck::forward::TypedCmp::slt")]
    Slt,
    #[strum(to_string = "::mck::forward::TypedCmp::sle")]
    Sle,
}

#[derive(Clone, Debug, Hash, strum::EnumString, strum::Display)]
pub enum IrStdUnaryOp {
    #[strum(to_string = "::std::ops::Not::not")]
    Not,
    #[strum(to_string = "::std::ops::Neg::neg")]
    Neg,
}

#[derive(Clone, Debug, Hash, strum::EnumString, strum::Display)]
pub enum IrStdBinaryOp {
    // bitwise
    #[strum(to_string = "::std::ops::BitAnd::bitand")]
    BitAnd,
    #[strum(to_string = "::std::ops::BitOr::bitor")]
    BitOr,
    #[strum(to_string = "::std::ops::BitXor::bitxor")]
    BitXor,
    // shifts
    #[strum(to_string = "::std::ops::Shl::shl")]
    Shl,
    #[strum(to_string = "::std::ops::Shr::shr")]
    Shr,
    // arithmetic
    #[strum(to_string = "::std::ops::Add::add")]
    Add,
    #[strum(to_string = "::std::ops::Sub::sub")]
    Sub,
    #[strum(to_string = "::std::ops::Mul::mul")]
    Mul,
    #[strum(to_string = "::std::ops::Div::div")]
    Div,
    #[strum(to_string = "::std::ops::Rem::rem")]
    Rem,
    // equality
    #[strum(to_string = "::std::cmp::PartialEq::eq")]
    Eq,
    #[strum(to_string = "::std::cmp::PartialEq::ne")]
    Ne,
    // comparison
    #[strum(to_string = "::std::cmp::PartialOrd::lt")]
    Lt,
    #[strum(to_string = "::std::cmp::PartialOrd::le")]
    Le,
    #[strum(to_string = "::std::cmp::PartialOrd::gt")]
    Gt,
    #[strum(to_string = "::std::cmp::PartialOrd::ge")]
    Ge,
}