Searched refs:BitVector (Results 1 – 8 of 8) sorted by relevance
| /wasmtime-44.0.1/cranelift/isle/veri/veri_engine/src/ |
| H A D | type_inference.rs | 152 annotation_ir::Type::BitVector => veri_ir::Type::BitVector(None), in convert_type()
374 annotation_ir::Type::BitVector => { in add_annotation_constraints()
1385 annotation_ir::Type::BitVector => tree in add_isle_constraints()
1837 annotation_ir::Type::BitVector => { in solve_constraints()
1981 Type::BitVector(None) => annotation_ir::Type::BitVector, in annotation_type_for_vir_type()
2044 if let Type::BitVector(Some(w)) = &types.ret { in create_parse_tree_pattern()
2384 TypeExpr::Concrete(1, annotation_ir::Type::BitVector), in test_solve_constraints()
2385 TypeExpr::Concrete(4, annotation_ir::Type::BitVector), in test_solve_constraints()
2412 TypeExpr::Concrete(1, annotation_ir::Type::BitVector), in test_solve_constraints()
2413 TypeExpr::Concrete(4, annotation_ir::Type::BitVector), in test_solve_constraints()
[all …]
|
| H A D | verify.rs | 39 "I8" => veri_ir::Type::BitVector(Some(8)), in verify_rules()
40 "I16" => veri_ir::Type::BitVector(Some(16)), in verify_rules()
41 "I32" => veri_ir::Type::BitVector(Some(32)), in verify_rules()
42 "I64" => veri_ir::Type::BitVector(Some(64)), in verify_rules()
|
| H A D | solver.rs | 513 Type::BitVector(w) => { in vir_to_smt_ty()
536 Some(Type::BitVector(w)) => *w, in static_width()
558 (Some(Type::BitVector(Some(xw))), Some(Type::BitVector(Some(yw)))) => { in assume_comparable_types()
585 Type::BitVector(w) => { in vir_expr_to_sexp()
786 (Some(Type::BitVector(_)), Some(Type::BitVector(_))) => "bvule", in vir_expr_to_sexp()
791 (Some(Type::BitVector(_)), Some(Type::BitVector(_))) => "bvult", in vir_expr_to_sexp()
986 if matches!(ty, Some(Type::BitVector(_))) { in vir_expr_to_sexp()
992 if matches!(cty, Some(Type::BitVector(_))) { in vir_expr_to_sexp()
1553 if let Type::BitVector(w) = ty { in declare_variables()
1675 if let Type::BitVector(w) = ty { in run_solver()
[all …]
|
| H A D | annotations.rs | 322 ModelType::BitVec(size) => veri_ir::Type::BitVector(*size), in model_type_to_type()
353 ModelType::BitVec(None) => annotation_ir::Type::BitVector, in parse_annotations()
|
| /wasmtime-44.0.1/cranelift/isle/veri/veri_engine/tests/ |
| H A D | veri.rs | 23 ty: veri_ir::Type::BitVector(Some(8)), in test_named_iadd_base_concrete()
27 ty: veri_ir::Type::BitVector(Some(8)), in test_named_iadd_base_concrete()
32 ty: veri_ir::Type::BitVector(Some(8)), in test_named_iadd_base_concrete()
149 ty: veri_ir::Type::BitVector(Some(16)), in test_named_iadd_extend_right_concrete()
170 ty: veri_ir::Type::BitVector(Some(32)), in test_named_iadd_extend_right_concrete()
486 ty: veri_ir::Type::BitVector(Some(8)), in test_named_isub_imm12_concrete()
565 ty: veri_ir::Type::BitVector(Some(64)), in test_named_isub_imm12_neg_concrete32()
593 ty: veri_ir::Type::BitVector(Some(64)), in test_named_isub_imm12_neg_concrete64()
958 ty: veri_ir::Type::BitVector(Some(8)), in test_named_urem_concrete()
1862 ty: veri_ir::Type::BitVector(Some(8)), in test_named_ishl_fits_in_32_concrete()
[all …]
|
| /wasmtime-44.0.1/cranelift/isle/veri/veri_engine/tests/utils/ |
| H A D | mod.rs | 125 Bitwidth::I8 => veri_ir::Type::BitVector(Some(8)), in test_rules_with_term()
126 Bitwidth::I16 => veri_ir::Type::BitVector(Some(16)), in test_rules_with_term()
127 Bitwidth::I32 => veri_ir::Type::BitVector(Some(32)), in test_rules_with_term()
128 Bitwidth::I64 => veri_ir::Type::BitVector(Some(64)), in test_rules_with_term()
|
| /wasmtime-44.0.1/cranelift/isle/veri/veri_ir/src/ |
| H A D | lib.rs | 48 BitVector(Option<usize>), enumerator
68 Type::BitVector(None) => write!(f, "bv"), in fmt()
69 Type::BitVector(Some(s)) => write!(f, "(bv {})", *s), in fmt()
|
| H A D | annotation_ir.rs | 85 BitVector, enumerator
109 Type::BitVector => write!(f, "bv"), in fmt()
|