9 ms·

Hmm. Would a SAT solver be useful for compiler technologies? A compiler is basically solving the problem of: here is a sequence of things I want done; here is

Hmm. Would a SAT solver be useful for compiler technologies? A compiler is basically solving the problem of: here is a sequence of things I want done; here is a description of what the machine can do; find a combination of the latter which achieves the former. The details are the tricky bit, particularly for unpleasantly asymmetric instruction sets like the old 8-bit architectures. It would be so nice if I could just throw a description of the problem at some sort of machine reasoning system and have it Just Work...

TheLoneWolfling 12y ago
There are superoptimizers that do exactly that. But current SAT solvers aren't powerful enough to do so at much more than a few tens of instructions long. Still useful though.
bronxbomber92 12y ago
Check out Alive http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 https://github.com/nunoplopes/alive https://github.com/nunoplopes/alive http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170
tikhonj 12y ago
Yes, although it's hard to make it scale in every case. What you're talking about sounds like the field of program synthesis[1], which uses SMT solvers (among other technologies) to generate code to some specification. I worked on a system[2] that used this sort of technique to optimize code for a weird architecture (GreenArrays' Forth-based chip[3]) and it was certainly much easier to implement than a classical optimizing compiler. Perhaps the most relevant example project here would be Rosette[4], which is basically a framework for easily writing synthesizers for different tasks. It would let you implement a description of your machine in Scheme (ie write a simple interpreter) and automatically generate a synthesizer for it that could compile programs in your language to formulas in a solver of some sort. [1]: http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-overview-notes.pdf http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-... [2]: http://jelv.is/chlorophyll.pdf http://jelv.is/chlorophyll.pdf [3]: http://www.greenarraychips.com/ http://www.greenarraychips.com/ [4]: http://homes.cs.washington.edu/~emina/rosette/ http://homes.cs.washington.edu/~emina/rosette/
- david-given 12y ago
  Hey, GreenArrays! I did code generation for the ShBoom / PSC1000 once --- heavily bending a traditional register-centric compiler architecture to produce terrible, terrible code. Fascinating processor, though. And I have an MSP430 right here on my desk. I'm afraid your paper is largely beyond me, though, but I'll go read up on program synthesis. Thanks!
tomp 12y ago
It could be useful for future compilers and languages that use refined types (e.g. `x : int if x > 0`). Check out Liquid Haskell!

TheLoneWolfling 12y ago

There are superoptimizers that do exactly that. But current SAT solvers aren't powerful enough to do so at much more than a few tens of instructions long. Still useful though.

bronxbomber92 12y ago

Check out Alive http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 https://github.com/nunoplopes/alive https://github.com/nunoplopes/alive http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170

tikhonj 12y ago

Yes, although it's hard to make it scale in every case. What you're talking about sounds like the field of program synthesis[1], which uses SMT solvers (among other technologies) to generate code to some specification. I worked on a system[2] that used this sort of technique to optimize code for a weird architecture (GreenArrays' Forth-based chip[3]) and it was certainly much easier to implement than a classical optimizing compiler. Perhaps the most relevant example project here would be Rosette[4], which is basically a framework for easily writing synthesizers for different tasks. It would let you implement a description of your machine in Scheme (ie write a simple interpreter) and automatically generate a synthesizer for it that could compile programs in your language to formulas in a solver of some sort. [1]: http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-overview-notes.pdf http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-... [2]: http://jelv.is/chlorophyll.pdf http://jelv.is/chlorophyll.pdf [3]: http://www.greenarraychips.com/ http://www.greenarraychips.com/ [4]: http://homes.cs.washington.edu/~emina/rosette/ http://homes.cs.washington.edu/~emina/rosette/

david-given 12y ago
Hey, GreenArrays! I did code generation for the ShBoom / PSC1000 once --- heavily bending a traditional register-centric compiler architecture to produce terrible, terrible code. Fascinating processor, though. And I have an MSP430 right here on my desk. I'm afraid your paper is largely beyond me, though, but I'll go read up on program synthesis. Thanks!

tomp 12y ago

It could be useful for future compilers and languages that use refined types (e.g. `x : int if x > 0`). Check out Liquid Haskell!