btor2rs 0.1.0

Safe-Rust Btor2 parser
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163

//! Btor2 operation nodes.
//!
//! Although the operations are normal nodes in a sense,
//! they are in a separate module for clarity.

use crate::id::{Rnid, Sid};

/// Unary operation type.
#[derive(Debug, Clone, strum::EnumString, strum::Display)]
#[strum(serialize_all = "lowercase")]
pub enum UniOpType {
    Not,
    Inc,
    Dec,
    Neg,
    Redand,
    Redor,
    Redxor,
}

/// Unary operation node.
#[derive(Debug, Clone)]
pub struct UniOp {
    /// Result sort.
    pub sid: Sid,
    /// Type of operation.
    pub ty: UniOpType,
    /// Operand right-side node id.
    pub a: Rnid,
}

/// Binary operation type.
#[derive(Debug, Clone, strum::EnumString, strum::Display)]
#[strum(serialize_all = "lowercase")]
pub enum BiOpType {
    // Boolean
    Iff,
    Implies,
    // (dis)equality
    Eq,
    Neq,
    // (un)signed equality
    Sgt,
    Ugt,
    Sgte,
    Ugte,
    Slt,
    Ult,
    Slte,
    Ulte,
    // bitwise
    And,
    Nand,
    Nor,
    Or,
    Xnor,
    Xor,
    // rotate
    Rol,
    Ror,
    // shift
    Sll,
    Sra,
    Srl,
    // arithmetic
    Add,
    Mul,
    Sdiv,
    Udiv,
    Smod,
    Srem,
    Urem,
    Sub,
    // overflow
    Saddo,
    Uaddo,
    Sdivo,
    Udivo,
    Smulo,
    Umulo,
    Ssubo,
    Usubo,
    // concatenation
    Concat,
    // array read
    Read,
}

/// Binary operation node.
#[derive(Debug, Clone)]
pub struct BiOp {
    /// Result sort.
    pub sid: Sid,
    /// Operation type.
    pub ty: BiOpType,
    /// First operand right-side node id.
    pub a: Rnid,
    /// Second operand right-side node id.
    pub b: Rnid,
}

/// Ternary operation type.
#[derive(Debug, Clone, strum::EnumString, strum::Display)]
#[strum(serialize_all = "lowercase")]
pub enum TriOpType {
    // if-then-else
    Ite,
    // array write
    Write,
}

/// Ternary operation node.
#[derive(Debug, Clone)]
pub struct TriOp {
    /// Result sort.
    pub sid: Sid,
    /// Operation type.
    pub ty: TriOpType,
    /// First operand right-side node id.
    pub a: Rnid,
    /// Second operand right-side node id.
    pub b: Rnid,
    /// Third operand right-side node id.
    pub c: Rnid,
}

/// Extension operation type.
#[derive(Debug, Clone, strum::EnumString, strum::Display)]
#[strum(serialize_all = "lowercase")]
pub enum ExtOpType {
    Sext,
    Uext,
}

/// Extension operation node.
#[derive(Debug, Clone)]
pub struct ExtOp {
    /// Result sort.
    pub sid: Sid,
    /// Operation type.
    pub ty: ExtOpType,
    /// Operand right-side node id.
    pub a: Rnid,
    /// Length of extension.
    pub length: u32,
}

/// Slice operation node.
#[derive(Debug, Clone)]
pub struct SliceOp {
    /// Result sort.
    pub sid: Sid,
    /// Operand right-side node id.
    pub a: Rnid,
    /// Upper bit of slice (inclusive).
    ///
    /// Guaranteed to be greater or equal to lower bit after parsing.
    pub upper_bit: u32,
    /// Lower bit of slice (inclusive).
    ///
    /// Guaranteed to be lesser or equal to upper bit after parsing.
    pub lower_bit: u32,
}