Speeding up compiled code with SAT

[Mate Soos <mate at srlabs dot de>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi All,

This idea has been brewing in my head lately. Basically, when I think
about the simplification steps that GCC does, it reminds me of applying
algebraic tautologies to simplify equations. The problem with that is
that there is no real reasoning involved, by which I mean that when a
propagation of a truth is not possible any further, we put our hands in
the air. SAT solvers go around this by guessing values, deriving
conflicts, trying to resolve the problem using the DPLL algorithm --
which is worst-case exponential of course, so it can be slow (but
usually isn't).

The point is that maybe we could try to use some real reasoning (not
just fact propagation) on the internal representation that GCC builds
from the code. This could be just a tech demo, and then later integrated
into GCC as a plug-in to do e.g. final compilations of stuff like
Firefox, where if the final compilation takes 1 CPU year, it's fine.
This could allow us to do some really whacky automated reasoning to
speed up complied code. Naturally, we would still need to limit the
reasoning engine (by e.g. number of conflicts derived), and throw our
hands in the air if nothing gets derived within that limit.

I could come up with any number of possibilities how this would speed up
compiled code, but I will save that to your imagination -- I am guessing
you know much more about this part than me. I am just a SAT solver guy.

Anyone thinks this may not be impossible? Or has this already been done?

Mate

- -- 
Mate Soos
Security Research Labs
http://www.srlabs.de
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk2oT4sACgkQsTOOstKb0jlxDgCcDr2Ao9BBL9ujNgzzX976wzlj
pBAAn2xZNsjVG8+lpKPNRJplmGxWP045
=/bTS
-----END PGP SIGNATURE-----