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.