1 /// A higher-level annotation IR that does not specify bitvector widths.
2 /// This allows annotations to be generic over possible types, which
3 /// corresponds to how ISLE rewrites are written.
4 use std::fmt;
5 /// A bound variable, including the VIR type
6 #[derive(Clone, Debug, PartialEq, Eq)]
7 pub struct BoundVar {
8     pub name: String,
9     pub ty: Option<Type>,
10 }
11 
12 impl BoundVar {
13     /// Construct a new bound variable
new_with_ty(name: &str, ty: &Type) -> Self14     pub fn new_with_ty(name: &str, ty: &Type) -> Self {
15         BoundVar {
16             name: name.to_string(),
17             ty: Some(ty.clone()),
18         }
19     }
20 
21     /// Construct a new bound variable, cloning from references
new(name: &str) -> Self22     pub fn new(name: &str) -> Self {
23         BoundVar {
24             name: name.to_string(),
25             ty: None,
26         }
27     }
28 
29     /// An expression with the bound variable's name
as_expr(&self) -> Expr30     pub fn as_expr(&self) -> Expr {
31         Expr::Var(self.name.clone())
32     }
33 }
34 
35 /// A function signature annotation, including the bound variable names for all
36 /// arguments and the return value.
37 #[derive(Clone, Debug, PartialEq, Eq)]
38 pub struct TermSignature {
39     pub args: Vec<BoundVar>,
40     pub ret: BoundVar,
41 }
42 
43 /// Verification IR annotations for an ISLE term consist of the function
44 /// signature and a list of assertions.
45 #[derive(Clone, Debug, PartialEq, Eq)]
46 pub struct TermAnnotation {
47     pub sig: TermSignature,
48     // Note: extra Box for now for ease of parsing
49     #[allow(clippy::vec_box)]
50     pub assumptions: Vec<Box<Expr>>,
51 
52     #[allow(clippy::vec_box)]
53     pub assertions: Vec<Box<Expr>>,
54 }
55 
56 impl TermAnnotation {
57     /// New annotation
new(sig: TermSignature, assumptions: Vec<Expr>, assertions: Vec<Expr>) -> Self58     pub fn new(sig: TermSignature, assumptions: Vec<Expr>, assertions: Vec<Expr>) -> Self {
59         TermAnnotation {
60             sig,
61             assumptions: assumptions.iter().map(|x| Box::new(x.clone())).collect(),
62             assertions: assertions.iter().map(|x| Box::new(x.clone())).collect(),
63         }
64     }
65 
sig(&self) -> &TermSignature66     pub fn sig(&self) -> &TermSignature {
67         &self.sig
68     }
69 
assertions(&self) -> Vec<Expr>70     pub fn assertions(&self) -> Vec<Expr> {
71         self.assumptions.iter().map(|x| *x.clone()).collect()
72     }
73 }
74 
75 /// Higher-level type, not including bitwidths.
76 #[derive(Clone, Debug, Hash, PartialEq, Eq)]
77 pub enum Type {
78     /// Internal type used solely for type inference
79     Poly(u32),
80 
81     /// The expression is a bitvector, currently modeled in the
82     /// logic QF_BV <https://SMT-LIB.cs.uiowa.edu/version1/logics/QF_BV.smt>
83     /// This corresponds to Cranelift's Isle type:
84     /// (type Value (primitive Value))
85     BitVector,
86 
87     /// Use if the width is known
88     BitVectorWithWidth(usize),
89 
90     // Use if the width is unknown after inference, indexed by a
91     // canonical type variable
92     BitVectorUnknown(u32),
93 
94     /// The expression is an integer (currently used for ISLE type,
95     /// representing bitwidth)
96     Int,
97 
98     /// The expression is a boolean.
99     Bool,
100 
101     /// Unit, removed before SMT-Lib
102     Unit,
103 }
104 
105 impl fmt::Display for Type {
fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result106     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
107         match self {
108             Type::Poly(_) => write!(f, "poly"),
109             Type::BitVector => write!(f, "bv"),
110             Type::BitVectorWithWidth(w) => write!(f, "bv{}", *w),
111             Type::BitVectorUnknown(_) => write!(f, "bv"),
112             Type::Int => write!(f, "Int"),
113             Type::Bool => write!(f, "Bool"),
114             Type::Unit => write!(f, "Unit"),
115         }
116     }
117 }
118 
119 impl Type {
is_poly(&self) -> bool120     pub fn is_poly(&self) -> bool {
121         matches!(self, Type::Poly(_))
122     }
123 }
124 
125 /// Type-specified constants
126 #[derive(Clone, Debug, PartialEq, Eq)]
127 pub struct Const {
128     pub ty: Type,
129     pub value: i128,
130     pub width: usize,
131 }
132 
133 /// Width arguments
134 #[derive(Clone, Debug, PartialEq, Eq)]
135 pub enum Width {
136     Const(usize),
137     RegWidth,
138 }
139 
140 /// Typed expressions (u32 is the type var)
141 #[derive(Clone, Debug, PartialEq, Eq)]
142 pub enum Expr {
143     // Terminal nodes
144     Var(String),
145     Const(Const),
146     True,
147     False,
148 
149     // Get the width of a bitvector
150     WidthOf(Box<Expr>),
151 
152     // Boolean operations
153     Not(Box<Expr>),
154     And(Box<Expr>, Box<Expr>),
155     Or(Box<Expr>, Box<Expr>),
156     Imp(Box<Expr>, Box<Expr>),
157     Eq(Box<Expr>, Box<Expr>),
158     Lte(Box<Expr>, Box<Expr>),
159     Lt(Box<Expr>, Box<Expr>),
160 
161     BVSgt(Box<Expr>, Box<Expr>),
162     BVSgte(Box<Expr>, Box<Expr>),
163     BVSlt(Box<Expr>, Box<Expr>),
164     BVSlte(Box<Expr>, Box<Expr>),
165     BVUgt(Box<Expr>, Box<Expr>),
166     BVUgte(Box<Expr>, Box<Expr>),
167     BVUlt(Box<Expr>, Box<Expr>),
168     BVUlte(Box<Expr>, Box<Expr>),
169 
170     BVSaddo(Box<Expr>, Box<Expr>),
171 
172     // Bitvector operations
173     //      Note: these follow the naming conventions of the SMT theory of bitvectors:
174     //      https://SMT-LIB.cs.uiowa.edu/version1/logics/QF_BV.smt
175     // Unary operators
176     BVNeg(Box<Expr>),
177     BVNot(Box<Expr>),
178     CLZ(Box<Expr>),
179     CLS(Box<Expr>),
180     Rev(Box<Expr>),
181     BVPopcnt(Box<Expr>),
182 
183     // Binary operators
184     BVMul(Box<Expr>, Box<Expr>),
185     BVUDiv(Box<Expr>, Box<Expr>),
186     BVSDiv(Box<Expr>, Box<Expr>),
187     BVAdd(Box<Expr>, Box<Expr>),
188     BVSub(Box<Expr>, Box<Expr>),
189     BVUrem(Box<Expr>, Box<Expr>),
190     BVSrem(Box<Expr>, Box<Expr>),
191     BVAnd(Box<Expr>, Box<Expr>),
192     BVOr(Box<Expr>, Box<Expr>),
193     BVXor(Box<Expr>, Box<Expr>),
194     BVRotl(Box<Expr>, Box<Expr>),
195     BVRotr(Box<Expr>, Box<Expr>),
196     BVShl(Box<Expr>, Box<Expr>),
197     BVShr(Box<Expr>, Box<Expr>),
198     BVAShr(Box<Expr>, Box<Expr>),
199 
200     // Includes type
201     BVSubs(Box<Expr>, Box<Expr>, Box<Expr>),
202 
203     // Conversions
204     // Zero extend, static and dynamic width
205     BVZeroExtTo(Box<Width>, Box<Expr>),
206     BVZeroExtToVarWidth(Box<Expr>, Box<Expr>),
207 
208     // Sign extend, static and dynamic width
209     BVSignExtTo(Box<Width>, Box<Expr>),
210     BVSignExtToVarWidth(Box<Expr>, Box<Expr>),
211 
212     // Extract specified bits
213     BVExtract(usize, usize, Box<Expr>),
214 
215     // Concat two bitvectors
216     BVConcat(Vec<Expr>),
217 
218     // Convert integer to bitvector
219     BVIntToBv(usize, Box<Expr>),
220 
221     // Convert bitvector to integer
222     BVToInt(Box<Expr>),
223 
224     // Conversion to wider/narrower bits, without an explicit extend
225     // Allow the destination width to be symbolic.
226     BVConvTo(Box<Expr>, Box<Expr>),
227 
228     // Conditional if-then-else
229     Conditional(Box<Expr>, Box<Expr>, Box<Expr>),
230 
231     // Switch
232     Switch(Box<Expr>, Vec<(Expr, Expr)>),
233 
234     LoadEffect(Box<Expr>, Box<Expr>, Box<Expr>),
235 
236     StoreEffect(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>),
237 }
238 
239 impl Expr {
var(s: &str) -> Expr240     pub fn var(s: &str) -> Expr {
241         Expr::Var(s.to_string())
242     }
243 
unary<F: Fn(Box<Expr>) -> Expr>(f: F, x: Expr) -> Expr244     pub fn unary<F: Fn(Box<Expr>) -> Expr>(f: F, x: Expr) -> Expr {
245         f(Box::new(x))
246     }
247 
binary<F: Fn(Box<Expr>, Box<Expr>) -> Expr>(f: F, x: Expr, y: Expr) -> Expr248     pub fn binary<F: Fn(Box<Expr>, Box<Expr>) -> Expr>(f: F, x: Expr, y: Expr) -> Expr {
249         f(Box::new(x), Box::new(y))
250     }
251 }
252