Algorithmic optimizations

Compilers and programming environments use program analyses to determine the safety of code transformations. Often, these program analyses are too conservative. As a result, the compiler or programming environment will consider many transformations unsound.;This affects aggressive or large-scale program transformations: As such transformations have complex requirements for their soundness, they are affected disproportionately. In practice, this causes almost any complex program analysis to be rejected.;One reason for this conservativeness is that optimizations attempt to preserve the semantics of the program as defined by the programming language, even if those semantics were never intended by the programmer. This can be avoided if the user adds annotations to the program. Such annotations relax the semantics and cause program analyses to have better results. In turn, fewer code transformations will be rejected.;However, specifying the intended semantics is tedious: First, programs are large. To fully annotate all parts, a programmer requires a lot of time. Second, there are many annotations a programmer could place. To fully annotate even a single line of a program, a programmer has to specify many properties. These issues force the programmer to place annotations that do not affect the intended transformations: A small subset of the intended semantics is sufficient to improve the results of most analyses. Specifying the entire intended semantics therefore is not practical.;We present an approach that identifies the intended semantics of a program. Our system guides the user into specifying parts of the intended semantics that aid analyses results. With this guidance, a user can avoid specifying irrelevant parts of the intended semantics. This reduces the effort he needs to invest.;We use our system to apply large-scale and aggressive optimizations. We call these algorithmic optimizations. Using a specification of the optimizations, our system determines why the optimizations fail. It identifies which failure causes are the most important ones and estimates the expected benefit gained from specifying the users intended semantics. Using this data as guidance, the user then can add specifications and subsequently apply the optimizations safely.