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 {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 swith_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(swith_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
280fn 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
317fn 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
326fn 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
334pub 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}
veri_engine_lib/annotations.rs

veri_engine_lib/
annotations.rs
