veri_engine_lib/
annotations.rs

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

veri_engine_lib/
annotations.rs
