paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Program Repair Guided by Datalog-Defined Static Analysis

由 Datalog 定义的静态分析引导的程序修复
FSE Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2023匹配度 2/10 · 论文属于纯静态分析与程序修复方向,提出 Datalog 符号执行来泛化程序修复,但不涉及 LLM/Agent、机器学习、浮点程序分析或贝叶斯程序分析,与用户画像的核心交叉方向基本无关。引用 23 inbox
Yu Liu, Sergey Mechtaev, Pavle Subotić, Abhik Roychoudhury
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:提出 Datalog 符号执行技术,将程序修复归约为修改 Datalog 事实,实现通用静态程序修复框架。

基于静态分析的自动程序修复无需失败测试即可修 bug,并能通过程序性质避免测试过拟合;但现有技术往往绑定特定分析器,只能修复很窄的缺陷类别。为构建面向多种性质与编程语言的通用静态修复框架,作者将程序修复与基于 Datalog 的分析相结合:被分析程序编码为 Datalog 事实,分析的不动点方程编码为递归 Datalog 规则,修复程序即修改相应的 Datalog 事实。为此提出 Datalog 的符号执行新技术,在符号事实库而非具体事实集上求值 Datalog 查询,从而推断出哪些事实改动能使程序满足期望的分析目标。作者实现了 Datalog 符号执行器 Symlog 及修复工具 SymlogRepair,并在多类分析问题上展示通用性:修复 Java 空指针异常、Python notebook 数据泄漏,以及 Solidity 智能合约中的四类安全漏洞。

问题
现有静态程序修复技术通常与特定分析器紧耦合,只能修复少数缺陷类别,难以面向多种程序性质和编程语言通用化。
方法
将程序编码为 Datalog 事实、将分析的不动点方程编码为递归 Datalog 规则,把修复视为修改 Datalog 事实;提出 Datalog 符号执行,在符号事实库上求值查询以推断达成分析目标的修复性改动。
评估
实现了 Datalog 符号执行器 Symlog 与修复工具 SymlogRepair,并在 Java 空指针异常、Python notebook 数据泄漏以及 Solidity 智能合约四类安全漏洞等分析问题上验证方法的通用性。
原文摘要(Abstract)

Automated program repair relying on static analysis complements test-driven repair, since it does not require failing tests to repair a bug, and it avoids test-overfitting by considering program properties. Due to the rich variety and complexity of program analyses, existing static program repair techniques are tied to specific analysers, and thus repair only narrow classes of defects. To develop a general-purpose static program repair framework that targets a wide range of properties and programming languages, we propose to integrate program repair with Datalog-based analysis. Datalog solvers are programmable fixed point engines which can be used to encode many program analysis problems in a modular fashion. The program under analysis is encoded as Datalog facts, while the fixed point equations of the program analysis are expressed as recursive Datalog rules. In this context, we view repairing the program as modifying the corresponding Datalog facts. This is accomplished by a novel technique, symbolic execution of Datalog, that evaluates Datalog queries over a symbolic database of facts, instead of a concrete set of facts. The result of symbolic query evaluation allows us to infer what changes to a given set of Datalog facts repair the program so that it meets the desired analysis goals. We developed a symbolic executor for Datalog called Symlog, on top of which we built a repair tool SymlogRepair. We show the versatility of our approach on several analysis problems --- repairing null pointer exceptions in Java programs, repairing data leaks in Python notebooks, and repairing four types of security vulnerabilities in Solidity smart contracts.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@inproceedings{LiuMSR23,
  title = {Program Repair Guided by Datalog-Defined Static Analysis},
  author = {Yu Liu and Sergey Mechtaev and Pavle Subotić and Abhik Roychoudhury},
  booktitle = {FSE},
  year = {2023},
  doi = {10.1145/3611643.3616363}
}