Leveraging Rust Types for Program Synthesis
Leveraging Rust Types for Program Synthesis
复制标题
DOI：
10.1145/3591278
复制
发表时间：
2023-06-01
影响因子：
1.8
通讯作者：
Sergey，Ilya
中科院分区：
文献类型：
--
作者：
Fiala，Jonas;Itzhaky，Shachar;Sergey，Ilya
Rust 类型系统保证内存安全和数据竞争自由。然而，为了满足 Rust 的类型规则，许多熟悉的实现模式必须进行大幅调整。这些必要的调整使编程变得复杂，并可能阻碍语言的采用。在本文中，我们证明，与手动编程相比，自动合成并不因 Rust 的类型系统而变得复杂，而是在两个主要方面受益。首先，Rust 合成器可以摆脱明显简单的规范。虽然在更传统的命令式语言中，合成器通常需要复杂逻辑中的冗长注释来描述数据结构的形状、别名和潜在的副作用，但在 Rust 中，所有这些信息都可以从类型中推断出来，让用户专注于使用 Rust 表达式的轻微扩展来指定功能属性。其次，Rust 类型系统减少了合成的搜索空间，从而提高了性能。在这项工作中，我们提出了第一种在安全 Rust 中自动合成正确构造程序的方法。我们的综合过程的关键要素是综合所有权逻辑，这是一种新的程序逻辑，用于派生程序，保证满足用户提供的功能规范，而且重要的是，满足 Rust 复杂的类型系统。我们在一个名为 RusSOL 的新工具中实现了这个逻辑。我们的评估显示了 RusSOL 在为新 Rust 开发人员面临的常见问题综合可证明正确的解决方案方面的有效性，无论是在注释负担还是性能方面。
The Rust type system guarantees memory safety and data-race freedom. However, to satisfy Rust's type rules, many familiar implementation patterns must be adapted substantially. These necessary adaptations complicate programming and might hinder language adoption. In this paper, we demonstrate that, in contrast to manual programming, automatic synthesis is not complicated by Rust's type system, but rather benefits in two major ways. First, a Rust synthesizer can get away with significantly simpler specifications. While in more traditional imperative languages, synthesizers often require lengthy annotations in a complex logic to describe the shape of data structures, aliasing, and potential side effects, in Rust, all this information can be inferred from the types, letting the user focus on specifying functional properties using a slight extension of Rust expressions. Second, the Rust type system reduces the search space for synthesis, which improves performance.In this work, we present the first approach to automatically synthesizing correct-by-construction programs in safe Rust. The key ingredient of our synthesis procedure is Synthetic Ownership Logic, a new program logic for deriving programs that are guaranteed to satisfy both a user-provided functional specification and, importantly, Rust's intricate type system. We implement this logic in a new tool called RusSOL. Our evaluation shows the effectiveness of RusSOL, both in terms of annotation burden and performance, in synthesizing provably correct solutions to common problems faced by new Rust developers.