[FEATURE] Discussion: Compatibility with "theory of fixed size bit-vectors"

[leonbett]

In order to model constraints imposed by general purpose programs, the operations used in the program have to be translated to an ISLa constraint. Currently, ISLa supports some arithmetic operations on unbounded integers (add,sub,mul,div,mod). However, some widely used operations are currently not supported:

• Bit operations, including: bit-wise and, or, not, xor; zero- and sign-extension; bit shifting
• Some more subtle behavior of operations on fixed-size machine registers (e.g. unsigned int overflow)

Some of these can be modeled in ISLa. For instance, unsigned int overflow could be tackled by wrapping every arithmetic operations in a mod 2**REGISTER_BIT_WIDTH. However, I believe that most operations cannot be translated this way, to the "theory of strings". And even if there was a way, the resulting expressions would be unreadable. Moreover, specialized bit-vector solvers could not be leveraged, resulting in much longer solving times.

Supporting the "theory of fixed size bit-vectors" (which is natively supported by symbolic executors such as KLEE) could unlock a new application domain (modeling constraints found in general purpose programs).

[rindPHI]

I see. It would make sense to offer something like that. One way could be to use int2bv chained with str.to.int (a little ugly, but we could also add some shortcut to abbreviate this). To make that useable, additional magic like that currently in place for str.to.int and str.len will be necessary (to circumvent string solving entirely). I estimate three days of work if there are no problems. Maybe in the fall this year :P