[david-given]

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

[tikhonj]

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

[2]: http://jelv.is/chlorophyll.pdf

[3]: http://www.greenarraychips.com/

[4]: http://homes.cs.washington.edu/~emina/rosette/

[david-given]

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!

[bronxbomber92]

Check out Alive

http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15

https://github.com/nunoplopes/alive

http://blog.regehr.org/archives/1170

[tomp]

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]

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.