1 use cranelift_isle::ast::{self, Signature};
2 use std::collections::HashMap;
3 use veri_ir::annotation_ir;
4 
5 use cranelift_isle::ast::{Def, Ident, Model, ModelType, SpecExpr, SpecOp};
6 use cranelift_isle::lexer::Pos;
7 use cranelift_isle::sema::{TermEnv, TermId, TypeEnv, TypeId};
8 use veri_ir::annotation_ir::Width;
9 use veri_ir::annotation_ir::{BoundVar, Const, Expr, TermAnnotation, TermSignature, Type};
10 use veri_ir::TermSignature as TermTypeSignature;
11 
12 static RESULT: &str = "result";
13 
14 #[derive(Clone, Debug)]
15 pub struct ParsingEnv<'a> {
16     pub typeenv: &'a TypeEnv,
17     pub enums: HashMap<String, Expr>,
18 }
19 
20 #[derive(Clone, Debug)]
21 pub struct AnnotationEnv {
22     pub annotation_map: HashMap<TermId, TermAnnotation>,
23 
24     // Mapping from ISLE term to its signature instantiations.
25     pub instantiations_map: HashMap<TermId, Vec<TermTypeSignature>>,
26 
27     // Mapping from ISLE type to its model (the annotation used to represent
28     // it).
29     pub model_map: HashMap<TypeId, annotation_ir::Type>,
30 }
31 
32 impl AnnotationEnv {
get_annotation_for_term(&self, term_id: &TermId) -> Option<TermAnnotation>33     pub fn get_annotation_for_term(&self, term_id: &TermId) -> Option<TermAnnotation> {
34         if self.annotation_map.contains_key(term_id) {
35             return Some(self.annotation_map[term_id].clone());
36         }
37         None
38     }
39 
get_term_signatures_by_name( &self, termenv: &TermEnv, typeenv: &TypeEnv, ) -> HashMap<String, Vec<TermTypeSignature>>40     pub fn get_term_signatures_by_name(
41         &self,
42         termenv: &TermEnv,
43         typeenv: &TypeEnv,
44     ) -> HashMap<String, Vec<TermTypeSignature>> {
45         let mut term_signatures_by_name = HashMap::new();
46         for (term_id, term_sigs) in &self.instantiations_map {
47             let sym = termenv.terms[term_id.index()].name;
48             let name = typeenv.syms[sym.index()].clone();
49             term_signatures_by_name.insert(name, term_sigs.clone());
50         }
51         term_signatures_by_name
52     }
53 }
54 
spec_to_annotation_bound_var(i: &Ident) -> BoundVar55 pub fn spec_to_annotation_bound_var(i: &Ident) -> BoundVar {
56     BoundVar {
57         name: i.0.clone(),
58         ty: None,
59     }
60 }
61 
spec_to_usize(s: &SpecExpr) -> Option<usize>62 fn spec_to_usize(s: &SpecExpr) -> Option<usize> {
63     match s {
64         SpecExpr::ConstInt { val, pos: _ } => Some(*val as usize),
65         _ => None,
66     }
67 }
68 
spec_op_to_expr(s: &SpecOp, args: &[SpecExpr], pos: &Pos, env: &ParsingEnv) -> Expr69 fn spec_op_to_expr(s: &SpecOp, args: &[SpecExpr], pos: &Pos, env: &ParsingEnv) -> Expr {
70     fn unop<F: Fn(Box<Expr>) -> Expr>(
71         u: F,
72         args: &[SpecExpr],
73         pos: &Pos,
74         env: &ParsingEnv,
75     ) -> Expr {
76         assert_eq!(
77             args.len(),
78             1,
79             "Unexpected number of args for unary operator {pos:?}",
80         );
81         u(Box::new(spec_to_expr(&args[0], env)))
82     }
83     fn binop<F: Fn(Box<Expr>, Box<Expr>) -> Expr>(
84         b: F,
85         args: &[SpecExpr],
86         _pos: &Pos,
87         env: &ParsingEnv,
88     ) -> Expr {
89         assert_eq!(
90             args.len(),
91             2,
92             "Unexpected number of args for binary operator {args:?}",
93         );
94         b(
95             Box::new(spec_to_expr(&args[0], env)),
96             Box::new(spec_to_expr(&args[1], env)),
97         )
98     }
99 
100     fn variadic_binop<F: Fn(Box<Expr>, Box<Expr>) -> Expr>(
101         b: F,
102         args: &[SpecExpr],
103         pos: &Pos,
104         env: &ParsingEnv,
105     ) -> Expr {
106         assert!(
107             !args.is_empty(),
108             "Unexpected number of args for variadic binary operator {pos:?}",
109         );
110         let mut expr_args: Vec<Expr> = args.iter().map(|a| spec_to_expr(a, env)).collect();
111         let last = expr_args.remove(expr_args.len() - 1);
112 
113         // Reverse to keep the order of the original list
114         expr_args
115             .iter()
116             .rev()
117             .fold(last, |acc, a| b(Box::new(a.clone()), Box::new(acc)))
118     }
119 
120     match s {
121         // Unary
122         SpecOp::Not => unop(Expr::Not, args, pos, env),
123         SpecOp::BVNot => unop(Expr::BVNot, args, pos, env),
124         SpecOp::BVNeg => unop(Expr::BVNeg, args, pos, env),
125         SpecOp::Rev => unop(Expr::Rev, args, pos, env),
126         SpecOp::Clz => unop(Expr::CLZ, args, pos, env),
127         SpecOp::Cls => unop(Expr::CLS, args, pos, env),
128         SpecOp::Popcnt => unop(Expr::BVPopcnt, args, pos, env),
129         SpecOp::BV2Int => unop(Expr::BVToInt, args, pos, env),
130 
131         // Variadic binops
132         SpecOp::And => variadic_binop(Expr::And, args, pos, env),
133         SpecOp::Or => variadic_binop(Expr::Or, args, pos, env),
134 
135         // Binary
136         SpecOp::Eq => binop(Expr::Eq, args, pos, env),
137         SpecOp::Lt => binop(Expr::Lt, args, pos, env),
138         SpecOp::Lte => binop(Expr::Lte, args, pos, env),
139         SpecOp::Gt => binop(|x, y| Expr::Lt(y, x), args, pos, env),
140         SpecOp::Gte => binop(|x, y| Expr::Lte(y, x), args, pos, env),
141         SpecOp::Imp => binop(Expr::Imp, args, pos, env),
142         SpecOp::BVAnd => binop(Expr::BVAnd, args, pos, env),
143         SpecOp::BVOr => binop(Expr::BVOr, args, pos, env),
144         SpecOp::BVXor => binop(Expr::BVXor, args, pos, env),
145         SpecOp::BVAdd => binop(Expr::BVAdd, args, pos, env),
146         SpecOp::BVSub => binop(Expr::BVSub, args, pos, env),
147         SpecOp::BVMul => binop(Expr::BVMul, args, pos, env),
148         SpecOp::BVUdiv => binop(Expr::BVUDiv, args, pos, env),
149         SpecOp::BVUrem => binop(Expr::BVUrem, args, pos, env),
150         SpecOp::BVSdiv => binop(Expr::BVSDiv, args, pos, env),
151         SpecOp::BVSrem => binop(Expr::BVSrem, args, pos, env),
152         SpecOp::BVShl => binop(Expr::BVShl, args, pos, env),
153         SpecOp::BVLshr => binop(Expr::BVShr, args, pos, env),
154         SpecOp::BVAshr => binop(Expr::BVAShr, args, pos, env),
155         SpecOp::BVSaddo => binop(Expr::BVSaddo, args, pos, env),
156         SpecOp::BVUle => binop(Expr::BVUlte, args, pos, env),
157         SpecOp::BVUlt => binop(Expr::BVUlt, args, pos, env),
158         SpecOp::BVUgt => binop(Expr::BVUgt, args, pos, env),
159         SpecOp::BVUge => binop(Expr::BVUgte, args, pos, env),
160         SpecOp::BVSlt => binop(Expr::BVSlt, args, pos, env),
161         SpecOp::BVSle => binop(Expr::BVSlte, args, pos, env),
162         SpecOp::BVSgt => binop(Expr::BVSgt, args, pos, env),
163         SpecOp::BVSge => binop(Expr::BVSgte, args, pos, env),
164         SpecOp::Rotr => binop(Expr::BVRotr, args, pos, env),
165         SpecOp::Rotl => binop(Expr::BVRotl, args, pos, env),
166         SpecOp::ZeroExt => match spec_to_usize(&args[0]) {
167             Some(i) => Expr::BVZeroExtTo(
168                 Box::new(Width::Const(i)),
169                 Box::new(spec_to_expr(&args[1], env)),
170             ),
171             None => binop(Expr::BVZeroExtToVarWidth, args, pos, env),
172         },
173         SpecOp::SignExt => match spec_to_usize(&args[0]) {
174             Some(i) => Expr::BVSignExtTo(
175                 Box::new(Width::Const(i)),
176                 Box::new(spec_to_expr(&args[1], env)),
177             ),
178             None => binop(Expr::BVSignExtToVarWidth, args, pos, env),
179         },
180         SpecOp::ConvTo => binop(Expr::BVConvTo, args, pos, env),
181         SpecOp::Concat => {
182             let cases: Vec<Expr> = args.iter().map(|a| spec_to_expr(a, env)).collect();
183             Expr::BVConcat(cases)
184         }
185         SpecOp::Extract => {
186             assert_eq!(
187                 args.len(),
188                 3,
189                 "Unexpected number of args for extract operator {pos:?}",
190             );
191             Expr::BVExtract(
192                 spec_to_usize(&args[0]).unwrap(),
193                 spec_to_usize(&args[1]).unwrap(),
194                 Box::new(spec_to_expr(&args[2], env)),
195             )
196         }
197         SpecOp::Int2BV => {
198             assert_eq!(
199                 args.len(),
200                 2,
201                 "Unexpected number of args for Int2BV operator {pos:?}",
202             );
203             Expr::BVIntToBv(
204                 spec_to_usize(&args[0]).unwrap(),
205                 Box::new(spec_to_expr(&args[1], env)),
206             )
207         }
208         SpecOp::Subs => {
209             assert_eq!(
210                 args.len(),
211                 3,
212                 "Unexpected number of args for subs operator {pos:?}",
213             );
214             Expr::BVSubs(
215                 Box::new(spec_to_expr(&args[0], env)),
216                 Box::new(spec_to_expr(&args[1], env)),
217                 Box::new(spec_to_expr(&args[2], env)),
218             )
219         }
220         SpecOp::WidthOf => unop(Expr::WidthOf, args, pos, env),
221         SpecOp::If => {
222             assert_eq!(
223                 args.len(),
224                 3,
225                 "Unexpected number of args for extract operator {pos:?}",
226             );
227             Expr::Conditional(
228                 Box::new(spec_to_expr(&args[0], env)),
229                 Box::new(spec_to_expr(&args[1], env)),
230                 Box::new(spec_to_expr(&args[2], env)),
231             )
232         }
233         SpecOp::Switch => {
234             assert!(
235                 args.len() > 1,
236                 "Unexpected number of args for switch operator {pos:?}",
237             );
238             let switch_on = spec_to_expr(&args[0], env);
239             let arms: Vec<(Expr, Expr)> = args[1..]
240                 .iter()
241                 .map(|a| match a {
242                     SpecExpr::Pair { l, r } => {
243                         let l_expr = spec_to_expr(l, env);
244                         let r_expr = spec_to_expr(r, env);
245                         (l_expr, r_expr)
246                     }
247                     _ => unreachable!(),
248                 })
249                 .collect();
250             Expr::Switch(Box::new(switch_on), arms)
251         }
252         SpecOp::LoadEffect => {
253             assert_eq!(
254                 args.len(),
255                 3,
256                 "Unexpected number of args for load operator {pos:?}",
257             );
258             Expr::LoadEffect(
259                 Box::new(spec_to_expr(&args[0], env)),
260                 Box::new(spec_to_expr(&args[1], env)),
261                 Box::new(spec_to_expr(&args[2], env)),
262             )
263         }
264         SpecOp::StoreEffect => {
265             assert_eq!(
266                 args.len(),
267                 4,
268                 "Unexpected number of args for store operator {pos:?}",
269             );
270             Expr::StoreEffect(
271                 Box::new(spec_to_expr(&args[0], env)),
272                 Box::new(spec_to_expr(&args[1], env)),
273                 Box::new(spec_to_expr(&args[2], env)),
274                 Box::new(spec_to_expr(&args[3], env)),
275             )
276         }
277     }
278 }
279 
spec_to_expr(s: &SpecExpr, env: &ParsingEnv) -> Expr280 fn spec_to_expr(s: &SpecExpr, env: &ParsingEnv) -> Expr {
281     match s {
282         SpecExpr::ConstUnit { pos: _ } => Expr::Const(Const {
283             ty: Type::Unit,
284             value: 0,
285             width: 0,
286         }),
287         SpecExpr::ConstInt { val, pos: _ } => Expr::Const(Const {
288             ty: Type::Int,
289             value: *val,
290             width: 0,
291         }),
292         SpecExpr::ConstBitVec { val, width, pos: _ } => Expr::Const(Const {
293             ty: Type::BitVectorWithWidth(*width as usize),
294             value: *val,
295             width: (*width as usize),
296         }),
297         SpecExpr::ConstBool { val, pos: _ } => Expr::Const(Const {
298             ty: Type::Bool,
299             value: *val as i128,
300             width: 0,
301         }),
302         SpecExpr::Var { var, pos: _ } => Expr::Var(var.0.clone()),
303         SpecExpr::Op { op, args, pos } => spec_op_to_expr(op, args, pos, env),
304         SpecExpr::Pair { l, r } => {
305             unreachable!("pairs currently only parsed as part of Switch statements, {l:?} {r:?}",)
306         }
307         SpecExpr::Enum { name } => {
308             if let Some(e) = env.enums.get(&name.0) {
309                 e.clone()
310             } else {
311                 panic!("Can't find model for enum {}", name.0);
312             }
313         }
314     }
315 }
316 
model_type_to_type(model_type: &ModelType) -> veri_ir::Type317 fn model_type_to_type(model_type: &ModelType) -> veri_ir::Type {
318     match model_type {
319         ModelType::Int => veri_ir::Type::Int,
320         ModelType::Unit => veri_ir::Type::Unit,
321         ModelType::Bool => veri_ir::Type::Bool,
322         ModelType::BitVec(size) => veri_ir::Type::BitVector(*size),
323     }
324 }
325 
signature_to_term_type_signature(sig: &Signature) -> TermTypeSignature326 fn signature_to_term_type_signature(sig: &Signature) -> TermTypeSignature {
327     TermTypeSignature {
328         args: sig.args.iter().map(model_type_to_type).collect(),
329         ret: model_type_to_type(&sig.ret),
330         canonical_type: Some(model_type_to_type(&sig.canonical)),
331     }
332 }
333 
parse_annotations(defs: &[Def], termenv: &TermEnv, typeenv: &TypeEnv) -> AnnotationEnv334 pub fn parse_annotations(defs: &[Def], termenv: &TermEnv, typeenv: &TypeEnv) -> AnnotationEnv {
335     let mut annotation_map = HashMap::new();
336     let mut model_map = HashMap::new();
337 
338     let mut env = ParsingEnv {
339         typeenv,
340         enums: HashMap::new(),
341     };
342 
343     // Traverse models to process spec annotations for enums
344     for def in defs {
345         if let &ast::Def::Model(Model { ref name, ref val }) = def {
346             match val {
347                 ast::ModelValue::TypeValue(model_type) => {
348                     let type_id = typeenv.get_type_by_name(name).unwrap();
349                     let ir_type = match model_type {
350                         ModelType::Int => annotation_ir::Type::Int,
351                         ModelType::Unit => annotation_ir::Type::Unit,
352                         ModelType::Bool => annotation_ir::Type::Bool,
353                         ModelType::BitVec(None) => annotation_ir::Type::BitVector,
354                         ModelType::BitVec(Some(size)) => {
355                             annotation_ir::Type::BitVectorWithWidth(*size)
356                         }
357                     };
358                     model_map.insert(type_id, ir_type);
359                 }
360                 ast::ModelValue::EnumValues(vals) => {
361                     for (v, e) in vals {
362                         let ident = ast::Ident(format!("{}.{}", name.0, v.0), v.1);
363                         let term_id = termenv.get_term_by_name(typeenv, &ident).unwrap();
364                         let val = spec_to_expr(e, &env);
365                         let ty = match val {
366                             Expr::Const(Const { ref ty, .. }) => ty,
367                             _ => unreachable!(),
368                         };
369                         env.enums.insert(ident.0.clone(), val.clone());
370                         let result = BoundVar {
371                             name: RESULT.to_string(),
372                             ty: Some(ty.clone()),
373                         };
374                         let sig = TermSignature {
375                             args: vec![],
376                             ret: result,
377                         };
378                         let annotation = TermAnnotation {
379                             sig,
380                             assumptions: vec![Box::new(Expr::Eq(
381                                 Box::new(Expr::Var(RESULT.to_string())),
382                                 Box::new(val),
383                             ))],
384                             assertions: vec![],
385                         };
386                         annotation_map.insert(term_id, annotation);
387                     }
388                 }
389             }
390         }
391     }
392 
393     // Traverse defs to process spec annotations
394     for def in defs {
395         if let ast::Def::Spec(spec) = def {
396             let termname = spec.term.0.clone();
397             let term_id = termenv
398                 .get_term_by_name(typeenv, &spec.term)
399                 .unwrap_or_else(|| panic!("Spec provided for unknown decl {termname}"));
400             assert!(
401                 !annotation_map.contains_key(&term_id),
402                 "duplicate spec for {termname}",
403             );
404             let sig = TermSignature {
405                 args: spec.args.iter().map(spec_to_annotation_bound_var).collect(),
406                 ret: BoundVar {
407                     name: RESULT.to_string(),
408                     ty: None,
409                 },
410             };
411 
412             let mut assumptions = vec![];
413             let mut assertions = vec![];
414             for a in &spec.provides {
415                 assumptions.push(Box::new(spec_to_expr(a, &env)));
416             }
417 
418             for a in &spec.requires {
419                 assertions.push(Box::new(spec_to_expr(a, &env)));
420             }
421 
422             let annotation = TermAnnotation {
423                 sig,
424                 assumptions,
425                 assertions,
426             };
427             annotation_map.insert(term_id, annotation);
428         }
429     }
430 
431     // Collect term instantiations.
432     let mut forms_map = HashMap::new();
433     for def in defs {
434         if let ast::Def::Form(form) = def {
435             let term_type_signatures: Vec<_> = form
436                 .signatures
437                 .iter()
438                 .map(signature_to_term_type_signature)
439                 .collect();
440             forms_map.insert(form.name.0.clone(), term_type_signatures);
441         }
442     }
443 
444     let mut instantiations_map = HashMap::new();
445     for def in defs {
446         if let ast::Def::Instantiation(inst) = def {
447             let term_id = termenv.get_term_by_name(typeenv, &inst.term).unwrap();
448             let sigs = match &inst.form {
449                 Some(form) => forms_map[&form.0].clone(),
450                 None => inst
451                     .signatures
452                     .iter()
453                     .map(signature_to_term_type_signature)
454                     .collect(),
455             };
456             instantiations_map.insert(term_id, sigs);
457         }
458     }
459 
460     AnnotationEnv {
461         annotation_map,
462         instantiations_map,
463         model_map,
464     }
465 }
466