5 ms·

Verifying GCC optimizations using an SMT solver

121 points by signa11 4y ago

sylware 4y ago
In "serious and critical" code, only the machine code would be "verified". And each time the machine code change, "verification" has to be done all over again.
- MaxBarraclough 4y ago
  > In "serious and critical" code, only the machine code would be "verified". As I understand it, this approach is not at all common in critical code. The SeL4 folks did some interesting work verifying assembly code, [0] but I'm not aware of anyone else doing anything similar. Also, there's no need for scare-quotes. Verification is standard terminology in this field. [0] https://entropy2018.sciencesconf.org/data/myreen.pdf https://entropy2018.sciencesconf.org/data/myreen.pdf
DannyBee 4y ago
Yeah, this kind of thing is nice. Alive had been used for years (almost a decade actually) by people to verify LLVM instcombine transforms. Alive2 (https://github.com/AliveToolkit/alive2 https://github.com/AliveToolkit/alive2) makes it easier to do the same with most optimization passes.
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 ago
  You 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
tannhaeuser 4y ago
There's this cool project using z3 (and racket) for formalizing CSS rendering [1] I never came around to lift for anything. Maybe someone else interested in leading the web out of the dark ages and give W3C's CSS WG an idea what we expect from them will. [1]: https://github.com/uwplse/cassius https://github.com/uwplse/cassius

121 points by signa11 4y ago

In "serious and critical" code, only the machine code would be "verified". And each time the machine code change, "verification" has to be done all over again.

MaxBarraclough 4y ago
> In "serious and critical" code, only the machine code would be "verified". As I understand it, this approach is not at all common in critical code. The SeL4 folks did some interesting work verifying assembly code, [0] but I'm not aware of anyone else doing anything similar. Also, there's no need for scare-quotes. Verification is standard terminology in this field. [0] https://entropy2018.sciencesconf.org/data/myreen.pdf https://entropy2018.sciencesconf.org/data/myreen.pdf

DannyBee 4y ago

Yeah, this kind of thing is nice. Alive had been used for years (almost a decade actually) by people to verify LLVM instcombine transforms. Alive2 (https://github.com/AliveToolkit/alive2 https://github.com/AliveToolkit/alive2) makes it easier to do the same with most optimization passes.

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 ago
You 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

tannhaeuser 4y ago

There's this cool project using z3 (and racket) for formalizing CSS rendering [1] I never came around to lift for anything. Maybe someone else interested in leading the web out of the dark ages and give W3C's CSS WG an idea what we expect from them will. [1]: https://github.com/uwplse/cassius https://github.com/uwplse/cassius