SPARTA

SPARTA 是一个软件组件库，专门设计用于根据抽象解释理论构建高性能静态分析器。

抽象解释

抽象解释 是一种语义近似理论，为静态程序分析器的设计提供了一个基础框架。按照抽象解释方法论构建的静态分析器在数学上是合理的，即它们计算的语义信息在所有可能的执行上下文中都得到保证。此外，这些分析器能够推断出程序复杂的属性，其表达性可以精细调整以控制分析时间。基于抽象解释的静态分析器通常用于航空航天工业中飞行软件的正式验证，例如。

为什么选择SPARTA？

从头开始构建基于抽象解释的工业级静态分析工具是一项艰巨的任务，需要领域专家的注意。SPARTA 的目的是通过提供一套具有简单API、高性能且易于组装的软件组件来极大地简化抽象解释的工程。通过封装抽象解释的复杂实现细节，SPARTA 让工具开发者能够专注于分析设计的三个基本轴

• 语义： 要分析的程序属性（数值变量的范围、别名关系等）
• 划分： 分析属性的粒度（过程内、过程间、上下文相关等）
• 抽象： 程序属性的表示（符号、区间、别名图等）

SPARTA 是 Semantics（语义）、PARTitioning（划分）和 Abstraction（抽象）的缩写。

SPARTA for C++ 是驱动 ReDex Android 字节码优化器大多数优化过程的分析引擎。ReDex 代码库包含了多个使用 SPARTA 构建的工业规模分析示例。交互式程序常数传播（interprocedural constant propagation）展示了如何组装 SPARTA 提供的构建块以实现复杂且可扩展的分析。

SPARTA in Rust

SPARTA for Rust 已作为 crate 发布在 crates.io 上。它目前处于实验阶段，无法保证 API 不会更改。到目前为止，我们已经重新实现了 C++ 版本中的基本功能，即

• 抽象域：SPARTA crate 将抽象域建模为一个 trait。C++ 版本使用 CRTP 和 static_asserts 来确保用户定义的类型满足抽象域的质量要求。在 Rust 中这不再是必需的。
• 数据结构：我们实现了基于 PatriciaTree 的 Set 和 Map 容器以及抽象域。
• 图 trait：SPARTA 的 fixpoint 迭代器可以在用户定义的、实现了 sparta::graph::Graph trait 的图类型上操作。这类似于 C++ 中的 Graph 接口，它使用 CRTP 实现编译时多态。
• 弱部分排序：这是对论文中描述的弱拓扑排序的替代。Sung Kook Kim, Arnaud J. Venet, 和 Aditya V. Thakur. 2019. 确定性并行 fixpoint 计算。Proc. ACM Program. Lang. 4, POPL, 文章 14（2020 年 1 月），33 页。 https://doi.org/10.1145/3371082https://dl.acm.org/doi/10.1145/3371082
• fixpoint 迭代：基于弱部分排序的单线程 fixpoint 迭代器。

问题

GitHub 上的问题被分配了优先级，这些优先级反映了它们的紧急程度以及它们被解决的可能性。

• P0：立即修复！一个严重的问题，应该有人现在正在解决。
• P1：高优先级。一个重要的问题，应该有人积极解决。
• P2：中等优先级。一个重要的问题，它很快将被处理。
• P3：低优先级。一个重要的问题，可能在未来某个时候处理。
• P4：愿望清单。一个有价值的但优先级低的问题，可以尝试解决，但如果在一定时间内没有解决，可能会被修剪。

许可

SPARTA 使用 MIT 许可证，请参阅此源代码树根目录下的 LICENSE 文件。