Effective, Efficient, and Correct Software Analysis and Optimization Tools

我们的现代社会越来越依赖于计算机软件的可靠性、安全性和保密性。 然而，分析软件并将其转换为可执行形式的编译器和其他工具可能会造成一个关键瓶颈：如果编译器出现错误，那么由它编译的任何软件都可能会受到损害。该项目通过开发有效、高效和正确的语言和工具实现技术来解决这一根本问题。 该项目的核心是程序分析和转换，即优化编译器和软件分析工具的核心，是用一种名为 Rhodium 的专门语言编写的。 通过专注于这个领域，构建一个全自动正确性检查器变得可行，以确保 Rhodium 分析和转换能够保留其处理的任何程序的行为。之前的工作开发了一个概念验证的 Rhodium 系统，并在一系列程序内优化中进行了演示。 该项目正在开发新技术，使Rhodium系统能够扩展到更丰富、更现实的设置，包括优化全功能面向对象和函数式语言的能力、执行可扩展的过程间分析、高效执行以及涵盖优化编译器和软件检查工具的“中端”的全部任务。

Our modern society increasingly depends on the reliability, safety, and security of computer software. However, the compilers and other tools that analyze and translate the software into executable form can create a critical bottleneck: if a compiler has an error, then any software compiled by it may in turn be compromised.This project addresses this fundamental problem by developing effective, efficient, and correct language and tool implementation technology. Central to the project is that program analyses and transformations, the heart of optimizing compilers and software analysis tools, are written in a specialized language, named Rhodium. By focusing on this domain, it becomes feasible to build a fully-automatic correctness checker that ensures that Rhodium analyses and transformations are guaranteed to preserve the behavior of any program they process.Previous work developed a proof-of-concept Rhodium system, and demonstrated it on a range of intraprocedural optimizations. This project is developing new techniques that will allow the Rhodium system to scale to richer and more realistic settings, including the ability to optimize full-featured object-oriented and functional languages, perform scalable interprocedural analyses, execute with high efficiency, and cover the full range of tasks in the "middle-end" of optimizing compilers and software checking tools.