A formal foundation for symbolic evaluation with merging
A formal foundation for symbolic evaluation with merging
复制标题
合并符号评估的正式基础
DOI：
10.1145/3498709
复制
发表时间：
2022
影响因子：
--
通讯作者：
Torlak, Emina
中科院分区：
文献类型：
--
作者：
Porncharoenwase, Sorawee;Nelson, Luke;Wang, Xi;Torlak, Emina
可重复使用的符号求值器是求解器辅助验证和综合工具的关键构建块。可重用的求值器将程序中所有路径的语义简化为逻辑约束，并且客户端工具使用这些约束来制定由 SAT 或 SMT 求解器释放的可满足性查询。评估器的正确性对于工具的健全性及其旨在保证的领域属性至关重要。然而到目前为止，对这些评估器的信任一直建立在测试和手动推理的临时基础上。本文提出了第一个用于推理可重用符号评估器行为的正式框架。我们为这些评估器开发了一种新的符号语义，其中包含状态合并。符号求值器使用状态合并来避免路径爆炸并生成紧凑的编码。为了适应广泛的实现，我们的语义由符号工厂参数化，它抽象了符号值的合并和创建的细节。语义的目标是一种丰富的语言，它通过假设和断言扩展了核心方案，从而支持分支、循环和（一流）过程。语义旨在通过保证两个关键属性来支持可重用性：生成的符号状态的合法性以及符号评估到具体评估的可还原性。合法性使客户端工具更容易制定查询，而可简化性使客户端工具能够根据具体输入进行测试。我们使用 Lean 定理证明器来机械化我们的符号语义，证明它在具体语义方面是健全和完整的，并证明它保证合法性和可还原性。为了证明我们语义的通用性，我们开发了 Leanette（用 Lean 编写的参考评估器）和 Rosette 4（用 Racket 编写的优化评估器）。我们证明 Leanette 在语义方面是正确的，并通过求解器辅助差分测试验证 Rosette 4 与 Leanette 的对比。为了证明我们方法的实用性，我们将 16 个已发布的验证和综合工具从 Rosette 3 移植到 Rosette 4。Rosette 3 是一个现有的可重用评估器，它实现了经典的合并语义，采用了有界模型检查。 Rosette 4 取代了 Rosette 3 的语义核心，但保留了其优化的符号工厂。我们的结果表明，Rosette 4 在广泛的基准测试中与 Rosette 3 的性能相匹配，同时提供了更清晰的界面，简化了客户端工具的实施。
Reusable symbolic evaluators are a key building block of solver-aided verification and synthesis tools. A reusable evaluator reduces the semantics of all paths in a program to logical constraints, and a client tool uses these constraints to formulate a satisfiability query that is discharged with SAT or SMT solvers. The correctness of the evaluator is critical to the soundness of the tool and the domain properties it aims to guarantee. Yet so far, the trust in these evaluators has been based on an ad-hoc foundation of testing and manual reasoning.This paper presents the first formal framework for reasoning about the behavior of reusable symbolic evaluators. We develop a new symbolic semantics for these evaluators that incorporates state merging. Symbolic evaluators use state merging to avoid path explosion and generate compact encodings. To accommodate a wide range of implementations, our semantics is parameterized by a symbolic factory, which abstracts away the details of merging and creation of symbolic values. The semantics targets a rich language that extends Core Scheme with assumptions and assertions, and thus supports branching, loops, and (first-class) procedures. The semantics is designed to support reusability, by guaranteeing two key properties: legality of the generated symbolic states, and the reducibility of symbolic evaluation to concrete evaluation. Legality makes it simpler for client tools to formulate queries, and reducibility enables testing of client tools on concrete inputs. We use the Lean theorem prover to mechanize our symbolic semantics, prove that it is sound and complete with respect to the concrete semantics, and prove that it guarantees legality and reducibility.To demonstrate the generality of our semantics, we develop Leanette, a reference evaluator written in Lean, and Rosette 4, an optimized evaluator written in Racket. We prove Leanette correct with respect to the semantics, and validate Rosette 4 against Leanette via solver-aided differential testing. To demonstrate the practicality of our approach, we port 16 published verification and synthesis tools from Rosette 3 to Rosette 4. Rosette 3 is an existing reusable evaluator that implements the classic merging semantics, adopted from bounded model checking. Rosette 4 replaces the semantic core of Rosette 3 but keeps its optimized symbolic factory. Our results show that Rosette 4 matches the performance of Rosette 3 across a wide range of benchmarks, while providing a cleaner interface that simplifies the implementation of client tools.
登录
查看更多内容
Ruby 的细化类型
DOI：
--
发表时间：
2018
期刊：
and Abstract Interpretation - VMCAI'18
影响因子：
--
作者：
Kazerounian, Milod;Vazou, Niki;Bourgerie, Austin;Foster, Jeff;Torlak, Emina
通讯作者：
Torlak, Emina
用于非纯函数语言的经过验证的编译器
DOI：
--
发表时间：
2010
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
A. Chlipala
通讯作者：
A. Chlipala
ACL2 定理证明器中经过验证的符号执行框架
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
S. Swords
通讯作者：
S. Swords
影响因子：
0.7
作者：
D. Lucanu;Vlad Rusu;Andrei Arusoaie
通讯作者：
Andrei Arusoaie
一种可编程的编程语言
影响因子：
22.7
作者：
M. Felleisen;R. Findler;M. Flatt;S. Krishnamurthi;Eli Barzilay;J. McCarthy;Sam Tobin
通讯作者：
Sam Tobin