Weakest precondition synthesis for compiler optimizations

Abstract. Compiler optimizations play an increasingly important role in code generation. This is especially true with the advent of resource-limited mobile devices. We rely on compiler optimizations to improve performance, reduce code size, and reduce power consumption of our programs. Despite being a mature field, compiler optimizations are still designed and implemented by hand, and usually without providing any guarantee of correctness. In addition to devising the code transformations, designers and imple-menters have to come up with an analysis that determines in which cases the optimization can be safely applied. In other words, the optimization designer has to specify a precondition that ensures that the optimization is semantics-preserving. However, devising preconditions for optimiza-tions by hand is a non-trivial task. It is easy to specify a precondition that, although correct, is too restrictive, and therefore misses some op-timization opportunities. In this paper, we propose, to the best of our knowledge, the first al-gorithm for the automatic synthesis of preconditions for compiler opti-mizations. The synthesized preconditions are provably correct by con-struction, and they are guaranteed to be the weakest in the precondition language that we consider. We implemented the proposed technique in a tool named PSyCO. We present examples of preconditions synthesized by PSyCO, as well as the results of running PSyCO on a set of optimizations.