Desyan：一个实现值流与符号分析无缝集成的平台
软件工程
2025-08-04 v1 编程语言
摘要
在过去的二十年中，两种不同类型的静态分析已成为学术界和工业界的主导范式：值流分析（例如，数据流分析或指向分析）和符号分析（例如，符号执行）。尽管它们在众多应用领域取得了各自的成功，但这两种方法在很大程度上仍然相互分离；这源于一个简单的事实：目前还没有一个广泛采用的统一平台，能够轻松高效地将符号技术与高性能数据流推理集成。为了弥合这一差距，我们引入了Desyan：一个用于编写程序分析的平台，实现了值流与符号推理的无缝集成。Desyan将一个生产就绪的Datalog不动点引擎(Soufflé)扩展为具备完整的SMT求解能力，调用业界领先的SMT引擎。Desyan提供了自动（且高效！）处理程序分析中常见模式的构造。同时，该集成与求解技术无关，并通过自底向上的代数推理模块支持Datalog原生的符号推理。其结果是一个引擎，允许根据需要为底层分析混合不同类型的推理。对于值流分析，该引擎是最佳类别的Datalog评估器（执行时间通常快20倍以上）；对于需要完整SMT的应用（例如，需要求解任意复杂条件的混合执行引擎或其他符号评估器），该引擎利用领先的SMT求解器；对于轻量级符号评估（例如，在路径敏感分析上下文中求解简单条件），该引擎可以使用Datalog原生的符号推理，与急切地调用SMT求解器相比，实现了大幅加速（通常超过2倍）。
引用
@article{arxiv.2508.00508,
title = {Desyan: A Platform for Seamless Value-Flow and Symbolic Analysis},
author = {Panagiotis Diamantakis and Thanassis Avgerinos and Yannis Smaragdakis},
journal= {arXiv preprint arXiv:2508.00508},
year = {2025}
}