This semester, we are taking a class on Program Synthesis, which is studying how to write programs that can write programs for people. Recently, we have covered the paper "Synthesis of Loop Free Programs" which describes a procedure that can synthesize programs without loops within a theory. We decided to employ the procedure described in the paper and include a library of components for it that isn't in the paper to synthesize nontrivial programs that use bitwise operations.
What it does
Ideally, given a suboptimal C program, our program will enumerate through the possible implementations of that program to find a procedure that implements the same feature, but more efficiently. As of now, we have not had enough time to implement accepting C program inputs, and require a specification written in first order logic using the Microsoft Z3 solver, which is around the same difficulty to write as a C program. If an optimal program exists to implement that specification, the program will successfully find it and print out the corresponding C code. We have written specifications for several programs and the tool successfully synthesizes nontrivial solutions to these problems.
How we built it
We have implemented the key idea of the paper "Synthesis of Loop Free Programs" using Z3 as our SMT solver. Along with this, we have included a library of components the algorithm can use for synthesis instead of having the user input the components as the paper suggests. We have used the Python wrapper of the solver to make ease development.
Challenges we ran into
In the beginning, we were ambitious that we could abstract away the necessity of the user needing to provide a program specification in first order logic, since it is harder to write the specifications than the program itself in some cases. However, this task proved harder than we anticipated, as user specified intent may be ambiguous. We had the idea of using a parser to go through C code and capture intent from there, but we did not have enough time to implement it.
Accomplishments that we're proud of
We were able to make a functional tool that can sometimes write better programs than it's creators can!
What we learned
We learned a lot about first order logic, and about managing our time and picking goals that are ambitious, but achievable.
What's next for Program Programmer
Completing implementation of gathering user intent from inefficient C code, support for more complex programs and data structures.