Live Feedback through Incremental Program Analysis (Keynote)

doi:10.5381/jot.2026.25.1.a6

Live Feedback through Incremental Program Analysis (Keynote)

2026-01-01

0

PRE

AI

E

Erdweg, Sebastian *

DOI：10.5381/jot.2026.25.1.a6

原文链接

原文求助

摘要

En 中文

静态分析在现代软件开发中至关重要。静态分析最广为人知的是在编译时检测错误，从而帮助开发者编写正确的代码。这是一项值得称赞的追求，也因此静态分析有时被称为轻量级验证。但静态分析还有同等重要的第二个目标：辅助程序理解。开发工具（如IDE）利用静态分析计算的信息向开发者解释程序（变量v的类型为int，变量v1和v2指向同一对象）、提供探索功能（跳转到声明、查找调用点）、引导开发者（未初始化的读取、死代码），以及提供复杂的编辑操作（重构）。IDE必须在不妨碍开发者工作流程的情况下提供所有这些功能。特别是，IDE必须快速响应代码更改。也就是说，其底层的静态分析需要是增量的。我们提出了IncA，一个与语言无关的增量静态分析框架，且不牺牲精度。IncA提供了一个DSL（领域特定语言）用于静态分析的定义，并自动增量化这些分析。我们解释了IncA编译器如何将分析规范转换为Datalog风格的规则，以及IncA运行时如何增量求解这些规则。我们特别讨论了IncA如何增量化固定点计算，这在数据流分析中无处不在。IncA已被用于增量化C语言的控制流和指向分析、Java的字符串分析和强指向分析，以及Rust的类型分析。

Keyword:

Incremental static analysis

Program understanding

Data-flow analysis

Datalog

Fixpoint computation

Live Feedback through Incremental Program Analysis (Keynote)

摘要

期刊

机构

引用论文