Abstract
In the third lecture, we looked at optimizations in compilers. These are program transformations that the compiler automatically applies to improve the performance of the generated code. Some optimizations apply unconditionally, but many others require a prior static analysis of the program to be compiled, in order to establish properties that are true of all program executions and without which the optimization would not apply.Dataflow analysis is a classic formalism for expressing several analyses as resolutions of flow equations guided by the program's control graph.
We have illustrated these concepts on an important analysis, variable liveliness analysis, and its use for two optimizations, dead code elimination and register allocation. We then mechanized this analysis, these two optimizations and their semantic correction demonstrations in Coq. The semantic characterization of the liveliness analysis is interesting because it is a hyper-property that links two executions of the same program in different states.
Finally, we took a closer look at the calculation of fixed points of increasing functions, a central operation in many static analyses. The Knaster-Tarski theorem shows the existence of such fixed points, and a constructive presentation of this theorem naturally leads to an algorithm for calculating fixed points.
