| This dissertation presents a translation validation framework for verifying optimizing compilers. Our validation work is focused on loop optimizations since loops are generally hard to analyze and many problems occurred in verifying loop optimizations. To solve these problems, a set of theories and algorithms are proposed, and they are implemented in our validation tool called TVOC.;In order to validate the optimizations performed by the compiler, we try to prove the equivalence of the intermediate codes before and after the optimizations. A set of proof rules were previously proposed to build the equivalence relation between two programs. However, they cannot validate some cases with legal loop optimizations. We improve these proof rules to consider the conditions of loops and possible eliminations of some loops, so that those cases can also be handled. According to the new proof rules, algorithms are designed to apply them to an automatic validation process.;Based on the above proof rules, our validation tool TVOC validates compiler optimizations by analyzing the original and optimized codes and generating checkable verification conditions. Previously TVOC only dealt with optimizations which do not significantly change the structure of the code, while loop optimizations do change the structure greatly. We build a new part of TVOC treating loop optimizations separately, which guesses what kinds of loop optimizations happened, analyzes the loops, proves the validity of a combination of loop optimizations, and synthesize a series of intermediate codes. With this new part, TVOC has succeeded in validating many examples with loop optimizations.;Speculative optimizations are the aggressive optimizations which are only correct under certain conditions that cannot be known at compile time. In this dissertation, we present the theory and algorithms of validating speculative optimizations and generating the runtime tests necessary for speculative optimizations. We also provide several examples and the results of the algorithms for speculative optimizations. |
