3 ms·
z3 is so cool. I used it in the same way you used it for optimizations to make sure the transformations my obfuscating LLVM pass was making were correct. Comp
by from 4y ago
z3 is so cool. I used it in the same way you used it for optimizations to make sure the transformations my obfuscating LLVM pass was making were correct.
Compilers can even tell that
int count(uint64_t x) {
int v = 0;
while(x != 0) {
x &= x - 1;
v++;
}
return v;
}
is the same as the popcnt instruction. Though I’m not sure it’s possible to transform that loop into terms Z3 can understand.
- aseipp 4y agoYou can't easily translate generalized unbounded loops into a solver (it introduces quantifiers that make things nasty; e.g. proving something about strcpy(x, n) forall x, n; translates to nested quantifier which gets hairy and requires you to boil oceans, but proving something about strcpy(x, N) for a fixed N is much simpler.) But in this case you can effectively unroll a lot of those loops assuming you can prove the necessary termination criteria about them. Here in your example the criteria is effectively a kind of structural induction on the input bit vector x (because it can be proven forall x. (x > (x & (x-1))), where bitwidth(x) = fixed N) so it's not hard to see it will terminate. So that's what would happen here, and you'd then feed the unrolled bitwise algorithm into Z3 instead.
- mhh__ 4y ago> even Unless you go really far into research/toy optimizations this is more of a pattern match than the compiler figuring it out by itself