Arbitrary Bitvector widths

[tiferrei]

Hi there,

Thanks again for this fantastic library! :)

I was doing some optimisations in my encoding by switching to a bit vector encoding of a finite domain. In the process, I hit some assertions about using non-standard bit vector widths (i.e., not 8/32/64).

From my (very poor) understanding of the implementation, is this because these vectors are backed by OCaml ints, of respective sizes? Is there a bigger limitation to supporting arbitrary width bit vectors?

If not, would it be reasonable for me to hack locally a Z.t-backed implementation to get started?

Thanks!

Tiago

[filipeom]

Hi! Thanks for the feedback!

I was doing some optimisations in my encoding by switching to a bit vector encoding of a finite domain. In the process, I hit some assertions about using non-standard bit vector widths (i.e., not 8/32/64).

Do you have some examples you can share with us?

If not, would it be reasonable for me to hack locally a Z.t-backed implementation to get started?

Previously we only supported bitvectors of size 8, 32, and 64. But recently we added a concrete arbitrary width bitvector implementation here: https://github.com/formalsec/smtml/blob/main/src/smtml/bitvector.ml

I think we should have arbitrary model lifting for bitvectors here as well:

smtml/src/smtml/mappings.ml

Lines 834 to 840 in 00590be

	| Ty_bitv 1 ->
	let b = M.Interp.to_bitv v 1 in
	if Z.equal b Z.one then Value.True
	else (
	assert (Z.equal b Z.zero);
	Value.False )
	| Ty_bitv m -> Value.Bitv (Bitvector.make (M.Interp.to_bitv v m) m)

But the operations over bitvectors in the solver I think are still hardcoded over I8s, I32s, and I64s here: https://github.com/formalsec/smtml/blob/main/src/smtml/mappings.ml#L612-L614

Changing this to support arbitrary width bitvectors was not done when we introduced the concrete Bitvector module, but I think it shouldn't be hard to adapt our mappings to support the arbitrary width bitvectors in the solver.

[tiferrei]

Thanks for the fast reply!

I hit the assert false when making an Expr.relop with non-standard Bitv widths. I think binop, etc have the same behaviour.

Locally I hacked some horrible module IN backed by Z.t and at least functionality wise that seems to do it, but glad to know there's already more extensive Bitvector support!