Verified Dataflow Analysis and Optimizations
From PUMA Graduiertenkolleg
The verification of simple optimizations such as constant propagation, redundancy or dead code elimination is rather obvious and has already been realized as part of the verified C-compiler of Leroy's team.
Within the doctorate program, we therefore concentrate on more sophisticated transformations which not only consist in canceling certain superfluous sub-computations. Here, we think of elimination of partial redundancies or partial dead code. Further challenges are optimizations beyond procedure boundaries such as last call optimization or variants of interprocedural constant propagation with procedure specialization.
For the optimization of a last call, e.g., it must be guaranteed that after entering the last call, no variable of the caller can be accessed (Escape analysis). Moreover, before procedure specialization, one would like to guarantee that a given argument may take values only in a small range.