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