yotann / alive2 Goto Github PK

In cases where all loads and stores are aligned to, say, 16 bits, upstream Alive2 will actually set bits_byte to 16, meaning that each "byte" in the memory SMT arrays is actually a 16-bit bitvector. This optimization is presumably helpful to the SMT solver, but it isn't really useful for the interpreter and it would just complicate things.

The ideal solution would be to run translation validation with bits_byte>8 (when appropriate), convert everything to 8-bit bytes when generating the counterexample test input, and then run the interpreter with bits_byte=8. The difficult part would be dealing with default memory block bytes; we might need multiple default bytes for different offsets if bits_byte>8.

For now, I'm avoiding the issue by forcing bits_byte=8 in translation validation (implemented in 0eed0f7).