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.