标题： Desyan：一个无缝价值流和符号分析的平台 显示英文标题

标题： Desyan: A Platform for Seamless Value-Flow and Symbolic Analysis

摘要： 在过去二十年中，两种不同的静态分析方法在学术界和工业界已成为主导范式：价值流分析（例如，数据流分析或指针分析）和符号分析（例如，符号执行）。尽管这两种方法在许多应用领域取得了各自的成功，但两者仍然 largely 分离；这是由于缺乏一个广泛采用的统一平台，使得符号技术与高性能数据流推理的无缝高效集成变得困难。为了弥合这一差距，我们引入了 Desyan：一个用于编写程序分析的平台，能够无缝集成价值流和符号推理。Desyan 扩展了一个生产就绪的 Datalog 固定点引擎（Soufflé），并完全集成了 SMT 求解，调用行业领先的 SMT 引擎。Desyan 提供了构造，用于自动（并且高效地）处理程序分析中常见的典型模式。同时，这种集成与求解技术无关，并通过自底向上的代数推理模块支持原生 Datalog 符号推理。结果是一个允许根据底层分析需要混合不同种类推理的引擎。对于价值流分析，该引擎是同类最佳的 Datalog 评估器（通常在执行时间上超过 20 倍）；对于需要完整 SMT 的应用（例如，一个协同执行引擎或其他需要解决任意复杂条件的符号求解器），该引擎利用领先的 SMT 求解器；对于轻量级符号求解（例如，在路径敏感分析的上下文中求解简单的条件），该引擎可以使用原生 Datalog 符号推理，与急于调用 SMT 求解器相比，通常能获得超过 2 倍的速度提升。 显示英文摘要

摘要： Over the past two decades, two different types of static analyses have emerged as dominant paradigms both in academia and industry: value-flow analysis (e.g., data-flow analysis or points-to analysis) and symbolic analysis (e.g., symbolic execution). Despite their individual successes in numerous application fields, the two approaches have remained largely separate; an artifact of the simple reality that there is no broadly adopted unifying platform for effortless and efficient integration of symbolic techniques with high-performance data-flow reasoning. To bridge this gap, we introduce Desyan: a platform for writing program analyses with seamless integration of value-flow and symbolic reasoning. Desyan expands a production-ready Datalog fixpoint engine (Souffl\'e) with full-fledged SMT solving invoking industry-leading SMT engines. Desyan provides constructs for automatically (and efficiently!) handling typical patterns that come up in program analysis. At the same time, the integration is agnostic with respect to the solving technology, and supports Datalog-native symbolic reasoning, via a bottom-up algebraic reasoning module. The result is an engine that allows blending different kinds of reasoning, as needed for the underlying analysis. For value-flow analysis, the engine is the best-in-class Datalog evaluator (often by a factor of over 20x in execution time); for applications that require full SMT (e.g., a concolic execution engine or other symbolic evaluator that needs to solve arbitrarily complex conditions), the engine is leveraging the leading SMT solvers; for lightweight symbolic evaluation (e.g., solving simple conditionals in the context of a path-sensitive analysis), the engine can use Datalog-native symbolic reasoning, achieving large speedups (often of over 2x) compared to eagerly appealing to an SMT solver.