bitblasting LLVM.Int type: another alternative

[luisacicolini]

This PR contains a second approach to the bitblastability of the LLVM.Int w type, based on this by @georgerennie and @alexkeizer

The idea is to not force a bitvector value via an explicit toIntBv conversion: instead, we introduce a new relation

@[llvm_toBitVec]
def is_eqv_bv (i : Int w) (i_bv : IntBv w) :=
  match i with
  | val v => i_bv.poison = false ∧ i_bv.toBitVec = v
  | poison => i_bv.poison = true

which allows us to say that any poison Int does not really have a value, and a new refinement relation that is bitblastable friendly, allowing us to unfold the refinement relations at the Int level to something bitblastable:

@[bv_normalize, llvm_toBitVec]
theorem isRefinedBy_toBitVec_eq (x y : Int w) :
    (x ⊑ y) ↔
      ∃ (x' : IntBv w) (h : is_eqv_bv x x'),
      ∃ (y' : IntBv w) (h : is_eqv_bv y y'),
        isRefinedBy_toBitVec x' y'

I started building some theory around it, but am not yet sure whether this is going in the right direction (we can not yet use bv_decide because some lemmas are still missing). @georgerennie and @alexkeizer if you could take a look and let me know whether this was the direction you had in mind it would be great :)

I am especially confused by these two relations and their interactions: because is_eqv_bv only appears in a hypothesis in isRefinedBy_toBitVec_eq, it is not used by the simp-set before the bv_decide call and therefore is useless.

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: 2425e5c	Previous: c5ccd9c	Ratio
add-fold-worklist/create	1903000 ns	2579000 ns	0.74
add-fold-worklist/rewrite	3454000 ns	3788000 ns	0.91
add-fold-worklist-local/create	1894000 ns	2307000 ns	0.82
add-fold-worklist-local/rewrite	2863000 ns	3159000 ns	0.91
add-zero-worklist/create	1897000 ns	2479000 ns	0.77
add-zero-worklist/rewrite	2171000 ns	2513000 ns	0.86
add-zero-reuse-worklist/create	1641000 ns	2045000 ns	0.80
add-zero-reuse-worklist/rewrite	1785000 ns	1989000 ns	0.90
mul-two-worklist/create	1937000 ns	2578000 ns	0.75
mul-two-worklist/rewrite	4948000 ns	5362000 ns	0.92
add-fold-forwards/create	1929000 ns	2561000 ns	0.75
add-fold-forwards/rewrite	2777000 ns	3076000 ns	0.90
add-zero-forwards/create	2033000 ns	2522000 ns	0.81
add-zero-forwards/rewrite	1745000 ns	2016000 ns	0.87
add-zero-reuse-forwards/create	1587000 ns	2170000 ns	0.73
add-zero-reuse-forwards/rewrite	1401000 ns	1586000 ns	0.88
mul-two-forwards/create	1982000 ns	2485000 ns	0.80
mul-two-forwards/rewrite	3352000 ns	3715000 ns	0.90
add-zero-reuse-first/create	1601000 ns	2034000 ns	0.79
add-zero-reuse-first/rewrite	9000 ns	8000 ns	1.13
add-zero-lots-of-reuse-first/create	1644000 ns	2214000 ns	0.74
add-zero-lots-of-reuse-first/rewrite	749000 ns	786000 ns	0.95

This comment was automatically generated by workflow using github-action-benchmark.