1 use itertools::Itertools;
2 use std::collections::{HashMap, HashSet};
3 use std::hash::Hash;
4
5 use crate::annotations::AnnotationEnv;
6 use crate::termname::pattern_contains_termname;
7 use cranelift_isle as isle;
8 use isle::sema::{Pattern, TermEnv, TermId, TypeEnv, VarId};
9 use itertools::izip;
10 use veri_ir::{annotation_ir, ConcreteTest, Expr, TermSignature, Type, TypeContext};
11
12 use crate::{Config, FLAGS_WIDTH, REG_WIDTH};
13
14 #[derive(Clone, Debug)]
15 struct RuleParseTree {
16 // a map of var name to type variable, where var could be
17 // Pattern::Var or var used in Pattern::BindPattern
18 varid_to_type_var_map: HashMap<VarId, u32>,
19 // a map of type var to value, if known
20 type_var_to_val_map: HashMap<u32, i128>,
21 // bookkeeping that tells the next unused type var
22 next_type_var: u32,
23 // combined constraints from all nodes
24 concrete_constraints: HashSet<TypeExpr>,
25 var_constraints: HashSet<TypeExpr>,
26 bv_constraints: HashSet<TypeExpr>,
27
28 ty_vars: HashMap<veri_ir::Expr, u32>,
29 quantified_vars: HashSet<(String, u32)>,
30 free_vars: HashSet<(String, u32)>,
31 // Used to check distinct models
32 term_input_bvs: Vec<String>,
33 // Used for custom verification conditions
34 term_args: Vec<String>,
35 lhs_assumptions: Vec<Expr>,
36 rhs_assumptions: Vec<Expr>,
37
38 rhs_assertions: Vec<Expr>,
39 concrete: Option<ConcreteTest>,
40 }
41
42 #[derive(Clone, Debug)]
43 pub enum TypeVarConstruct {
44 Var,
45 BindPattern,
46 Wildcard(u32),
47 Term(TermId),
48 Bool(bool),
49 Const(i128),
50 Let(Vec<String>),
51 And,
52 }
53
54 #[derive(Clone, Debug)]
55 pub struct TypeVarNode {
56 ident: String,
57 construct: TypeVarConstruct,
58 type_var: u32,
59 children: Vec<TypeVarNode>,
60 assertions: Vec<veri_ir::Expr>,
61 }
62
63 #[derive(Clone, Debug, Eq, Hash, PartialEq)]
64 // Constraints either assign concrete types to type variables
65 // or set them equal to other type variables
66 enum TypeExpr {
67 Concrete(u32, annotation_ir::Type),
68 Variable(u32, u32),
69 // The type variable of the first arg is equal to the value of the second
70 WidthInt(u32, u32),
71 }
72
73 #[derive(Debug)]
74 pub struct AnnotationTypeInfo {
75 // map of annotation variable to assigned type var
76 pub term: String,
77 pub var_to_type_var: HashMap<String, u32>,
78 }
79
80 #[derive(Debug)]
81 pub struct RuleSemantics {
82 pub annotation_infos: Vec<AnnotationTypeInfo>,
83
84 // map of type var to solved type
85 pub type_var_to_type: HashMap<u32, annotation_ir::Type>,
86
87 pub lhs: veri_ir::Expr,
88 pub rhs: veri_ir::Expr,
89 pub quantified_vars: Vec<veri_ir::BoundVar>,
90 pub free_vars: Vec<veri_ir::BoundVar>,
91 pub term_input_bvs: Vec<String>,
92 // Used for custom verification conditions
93 pub term_args: Vec<String>,
94 pub lhs_assumptions: Vec<Expr>,
95 pub rhs_assumptions: Vec<Expr>,
96 pub rhs_assertions: Vec<Expr>,
97 pub tyctx: TypeContext,
98 }
99
type_rules_with_term_and_types( termenv: &TermEnv, typeenv: &TypeEnv, annotation_env: &AnnotationEnv, config: &Config, types: &TermSignature, concrete: &Option<ConcreteTest>, ) -> HashMap<isle::sema::RuleId, RuleSemantics>100 pub fn type_rules_with_term_and_types(
101 termenv: &TermEnv,
102 typeenv: &TypeEnv,
103 annotation_env: &AnnotationEnv,
104 config: &Config,
105 types: &TermSignature,
106 concrete: &Option<ConcreteTest>,
107 ) -> HashMap<isle::sema::RuleId, RuleSemantics> {
108 let mut solutions = HashMap::new();
109
110 for rule in &termenv.rules {
111 // Only type rules with the given term on the LHS
112 if !pattern_contains_termname(
113 // Hack for now: typeid not used
114 &Pattern::Term(
115 cranelift_isle::sema::TypeId(0),
116 rule.root_term,
117 rule.args.clone(),
118 ),
119 &config.term,
120 termenv,
121 typeenv,
122 ) {
123 continue;
124 }
125 if let Some(names) = &config.names {
126 if rule.name.is_none() {
127 continue;
128 }
129 let name = &typeenv.syms[rule.name.unwrap().index()];
130 if !names.contains(name) {
131 continue;
132 }
133 }
134 if let Some(s) = type_annotations_using_rule(
135 rule,
136 annotation_env,
137 typeenv,
138 termenv,
139 &config.term,
140 types,
141 concrete,
142 ) {
143 solutions.insert(rule.id, s);
144 }
145 }
146 solutions
147 }
148
convert_type(aty: &annotation_ir::Type) -> veri_ir::Type149 fn convert_type(aty: &annotation_ir::Type) -> veri_ir::Type {
150 match aty {
151 annotation_ir::Type::BitVectorUnknown(..) => veri_ir::Type::BitVector(None),
152 annotation_ir::Type::BitVector => veri_ir::Type::BitVector(None),
153 annotation_ir::Type::BitVectorWithWidth(w) => veri_ir::Type::BitVector(Some(*w)),
154 annotation_ir::Type::Int => veri_ir::Type::Int,
155 annotation_ir::Type::Bool => veri_ir::Type::Bool,
156 annotation_ir::Type::Unit => veri_ir::Type::Unit,
157 annotation_ir::Type::Poly(_) => veri_ir::Type::BitVector(None),
158 }
159 }
160
type_annotations_using_rule<'a>( rule: &'a isle::sema::Rule, annotation_env: &'a AnnotationEnv, typeenv: &'a TypeEnv, termenv: &'a TermEnv, term: &String, types: &TermSignature, concrete: &'a Option<ConcreteTest>, ) -> Option<RuleSemantics>161 fn type_annotations_using_rule<'a>(
162 rule: &'a isle::sema::Rule,
163 annotation_env: &'a AnnotationEnv,
164 typeenv: &'a TypeEnv,
165 termenv: &'a TermEnv,
166 term: &String,
167 types: &TermSignature,
168 concrete: &'a Option<ConcreteTest>,
169 ) -> Option<RuleSemantics> {
170 let mut parse_tree = RuleParseTree {
171 varid_to_type_var_map: HashMap::new(),
172 type_var_to_val_map: HashMap::new(),
173 next_type_var: 1,
174 concrete_constraints: HashSet::new(),
175 var_constraints: HashSet::new(),
176 bv_constraints: HashSet::new(),
177 ty_vars: HashMap::new(),
178 quantified_vars: HashSet::new(),
179 free_vars: HashSet::new(),
180 term_input_bvs: vec![],
181 term_args: vec![],
182 lhs_assumptions: vec![],
183 rhs_assumptions: vec![],
184 rhs_assertions: vec![],
185 concrete: concrete.clone(),
186 };
187
188 let mut annotation_infos = vec![];
189 if !rule.iflets.is_empty() {
190 for iflet in &rule.iflets {
191 let iflet_lhs = &mut create_parse_tree_pattern(
192 rule,
193 &iflet.lhs,
194 &mut parse_tree,
195 typeenv,
196 termenv,
197 term,
198 types,
199 );
200 let iflet_rhs =
201 &mut create_parse_tree_expr(rule, &iflet.rhs, &mut parse_tree, typeenv, termenv);
202
203 let iflet_lhs_expr = add_rule_constraints(
204 &mut parse_tree,
205 iflet_lhs,
206 termenv,
207 typeenv,
208 annotation_env,
209 &mut annotation_infos,
210 false,
211 );
212 iflet_lhs_expr.as_ref()?;
213
214 let iflet_rhs_expr = add_rule_constraints(
215 &mut parse_tree,
216 iflet_rhs,
217 termenv,
218 typeenv,
219 annotation_env,
220 &mut annotation_infos,
221 false,
222 );
223 iflet_rhs_expr.as_ref()?;
224 parse_tree
225 .var_constraints
226 .insert(TypeExpr::Variable(iflet_lhs.type_var, iflet_rhs.type_var));
227 // Add if-lets to the LHS
228 parse_tree.lhs_assumptions.push(veri_ir::Expr::Binary(
229 veri_ir::BinaryOp::Eq,
230 Box::new(iflet_lhs_expr.unwrap()),
231 Box::new(iflet_rhs_expr.unwrap()),
232 ));
233 }
234 }
235 let lhs = &mut create_parse_tree_pattern(
236 rule,
237 // Hack for now: typeid not used
238 &isle::sema::Pattern::Term(
239 cranelift_isle::sema::TypeId(0),
240 rule.root_term,
241 rule.args.clone(),
242 ),
243 &mut parse_tree,
244 typeenv,
245 termenv,
246 term,
247 types,
248 );
249 let rhs = &mut create_parse_tree_expr(rule, &rule.rhs, &mut parse_tree, typeenv, termenv);
250
251 log::trace!("LHS:");
252 let lhs_expr = add_rule_constraints(
253 &mut parse_tree,
254 lhs,
255 termenv,
256 typeenv,
257 annotation_env,
258 &mut annotation_infos,
259 false,
260 );
261 lhs_expr.as_ref()?;
262 log::trace!("\n\tRHS:");
263 let rhs_expr = add_rule_constraints(
264 &mut parse_tree,
265 rhs,
266 termenv,
267 typeenv,
268 annotation_env,
269 &mut annotation_infos,
270 true,
271 );
272 rhs_expr.as_ref()?;
273
274 match (lhs_expr, rhs_expr) {
275 (Some(lhs_expr), Some(rhs_expr)) => {
276 parse_tree
277 .var_constraints
278 .insert(TypeExpr::Variable(lhs.type_var, rhs.type_var));
279
280 let (solution, bv_unknown_width_sets) = solve_constraints(
281 parse_tree.concrete_constraints,
282 parse_tree.var_constraints,
283 parse_tree.bv_constraints,
284 &mut parse_tree.type_var_to_val_map,
285 Some(&parse_tree.ty_vars),
286 );
287
288 let mut tymap = HashMap::new();
289
290 for (expr, t) in &parse_tree.ty_vars {
291 if let Some(ty) = solution.get(t) {
292 tymap.insert(*t, convert_type(ty));
293 } else {
294 panic!("missing type variable {t} in solution for: {expr:?}");
295 }
296 }
297 let mut quantified_vars = vec![];
298 for (s, t) in parse_tree.quantified_vars.iter().sorted() {
299 let expr = veri_ir::Expr::Terminal(veri_ir::Terminal::Var(s.clone()));
300 if let Some(ty) = solution.get(t) {
301 let ty = convert_type(ty);
302 parse_tree.ty_vars.insert(expr, *t);
303 tymap.insert(*t, ty);
304 quantified_vars.push(veri_ir::BoundVar {
305 name: s.clone(),
306 tyvar: *t,
307 });
308 } else {
309 panic!("missing type variable {t} in solution for: {expr:?}");
310 }
311 }
312 let mut free_vars = vec![];
313 for (s, t) in parse_tree.free_vars {
314 let expr = veri_ir::Expr::Terminal(veri_ir::Terminal::Var(s.clone()));
315 if let Some(ty) = solution.get(&t) {
316 let ty = convert_type(ty);
317 parse_tree.ty_vars.insert(expr, t);
318 tymap.insert(t, ty);
319 free_vars.push(veri_ir::BoundVar { name: s, tyvar: t });
320 } else {
321 panic!("missing type variable {t} in solution for: {expr:?}");
322 }
323 }
324
325 Some(RuleSemantics {
326 annotation_infos,
327 type_var_to_type: solution,
328 lhs: lhs_expr,
329 rhs: rhs_expr,
330 lhs_assumptions: parse_tree.lhs_assumptions,
331 rhs_assumptions: parse_tree.rhs_assumptions,
332 rhs_assertions: parse_tree.rhs_assertions,
333 quantified_vars,
334 free_vars,
335 term_input_bvs: parse_tree.term_input_bvs,
336 term_args: parse_tree.term_args,
337 tyctx: TypeContext {
338 tyvars: parse_tree.ty_vars.clone(),
339 tymap,
340 tyvals: parse_tree.type_var_to_val_map,
341 bv_unknown_width_sets,
342 },
343 })
344 }
345 _ => None,
346 }
347 }
348
const_fold_to_int(e: &veri_ir::Expr) -> Option<i128>349 fn const_fold_to_int(e: &veri_ir::Expr) -> Option<i128> {
350 match e {
351 Expr::Terminal(veri_ir::Terminal::Const(c, _)) => Some(*c),
352 _ => None,
353 }
354 }
355
add_annotation_constraints( expr: annotation_ir::Expr, tree: &mut RuleParseTree, annotation_info: &mut AnnotationTypeInfo, ) -> (veri_ir::Expr, u32)356 fn add_annotation_constraints(
357 expr: annotation_ir::Expr,
358 tree: &mut RuleParseTree,
359 annotation_info: &mut AnnotationTypeInfo,
360 ) -> (veri_ir::Expr, u32) {
361 let (e, t) = match expr {
362 annotation_ir::Expr::Var(x, ..) => {
363 if !annotation_info.var_to_type_var.contains_key(&x) {
364 panic!("Error: unbound variable: {x}");
365 }
366 let t = annotation_info.var_to_type_var[&x];
367 let name = format!("{}__{}__{}", annotation_info.term, x, t);
368 (veri_ir::Expr::Terminal(veri_ir::Terminal::Var(name)), t)
369 }
370 annotation_ir::Expr::Const(c, ..) => {
371 let t = tree.next_type_var;
372 let e = veri_ir::Expr::Terminal(veri_ir::Terminal::Const(c.value, t));
373 match c.ty {
374 annotation_ir::Type::BitVector => {
375 let ty = annotation_ir::Type::BitVectorWithWidth(c.width);
376 tree.concrete_constraints.insert(TypeExpr::Concrete(t, ty));
377 }
378 _ => {
379 tree.concrete_constraints
380 .insert(TypeExpr::Concrete(t, c.ty.clone()));
381 }
382 }
383 tree.next_type_var += 1;
384
385 // If constant is known, add the value to the tree. Useful for
386 // capturing isleTypes
387 tree.type_var_to_val_map.insert(t, c.value);
388 (e, t)
389 }
390 annotation_ir::Expr::True => {
391 let t = tree.next_type_var;
392 tree.concrete_constraints
393 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
394
395 tree.next_type_var += 1;
396 (veri_ir::Expr::Terminal(veri_ir::Terminal::True), t)
397 }
398 annotation_ir::Expr::False => {
399 let t = tree.next_type_var;
400 tree.concrete_constraints
401 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
402
403 tree.next_type_var += 1;
404 (veri_ir::Expr::Terminal(veri_ir::Terminal::False), t)
405 }
406
407 annotation_ir::Expr::WidthOf(x) => {
408 let (ex, tx) = add_annotation_constraints(*x.clone(), tree, annotation_info);
409 let t = tree.next_type_var;
410 tree.next_type_var += 1;
411 tree.bv_constraints
412 .insert(TypeExpr::Concrete(tx, annotation_ir::Type::BitVector));
413 tree.concrete_constraints
414 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Int));
415 tree.concrete_constraints.insert(TypeExpr::WidthInt(tx, t));
416 (veri_ir::Expr::WidthOf(Box::new(ex)), t)
417 }
418
419 annotation_ir::Expr::Eq(x, y) => {
420 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
421 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
422 let t = tree.next_type_var;
423
424 tree.concrete_constraints
425 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
426 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
427
428 tree.next_type_var += 1;
429 (
430 veri_ir::Expr::Binary(veri_ir::BinaryOp::Eq, Box::new(e1), Box::new(e2)),
431 t,
432 )
433 }
434 annotation_ir::Expr::Imp(x, y) => {
435 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
436 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
437 let t = tree.next_type_var;
438
439 tree.concrete_constraints
440 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Bool));
441 tree.concrete_constraints
442 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Bool));
443 tree.concrete_constraints
444 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
445
446 tree.next_type_var += 1;
447 (
448 veri_ir::Expr::Binary(veri_ir::BinaryOp::Imp, Box::new(e1), Box::new(e2)),
449 t,
450 )
451 }
452 annotation_ir::Expr::Lte(x, y) => {
453 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
454 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
455 let t = tree.next_type_var;
456
457 tree.concrete_constraints
458 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
459 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
460
461 tree.next_type_var += 1;
462 (
463 veri_ir::Expr::Binary(veri_ir::BinaryOp::Lte, Box::new(e1), Box::new(e2)),
464 t,
465 )
466 }
467
468 annotation_ir::Expr::Not(x) => {
469 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
470 let t = tree.next_type_var;
471
472 tree.concrete_constraints
473 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Bool));
474 tree.concrete_constraints
475 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
476
477 tree.next_type_var += 1;
478 (veri_ir::Expr::Unary(veri_ir::UnaryOp::Not, Box::new(e1)), t)
479 }
480 annotation_ir::Expr::Or(x, y) => {
481 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
482 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
483 let t = tree.next_type_var;
484
485 tree.concrete_constraints
486 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
487 tree.concrete_constraints
488 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Bool));
489 tree.concrete_constraints
490 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Bool));
491
492 tree.next_type_var += 1;
493 (
494 veri_ir::Expr::Binary(veri_ir::BinaryOp::Or, Box::new(e1), Box::new(e2)),
495 t,
496 )
497 }
498 annotation_ir::Expr::And(x, y) => {
499 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
500 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
501 let t = tree.next_type_var;
502
503 tree.concrete_constraints
504 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
505 tree.concrete_constraints
506 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Bool));
507 tree.concrete_constraints
508 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Bool));
509
510 tree.next_type_var += 1;
511 (
512 veri_ir::Expr::Binary(veri_ir::BinaryOp::And, Box::new(e1), Box::new(e2)),
513 t,
514 )
515 }
516
517 annotation_ir::Expr::BVSgt(x, y) => {
518 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
519 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
520 let t = tree.next_type_var;
521
522 tree.concrete_constraints
523 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
524 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
525
526 tree.next_type_var += 1;
527 (
528 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSgt, Box::new(e1), Box::new(e2)),
529 t,
530 )
531 }
532
533 annotation_ir::Expr::BVSgte(x, y) => {
534 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
535 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
536 let t = tree.next_type_var;
537
538 tree.concrete_constraints
539 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
540 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
541
542 tree.next_type_var += 1;
543 (
544 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSgte, Box::new(e1), Box::new(e2)),
545 t,
546 )
547 }
548
549 annotation_ir::Expr::BVSlt(x, y) => {
550 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
551 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
552 let t = tree.next_type_var;
553
554 tree.concrete_constraints
555 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
556 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
557
558 tree.next_type_var += 1;
559 (
560 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSlt, Box::new(e1), Box::new(e2)),
561 t,
562 )
563 }
564
565 annotation_ir::Expr::BVSlte(x, y) => {
566 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
567 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
568 let t = tree.next_type_var;
569
570 tree.concrete_constraints
571 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
572 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
573
574 tree.next_type_var += 1;
575 (
576 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSlte, Box::new(e1), Box::new(e2)),
577 t,
578 )
579 }
580
581 annotation_ir::Expr::BVUgt(x, y) => {
582 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
583 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
584 let t = tree.next_type_var;
585
586 tree.concrete_constraints
587 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
588 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
589
590 tree.next_type_var += 1;
591 (
592 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVUgt, Box::new(e1), Box::new(e2)),
593 t,
594 )
595 }
596
597 annotation_ir::Expr::BVUgte(x, y) => {
598 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
599 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
600 let t = tree.next_type_var;
601
602 tree.concrete_constraints
603 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
604 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
605
606 tree.next_type_var += 1;
607 (
608 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVUgte, Box::new(e1), Box::new(e2)),
609 t,
610 )
611 }
612
613 annotation_ir::Expr::BVUlt(x, y) => {
614 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
615 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
616 let t = tree.next_type_var;
617
618 tree.concrete_constraints
619 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
620 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
621
622 tree.next_type_var += 1;
623 (
624 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVUlt, Box::new(e1), Box::new(e2)),
625 t,
626 )
627 }
628
629 annotation_ir::Expr::BVUlte(x, y) => {
630 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
631 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
632 let t = tree.next_type_var;
633
634 tree.concrete_constraints
635 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
636 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
637
638 tree.next_type_var += 1;
639 (
640 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVUlte, Box::new(e1), Box::new(e2)),
641 t,
642 )
643 }
644
645 annotation_ir::Expr::BVSaddo(x, y) => {
646 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
647 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
648 let t = tree.next_type_var;
649
650 tree.concrete_constraints
651 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
652 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
653
654 tree.next_type_var += 1;
655 (
656 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSaddo, Box::new(e1), Box::new(e2)),
657 t,
658 )
659 }
660
661 annotation_ir::Expr::BVNeg(x) => {
662 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
663
664 let t = tree.next_type_var;
665 tree.bv_constraints
666 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
667 tree.bv_constraints
668 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
669 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
670
671 tree.next_type_var += 1;
672 (
673 veri_ir::Expr::Unary(veri_ir::UnaryOp::BVNeg, Box::new(e1)),
674 t,
675 )
676 }
677 annotation_ir::Expr::BVNot(x) => {
678 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
679
680 let t = tree.next_type_var;
681 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
682
683 tree.next_type_var += 1;
684 (
685 veri_ir::Expr::Unary(veri_ir::UnaryOp::BVNot, Box::new(e1)),
686 t,
687 )
688 }
689
690 annotation_ir::Expr::BVMul(x, y) => {
691 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
692 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
693 let t = tree.next_type_var;
694
695 tree.bv_constraints
696 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
697 tree.bv_constraints
698 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
699 tree.bv_constraints
700 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
701 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
702 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
703 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
704
705 tree.next_type_var += 1;
706 (
707 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVMul, Box::new(e1), Box::new(e2)),
708 t,
709 )
710 }
711 annotation_ir::Expr::BVUDiv(x, y) => {
712 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
713 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
714 let t = tree.next_type_var;
715
716 tree.bv_constraints
717 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
718 tree.bv_constraints
719 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
720 tree.bv_constraints
721 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
722 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
723 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
724 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
725
726 tree.next_type_var += 1;
727 (
728 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVUDiv, Box::new(e1), Box::new(e2)),
729 t,
730 )
731 }
732 annotation_ir::Expr::BVSDiv(x, y) => {
733 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
734 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
735 let t = tree.next_type_var;
736
737 tree.bv_constraints
738 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
739 tree.bv_constraints
740 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
741 tree.bv_constraints
742 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
743 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
744 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
745 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
746
747 tree.next_type_var += 1;
748 (
749 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSDiv, Box::new(e1), Box::new(e2)),
750 t,
751 )
752 }
753 annotation_ir::Expr::BVAdd(x, y) => {
754 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
755 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
756 let t = tree.next_type_var;
757
758 tree.bv_constraints
759 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
760 tree.bv_constraints
761 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
762 tree.bv_constraints
763 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
764 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
765 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
766 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
767
768 tree.next_type_var += 1;
769 (
770 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVAdd, Box::new(e1), Box::new(e2)),
771 t,
772 )
773 }
774 annotation_ir::Expr::BVSub(x, y) => {
775 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
776 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
777 let t = tree.next_type_var;
778
779 tree.bv_constraints
780 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
781 tree.bv_constraints
782 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
783 tree.bv_constraints
784 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
785 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
786 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
787 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
788
789 tree.next_type_var += 1;
790 (
791 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSub, Box::new(e1), Box::new(e2)),
792 t,
793 )
794 }
795 annotation_ir::Expr::BVUrem(x, y) => {
796 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
797 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
798 let t = tree.next_type_var;
799
800 tree.bv_constraints
801 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
802 tree.bv_constraints
803 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
804 tree.bv_constraints
805 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
806 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
807 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
808 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
809
810 tree.next_type_var += 1;
811 (
812 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVUrem, Box::new(e1), Box::new(e2)),
813 t,
814 )
815 }
816 annotation_ir::Expr::BVSrem(x, y) => {
817 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
818 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
819 let t = tree.next_type_var;
820
821 tree.bv_constraints
822 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
823 tree.bv_constraints
824 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
825 tree.bv_constraints
826 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
827 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
828 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
829 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
830
831 tree.next_type_var += 1;
832 (
833 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSrem, Box::new(e1), Box::new(e2)),
834 t,
835 )
836 }
837
838 annotation_ir::Expr::BVAnd(x, y) => {
839 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
840 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
841 let t = tree.next_type_var;
842
843 tree.bv_constraints
844 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
845 tree.bv_constraints
846 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
847 tree.bv_constraints
848 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
849 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
850 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
851 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
852
853 tree.next_type_var += 1;
854 (
855 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVAnd, Box::new(e1), Box::new(e2)),
856 t,
857 )
858 }
859 annotation_ir::Expr::BVOr(x, y) => {
860 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
861 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
862 let t = tree.next_type_var;
863
864 tree.bv_constraints
865 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
866 tree.bv_constraints
867 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
868 tree.bv_constraints
869 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
870 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
871 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
872 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
873
874 tree.next_type_var += 1;
875 (
876 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVOr, Box::new(e1), Box::new(e2)),
877 t,
878 )
879 }
880 annotation_ir::Expr::BVXor(x, y) => {
881 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
882 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
883 let t = tree.next_type_var;
884
885 tree.bv_constraints
886 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
887 tree.bv_constraints
888 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
889 tree.bv_constraints
890 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
891 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
892 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
893 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
894
895 tree.next_type_var += 1;
896 (
897 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVXor, Box::new(e1), Box::new(e2)),
898 t,
899 )
900 }
901 annotation_ir::Expr::BVRotl(x, a) => {
902 let (xe, xt) = add_annotation_constraints(*x, tree, annotation_info);
903 let (ae, at) = add_annotation_constraints(*a, tree, annotation_info);
904 let t = tree.next_type_var;
905 tree.next_type_var += 1;
906
907 tree.bv_constraints
908 .insert(TypeExpr::Concrete(xt, annotation_ir::Type::BitVector));
909 tree.bv_constraints
910 .insert(TypeExpr::Concrete(at, annotation_ir::Type::BitVector));
911 tree.var_constraints.insert(TypeExpr::Variable(t, xt));
912
913 (
914 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVRotl, Box::new(xe), Box::new(ae)),
915 t,
916 )
917 }
918 annotation_ir::Expr::BVRotr(x, a) => {
919 let (xe, xt) = add_annotation_constraints(*x, tree, annotation_info);
920 let (ae, at) = add_annotation_constraints(*a, tree, annotation_info);
921 let t = tree.next_type_var;
922 tree.next_type_var += 1;
923
924 tree.bv_constraints
925 .insert(TypeExpr::Concrete(xt, annotation_ir::Type::BitVector));
926 tree.bv_constraints
927 .insert(TypeExpr::Concrete(at, annotation_ir::Type::BitVector));
928 tree.var_constraints.insert(TypeExpr::Variable(t, xt));
929
930 (
931 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVRotr, Box::new(xe), Box::new(ae)),
932 t,
933 )
934 }
935 annotation_ir::Expr::BVShl(x, a) => {
936 let (xe, xt) = add_annotation_constraints(*x, tree, annotation_info);
937 let (ae, at) = add_annotation_constraints(*a, tree, annotation_info);
938 let t = tree.next_type_var;
939 tree.next_type_var += 1;
940
941 tree.bv_constraints
942 .insert(TypeExpr::Concrete(xt, annotation_ir::Type::BitVector));
943 tree.bv_constraints
944 .insert(TypeExpr::Concrete(at, annotation_ir::Type::BitVector));
945 tree.var_constraints.insert(TypeExpr::Variable(t, xt));
946 tree.var_constraints.insert(TypeExpr::Variable(xt, at));
947
948 (
949 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVShl, Box::new(xe), Box::new(ae)),
950 t,
951 )
952 }
953 annotation_ir::Expr::BVShr(x, a) => {
954 let (xe, xt) = add_annotation_constraints(*x, tree, annotation_info);
955 let (ae, at) = add_annotation_constraints(*a, tree, annotation_info);
956 let t = tree.next_type_var;
957 tree.next_type_var += 1;
958
959 tree.bv_constraints
960 .insert(TypeExpr::Concrete(xt, annotation_ir::Type::BitVector));
961 tree.bv_constraints
962 .insert(TypeExpr::Concrete(at, annotation_ir::Type::BitVector));
963 tree.var_constraints.insert(TypeExpr::Variable(t, xt));
964 tree.var_constraints.insert(TypeExpr::Variable(xt, at));
965
966 (
967 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVShr, Box::new(xe), Box::new(ae)),
968 t,
969 )
970 }
971 annotation_ir::Expr::BVAShr(x, a) => {
972 let (xe, xt) = add_annotation_constraints(*x, tree, annotation_info);
973 let (ae, at) = add_annotation_constraints(*a, tree, annotation_info);
974 let t = tree.next_type_var;
975 tree.next_type_var += 1;
976
977 tree.bv_constraints
978 .insert(TypeExpr::Concrete(xt, annotation_ir::Type::BitVector));
979 tree.bv_constraints
980 .insert(TypeExpr::Concrete(at, annotation_ir::Type::BitVector));
981 tree.var_constraints.insert(TypeExpr::Variable(t, xt));
982 tree.var_constraints.insert(TypeExpr::Variable(at, xt));
983
984 (
985 veri_ir::Expr::Binary(veri_ir::BinaryOp::BVAShr, Box::new(xe), Box::new(ae)),
986 t,
987 )
988 }
989 annotation_ir::Expr::Lt(x, y) => {
990 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
991 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
992 let t = tree.next_type_var;
993
994 tree.concrete_constraints
995 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
996 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
997
998 tree.next_type_var += 1;
999 (
1000 veri_ir::Expr::Binary(veri_ir::BinaryOp::Lt, Box::new(e1), Box::new(e2)),
1001 t,
1002 )
1003 }
1004 annotation_ir::Expr::BVConvTo(w, x) => {
1005 let (we, wt) = add_annotation_constraints(*w, tree, annotation_info);
1006 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1007 let t = tree.next_type_var;
1008 tree.next_type_var += 1;
1009
1010 // In the dynamic case, we don't know the width at this point
1011 tree.concrete_constraints
1012 .insert(TypeExpr::Concrete(wt, annotation_ir::Type::Int));
1013
1014 if let Some(w) = const_fold_to_int(&we) {
1015 tree.concrete_constraints.insert(TypeExpr::Concrete(
1016 t,
1017 annotation_ir::Type::BitVectorWithWidth(w.try_into().unwrap()),
1018 ));
1019 tree.bv_constraints
1020 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1021 let t2 = tree.next_type_var;
1022 tree.next_type_var += 1;
1023 let width = Expr::Terminal(veri_ir::Terminal::Const(w, t2));
1024 tree.type_var_to_val_map.insert(t2, w);
1025 tree.ty_vars.insert(width.clone(), t2);
1026 tree.concrete_constraints
1027 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Int));
1028 (veri_ir::Expr::BVConvTo(Box::new(width), Box::new(e1)), t)
1029 } else {
1030 tree.concrete_constraints.insert(TypeExpr::WidthInt(t, wt));
1031 tree.bv_constraints
1032 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1033 tree.bv_constraints
1034 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1035
1036 (veri_ir::Expr::BVConvTo(Box::new(we), Box::new(e1)), t)
1037 }
1038 }
1039 annotation_ir::Expr::BVSignExtToVarWidth(w, x) => {
1040 let (we, wt) = add_annotation_constraints(*w, tree, annotation_info);
1041 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1042 let t = tree.next_type_var;
1043 tree.next_type_var += 1;
1044
1045 // In the dynamic case, we don't know the width at this point
1046 tree.concrete_constraints
1047 .insert(TypeExpr::Concrete(wt, annotation_ir::Type::Int));
1048 tree.bv_constraints
1049 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1050 tree.bv_constraints
1051 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1052
1053 (
1054 veri_ir::Expr::BVSignExtToVarWidth(Box::new(we), Box::new(e1)),
1055 t,
1056 )
1057 }
1058 annotation_ir::Expr::BVZeroExtTo(w, x) => {
1059 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1060 let t = tree.next_type_var;
1061 tree.next_type_var += 1;
1062
1063 let width = match *w {
1064 veri_ir::annotation_ir::Width::Const(c) => c,
1065 veri_ir::annotation_ir::Width::RegWidth => REG_WIDTH,
1066 };
1067
1068 tree.bv_constraints
1069 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1070 tree.concrete_constraints.insert(TypeExpr::Concrete(
1071 t,
1072 annotation_ir::Type::BitVectorWithWidth(width),
1073 ));
1074
1075 (veri_ir::Expr::BVZeroExtTo(width, Box::new(e1)), t)
1076 }
1077 annotation_ir::Expr::BVZeroExtToVarWidth(w, x) => {
1078 let (we, wt) = add_annotation_constraints(*w, tree, annotation_info);
1079 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1080 let t = tree.next_type_var;
1081 tree.next_type_var += 1;
1082
1083 // In the dynamic case, we don't know the width at this point
1084 tree.concrete_constraints
1085 .insert(TypeExpr::Concrete(wt, annotation_ir::Type::Int));
1086 tree.bv_constraints
1087 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1088 tree.bv_constraints
1089 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1090
1091 (
1092 veri_ir::Expr::BVZeroExtToVarWidth(Box::new(we), Box::new(e1)),
1093 t,
1094 )
1095 }
1096 annotation_ir::Expr::BVSignExtTo(w, x) => {
1097 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1098 let t = tree.next_type_var;
1099
1100 let width = match *w {
1101 veri_ir::annotation_ir::Width::Const(c) => c,
1102 veri_ir::annotation_ir::Width::RegWidth => REG_WIDTH,
1103 };
1104
1105 tree.bv_constraints
1106 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1107 tree.concrete_constraints.insert(TypeExpr::Concrete(
1108 t,
1109 annotation_ir::Type::BitVectorWithWidth(width),
1110 ));
1111
1112 tree.next_type_var += 1;
1113
1114 (veri_ir::Expr::BVSignExtTo(width, Box::new(e1)), t)
1115 }
1116 annotation_ir::Expr::BVExtract(l, r, x) => {
1117 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1118 let t = tree.next_type_var;
1119
1120 tree.bv_constraints
1121 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1122 tree.concrete_constraints.insert(TypeExpr::Concrete(
1123 t,
1124 annotation_ir::Type::BitVectorWithWidth(l - r + 1),
1125 ));
1126
1127 tree.next_type_var += 1;
1128
1129 (veri_ir::Expr::BVExtract(l, r, Box::new(e1)), t)
1130 }
1131 annotation_ir::Expr::BVConcat(xs) => {
1132 // AVH todo: doesn't sum the various widths, has to be done in the solver
1133 let t = tree.next_type_var;
1134 tree.next_type_var += 1;
1135
1136 let mut exprs = vec![];
1137 for x in xs {
1138 let (xe, xt) = add_annotation_constraints(x, tree, annotation_info);
1139 tree.bv_constraints
1140 .insert(TypeExpr::Concrete(xt, annotation_ir::Type::BitVector));
1141 exprs.push(xe);
1142 }
1143 tree.bv_constraints
1144 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1145
1146 tree.next_type_var += 1;
1147
1148 (veri_ir::Expr::BVConcat(exprs), t)
1149 }
1150 annotation_ir::Expr::BVIntToBv(w, x) => {
1151 let (ex, tx) = add_annotation_constraints(*x.clone(), tree, annotation_info);
1152
1153 let t = tree.next_type_var;
1154 tree.next_type_var += 1;
1155
1156 tree.concrete_constraints
1157 .insert(TypeExpr::Concrete(tx, annotation_ir::Type::Int));
1158
1159 tree.concrete_constraints.insert(TypeExpr::Concrete(
1160 t,
1161 annotation_ir::Type::BitVectorWithWidth(w),
1162 ));
1163
1164 (veri_ir::Expr::BVIntToBV(w, Box::new(ex)), t)
1165 }
1166 annotation_ir::Expr::BVToInt(x) => {
1167 let (ex, tx) = add_annotation_constraints(*x.clone(), tree, annotation_info);
1168
1169 let t = tree.next_type_var;
1170 tree.next_type_var += 1;
1171
1172 tree.bv_constraints
1173 .insert(TypeExpr::Concrete(tx, annotation_ir::Type::BitVector));
1174
1175 tree.concrete_constraints
1176 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Int));
1177
1178 (veri_ir::Expr::BVToInt(Box::new(ex)), t)
1179 }
1180 annotation_ir::Expr::Conditional(c, t, e) => {
1181 let (e1, t1) = add_annotation_constraints(*c, tree, annotation_info);
1182 let (e2, t2) = add_annotation_constraints(*t, tree, annotation_info);
1183 let (e3, t3) = add_annotation_constraints(*e, tree, annotation_info);
1184 let t = tree.next_type_var;
1185
1186 tree.concrete_constraints
1187 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Bool));
1188 tree.var_constraints.insert(TypeExpr::Variable(t2, t3));
1189 tree.var_constraints.insert(TypeExpr::Variable(t, t2));
1190
1191 tree.next_type_var += 1;
1192 (
1193 veri_ir::Expr::Conditional(Box::new(e1), Box::new(e2), Box::new(e3)),
1194 t,
1195 )
1196 }
1197 annotation_ir::Expr::Switch(c, cases) => {
1198 let (c_expr, c_t) = add_annotation_constraints(*c, tree, annotation_info);
1199
1200 let t = tree.next_type_var;
1201 tree.next_type_var += 1;
1202
1203 let mut case_exprs = vec![];
1204 for (m, b) in cases {
1205 let (case_expr, case_t) =
1206 add_annotation_constraints(m.clone(), tree, annotation_info);
1207 let (body_expr, body_t) =
1208 add_annotation_constraints(b.clone(), tree, annotation_info);
1209
1210 tree.var_constraints.insert(TypeExpr::Variable(c_t, case_t));
1211 tree.var_constraints.insert(TypeExpr::Variable(t, body_t));
1212 case_exprs.push((case_expr, body_expr));
1213 }
1214 (veri_ir::Expr::Switch(Box::new(c_expr), case_exprs), t)
1215 }
1216 annotation_ir::Expr::CLZ(x) => {
1217 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1218
1219 let t = tree.next_type_var;
1220 tree.bv_constraints
1221 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1222 tree.bv_constraints
1223 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1224 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
1225
1226 tree.next_type_var += 1;
1227 (veri_ir::Expr::CLZ(Box::new(e1)), t)
1228 }
1229 annotation_ir::Expr::CLS(x) => {
1230 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1231
1232 let t = tree.next_type_var;
1233 tree.bv_constraints
1234 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1235 tree.bv_constraints
1236 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1237 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
1238
1239 tree.next_type_var += 1;
1240 (veri_ir::Expr::CLS(Box::new(e1)), t)
1241 }
1242 annotation_ir::Expr::Rev(x) => {
1243 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1244
1245 let t = tree.next_type_var;
1246 tree.bv_constraints
1247 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1248 tree.bv_constraints
1249 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1250 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
1251
1252 tree.next_type_var += 1;
1253 (veri_ir::Expr::Rev(Box::new(e1)), t)
1254 }
1255 annotation_ir::Expr::BVSubs(ty, x, y) => {
1256 let (e0, t0) = add_annotation_constraints(*ty, tree, annotation_info);
1257 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1258 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
1259
1260 let t = tree.next_type_var;
1261
1262 // For aarch64, subs sets 4 flags. Model these as 4 bit appended to the left of the
1263 // register.
1264 tree.concrete_constraints.insert(TypeExpr::Concrete(
1265 t,
1266 annotation_ir::Type::BitVectorWithWidth(REG_WIDTH + FLAGS_WIDTH),
1267 ));
1268 tree.concrete_constraints
1269 .insert(TypeExpr::Concrete(t0, annotation_ir::Type::Int));
1270 tree.bv_constraints
1271 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1272 tree.bv_constraints
1273 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
1274 tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
1275
1276 tree.next_type_var += 1;
1277 (
1278 veri_ir::Expr::BVSubs(Box::new(e0), Box::new(e1), Box::new(e2)),
1279 t,
1280 )
1281 }
1282 annotation_ir::Expr::BVPopcnt(x) => {
1283 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1284
1285 let t = tree.next_type_var;
1286
1287 tree.bv_constraints
1288 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1289 tree.bv_constraints
1290 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1291 tree.var_constraints.insert(TypeExpr::Variable(t, t1));
1292
1293 tree.next_type_var += 1;
1294 (veri_ir::Expr::BVPopcnt(Box::new(e1)), t)
1295 }
1296 annotation_ir::Expr::LoadEffect(x, y, z) => {
1297 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1298 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
1299 let (e3, t3) = add_annotation_constraints(*z, tree, annotation_info);
1300 let t = tree.next_type_var;
1301
1302 tree.bv_constraints
1303 .insert(TypeExpr::Concrete(t, annotation_ir::Type::BitVector));
1304 tree.bv_constraints
1305 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::BitVector));
1306 tree.concrete_constraints
1307 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Int));
1308 tree.bv_constraints
1309 .insert(TypeExpr::Concrete(t3, annotation_ir::Type::BitVector));
1310
1311 tree.next_type_var += 1;
1312 (
1313 veri_ir::Expr::LoadEffect(Box::new(e1), Box::new(e2), Box::new(e3)),
1314 t,
1315 )
1316 }
1317 annotation_ir::Expr::StoreEffect(w, x, y, z) => {
1318 let (e0, t0) = add_annotation_constraints(*w, tree, annotation_info);
1319 let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
1320 let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
1321 let (e3, t3) = add_annotation_constraints(*z, tree, annotation_info);
1322 let t = tree.next_type_var;
1323
1324 tree.concrete_constraints
1325 .insert(TypeExpr::Concrete(t, annotation_ir::Type::Unit));
1326 tree.bv_constraints
1327 .insert(TypeExpr::Concrete(t0, annotation_ir::Type::BitVector));
1328 tree.concrete_constraints
1329 .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Int));
1330 tree.bv_constraints
1331 .insert(TypeExpr::Concrete(t2, annotation_ir::Type::BitVector));
1332 tree.bv_constraints
1333 .insert(TypeExpr::Concrete(t3, annotation_ir::Type::BitVector));
1334
1335 tree.next_type_var += 1;
1336 (
1337 veri_ir::Expr::StoreEffect(Box::new(e0), Box::new(e1), Box::new(e2), Box::new(e3)),
1338 t,
1339 )
1340 }
1341 };
1342 tree.ty_vars.insert(e.clone(), t);
1343 // let fmt = format!("{}:\t{:?}", t, e);
1344 // dbg!(fmt);
1345 (e, t)
1346 }
1347
add_isle_constraints( term: &isle::sema::Term, tree: &mut RuleParseTree, annotation_env: &AnnotationEnv, annotation_info: &mut AnnotationTypeInfo, annotation: annotation_ir::TermSignature, )1348 fn add_isle_constraints(
1349 term: &isle::sema::Term,
1350 tree: &mut RuleParseTree,
1351 annotation_env: &AnnotationEnv,
1352 annotation_info: &mut AnnotationTypeInfo,
1353 annotation: annotation_ir::TermSignature,
1354 ) {
1355 let mut annotation_vars = vec![];
1356 for a in annotation.args {
1357 annotation_vars.push(a.name);
1358 }
1359 annotation_vars.push(annotation.ret.name);
1360
1361 let mut isle_types = vec![];
1362 for arg_ty in term.arg_tys.iter() {
1363 isle_types.push(*arg_ty);
1364 }
1365 isle_types.push(term.ret_ty);
1366 assert_eq!(annotation_vars.len(), isle_types.len());
1367
1368 for (isle_type_id, annotation_var) in isle_types.iter().zip(annotation_vars) {
1369 // in case the var was not in the annotation
1370 if !annotation_info
1371 .var_to_type_var
1372 .contains_key(&annotation_var)
1373 {
1374 let type_var = tree.next_type_var;
1375 tree.next_type_var += 1;
1376
1377 annotation_info
1378 .var_to_type_var
1379 .insert(annotation_var.clone(), type_var);
1380 }
1381
1382 if let Some(ir_type) = annotation_env.model_map.get(isle_type_id) {
1383 let type_var = annotation_info.var_to_type_var[&annotation_var];
1384 match ir_type {
1385 annotation_ir::Type::BitVector => tree
1386 .bv_constraints
1387 .insert(TypeExpr::Concrete(type_var, ir_type.clone())),
1388 _ => tree
1389 .concrete_constraints
1390 .insert(TypeExpr::Concrete(type_var, ir_type.clone())),
1391 };
1392 }
1393 }
1394 }
1395
add_rule_constraints( tree: &mut RuleParseTree, curr: &mut TypeVarNode, termenv: &TermEnv, typeenv: &TypeEnv, annotation_env: &AnnotationEnv, annotation_infos: &mut Vec<AnnotationTypeInfo>, rhs: bool, ) -> Option<veri_ir::Expr>1396 fn add_rule_constraints(
1397 tree: &mut RuleParseTree,
1398 curr: &mut TypeVarNode,
1399 termenv: &TermEnv,
1400 typeenv: &TypeEnv,
1401 annotation_env: &AnnotationEnv,
1402 annotation_infos: &mut Vec<AnnotationTypeInfo>,
1403 rhs: bool,
1404 ) -> Option<veri_ir::Expr> {
1405 // Only relate args to annotations for terms. For leaves, return immediately.
1406 // For recursive definitions without annotations (like And and Let), recur.
1407 let mut children = vec![];
1408 for child in &mut curr.children {
1409 if let Some(e) = add_rule_constraints(
1410 tree,
1411 child,
1412 termenv,
1413 typeenv,
1414 annotation_env,
1415 annotation_infos,
1416 rhs,
1417 ) {
1418 children.push(e);
1419 } else {
1420 return None;
1421 }
1422 }
1423 let e = match &curr.construct {
1424 TypeVarConstruct::Var => {
1425 tree.quantified_vars
1426 .insert((curr.ident.clone(), curr.type_var));
1427 tree.free_vars.insert((curr.ident.clone(), curr.type_var));
1428 Some(veri_ir::Expr::Terminal(veri_ir::Terminal::Var(
1429 curr.ident.clone(),
1430 )))
1431 }
1432 TypeVarConstruct::BindPattern => {
1433 assert_eq!(children.len(), 2);
1434 let eq = veri_ir::Expr::Binary(
1435 veri_ir::BinaryOp::Eq,
1436 Box::new(children[0].clone()),
1437 Box::new(children[1].clone()),
1438 );
1439 if rhs {
1440 tree.rhs_assumptions.push(eq);
1441 } else {
1442 tree.lhs_assumptions.push(eq);
1443 }
1444 Some(children[0].clone())
1445 }
1446 TypeVarConstruct::Wildcard(i) => {
1447 Some(veri_ir::Expr::Terminal(veri_ir::Terminal::Wildcard(*i)))
1448 }
1449 TypeVarConstruct::Const(i) => {
1450 // If constant is known, add the value to the tree. Useful for
1451 // capturing isleTypes
1452 tree.type_var_to_val_map.insert(curr.type_var, *i);
1453
1454 Some(veri_ir::Expr::Terminal(veri_ir::Terminal::Const(
1455 *i,
1456 curr.type_var,
1457 )))
1458 }
1459 TypeVarConstruct::Bool(val) => {
1460 // If constant is known, add the value to the tree. Useful for
1461 // capturing isleTypes
1462 tree.type_var_to_val_map
1463 .insert(curr.type_var, i128::from(*val));
1464
1465 Some(veri_ir::Expr::Terminal(veri_ir::Terminal::Const(
1466 i128::from(*val),
1467 curr.type_var,
1468 )))
1469 }
1470 TypeVarConstruct::And => {
1471 tree.quantified_vars
1472 .insert((curr.ident.clone(), curr.type_var));
1473 let first = &children[0];
1474 for (i, e) in children.iter().enumerate() {
1475 if i != 0 {
1476 let eq = veri_ir::Expr::Binary(
1477 veri_ir::BinaryOp::Eq,
1478 Box::new(first.clone()),
1479 Box::new(e.clone()),
1480 );
1481 if rhs {
1482 tree.rhs_assumptions.push(eq);
1483 } else {
1484 tree.lhs_assumptions.push(eq);
1485 }
1486 }
1487 }
1488 Some(first.to_owned())
1489 }
1490 TypeVarConstruct::Let(bound) => {
1491 tree.quantified_vars
1492 .insert((curr.ident.clone(), curr.type_var));
1493 for (e, s) in children.iter().zip(bound) {
1494 let eq = veri_ir::Expr::Binary(
1495 veri_ir::BinaryOp::Eq,
1496 Box::new(veri_ir::Expr::Terminal(veri_ir::Terminal::Var(
1497 s.to_owned(),
1498 ))),
1499 Box::new(e.to_owned()),
1500 );
1501 if rhs {
1502 tree.rhs_assumptions.push(eq);
1503 } else {
1504 tree.lhs_assumptions.push(eq);
1505 }
1506 }
1507 children.last().cloned()
1508 }
1509 TypeVarConstruct::Term(term_id) => {
1510 let term = &termenv.terms[term_id.index()];
1511 let term_name = typeenv.syms[term.name.index()].clone();
1512
1513 // Print term for debugging
1514 log::trace!(" {term_name}");
1515
1516 tree.quantified_vars
1517 .insert((curr.ident.clone(), curr.type_var));
1518 let a = annotation_env.get_annotation_for_term(term_id);
1519 if a.is_none() {
1520 log::error!("\nSkipping rule with unannotated term: {term_name}");
1521 return None;
1522 }
1523 let annotation = a.unwrap();
1524
1525 // Test code only: support providing concrete inputs
1526 if let Some(concrete) = &tree.concrete {
1527 if concrete.termname == term_name {
1528 for (child, node, input) in
1529 izip!(&children, curr.children.iter(), &concrete.args)
1530 {
1531 let type_var = tree.next_type_var;
1532 tree.next_type_var += 1;
1533 let lit = veri_ir::Expr::Terminal(veri_ir::Terminal::Literal(
1534 input.literal.clone(),
1535 type_var,
1536 ));
1537 tree.var_constraints
1538 .insert(TypeExpr::Variable(node.type_var, type_var));
1539 tree.ty_vars.insert(lit.clone(), type_var);
1540 let eq = veri_ir::Expr::Binary(
1541 veri_ir::BinaryOp::Eq,
1542 Box::new(child.clone()),
1543 Box::new(lit),
1544 );
1545 curr.assertions.push(eq.clone());
1546 if rhs {
1547 tree.rhs_assumptions.push(eq);
1548 } else {
1549 tree.lhs_assumptions.push(eq);
1550 }
1551 }
1552 }
1553 }
1554
1555 // use a fresh mapping for each term
1556 // keep the same mapping between assertions in the same annotation
1557 let mut annotation_info = AnnotationTypeInfo {
1558 term: curr.ident.clone(),
1559 var_to_type_var: HashMap::new(),
1560 };
1561 for arg in &annotation.sig.args {
1562 annotation_info
1563 .var_to_type_var
1564 .insert(arg.name.clone(), tree.next_type_var);
1565 tree.next_type_var += 1;
1566 }
1567 annotation_info
1568 .var_to_type_var
1569 .insert(annotation.sig.ret.name.clone(), tree.next_type_var);
1570 tree.next_type_var += 1;
1571
1572 for expr in annotation.assumptions {
1573 let (typed_expr, _) = add_annotation_constraints(*expr, tree, &mut annotation_info);
1574 curr.assertions.push(typed_expr.clone());
1575 if rhs {
1576 tree.rhs_assumptions.push(typed_expr);
1577 } else {
1578 tree.lhs_assumptions.push(typed_expr);
1579 }
1580 add_isle_constraints(
1581 term,
1582 tree,
1583 annotation_env,
1584 &mut annotation_info,
1585 annotation.sig.clone(),
1586 );
1587 }
1588 // For assertions, global assume if not RHS, otherwise assert
1589 for expr in annotation.assertions {
1590 let (typed_expr, _) = add_annotation_constraints(*expr, tree, &mut annotation_info);
1591 curr.assertions.push(typed_expr.clone());
1592 add_isle_constraints(
1593 term,
1594 tree,
1595 annotation_env,
1596 &mut annotation_info,
1597 annotation.sig.clone(),
1598 );
1599 if rhs {
1600 tree.rhs_assertions.push(typed_expr);
1601 } else {
1602 tree.lhs_assumptions.push(typed_expr);
1603 }
1604 }
1605
1606 // set args in rule equal to args in annotation
1607 for (child, arg) in curr.children.iter().zip(&annotation.sig.args) {
1608 let rule_type_var = child.type_var;
1609 if !annotation_info.var_to_type_var.contains_key(&arg.name) {
1610 continue;
1611 }
1612 let annotation_type_var = annotation_info.var_to_type_var[&arg.name];
1613
1614 // essentially constant propagate: if we know the value from the rule arg being
1615 // provided as a literal, propagate this to the annotation.
1616 if let Some(c) = tree.type_var_to_val_map.get(&rule_type_var) {
1617 tree.type_var_to_val_map.insert(annotation_type_var, *c);
1618 }
1619 tree.var_constraints
1620 .insert(TypeExpr::Variable(rule_type_var, annotation_type_var));
1621 }
1622
1623 for (child, arg) in children.iter().zip(&annotation.sig.args) {
1624 let annotation_type_var = annotation_info.var_to_type_var[&arg.name];
1625 let arg_name = format!(
1626 "{}__{}__{}",
1627 annotation_info.term, arg.name, annotation_type_var
1628 );
1629 tree.quantified_vars
1630 .insert((arg_name.clone(), annotation_type_var));
1631 let eq = veri_ir::Expr::Binary(
1632 veri_ir::BinaryOp::Eq,
1633 Box::new(child.clone()),
1634 Box::new(veri_ir::Expr::Terminal(veri_ir::Terminal::Var(arg_name))),
1635 );
1636 if rhs {
1637 tree.rhs_assumptions.push(eq);
1638 } else {
1639 tree.lhs_assumptions.push(eq);
1640 }
1641 }
1642 // set term ret var equal to annotation ret var
1643 let ret_var = annotation_info.var_to_type_var[&annotation.sig.ret.name];
1644 tree.var_constraints
1645 .insert(TypeExpr::Variable(curr.type_var, ret_var));
1646 let ret_name = format!(
1647 "{}__{}__{}",
1648 annotation_info.term, annotation.sig.ret.name, ret_var
1649 );
1650 tree.quantified_vars.insert((ret_name.clone(), ret_var));
1651 let eq = veri_ir::Expr::Binary(
1652 veri_ir::BinaryOp::Eq,
1653 Box::new(veri_ir::Expr::Terminal(veri_ir::Terminal::Var(
1654 curr.ident.clone(),
1655 ))),
1656 Box::new(veri_ir::Expr::Terminal(veri_ir::Terminal::Var(ret_name))),
1657 );
1658 if rhs {
1659 tree.rhs_assumptions.push(eq);
1660 } else {
1661 tree.lhs_assumptions.push(eq);
1662 }
1663
1664 annotation_infos.push(annotation_info);
1665 Some(veri_ir::Expr::Terminal(veri_ir::Terminal::Var(
1666 curr.ident.clone(),
1667 )))
1668 }
1669 };
1670 if let Some(e) = e {
1671 tree.ty_vars.insert(e.clone(), curr.type_var);
1672 Some(e)
1673 } else {
1674 None
1675 }
1676 }
1677
1678 // Solve constraints as follows:
1679 // - process concrete constraints first
1680 // - then process variable constraints
1681 // - constraints involving bv without widths are last priority
1682 //
1683 // for example:
1684 // t2 = bv16
1685 // t3 = bv8
1686 //
1687 // t5 = t4
1688 // t6 = t1
1689 // t3 = t4
1690 // t1 = t2
1691 // t7 = t8
1692 //
1693 // t4 = bv
1694 // t1 = bv
1695 // t7 = bv
1696 //
1697 // would result in:
1698 // bv16 -> t2, t6, t1
1699 // bv8 -> t3, t5, t4
1700 // poly(0) -> t5, t4 (intermediate group that gets removed)
1701 // poly(1) -> t6, t1 (intermediate group that gets removed)
1702 // poly(2) -> t7, t8 (intermediate group that gets removed)
1703 // bv -> t7, t8
1704
1705 // TODO: clean up
solve_constraints( concrete: HashSet<TypeExpr>, var: HashSet<TypeExpr>, bv: HashSet<TypeExpr>, vals: &mut HashMap<u32, i128>, ty_vars: Option<&HashMap<veri_ir::Expr, u32>>, ) -> (HashMap<u32, annotation_ir::Type>, HashMap<u32, u32>)1706 fn solve_constraints(
1707 concrete: HashSet<TypeExpr>,
1708 var: HashSet<TypeExpr>,
1709 bv: HashSet<TypeExpr>,
1710 vals: &mut HashMap<u32, i128>,
1711 ty_vars: Option<&HashMap<veri_ir::Expr, u32>>,
1712 ) -> (HashMap<u32, annotation_ir::Type>, HashMap<u32, u32>) {
1713 // maintain a union find that maps types to sets of type vars that have that type
1714 let mut union_find = HashMap::new();
1715 let mut poly = 0;
1716
1717 let mut iterate = || {
1718 // initialize union find with groups corresponding to concrete constraints
1719 for c in &concrete {
1720 match c {
1721 TypeExpr::Concrete(v, t) => {
1722 if !union_find.contains_key(t) {
1723 union_find.insert(t.clone(), HashSet::new());
1724 }
1725 if let Some(group) = union_find.get_mut(t) {
1726 group.insert(*v);
1727 }
1728 }
1729 TypeExpr::WidthInt(v, w) => {
1730 if let Some(c) = vals.get(w) {
1731 let width: usize = (*c).try_into().unwrap();
1732 let ty = annotation_ir::Type::BitVectorWithWidth(width);
1733 if !union_find.contains_key(&ty) {
1734 union_find.insert(ty.clone(), HashSet::new());
1735 }
1736 if let Some(group) = union_find.get_mut(&ty) {
1737 group.insert(*v);
1738 }
1739 }
1740 }
1741 _ => panic!("Non-concrete constraint found in concrete constraints: {c:#?}"),
1742 };
1743 }
1744
1745 // process variable constraints as follows:
1746 // if t1 = t2 and only t1 has been typed, add t2 to the same set as t1
1747 // if t1 = t2 and only t2 has been typed, add t1 to the same set t2
1748 // if t1 = t2 and neither has been typed, create a new poly type and add both to the set
1749 // if t1 = t2 and both have been typed, union appropriately
1750 for v in &var {
1751 match v {
1752 TypeExpr::Variable(v1, v2) => {
1753 let t1 = get_var_type(*v1, &union_find);
1754 let t2 = get_var_type(*v2, &union_find);
1755
1756 match (t1, t2) {
1757 (Some(x), Some(y)) => {
1758 match (x.is_poly(), y.is_poly()) {
1759 (false, false) => {
1760 if x != y {
1761 let e1 = ty_vars.unwrap().iter().find_map(|(k, &v)| {
1762 if v == *v1 {
1763 Some(k)
1764 } else {
1765 None
1766 }
1767 });
1768 let e2 = ty_vars.unwrap().iter().find_map(|(k, &v)| {
1769 if v == *v2 {
1770 Some(k)
1771 } else {
1772 None
1773 }
1774 });
1775 match (e1, e2) {
1776 (Some(e1), Some(e2)) =>
1777 panic!(
1778 "type conflict\n\t{e1}\nhas type\n\t{x}\nbut\n\t{e2}\nhas type\n\t{y}"
1779 ),
1780 _ => continue,
1781 }
1782 }
1783 }
1784 // union t1 and t2, keeping t2 as the leader
1785 (true, false) => {
1786 let g1 =
1787 union_find.remove(&x).expect("expected key in union find");
1788 let g2 =
1789 union_find.get_mut(&y).expect("expected key in union find");
1790 g2.extend(g1.iter());
1791 }
1792 // union t1 and t2, keeping t1 as the leader
1793 (_, true) => {
1794 // guard against the case where x and y have the same poly type
1795 // so we remove the key and can't find it in the next line
1796 if x != y {
1797 let g2 = union_find
1798 .remove(&y)
1799 .expect("expected key in union find");
1800 let g1 = union_find
1801 .get_mut(&x)
1802 .expect("expected key in union find");
1803 g1.extend(g2.iter());
1804 }
1805 }
1806 };
1807 }
1808 (Some(x), None) => {
1809 if let Some(group) = union_find.get_mut(&x) {
1810 group.insert(*v2);
1811 }
1812 }
1813 (None, Some(x)) => {
1814 if let Some(group) = union_find.get_mut(&x) {
1815 group.insert(*v1);
1816 }
1817 }
1818 (None, None) => {
1819 let t = annotation_ir::Type::Poly(poly);
1820 union_find.insert(t.clone(), HashSet::new());
1821 if let Some(group) = union_find.get_mut(&t) {
1822 group.insert(*v1);
1823 group.insert(*v2);
1824 }
1825 poly += 1;
1826 }
1827 }
1828 }
1829 _ => panic!("Non-variable constraint found in var constraints: {v:#?}"),
1830 }
1831 }
1832
1833 for b in &bv {
1834 match b {
1835 TypeExpr::Concrete(v, ref t) => {
1836 match t {
1837 annotation_ir::Type::BitVector => {
1838 // if there's a bv constraint and the var has already
1839 // been typed (with a width), ignore the constraint
1840 if let Some(var_type) = get_var_type_concrete(*v, &union_find) {
1841 match var_type {
1842 annotation_ir::Type::BitVectorWithWidth(_) => {
1843 continue;
1844 }
1845 annotation_ir::Type::BitVectorUnknown(_) => {
1846 continue;
1847 }
1848 _ => {
1849 let e = ty_vars
1850 .unwrap()
1851 .iter()
1852 .find_map(
1853 |(k, &u)| if u == *v { Some(k) } else { None },
1854 )
1855 .unwrap();
1856 panic!("Var was already typed as {var_type:#?} but currently processing constraint: {b:#?}\n{e:?}")
1857 }
1858 }
1859
1860 // otherwise add it to a generic bv bucket
1861 } else {
1862 // if !union_find.contains_key(t) {
1863 // union_find.insert(t.clone(), HashSet::new());
1864 // }
1865 // if let Some(group) = union_find.get_mut(t) {
1866 // group.insert(v);
1867 // }
1868 let unknown_by_tyvar = annotation_ir::Type::BitVectorUnknown(*v);
1869 let mut set = HashSet::new();
1870 set.insert(*v);
1871 union_find.insert(unknown_by_tyvar.clone(), set);
1872
1873 // if this type var also has a polymorphic type, union
1874 if let Some(var_type) = get_var_type_poly(*v, &union_find) {
1875 let poly_bucket = union_find
1876 .remove(&var_type)
1877 .expect("expected key in union find");
1878 let bv_bucket = union_find
1879 .get_mut(&unknown_by_tyvar)
1880 .expect("expected key in union find");
1881 bv_bucket.extend(poly_bucket.iter());
1882 }
1883 }
1884 }
1885 _ => panic!("Non-bv constraint found in bv constraints: {b:#?}"),
1886 }
1887 }
1888 TypeExpr::Variable(_, _) => {
1889 panic!("Non-bv constraint found in bv constraints: {b:#?}")
1890 }
1891 TypeExpr::WidthInt(_, _) => {
1892 panic!("Non-bv constraint found in bv constraints: {b:#?}")
1893 }
1894 }
1895 }
1896 for c in &concrete {
1897 if let TypeExpr::WidthInt(v, w) = c {
1898 if let Some(annotation_ir::Type::BitVectorWithWidth(width)) =
1899 get_var_type_concrete(*v, &union_find)
1900 {
1901 vals.insert(*w, width as i128);
1902 }
1903 }
1904 }
1905 };
1906
1907 iterate();
1908
1909 let mut result = HashMap::new();
1910 let mut bv_unknown_width_sets = HashMap::new();
1911 let mut bv_unknown_width_idx = 0u32;
1912 for (t, vars) in union_find {
1913 for var in &vars {
1914 result.insert(*var, t.clone());
1915 }
1916 if matches!(t, annotation_ir::Type::BitVectorUnknown(..)) {
1917 for var in &vars {
1918 bv_unknown_width_sets.insert(*var, bv_unknown_width_idx);
1919 }
1920 bv_unknown_width_idx += 1;
1921 }
1922 }
1923 (result, bv_unknown_width_sets)
1924 }
1925
1926 // if the union find already contains the type var, return its type
1927 // otherwise return None
get_var_type( t: u32, u: &HashMap<annotation_ir::Type, HashSet<u32>>, ) -> Option<annotation_ir::Type>1928 fn get_var_type(
1929 t: u32,
1930 u: &HashMap<annotation_ir::Type, HashSet<u32>>,
1931 ) -> Option<annotation_ir::Type> {
1932 for (ty, vars) in u {
1933 if vars.contains(&t) {
1934 return Some(ty.clone());
1935 }
1936 }
1937 None
1938 }
1939
1940 // If the union find contains the type var and it has a non-polymorphic, specific type
1941 // return it. Otherwise return None.
get_var_type_concrete( t: u32, u: &HashMap<annotation_ir::Type, HashSet<u32>>, ) -> Option<annotation_ir::Type>1942 fn get_var_type_concrete(
1943 t: u32,
1944 u: &HashMap<annotation_ir::Type, HashSet<u32>>,
1945 ) -> Option<annotation_ir::Type> {
1946 for (ty, vars) in u {
1947 match ty {
1948 annotation_ir::Type::Poly(_) | annotation_ir::Type::BitVector => continue,
1949 _ => {
1950 if vars.contains(&t) {
1951 return Some(ty.clone());
1952 }
1953 }
1954 }
1955 }
1956 None
1957 }
1958
1959 // If the union find contains the type var and it has a polymorphic type,
1960 // return the polymorphic type. Otherwise return None.
get_var_type_poly( t: u32, u: &HashMap<annotation_ir::Type, HashSet<u32>>, ) -> Option<annotation_ir::Type>1961 fn get_var_type_poly(
1962 t: u32,
1963 u: &HashMap<annotation_ir::Type, HashSet<u32>>,
1964 ) -> Option<annotation_ir::Type> {
1965 for (ty, vars) in u {
1966 match ty {
1967 annotation_ir::Type::Poly(_) => {
1968 if vars.contains(&t) {
1969 return Some(ty.clone());
1970 }
1971 }
1972 _ => continue,
1973 }
1974 }
1975 None
1976 }
1977
annotation_type_for_vir_type(ty: &Type) -> annotation_ir::Type1978 fn annotation_type_for_vir_type(ty: &Type) -> annotation_ir::Type {
1979 match ty {
1980 Type::BitVector(Some(x)) => annotation_ir::Type::BitVectorWithWidth(*x),
1981 Type::BitVector(None) => annotation_ir::Type::BitVector,
1982 Type::Bool => annotation_ir::Type::Bool,
1983 Type::Int => annotation_ir::Type::Int,
1984 Type::Unit => annotation_ir::Type::Unit,
1985 }
1986 }
1987
create_parse_tree_pattern( rule: &isle::sema::Rule, pattern: &isle::sema::Pattern, tree: &mut RuleParseTree, typeenv: &TypeEnv, termenv: &TermEnv, term: &String, types: &TermSignature, ) -> TypeVarNode1988 fn create_parse_tree_pattern(
1989 rule: &isle::sema::Rule,
1990 pattern: &isle::sema::Pattern,
1991 tree: &mut RuleParseTree,
1992 typeenv: &TypeEnv,
1993 termenv: &TermEnv,
1994 term: &String,
1995 types: &TermSignature,
1996 ) -> TypeVarNode {
1997 match pattern {
1998 isle::sema::Pattern::Term(_, term_id, args) => {
1999 let sym = termenv.terms[term_id.index()].name;
2000 let name = typeenv.syms[sym.index()].clone();
2001
2002 let mut assertions = vec![];
2003 // process children first
2004 let mut children = vec![];
2005 for (i, arg) in args.iter().enumerate() {
2006 let child =
2007 create_parse_tree_pattern(rule, arg, tree, typeenv, termenv, term, types);
2008
2009 // Our specified input term, use external types
2010 if name.eq(term) {
2011 tree.concrete_constraints.insert(TypeExpr::Concrete(
2012 child.type_var,
2013 annotation_type_for_vir_type(&types.args[i]),
2014 ));
2015
2016 // If this is a bitvector, mark the name for the assumption feasibility check
2017 if let Type::BitVector(Some(w)) = &types.args[i] {
2018 tree.term_input_bvs.push(child.ident.clone());
2019
2020 // Hack: width matching
2021 let lit = veri_ir::Expr::Terminal(veri_ir::Terminal::Const(*w as i128, 0));
2022 let eq = veri_ir::Expr::Binary(
2023 veri_ir::BinaryOp::Eq,
2024 Box::new(veri_ir::Expr::WidthOf(Box::new(veri_ir::Expr::Terminal(
2025 veri_ir::Terminal::Var(child.ident.clone()),
2026 )))),
2027 Box::new(lit),
2028 );
2029 assertions.push(eq);
2030 }
2031 tree.term_args.push(child.ident.clone())
2032 }
2033 children.push(child);
2034 }
2035 let type_var = tree.next_type_var;
2036 tree.next_type_var += 1;
2037
2038 if name.eq(term) {
2039 tree.concrete_constraints.insert(TypeExpr::Concrete(
2040 type_var,
2041 annotation_type_for_vir_type(&types.ret),
2042 ));
2043 // Hack: width matching
2044 if let Type::BitVector(Some(w)) = &types.ret {
2045 let lit = veri_ir::Expr::Terminal(veri_ir::Terminal::Const(*w as i128, 0));
2046 let eq = veri_ir::Expr::Binary(
2047 veri_ir::BinaryOp::Eq,
2048 Box::new(veri_ir::Expr::WidthOf(Box::new(veri_ir::Expr::Terminal(
2049 veri_ir::Terminal::Var(format!("{name}__{type_var}")),
2050 )))),
2051 Box::new(lit),
2052 );
2053 assertions.push(eq);
2054 }
2055 }
2056
2057 TypeVarNode {
2058 ident: format!("{name}__{type_var}"),
2059 construct: TypeVarConstruct::Term(*term_id),
2060 type_var,
2061 children,
2062 assertions,
2063 }
2064 }
2065 isle::sema::Pattern::Var(_, var_id) => {
2066 let sym = rule.vars[var_id.index()].name;
2067 let ident = typeenv.syms[sym.index()].clone();
2068
2069 let type_var = tree
2070 .varid_to_type_var_map
2071 .entry(*var_id)
2072 .or_insert(tree.next_type_var);
2073 if *type_var == tree.next_type_var {
2074 tree.next_type_var += 1;
2075 }
2076 let ident = format!("{}__clif{}__{}", ident, var_id.index(), *type_var);
2077 // this is a base case so there are no children
2078 TypeVarNode {
2079 ident,
2080 construct: TypeVarConstruct::Var,
2081 type_var: *type_var,
2082 children: vec![],
2083 assertions: vec![],
2084 }
2085 }
2086 isle::sema::Pattern::BindPattern(_, var_id, subpat) => {
2087 let sym = rule.vars[var_id.index()].name;
2088
2089 let type_var = *tree
2090 .varid_to_type_var_map
2091 .entry(*var_id)
2092 .or_insert(tree.next_type_var);
2093 if type_var == tree.next_type_var {
2094 tree.next_type_var += 1;
2095 }
2096
2097 let ident = format!(
2098 "{}__clif{}__{}",
2099 typeenv.syms[sym.index()],
2100 var_id.index(),
2101 type_var
2102 );
2103
2104 // this is a base case so there are no children
2105 let var_node = TypeVarNode {
2106 ident: ident.clone(),
2107 construct: TypeVarConstruct::Var,
2108 type_var,
2109 children: vec![],
2110 assertions: vec![],
2111 };
2112
2113 let subpat_node =
2114 create_parse_tree_pattern(rule, subpat, tree, typeenv, termenv, term, types);
2115
2116 let bind_type_var = tree.next_type_var;
2117 tree.next_type_var += 1;
2118
2119 tree.var_constraints
2120 .insert(TypeExpr::Variable(type_var, subpat_node.type_var));
2121 tree.var_constraints
2122 .insert(TypeExpr::Variable(bind_type_var, type_var));
2123 tree.var_constraints
2124 .insert(TypeExpr::Variable(bind_type_var, subpat_node.type_var));
2125
2126 TypeVarNode {
2127 ident,
2128 construct: TypeVarConstruct::BindPattern,
2129 type_var,
2130 children: vec![var_node, subpat_node],
2131 assertions: vec![],
2132 }
2133 }
2134 isle::sema::Pattern::Wildcard(_) => {
2135 let type_var = tree.next_type_var;
2136 tree.next_type_var += 1;
2137 TypeVarNode {
2138 ident: format!("wildcard__{type_var}"),
2139 construct: TypeVarConstruct::Wildcard(type_var),
2140 type_var,
2141 children: vec![],
2142 assertions: vec![],
2143 }
2144 }
2145 isle::sema::Pattern::ConstPrim(_, sym) => {
2146 let type_var = tree.next_type_var;
2147 tree.next_type_var += 1;
2148 let name = typeenv.syms[sym.index()].clone();
2149 let val = match name.as_str() {
2150 "I64" => 64,
2151 "I32" => 32,
2152 "I16" => 16,
2153 "I8" => 8,
2154 "true" => 1,
2155 "false" => 0,
2156 // Not currently used, but parsed
2157 "I128" => 16,
2158 _ => todo!("{:?}", &name),
2159 };
2160 let name = format!("{name}__{type_var}");
2161
2162 TypeVarNode {
2163 ident: name,
2164 construct: TypeVarConstruct::Const(val),
2165 type_var,
2166 children: vec![],
2167 assertions: vec![],
2168 }
2169 }
2170 isle::sema::Pattern::ConstBool(_, val) => {
2171 let type_var = tree.next_type_var;
2172 tree.next_type_var += 1;
2173 let name = format!("{val}__{type_var}");
2174 TypeVarNode {
2175 ident: name,
2176 construct: TypeVarConstruct::Bool(*val),
2177 type_var,
2178 children: vec![],
2179 assertions: vec![],
2180 }
2181 }
2182 isle::sema::Pattern::ConstInt(_, num) => {
2183 let type_var = tree.next_type_var;
2184 tree.next_type_var += 1;
2185 let name = format!("{num}__{type_var}");
2186 TypeVarNode {
2187 ident: name,
2188 construct: TypeVarConstruct::Const(*num),
2189 type_var,
2190 children: vec![],
2191 assertions: vec![],
2192 }
2193 }
2194 isle::sema::Pattern::And(_, subpats) => {
2195 let mut children = vec![];
2196 let mut ty_vars = vec![];
2197 for p in subpats {
2198 let child = create_parse_tree_pattern(rule, p, tree, typeenv, termenv, term, types);
2199 ty_vars.push(child.type_var);
2200 children.push(child);
2201 }
2202 let type_var = tree.next_type_var;
2203 tree.next_type_var += 1;
2204
2205 // Assert all sub type constraints are equivalent to the first subexpression
2206 let first = ty_vars[0];
2207 for e in &ty_vars[1..] {
2208 tree.var_constraints
2209 .insert(TypeExpr::Variable(first, e.to_owned()));
2210 }
2211
2212 TypeVarNode {
2213 ident: String::from("and"),
2214 construct: TypeVarConstruct::And,
2215 type_var,
2216 children,
2217 assertions: vec![],
2218 }
2219 }
2220 }
2221 }
2222
create_parse_tree_expr( rule: &isle::sema::Rule, expr: &isle::sema::Expr, tree: &mut RuleParseTree, typeenv: &TypeEnv, termenv: &TermEnv, ) -> TypeVarNode2223 fn create_parse_tree_expr(
2224 rule: &isle::sema::Rule,
2225 expr: &isle::sema::Expr,
2226 tree: &mut RuleParseTree,
2227 typeenv: &TypeEnv,
2228 termenv: &TermEnv,
2229 ) -> TypeVarNode {
2230 match expr {
2231 isle::sema::Expr::Term(_, term_id, args) => {
2232 let sym = termenv.terms[term_id.index()].name;
2233 let name = typeenv.syms[sym.index()].clone();
2234
2235 // process children first
2236 let mut children = vec![];
2237 for arg in args {
2238 let child = create_parse_tree_expr(rule, arg, tree, typeenv, termenv);
2239 children.push(child);
2240 }
2241 let type_var = tree.next_type_var;
2242 tree.next_type_var += 1;
2243
2244 TypeVarNode {
2245 ident: format!("{name}__{type_var}"),
2246 construct: TypeVarConstruct::Term(*term_id),
2247 type_var,
2248 children,
2249 assertions: vec![],
2250 }
2251 }
2252 isle::sema::Expr::Var(_, var_id) => {
2253 let mut ident = var_id.0.to_string();
2254 if var_id.index() < rule.vars.len() {
2255 let sym = rule.vars[var_id.index()].name;
2256 ident.clone_from(&typeenv.syms[sym.index()])
2257 } else {
2258 println!("var {} not found, using var id instead", var_id.0);
2259 ident = format!("v{ident}");
2260 }
2261
2262 let type_var = tree
2263 .varid_to_type_var_map
2264 .entry(*var_id)
2265 .or_insert(tree.next_type_var);
2266 if *type_var == tree.next_type_var {
2267 tree.next_type_var += 1;
2268 }
2269 let ident = format!("{}__clif{}__{}", ident, var_id.index(), *type_var);
2270 // this is a base case so there are no children
2271 TypeVarNode {
2272 ident,
2273 construct: TypeVarConstruct::Var,
2274 type_var: *type_var,
2275 children: vec![],
2276 assertions: vec![],
2277 }
2278 }
2279 isle::sema::Expr::ConstPrim(_, sym) => {
2280 let type_var = tree.next_type_var;
2281 tree.next_type_var += 1;
2282 let name = typeenv.syms[sym.index()].clone();
2283 let val = match name.as_str() {
2284 "I8" => 8,
2285 "I16" => 16,
2286 "I64" => 64,
2287 "I32" => 32,
2288 "false" => 0,
2289 "true" => 1,
2290 _ => todo!("{:?}", &name),
2291 };
2292 let name = format!("{name}__{type_var}");
2293 TypeVarNode {
2294 ident: name,
2295 construct: TypeVarConstruct::Const(val),
2296 type_var,
2297 children: vec![],
2298 assertions: vec![],
2299 }
2300 }
2301 isle::sema::Expr::ConstBool(_, val) => {
2302 let type_var = tree.next_type_var;
2303 tree.next_type_var += 1;
2304 let name = format!("{val}__{type_var}");
2305 TypeVarNode {
2306 ident: name,
2307 construct: TypeVarConstruct::Bool(*val),
2308 type_var,
2309 children: vec![],
2310 assertions: vec![],
2311 }
2312 }
2313 isle::sema::Expr::ConstInt(_, num) => {
2314 let type_var = tree.next_type_var;
2315 tree.next_type_var += 1;
2316 let name = format!("{num}__{type_var}");
2317 TypeVarNode {
2318 ident: name,
2319 construct: TypeVarConstruct::Const(*num),
2320 type_var,
2321 children: vec![],
2322 assertions: vec![],
2323 }
2324 }
2325 isle::sema::Expr::Let { bindings, body, .. } => {
2326 let mut children = vec![];
2327 let mut bound = vec![];
2328 for (varid, _, expr) in bindings {
2329 let sym = rule.vars[varid.index()].name;
2330 let var = typeenv.syms[sym.index()].clone();
2331 let subpat_node = create_parse_tree_expr(rule, expr, tree, typeenv, termenv);
2332
2333 let ty_var = tree.next_type_var;
2334 tree.next_type_var += 1;
2335
2336 tree.var_constraints
2337 .insert(TypeExpr::Variable(ty_var, subpat_node.type_var));
2338
2339 tree.varid_to_type_var_map.insert(*varid, ty_var);
2340 children.push(subpat_node);
2341 let ident = format!("{}__clif{}__{}", var, varid.index(), ty_var);
2342 tree.quantified_vars.insert((ident.clone(), ty_var));
2343 bound.push(ident);
2344 }
2345 let body = create_parse_tree_expr(rule, body, tree, typeenv, termenv);
2346 let body_var = body.type_var;
2347 children.push(body);
2348
2349 let type_var = tree.next_type_var;
2350 tree.next_type_var += 1;
2351
2352 let name = format!("let__{type_var}");
2353
2354 // The let should have the same type as the body
2355 tree.var_constraints
2356 .insert(TypeExpr::Variable(type_var, body_var));
2357
2358 TypeVarNode {
2359 ident: name,
2360 construct: TypeVarConstruct::Let(bound),
2361 type_var,
2362 children,
2363 assertions: vec![],
2364 }
2365 }
2366 }
2367 }
2368
2369 // TODO mod tests?
2370 #[test]
test_solve_constraints()2371 fn test_solve_constraints() {
2372 // simple with specific and generic bvs
2373 let concrete = HashSet::from([
2374 TypeExpr::Concrete(2, annotation_ir::Type::BitVectorWithWidth(16)),
2375 TypeExpr::Concrete(3, annotation_ir::Type::BitVectorWithWidth(8)),
2376 ]);
2377 let var = HashSet::from([
2378 TypeExpr::Variable(5, 4),
2379 TypeExpr::Variable(6, 1),
2380 TypeExpr::Variable(3, 4),
2381 TypeExpr::Variable(1, 2),
2382 ]);
2383 let bv = HashSet::from([
2384 TypeExpr::Concrete(1, annotation_ir::Type::BitVector),
2385 TypeExpr::Concrete(4, annotation_ir::Type::BitVector),
2386 ]);
2387 let expected = HashMap::from([
2388 (1, annotation_ir::Type::BitVectorWithWidth(16)),
2389 (2, annotation_ir::Type::BitVectorWithWidth(16)),
2390 (3, annotation_ir::Type::BitVectorWithWidth(8)),
2391 (4, annotation_ir::Type::BitVectorWithWidth(8)),
2392 (5, annotation_ir::Type::BitVectorWithWidth(8)),
2393 (6, annotation_ir::Type::BitVectorWithWidth(16)),
2394 ]);
2395 let (sol, bvsets) = solve_constraints(concrete, var, bv, &mut HashMap::new(), None);
2396 assert_eq!(expected, sol);
2397 assert!(bvsets.is_empty());
2398
2399 // slightly more complicated with specific and generic bvs
2400 let concrete = HashSet::from([
2401 TypeExpr::Concrete(2, annotation_ir::Type::BitVectorWithWidth(16)),
2402 TypeExpr::Concrete(3, annotation_ir::Type::BitVectorWithWidth(8)),
2403 ]);
2404 let var = HashSet::from([
2405 TypeExpr::Variable(5, 4),
2406 TypeExpr::Variable(6, 1),
2407 TypeExpr::Variable(3, 4),
2408 TypeExpr::Variable(1, 2),
2409 TypeExpr::Variable(7, 8),
2410 ]);
2411 let bv = HashSet::from([
2412 TypeExpr::Concrete(1, annotation_ir::Type::BitVector),
2413 TypeExpr::Concrete(4, annotation_ir::Type::BitVector),
2414 TypeExpr::Concrete(7, annotation_ir::Type::BitVector),
2415 ]);
2416 let expected = HashMap::from([
2417 (1, annotation_ir::Type::BitVectorWithWidth(16)),
2418 (2, annotation_ir::Type::BitVectorWithWidth(16)),
2419 (3, annotation_ir::Type::BitVectorWithWidth(8)),
2420 (4, annotation_ir::Type::BitVectorWithWidth(8)),
2421 (5, annotation_ir::Type::BitVectorWithWidth(8)),
2422 (6, annotation_ir::Type::BitVectorWithWidth(16)),
2423 (7, annotation_ir::Type::BitVectorUnknown(7)),
2424 (8, annotation_ir::Type::BitVectorUnknown(7)),
2425 ]);
2426 let expected_bvsets = HashMap::from([(7, 0), (8, 0)]);
2427 let (sol, bvsets) = solve_constraints(concrete, var, bv, &mut HashMap::new(), None);
2428 assert_eq!(expected, sol);
2429 assert_eq!(expected_bvsets, bvsets);
2430 }
2431
2432 #[test]
2433 #[should_panic]
test_solve_constraints_ill_typed()2434 fn test_solve_constraints_ill_typed() {
2435 // ill-typed
2436 let concrete = HashSet::from([
2437 TypeExpr::Concrete(2, annotation_ir::Type::BitVectorWithWidth(16)),
2438 TypeExpr::Concrete(3, annotation_ir::Type::BitVectorWithWidth(8)),
2439 ]);
2440 let var = HashSet::from([
2441 TypeExpr::Variable(5, 4),
2442 TypeExpr::Variable(6, 1),
2443 TypeExpr::Variable(4, 6),
2444 TypeExpr::Variable(3, 4),
2445 TypeExpr::Variable(1, 2),
2446 ]);
2447 let bv = HashSet::from([
2448 TypeExpr::Concrete(1, annotation_ir::Type::BitVector),
2449 TypeExpr::Concrete(4, annotation_ir::Type::BitVector),
2450 ]);
2451 solve_constraints(concrete, var, bv, &mut HashMap::new(), None);
2452 }
2453